prune_lang/interp/
strategy.rs1use super::*;
2use itertools::Itertools;
3use std::fmt;
4
5#[derive(Clone, Debug)]
6pub struct Branch {
7 pub depth: usize,
8 pub answers: Vec<(Ident, TermVal<IdentCtx>)>,
9 pub prims: Vec<(Prim, Vec<AtomVal<IdentCtx>>)>,
10 pub calls: Vec<PredCall>,
11}
12
13impl fmt::Display for Branch {
14 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
15 writeln!(f, "##### depth: = {} #####", self.depth)?;
16
17 for (par, val) in self.answers.iter() {
18 writeln!(f, "{} = {}", par, val)?;
19 }
20
21 for (prim, args) in self.prims.iter() {
22 let args = args.iter().format(", ");
23 writeln!(f, "{:?}({})", prim, args)?;
24 }
25
26 for call in self.calls.iter() {
27 writeln!(f, "{}", call)?;
28 }
29
30 Ok(())
31 }
32}
33
34impl Branch {
35 pub fn new(pred: Ident, pars: Vec<Ident>, rule_cnt: usize) -> Branch {
36 let call = PredCall {
37 pred,
38 polys: Vec::new(),
39 args: pars.iter().map(|par| Term::Var(par.tag_ctx(0))).collect(),
40 looks: (0..rule_cnt).collect(),
41 history: History::new(),
42 };
43
44 Branch {
45 depth: 0,
46 answers: pars
47 .iter()
48 .map(|par| (*par, Term::Var(par.tag_ctx(0))))
49 .collect(),
50 prims: Vec::new(),
51 calls: vec![call],
52 }
53 }
54
55 pub fn clear_history(&mut self) {
56 for call in self.calls.iter_mut() {
57 call.history.clear();
58 }
59 }
60
61 pub fn merge(&mut self, unifier: Unifier<IdentCtx, LitVal, OptCons<Ident>>) {
62 for call in self.calls.iter_mut() {
63 for arg in call.args.iter_mut() {
64 *arg = unifier.subst(arg);
65 }
66 }
67
68 for (_par, val) in self.answers.iter_mut() {
69 *val = unifier.subst(val);
70 }
71 }
72
73 pub fn insert(&mut self, call_idx: usize, call: PredCall) {
74 self.calls.insert(call_idx, call);
75 }
76
77 pub fn remove(&mut self, call_idx: usize) -> PredCall {
78 self.calls.remove(call_idx)
79 }
80
81 #[allow(unused)]
82 pub fn random_strategy(&mut self) -> usize {
83 assert!(!self.calls.is_empty());
84 rand::random::<u32>().rem_euclid(self.calls.len() as u32) as usize
85 }
86
87 #[allow(unused)]
88 pub fn left_biased_strategy(&mut self) -> usize {
89 assert!(!self.calls.is_empty());
90 0
91 }
92
93 #[allow(unused)]
94 pub fn naive_strategy(&mut self, n: usize) -> usize {
95 assert!(!self.calls.is_empty());
96
97 let idx = self
98 .calls
99 .iter()
100 .position(|call| call.history.naive_strategy_pred(n));
101
102 if let Some(idx) = idx {
103 idx
104 } else {
105 self.clear_history();
106 self.naive_strategy(n)
107 }
108 }
109
110 #[allow(unused)]
111 pub fn struct_recur_strategy(&mut self) -> usize {
112 assert!(!self.calls.is_empty());
113
114 let idx = self.calls.iter().position(|call| {
115 call.history
116 .struct_recur_strategy_pred(call.pred, &call.args)
117 });
118
119 if let Some(idx) = idx {
120 idx
121 } else {
122 self.clear_history();
123 self.struct_recur_strategy()
124 }
125 }
126
127 pub fn lookahead_strategy(&mut self) -> usize {
128 let mut vec = Vec::new();
129
130 for call_idx in 0..self.calls.len() {
131 let call = &self.calls[call_idx];
132 if call.looks.len() <= 1 {
133 return call_idx;
134 }
135 vec.push(5 * call.looks.len() + call.history.len());
136 }
137
138 let (idx, _) = vec.iter().enumerate().min_by_key(|(_idx, br)| *br).unwrap();
139 idx
140 }
141}
142
143#[derive(Clone, Debug)]
144#[allow(dead_code)]
145pub struct PredCall {
146 pub pred: Ident,
147 pub polys: Vec<TermType>,
148 pub args: Vec<TermVal<IdentCtx>>,
149 pub looks: Vec<usize>,
150 pub history: History,
151}
152
153impl fmt::Display for PredCall {
154 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
155 let args = self.args.iter().format(", ");
156 if self.polys.is_empty() {
157 write!(f, "{}({})", self.pred, args)
158 } else {
159 let polys = self.polys.iter().format(", ");
160 write!(f, "{}[{}]({})", self.pred, polys, args)
161 }
162 }
163}
164
165impl PredCall {
166 fn try_unify_rule_head(&self, head: &[TermVal]) -> Result<(), ()> {
167 assert_eq!(head.len(), self.args.len());
168
169 let mut unifier: Unifier<IdentCtx, LitVal, OptCons<Ident>> = Unifier::new();
170 for (par, arg) in head.iter().zip(self.args.iter()) {
171 if unifier.unify(&par.tag_ctx(0), arg).is_err() {
172 return Err(());
173 }
174 }
175
176 Ok(())
177 }
178
179 pub fn lookahead_update(&mut self, rules: &[Rule]) {
180 let mut new_looks = self.looks.clone();
181 new_looks.retain(|look| self.try_unify_rule_head(&rules[*look].head).is_ok());
182 self.looks = new_looks
183 }
184}
185
186#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
187struct HistoryNode {
188 pred: Ident,
189 args_size: Vec<usize>,
190}
191
192#[derive(Clone, Debug, PartialEq)]
193pub struct History(Vec<HistoryNode>);
194
195impl History {
196 pub fn new() -> History {
197 History(Vec::new())
198 }
199
200 pub fn len(&self) -> usize {
201 self.0.len()
202 }
203
204 pub fn is_empty(&self) -> bool {
205 self.0.is_empty()
206 }
207
208 pub fn clear(&mut self) {
209 self.0.clear();
210 }
211
212 pub fn push(&mut self, pred: Ident, args_size: Vec<usize>) {
213 self.0.push(HistoryNode { pred, args_size });
214 }
215
216 pub fn left_biased_strategy_pred(&self) -> bool {
217 true
218 }
219
220 pub fn naive_strategy_pred(&self, n: usize) -> bool {
221 self.0.len() < n
222 }
223
224 pub fn struct_recur_strategy_pred(&self, pred: Ident, args: &[TermVal<IdentCtx>]) -> bool {
225 let args_size: Vec<usize> = args.iter().map(|arg| arg.height()).collect();
226
227 for node in self.0.iter() {
228 if node.pred == pred
229 && node
230 .args_size
231 .iter()
232 .zip(args_size.iter())
233 .all(|(arg0, arg)| arg0 <= arg)
234 {
235 return false;
236 }
237 }
238
239 true
240 }
241}
242
243impl Default for History {
244 fn default() -> Self {
245 Self::new()
246 }
247}