litex/stmt/
definition_stmt.rs

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

litex/stmt/
definition_stmt.rs
