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/// `have fn` `{ ... }` piece. Parameter sets may depend on earlier parameters; `ret_set` must not
49/// cite these parameters.
50#[derive(Clone)]
51pub struct FnSetClause {
52    pub params_def_with_set: ParamDefWithSet,
53    pub dom_facts: Vec<OrAndChainAtomicFact>,
54    pub ret_set: Obj,
55}
56
57impl FnSetClause {
58    pub fn new(
59        params_def_with_set: impl Into<ParamDefWithSet>,
60        dom_facts: Vec<OrAndChainAtomicFact>,
61        ret_set: Obj,
62    ) -> Result<Self, RuntimeError> {
63        let params_def_with_set = params_def_with_set.into();
64        params_def_with_set.validate_obj_does_not_cite_params(&ret_set, "function return set")?;
65        Ok(FnSetClause {
66            params_def_with_set,
67            dom_facts,
68            ret_set,
69        })
70    }
71
72    /// Outer `{...}` binders first, then each nested function return `fn` layer, in order.
73    /// Used when parsing `have fn ... = rhs` so RHS identifiers match nested return fn-set params.
74    pub fn collect_all_param_names_including_nested_ret_fn_sets(&self) -> Vec<String> {
75        let mut names = ParamGroupWithSet::collect_param_names(&self.params_def_with_set);
76        let mut ret_set = self.ret_set.clone();
77        while let Obj::FnSet(inner) = ret_set {
78            names.extend(ParamGroupWithSet::collect_param_names(
79                &inner.body.params_def_with_set,
80            ));
81            ret_set = (*inner.body.ret_set).clone();
82        }
83        names
84    }
85}
86
87#[derive(Clone)]
88pub struct HaveFnEqualCaseByCaseStmt {
89    pub name: String,
90    pub fn_set_clause: FnSetClause,
91    pub cases: Vec<AndChainAtomicFact>,
92    pub equal_tos: Vec<Obj>,
93    pub line_file: LineFile,
94}
95
96#[derive(Clone)]
97pub struct HaveFnEqualStmt {
98    pub name: String,
99    pub equal_to_anonymous_fn: AnonymousFn,
100    pub line_file: LineFile,
101}
102
103#[derive(Clone)]
104pub struct HaveFnByForallExistUniqueStmt {
105    pub fn_name: String,
106    pub forall: ForallFact,
107    pub line_file: LineFile,
108}
109
110#[derive(Clone)]
111pub struct DefTemplateStmt {
112    pub template_name: String,
113    pub template_arg_def: ParamDefWithType,
114    pub template_arg_dom: Vec<OrAndChainAtomicFact>,
115    pub template_def_stmt: TemplateDefEnum,
116    pub line_file: LineFile,
117}
118
119#[derive(Clone)]
120pub enum TemplateDefEnum {
121    HaveObjInNonemptySetStmt(HaveObjInNonemptySetOrParamTypeStmt),
122    HaveObjEqualStmt(HaveObjEqualStmt),
123    HaveByExistStmt(HaveByExistStmt),
124    HaveFnEqualStmt(HaveFnEqualStmt),
125    HaveFnEqualCaseByCaseStmt(HaveFnEqualCaseByCaseStmt),
126    HaveFnByInducStmt(HaveFnByInducStmt),
127    HaveFnByForallExistUniqueStmt(HaveFnByForallExistUniqueStmt),
128}
129
130// have by exist a R st {$p(a)}: a
131#[derive(Clone)]
132pub struct HaveByExistStmt {
133    pub equal_tos: Vec<String>,
134    pub exist_fact_in_have_obj_st: ExistFactEnum,
135    pub line_file: LineFile,
136}
137
138#[derive(Clone)]
139pub struct HaveObjEqualStmt {
140    pub param_def: ParamDefWithType,
141    pub objs_equal_to: Vec<Obj>,
142    pub line_file: LineFile,
143}
144
145#[derive(Clone)]
146pub struct HaveObjInNonemptySetOrParamTypeStmt {
147    pub param_def: ParamDefWithType,
148    pub line_file: LineFile,
149}
150
151#[derive(Clone)]
152pub struct DefLetStmt {
153    pub param_def: ParamDefWithType,
154    pub facts: Vec<Fact>,
155    pub line_file: LineFile,
156}
157
158#[derive(Clone)]
159pub struct DefPropStmt {
160    pub name: String,
161    pub params_def_with_type: ParamDefWithType,
162    pub iff_facts: Vec<Fact>,
163    pub line_file: LineFile,
164}
165
166impl fmt::Display for DefAbstractPropStmt {
167    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
168        write!(
169            f,
170            "{} {}{}{}{}",
171            ABSTRACT_PROP,
172            self.name,
173            LEFT_BRACE,
174            vec_to_string_join_by_comma(&self.params),
175            RIGHT_BRACE
176        )
177    }
178}
179
180impl DefPropStmt {
181    pub fn new(
182        name: String,
183        params_def_with_type: ParamDefWithType,
184        iff_facts: Vec<Fact>,
185        line_file: LineFile,
186    ) -> Self {
187        DefPropStmt {
188            name,
189            params_def_with_type,
190            iff_facts,
191            line_file,
192        }
193    }
194}
195
196impl fmt::Display for DefPropStmt {
197    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
198        match self.iff_facts.len() {
199            0 => write!(
200                f,
201                "{} {}{}",
202                PROP,
203                self.name,
204                braced_string(&self.params_def_with_type)
205            ),
206            _ => write!(
207                f,
208                "{} {}{}{}\n{}",
209                PROP,
210                self.name,
211                braced_string(&self.params_def_with_type),
212                COLON,
213                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.iff_facts, 1)
214            ),
215        }
216    }
217}
218
219impl DefLetStmt {
220    pub fn new(param_def: ParamDefWithType, facts: Vec<Fact>, line_file: LineFile) -> Self {
221        DefLetStmt {
222            param_def,
223            facts,
224            line_file,
225        }
226    }
227}
228
229impl fmt::Display for DefLetStmt {
230    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
231        let param_str = self.param_def.to_string();
232        match self.facts.len() {
233            0 => write!(f, "{} {}", LET, param_str),
234            _ => write!(
235                f,
236                "{} {}{}\n{}",
237                LET,
238                param_str,
239                COLON,
240                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.facts, 1)
241            ),
242        }
243    }
244}
245
246impl HaveObjInNonemptySetOrParamTypeStmt {
247    pub fn new(param_def: ParamDefWithType, line_file: LineFile) -> Self {
248        HaveObjInNonemptySetOrParamTypeStmt {
249            param_def,
250            line_file,
251        }
252    }
253}
254
255impl fmt::Display for HaveObjInNonemptySetOrParamTypeStmt {
256    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
257        write!(f, "{} {}", HAVE, self.param_def.to_string())
258    }
259}
260
261impl HaveObjEqualStmt {
262    pub fn new(param_def: ParamDefWithType, objs_equal_to: Vec<Obj>, line_file: LineFile) -> Self {
263        HaveObjEqualStmt {
264            param_def,
265            objs_equal_to,
266            line_file,
267        }
268    }
269}
270
271impl fmt::Display for HaveObjEqualStmt {
272    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
273        write!(
274            f,
275            "{} {} {} {}",
276            HAVE,
277            self.param_def.to_string(),
278            EQUAL,
279            vec_to_string_join_by_comma(&self.objs_equal_to)
280        )
281    }
282}
283
284impl HaveObjInNonemptySetOrParamTypeStmt {
285    pub fn single_defined_name(&self) -> Option<String> {
286        let names = self.param_def.collect_param_names();
287        if names.len() == 1 {
288            Some(names[0].clone())
289        } else {
290            None
291        }
292    }
293}
294
295impl HaveObjEqualStmt {
296    pub fn single_defined_name(&self) -> Option<String> {
297        let names = self.param_def.collect_param_names();
298        if names.len() == 1 {
299            Some(names[0].clone())
300        } else {
301            None
302        }
303    }
304}
305
306impl HaveByExistStmt {
307    pub fn new(
308        equal_tos: Vec<String>,
309        exist_fact_in_have_obj_st: ExistFactEnum,
310        line_file: LineFile,
311    ) -> Self {
312        HaveByExistStmt {
313            equal_tos,
314            exist_fact_in_have_obj_st,
315            line_file,
316        }
317    }
318}
319
320impl fmt::Display for HaveByExistStmt {
321    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
322        write!(
323            f,
324            "{} {} {} {} {}",
325            HAVE,
326            BY,
327            self.exist_fact_in_have_obj_st,
328            COLON,
329            vec_to_string_join_by_comma(&self.equal_tos),
330        )
331    }
332}
333
334impl HaveFnEqualStmt {
335    pub fn new(name: String, equal_to_anonymous_fn: AnonymousFn, line_file: LineFile) -> Self {
336        HaveFnEqualStmt {
337            name,
338            equal_to_anonymous_fn,
339            line_file,
340        }
341    }
342}
343
344impl fmt::Display for HaveFnEqualStmt {
345    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
346        let fn_set_clause = FnSetClause::new(
347            self.equal_to_anonymous_fn.body.params_def_with_set.clone(),
348            self.equal_to_anonymous_fn.body.dom_facts.clone(),
349            (*self.equal_to_anonymous_fn.body.ret_set).clone(),
350        )
351        .expect("anonymous function signature was already validated");
352        write!(
353            f,
354            "{} {} {}{} {} {}",
355            HAVE,
356            FN_LOWER_CASE,
357            self.name,
358            brace_vec_colon_vec_to_string(
359                &fn_set_clause.params_def_with_set,
360                &fn_set_clause.dom_facts
361            ),
362            EQUAL,
363            self.equal_to_anonymous_fn.equal_to
364        )
365    }
366}
367
368impl HaveFnByForallExistUniqueStmt {
369    pub fn new(fn_name: String, forall: ForallFact, line_file: LineFile) -> Self {
370        HaveFnByForallExistUniqueStmt {
371            fn_name,
372            forall,
373            line_file,
374        }
375    }
376}
377
378impl fmt::Display for HaveFnByForallExistUniqueStmt {
379    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
380        write!(
381            f,
382            "{} {} {} {} {}{}\n{}",
383            HAVE,
384            FN_LOWER_CASE,
385            self.fn_name,
386            AS,
387            SET,
388            COLON,
389            to_string_and_add_four_spaces_at_beginning_of_each_line(&self.forall, 1)
390        )
391    }
392}
393
394impl DefTemplateStmt {
395    pub fn new(
396        template_name: String,
397        template_arg_def: ParamDefWithType,
398        template_arg_dom: Vec<OrAndChainAtomicFact>,
399        template_def_stmt: TemplateDefEnum,
400        line_file: LineFile,
401    ) -> Self {
402        DefTemplateStmt {
403            template_name,
404            template_arg_def,
405            template_arg_dom,
406            template_def_stmt,
407            line_file,
408        }
409    }
410}
411
412impl TemplateDefEnum {
413    pub fn defined_name(&self) -> Option<String> {
414        match self {
415            TemplateDefEnum::HaveObjInNonemptySetStmt(stmt) => stmt.single_defined_name(),
416            TemplateDefEnum::HaveObjEqualStmt(stmt) => stmt.single_defined_name(),
417            TemplateDefEnum::HaveByExistStmt(stmt) => {
418                if stmt.equal_tos.len() == 1 {
419                    Some(stmt.equal_tos[0].clone())
420                } else {
421                    None
422                }
423            }
424            TemplateDefEnum::HaveFnEqualStmt(stmt) => Some(stmt.name.clone()),
425            TemplateDefEnum::HaveFnEqualCaseByCaseStmt(stmt) => Some(stmt.name.clone()),
426            TemplateDefEnum::HaveFnByInducStmt(stmt) => Some(stmt.name.clone()),
427            TemplateDefEnum::HaveFnByForallExistUniqueStmt(stmt) => Some(stmt.fn_name.clone()),
428        }
429    }
430
431    pub fn to_stmt(&self) -> Stmt {
432        match self {
433            TemplateDefEnum::HaveObjInNonemptySetStmt(stmt) => stmt.clone().into(),
434            TemplateDefEnum::HaveObjEqualStmt(stmt) => stmt.clone().into(),
435            TemplateDefEnum::HaveByExistStmt(stmt) => stmt.clone().into(),
436            TemplateDefEnum::HaveFnEqualStmt(stmt) => stmt.clone().into(),
437            TemplateDefEnum::HaveFnEqualCaseByCaseStmt(stmt) => stmt.clone().into(),
438            TemplateDefEnum::HaveFnByInducStmt(stmt) => stmt.clone().into(),
439            TemplateDefEnum::HaveFnByForallExistUniqueStmt(stmt) => stmt.clone().into(),
440        }
441    }
442}
443
444impl fmt::Display for TemplateDefEnum {
445    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
446        match self {
447            TemplateDefEnum::HaveObjInNonemptySetStmt(stmt) => write!(f, "{}", stmt),
448            TemplateDefEnum::HaveObjEqualStmt(stmt) => write!(f, "{}", stmt),
449            TemplateDefEnum::HaveByExistStmt(stmt) => write!(f, "{}", stmt),
450            TemplateDefEnum::HaveFnEqualStmt(stmt) => write!(f, "{}", stmt),
451            TemplateDefEnum::HaveFnEqualCaseByCaseStmt(stmt) => write!(f, "{}", stmt),
452            TemplateDefEnum::HaveFnByInducStmt(stmt) => write!(f, "{}", stmt),
453            TemplateDefEnum::HaveFnByForallExistUniqueStmt(stmt) => write!(f, "{}", stmt),
454        }
455    }
456}
457
458impl fmt::Display for DefTemplateStmt {
459    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
460        write!(
461            f,
462            "{} {}{}{}{}{}{}\n{}",
463            TEMPLATE,
464            self.template_name,
465            LESS,
466            self.template_arg_def,
467            if self.template_arg_dom.is_empty() {
468                String::new()
469            } else {
470                format!(
471                    "{} {}",
472                    COLON,
473                    vec_to_string_join_by_comma(&self.template_arg_dom)
474                )
475            },
476            GREATER,
477            COLON,
478            to_string_and_add_four_spaces_at_beginning_of_each_line(&self.template_def_stmt, 1)
479        )
480    }
481}
482
483impl fmt::Display for HaveFnEqualCaseByCaseStmt {
484    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
485        let cases_and_proofs = self
486            .cases
487            .iter()
488            .enumerate()
489            .map(|(i, case)| {
490                to_string_and_add_four_spaces_at_beginning_of_each_line(
491                    &format!("{} {}{} {}", CASE, case, COLON, self.equal_tos[i]),
492                    1,
493                )
494            })
495            .collect::<Vec<String>>();
496
497        write!(
498            f,
499            "{} {} {}{} {} {} {}{}\n{}",
500            HAVE,
501            FN_LOWER_CASE,
502            self.name,
503            brace_vec_colon_vec_to_string(
504                &self.fn_set_clause.params_def_with_set,
505                &self.fn_set_clause.dom_facts
506            ),
507            self.fn_set_clause.ret_set,
508            BY,
509            CASES,
510            COLON,
511            vec_to_string_with_sep(&cases_and_proofs, "\n".to_string())
512        )
513    }
514}
515
516impl HaveFnEqualCaseByCaseStmt {
517    pub fn new(
518        name: String,
519        fn_set_clause: FnSetClause,
520        cases: Vec<AndChainAtomicFact>,
521        equal_tos: Vec<Obj>,
522        line_file: LineFile,
523    ) -> Self {
524        HaveFnEqualCaseByCaseStmt {
525            name,
526            fn_set_clause,
527            cases,
528            equal_tos,
529            line_file,
530        }
531    }
532}
533
534pub fn induc_obj_plus_offset(induc_from: &Obj, offset: usize) -> Obj {
535    if offset == 0 {
536        induc_from.clone()
537    } else {
538        Add::new(induc_from.clone(), Number::new(offset.to_string()).into()).into()
539    }
540}
541
542fn flatten_and_chain_to_atomic_facts(c: &AndChainAtomicFact) -> Vec<AtomicFact> {
543    match c {
544        AndChainAtomicFact::AtomicFact(a) => vec![a.clone()],
545        AndChainAtomicFact::AndFact(af) => af.facts.clone(),
546        AndChainAtomicFact::ChainFact(cf) => cf.facts().unwrap(),
547    }
548}
549
550fn merge_two_and_chain_clauses(
551    a: AndChainAtomicFact,
552    b: AndChainAtomicFact,
553    line_file: LineFile,
554) -> AndChainAtomicFact {
555    let mut atoms = flatten_and_chain_to_atomic_facts(&a);
556    atoms.extend(flatten_and_chain_to_atomic_facts(&b));
557    AndChainAtomicFact::AndFact(AndFact::new(atoms, line_file))
558}
559
560impl HaveFnByInducCase {
561    pub fn new(case_fact: AndChainAtomicFact, body: HaveFnByInducCaseBody) -> Self {
562        HaveFnByInducCase { case_fact, body }
563    }
564}
565
566impl HaveFnByInducStmt {
567    pub fn new(
568        name: String,
569        fn_set_clause: FnSetClause,
570        measure: Obj,
571        lower_bound: Obj,
572        cases: Vec<HaveFnByInducCase>,
573        line_file: LineFile,
574    ) -> Self {
575        HaveFnByInducStmt {
576            name,
577            fn_set_clause,
578            measure,
579            lower_bound,
580            cases,
581            line_file,
582        }
583    }
584
585    pub fn param_names(&self) -> Vec<String> {
586        ParamGroupWithSet::collect_param_names(&self.fn_set_clause.params_def_with_set)
587    }
588
589    /// Flatten nested cases into the ordinary case-by-case shape used for stored forall facts.
590    pub fn to_have_fn_equal_case_by_case_stmt(&self) -> HaveFnEqualCaseByCaseStmt {
591        let line_file = self.line_file.clone();
592        let mut cases: Vec<AndChainAtomicFact> = Vec::new();
593        let mut equal_tos: Vec<Obj> = Vec::new();
594        Self::flatten_case_list(&self.cases, None, &mut cases, &mut equal_tos, &line_file);
595        HaveFnEqualCaseByCaseStmt::new(
596            self.name.clone(),
597            self.fn_set_clause.clone(),
598            cases,
599            equal_tos,
600            line_file,
601        )
602    }
603
604    fn flatten_case_list(
605        source_cases: &[HaveFnByInducCase],
606        prefix: Option<AndChainAtomicFact>,
607        cases: &mut Vec<AndChainAtomicFact>,
608        equal_tos: &mut Vec<Obj>,
609        line_file: &LineFile,
610    ) {
611        for c in source_cases {
612            let merged = match &prefix {
613                Some(p) => {
614                    merge_two_and_chain_clauses(p.clone(), c.case_fact.clone(), line_file.clone())
615                }
616                None => c.case_fact.clone(),
617            };
618            match &c.body {
619                HaveFnByInducCaseBody::EqualTo(eq) => {
620                    cases.push(merged);
621                    equal_tos.push(eq.clone());
622                }
623                HaveFnByInducCaseBody::NestedCases(nested) => {
624                    Self::flatten_case_list(nested, Some(merged), cases, equal_tos, line_file);
625                }
626            }
627        }
628    }
629}
630
631impl fmt::Display for HaveFnByInducStmt {
632    /// Display uses the same parameter names as in source.
633    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
634        write!(
635            f,
636            "{} {} {}{} {} {} {} {} {} {}{}",
637            HAVE,
638            FN_LOWER_CASE,
639            self.name,
640            brace_vec_colon_vec_to_string(
641                &self.fn_set_clause.params_def_with_set,
642                &self.fn_set_clause.dom_facts
643            ),
644            self.fn_set_clause.ret_set,
645            BY,
646            DECREASING,
647            self.measure,
648            FROM,
649            self.lower_bound,
650            COLON
651        )?;
652        Self::fmt_cases(f, &self.cases, 1)
653    }
654}
655
656impl HaveFnByInducStmt {
657    fn fmt_cases(
658        f: &mut fmt::Formatter<'_>,
659        cases: &[HaveFnByInducCase],
660        indent: usize,
661    ) -> fmt::Result {
662        let pad = "    ".repeat(indent);
663        for c in cases {
664            writeln!(f)?;
665            match &c.body {
666                HaveFnByInducCaseBody::EqualTo(eq) => {
667                    write!(f, "{}{} {}: {}", pad, CASE, c.case_fact, eq)?;
668                }
669                HaveFnByInducCaseBody::NestedCases(nested) => {
670                    write!(f, "{}{} {}:", pad, CASE, c.case_fact)?;
671                    Self::fmt_cases(f, nested, indent + 1)?;
672                }
673            }
674        }
675        Ok(())
676    }
677}
litex/stmt/definition_stmt.rs

litex/stmt/
definition_stmt.rs
