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

litex/stmt/
definition_stmt.rs
