A simple single-file elaborator for MLTT

MicroTT.ml

(** Core Types *)
module Syntax =
struct
  type t =
    | Local of int
    | Hole of string
    | Let of string * t * t
    | Lam of string * t
    | Ap of t * t
    | Pair of t * t
    | Fst of t
    | Snd of t
    | True
    | False
    | BoolElim of { motive : t; tcase : t; fcase : t; scrut : t }
    | Refl of t
    | J of { motive : t; refl : t; x: t; y: t; scrut: t }
    | Pi of string * t * t
    | Sg of string * t * t
    | Bool
    | Id of t * t * t
    | Univ

  let rec pp (pp_env : string list) (fmt : Format.formatter) (tm : t) : unit =
    match tm with
    | Local n ->
      Format.fprintf fmt "%s" (List.nth pp_env n) 
    | Hole nm ->
      Format.fprintf fmt "?%s" nm
    | Let (x, e, body) ->
      Format.fprintf fmt "@[let %s = %a in@ %a@]" x (pp (x :: pp_env)) e (pp pp_env) body
    | Lam (x, body) ->
      Format.fprintf fmt "@[%s =>@ %a@]" x (pp (x :: pp_env)) body
    | Ap (fn, arg) ->
      Format.fprintf fmt "%a %a" (pp pp_env) fn (pp pp_env) arg
    | Pair (fst, snd) ->
      Format.fprintf fmt "@[(%a, %a)@]" (pp pp_env) fst (pp pp_env) snd
    | Fst tm ->
      Format.fprintf fmt "fst %a" (pp pp_env) tm
    | Snd tm ->
      Format.fprintf fmt "snd %a" (pp pp_env) tm
    | True ->
      Format.fprintf fmt "true"
    | False ->
      Format.fprintf fmt "false"
    | BoolElim {motive; tcase; fcase; scrut} ->
      Format.fprintf fmt "bool/elim %a %a %a %a" (pp pp_env) motive (pp pp_env) tcase (pp pp_env) fcase (pp pp_env) scrut
    | Refl x ->
      Format.fprintf fmt "refl %a" (pp pp_env) x
    | J {motive; refl; x; y; scrut} ->
      Format.fprintf fmt "J %a %a %a %a %a" (pp pp_env) motive (pp pp_env) refl (pp pp_env) x (pp pp_env) y (pp pp_env) scrut
    | Pi (x, base, fam) ->
      Format.fprintf fmt "@[(%s : %a)@]@ -> %a" x (pp pp_env) base (pp (x :: pp_env)) fam 
    | Sg (x, base, fam) ->
      Format.fprintf fmt "@[(%s : %a)@]@ ** %a" x (pp pp_env) base (pp (x :: pp_env)) fam 
    | Bool ->
      Format.fprintf fmt "bool"
    | Id (a, x, y) ->
      Format.fprintf fmt "%a =[%a] %a" (pp pp_env) x (pp pp_env) a (pp pp_env) y
    | Univ ->
      Format.fprintf fmt "type"

  let pp_sequent (sequent : t list) (fmt : Format.formatter) (goal : t) : unit =
    let rec go pp_env fmt =
      function
      | [] -> Format.fprintf fmt "@,|- %a" (pp pp_env) goal
      | (tm :: tms) ->
        let x = "x" in
        Format.fprintf fmt "@[%s :@;%a@]@;%a" x (pp pp_env) tm (go (x :: pp_env)) tms
    in go [] fmt sequent
end

