1use super::*;
2
3use itertools::Itertools;
4use std::fmt;
5
6#[derive(Clone, Debug, PartialEq)]
7pub struct Program {
8 pub datas: HashMap<Ident, DataDecl>,
9 pub preds: HashMap<Ident, PredDecl>,
10 pub querys: Vec<QueryDecl>,
11}
12
13#[derive(Clone, Debug, PartialEq)]
14pub struct Rule<V = Ident> {
15 pub vars: Vec<(V, TermType)>,
16 pub head: Vec<TermVal<V>>,
17 pub prims: Vec<(Prim, Vec<AtomVal<V>>)>,
18 pub calls: Vec<(Ident, Vec<TermType>, Vec<TermVal<V>>)>,
19}
20
21impl Rule<Ident> {
22 pub fn tag_ctx(&self, ctx: usize) -> Rule<IdentCtx> {
23 let vars: Vec<(IdentCtx, TermType)> = self
24 .vars
25 .iter()
26 .map(|(par, typ)| (par.tag_ctx(ctx), typ.clone()))
27 .collect();
28
29 let head: Vec<TermVal<IdentCtx>> = self.head.iter().map(|par| par.tag_ctx(ctx)).collect();
30
31 let prims: Vec<(Prim, Vec<AtomVal<IdentCtx>>)> = self
32 .prims
33 .iter()
34 .map(|(prim, args)| (*prim, args.iter().map(|arg| arg.tag_ctx(ctx)).collect()))
35 .collect();
36
37 let calls: Vec<(Ident, Vec<TermType>, Vec<TermVal<IdentCtx>>)> = self
38 .calls
39 .iter()
40 .map(|(pred, poly, args)| {
41 (
42 *pred,
43 poly.clone(),
44 args.iter().map(|arg| arg.tag_ctx(ctx)).collect(),
45 )
46 })
47 .collect();
48
49 Rule {
50 vars,
51 head,
52 prims,
53 calls,
54 }
55 }
56}
57
58#[derive(Clone, Debug, PartialEq)]
59pub struct DataDecl {
60 pub name: Ident,
61 pub polys: Vec<Ident>,
62 pub cons: Vec<Constructor>,
63}
64
65#[derive(Clone, Debug, PartialEq)]
66pub struct Constructor {
67 pub name: Ident,
68 pub flds: Vec<TermType>,
69}
70
71#[derive(Clone, Debug, PartialEq)]
72pub struct PredDecl {
73 pub name: Ident,
74 pub polys: Vec<Ident>,
75 pub pars: Vec<(Ident, TermType)>,
76 pub rules: Vec<Rule>,
77}
78
79#[derive(Clone, Debug, PartialEq)]
80pub struct QueryDecl {
81 pub entry: Ident,
82 pub params: Vec<QueryParam>,
83}
84
85#[derive(Clone, Debug, PartialEq)]
86pub enum QueryParam {
87 DepthStep(usize),
88 DepthLimit(usize),
89 AnswerLimit(usize),
90 AnswerPause(bool),
91}
92
93impl fmt::Display for PredDecl {
94 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
95 let pars = self
96 .pars
97 .iter()
98 .format_with(", ", |(var, typ), f| f(&format_args!("{}: {}", var, typ)));
99
100 if self.polys.is_empty() {
101 writeln!(f, "predicate {}({}):", self.name, pars)?;
102 } else {
103 let polys = self.polys.iter().format(", ");
104 writeln!(f, "predicate {}[{}]({}):", self.name, polys, pars)?;
105 }
106
107 for rule in self.rules.iter() {
108 write!(f, "{}", rule)?;
109 }
110 writeln!(f, "end")?;
111
112 Ok(())
113 }
114}
115
116impl<V: fmt::Display> fmt::Display for Rule<V> {
117 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
118 if self.calls.is_empty() && self.prims.is_empty() {
124 writeln!(f, "| ({}).", self.head.iter().format(", "))?;
125 return Ok(());
126 }
127
128 writeln!(f, "| ({}) :-", self.head.iter().format(", "))?;
129
130 for (prim, args) in self.prims.iter() {
131 writeln!(f, " {:?}({})", prim, args.iter().format(", "))?;
132 }
133
134 for (pred, polys, args) in self.calls.iter() {
135 if polys.is_empty() {
136 writeln!(f, " {}({})", pred, args.iter().format(", "))?;
137 } else {
138 writeln!(
139 f,
140 " {}[{}]({})",
141 pred,
142 polys.iter().format(", "),
143 args.iter().format(", ")
144 )?;
145 }
146 }
147
148 Ok(())
149 }
150}
151
152impl fmt::Display for DataDecl {
153 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
154 if self.polys.is_empty() {
155 writeln!(
156 f,
157 "datatype {}[{}] where",
158 self.name,
159 self.polys.iter().format(", ")
160 )?;
161 } else {
162 writeln!(f, "datatype {} where", self.name)?;
163 }
164
165 for cons in self.cons.iter() {
166 write!(f, "{}", cons)?;
167 }
168
169 writeln!(f, "end")?;
170 Ok(())
171 }
172}
173
174impl fmt::Display for Constructor {
175 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
176 writeln!(f, "| {}({})", self.name, self.flds.iter().format(", "))
177 }
178}
179
180impl fmt::Display for Program {
181 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
182 for (_data, data_decl) in self.datas.iter() {
183 writeln!(f, "{}", data_decl)?;
184 }
185
186 for (_pred, pred_decl) in self.preds.iter() {
187 writeln!(f, "{}", pred_decl)?;
188 }
189
190 Ok(())
191 }
192}
193
194#[derive(Clone, Debug, PartialEq)]
196pub(super) enum Goal {
197 Lit(bool),
198 Eq(TermVal, TermVal),
199 Prim(Prim, Vec<AtomVal>),
200 And(Vec<Goal>),
201 Or(Vec<Goal>),
202 Call(Ident, Vec<TermType>, Vec<TermVal>),
203}
204
205#[derive(Clone, Debug, PartialEq)]
206pub(super) struct GoalPredDecl {
207 pub name: Ident,
208 pub polys: Vec<Ident>,
209 pub pars: Vec<(Ident, TermType)>,
210 pub vars: Vec<(Ident, TermType)>,
211 pub goal: Goal,
212}