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

litex/stmt/
definition_stmt.rs