module Domain =
struct
  type t =
    | Cut of cut
    | Lam of string * clo
    | Pair of t * t
    | True
    | False
    | Refl of t
    | Pi of string * t * clo
    | Sg of string * t * clo
    | Bool
    | Id of t * t * t
    | Univ

  and cut = { hd : hd; spine : frm list }

  and hd =
    | Hole of string
    | Local of int
    | LetBind of int * t Lazy.t

  and frm =
    | Ap of t
    | Fst
    | Snd
    | BoolElim of { motive : t; tcase : t; fcase : t }
    | J of { motive : t; refl : t; x : t; y : t }

  and env = (t Lazy.t) list
  and clo = { tm : Syntax.t; env : env }

  module Env =
  struct
    let empty : env =
      []

    let extend (env : env) (v : t Lazy.t) : env =
      v :: env

    let index (env : env) (ix : int) =
      List.nth env ix

    let size (env : env) : int =
      List.length env
  end

  let local (lvl : int) : t =
    Cut { hd = Local lvl; spine = [] }

  let hole (nm : string) : t =
    Cut { hd = Hole nm; spine = [] }

  let let_bind (lvl : int) (v : t Lazy.t) : t =
    Cut { hd = LetBind (lvl, v); spine = [] }
end

module S = Syntax
module D = Domain

module TB =
struct
  type 'a m = int -> 'a

  let run (env : D.env) (k : 'a m) : 'a =
    k (List.length env)

  let var (lvl : int) : S.t m = 
    fun size ->
    S.Local (size - lvl - 1)

  let bind_var (k : int -> 'a m) : 'a m =
    fun size ->
    k size (size + 1)

  let scope (k : S.t m -> 'a m) : 'a m =
    bind_var (fun lvl -> k (var lvl))

  (** Helpers for Constructing Terms *)
  let let_ (x : string) (e : S.t m) (body : S.t m -> S.t m) : S.t m =
    fun env ->
    S.Let (x, e env, scope body env)

  let lam (x : string) (body : S.t m -> S.t m) : S.t m =
    fun env ->
    S.Lam (x, scope body env)

  let ap (fn : S.t m) (arg : S.t m) : S.t m =
    fun env ->
    S.Ap (fn env, arg env)

  let aps (fn : S.t m) (args : S.t m list) : S.t m =
    List.fold_left ap fn args

  let pair (t1 : S.t m) (t2 : S.t m) : S.t m =
    fun env ->
    S.Pair (t1 env, t2 env)

  let fst (t : S.t m) : S.t m =
    fun env ->
    S.Fst (t env)

  let snd (t : S.t m) : S.t m =
    fun env ->
    S.Snd (t env)

  let true_ : S.t m =
    fun _ ->
    S.True

  let false_ : S.t m =
    fun _ ->
    S.False

  let pi ?(name = "") (base : S.t m) (body : S.t m -> S.t m) : S.t m =
    fun env ->
    S.Pi (name, base env, scope body env)

  let sg ?(name = "") (base : S.t m) (body : S.t m -> S.t m) : S.t m =
    fun env ->
    S.Sg (name, base env, scope body env)

  let bool : S.t m =
    fun _ ->
    S.Bool

  let id (tp : S.t m) (x : S.t m) (y : S.t m) : S.t m =
    fun env ->
    S.Id (tp env, x env, y env)

  let refl (x : S.t m) : S.t m =
    fun env ->
    S.Refl (x env)

  let univ : S.t m =
    fun _ ->
    S.Univ
end

module Splice =
struct
  type 'a t = D.env -> 'a TB.m * D.env

  let value (v : D.t) (k : S.t TB.m -> 'a t) : 'a t =
    fun env ->
    let x = TB.var (List.length env) in
    let env = D.Env.extend env (Lazy.from_val v) in
    k x env

  let build (tb : 'a TB.m) : 'a t =
    fun env -> (tb, env)

  let compile (k : 'a t) : 'a * D.env =
    let (tb, env) = k D.Env.empty in
    (TB.run env tb, env)
end

module Eval =
struct
  let rec eval (env : D.env) (e : S.t) : D.t =
    match e with
    | Local ix ->
      Lazy.force @@ D.Env.index env ix
    | Hole nm ->
      D.hole nm
    | Let (x, e, body) ->
      let unf = D.let_bind (D.Env.size env) (Lazy.from_fun @@ fun () -> eval env e) in
      eval (D.Env.extend env @@ Lazy.from_val unf) body
    | Lam (x, body) ->
      D.Lam (x, { env; tm = body })
    | Ap (fn, arg) ->
      do_ap (eval env fn) (eval env arg)
    | Pair (t1, t2) ->
      D.Pair (eval env t1, eval env t2)
    | Fst t1 ->
      do_fst (eval env t1)
    | Snd t1 ->
      do_fst (eval env t1)
    | True ->
      D.True
    | False ->
      D.False
    | BoolElim {motive; tcase; fcase; scrut} ->
      do_bool_elim (eval env motive) (eval env tcase) (eval env fcase) (eval env scrut)
    | Refl x ->
      Refl (eval env x)
    | J {motive; refl; x; y; scrut} ->
      do_j (eval env motive) (eval env refl) (eval env x) (eval env y) (eval env scrut)
    | Pi (x, base, fam) -> 
      D.Pi (x, eval env base, { env; tm = fam })
    | Sg (x, base, fam) -> 
      D.Sg (x, eval env base, { env; tm = fam })
    | Bool ->
      D.Bool
    | Id (a, x, y) ->
      D.Id (eval env a, eval env x, eval env y)
    | Univ ->
      D.Univ

  and do_ap (fn : D.t) (arg : D.t) : D.t =
    match fn with
    | Lam (_, clo) -> inst_clo clo arg
    | Cut cut -> Cut (push_frm cut (D.Ap arg) (fun fn -> do_ap fn arg))
    | _ -> failwith "Bad do_ap"

  and do_fst (v : D.t) : D.t =
    match v with
    | Pair (v, _) -> v
    | Cut cut -> Cut (push_frm cut D.Fst do_fst)
    | _ -> failwith "bad do_fst"

  and do_snd (v : D.t) : D.t =
    match v with
    | Pair (v, _) -> v
    | Cut cut -> Cut (push_frm cut D.Snd do_snd)
    | _ -> failwith "bad do_fst"

  and do_bool_elim (motive : D.t) (tcase : D.t) (fcase : D.t) (scrut : D.t) : D.t =
    match scrut with
    | True -> tcase
    | False -> fcase
    | Cut cut -> Cut (push_frm cut (D.BoolElim {motive; tcase; fcase}) (do_bool_elim motive tcase fcase))
    | _ -> failwith "bad do_bool_elim"

  and do_j (motive : D.t) (refl : D.t) (x : D.t) (y : D.t) (scrut : D.t) : D.t =
    match scrut with
    | Refl x -> do_ap refl x
    | Cut cut -> Cut (push_frm cut (D.J {motive; refl; x; y}) (do_j motive refl x y))
    | _ -> failwith "bad do_j"

  and push_frm (cut : D.cut) (frm : D.frm) (unf : D.t -> D.t) : D.cut =
    let hd =
      match cut.hd with
      | Local ix ->  D.Local ix
      | Hole nm -> D.Hole nm
      | LetBind (lvl, v) -> D.LetBind(lvl, Lazy.map unf v)
    in { hd; spine = frm :: cut.spine }

  and inst_clo (clo : D.clo) (v : D.t) : D.t =
    eval (D.Env.extend clo.env @@ Lazy.from_val v) clo.tm

  and splice (k : S.t Splice.t) : D.t =
    let tm, env = Splice.compile k in
    eval env tm

  and unfold (tm : D.t) : D.t =
    match tm with
    | D.Cut { hd = D.LetBind (_, unf); spine } -> Lazy.force unf
    | tm -> tm
end

module Quote =
struct
  let bind_var (size : int) (k : int -> D.t ->'a)  : 'a  =
    k (size + 1) (D.Cut { hd = Local size; spine = [] }) 

  let rec quote (size : int) (v : D.t) : S.t =
    match v with
    | Cut cut ->
      quote_cut size cut
    | Lam (x, clo) ->
      S.Lam (x, quote_clo size clo)
    | Pair (v1, v2) ->
      S.Pair (quote size v1, quote size v2)
    | True ->
      S.True
    | False ->
      S.False
    | Refl x ->
      S.Refl (quote size x)
    | Pi (x, base, clo) ->
      S.Pi (x, quote size base, quote_clo size clo)
    | Sg (x, base, clo) ->
      S.Sg (x, quote size base, quote_clo size clo)
    | Bool ->
      S.Bool
    | Id (a, x, y) ->
      S.Id (quote size a, quote size x, quote size y)
    | Univ ->
      S.Univ

  and quote_cut (size : int) (cut : D.cut) : S.t =
    quote_spine size (quote_hd size cut.hd) cut.spine

  and quote_hd (size : int) (hd : D.hd) : S.t =
    match hd with
    | Local lvl -> S.Local (size - lvl - 1)
    | Hole nm -> S.Hole nm
    | LetBind (_, unf) -> quote size (Lazy.force unf)

  and quote_spine (size : int) (tm : S.t) : D.frm list -> S.t =
    function
    | [] -> tm
    | (frm :: spine) -> quote_spine size (quote_frm size tm frm) spine

  and quote_frm (size : int) (scrut : S.t) : D.frm -> S.t =
    function
    | D.Ap arg ->
      S.Ap (scrut, quote size arg)
    | D.Fst ->
      S.Fst scrut
    | D.Snd ->
      S.Fst scrut
    | D.BoolElim {motive; tcase; fcase} ->
      let motive = quote size motive in
      let tcase = quote size tcase in
      let fcase = quote size fcase in
      S.BoolElim {motive; tcase; fcase; scrut}
    | D.J {motive; refl; x; y} ->
      let motive = quote size motive in
      let refl = quote size refl in
      let x = quote size x in
      let y = quote size y in
      S.J {motive; refl; x; y; scrut}

  and quote_clo (size : int) (clo : D.clo) : S.t = 
    bind_var size (fun size arg -> quote size @@ Eval.inst_clo clo arg)
end

module Conversion =
struct
  exception NotConvertible

  type mode =
    | UnfoldAll
    | UnfoldOnHeadMismatch
    | UnfoldNothing

  type env = { mode : mode; size : int }

  let unfold (env : env) (tm : D.t) =
    match env.mode with
    | UnfoldAll -> Eval.unfold tm
    | _ -> tm

  let bind_var (env : env) (k : env -> D.t -> 'a) : 'a =
    k { env with size = env.size + 1 } (D.local env.size)

  let rec equate (env : env) (v0 : D.t) (v1 : D.t) : unit =
    match unfold env v0, unfold env v1 with
    | Cut cut0, Cut cut1 ->
      equate_cut env cut0 cut1
    | Lam (_, clo0), Lam (_, clo1) ->
      equate_clo env clo0 clo1
    | Pair (vfst0, vsnd0), Pair (vfst1, vsnd1) ->
      equate env vfst0 vfst1;
      equate env vsnd0 vsnd1
    | True, True ->
      ()
    | False, False ->
      ()
    | Refl x0, Refl x1 ->
      equate env x0 x1
    | Pi (_, base0, clo0), Pi (_, base1, clo1) ->
      equate env base0 base1;
      equate_clo env clo0 clo1;
    | Sg (_, base0, clo0), Sg (_, base1, clo1) ->
      equate env base0 base1;
      equate_clo env clo0 clo1;
    | Bool, Bool ->
      ()
    | Id (a0, x0, y0), Id (a1, x1, y1) ->
      equate env a0 a1;
      equate env x0 x1;
      equate env y0 y1;
    | Univ, Univ ->
      ()
    | Cut { hd = LetBind (_, unf); _ }, v
    | v, Cut { hd = D.LetBind (_, unf); _ } when env.mode = UnfoldOnHeadMismatch ->
      (* Before attempting eta expansion, let's unfold the let-bound variables. *)
      equate env (Lazy.force unf) v
    | Cut cut, v
    | v, Cut cut ->
      equate_eta env cut v
    | _ -> raise NotConvertible

  (** Equating cuts *)
  and equate_cut (env : env) (cut0 : D.cut) (cut1 : D.cut) : unit =
    match cut0.hd, cut1.hd with
    | D.Local lvl0, D.Local lvl1 when lvl0 = lvl1 -> ()
    | D.LetBind (lvl0, unf0), D.LetBind (lvl1, unf1) ->
      begin
        match env.mode with
        | UnfoldNothing ->
          if lvl0 = lvl1 then
            equate_spine env cut0.spine cut1.spine
          else
            raise NotConvertible
        | UnfoldOnHeadMismatch ->
          if lvl0 = lvl1 then
            try
              equate_spine { env with mode = UnfoldNothing } cut0.spine cut1.spine
            with NotConvertible ->
              equate { env with mode = UnfoldAll } (Lazy.force unf0) (Lazy.force unf1)
          else
            equate { env with mode = UnfoldOnHeadMismatch } (Lazy.force unf0) (Lazy.force unf1)
        | UnfoldAll ->
          failwith "The impossible happened! We didn't unfold a let binding while in full env."
      end
    | _ -> raise NotConvertible

  and equate_spine (env : env) (spine0 : D.frm list) (spine1 : D.frm list) : unit =
    match spine0, spine1 with
    | [], [] -> ()
    | (frm0 :: spine0, frm1 :: spine1) ->
      equate_frm env frm0 frm1;
      equate_spine env spine0 spine1
    | _ -> raise NotConvertible

  and equate_frm (env : env) (frm0 : D.frm) (frm1 : D.frm) : unit =
    match frm0, frm1 with
    | D.Ap v0, D.Ap v1 ->
      equate env v0 v1
    | D.Fst, D.Fst ->
      ()
    | D.Snd, D.Snd ->
      ()
    | D.BoolElim e0, D.BoolElim e1 ->
      equate env e0.motive e1.motive;
      equate env e0.tcase e1.tcase;
      equate env e0.fcase e1.fcase
    | D.J j0, D.J j1 ->
      equate env j0.motive j1.motive;
      equate env j0.refl j1.refl;
      equate env j0.x j1.x;
      equate env j0.y j1.y;
    | _, _ ->
      raise NotConvertible

  (** Equating modulo eta expansion *)
  and equate_eta (env : env) (cut0 : D.cut) (v1 : D.t) : unit =
    match unfold env v1 with
    | D.Cut cut1 ->
      equate_cut env cut0 cut1
    | D.Lam (x, clo) ->
      bind_var env @@ fun env arg ->
      let unf fn = Eval.do_ap fn arg in
      equate_eta env (Eval.push_frm cut0 (D.Ap arg) unf) (Eval.inst_clo clo arg)
    | D.Pair (vfst, vsnd) ->
      equate_eta env (Eval.push_frm cut0 D.Fst Eval.do_fst) vfst;
      equate_eta env (Eval.push_frm cut0 D.Snd Eval.do_snd) vsnd;
    | _ -> raise NotConvertible

  and equate_clo (env : env) (clo0 : D.clo) (clo1 : D.clo) : unit =
    bind_var env @@ fun env arg ->
    equate env (Eval.inst_clo clo0 arg) (Eval.inst_clo clo1 arg)
end


(** Logical Framework *)

module Tactics =
struct

  type env = { locals : D.env; types : (string * D.t) list }
  type syn = env -> D.t * S.t
  type chk = env -> D.t -> S.t
  type var = { tp : D.t; value : D.t }

  module Env =
  struct
    let size (env : env) = List.length env.locals

    let empty : env = { locals = []; types = [] }

    let extend (env : env) (name : string) (tp : D.t) (value : D.t) : env =
      { locals = Lazy.from_val value :: env.locals; types = (name, tp) :: env.types }
  end

  let eval (env : env) (tm : S.t) : D.t = 
    Eval.eval env.locals tm

  let quote (env : env) (v : D.t) : S.t =
    Quote.quote (Env.size env) v

  let equate (env : env) (v0 : D.t) (v1 : D.t) : unit =
    Conversion.equate { size = Env.size env; mode = UnfoldOnHeadMismatch } v0 v1

  let inst_clo (clo : D.clo) (v : D.t) : D.t =
    Eval.inst_clo clo v

  let run_chk (goal : D.t) (tac : chk) =
    tac Env.empty goal

  let run_syn (tac : syn) =
    tac Env.empty

  let run_tp (tac : chk) =
    eval Env.empty @@ tac Env.empty D.Univ

  let chk (syn : syn) : chk =
    fun env goal ->
    let (tp, tm) = syn env in
    equate env goal tp;
    tm

  let ann ~(tp : chk) (tm_tac : chk) : syn =
    fun env ->
    let tp = tp env D.Univ in
    let vtp = eval env tp in
    (vtp, tm_tac env vtp)

  let var (v : var) : syn =
    fun env ->
    let tm = quote env v.value in
    (v.tp, tm)

  let abstract (env : env) (name : string) (tp : D.t) (k : env -> var -> 'a)  : 'a =
    let var = D.local (Env.size env) in
    k (Env.extend env name tp var) { tp; value = var } 

  let let_bind (env : env) (name : string) (tp : D.t) (v : D.t Lazy.t) (k : env -> var -> 'a)  : 'a =
    let var = D.let_bind (Env.size env) v in
    k (Env.extend env name tp var) { tp; value = var } 

end

module T = Tactics

module Refiner =
struct
  exception TypeError

  module Pi =
  struct
    let intro ?(name = "_") (tac : T.syn -> T.chk) : T.chk =
      fun env goal ->
        match goal with
        | D.Pi (x, base, clo) ->
          T.abstract env x base @@ fun env v ->
          let vfib = T.inst_clo clo v.value in
          let tbody = tac (T.var v) env vfib in
          S.Lam (name, tbody)
        | _ -> raise TypeError

    let apply (fn_tac : T.syn) (arg_tac : T.chk) : T.syn =
      fun env ->
      let (fn_tp, fn) = fn_tac env in
      match fn_tp with
      | D.Pi (x, base, clo) ->
        let targ = arg_tac env base in
        let varg = T.eval env targ in
        let fib = T.inst_clo clo varg in
        (fib, S.Ap (fn, targ))
      | _ -> raise TypeError
  end

  module Sg =
  struct
    let intro (tac_fst : T.chk) (tac_snd : T.chk) : T.chk =
      fun env goal ->
        match goal with
        | D.Sg (x, base, clo) ->
          let tfst = tac_fst env base in
          let vfst = T.eval env tfst in
          let tsnd = tac_snd env (T.inst_clo clo vfst) in
          S.Pair (tfst, tsnd)
        | _ -> raise TypeError

    let fst (tac : T.syn) : T.syn =
      fun env ->
      let (pair_tp, tpair) = tac env in
      match pair_tp with
      | D.Sg (x, base, clo) ->
        (base, S.Fst tpair)
      | _ -> raise TypeError

    let snd (tac : T.syn) : T.syn =
      fun env ->
      let (pair_tp, tpair) = tac env in
      match pair_tp with
      | D.Sg (x, base, clo) ->
        let vfst = T.eval env (S.Fst tpair) in
        let fib = T.inst_clo clo vfst in
        (fib, S.Snd tpair)
      | _ -> raise TypeError
  end

  module Bool =
  struct
    let literal (b : bool) : T.chk =
      fun env goal ->
        match goal with
        | Bool ->
          if b then S.True else S.False
        | _ -> raise TypeError

    let elim (tac_motive : T.chk) (tac_tcase : T.chk) (tac_fcase : T.chk) (tac_scrut : T.syn) : T.syn =
      fun env ->
      let scrut_tp, scrut = tac_scrut env in
      let vscrut = T.eval env scrut in
      match scrut_tp with
      | Bool ->
        let motive_tp =
          Eval.splice @@
          Splice.build @@
          TB.pi TB.bool @@ fun _ -> TB.univ
        in
        let motive = tac_motive env motive_tp in
        let vmotive = T.eval env motive in
        let tcase_tp =
          Eval.splice @@
          Splice.value vmotive @@ fun motive ->
          Splice.build @@
          TB.ap motive TB.true_
        in
        let tcase = tac_tcase env tcase_tp in
        let fcase_tp =
          Eval.splice @@
          Splice.value vmotive @@ fun motive ->
          Splice.build @@
          TB.ap motive TB.false_
        in
        let fcase = tac_tcase env fcase_tp in
        let fib_tp =
          Eval.splice @@
          Splice.value vmotive @@ fun motive ->
          Splice.value vscrut @@ fun scrut ->
          Splice.build @@
          TB.ap motive scrut
        in
        (fib_tp, S.BoolElim {motive; tcase; fcase; scrut})
      | _ -> raise TypeError
  end

  module Id =
  struct
    let refl (tac : T.chk) : T.chk =
      fun env goal ->
        match goal with
        | Id (tp, x, y) ->
          let tm = tac env tp in
          let vtm = T.eval env tm in
          T.equate env x vtm;
          T.equate env y vtm;
          S.Refl tm
        | _ -> raise TypeError

    let j (tac_motive : T.chk) (tac_refl : T.chk) (tac_scrut : T.syn) : T.syn =
      fun env ->
      let scrut_tp, scrut = tac_scrut env in
      let vscrut = T.eval env scrut in
      match scrut_tp with
      | Id (a, vx, vy) ->
        let x = T.quote env vx in
        let y = T.quote env vy in
        let motive_tp =
          Eval.splice @@
          Splice.value a @@ fun a ->
          Splice.build @@
          TB.pi a @@ fun x -> TB.pi a @@ fun y ->
          TB.pi (TB.id a x y) @@ fun _ -> TB.univ
        in
        let motive = tac_motive env motive_tp in
        let vmotive = T.eval env motive in
        let refl_tp =
          Eval.splice @@
          Splice.value a @@ fun a ->
          Splice.value vmotive @@ fun motive ->
          Splice.build @@
          TB.pi a @@ fun x ->
          TB.aps motive [x; x; TB.refl x]
        in
        let refl =  tac_refl env refl_tp in
        let fib_tp =
          Eval.splice @@
          Splice.value vx @@ fun x ->
          Splice.value vy @@ fun y ->
          Splice.value vmotive @@ fun motive ->
          Splice.value vscrut @@ fun scrut ->
          Splice.build @@
          TB.aps motive [x; y; scrut]
        in
        (fib_tp, S.J {motive; refl; x; y; scrut})
      | _ -> raise TypeError
  end

  module Univ =
  struct
    let univ_tac (k : T.env -> D.t -> S.t) : T.chk =
      fun env goal ->
        match goal with
        | D.Univ ->
          k env D.Univ
        | _ -> raise TypeError

    let pi ?(name = "_") (tac_base : T.chk) (tac_fam : T.syn -> T.chk) : T.chk =
      univ_tac @@ fun env univ ->
      let tbase = tac_base env univ in
      let vbase = T.eval env tbase in
      T.abstract env name vbase @@ fun env v ->
      let tfam = tac_fam (T.var v) env univ in
      S.Pi (name, tbase, tfam)

    let sg ?(name = "_") (tac_base : T.chk) (tac_fam : T.syn -> T.chk) : T.chk =
      univ_tac @@ fun env univ ->
      let tbase = tac_base env univ in
      let vbase = T.eval env tbase in
      T.abstract env name vbase @@ fun env v ->
      let tfam = tac_fam (T.var v) env univ in
      S.Sg (name, tbase, tfam)

    let id (tac_tp : T.chk) (tac_x : T.chk) (tac_y : T.chk) : T.chk =
      univ_tac @@ fun env univ ->
      let tp = tac_tp env univ in
      let vtp = T.eval env tp in
      let tx = tac_x env vtp in
      let ty = tac_y env vtp in
      S.Id (tp, tx, ty)

    let univ : T.chk =
      univ_tac @@ fun _ _ ->
      S.Univ
  end 

  module Structural =
  struct
    let let_ ?(name = "_") (tac_e : T.syn) (tac_body : T.syn -> T.chk) : T.chk =
      fun env goal ->
        let (e_tp, te) = tac_e env in
        T.let_bind env name e_tp (Lazy.from_fun @@ fun () -> T.eval env te) @@ fun env v ->
        let tbody = tac_body (T.var v) env goal in
        S.Let (name, te, tbody)
  end

  module Hole =
  struct
    let unleash ?(name = "") ?(infer : T.syn option) : unit -> T.chk =
      fun _ env goal  ->
        let names = List.map fst env.types in
        let tgoal = T.quote env @@ Eval.unfold goal in
        Format.printf "Encountered Hole:@; @[%a@]@." (S.pp names) tgoal;
        let _ =
          match infer with
          | Some infer ->
            let vtp, _ = infer env in
            let tp = T.quote env vtp in
            Format.printf "Have:@; @[%a@]@." (S.pp names) tp
          | None -> ()
        in
        S.Hole name
  end
end

(** Examples *)
open Refiner

let id_tp =
  T.run_tp @@
  Univ.pi Univ.univ @@ fun a ->
  Univ.pi (T.chk a) @@ fun _ -> (T.chk a)

let id_tm =
  T.run_chk id_tp @@
  Pi.intro @@ fun _ ->
  Pi.intro @@ fun a ->
  T.chk a

let swap_involutive_tp =
  T.run_tp @@
  let swap_tp =
    Univ.pi Univ.univ @@ fun a ->
    Univ.pi Univ.univ @@ fun b ->
    Univ.pi (Univ.sg (T.chk a) (fun _ -> T.chk b)) @@ fun _ ->
    Univ.sg (T.chk b) (fun _ -> T.chk a)
  in
  let swap =
    Pi.intro @@ fun _ ->
    Pi.intro @@ fun _ ->
    Pi.intro @@ fun xy ->
    Sg.intro (T.chk @@ Sg.snd xy) (T.chk @@ Sg.fst xy)
  in
  Structural.let_ ~name:"swap" (T.ann ~tp:swap_tp swap) @@ fun swap ->
  Univ.pi ~name:"a" Univ.univ @@ fun a ->
  Univ.pi ~name:"b" Univ.univ @@ fun b ->
  Structural.let_ ~name:"ab" (T.ann ~tp:Univ.univ (Univ.sg (T.chk a) (fun _ -> T.chk b))) @@ fun ab ->
  Univ.pi ~name:"xy" (T.chk ab) @@ fun xy ->
  Univ.id (T.chk ab)
    (T.chk xy)
    (T.chk @@ Pi.apply (Pi.apply (Pi.apply swap (T.chk b)) (T.chk a)) @@ T.chk @@ Pi.apply (Pi.apply (Pi.apply swap (T.chk a)) (T.chk b)) (T.chk xy))

let swap_involutive =
  T.run_chk swap_involutive_tp @@
  Pi.intro @@ fun _ ->
  Pi.intro @@ fun _ ->
  Pi.intro ~name:"xy" @@ fun xy ->
  Id.refl (T.chk xy)

let sym_tp =
  T.run_tp @@
  Univ.pi ~name:"a" Univ.univ @@ fun a ->
  Univ.pi ~name:"x" (T.chk a) @@ fun x ->
  Univ.pi ~name:"y" (T.chk a) @@ fun y ->
  Univ.pi (Univ.id (T.chk a) (T.chk x) (T.chk y)) @@ fun _ ->
  Univ.id (T.chk a) (T.chk y) (T.chk x)

let sym = 
  T.run_chk sym_tp @@
  Pi.intro ~name:"a" @@ fun a ->
  Pi.intro ~name:"x" @@ fun x ->
  Pi.intro ~name:"y" @@ fun y ->
  Pi.intro ~name:"p" @@ fun p ->
  T.chk @@ Id.j (Pi.intro @@ fun x -> Pi.intro @@ fun y -> Pi.intro @@ fun _ -> Univ.id (T.chk a) (T.chk y) (T.chk x)) (Pi.intro @@ fun x -> Id.refl (T.chk x)) p