litex/stmt/
definition_stmt.rs

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

litex/stmt/
definition_stmt.rs
