# 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.lbox(), b.lbox()) }

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.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
TOP ==> define ID:@Var(x)@ = T:v {
  let nv = Def(true,x,v.lbox());
  //parser.exstate.push(parser.lbx(0,nv));
  nv 
 } <==

TOP ==> define lazy ID:@Var(x)@ = T:v {
  let nv = Def(false,x,v.lbox());
  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