Skip to content

Instantly share code, notes, and snippets.

@TOTBWF
Last active November 30, 2022 05:29
Show Gist options
  • Save TOTBWF/9b2c071d2edb1c6596b785656c866fd6 to your computer and use it in GitHub Desktop.
Save TOTBWF/9b2c071d2edb1c6596b785656c866fd6 to your computer and use it in GitHub Desktop.
A simple single-file elaborator for MLTT
(** 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment