open Bwd

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

and ne = Data.ne
and ne_head = Data.ne_head =
  | Var of int (* De Bruijn levels *)

and unfold = Data.unfold
and unfold_head = Data.unfold_head =
  | Def of Name.t * t Lazy.t

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

and env = Data.env
and clo = Data.clo = Clo of { body : Data.syn; env : env }

let var i = Neutral (Var i, Emp)
let def p v = Unfold (Def (p, v), Emp, v)