litex/fact/
fact_inside_forall.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub enum ExistOrAndChainAtomicFact {
6    AtomicFact(AtomicFact),
7    AndFact(AndFact),
8    ChainFact(ChainFact),
9    OrFact(OrFact),
10    ExistFact(ExistFact),
11}
12
13impl fmt::Display for ExistOrAndChainAtomicFact {
14    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
15        match self {
16            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => write!(f, "{}", atomic_fact),
17            ExistOrAndChainAtomicFact::AndFact(and_fact) => write!(f, "{}", and_fact),
18            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => write!(f, "{}", chain_fact),
19            ExistOrAndChainAtomicFact::OrFact(or_fact) => write!(f, "{}", or_fact),
20            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => write!(f, "{}", exist_fact),
21        }
22    }
23}
24
25impl ExistOrAndChainAtomicFact {
26    pub fn to_fact(self) -> Fact {
27        match self {
28            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => Fact::AtomicFact(atomic_fact),
29            ExistOrAndChainAtomicFact::AndFact(and_fact) => Fact::AndFact(and_fact),
30            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => Fact::ChainFact(chain_fact),
31            ExistOrAndChainAtomicFact::OrFact(or_fact) => Fact::OrFact(or_fact),
32            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => Fact::ExistFact(exist_fact),
33        }
34    }
35
36    pub fn line_file(&self) -> LineFile {
37        match self {
38            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => atomic_fact.line_file(),
39            ExistOrAndChainAtomicFact::AndFact(and_fact) => and_fact.line_file(),
40            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => chain_fact.line_file(),
41            ExistOrAndChainAtomicFact::OrFact(or_fact) => or_fact.line_file.clone(),
42            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => exist_fact.line_file(),
43        }
44    }
45
46    pub fn with_new_line_file(self, line_file: LineFile) -> Self {
47        match self {
48            ExistOrAndChainAtomicFact::AtomicFact(a) => {
49                ExistOrAndChainAtomicFact::AtomicFact(a.with_new_line_file(line_file))
50            }
51            ExistOrAndChainAtomicFact::AndFact(af) => {
52                ExistOrAndChainAtomicFact::AndFact(AndFact::new(
53                    af.facts
54                        .into_iter()
55                        .map(|x| x.with_new_line_file(line_file.clone()))
56                        .collect(),
57                    line_file,
58                ))
59            }
60            ExistOrAndChainAtomicFact::ChainFact(cf) => ExistOrAndChainAtomicFact::ChainFact(
61                ChainFact::new(cf.objs, cf.prop_names, line_file),
62            ),
63            ExistOrAndChainAtomicFact::OrFact(of) => {
64                ExistOrAndChainAtomicFact::OrFact(OrFact::new(
65                    of.facts
66                        .into_iter()
67                        .map(|x| x.with_new_line_file(line_file.clone()))
68                        .collect(),
69                    line_file,
70                ))
71            }
72            ExistOrAndChainAtomicFact::ExistFact(e) => {
73                ExistOrAndChainAtomicFact::ExistFact(ExistFact::new(
74                    e.params_def_with_type,
75                    e.facts
76                        .into_iter()
77                        .map(|x| x.with_new_line_file(line_file.clone()))
78                        .collect(),
79                    e.is_exist_unique,
80                    line_file,
81                ))
82            }
83        }
84    }
85}
86
87impl From<AtomicFact> for ExistOrAndChainAtomicFact {
88    fn from(atomic_fact: AtomicFact) -> Self {
89        ExistOrAndChainAtomicFact::AtomicFact(atomic_fact)
90    }
91}
92
93impl From<GreaterEqualFact> for ExistOrAndChainAtomicFact {
94    fn from(f: GreaterEqualFact) -> Self {
95        AtomicFact::from(f).into()
96    }
97}
98
99impl From<IsNonemptySetFact> for ExistOrAndChainAtomicFact {
100    fn from(f: IsNonemptySetFact) -> Self {
101        AtomicFact::from(f).into()
102    }
103}
104
105impl From<EqualFact> for ExistOrAndChainAtomicFact {
106    fn from(f: EqualFact) -> Self {
107        AtomicFact::from(f).into()
108    }
109}
110
111impl From<InFact> for ExistOrAndChainAtomicFact {
112    fn from(f: InFact) -> Self {
113        ExistOrAndChainAtomicFact::AtomicFact(f.into())
114    }
115}
116
117impl From<ExistFact> for ExistOrAndChainAtomicFact {
118    fn from(exist_fact: ExistFact) -> Self {
119        ExistOrAndChainAtomicFact::ExistFact(exist_fact)
120    }
121}
122
123impl From<AndFact> for ExistOrAndChainAtomicFact {
124    fn from(a: AndFact) -> Self {
125        ExistOrAndChainAtomicFact::AndFact(a)
126    }
127}
128
129impl From<ChainFact> for ExistOrAndChainAtomicFact {
130    fn from(c: ChainFact) -> Self {
131        ExistOrAndChainAtomicFact::ChainFact(c)
132    }
133}
134
135impl From<OrFact> for ExistOrAndChainAtomicFact {
136    fn from(o: OrFact) -> Self {
137        ExistOrAndChainAtomicFact::OrFact(o)
138    }
139}
litex/fact/fact_inside_forall.rs

litex/fact/
fact_inside_forall.rs
