Skip to main content

riddle/
env.rs

1use crate::scope::{BoolType, Predicate, Scope, Type};
2use std::{
3    any::Any,
4    cell::RefCell,
5    collections::HashMap,
6    fmt,
7    rc::{Rc, Weak},
8};
9
10pub trait Var: fmt::Debug {
11    fn var_type(&self) -> Rc<dyn Type>;
12    fn as_any(self: Rc<Self>) -> Rc<dyn Any>;
13    fn as_env(self: Rc<Self>) -> Option<Rc<dyn Env>> {
14        None
15    }
16}
17
18pub trait Env: fmt::Debug {
19    fn parent(&self) -> Option<Rc<dyn Env>>;
20    fn get(&self, name: &str) -> Option<Rc<dyn Var>>;
21    fn set(&self, name: String, value: Rc<dyn Var>);
22}
23
24pub trait EnvExt {
25    fn get_as<T: Var + 'static>(&self, name: &str) -> Option<Rc<T>>;
26}
27
28impl<E: Env + ?Sized> EnvExt for E {
29    fn get_as<T: Var + 'static>(&self, name: &str) -> Option<Rc<T>> {
30        self.get(name)?.as_any().downcast::<T>().ok()
31    }
32}
33
34#[derive(Debug)]
35pub struct CommonEnv {
36    parent: Option<Rc<dyn Env>>,
37    variables: RefCell<HashMap<String, Rc<dyn Var>>>,
38}
39
40impl CommonEnv {
41    pub fn new(parent: Option<Rc<dyn Env>>) -> Self {
42        Self { parent, variables: RefCell::new(HashMap::new()) }
43    }
44}
45
46impl Env for CommonEnv {
47    fn parent(&self) -> Option<Rc<dyn Env>> {
48        self.parent.clone()
49    }
50
51    fn get(&self, name: &str) -> Option<Rc<dyn Var>> {
52        self.variables.borrow().get(name).cloned().or_else(|| self.parent.as_ref()?.get(name))
53    }
54
55    fn set(&self, name: String, value: Rc<dyn Var>) {
56        self.variables.borrow_mut().insert(name, value);
57    }
58}
59
60#[derive(Debug)]
61pub struct Atom {
62    predicate: Weak<Predicate>,
63    fact: bool,
64    env: CommonEnv,
65}
66
67impl Atom {
68    pub fn new(predicate: Rc<Predicate>, fact: bool, args: HashMap<String, Rc<dyn Var>>) -> Self {
69        let env = args.get("tau").and_then(|tau| tau.clone().as_env()).unwrap_or_else(|| predicate.clone().core());
70        let env = CommonEnv::new(Some(env));
71        for (name, value) in args {
72            env.set(name, value);
73        }
74        Self { predicate: Rc::downgrade(&predicate), fact, env }
75    }
76
77    pub fn predicate(&self) -> Rc<Predicate> {
78        self.predicate.upgrade().unwrap()
79    }
80
81    pub fn is_fact(&self) -> bool {
82        self.fact
83    }
84}
85
86impl Var for Atom {
87    fn var_type(&self) -> Rc<dyn Type> {
88        self.predicate()
89    }
90
91    fn as_any(self: Rc<Self>) -> Rc<dyn Any> {
92        self
93    }
94
95    fn as_env(self: Rc<Self>) -> Option<Rc<dyn Env>> {
96        Some(self.clone())
97    }
98}
99
100impl Env for Atom {
101    fn parent(&self) -> Option<Rc<dyn Env>> {
102        self.env.parent.clone()
103    }
104
105    fn get(&self, name: &str) -> Option<Rc<dyn Var>> {
106        self.env.get(name)
107    }
108
109    fn set(&self, name: String, value: Rc<dyn Var>) {
110        self.env.set(name, value);
111    }
112}
113
114#[derive(Debug)]
115pub struct Object {
116    class: Weak<dyn Type>,
117    env: CommonEnv,
118}
119
120impl Object {
121    pub fn new(class: Rc<dyn Type>, parent_env: Option<Rc<dyn Env>>) -> Self {
122        Self { class: Rc::downgrade(&class), env: CommonEnv::new(parent_env) }
123    }
124}
125
126impl Var for Object {
127    fn var_type(&self) -> Rc<dyn Type> {
128        self.class.upgrade().unwrap()
129    }
130
131    fn as_any(self: Rc<Self>) -> Rc<dyn Any> {
132        self
133    }
134
135    fn as_env(self: Rc<Self>) -> Option<Rc<dyn Env>> {
136        Some(self.clone())
137    }
138}
139
140impl Env for Object {
141    fn parent(&self) -> Option<Rc<dyn Env>> {
142        self.env.parent.clone()
143    }
144
145    fn get(&self, name: &str) -> Option<Rc<dyn Var>> {
146        self.env.get(name)
147    }
148
149    fn set(&self, name: String, value: Rc<dyn Var>) {
150        self.env.set(name, value);
151    }
152}
153
154#[derive(Debug)]
155pub enum BoolExpr {
156    Term { var_type: Weak<BoolType>, term: Rc<dyn Var> },
157    Not { var_type: Weak<BoolType>, term: Rc<BoolExpr> },
158    Eq { var_type: Weak<BoolType>, left: Rc<dyn Var>, right: Rc<dyn Var> },
159    Lt { var_type: Weak<BoolType>, left: Rc<dyn Var>, right: Rc<dyn Var> },
160    Leq { var_type: Weak<BoolType>, left: Rc<dyn Var>, right: Rc<dyn Var> },
161    Or { var_type: Weak<BoolType>, terms: Vec<Rc<BoolExpr>> },
162    And { var_type: Weak<BoolType>, terms: Vec<Rc<BoolExpr>> },
163}
164
165impl Var for BoolExpr {
166    fn var_type(&self) -> Rc<dyn Type> {
167        match self {
168            BoolExpr::Term { var_type: var_tp, .. } | BoolExpr::Not { var_type: var_tp, .. } | BoolExpr::Eq { var_type: var_tp, .. } | BoolExpr::Lt { var_type: var_tp, .. } | BoolExpr::Leq { var_type: var_tp, .. } | BoolExpr::Or { var_type: var_tp, .. } | BoolExpr::And { var_type: var_tp, .. } => var_tp.upgrade().unwrap(),
169        }
170    }
171
172    fn as_any(self: Rc<Self>) -> Rc<dyn Any> {
173        self
174    }
175}
176
177fn push_negations(expr: Rc<dyn Var>) -> Rc<BoolExpr> {
178    if let Ok(bool_expr) = expr.as_any().downcast::<BoolExpr>() {
179        match bool_expr.as_ref() {
180            BoolExpr::Not { var_type, term } => {
181                let inner_expr = push_negations(term.clone());
182                match inner_expr.as_any().downcast_ref::<BoolExpr>() {
183                    Some(BoolExpr::Not { var_type: inner_var_type, term: inner_term }) => Rc::new(BoolExpr::Term { var_type: inner_var_type.clone(), term: inner_term.clone() }),
184                    Some(BoolExpr::And { var_type: inner_var_type, terms }) => Rc::new(BoolExpr::Or {
185                        var_type: inner_var_type.clone(),
186                        terms: terms.iter().map(|t| push_negations(t.clone())).collect(),
187                    }),
188                    Some(BoolExpr::Or { var_type: inner_var_type, terms }) => Rc::new(BoolExpr::And {
189                        var_type: inner_var_type.clone(),
190                        terms: terms.iter().map(|t| push_negations(t.clone())).collect(),
191                    }),
192                    _ => Rc::new(BoolExpr::Not { var_type: var_type.clone(), term: push_negations(term.clone()) }),
193                }
194            }
195            BoolExpr::And { var_type, terms } => Rc::new(BoolExpr::And {
196                var_type: var_type.clone(),
197                terms: terms.iter().map(|t| push_negations(t.clone())).collect(),
198            }),
199            BoolExpr::Or { var_type, terms } => Rc::new(BoolExpr::Or {
200                var_type: var_type.clone(),
201                terms: terms.iter().map(|t| push_negations(t.clone())).collect(),
202            }),
203            _ => bool_expr.clone(),
204        }
205    } else {
206        panic!("Expected a BoolExpr");
207    }
208}
209
210fn distribute(expr: Rc<dyn Var>) -> Rc<BoolExpr> {
211    if let Ok(bool_expr) = expr.as_any().downcast::<BoolExpr>() {
212        match bool_expr.as_ref() {
213            BoolExpr::Or { var_type, terms } => {
214                let distributed_terms: Vec<Rc<BoolExpr>> = terms.iter().map(|t| distribute(t.clone())).collect();
215                let mut result_terms: Vec<Rc<BoolExpr>> = vec![Rc::new(BoolExpr::Term {
216                    var_type: var_type.clone(),
217                    term: Rc::new(BoolExpr::And { var_type: var_type.clone(), terms: vec![] }),
218                })];
219                for term in distributed_terms {
220                    if let BoolExpr::Or { terms: or_terms, .. } = term.as_ref() {
221                        let mut new_result_terms: Vec<Rc<BoolExpr>> = Vec::new();
222                        for res_term in &result_terms {
223                            for or_term in or_terms {
224                                new_result_terms.push(Rc::new(BoolExpr::And { var_type: var_type.clone(), terms: vec![res_term.clone(), or_term.clone()] }));
225                            }
226                        }
227                        result_terms = new_result_terms;
228                    } else {
229                        result_terms = result_terms.into_iter().map(|res_term| Rc::new(BoolExpr::And { var_type: var_type.clone(), terms: vec![res_term, term.clone()] })).collect();
230                    }
231                }
232                Rc::new(BoolExpr::Or { var_type: var_type.clone(), terms: result_terms })
233            }
234            BoolExpr::And { var_type, terms } => Rc::new(BoolExpr::Or { var_type: var_type.clone(), terms: terms.iter().map(|t| distribute(t.clone())).collect() }),
235            _ => bool_expr.clone(),
236        }
237    } else {
238        panic!("Expected a BoolExpr");
239    }
240}
241
242pub(crate) fn to_cnf(expr: Rc<dyn Var>) -> Rc<BoolExpr> {
243    distribute(push_negations(expr))
244}