Skip to main content

prune_lang/logic/
ast.rs

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        // let vars = self
119        //     .vars
120        //     .iter()
121        //     .format_with(",", |(var, typ), f| f(&format_args!("{} : {}", var, typ)));
122
123        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// `Goal` and `GoalPredDecl` are temporary data structure used inside the compiling pass
195#[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}