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}