yatima_core/
eval.rs

1use core::ptr::NonNull;
2
3use crate::{
4  dag::*,
5  defs::Defs,
6  dll::*,
7  upcopy::*,
8};
9
10use sp_std::{
11  collections::btree_map::BTreeMap,
12  mem,
13  vec::Vec,
14};
15
16use alloc::string::String;
17
18enum Single {
19  Lam(Var),
20  Slf(Var),
21  Fix(Var),
22  Dat,
23  Cse,
24}
25
26enum Branch {
27  All(NonNull<All>),
28  App(NonNull<App>),
29  Ann(NonNull<Ann>),
30  Let(NonNull<Let>),
31}
32
33/// Substitutes a variable
34#[inline]
35pub fn subst(
36  bod: DAGPtr,
37  var: &Var,
38  arg: DAGPtr,
39  fix: bool,
40  should_count: bool,
41) -> DAGPtr {
42  let mut input = bod;
43  let mut top_branch = None;
44  let mut result = arg;
45  let mut spine = vec![];
46  loop {
47    match input {
48      DAGPtr::Lam(link) => {
49        let Lam { var, bod, .. } = unsafe { link.as_ref() };
50        input = *bod;
51        spine.push(Single::Lam(var.clone()));
52      }
53      DAGPtr::Slf(link) => {
54        let Slf { var, bod, .. } = unsafe { link.as_ref() };
55        input = *bod;
56        spine.push(Single::Slf(var.clone()));
57      }
58      DAGPtr::Fix(link) => {
59        let Fix { var, bod, .. } = unsafe { link.as_ref() };
60        input = *bod;
61        spine.push(Single::Fix(var.clone()));
62      }
63      DAGPtr::Dat(link) => {
64        let Dat { bod, .. } = unsafe { link.as_ref() };
65        input = *bod;
66        spine.push(Single::Dat);
67      }
68      DAGPtr::Cse(link) => {
69        let Cse { bod, .. } = unsafe { link.as_ref() };
70        input = *bod;
71        spine.push(Single::Cse);
72      }
73      DAGPtr::App(link) => {
74        let App { fun, arg: app_arg, .. } = unsafe { link.as_ref() };
75        let new_app = alloc_app(*fun, *app_arg, None);
76        unsafe {
77          (*link.as_ptr()).copy = Some(new_app);
78        }
79        top_branch = Some(Branch::App(link));
80        for parent in DLL::iter_option(var.parents) {
81          upcopy(arg, *parent, should_count);
82        }
83        result = DAGPtr::App(new_app);
84        break;
85      }
86      DAGPtr::All(link) => {
87        let All { uses, dom, img, .. } = unsafe { link.as_ref() };
88        let new_all = alloc_all(*uses, *dom, *img, None);
89        unsafe {
90          (*link.as_ptr()).copy = Some(new_all);
91        }
92        top_branch = Some(Branch::All(link));
93        for parent in DLL::iter_option(var.parents) {
94          upcopy(arg, *parent, should_count);
95        }
96        result = DAGPtr::All(new_all);
97        break;
98      }
99      DAGPtr::Ann(link) => {
100        let Ann { typ, exp, .. } = unsafe { link.as_ref() };
101        let new_ann = alloc_ann(*typ, *exp, None);
102        unsafe {
103          (*link.as_ptr()).copy = Some(new_ann);
104        }
105        top_branch = Some(Branch::Ann(link));
106        for parent in DLL::iter_option(var.parents) {
107          upcopy(arg, *parent, should_count);
108        }
109        result = DAGPtr::Ann(new_ann);
110        break;
111      }
112      DAGPtr::Let(link) => {
113        let Let { uses, typ, exp, bod, .. } = unsafe { link.as_ref() };
114        let new_let = alloc_let(*uses, *typ, *exp, *bod, None);
115        unsafe {
116          (*link.as_ptr()).copy = Some(new_let);
117        }
118        top_branch = Some(Branch::Let(link));
119        for parent in DLL::iter_option(var.parents) {
120          upcopy(arg, *parent, should_count);
121        }
122        result = DAGPtr::Let(new_let);
123        break;
124      }
125      // Otherwise it must be `var`, since `var` necessarily appears inside
126      // `body`
127      _ => break,
128    }
129  }
130  if fix && top_branch.is_none() && spine.is_empty() {
131    panic!("Infinite loop found");
132  }
133  while let Some(single) = spine.pop() {
134    match single {
135      Single::Lam(var) => {
136        let Var { nam, dep, parents: var_parents, .. } = var;
137        let new_lam = alloc_lam(nam, dep, result, None);
138        let ptr: *mut Parents = unsafe { &mut (*new_lam.as_ptr()).bod_ref };
139        add_to_parents(result, NonNull::new(ptr).unwrap());
140        let ptr: *mut Var = unsafe { &mut (*new_lam.as_ptr()).var };
141        for parent in DLL::iter_option(var_parents) {
142          upcopy(DAGPtr::Var(NonNull::new(ptr).unwrap()), *parent, should_count)
143        }
144        result = DAGPtr::Lam(new_lam);
145      }
146      Single::Slf(var) => {
147        let Var { nam, dep, parents: var_parents, .. } = var;
148        let new_slf = alloc_slf(nam, dep, result, None);
149        let ptr: *mut Parents = unsafe { &mut (*new_slf.as_ptr()).bod_ref };
150        add_to_parents(result, NonNull::new(ptr).unwrap());
151        let ptr: *mut Var = unsafe { &mut (*new_slf.as_ptr()).var };
152        for parent in DLL::iter_option(var_parents) {
153          upcopy(DAGPtr::Var(NonNull::new(ptr).unwrap()), *parent, should_count)
154        }
155        result = DAGPtr::Slf(new_slf);
156      }
157      Single::Fix(var) => {
158        let Var { nam, dep, parents: var_parents, .. } = var;
159        let new_fix = alloc_fix(nam, dep, result, None);
160        let ptr: *mut Parents = unsafe { &mut (*new_fix.as_ptr()).bod_ref };
161        add_to_parents(result, NonNull::new(ptr).unwrap());
162        let ptr: *mut Var = unsafe { &mut (*new_fix.as_ptr()).var };
163        for parent in DLL::iter_option(var_parents) {
164          upcopy(DAGPtr::Var(NonNull::new(ptr).unwrap()), *parent, should_count)
165        }
166        result = DAGPtr::Fix(new_fix);
167      }
168      Single::Dat => {
169        let new_dat = alloc_dat(result, None);
170        let ptr: *mut Parents = unsafe { &mut (*new_dat.as_ptr()).bod_ref };
171        add_to_parents(result, NonNull::new(ptr).unwrap());
172        result = DAGPtr::Dat(new_dat);
173      }
174      Single::Cse => {
175        let new_cse = alloc_cse(result, None);
176        let ptr: *mut Parents = unsafe { &mut (*new_cse.as_ptr()).bod_ref };
177        add_to_parents(result, NonNull::new(ptr).unwrap());
178        result = DAGPtr::Cse(new_cse);
179      }
180    }
181  }
182  // If the top branch is non-null, then clear the copies and fix the uplinks
183  if let Some(top_branch) = top_branch {
184    match top_branch {
185      Branch::App(link) => unsafe {
186        let top_app = &mut *link.as_ptr();
187        let link = top_app.copy.unwrap();
188        top_app.copy = None;
189        let App { fun, fun_ref, arg, arg_ref, .. } = &mut *link.as_ptr();
190        add_to_parents(*fun, NonNull::new(fun_ref).unwrap());
191        add_to_parents(*arg, NonNull::new(arg_ref).unwrap());
192      },
193      Branch::All(link) => unsafe {
194        let top_all = &mut *link.as_ptr();
195        let link = top_all.copy.unwrap();
196        top_all.copy = None;
197        let All { dom, dom_ref, img, img_ref, .. } = &mut *link.as_ptr();
198        add_to_parents(*dom, NonNull::new(dom_ref).unwrap());
199        add_to_parents(DAGPtr::Lam(*img), NonNull::new(img_ref).unwrap());
200      },
201      Branch::Ann(link) => unsafe {
202        let top_ann = &mut *link.as_ptr();
203        let link = top_ann.copy.unwrap();
204        top_ann.copy = None;
205        let Ann { typ, typ_ref, exp, exp_ref, .. } = &mut *link.as_ptr();
206        add_to_parents(*typ, NonNull::new(typ_ref).unwrap());
207        add_to_parents(*exp, NonNull::new(exp_ref).unwrap());
208      },
209      Branch::Let(link) => unsafe {
210        let top_let = &mut *link.as_ptr();
211        let link = top_let.copy.unwrap();
212        top_let.copy = None;
213        let Let { typ, typ_ref, exp, exp_ref, bod, bod_ref, .. } =
214          &mut *link.as_ptr();
215        add_to_parents(*typ, NonNull::new(typ_ref).unwrap());
216        add_to_parents(*exp, NonNull::new(exp_ref).unwrap());
217        add_to_parents(DAGPtr::Lam(*bod), NonNull::new(bod_ref).unwrap());
218      },
219    }
220    for parent in DLL::iter_option(var.parents) {
221      clean_up(parent);
222    }
223    let mut spine = bod;
224    loop {
225      match spine {
226        DAGPtr::Lam(link) => unsafe {
227          let Lam { var, bod, .. } = &mut *link.as_ptr();
228          for parent in DLL::iter_option(var.parents) {
229            clean_up(parent);
230          }
231          spine = *bod;
232        },
233        DAGPtr::Slf(link) => unsafe {
234          let Slf { var, bod, .. } = &mut *link.as_ptr();
235          for parent in DLL::iter_option(var.parents) {
236            clean_up(parent);
237          }
238          spine = *bod;
239        },
240        DAGPtr::Fix(link) => unsafe {
241          let Fix { var, bod, .. } = &mut *link.as_ptr();
242          for parent in DLL::iter_option(var.parents) {
243            clean_up(parent);
244          }
245          spine = *bod;
246        },
247        DAGPtr::Dat(link) => unsafe {
248          spine = link.as_ref().bod;
249        },
250        DAGPtr::Cse(link) => unsafe {
251          spine = link.as_ref().bod;
252        },
253        _ => break,
254      }
255    }
256  }
257  result
258}
259
260/// Contracts a lambda redex and return the body.
261#[inline]
262pub fn reduce_lam(
263  redex: NonNull<App>,
264  lam: NonNull<Lam>,
265  should_count: bool,
266) -> DAGPtr {
267  let App { arg, .. } = unsafe { redex.as_ref() };
268  let Lam { var, bod, parents, .. } = unsafe { &mut *lam.as_ptr() };
269  let top_node = if DLL::is_singleton(*parents) {
270    replace_child(DAGPtr::Var(NonNull::new(var).unwrap()), *arg);
271    *bod
272  }
273  else if var.parents.is_none() {
274    *bod
275  }
276  else {
277    subst(*bod, var, *arg, false, should_count)
278  };
279  replace_child(DAGPtr::App(redex), top_node);
280  free_dead_node(DAGPtr::App(redex));
281  top_node
282}
283
284/// Contracts a let redex and return the body.
285#[inline]
286pub fn reduce_let(redex: NonNull<Let>, should_count: bool) -> DAGPtr {
287  let Let { bod: lam, exp: arg, .. } = unsafe { redex.as_ref() };
288  let Lam { var, bod, parents, .. } = unsafe { &mut *lam.as_ptr() };
289  let top_node = if DLL::is_singleton(*parents) {
290    replace_child(DAGPtr::Var(NonNull::new(var).unwrap()), *arg);
291    *bod
292  }
293  else if var.parents.is_none() {
294    *bod
295  }
296  else {
297    subst(*bod, var, *arg, false, should_count)
298  };
299  replace_child(DAGPtr::Let(redex), top_node);
300  free_dead_node(DAGPtr::Let(redex));
301  top_node
302}
303
304pub fn print_trail(trail: &Vec<NonNull<App>>) -> Vec<String> {
305  let mut res: Vec<String> = vec![];
306  for link in trail {
307    let App { arg, .. } = unsafe { link.as_ref() };
308    res.push(format!("{}", arg));
309  }
310  res
311}
312
313impl DAG {
314  /// Reduces a DAG to its weak head normal form.
315  pub fn whnf(&mut self, defs: &Defs, should_count: bool) {
316    let mut node = self.head;
317    let mut trail: Vec<NonNull<App>> = vec![];
318    loop {
319      match node {
320        DAGPtr::App(link) => {
321          let App { fun, .. } = unsafe { link.as_ref() };
322          trail.push(link);
323          node = *fun;
324        }
325        DAGPtr::Lam(link) => {
326          if let Some(app_link) = trail.pop() {
327            node = reduce_lam(app_link, link, should_count);
328          }
329          else {
330            break;
331          }
332        }
333        DAGPtr::Ann(link) => {
334          let Ann { exp, .. } = unsafe { link.as_ref() };
335          replace_child(node, *exp);
336          free_dead_node(node);
337          node = *exp;
338        }
339        DAGPtr::Cse(link) => {
340          let mut body = unsafe { DAG::new((*link.as_ptr()).bod) };
341          body.whnf(defs, should_count);
342          match body.head {
343            DAGPtr::Dat(body_link) => {
344              let bod = unsafe { body_link.as_ref().bod };
345              replace_child(node, bod);
346              free_dead_node(node);
347              node = bod;
348            }
349            DAGPtr::Lit(link) => {
350              let Lit { lit, parents, .. } = unsafe { link.as_ref() };
351              match &lit.clone().expand() {
352                None => break,
353                Some(expand) => {
354                  let expand = DAG::from_term_inner(
355                    expand,
356                    0,
357                    BTreeMap::new(),
358                    *parents,
359                    None,
360                  );
361                  replace_child(node, expand);
362                  free_dead_node(node);
363                  node = expand;
364                }
365              }
366            }
367            _ => break,
368          }
369        }
370        DAGPtr::Let(link) => {
371          node = reduce_let(link, should_count);
372        }
373        DAGPtr::Fix(link) => unsafe {
374          let Fix { var, bod, .. } = &mut *link.as_ptr();
375          replace_child(node, *bod);
376          if var.parents.is_some() {
377            let new_fix =
378              alloc_fix(var.nam.clone(), 0, mem::zeroed(), None).as_mut();
379            let result = subst(
380              *bod,
381              var,
382              DAGPtr::Var(NonNull::new_unchecked(&mut new_fix.var)),
383              true,
384              should_count,
385            );
386            new_fix.bod = result;
387            add_to_parents(
388              result,
389              NonNull::new_unchecked(&mut new_fix.bod_ref),
390            );
391            replace_child(
392              DAGPtr::Var(NonNull::new(var).unwrap()),
393              DAGPtr::Fix(NonNull::new_unchecked(new_fix)),
394            );
395          }
396          free_dead_node(node);
397          node = *bod;
398        },
399        DAGPtr::Ref(link) => {
400          let Ref { nam, exp, ast, parents: ref_parents, .. } =
401            unsafe { &mut *link.as_ptr() };
402          if let Some(def) = defs.defs.get(exp) {
403            let parents = *ref_parents;
404            *ref_parents = None;
405            let ref_node = node;
406            node = DAG::from_ref(def, nam.clone(), *exp, *ast, parents);
407            free_dead_node(ref_node);
408            for parent in DLL::iter_option(parents) {
409              install_child(parent, node);
410            }
411          }
412          else {
413            panic!("undefined runtime reference: {}, {}", nam, exp);
414          }
415        }
416        DAGPtr::Opr(link) => {
417          let opr = unsafe { (*link.as_ptr()).opr.clone() };
418          let len = trail.len();
419          if len == 0 && opr.arity() == 0 {
420            let res = opr.apply0();
421            if let Some(res) = res {
422              node = DAGPtr::Lit(alloc_val(Lit { lit: res, parents: None }));
423            }
424            else {
425              break;
426            }
427          }
428          else if len >= 1 && opr.arity() == 1 {
429            let mut arg = unsafe { DAG::new((*trail[len - 1].as_ptr()).arg) };
430            arg.whnf(defs, should_count);
431            match arg.head {
432              DAGPtr::Lit(link) => {
433                let x = unsafe { &(*link.as_ptr()).lit };
434                let res = opr.apply1(x);
435                if let Some(res) = res {
436                  let top = DAGPtr::App(trail.pop().unwrap());
437                  let new_node =
438                    DAGPtr::Lit(alloc_val(Lit { lit: res, parents: None }));
439                  replace_child(top, new_node);
440                  free_dead_node(top);
441                  node = new_node;
442                }
443                else {
444                  break;
445                }
446              }
447              _ => break,
448            }
449          }
450          else if len >= 2 && opr.arity() == 2 {
451            let mut arg1 = unsafe { DAG::new((*trail[len - 1].as_ptr()).arg) };
452            let mut arg2 = unsafe { DAG::new((*trail[len - 2].as_ptr()).arg) };
453            arg1.whnf(defs, should_count);
454            arg2.whnf(defs, should_count);
455            match (arg1.head, arg2.head) {
456              (DAGPtr::Lit(x_link), DAGPtr::Lit(y_link)) => {
457                let x = unsafe { &(*x_link.as_ptr()).lit };
458                let y = unsafe { &(*y_link.as_ptr()).lit };
459                let res = opr.apply2(x, y);
460                if let Some(res) = res {
461                  trail.pop();
462                  let top = DAGPtr::App(trail.pop().unwrap());
463                  let new_node =
464                    DAGPtr::Lit(alloc_val(Lit { lit: res, parents: None }));
465                  replace_child(top, new_node);
466                  free_dead_node(top);
467                  node = new_node;
468                }
469                else {
470                  break;
471                }
472              }
473              _ => break,
474            }
475          }
476          else if len >= 3 && opr.arity() == 3 {
477            let mut arg1 = unsafe { DAG::new((*trail[len - 1].as_ptr()).arg) };
478            let mut arg2 = unsafe { DAG::new((*trail[len - 2].as_ptr()).arg) };
479            let mut arg3 = unsafe { DAG::new((*trail[len - 3].as_ptr()).arg) };
480            arg1.whnf(defs, should_count);
481            arg2.whnf(defs, should_count);
482            arg3.whnf(defs, should_count);
483            match (arg1.head, arg2.head, arg3.head) {
484              (
485                DAGPtr::Lit(x_link),
486                DAGPtr::Lit(y_link),
487                DAGPtr::Lit(z_link),
488              ) => {
489                let x = unsafe { &(*x_link.as_ptr()).lit };
490                let y = unsafe { &(*y_link.as_ptr()).lit };
491                let z = unsafe { &(*z_link.as_ptr()).lit };
492                let res = opr.apply3(x, y, z);
493                if let Some(res) = res {
494                  trail.pop();
495                  trail.pop();
496                  let top = DAGPtr::App(trail.pop().unwrap());
497                  let new_node =
498                    DAGPtr::Lit(alloc_val(Lit { lit: res, parents: None }));
499                  replace_child(top, new_node);
500                  free_dead_node(top);
501                  node = new_node;
502                }
503                else {
504                  break;
505                }
506              }
507              _ => break,
508            }
509          }
510          else {
511            break;
512          }
513        }
514        _ => break,
515      }
516    }
517    if trail.is_empty() {
518      self.head = node;
519    }
520    else {
521      self.head = DAGPtr::App(trail[0]);
522    }
523  }
524
525  /// Reduces a DAG to its normal form.
526  pub fn norm(&mut self, defs: &Defs, should_count: bool) {
527    self.whnf(defs, should_count);
528    let mut trail = vec![self.head];
529    while let Some(node) = trail.pop() {
530      match node {
531        DAGPtr::App(link) => unsafe {
532          let app = link.as_ptr();
533          let mut fun = DAG::new((*app).fun);
534          let mut arg = DAG::new((*app).arg);
535          fun.whnf(defs, should_count);
536          arg.whnf(defs, should_count);
537          trail.push(fun.head);
538          trail.push(arg.head);
539        },
540        DAGPtr::All(link) => unsafe {
541          let all = link.as_ptr();
542          let mut dom = DAG::new((*all).dom);
543          let mut img = DAG::new(DAGPtr::Lam((*all).img));
544          dom.whnf(defs, should_count);
545          img.whnf(defs, should_count);
546          trail.push(dom.head);
547          trail.push(img.head);
548        },
549        DAGPtr::Lam(link) => unsafe {
550          let lam = link.as_ptr();
551          let mut body = DAG::new((*lam).bod);
552          body.whnf(defs, should_count);
553          trail.push(body.head);
554        },
555        DAGPtr::Slf(link) => unsafe {
556          let slf = link.as_ptr();
557          let mut body = DAG::new((*slf).bod);
558          body.whnf(defs, should_count);
559          trail.push(body.head);
560        },
561        DAGPtr::Cse(link) => unsafe {
562          let cse = link.as_ptr();
563          let mut body = DAG::new((*cse).bod);
564          body.whnf(defs, should_count);
565          trail.push(body.head);
566        },
567        DAGPtr::Dat(link) => unsafe {
568          let dat = link.as_ptr();
569          let mut body = DAG::new((*dat).bod);
570          body.whnf(defs, should_count);
571          trail.push(body.head);
572        },
573        _ => (),
574      }
575    }
576  }
577}
578
579//#[cfg(test)]
580pub mod test {
581  use super::DAG;
582  use crate::{
583    defs::Defs,
584    parse::{
585      package,
586      span::Span,
587      term::input_cid,
588    },
589  };
590
591  pub fn parse(
592    i: &str,
593  ) -> nom::IResult<Span, DAG, crate::parse::error::ParseError<Span>> {
594    let (i, tree) = crate::parse::term::parse(i, Defs::new())?;
595    let (i, _) = nom::character::complete::multispace0(i)?;
596    let (i, _) = nom::combinator::eof(i)?;
597    let dag = DAG::from_term(&tree);
598    Ok((i, dag))
599  }
600  pub fn parse_defs(
601    i: &str,
602  ) -> nom::IResult<Span, Defs, crate::parse::error::ParseError<Span>> {
603    let (i, (defs, _)) =
604      package::parse_defs(input_cid(i), Defs::new())(Span::new(i))?;
605    Ok((i, defs))
606  }
607
608  #[test]
609  pub fn parse_test() {
610    fn parse_assert(input: &str) {
611      match parse(input) {
612        Ok((_, dag)) => assert_eq!(format!("{}", dag), input),
613        Err(_) => panic!("Did not parse."),
614      }
615    }
616    parse_assert("λ x => x");
617    parse_assert("λ x y => x y");
618    parse_assert("λ y => (λ x => x) y");
619    parse_assert("λ y => (λ z => z z) ((λ x => x) y)");
620  }
621
622  pub fn norm_assert(input: &str, result: &str) {
623    match parse(&input) {
624      Ok((_, mut dag)) => {
625        dag.norm(&Defs::new(), false);
626        assert_eq!(format!("{}", dag), result)
627      }
628      Err(_) => panic!("Did not parse."),
629    }
630  }
631
632  pub fn norm_assert_defs(input: &str, result: &str, defs: Defs) {
633    match parse(&input) {
634      Ok((_, mut dag)) => {
635        dag.norm(&defs, false);
636        assert_eq!(format!("{}", dag), result)
637      }
638      Err(_) => panic!("Did not parse."),
639    }
640  }
641
642  #[test]
643  pub fn reduce_test_ann() {
644    norm_assert("(Type :: Type)", "Type");
645    norm_assert("((λ x => x) #Nat :: Type)", "#Nat");
646    norm_assert("(λ A => A :: ∀ (A: Type) -> Type)", "λ A => A");
647    norm_assert("(λ A x => A :: ∀ (A: Type) (x: A) -> Type)", "λ A x => A");
648    norm_assert(
649      "(∀ (A: Type) (x: A) -> Type :: Type)",
650      "∀ (A: Type) (x: A) -> Type",
651    );
652    norm_assert("Type :: ∀ (A: Type) (x: A) -> Type", "Type");
653  }
654
655  #[test]
656  pub fn reduce_test_app() {
657    norm_assert(
658      "Type (∀ (A: Type) (x: A) -> Type)",
659      "Type (∀ (A: Type) (x: A) -> Type)",
660    );
661    norm_assert(
662      "(∀ (A: Type) (x: A) -> Type) Type",
663      "(∀ (A: Type) (x: A) -> Type) Type",
664    )
665  }
666
667  #[test]
668  pub fn reduce_test_all() {
669    norm_assert(
670      "∀ (f: ∀ (A: Type) (x: A) -> Type) -> Type",
671      "∀ (f: ∀ (A: Type) (x: A) -> Type) -> Type",
672    );
673    norm_assert(
674      "∀ (f: Type) -> ∀ (A: Type) (x: A) -> Type",
675      "∀ (f: Type) (A: Type) (x: A) -> Type",
676    );
677  }
678
679  #[test]
680  pub fn reduce_test_let() {
681    norm_assert("let f: Type = Type; f", "Type");
682    norm_assert("let f: ∀ (A: Type) (x: A) -> A = λ A x => x; f", "λ A x => x");
683    norm_assert(
684      "let f: Type = ∀ (A: Type) (x: A) -> A; f",
685      "∀ (A: Type) (x: A) -> A",
686    );
687    norm_assert(
688      "let f: Type = Type; ∀ (A: Type) (x: A) -> A",
689      "∀ (A: Type) (x: A) -> A",
690    );
691  }
692
693  #[test]
694  pub fn reduce_test() {
695    // Already normalized
696    norm_assert("λ x => x", "λ x => x");
697    norm_assert("λ x y => x y", "λ x y => x y");
698    // Not normalized cases
699    norm_assert("λ y => (λ x => x) y", "λ y => y");
700    norm_assert("λ y => (λ z => z z) ((λ x => x) y)", "λ y => y y");
701    // // Church arithmetic
702    let zero = "λ s z => z";
703    let one = "λ s z => (s z)";
704    let two = "λ s z => s (s z)";
705    let three = "λ s z => s (s (s z))";
706    let four = "λ s z => s (s (s (s z)))";
707    let seven = "λ s z => s (s (s (s (s (s (s z))))))";
708    let add = "λ m n s z => m s (n s z)";
709    let is_three = format!("(({}) ({}) {})", add, zero, three);
710    let is_three2 = format!("(({}) ({}) {})", add, one, two);
711    let is_seven = format!("(({}) ({}) {})", add, four, three);
712    norm_assert(&is_three, three);
713    norm_assert(&is_three2, three);
714    norm_assert(&is_seven, seven);
715    let id = "λ x => x";
716    norm_assert(
717      &format!("({three}) (({three}) ({id})) ({id})", id = id, three = three),
718      id,
719    );
720    let trm_str =
721      &format!("(({n}) (({m}) ({id})) {id})", n = three, m = three, id = id);
722    println!("{}", trm_str);
723    let (_, trm) = parse(trm_str).unwrap();
724    println!("{:?}", DAG::to_term(&trm, true));
725    // assert_eq!(true, false);
726    norm_assert(trm_str, id);
727  }
728}
yatima_core/eval.rs

yatima_core/
eval.rs
