yatima_core/
term.rs

1pub use crate::{
2  anon::Anon,
3  defs,
4  embed_error::EmbedError,
5  literal::{
6    LitType,
7    Literal,
8  },
9  meta::Meta,
10  name::Name,
11  parse,
12  position::Pos,
13  prim::Op,
14  uses::Uses,
15};
16
17use sp_cid::Cid;
18
19use sp_std::{
20  borrow::ToOwned,
21  boxed::Box,
22  fmt,
23  rc::Rc,
24};
25
26use alloc::string::{
27  String,
28  ToString,
29};
30
31/// Yatima terms with source positions
32#[derive(Clone)]
33pub enum Term {
34  /// Local variable
35  Var(Pos, Name, u64),
36  /// Lambda
37  Lam(Pos, Name, Box<Term>),
38  /// Application of a function to an argument
39  App(Pos, Box<(Term, Term)>),
40  /// Forall
41  All(Pos, Uses, Name, Box<(Term, Term)>),
42  /// Self type
43  Slf(Pos, Name, Box<Term>),
44  /// Self type constructor
45  Dat(Pos, Box<Term>),
46  /// Self type destructor
47  Cse(Pos, Box<Term>),
48  /// Immutable global reference to a term
49  Ref(Pos, Name, Cid, Cid),
50  /// Inline local definition
51  Let(Pos, bool, Uses, Name, Box<(Term, Term, Term)>),
52  /// Type of types
53  Typ(Pos),
54  /// Type annotation
55  Ann(Pos, Box<(Term, Term)>),
56  /// Primitive literal
57  Lit(Pos, Literal),
58  /// The type of a literal
59  LTy(Pos, LitType),
60  /// Primitive operation
61  Opr(Pos, Op),
62  /// Recursion marker
63  Rec(Pos),
64}
65
66impl fmt::Debug for Term {
67  fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
68    match self {
69      Self::Var(_, n, i) => fmt.debug_tuple("Var").field(&n).field(i).finish(),
70      Self::Lam(_, n, b) => fmt.debug_tuple("Lam").field(&n).field(&b).finish(),
71      Self::App(_, t) => fmt.debug_tuple("App").field(&t).finish(),
72      Self::All(_, u, n, t) => {
73        fmt.debug_tuple("All").field(&u).field(&n).field(&t).finish()
74      }
75      Self::Slf(_, n, b) => fmt.debug_tuple("Slf").field(&n).field(&b).finish(),
76      Self::Dat(_, b) => fmt.debug_tuple("Dat").field(&b).finish(),
77      Self::Cse(_, b) => fmt.debug_tuple("Cse").field(&b).finish(),
78      Self::Ref(_, n, d, a) => {
79        fmt.debug_tuple("Ref").field(&n).field(&d).field(&a).finish()
80      }
81      Self::Let(_, r, u, n, t) => {
82        fmt.debug_tuple("Let").field(r).field(&u).field(&n).field(&t).finish()
83      }
84      Self::Typ(_) => write!(fmt, "Typ(..)"),
85      Self::Ann(_, t) => fmt.debug_tuple("Ann").field(&t).finish(),
86      Self::Lit(_, a) => fmt.debug_tuple("Lit").field(&a).finish(),
87      Self::LTy(_, a) => fmt.debug_tuple("LTy").field(&a).finish(),
88      Self::Opr(_, a) => fmt.debug_tuple("Opr").field(&a).finish(),
89      Self::Rec(_) => write!(fmt, "Rec(..)"),
90    }
91  }
92}
93
94impl PartialEq for Term {
95  fn eq(&self, other: &Self) -> bool {
96    match (self, other) {
97      (Self::Var(_, na, ia), Self::Var(_, nb, ib)) => na == nb && ia == ib,
98      (Self::Lam(_, na, ba), Self::Lam(_, nb, bb)) => na == nb && ba == bb,
99      (Self::App(_, ta), Self::App(_, tb)) => ta.0 == tb.0 && ta.1 == tb.1,
100      (Self::All(_, ua, na, ta), Self::All(_, ub, nb, tb)) => {
101        ua == ub && na == nb && ta.0 == tb.0 && ta.1 == tb.1
102      }
103      (Self::Slf(_, na, ba), Self::Slf(_, nb, bb)) => na == nb && ba == bb,
104      (Self::Dat(_, ba), Self::Dat(_, bb)) => ba == bb,
105      (Self::Cse(_, ba), Self::Cse(_, bb)) => ba == bb,
106      (Self::Ref(_, na, da, aa), Self::Ref(_, nb, db, ab)) => {
107        na == nb && da == db && aa == ab
108      }
109      (Self::Let(_, ra, ua, na, ta), Self::Let(_, rb, ub, nb, tb)) => {
110        ra == rb
111          && ua == ub
112          && na == nb
113          && ta.0 == tb.0
114          && ta.1 == tb.1
115          && ta.2 == tb.2
116      }
117      (Self::Typ(_), Self::Typ(_)) => true,
118      (Self::Rec(_), Self::Rec(_)) => true,
119      (Self::Ann(_, ta), Self::Ann(_, tb)) => ta.0 == tb.0 && ta.1 == tb.1,
120      (Self::Lit(_, a), Self::Lit(_, b)) => a == b,
121      (Self::LTy(_, a), Self::LTy(_, b)) => a == b,
122      (Self::Opr(_, a), Self::Opr(_, b)) => a == b,
123      _ => false,
124    }
125  }
126}
127
128impl Term {
129  /// Returns the position of the term
130  pub fn pos(&self) -> Pos {
131    match self {
132      Term::Var(pos, ..) => *pos,
133      Term::Ref(pos, ..) => *pos,
134      Term::Lam(pos, ..) => *pos,
135      Term::App(pos, _) => *pos,
136      Term::Ann(pos, _) => *pos,
137      Term::All(pos, ..) => *pos,
138      Term::Slf(pos, ..) => *pos,
139      Term::Dat(pos, _) => *pos,
140      Term::Cse(pos, _) => *pos,
141      Term::Let(pos, ..) => *pos,
142      Term::Typ(pos) => *pos,
143      Term::LTy(pos, _) => *pos,
144      Term::Lit(pos, _) => *pos,
145      Term::Opr(pos, _) => *pos,
146      Term::Rec(pos) => *pos,
147    }
148  }
149
150  /// Shifts the term's de Bruijn index by a given incrementor
151  pub fn shift(self, inc: i64, dep: Option<u64>) -> Self {
152    match self {
153      Self::Var(pos, nam, idx) => match dep {
154        Some(dep) if idx < dep => Self::Var(pos, nam, idx),
155        _ => Self::Var(pos, nam, ((idx as i64) + inc) as u64),
156      },
157      Self::Lam(pos, nam, bod) => {
158        Self::Lam(pos, nam, Box::new((*bod).shift(inc, dep.map(|x| x + 1))))
159      }
160      Self::Slf(pos, nam, bod) => {
161        Self::Slf(pos, nam, Box::new((*bod).shift(inc, dep.map(|x| x + 1))))
162      }
163      Self::Cse(pos, bod) => Self::Cse(pos, Box::new((*bod).shift(inc, dep))),
164      Self::Dat(pos, bod) => Self::Dat(pos, Box::new((*bod).shift(inc, dep))),
165      Self::App(pos, fun_arg) => {
166        let (fun, arg) = *fun_arg;
167        Self::App(pos, Box::new((fun.shift(inc, dep), arg.shift(inc, dep))))
168      }
169      Self::Ann(pos, typ_exp) => {
170        let (typ, exp) = *typ_exp;
171        Self::Ann(pos, Box::new((typ.shift(inc, dep), exp.shift(inc, dep))))
172      }
173      Self::All(pos, uses, nam, dom_img) => {
174        let (dom, img) = *dom_img;
175        Self::All(
176          pos,
177          uses,
178          nam,
179          Box::new((dom.shift(inc, dep), img.shift(inc, dep.map(|x| x + 1)))),
180        )
181      }
182      Self::Let(pos, rec, uses, nam, typ_exp_bod) => {
183        let (typ, exp, bod) = *typ_exp_bod;
184        Self::Let(
185          pos,
186          rec,
187          uses,
188          nam,
189          Box::new((
190            typ.shift(inc, dep),
191            exp.shift(inc, if rec { dep.map(|x| x + 1) } else { dep }),
192            bod.shift(inc, dep.map(|x| x + 1)),
193          )),
194        )
195      }
196      x => x,
197    }
198  }
199
200  /// Unwinds a recursive function
201  pub fn un_rec(self, trm: Rc<Term>) -> Self {
202    match self {
203      Self::Rec(_) => trm.as_ref().clone(),
204      Self::Lam(pos, nam, bod) => {
205        Self::Lam(pos, nam, Box::new((*bod).un_rec(trm)))
206      }
207      Self::Slf(pos, nam, bod) => {
208        Self::Slf(pos, nam, Box::new((*bod).un_rec(trm)))
209      }
210      Self::Cse(pos, bod) => Self::Cse(pos, Box::new((*bod).un_rec(trm))),
211      Self::Dat(pos, bod) => Self::Dat(pos, Box::new((*bod).un_rec(trm))),
212      Self::App(pos, fun_arg) => {
213        let (fun, arg) = *fun_arg;
214        Self::App(pos, Box::new((fun.un_rec(trm.clone()), arg.un_rec(trm))))
215      }
216      Self::Ann(pos, typ_exp) => {
217        let (typ, exp) = *typ_exp;
218        Self::Ann(pos, Box::new((typ.un_rec(trm.clone()), exp.un_rec(trm))))
219      }
220      Self::All(pos, uses, nam, dom_img) => {
221        let (dom, img) = *dom_img;
222        Self::All(
223          pos,
224          uses,
225          nam,
226          Box::new((dom.un_rec(trm.clone()), img.un_rec(trm))),
227        )
228      }
229      Self::Let(pos, rec, uses, nam, typ_exp_bod) => {
230        let (typ, exp, bod) = *typ_exp_bod;
231        Self::Let(
232          pos,
233          rec,
234          uses,
235          nam,
236          Box::new((
237            typ.un_rec(trm.clone()),
238            exp.un_rec(trm.clone()),
239            bod.un_rec(trm),
240          )),
241        )
242      }
243      x => x,
244    }
245  }
246
247  /// Embeds term into anonymous data and metadata for package definition and
248  /// IPFS storage
249  pub fn embed(&self) -> (Anon, Meta) {
250    match self {
251      Self::Var(pos, name, idx) => {
252        (Anon::Var(*idx), Meta::Var(*pos, name.clone()))
253      }
254      Self::Ref(pos, name, def, ast) => {
255        (Anon::Ref(*ast), Meta::Ref(*pos, name.clone(), *def))
256      }
257      Self::Lit(pos, lit) => (Anon::Lit(lit.clone()), Meta::Lit(*pos)),
258      Self::LTy(pos, lty) => (Anon::LTy(*lty), Meta::LTy(*pos)),
259      Self::Opr(pos, opr) => (Anon::Opr(opr.clone()), Meta::Opr(*pos)),
260      Self::Rec(pos) => (Anon::Rec, Meta::Rec(*pos)),
261      Self::Typ(pos) => (Anon::Typ, Meta::Typ(*pos)),
262      Self::Lam(pos, name, body) => {
263        let (anon, meta) = (*body).embed();
264        (
265          Anon::Lam(Box::new(anon)),
266          Meta::Lam(*pos, name.clone(), Box::new(meta)),
267        )
268      }
269      Self::Slf(pos, name, body) => {
270        let (anon, meta) = (*body).embed();
271        (
272          Anon::Slf(Box::new(anon)),
273          Meta::Slf(*pos, name.clone(), Box::new(meta)),
274        )
275      }
276      Self::App(pos, terms) => {
277        let (fun_anon, fun_meta) = terms.0.embed();
278        let (arg_anon, arg_meta) = terms.1.embed();
279        (
280          Anon::App(Box::new((fun_anon, arg_anon))),
281          Meta::App(*pos, Box::new((fun_meta, arg_meta))),
282        )
283      }
284      Self::Ann(pos, terms) => {
285        let (typ_anon, typ_meta) = terms.0.embed();
286        let (exp_anon, exp_meta) = terms.1.embed();
287        (
288          Anon::Ann(Box::new((typ_anon, exp_anon))),
289          Meta::Ann(*pos, Box::new((typ_meta, exp_meta))),
290        )
291      }
292      Self::Dat(pos, body) => {
293        let (anon, meta) = (*body).embed();
294        (Anon::Dat(Box::new(anon)), Meta::Dat(*pos, Box::new(meta)))
295      }
296      Self::Cse(pos, body) => {
297        let (anon, meta) = (*body).embed();
298        (Anon::Cse(Box::new(anon)), Meta::Cse(*pos, Box::new(meta)))
299      }
300      Self::All(pos, uses, name, terms) => {
301        let (typ_anon, typ_meta) = terms.0.embed();
302        let (bod_anon, bod_meta) = terms.1.embed();
303        (
304          Anon::All(*uses, Box::new((typ_anon, bod_anon))),
305          Meta::All(*pos, name.clone(), Box::new((typ_meta, bod_meta))),
306        )
307      }
308      Self::Let(pos, rec, uses, name, terms) => {
309        let (typ_anon, typ_meta) = terms.0.embed();
310        let (exp_anon, exp_meta) = terms.1.embed();
311        let (bod_anon, bod_meta) = terms.2.embed();
312        (
313          Anon::Let(*rec, *uses, Box::new((typ_anon, exp_anon, bod_anon))),
314          Meta::Let(
315            *pos,
316            name.clone(),
317            Box::new((typ_meta, exp_meta, bod_meta)),
318          ),
319        )
320      }
321    }
322  }
323
324  /// Unembeds anon and meta into term
325  pub fn unembed(anon: &Anon, meta: &Meta) -> Result<Self, EmbedError> {
326    match (anon, meta) {
327      (Anon::Var(idx), Meta::Var(pos, nam)) => {
328        Ok(Self::Var(*pos, nam.clone(), *idx))
329      }
330      (Anon::Ref(ast), Meta::Ref(pos, nam, def)) => {
331        Ok(Self::Ref(*pos, nam.clone(), *def, *ast))
332      }
333      (Anon::Lit(lit), Meta::Lit(pos)) => Ok(Self::Lit(*pos, lit.clone())),
334      (Anon::LTy(lty), Meta::LTy(pos)) => Ok(Self::LTy(*pos, *lty)),
335      (Anon::Opr(opr), Meta::Opr(pos)) => Ok(Self::Opr(*pos, opr.clone())),
336      (Anon::Typ, Meta::Typ(pos)) => Ok(Self::Typ(*pos)),
337      (Anon::Rec, Meta::Rec(pos)) => Ok(Self::Rec(*pos)),
338      (Anon::Lam(anon_bod), Meta::Lam(pos, nam, meta_bod)) => {
339        let bod = Term::unembed(anon_bod, meta_bod)?;
340        Ok(Self::Lam(*pos, nam.clone(), Box::new(bod)))
341      }
342      (Anon::Slf(anon_bod), Meta::Slf(pos, nam, meta_bod)) => {
343        let bod = Term::unembed(anon_bod, meta_bod)?;
344        Ok(Self::Slf(*pos, nam.clone(), Box::new(bod)))
345      }
346      (Anon::Dat(anon_bod), Meta::Dat(pos, meta_bod)) => {
347        let bod = Term::unembed(anon_bod, meta_bod)?;
348        Ok(Self::Dat(*pos, Box::new(bod)))
349      }
350      (Anon::Cse(anon_bod), Meta::Cse(pos, meta_bod)) => {
351        let bod = Term::unembed(anon_bod, meta_bod)?;
352        Ok(Self::Cse(*pos, Box::new(bod)))
353      }
354      (Anon::App(anon), Meta::App(pos, meta)) => {
355        let (fun_anon, arg_anon) = anon.as_ref();
356        let (fun_meta, arg_meta) = meta.as_ref();
357        let fun = Term::unembed(fun_anon, fun_meta)?;
358        let arg = Term::unembed(arg_anon, arg_meta)?;
359        Ok(Self::App(*pos, Box::new((fun, arg))))
360      }
361      (Anon::Ann(anon), Meta::Ann(pos, meta)) => {
362        let (typ_anon, exp_anon) = anon.as_ref();
363        let (typ_meta, exp_meta) = meta.as_ref();
364        let typ = Term::unembed(typ_anon, typ_meta)?;
365        let exp = Term::unembed(exp_anon, exp_meta)?;
366        Ok(Self::Ann(*pos, Box::new((typ, exp))))
367      }
368      (Anon::All(uses, anon), Meta::All(pos, name, meta)) => {
369        let (dom_anon, img_anon) = anon.as_ref();
370        let (dom_meta, img_meta) = meta.as_ref();
371        let dom = Term::unembed(dom_anon, dom_meta)?;
372        let img = Term::unembed(img_anon, img_meta)?;
373        Ok(Self::All(*pos, *uses, name.clone(), Box::new((dom, img))))
374      }
375      (Anon::Let(rec, uses, anon), Meta::Let(pos, name, meta)) => {
376        let (typ_anon, exp_anon, bod_anon) = anon.as_ref();
377        let (typ_meta, exp_meta, bod_meta) = meta.as_ref();
378        let typ = Term::unembed(typ_anon, typ_meta)?;
379        let exp = Term::unembed(exp_anon, exp_meta)?;
380        let bod = Term::unembed(bod_anon, bod_meta)?;
381        Ok(Self::Let(
382          *pos,
383          *rec,
384          *uses,
385          name.clone(),
386          Box::new((typ, exp, bod)),
387        ))
388      }
389      (anon, meta) => Err(EmbedError::Term(anon.clone(), meta.clone())),
390    }
391  }
392
393  /// Formats term for pretty-printing
394  pub fn pretty(&self, rec: Option<&String>, ind: bool) -> String {
395    use Term::*;
396    const WILDCARD: &str = "_";
397
398    fn name(nam: &str) -> &str { if nam.is_empty() { WILDCARD } else { nam } }
399
400    fn uses(uses: &Uses) -> &str {
401      match uses {
402        Uses::None => "0 ",
403        Uses::Affi => "& ",
404        Uses::Once => "1 ",
405        Uses::Many => "",
406      }
407    }
408
409    fn is_atom(term: &Term) -> bool {
410      matches!(term, Var(..) | Ref(..) | Lit(..) | LTy(..) | Opr(..) | Typ(..))
411    }
412
413    fn lams(rec: Option<&String>, ind: bool, nam: &str, bod: &Term) -> String {
414      match bod {
415        Lam(_, nam2, bod2) => {
416          format!("{} {}", name(nam), lams(rec, ind, nam2, bod2))
417        }
418        _ => format!("{} => {}", nam, bod.pretty(rec, ind)),
419      }
420    }
421
422    fn alls(
423      rec: Option<&String>,
424      ind: bool,
425      use_: &Uses,
426      nam: &str,
427      typ: &Term,
428      bod: &Term,
429    ) -> String {
430      match bod {
431        All(_, bod_use, bod_nam, bod) => {
432          format!(
433            " ({}{}: {}){}",
434            uses(use_),
435            name(nam),
436            typ.pretty(rec, ind),
437            alls(rec, ind, bod_use, bod_nam, &bod.0, &bod.1)
438          )
439        }
440        _ => format!(
441          " ({}{}: {}) -> {}",
442          uses(use_),
443          name(nam),
444          typ.pretty(rec, ind),
445          bod.pretty(rec, ind)
446        ),
447      }
448    }
449
450    fn parens(rec: Option<&String>, ind: bool, term: &Term) -> String {
451      if is_atom(term) {
452        term.pretty(rec, ind)
453      }
454      else {
455        format!("({})", term.pretty(rec, ind))
456      }
457    }
458
459    fn apps(rec: Option<&String>, ind: bool, fun: &Term, arg: &Term) -> String {
460      match (fun, arg) {
461        (App(_, f), App(_, a)) => {
462          format!(
463            "{} ({})",
464            apps(rec, ind, &f.0, &f.1),
465            apps(rec, ind, &a.0, &a.1)
466          )
467        }
468        (App(_, f), arg) => {
469          format!("{} {}", apps(rec, ind, &f.0, &f.1), parens(rec, ind, arg))
470        }
471        (fun, App(_, a)) => {
472          format!("{} ({})", parens(rec, ind, fun), apps(rec, ind, &a.0, &a.1))
473        }
474        (fun, arg) => {
475          format!("{} {}", parens(rec, ind, fun), parens(rec, ind, arg))
476        }
477      }
478    }
479
480    match self {
481      Var(_, nam, index) => {
482        if ind {
483          format!("{}^{}", nam, index)
484        }
485        else {
486          nam.to_string()
487        }
488      }
489      Ref(_, nam, ..) => nam.to_string(),
490      Rec(_) => match rec {
491        Some(rec) => rec.to_owned(),
492        _ => "#^".to_string(),
493      },
494
495      Lam(_, nam, term) => format!("λ {}", lams(rec, ind, nam, term)),
496      App(_, terms) => apps(rec, ind, &terms.0, &terms.1),
497      Let(_, letrec, u, n, terms) => {
498        format!(
499          "let{} {}{}: {} = {}; {}",
500          if *letrec { "rec" } else { "" },
501          uses(u),
502          name(n),
503          terms.0.pretty(rec, ind),
504          terms.1.pretty(rec, ind),
505          terms.2.pretty(rec, ind),
506        )
507      }
508      Slf(_, nam, bod) => format!("@{} {}", name(nam), bod.pretty(rec, ind)),
509      All(_, us_, nam, terms) => {
510        format!("∀{}", alls(rec, ind, us_, nam, &terms.0, &terms.1))
511      }
512      Ann(_, terms) => {
513        format!(
514          "{} :: {}",
515          parens(rec, ind, &terms.1),
516          parens(rec, ind, &terms.0)
517        )
518      }
519      Dat(_, bod) => format!("data {}", bod.pretty(rec, ind)),
520      Cse(_, bod) => format!("case {}", bod.pretty(rec, ind)),
521      Typ(_) => "Type".to_string(),
522      Lit(_, lit) => format!("{}", lit),
523      LTy(_, lty) => format!("{}", lty),
524      Opr(_, opr) => format!("{}", opr),
525    }
526  }
527}
528
529impl fmt::Display for Term {
530  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
531    write!(f, "{}", self.pretty(None, false))
532  }
533}
534
535#[cfg(test)]
536pub mod tests {
537
538  use super::{
539    *,
540  };
541  use crate::{
542    defs::{
543      Def,
544      Defs,
545    },
546    yatima,
547  };
548  use quickcheck::{
549    Arbitrary,
550    Gen,
551  };
552  use sp_std::ops::Range;
553
554  use sp_im::Vector;
555  use sp_std::{
556    boxed::Box,
557    vec::Vec,
558  };
559
560  use crate::{
561    name::Name,
562    parse::term::is_valid_symbol_char,
563  };
564
565  pub fn arbitrary_name(g: &mut Gen) -> Name {
566    let s: String = Arbitrary::arbitrary(g);
567    let mut s: String = s
568      .chars()
569      .filter(|x| is_valid_symbol_char(*x) && char::is_ascii_alphabetic(x))
570      .collect();
571    s.truncate(1);
572    Name::from(format!("_{}", s))
573  }
574
575  pub fn test_defs() -> Defs {
576    let mut defs = Defs::new();
577    let (id, _) = Def::make(
578      Pos::None,
579      yatima!("∀ (A: Type) (x: A) -> A"),
580      yatima!("λ A x => x"),
581    );
582    let (fst, _) = Def::make(
583      Pos::None,
584      yatima!("∀ (A: Type) (x y: A) -> A"),
585      yatima!("λ A x y => x"),
586    );
587    let (snd, _) = Def::make(
588      Pos::None,
589      yatima!("∀ (A: Type) (x y: A) -> A"),
590      yatima!("λ A x y => y"),
591    );
592    defs.insert(Name::from("id"), id);
593    defs.insert(Name::from("fst"), fst);
594    defs.insert(Name::from("snd"), snd);
595    defs
596  }
597
598  fn arbitrary_ref(g: &mut Gen, defs: Defs, ctx: Vector<Name>) -> Tree {
599    let refs: Vec<(Name, Cid)> = defs
600      .names
601      .clone()
602      .into_iter()
603      .filter(|(n, _)| !ctx.contains(n))
604      .collect();
605    let len = refs.len();
606    if len == 0 {
607      return Tree::Typ;
608    };
609    let gen = gen_range(g, 0..(len - 1));
610    let (n, _) = refs[gen].clone();
611    let def = defs.get(&n).unwrap();
612    Tree::Ref(n.clone(), def.def_cid, def.ast_cid)
613  }
614
615  #[derive(Debug, Clone)]
616  pub enum Tree {
617    Var(Name, u64),
618    Typ,
619    Rec,
620    Ref(Name, Cid, Cid),
621    Opr(Op),
622    Lit(Literal),
623    LTy(LitType),
624    Lam(Name, usize),
625    Slf(Name, usize),
626    App(usize, usize),
627    Ann(usize, usize),
628    Cse(usize),
629    Dat(usize),
630    All(Uses, Name, usize, usize),
631    Let(bool, Uses, Name, usize, usize, usize),
632  }
633
634  impl Tree {
635    pub fn into_term(&self, arena: &Vec<Tree>) -> Term {
636      match self {
637        Self::Var(n, i) => Term::Var(Pos::None, n.clone(), *i),
638        Self::Rec => Term::Rec(Pos::None),
639        Self::Typ => Term::Typ(Pos::None),
640        Self::Ref(n, d, a) => Term::Ref(Pos::None, n.clone(), *d, *a),
641        Self::Opr(x) => Term::Opr(Pos::None, x.clone()),
642        Self::Lit(x) => Term::Lit(Pos::None, x.clone()),
643        Self::LTy(x) => Term::LTy(Pos::None, *x),
644        Self::Lam(n, bod) => {
645          let bod = arena[*bod].into_term(&arena);
646          Term::Lam(Pos::None, n.clone(), Box::new(bod))
647        }
648        Self::Slf(n, bod) => {
649          let bod = arena[*bod].into_term(&arena);
650          Term::Slf(Pos::None, n.clone(), Box::new(bod))
651        }
652        Self::Cse(bod) => {
653          let bod = arena[*bod].into_term(&arena);
654          Term::Cse(Pos::None, Box::new(bod))
655        }
656        Self::Dat(bod) => {
657          let bod = arena[*bod].into_term(&arena);
658          Term::Dat(Pos::None, Box::new(bod))
659        }
660        Self::App(fun, arg) => {
661          let fun = arena[*fun].into_term(&arena);
662          let arg = arena[*arg].into_term(&arena);
663          Term::App(Pos::None, Box::new((fun, arg)))
664        }
665        Self::Ann(typ, trm) => {
666          let typ = arena[*typ].into_term(&arena);
667          let trm = arena[*trm].into_term(&arena);
668          Term::Ann(Pos::None, Box::new((typ, trm)))
669        }
670        Self::All(uses, n, dom, img) => {
671          let dom = arena[*dom].into_term(&arena);
672          let img = arena[*img].into_term(&arena);
673          Term::All(Pos::None, *uses, n.clone(), Box::new((dom, img)))
674        }
675        Self::Let(rec, uses, n, typ, trm, bod) => {
676          let typ = arena[*typ].into_term(&arena);
677          let trm = arena[*trm].into_term(&arena);
678          let bod = arena[*bod].into_term(&arena);
679          Term::Let(
680            Pos::None,
681            *rec,
682            *uses,
683            n.clone(),
684            Box::new((typ, trm, bod)),
685          )
686        }
687      }
688    }
689  }
690
691  #[derive(Debug, Clone, Copy)]
692  pub enum Case {
693    VAR,
694    TYP,
695    REC,
696    REF,
697    LIT,
698    LTY,
699    OPR,
700    LAM,
701    APP,
702    ANN,
703    SLF,
704    CSE,
705    DAT,
706    ALL,
707    LET,
708  }
709
710  pub fn gen_range(g: &mut Gen, range: Range<usize>) -> usize {
711    let res: usize = Arbitrary::arbitrary(g);
712    (res % (range.end - range.start)) + range.start
713  }
714
715  pub fn next_case(g: &mut Gen, gens: &Vec<(usize, Case)>) -> Case {
716    let sum: usize = gens.iter().map(|x| x.0).sum();
717    let mut weight: usize = gen_range(g, 1..(sum + 1));
718    for gen in gens {
719      match weight.checked_sub(gen.0 + 1) {
720        None | Some(0) => {
721          return gen.1;
722        }
723        _ => {
724          weight -= gen.0;
725        }
726      }
727    }
728    panic!("Calculation error for weight = {}", weight);
729  }
730
731  pub fn arbitrary_term(
732    g: &mut Gen,
733    rec: bool,
734    defs: Defs,
735    ctx0: Vector<Name>,
736  ) -> Term {
737    let name = Name::from("_r");
738    let mut ctx1 = ctx0.clone();
739    ctx1.push_front(name.clone());
740    let mut ctxs: Vec<Vector<Name>> = vec![ctx0, ctx1];
741    let mut arena: Vec<Option<Tree>> = vec![Some(Tree::Lam(name, 1)), None];
742    let mut todo: Vec<usize> = vec![1];
743
744    while let Some(idx) = todo.pop() {
745      let ctx: Vector<Name> = ctxs[idx].clone();
746      let depth = ctx.len();
747      let gens: Vec<(usize, Case)> = vec![
748        (100, Case::VAR),
749        (100, Case::TYP),
750        (100, Case::REF),
751        (100, Case::LIT),
752        (100, Case::LTY),
753        (100, Case::OPR),
754        (if rec { 100 } else { 0 }, Case::REC),
755        (90usize.saturating_sub(depth), Case::LAM),
756        (90usize.saturating_sub(depth), Case::SLF),
757        (90usize.saturating_sub(depth), Case::CSE),
758        (90usize.saturating_sub(depth), Case::DAT),
759        (80usize.saturating_sub(2 * depth), Case::APP),
760        (80usize.saturating_sub(2 * depth), Case::ANN),
761        (80usize.saturating_sub(2 * depth), Case::ALL),
762        (30usize.saturating_sub(3 * depth), Case::LET),
763      ];
764
765      match next_case(g, &gens) {
766        Case::TYP => {
767          arena[idx] = Some(Tree::Typ);
768        }
769        Case::REC => {
770          arena[idx] = Some(Tree::Rec);
771        }
772        Case::LTY => {
773          arena[idx] = Some(Tree::LTy(Arbitrary::arbitrary(g)));
774        }
775        Case::LIT => {
776          arena[idx] = Some(Tree::Lit(Arbitrary::arbitrary(g)));
777        }
778        Case::OPR => {
779          arena[idx] = Some(Tree::Opr(Arbitrary::arbitrary(g)));
780        }
781        Case::REF => {
782          arena[idx] = Some(arbitrary_ref(g, defs.clone(), ctx.clone()));
783        }
784        Case::VAR => {
785          let gen = gen_range(g, 0..ctx.len());
786          let n = &ctx[gen];
787          let (i, _) = ctx.iter().enumerate().find(|(_, x)| *x == n).unwrap();
788          arena[idx] = Some(Tree::Var(n.clone(), i as u64));
789        }
790        Case::LAM => {
791          let n = arbitrary_name(g);
792          let mut ctx2 = ctx.clone();
793          ctx2.push_front(n.clone());
794          let bod = arena.len();
795          todo.push(bod);
796          ctxs.push(ctx2);
797          arena.push(None);
798          arena[idx] = Some(Tree::Lam(n, bod));
799        }
800        Case::SLF => {
801          let n = arbitrary_name(g);
802          let mut ctx2 = ctx.clone();
803          ctx2.push_front(n.clone());
804          let bod = arena.len();
805          todo.push(bod);
806          ctxs.push(ctx2);
807          arena.push(None);
808          arena[idx] = Some(Tree::Slf(n, bod));
809        }
810        Case::CSE => {
811          let bod = arena.len();
812          todo.push(bod);
813          ctxs.push(ctx.clone());
814          arena.push(None);
815          arena[idx] = Some(Tree::Cse(bod));
816        }
817        Case::DAT => {
818          let bod = arena.len();
819          todo.push(bod);
820          ctxs.push(ctx.clone());
821          arena.push(None);
822          arena[idx] = Some(Tree::Dat(bod));
823        }
824        Case::APP => {
825          let fun = arena.len();
826          todo.push(fun);
827          ctxs.push(ctx.clone());
828          arena.push(None);
829          let arg = arena.len();
830          todo.push(arg);
831          ctxs.push(ctx.clone());
832          arena.push(None);
833          arena[idx] = Some(Tree::App(fun, arg));
834        }
835        Case::ANN => {
836          let typ = arena.len();
837          todo.push(typ);
838          ctxs.push(ctx.clone());
839          arena.push(None);
840          let trm = arena.len();
841          todo.push(trm);
842          ctxs.push(ctx.clone());
843          arena.push(None);
844          arena[idx] = Some(Tree::Ann(typ, trm));
845        }
846        Case::ALL => {
847          let uses: Uses = Arbitrary::arbitrary(g);
848          let n = arbitrary_name(g);
849          let mut ctx2 = ctx.clone();
850          ctx2.push_front(n.clone());
851          let dom = arena.len();
852          todo.push(dom);
853          ctxs.push(ctx.clone());
854          arena.push(None);
855          let img = arena.len();
856          todo.push(img);
857          ctxs.push(ctx2);
858          arena.push(None);
859          arena[idx] = Some(Tree::All(uses, n, dom, img));
860        }
861        Case::LET => {
862          let letrec: bool = Arbitrary::arbitrary(g);
863          let uses: Uses = Arbitrary::arbitrary(g);
864          let n = arbitrary_name(g);
865          let mut ctx2 = ctx.clone();
866          ctx2.push_front(n.clone());
867          let typ = arena.len();
868          todo.push(typ);
869          ctxs.push(ctx.clone());
870          arena.push(None);
871          let trm = arena.len();
872          todo.push(trm);
873          if letrec {
874            ctxs.push(ctx2.clone());
875          }
876          else {
877            ctxs.push(ctx.clone())
878          };
879          arena.push(None);
880          let bod = arena.len();
881          todo.push(bod);
882          ctxs.push(ctx2.clone());
883          arena.push(None);
884          arena[idx] = Some(Tree::Let(letrec, uses, n, typ, trm, bod));
885        }
886      }
887    }
888    //    println!("arena: {:?}", arena);
889    let arena: Vec<Tree> = arena.into_iter().map(|x| x.unwrap()).collect();
890    //    println!("arena: {:?}", arena);
891    arena[0].into_term(&arena)
892  }
893
894  impl Arbitrary for Term {
895    fn arbitrary(g: &mut Gen) -> Self {
896      arbitrary_term(g, false, test_defs(), Vector::new())
897    }
898  }
899
900  #[quickcheck]
901  fn term_embed_unembed(x: Term) -> bool {
902    let (a, m) = x.clone().embed();
903    println!("x: {}", x);
904    match Term::unembed(&a, &m) {
905      Ok(y) => {
906        if x == y {
907          true
908        }
909        else {
910          // println!("x: {:?}", x);
911          // println!("y: {:?}", y);
912          false
913        }
914      }
915      _e => {
916        // println!("x: {:?}", x);
917        // println!("a: {:?}", a);
918        // println!("m: {:?}", m);
919        // println!("e: {:?}", _e);
920        false
921      }
922    }
923  }
924}
yatima_core/term.rs

yatima_core/
term.rs
