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

litex/stmt/
definition_stmt.rs
