open Bwd

type syn =
  | Var of int
  | Def of Name.t * value Lazy.t
  | Pi of Name.local * syn * (* BINDS *) syn
  | Lam of Name.local * (* BINDS *) syn
  | App of syn * syn
  | Sg of Name.local * syn * (* BINDS *) syn
  | Pair of syn * syn
  | Fst of syn
  | Snd of syn
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive_var : Name.local;
      motive : (* BINDS *) syn;
      true_case : syn;
      false_case : syn;
      scrut : syn;
    }

and value =
  | Neutral of ne
  | Unfold of unfold
  | Pi of Name.local * value * clo
  | Lam of Name.local * clo
  | Sg of Name.local * value * clo
  | Pair of value * value
  | Type
  | Bool
  | True
  | False

and ne = ne_head * frm bwd
and ne_head =
  | Var of int (* De Bruijn levels *)

and unfold = unfold_head * frm bwd * value Lazy.t
and unfold_head =
  | Def of Name.t * value Lazy.t

and frm = 
  | App of value
  | Fst
  | Snd
  | BoolElim of {
      motive_var : Name.local;
      motive: clo;
      true_case: value;
      false_case: value;
    }

and env = value bwd
and clo = Clo of { body : syn; env : env }