%{
  open Closures_types

  module StrMap = Map.Make(String)


  let bind e = 
    let global_venv = ref Var.empty_env in

    let new_fresh str =
      let x, venv = Var.fresh str !global_venv in
      global_venv := venv;
      x in

    let new_binder str env =
      let x = new_fresh str in
      let env = StrMap.add str x env in
      x, env in

    let bind_var env x = 
      try StrMap.find x env
      with Not_found ->
        (* assume this is a global variable *)
        match Var.find x !global_venv with
          | None -> new_fresh x
          | Some v -> v
    in

    let rec bind_exp env : string _exp -> Var.t _exp = function
      | Var x -> Var (bind_var env x)
      | Pair (e1, e2) -> Pair (bind_exp env e1, bind_exp env e2)
      | App (e1, e2) ->  App (bind_exp env e1, bind_exp env e2)
      | Proj (p, e) -> Proj (p, bind_exp env e)
      | Let (x, e1, e2) ->
        let x, env = new_binder x env in
        let e1 = bind_exp env e1 in
        let e2 = bind_exp env e2 in
        Let (x, e1, e2)
      | Lam (x, sigma, t) ->
        let x, env = new_binder x env in
        let sigma = bind_ty env sigma in
        let t = bind_exp env t in
        Lam (x, sigma, t)
        
    and bind_ty env = function
      | Atom atom -> Atom atom
      | Product (t1, t2) ->
        let t1 = bind_ty env t1 in
        let t2 = bind_ty env t2 in
        Product (t1, t2)
      | Closure (gamma, x, sigma_phi, tau)  ->
        let gamma =
          let bind_binding env (x, sigma_phi) =
            (bind_var env x, bind_ann_ty env sigma_phi) in
          List.map (bind_binding env) gamma in
        let sigma_phi = bind_ann_ty env sigma_phi in
        let x, env = new_binder x env in
        let tau = bind_ty env tau in
        Closure (gamma, x, sigma_phi, tau)
  
    and bind_ann_ty env (sigma, ann) = (bind_ty env sigma, ann)

    in
    bind_exp StrMap.empty e
%}

%token <string>LATIN_INDENT
%token <string>GREEK_INDENT
%token BACKQUOTE_LPAREN LAMBDA_LPAREN
%token COLON
%token LPAREN RPAREN COMMA LBRACKET RBRACKET EMPTYSET
%token ARROW STAR
%token LET EQUAL IN
%token <bool>PI
%token CARET ZERO ONE HIGH_ZERO HIGH_ONE
%token EOF

%start <Closures_types.exp> main

%%

main:
| e = expr EOF { bind e }

expr:
| lambda b=binding(ty) RPAREN e=expr { let (x,sigma) = b in Lam (x,sigma,e) }
| LET x=evar EQUAL e1=expr IN e2=expr { Let (x,e1,e2) }
| e=simple_expr xs=list(simple_expr)
    { List.fold_left (fun f x -> App(f,x)) e xs }

simple_expr:
| x=evar { Var x }
| LPAREN e1=expr COMMA e2=expr RPAREN { Pair (e1, e2) }
| LPAREN e=expr RPAREN { e }
| p=PI e=simple_expr { Proj(p, e) }

lambda:
| BACKQUOTE_LPAREN { () }
| LAMBDA_LPAREN { () }

binding(ty):
| x=evar COLON sigma=ty { (x, sigma) }

evar:
| id=LATIN_INDENT { id }

ty:
| a=tvar { Atom a }
| LPAREN t1=ty STAR t2=ty RPAREN { Product (t1, t2) }
| LBRACKET gamma=context(ann_ty) RBRACKET
    LPAREN b=binding(ann_ty) RPAREN ARROW tau=ty
    { let (x,sigma_phi) = b in
      Closure (gamma, x, sigma_phi, tau) }

tvar:
| id=LATIN_INDENT { Const id }
| id=GREEK_INDENT { Const id }

context(ty):
| gamma=separated_list(COMMA,binding(ty)) { List.rev gamma }
| EMPTYSET { [] }

ann_ty:
| sigma=ty CARET ZERO { (sigma, true) }
| sigma=ty HIGH_ZERO { (sigma, true) }
| sigma=ty CARET ONE { (sigma, true) }
| sigma=ty HIGH_ONE { (sigma, true) }