# Grammar for untyped lambda calculus

!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 TOP
nonterminal Vars
#nonterminal Moreargs
nonterminal LAMSYM
nonterminal Ts
topsym Ts
resync ;

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

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

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

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

# F used below to require ()s around expression
T --> CBV F:[x] { CBV(x) }
T --> weak F:[x] { Weak(x) }

#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); Seq(vs) }

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

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

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

TOP --> T:(x) { x }

LAMSYM --> lambda | lam | Lam


## untypedlexer specs
!use fixedstr::str16;
lexname DOT .
lexvalue INTEGER Num(n) Const(n)
lexvalue Liang Alphanum("liang") Nothing
lexvalue ID Alphanum(a) Var(str16::from(a))

EOF