open Bwd

(** Syntactic terms *)

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

(** Semantic domain *)

type value =
  | Neutral of ne
  | Pi of Ident.local * value * clo
  | Lam of Ident.local * clo
  | Sg of Ident.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 frm = 
  | App of value
  | Fst
  | Snd
  | BoolElim of {
      motive_var : Ident.local;
      motive: clo;
      true_case: value;
      false_case: value;
    }

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