litex/stmt/
definition_stmt.rs

1use crate::{
2    common::keywords::GREATER_EQUAL,
3    prelude::*,
4    stmt::parameter_def::{ParamGroupWithStructFieldType, StructFieldType},
5};
6use std::fmt;
7
8#[derive(Clone)]
9pub struct HaveFnByInducNestedCase {
10    pub case_fact: AndChainAtomicFact,
11    pub equal_to: Obj,
12}
13
14#[derive(Clone)]
15pub enum HaveFnByInducLastCase {
16    EqualTo(Obj),
17    NestedCases(Vec<HaveFnByInducNestedCase>),
18}
19
20// have fn by induc from 0: f(x Z: x >= 0) R:
21//     case 0: 1
22//     case 1: 1
23//     case >= 2:
24//         case x % 2 = 0: f(x / 2)
25//         case x % 2 = 1: f(x / 2) + f(x / 2 + 1)
26#[derive(Clone)]
27pub struct HaveFnByInducStmt {
28    pub induc_from: Obj,
29    pub name: String,
30    pub param: String,
31    pub ret_set: Obj,
32    pub special_cases_equal_tos: Vec<Obj>,
33    pub last_case: HaveFnByInducLastCase,
34    pub line_file: LineFile,
35}
36
37#[derive(Clone)]
38pub struct DefAbstractPropStmt {
39    pub name: String,
40    pub params: Vec<String>,
41    pub line_file: LineFile,
42}
43
44impl DefAbstractPropStmt {
45    pub fn new(name: String, params: Vec<String>, line_file: LineFile) -> Self {
46        DefAbstractPropStmt {
47            name,
48            params,
49            line_file,
50        }
51    }
52}
53
54#[derive(Clone)]
55pub struct DefStructStmt {
56    pub name: String,
57    pub param_defs: Vec<ParamGroupWithStructFieldType>,
58    pub dom_facts: Vec<OrAndChainAtomicFact>,
59    pub fields: Vec<(String, StructFieldType)>,
60    pub facts: Vec<OrAndChainAtomicFact>,
61    pub line_file: LineFile,
62}
63
64#[derive(Clone)]
65pub struct DefFamilyStmt {
66    pub name: String,
67    pub params_def_with_type: Vec<ParamGroupWithParamType>,
68    pub dom_facts: Vec<OrAndChainAtomicFact>,
69    pub equal_to: Obj,
70    pub line_file: LineFile,
71}
72
73/// `have fn` 里 `{ … }` 一段的源码形态：形参名为用户符，dom/ret 中标识符亦为源码名；**不含** `__` mangling。
74/// 需要存入 `Obj::FnSet` 时由 [`Runtime::fn_set_for_storage_from_have_fn_clause`] 生成存储用 [`FnSet`]。
75#[derive(Clone)]
76pub struct FnSetClause {
77    pub params_def_with_set: Vec<ParamGroupWithSet>,
78    pub dom_facts: Vec<OrAndChainAtomicFact>,
79    pub ret_set: Obj,
80}
81
82#[derive(Clone)]
83pub struct HaveFnEqualCaseByCaseStmt {
84    pub name: String,
85    pub fn_set_clause: FnSetClause,
86    pub cases: Vec<AndChainAtomicFact>,
87    pub equal_tos: Vec<Obj>,
88    pub line_file: LineFile,
89}
90
91#[derive(Clone)]
92pub struct HaveFnEqualStmt {
93    pub name: String,
94    pub fn_set_clause: FnSetClause,
95    pub equal_to: Obj,
96    pub line_file: LineFile,
97}
98
99#[derive(Clone)]
100pub struct HaveByExistStmt {
101    pub equal_tos: Vec<String>,
102    pub exist_fact_in_have_obj_st: ExistFact,
103    pub line_file: LineFile,
104}
105
106#[derive(Clone)]
107pub struct HaveObjEqualStmt {
108    pub param_def: Vec<ParamGroupWithParamType>,
109    pub objs_equal_to: Vec<Obj>,
110    pub line_file: LineFile,
111}
112
113#[derive(Clone)]
114pub struct HaveObjInNonemptySetOrParamTypeStmt {
115    pub param_def: Vec<ParamGroupWithParamType>,
116    pub line_file: LineFile,
117}
118
119#[derive(Clone)]
120pub struct DefLetStmt {
121    pub param_def: Vec<ParamGroupWithParamType>,
122    pub facts: Vec<Fact>,
123    pub line_file: LineFile,
124}
125
126#[derive(Clone)]
127pub struct DefPropStmt {
128    pub name: String,
129    pub params_def_with_type: Vec<ParamGroupWithParamType>,
130    pub iff_facts: Vec<Fact>,
131    pub line_file: LineFile,
132}
133
134impl fmt::Display for DefAbstractPropStmt {
135    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
136        write!(
137            f,
138            "{} {}{}{}{}",
139            ABSTRACT_PROP,
140            self.name,
141            LEFT_BRACE,
142            vec_to_string_join_by_comma(&self.params),
143            RIGHT_BRACE
144        )
145    }
146}
147
148impl fmt::Display for DefStructStmt {
149    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
150        // 格式: struct name(params): \n  field1 or1 \n  field2 or2 \n  <=>: \n  facts...
151        // 解析器会为每个类型参数自动前置一条 field；Display 只还原用户写出来的字段。
152        let implicit_prefix_len = ParamGroupWithStructFieldType::number_of_params(&self.param_defs);
153        let fields_str: String = self
154            .fields
155            .iter()
156            .skip(implicit_prefix_len)
157            .map(|(name, or_val)| format!("{} {}", name, or_val))
158            .collect::<Vec<_>>()
159            .join("\n");
160        let fields_indented =
161            to_string_and_add_four_spaces_at_beginning_of_each_line(&fields_str, 1);
162        let equiv_line = add_four_spaces_at_beginning(format!("{}{}", EQUIVALENT_SIGN, COLON), 1);
163        let facts_indented = vec_to_string_add_four_spaces_at_beginning_of_each_line(
164            &self
165                .facts
166                .iter()
167                .skip(implicit_prefix_len)
168                .cloned()
169                .collect(),
170            1,
171        );
172        write!(
173            f,
174            "{} {}{}{}{} {}\n{}\n{}\n{}",
175            STRUCT,
176            self.name,
177            LEFT_BRACE,
178            vec_to_string_join_by_comma(&self.param_defs),
179            RIGHT_BRACE,
180            COLON,
181            fields_indented,
182            equiv_line,
183            facts_indented
184        )
185    }
186}
187
188impl DefPropStmt {
189    pub fn new(
190        name: String,
191        params_def_with_type: Vec<ParamGroupWithParamType>,
192        iff_facts: Vec<Fact>,
193        line_file: LineFile,
194    ) -> Self {
195        DefPropStmt {
196            name,
197            params_def_with_type,
198            iff_facts,
199            line_file,
200        }
201    }
202}
203
204impl fmt::Display for DefPropStmt {
205    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
206        match self.iff_facts.len() {
207            0 => write!(
208                f,
209                "{} {}{}",
210                PROP,
211                self.name,
212                braced_vec_to_string(&self.params_def_with_type)
213            ),
214            _ => write!(
215                f,
216                "{} {}{}{}\n{}",
217                PROP,
218                self.name,
219                braced_vec_to_string(&self.params_def_with_type),
220                COLON,
221                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.iff_facts, 1)
222            ),
223        }
224    }
225}
226
227impl DefLetStmt {
228    pub fn new(
229        param_def: Vec<ParamGroupWithParamType>,
230        facts: Vec<Fact>,
231        line_file: LineFile,
232    ) -> Self {
233        DefLetStmt {
234            param_def,
235            facts,
236            line_file,
237        }
238    }
239}
240
241impl fmt::Display for DefLetStmt {
242    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
243        let param_str = vec_to_string_with_sep(&self.param_def, ", ".to_string());
244        match self.facts.len() {
245            0 => write!(f, "{} {}", LET, param_str),
246            _ => write!(
247                f,
248                "{} {}{}\n{}",
249                LET,
250                param_str,
251                COLON,
252                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.facts, 1)
253            ),
254        }
255    }
256}
257
258impl HaveObjInNonemptySetOrParamTypeStmt {
259    pub fn new(param_def: Vec<ParamGroupWithParamType>, line_file: LineFile) -> Self {
260        HaveObjInNonemptySetOrParamTypeStmt {
261            param_def,
262            line_file,
263        }
264    }
265}
266
267impl fmt::Display for HaveObjInNonemptySetOrParamTypeStmt {
268    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
269        write!(
270            f,
271            "{} {}",
272            HAVE,
273            vec_to_string_join_by_comma(&self.param_def)
274        )
275    }
276}
277
278impl HaveObjEqualStmt {
279    pub fn new(
280        param_def: Vec<ParamGroupWithParamType>,
281        objs_equal_to: Vec<Obj>,
282        line_file: LineFile,
283    ) -> Self {
284        HaveObjEqualStmt {
285            param_def,
286            objs_equal_to,
287            line_file,
288        }
289    }
290}
291
292impl fmt::Display for HaveObjEqualStmt {
293    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
294        write!(
295            f,
296            "{} {} {} {}",
297            HAVE,
298            vec_to_string_with_sep(&self.param_def, ", ".to_string()),
299            EQUAL,
300            vec_to_string_join_by_comma(&self.objs_equal_to)
301        )
302    }
303}
304
305impl HaveByExistStmt {
306    pub fn new(
307        equal_tos: Vec<String>,
308        exist_fact_in_have_obj_st: ExistFact,
309        line_file: LineFile,
310    ) -> Self {
311        HaveByExistStmt {
312            equal_tos,
313            exist_fact_in_have_obj_st,
314            line_file,
315        }
316    }
317}
318
319impl fmt::Display for HaveByExistStmt {
320    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
321        write!(
322            f,
323            "{} {} {} {} {}",
324            HAVE,
325            BY,
326            self.exist_fact_in_have_obj_st,
327            COLON,
328            vec_to_string_join_by_comma(&self.equal_tos),
329        )
330    }
331}
332
333impl HaveFnEqualStmt {
334    pub fn new(
335        name: String,
336        fn_set_clause: FnSetClause,
337        equal_to: Obj,
338        line_file: LineFile,
339    ) -> Self {
340        HaveFnEqualStmt {
341            name,
342            fn_set_clause,
343            equal_to,
344            line_file,
345        }
346    }
347}
348
349impl fmt::Display for HaveFnEqualStmt {
350    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
351        write!(
352            f,
353            "{} {} {}{} {} {}",
354            HAVE,
355            FN_LOWER_CASE,
356            self.name,
357            brace_vec_colon_vec_to_string(
358                &self.fn_set_clause.params_def_with_set,
359                &self.fn_set_clause.dom_facts
360            ),
361            EQUAL,
362            self.equal_to
363        )
364    }
365}
366
367impl fmt::Display for HaveFnEqualCaseByCaseStmt {
368    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
369        let cases_and_proofs = self
370            .cases
371            .iter()
372            .enumerate()
373            .map(|(i, case)| {
374                to_string_and_add_four_spaces_at_beginning_of_each_line(
375                    &format!(
376                        "{} {}{} {}{} {} {}",
377                        CASE,
378                        case,
379                        COMMA,
380                        self.name,
381                        braced_vec_to_string(&ParamGroupWithSet::collect_param_names(
382                            &self.fn_set_clause.params_def_with_set,
383                        )),
384                        EQUAL,
385                        self.equal_tos[i]
386                    ),
387                    1,
388                )
389            })
390            .collect::<Vec<String>>();
391
392        write!(
393            f,
394            "{} {} {}{} {} {}\n{}",
395            HAVE,
396            FN_LOWER_CASE,
397            self.name,
398            brace_vec_colon_vec_to_string(
399                &self.fn_set_clause.params_def_with_set,
400                &self.fn_set_clause.dom_facts
401            ),
402            EQUAL,
403            COLON,
404            vec_to_string_with_sep(&cases_and_proofs, "\n".to_string())
405        )
406    }
407}
408
409impl HaveFnEqualCaseByCaseStmt {
410    pub fn new(
411        name: String,
412        fn_set_clause: FnSetClause,
413        cases: Vec<AndChainAtomicFact>,
414        equal_tos: Vec<Obj>,
415        line_file: LineFile,
416    ) -> Self {
417        HaveFnEqualCaseByCaseStmt {
418            name,
419            fn_set_clause,
420            cases,
421            equal_tos,
422            line_file,
423        }
424    }
425}
426
427pub(crate) fn induc_obj_plus_offset(induc_from: &Obj, offset: usize) -> Obj {
428    if offset == 0 {
429        induc_from.clone()
430    } else {
431        Obj::Add(Add::new(
432            induc_from.clone(),
433            Obj::Number(Number::new(offset.to_string())),
434        ))
435    }
436}
437
438fn flatten_and_chain_to_atomic_facts(c: &AndChainAtomicFact) -> Vec<AtomicFact> {
439    match c {
440        AndChainAtomicFact::AtomicFact(a) => vec![a.clone()],
441        AndChainAtomicFact::AndFact(af) => af.facts.clone(),
442        AndChainAtomicFact::ChainFact(cf) => cf.facts().unwrap(),
443    }
444}
445
446fn merge_two_and_chain_clauses(
447    a: AndChainAtomicFact,
448    b: AndChainAtomicFact,
449    line_file: LineFile,
450) -> AndChainAtomicFact {
451    let mut atoms = flatten_and_chain_to_atomic_facts(&a);
452    atoms.extend(flatten_and_chain_to_atomic_facts(&b));
453    AndChainAtomicFact::AndFact(AndFact::new(atoms, line_file))
454}
455
456impl HaveFnByInducStmt {
457    /// 与源码一致的 `fn` 空间（用户形参名 + dom + ret），不含 `__`；存 `Obj::FnSet` 时用 [`Runtime::fn_set_for_storage_from_have_fn_clause`]。
458    pub fn fn_user_fn_set_clause(&self) -> FnSetClause {
459        FnSetClause {
460            params_def_with_set: vec![ParamGroupWithSet::new(
461                vec![self.param.clone()],
462                Obj::StandardSet(StandardSet::Z),
463            )],
464            dom_facts: vec![OrAndChainAtomicFact::AtomicFact(
465                AtomicFact::GreaterEqualFact(GreaterEqualFact::new(
466                    Obj::Identifier(Identifier::new(self.param.clone())),
467                    self.induc_from.clone(),
468                    self.line_file.clone(),
469                )),
470            )],
471            ret_set: self.ret_set.clone(),
472        }
473    }
474
475    /// `forall x Z: ...` 里与 `fn` 定义域一致的那一段：标识符用源码 [`Self::param`]，与 [`Self::fn_user_fn_set_clause`] 的 dom 语义相同。
476    pub fn forall_fn_base_dom_exist_or_facts(&self) -> Vec<ExistOrAndChainAtomicFact> {
477        vec![ExistOrAndChainAtomicFact::AtomicFact(
478            AtomicFact::GreaterEqualFact(GreaterEqualFact::new(
479                Obj::Identifier(Identifier::new(self.param.clone())),
480                self.induc_from.clone(),
481                self.line_file.clone(),
482            )),
483        )]
484    }
485
486    pub fn new(
487        name: String,
488        param: String,
489        ret_set: Obj,
490        induc_from: Obj,
491        special_cases_equal_tos: Vec<Obj>,
492        last_case: HaveFnByInducLastCase,
493        line_file: LineFile,
494    ) -> Self {
495        HaveFnByInducStmt {
496            name,
497            param,
498            ret_set,
499            induc_from,
500            special_cases_equal_tos,
501            last_case,
502            line_file,
503        }
504    }
505
506    /// 展开为与旧 `HaveFnEqualCaseByCaseStmt` 兼容的平铺 `case` 列表（源码最后一条为 `case >= n:`（n 为特例个数），此处仍展开为 `param = from + n` 与可选子条件的合取）。
507    pub fn to_have_fn_equal_case_by_case_stmt(&self) -> HaveFnEqualCaseByCaseStmt {
508        let line_file = self.line_file.clone();
509        let left_id = Obj::Identifier(Identifier::new(self.param.clone()));
510        let n = self.special_cases_equal_tos.len();
511        let mut cases: Vec<AndChainAtomicFact> = Vec::new();
512        let mut equal_tos: Vec<Obj> = Vec::new();
513        for i in 0..n {
514            let when = AndChainAtomicFact::AtomicFact(AtomicFact::EqualFact(EqualFact::new(
515                left_id.clone(),
516                induc_obj_plus_offset(&self.induc_from, i),
517                line_file.clone(),
518            )));
519            cases.push(when);
520            equal_tos.push(self.special_cases_equal_tos[i].clone());
521        }
522        let step = AndChainAtomicFact::AtomicFact(AtomicFact::EqualFact(EqualFact::new(
523            left_id.clone(),
524            induc_obj_plus_offset(&self.induc_from, n),
525            line_file.clone(),
526        )));
527        match &self.last_case {
528            HaveFnByInducLastCase::EqualTo(eq) => {
529                cases.push(step);
530                equal_tos.push(eq.clone());
531            }
532            HaveFnByInducLastCase::NestedCases(last_pairs) => {
533                for nested in last_pairs {
534                    let merged = merge_two_and_chain_clauses(
535                        step.clone(),
536                        nested.case_fact.clone(),
537                        line_file.clone(),
538                    );
539                    cases.push(merged);
540                    equal_tos.push(nested.equal_to.clone());
541                }
542            }
543        }
544        HaveFnEqualCaseByCaseStmt::new(
545            self.name.clone(),
546            self.fn_user_fn_set_clause(),
547            cases,
548            equal_tos,
549            line_file,
550        )
551    }
552}
553
554impl fmt::Display for HaveFnByInducStmt {
555    /// 与源码一致：形参用用户名字，不出现 `__`；存 `FnSet` 时再 mangling。
556    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
557        let n = self.special_cases_equal_tos.len();
558        write!(
559            f,
560            "{} {} {} {} {} {} {}{}",
561            HAVE, FN_LOWER_CASE, BY, INDUC, FROM, " ", self.induc_from, COLON,
562        )?;
563        write!(f, " {} {}{}", self.name, LEFT_BRACE, self.param)?;
564        write!(
565            f,
566            " {} {} {} {} {} {} {} {} {} {} {} {}",
567            Z,
568            COLON,
569            " ",
570            self.param,
571            " ",
572            GREATER_EQUAL,
573            " ",
574            self.induc_from,
575            RIGHT_BRACE,
576            " ",
577            self.ret_set,
578            COLON,
579        )?;
580        for (i, eq) in self.special_cases_equal_tos.iter().enumerate() {
581            writeln!(f)?;
582            write!(f, "    {} {}: {}", CASE, i, eq)?;
583        }
584        writeln!(f)?;
585        match &self.last_case {
586            HaveFnByInducLastCase::EqualTo(eq) => {
587                write!(f, "    {} {} {}: {}", CASE, GREATER_EQUAL, n, eq)?;
588            }
589            HaveFnByInducLastCase::NestedCases(nested) => {
590                write!(f, "    {} {} {}:", CASE, GREATER_EQUAL, n)?;
591                for nc in nested {
592                    writeln!(f)?;
593                    write!(f, "        {} {}: {}", CASE, nc.case_fact, nc.equal_to)?;
594                }
595            }
596        }
597        Ok(())
598    }
599}
600
601impl DefFamilyStmt {
602    pub fn new(
603        name: String,
604        params_def_with_type: Vec<ParamGroupWithParamType>,
605        dom_facts: Vec<OrAndChainAtomicFact>,
606        equal_to: Obj,
607        line_file: LineFile,
608    ) -> Self {
609        DefFamilyStmt {
610            name,
611            params_def_with_type,
612            dom_facts,
613            equal_to,
614            line_file,
615        }
616    }
617}
618
619impl fmt::Display for DefFamilyStmt {
620    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
621        write!(
622            f,
623            "{} {}{}{} {} {}{} {} {}",
624            FAMILY,
625            self.name,
626            LEFT_BRACE,
627            vec_to_string_join_by_comma(&self.params_def_with_type),
628            COLON,
629            vec_to_string_join_by_comma(&self.dom_facts),
630            RIGHT_BRACE,
631            EQUAL,
632            self.equal_to
633        )
634    }
635}
636
637impl DefStructStmt {
638    pub fn new(
639        name: String,
640        param_defs: Vec<ParamGroupWithStructFieldType>,
641        dom_facts: Vec<OrAndChainAtomicFact>,
642        fields: Vec<(String, StructFieldType)>,
643        facts: Vec<OrAndChainAtomicFact>,
644        line_file: LineFile,
645    ) -> Self {
646        if fields.len() <= 1 {
647            unreachable!();
648        }
649
650        DefStructStmt {
651            name,
652            param_defs,
653            dom_facts,
654            fields,
655            facts,
656            line_file,
657        }
658    }
659
660    pub fn number_of_params(&self) -> usize {
661        ParamGroupWithStructFieldType::number_of_params(&self.param_defs)
662    }
663
664    /// 按定义顺序展开所有类型形参名（与 `struct T(...)` 中参数顺序一致）。
665    pub fn get_params(&self) -> Vec<String> {
666        ParamGroupWithStructFieldType::collect_param_names(&self.param_defs)
667    }
668}
litex/stmt/definition_stmt.rs

litex/stmt/
definition_stmt.rs
