lambdascript 0.1.0

Educational tool illustrating beta reduction of untyped lambda terms, parser generation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

# Grammar for lambda calculus with step-by-step reduction

!use rustlr::{LBox,unbox};
!use crate::untyped::*;
!use crate::untyped::Term::*;

absyntype Term
externtype Vec<LBox<Term>>
terminals lambda lam Lam ( ) [ ] DOT let = in define lazy weak CBV Liang ;
terminal INTEGER
terminal ID
nonterminals T F Fs
nonterminal Vars
#nonterminal Moreargs
nonterminal LAMSYM
nonterminal Ts
topsym Ts
resync ;

# place defs in exstate
Ts --> T:x ;  { parser.exstate.push(x.lbox()); Nothing }
Ts --> Ts T:x ;  { parser.exstate.push(x.lbox()); Nothing }

# precedence order: T > Fs > F, Fs defines left-associative application.
# application binds tighter than abstraction.
Fs --> F:@a@ { a }
Fs --> Fs:a F:b { App(a.lbox(), b.lbox()) }

F --> ID:(x) { x } /* var */
F --> INTEGER:(x) { x } /* const*/

T --> Fs:@a@ { a }
F --> ( T:@a@ ) { a }

T --> CBV F:x { CBV(x.lbox()) }
T --> weak F:x { Weak(x.lbox()) }

#T --> LAMSYM ID:@Var(x)@ DOT T:b { Abs(x,b.lbox()) }
T ==> LAMSYM Vars:@Seq(mut vs)@ DOT T:b  {
  let mut t = b.value;
  while vs.len()>0 {
    t = Abs(getvar(&unbox!(vs.pop().unwrap())),parser.lbx(0,t));
  }
  return t; }
  <==

Vars --> ID:x { Seq(vec![x.lbox()]) }
Vars --> Vars:@Seq(mut vs)@ ID:y { vs.push(y.lbox()); Seq(vs) }


T --> let ID:@Var(x)@ = T:v in T:b  { App(parser.lbx(0,Abs(x,b.lbox())), v.lbox()) }


# define evaluate to the term being defined, but also affects global env
T ==> define ID:@Var(x)@ = T:v {
  let nv = Def(true,x,v.lbox());
  //parser.exstate.push(parser.lbx(0,nv));
  nv 
 } <==

T ==> define lazy ID:@Var(x)@ = T:v {
  let nv = Def(false,x,v.lbox());
  nv 
 } <==

LAMSYM --> lambda | lam | Lam

EOF


Everything after EOF is ignored ... alternate productions below are not
part of the grammar.

F ==> F:a Moreargs:@Seq(mut ts)@  {
  if ts.len()<1 {return a.value;}
  let mut apterm = App(a.lbox(), ts.pop().unwrap());
  while ts.len()>0 {
    apterm = App(parser.lbx(0,apterm), ts.pop().unwrap());
  }
  apterm }
  <==

T ==> LAMSYM Vars:@Seq(mut vs)@ DOT T:b  {
  let mut t = b.value;
  while vs.len()>0 {
    t = Abs(getvar(&unbox!(vs.pop().unwrap())),parser.lbx(0,t));
  }
  return t; }
  <==

Moreargs --> F:b { Seq(vec![b.lbox()]) }
Moreargs --> F:b Moreargs:ms@Seq(ts)@ { ts.push(b.lbox()); ms.value }

Vars --> ID:x { Seq(vec![x.lbox()]) }
Vars --> Vars:@Seq(mut vs)@ ID:y { vs.push(y.lbox()); Seq(vs) }