Current section
Files
Jump to
Current section
Files
src/ocaml/per.txt
open Printer
open Error
open Exp
let extPiG : value -> value * clos = function | VPi (t, g) -> (t, g) | u -> raise (ExpectedPi (rbV u))
let extSigG : value -> value * clos = function | VSig (t, g) -> (t, g) | u -> raise (ExpectedSig (rbV u))
let extSet : value -> Z.t = function | VPre n | VKan n -> n | v -> raise (ExpectedVSet (rbV v))
let extKan : value -> Z.t = function | VKan n -> n | v -> raise (ExpectedFibrant (rbV v))
let extPathP = function | VApp (VApp (VPathP v, u0), u1) -> (v, u0, u1) | v -> raise (ExpectedPath (rbV v))
let extVar ctx x = match Env.find_opt x ctx with | Some (_, _, Value (Var (y, _))) -> y | Some (_, _, Exp (EVar y)) -> y | _ -> x
let idv t x y = VApp (VApp (VId t, x), y)
let implv a b = VPi (a, (Irrefutable, fun _ -> b))
let hcompval u = EApp (EApp (u, ezero), ERef eone)
let imax a b = match a, b with
| VKan u, VKan v -> VKan (max u v)
| VPre u, VPre v | VPre u, VKan v | VKan u, VPre v -> VPre (max u v)
| VKan _, _ | VPre _, _ -> raise (ExpectedVSet (rbV b))
| _, _ -> raise (ExpectedVSet (rbV a))
let orEq f g = Disjunction.equal (Dnf.uniq (Dnf.extOr f)) (Dnf.uniq (Dnf.extOr g))
let andEq f g = Conjunction.equal (Dnf.extAnd f) (Dnf.extAnd g)
let compatible xs ys = Env.merge (fun _ x y -> match x, y with | Some d1, Some d2 -> Some (d1 = d2) | _, _ -> Some true) xs ys |> Env.for_all (fun _ b -> b)
let leq xs ys = Env.for_all (fun k d1 -> match Env.find_opt k ys with | Some d2 -> d1 = d2 | None -> false) xs
let lt xs ys = not (Env.equal (=) xs ys) && leq xs ys
let comparable xs ys = leq xs ys || leq ys xs
let meet = Env.union (fun _ x y -> if x = y then Some x else raise IncompatibleFaces)
let nubRev xs = let ys = ref [] in List.iter (fun x -> if not (List.mem x !ys) then ys := x :: !ys) xs; !ys
let meets xs ys = let zs = ref [] in List.iter (fun x -> List.iter (fun y -> try zs := meet x y :: !zs with IncompatibleFaces -> ()) ys) xs; nubRev !zs
let eps : face = Env.empty
let meetss = List.fold_left meets [eps]
let union xs ys = nubRev (List.rev_append xs ys)
let mkSystem xs = System.of_seq (List.to_seq xs)
let unionSystem xs ys = System.union (fun _ _ _ -> raise (Failure "unionSystem")) xs ys
let sign x = function | Zero -> ENeg (EVar x) | One -> EVar x
let getFace xs = Env.fold (fun x d y -> EAnd (y, sign x d)) xs (EDir One)
let getFormula ts = System.fold (fun x _ e -> EOr (getFace x, e)) ts (EDir Zero)
let singleton p x = Env.add p x Env.empty
let getFaceV xs = Env.fold (fun x d y -> Dnf.andFormula y (Dnf.contrAtom (x, d))) xs vone
let getFormulaV ts = System.fold (fun x _ v -> Dnf.orFormula (Dnf.getFaceV x) v) ts vzero
let rec solve k x = match k, x with
| VDir y, _ -> if x = y then [eps] else []
| Var (p, _), _ -> [singleton p x]
| VNeg n, _ -> solve n (negDir x)
| VOr (f, g), One | VAnd (f, g), Zero -> union (solve f x) (solve g x)
| VOr (f, g), Zero | VAnd (f, g), One -> meets (solve f x) (solve g x)
| _, _ -> failwith (Printf.sprintf "Cannot solve: %s = %s" (showExp (rbV k)) (showDir x))
let freshDim () = let i = freshName "ι" in (i, EVar i, Var (i, VI))
let ieq u v : bool = !girard || u = v
let vfst : value -> value = function | VPair (_, u, _) -> u | v -> VFst v
let vsnd : value -> value = function | VPair (_, _, u) -> u | v -> VSnd v
let rec eval (e0 : exp) (ctx : ctx) = match e0 with
| EPre u -> VPre u
| EKan u -> VKan u
| EVar x -> getRho ctx x
| EHole -> VHole
| EPi (a, (p, b)) -> let t = eval a ctx in VPi (t, (p, closByVal ctx p t b))
| ESig (a, (p, b)) -> let t = eval a ctx in VSig (t, (p, closByVal ctx p t b))
| ELam (a, (p, b)) -> let t = eval a ctx in VLam (t, (p, closByVal ctx p t b))
| EApp (f, x) -> app (eval f ctx, eval x ctx)
| EPair (r, e1, e2) -> VPair (r, eval e1 ctx, eval e2 ctx)
| EFst e -> vfst (eval e ctx)
| ESnd e -> vsnd (eval e ctx)
| EField (e, p) -> evalField p (eval e ctx)
| EId e -> VId (eval e ctx)
| ERef e -> VRef (eval e ctx)
| EJ e -> VJ (eval e ctx)
| EPathP e -> VPathP (eval e ctx)
| EPLam e -> VPLam (eval e ctx)
| EAppFormula (e, x) -> appFormula (eval e ctx) (eval x ctx)
| EI -> VI
| EDir d -> VDir d
| EAnd (e1, e2) -> evalAnd (eval e1 ctx) (eval e2 ctx)
| EOr (e1, e2) -> evalOr (eval e1 ctx) (eval e2 ctx)
| ENeg e -> Dnf.negFormula (eval e ctx)
| ETransp (p, i) -> VTransp (eval p ctx, eval i ctx)
| EHComp (t, r, u, u0) -> hcomp (eval t ctx) (eval r ctx) (eval u ctx) (eval u0 ctx)
| EPartial e -> let (i, _, _) = freshDim () in VLam (VI, (i, fun r -> let ts = mkSystem (List.map (fun mu -> (mu, eval e (faceEnv mu ctx))) (solve r One)) in VPartialP (VSystem ts, r)))
| EPartialP (t, r) -> VPartialP (eval t ctx, eval r ctx)
| ESystem xs -> VSystem (evalSystem ctx xs)
| ESub (a, i, u) -> VSub (eval a ctx, eval i ctx, eval u ctx)
| EInc (t, r) -> VInc (eval t ctx, eval r ctx)
| EOuc e -> evalOuc (eval e ctx)
| EEmpty -> VEmpty
| EIndEmpty e -> VIndEmpty (eval e ctx)
| EUnit -> VUnit
| EStar -> VStar
| EIndUnit e -> VIndUnit (eval e ctx)
| EBool -> VBool
| EFalse -> VFalse
| ETrue -> VTrue
| EIndBool e -> VIndBool (eval e ctx)
| EW (a, (p, b)) -> let t = eval a ctx in VW (t, (fresh p, closByVal ctx p t b))
| ESup (a, b) -> VSup (eval a ctx, eval b ctx)
| EIndW (a, b, c) -> VIndW (eval a ctx, eval b ctx, eval c ctx)
and appFormula v x = match v with
| VPLam f -> app (f, x)
| _ -> let (_, u0, u1) = extPathP (inferV v) in
begin match x with
| VDir Zero -> u0
| VDir One -> u1
| i -> VAppFormula (v, i)
end
and evalAnd a b = Dnf.evalAnd a b
and evalOr a b = Dnf.evalOr a b
and border xs v = mkSystem (List.map (fun alpha -> (alpha, upd alpha v)) xs)
and partialv t r = VPartialP (VSystem (border (solve r One) t) , r)
and transport p phi u0 = let (_, _, v) = freshDim () in match appFormula p v, phi with
(* transp p 1 u₀ ~> u₀ *)
| _, VDir One -> u0
(* transp (<_> U) i A ~> A *)
| VKan _, _ -> u0
(* transp (<i> Π (x : A i), B i x) φ u₀ ~> λ (x : A 1), transp (<i> B i (transFill (<j> A -j) φ x i)) φ (u₀ (transFill (<j> A -j) φ x 1)) *)
| VPi _, _ -> let x = fresh (ident "x") in
let (i, _, _) = freshDim () in let (j, _, _) = freshDim () in
let (t, _) = extPiG (appFormula p vone) in
VLam (t, (x, fun x ->
let v = transFill (VPLam (VLam (VI, (j, fun j ->
fst (extPiG (appFormula p (Dnf.negFormula j))))))) phi x in
transport (VPLam (VLam (VI, (i, fun i ->
let (_, (_, b)) = extPiG (appFormula p i) in
b (v (Dnf.negFormula i))))))
phi (app (u0, v vone))))
(* transp (<i> Σ (x : A i), B i x) φ u₀ ~> (transp (<j> A j) φ u₀.1, transp (<i> B i (transFill (<j> A j) φ u₀.1 i)) φ u₀.2) *)
| VSig _, _ ->
let (i, _, _) = freshDim () in let (j, _, _) = freshDim () in
let a = VPLam (VLam (VI, (j, fun j -> fst (extSigG (appFormula p j))))) in
let v1 = transFill a phi (vfst u0) in
let v2 = transport (VPLam (VLam (VI, (i, fun i ->
let (_, (_, b)) = extSigG (appFormula p i) in
b (v1 i))))) phi (vsnd u0) in
VPair (ref None, v1 vone, v2)
(* transp (<i> PathP (P i) (v i) (w i)) φ u₀ ~> <j> comp (λ i, P i @ j) (φ ∨ j ∨ -j) (λ (i : I), [(φ = 1) → u₀ @ j, (j = 0) → v i, (j = 1) → w i]) (u₀ @ j) *)
| VApp (VApp (VPathP _, _), _), _ ->
let i = fresh (ident "ι") in let j = fresh (ident "υ") in
VPLam (VLam (VI, (j, fun j ->
let uj = appFormula u0 j in let r = Dnf.orFormula phi (Dnf.orFormula j (Dnf.negFormula j)) in
comp (fun i -> let (q, _, _) = extPathP (appFormula p i) in appFormula q j) r
(VLam (VI, (i, fun i ->
let (_, v, w) = extPathP (appFormula p i) in
VSystem (unionSystem (border (solve phi One) uj)
(unionSystem (border (solve j Zero) v)
(border (solve j One) w)))))) uj)))
| _, _ -> VApp (VTransp (p, phi), u0)
and hcomp t r u u0 = match t, r with
(* hcomp A 1 u u₀ ~> u 1 1=1 *)
| _, VDir One -> app (app (u, vone), VRef vone)
(* hcomp (Π (x : A), B x) φ u u₀ ~> λ (x : A), hcomp (B x) φ (λ (i : I), [φ → u i 1=1 x]) (u₀ x) *)
| VPi (t, (_, b)), _ -> let (i, _, _) = freshDim () in let x = fresh (ident "x") in
VLam (t, (x, fun x ->
hcomp (b x) r (VLam (VI, (i, fun i ->
VSystem (border (solve r One)
(app (app (app (u, i), VRef vone), x)))))) (app (u0, x))))
(* hcomp (Σ (x : A), B x) φ u u₀ ~> (hfill A φ (λ (k : I), [(r = 1) → (u k 1=1).1]) u₀.1 1, comp (λ i, B (hfill A φ (λ (k : I), [(r = 1) → (u k 1=1).1]) u₀.1 i)) φ (λ (k : I), [(r = 1) → (u k 1=1).2]) u₀.2) *)
| VSig (t, (_, b)), _ ->
let (k, _, _) = freshDim () in
let v1 = hfill t r (VLam (VI, (k, fun k ->
VSystem (border (solve r One)
(vfst (app (app (u, k), VRef vone))))))) (vfst u0) in
let v2 = comp (v1 >> b) r (VLam (VI, (k, fun k ->
VSystem (border (solve r One)
(vsnd (app (app (u, k), VRef vone))))))) (vsnd u0) in
VPair (ref None, v1 vone, v2)
(* hcomp (PathP A v w) φ u u₀ ~> <j> hcomp (A @ j) (λ (i : I), [(r = 1) → u i 1=1, (j = 0) → v, (j = 1) → w]) (u₀ @ j) *)
| VApp (VApp (VPathP t, v), w), _ ->
let (j, _, _) = freshDim () in let (i, _, _) = freshDim () in
VPLam (VLam (VI, (j, fun j ->
hcomp (appFormula t j) (Dnf.orFormula r (Dnf.orFormula j (Dnf.negFormula j)))
(VLam (VI, (i, fun i ->
(VSystem (unionSystem (border (solve r One) (appFormula (app (app (u, i), VRef vone)) j))
(unionSystem (border (solve j Zero) v) (border (solve j One) w)))))))
(appFormula u0 j))))
| _, _ -> VHComp (t, r, u, u0)
and inc t r v = app (VInc (t, r), v)
and comp t r u u0 =
let (i, _, _) = freshDim () in let (j, _, _) = freshDim () in
hcomp (t vone) r (VLam (VI, (i, fun i ->
let u1 = transport (VPLam (VLam (VI, (j, fun j -> t (Dnf.orFormula i j))))) i (app (app (u, i), VRef vone)) in
VSystem (border (solve r One) u1))))
(transport (VPLam (VLam (VI, (i, t)))) vzero u0)
and hfill t r u u0 j =
let (i, _, _) = freshDim () in
hcomp t (Dnf.orFormula (Dnf.negFormula j) r)
(VLam (VI, (i, fun i ->
VSystem (unionSystem (border (solve r One)
(app (app (u, Dnf.andFormula i j), VRef vone)))
(border (solve j Zero) u0))))) u0
and transFill p phi u0 j = let (i, _, _) = freshDim () in
transport (VPLam (VLam (VI, (i, fun i -> appFormula p (Dnf.andFormula i j)))))
(Dnf.orFormula phi (Dnf.negFormula j)) u0
and closByVal ctx p t e v =
(* dirty hack to handle free variables introduced by type checker, for example, while checking terms like p : Path P a b *)
let ctx' = match v with
| Var (x, t) -> if Env.mem x ctx then ctx else upLocal ctx x t v
| _ -> ctx in
eval e (upLocal ctx' p t v)
and app : value * value -> value = function
| VApp (VApp (VApp (VApp (VJ _, _), _), f), _), VRef _ -> f
| VTransp (p, i), u0 -> transport p i u0
| VSystem ts, x -> reduceSystem ts x
| VLam (_, (_, f)), v -> f v
| VInc _, VOuc v -> v
| VApp (VIndUnit _, f), VStar -> f
| VApp (VApp (VIndBool _, f), _), VFalse -> f
| VApp (VApp (VIndBool _, _), g), VTrue -> g
| VApp (VIndW (a, b, c), g), VApp (VApp (VSup (_, b1), x), f) ->
let rec_call = VLam (app (b1, x), (fresh (ident "b"), fun b' -> app (app (VIndW (a, b, c), g), app (f, b')))) in
app (app (app (g, x), f), rec_call)
| f, x -> VApp (f, x)
and evalSystem ctx ts =
let ts' = System.fold (fun alpha talpha ->
Env.bindings alpha
|> List.rev_map (fun (i, d) -> solve (getRho ctx i) d)
|> meetss
|> List.rev_map (fun beta -> (beta, eval talpha (faceEnv beta ctx)))
|> List.rev_append) ts [] in
List.filter (fun (alpha, _) -> not (List.exists (fun (beta, _) -> lt beta alpha) ts')) ts' |> mkSystem
and reduceSystem ts x =
match System.find_opt eps ts with
| Some v -> v
| None -> VApp (VSystem ts, x)
and evalOuc v = match v, inferV v with
| _, VSub (_, VDir One, u) -> app (u, VRef vone)
| VApp (VInc _, v), _ -> v
| _, _ -> VOuc v
and getRho ctx x = match Env.find_opt x ctx with
| Some (_, _, Value v) -> v
| Some (_, _, Exp e) -> eval e ctx
| None -> raise (VariableNotFound x)
and act e i ctx = eval (EAppFormula (e, i)) ctx
and inferV v = match v with
| VPi (t, (x, f)) | VSig (t, (x, f)) -> imax (inferV t) (inferV (f (Var (x, t))))
| VLam (t, (x, f)) -> VPi (t, (x, fun x -> inferV (f x)))
| VPLam (VLam (VI, (_, g))) -> let t = VLam (VI, (freshName "ι", g >> inferV)) in VApp (VApp (VPathP (VPLam t), g vzero), g vone)
| VW (t, (x, f)) -> inferVTele imax t x f
| Var (_, t) -> t
| VFst e -> fst (extSigG (inferV e))
| VSnd e -> let (_, (_, g)) = extSigG (inferV e) in g (vfst e)
| VApp (VTransp (p, _), _) -> appFormula p vone
| VApp (f, x) ->
begin match inferV f with
| VPartialP (t, _) -> app (t, x)
| VPi (_, (_, g)) -> g x
| v -> raise (ExpectedPi (rbV v))
end
| VAppFormula (f, x) -> let (p, _, _) = extPathP (inferV f) in appFormula p x
| VRef v -> VApp (VApp (VId (inferV v), v), v)
| VPre n -> VPre (Z.succ n)
| VKan n -> VKan (Z.succ n)
| VI -> VPre Z.zero
| VInc (t, i) -> inferInc t i
| VOuc v ->
begin match inferV v with
| VSub (t, _, _) -> t
| _ -> raise (ExpectedSubtype (rbV v))
end
| VId v -> let n = extSet (inferV v) in implv v (implv v (VPre n))
| VJ v -> inferJ v (inferV v)
| VPathP p -> let (_, _, v) = freshDim () in let t = inferV (appFormula p v) in
let v0 = appFormula p vzero in let v1 = appFormula p vone in implv v0 (implv v1 t)
| VDir _ | VOr _ | VAnd _ | VNeg _ -> VI
| VTransp (p, _) -> implv (appFormula p vzero) (appFormula p vone)
| VHComp (t, _, _, _) -> t
| VSub (t, _, _) -> VPre (extSet (inferV t))
| VPartialP (VSystem ts, _) ->
begin match System.choose_opt ts with
| Some (_, t) -> VPre (extSet (inferV t))
| None -> VPre Z.zero
end
| VPartialP (t, _) -> inferV (inferV t)
| VSystem ts -> VPartialP (VSystem (System.map inferV ts), getFormulaV ts)
| VEmpty | VUnit | VBool -> VKan Z.zero
| VStar -> VUnit | VFalse | VTrue -> VBool
| VIndEmpty t -> implv VEmpty t
| VIndUnit t -> recUnit t
| VIndBool t -> recBool t
| VSup (a, b) -> inferSup a b
| VIndW (a, b, c) -> inferIndW a b c
| VPLam _ | VPair _ | VHole -> raise (InferError (rbV v))
and inferVTele g t x f = g (inferV t) (inferV (f (Var (x, t))))
and extByTag p : value -> value option = function
| VPair (t, fst, snd) ->
begin match !t with
| Some q -> if p = q then Some fst else extByTag p snd
| _ -> extByTag p snd
end
| _ -> None
and evalField p v =
match extByTag p v with
| Some k -> k | None -> begin match inferV v with
| VSig (_, (q, _)) -> if matchIdent p q then vfst v else evalField p (vsnd v)
| t -> raise (ExpectedSig (rbV t))
end
and upd e = function
| VLam (t, (x, g)) -> VLam (upd e t, (x, g >> upd e))
| VPair (r, u, v) -> VPair (r, upd e u, upd e v)
| VKan u -> VKan u
| VPi (t, (x, g)) -> VPi (upd e t, (x, g >> upd e))
| VSig (t, (x, g)) -> VSig (upd e t, (x, g >> upd e))
| VPre u -> VPre u
| VPLam f -> VPLam (upd e f)
| Var (i, VI) -> begin match Env.find_opt i e with | Some d -> VDir d | None -> Var (i, VI) end
| Var (x, t) -> Var (x, upd e t)
| VApp (f, x) -> app (upd e f, upd e x)
| VFst k -> vfst (upd e k)
| VSnd k -> vsnd (upd e k)
| VHole -> VHole
| VPathP v -> VPathP (upd e v)
| VPartialP (t, r) -> VPartialP (upd e t, upd e r)
| VSystem ts -> VSystem (System.bindings ts |> List.filter_map (fun (e', v) -> if compatible e e' then Some (Env.filter (fun k _ -> not (Env.mem k e)) e', upd e v) else None) |> mkSystem)
| VSub (t, i, u) -> VSub (upd e t, upd e i, upd e u)
| VTransp (p, i) -> VTransp (upd e p, upd e i)
| VHComp (t, r, u, u0) -> hcomp (upd e t) (upd e r) (upd e u) (upd e u0)
| VAppFormula (f, x) -> appFormula (upd e f) (upd e x)
| VId v -> VId (upd e v)
| VRef v -> VRef (upd e v)
| VJ v -> VJ (upd e v)
| VI -> VI
| VDir d -> VDir d
| VAnd (u, v) -> Dnf.andFormula (upd e u) (upd e v)
| VOr (u, v) -> Dnf.orFormula (upd e u) (upd e v)
| VNeg u -> Dnf.negFormula (upd e u)
| VInc (t, r) -> VInc (upd e t, upd e r)
| VOuc v -> evalOuc (upd e v)
| VEmpty -> VEmpty
| VIndEmpty v -> VIndEmpty (upd e v)
| VUnit -> VUnit
| VStar -> VStar
| VIndUnit v -> VIndUnit (upd e v)
| VBool -> VBool
| VFalse -> VFalse
| VTrue -> VTrue
| VIndBool v -> VIndBool (upd e v)
| VW (t, (x, g)) -> VW (upd e t, (x, g >> upd e))
| VSup (a, b) -> VSup (upd e a, upd e b)
| VIndW (a, b, c) -> VIndW (upd e a, upd e b, upd e c)
and updTerm alpha = function
| Exp e -> Exp e
| Value v -> Value (upd alpha v)
and faceEnv alpha ctx =
Env.map (fun (p, t, v) -> if p = Local then (p, updTerm alpha t, updTerm alpha v) else (p, t, v)) ctx
|> Env.fold (fun p dir -> Env.add p (Local, Value VI, Value (VDir dir))) alpha
and rbV v : exp = match v with
| VLam (t, g) -> rbVTele eLam t g
| VPair (r, u, v) -> EPair (r, rbV u, rbV v)
| VKan u -> EKan u
| VPi (t, g) -> rbVTele ePi t g
| VSig (t, g) -> rbVTele eSig t g
| VPre u -> EPre u
| VPLam f -> EPLam (rbV f)
| Var (x, _) -> EVar x
| VApp (f, x) -> EApp (rbV f, rbV x)
| VFst k -> EFst (rbV k)
| VSnd k -> ESnd (rbV k)
| VHole -> EHole
| VPathP v -> EPathP (rbV v)
| VPartialP (t, r) -> EPartialP (rbV t, rbV r)
| VSystem ts -> ESystem (System.map rbV ts)
| VSub (a, i, u) -> ESub (rbV a, rbV i, rbV u)
| VTransp (p, i) -> ETransp (rbV p, rbV i)
| VHComp (t, r, u, u0) -> EHComp (rbV t, rbV r, rbV u, rbV u0)
| VAppFormula (f, x) -> EAppFormula (rbV f, rbV x)
| VId v -> EId (rbV v)
| VRef v -> ERef (rbV v)
| VJ v -> EJ (rbV v)
| VI -> EI
| VDir d -> EDir d
| VAnd (u, v) -> EAnd (rbV u, rbV v)
| VOr (u, v) -> EOr (rbV u, rbV v)
| VNeg u -> ENeg (rbV u)
| VInc (t, r) -> EInc (rbV t, rbV r)
| VOuc v -> EOuc (rbV v)
| VEmpty -> EEmpty
| VIndEmpty v -> EIndEmpty (rbV v)
| VUnit -> EUnit
| VStar -> EStar
| VIndUnit v -> EIndUnit (rbV v)
| VBool -> EBool
| VFalse -> EFalse
| VTrue -> ETrue
| VIndBool v -> EIndBool (rbV v)
| VW (t, g) -> rbVTele eW t g
| VSup (a, b) -> ESup (rbV a, rbV b)
| VIndW (a, b, c) -> EIndW (rbV a, rbV b, rbV c)
and rbVTele ctor t (p, g) = let x = Var (p, t) in ctor p (rbV t) (rbV (g x))
and prune ctx x = match Env.find_opt x ctx with
| Some (_, _, Exp e) -> e
| Some (_, _, Value v) -> rbV v
| None -> raise (VariableNotFound x)
and conv v1 v2 : bool =
v1 == v2 || convInd v1 v2 || begin match v1, v2 with
| VKan u, VKan v -> ieq u v
| VPair (_, a, b), VPair (_, c, d) -> conv a c && conv b d
| VPair (_, a, b), v | v, VPair (_, a, b) -> conv (vfst v) a && conv (vsnd v) b
| VPi (a, (p, f)), VPi (b, (_, g))
| VSig (a, (p, f)), VSig (b, (_, g))
| VLam (a, (p, f)), VLam (b, (_, g)) -> let x = Var (p, a) in conv a b && conv (f x) (g x)
| VLam (a, (p, f)), b | b, VLam (a, (p, f)) -> let x = Var (p, a) in conv (app (b, x)) (f x)
| VW (a, (p, f)), VW (b, (_, g)) -> let x = Var (p, a) in conv a b && conv (f x) (g x)
| VPre u, VPre v -> ieq u v
| VPLam f, VPLam g -> conv f g
| VPLam f, v | v, VPLam f -> let (_, _, i) = freshDim () in conv (appFormula v i) (app (f, i))
| Var (u, _), Var (v, _) -> u = v
| VApp (f, a), VApp (g, b) -> conv f g && conv a b
| VFst x, VFst y | VSnd x, VSnd y -> conv x y
| VPathP a, VPathP b -> conv a b
| VPartialP (t1, r1), VPartialP (t2, r2) -> conv t1 t2 && conv r1 r2
| VAppFormula (f, x), VAppFormula (g, y) -> conv f g && conv x y
| VSystem xs, VSystem ys -> keys xs = keys ys && System.for_all (fun _ b -> b) (intersectionWith conv xs ys)
| VSystem xs, x | x, VSystem xs -> System.for_all (fun alpha y -> conv (app (upd alpha x, VRef vone)) y) xs
| VTransp (p, i), VTransp (q, j) -> conv p q && conv i j
| VHComp (t1, r1, u1, v1), VHComp (t2, r2, u2, v2) -> conv t1 t2 && conv r1 r2 && conv u1 u2 && conv v1 v2
| VSub (a, i, u), VSub (b, j, v) -> conv a b && conv i j && conv u v
| VOr (x, y), VDir Zero | VAnd (x, y), VDir One -> conv x v2 && conv y v2
| VOr (x, y), VDir One | VAnd (x, y), VDir Zero -> conv x v2 || conv y v2
| VOr _, _ | _, VOr _ -> orEq v1 v2
| VAnd _, _ | _, VAnd _ -> andEq v1 v2
| VNeg x, VNeg y -> conv x y
| VI, VI -> true
| VDir u, VDir v -> u = v
| VId u, VId v | VJ u, VJ v -> conv u v
| VInc (t1, r1), VInc (t2, r2) -> conv t1 t2 && conv r1 r2
| VOuc u, VOuc v -> conv u v
| VEmpty, VEmpty -> true
| VIndEmpty u, VIndEmpty v -> conv u v
| VUnit, VUnit -> true
| VStar, VStar -> true
| VIndUnit u, VIndUnit v -> conv u v
| VBool, VBool -> true
| VFalse, VFalse -> true
| VTrue, VTrue -> true
| VIndBool u, VIndBool v -> conv u v
| VSup (a1, b1), VSup (a2, b2) -> conv a1 a2 && conv b1 b2
| VIndW (a1, b1, c1), VIndW (a2, b2, c2) -> conv a1 a2 && conv b1 b2 && conv c1 c2
| _, _ -> false
end || convWithSystem (v1, v2) || convId v1 v2
and convWithSystem = function
| v, VApp (VSystem ts, _) | VApp (VSystem ts, _), v ->
System.for_all (fun mu -> conv (upd mu v)) ts
| _, _ -> false
and convId v1 v2 =
(* Id A a b is proof-irrelevant *)
try match inferV v1, inferV v2 with
| VApp (VApp (VId t1, a1), b1), VApp (VApp (VId t2, a2), b2) ->
conv t1 t2 && conv a1 a2 && conv b1 b2
| _, _ -> false
with ExpectedNeutral _ -> false
and convInd v1 v2 =
try match inferV v1, inferV v2 with
| VUnit, VUnit -> true
| VEmpty, VEmpty -> true
| _, _ -> false
with _ -> false
and eqNf v1 v2 : unit = if conv v1 v2 then () else raise (Ineq (rbV v1, rbV v2))
and lookup (x : ident) (ctx : ctx) = match Env.find_opt x ctx with
| Some (_, Value v, _) -> v
| Some (_, Exp e, _) -> eval e ctx
| None -> raise (VariableNotFound x)
and check ctx (e0 : exp) (t0 : value) =
try match e0, t0 with
| ELam (a, (p, b)), VPi (t, (_, g)) ->
ignore (extSet (infer ctx a)); eqNf (eval a ctx) t;
let x = Var (p, t) in let ctx' = upLocal ctx p t x in check ctx' b (g x)
| EPair (r, e1, e2), VSig (t, (p, g)) ->
ignore (extSet (inferV t)); check ctx e1 t;
check ctx e2 (g (eval e1 ctx));
begin match p with
| Ident (v, _) -> r := Some v
| Irrefutable -> ()
end
| EHole, v -> traceHole v ctx
| EPLam (ELam (EI, (i, e))), VApp (VApp (VPathP p, u0), u1) ->
let v = Var (i, VI) in let ctx' = upLocal ctx i VI v in
let v0 = eval e (upLocal ctx i VI vzero) in
let v1 = eval e (upLocal ctx i VI vone) in
check ctx' e (appFormula p v); eqNf v0 u0; eqNf v1 u1
| e, VPre u -> begin
match infer ctx e with
| VKan v | VPre v -> if ieq u v then () else raise (Ineq (rbV (VPre u), rbV (VPre v)))
| t -> raise (Ineq (rbV (VPre u), rbV t))
end
| ESystem ts, VPartialP (u, i) ->
eqNf (eval (getFormula ts) ctx) i;
System.iter (fun alpha e ->
check (faceEnv alpha ctx) e
(app (upd alpha u, VRef vone))) ts;
checkOverlapping ctx ts
| e, t -> eqNf (infer ctx e) t
with ex -> Printf.printf "When trying to typecheck\n %s\nAgainst type\n %s\n" (showExp e0) (showExp (rbV t0)); raise ex
and checkOverlapping ctx ts =
System.iter (fun alpha e1 ->
System.iter (fun beta e2 ->
if comparable alpha beta then
let ctx' = faceEnv (meet alpha beta) ctx in
eqNf (eval e1 ctx') (eval e2 ctx')
else ()) ts) ts
and infer ctx e : value = match e with
| EVar x -> lookup x ctx
| EKan u -> VKan (Z.succ u)
| EPi (a, (p, b)) -> inferTele ctx imax p a b
| ESig (a, (p, b)) | EW (a, (p, b)) -> inferTele ctx imax p a b
| ELam (a, (p, b)) -> inferLam ctx p a b
| EApp (f, x) -> begin match infer ctx f with
| VPartialP (t, i) -> check ctx x (isOne i); app (t, eval x ctx)
| VPi (t, (_, g)) -> check ctx x t; g (eval x ctx)
| v -> raise (ExpectedPi (rbV v))
end
| EFst e -> fst (extSigG (infer ctx e))
| ESnd e -> let (_, (_, g)) = extSigG (infer ctx e) in g (vfst (eval e ctx))
| EField (e, p) -> inferField ctx p e
| EPre u -> VPre (Z.succ u)
| EPathP p -> inferPath ctx p
| EPLam p -> inferV (eval (EPLam p) ctx)
| EPair (_, e1, e2) -> let t1 = infer ctx e1 in let t2 = infer ctx e2 in VSig (t1, (Irrefutable, fun _ -> t2))
| EPartial e -> let n = extSet (infer ctx e) in implv VI (VPre n)
| EPartialP (u, r0) -> check ctx r0 VI; let t = infer ctx u in
begin match t with
| VPartialP (ts, r) -> eqNf r (eval r0 ctx); inferV (inferV ts)
| _ -> failwith "Expected partial function into universe"
end
| EAppFormula (f, x) -> check ctx x VI; let (p, _, _) = extPathP (infer ctx (rbV (eval f ctx))) in appFormula p (eval x ctx)
| ETransp (p, i) -> inferTransport ctx p i
| EHComp (e, i, u, u0) -> let t = eval e ctx in let r = eval i ctx in ignore (extKan (infer ctx e)); check ctx i VI; check ctx u (implv VI (partialv t r)); check ctx u0 t;
List.iter (fun phi -> let ctx' = faceEnv phi ctx in eqNf (eval (hcompval u) ctx') (eval u0 ctx')) (solve r One); t
| ESub (a, i, u) -> let n = extSet (infer ctx a) in check ctx i VI; check ctx u (partialv (eval a ctx) (eval i ctx)); VPre n
| EI -> VPre Z.zero | EDir _ -> VI
| ENeg e -> check ctx e VI; VI
| EOr (e1, e2) | EAnd (e1, e2) -> check ctx e1 VI; check ctx e2 VI; VI
| EId e -> let v = eval e ctx in let n = extSet (infer ctx e) in implv v (implv v (VPre n))
| ERef e -> let v = eval e ctx in let t = infer ctx e in VApp (VApp (VId t, v), v)
| EJ e -> inferJ (eval e ctx) (infer ctx e)
| EInc (e, r) -> ignore (extKan (infer ctx e)); check ctx r VI; inferInc (eval e ctx) (eval r ctx)
| EOuc e -> begin match infer ctx e with | VSub (t, _, _) -> t | _ -> raise (ExpectedSubtype e) end
| ESystem ts -> checkOverlapping ctx ts; VPartialP (VSystem (System.map (infer ctx) ts), eval (getFormula ts) ctx)
| EEmpty | EUnit | EBool -> VKan Z.zero
| EStar -> VUnit | EFalse | ETrue -> VBool
| EIndEmpty e -> ignore (extSet (infer ctx e)); implv VEmpty (eval e ctx)
| EIndUnit e -> inferInd false ctx VUnit e recUnit
| EIndBool e -> inferInd false ctx VBool e recBool
| ESup (a, b) -> let t = eval a ctx in ignore (extSet (infer ctx a)); let (t', (p, g)) = extPiG (infer ctx b) in eqNf t t'; ignore (extSet (g (Var (p, t)))); inferSup t (eval b ctx)
| EIndW (a, b, c) -> let t = eval a ctx in ignore (extSet (infer ctx a));
let (t', (p, g)) = extPiG (infer ctx b) in eqNf t t'; ignore (extSet (g (Var (p, t))));
let (w', (q, h)) = extPiG (infer ctx c) in eqNf (wtype t (eval b ctx)) w';
ignore (extSet (h (Var (q, w'))));
inferIndW t (eval b ctx) (eval c ctx)
| e -> raise (InferError e)
and inferInd fibrant ctx t e f =
let (t', (p, g)) = extPiG (infer ctx e) in eqNf t t'; let k = g (Var (p, t)) in
ignore (if fibrant then extKan k else extSet k); f (eval e ctx)
and inferField ctx p e = match infer ctx e with
| VSig (t, (q, _)) -> if matchIdent p q then t else inferField ctx p (ESnd e)
| t -> raise (ExpectedSig (rbV t))
and inferTele ctx g p a b =
ignore (extSet (infer ctx a));
let t = eval a ctx in let x = Var (p, t) in
let ctx' = upLocal ctx p t x in
let v = infer ctx' b in g (infer ctx a) v
and inferLam ctx p a e =
ignore (extSet (infer ctx a)); let t = eval a ctx in
ignore (infer (upLocal ctx p t (Var (p, t))) e);
VPi (t, (p, fun x -> inferV (eval e (upLocal ctx p t x))))
and inferPath (ctx : ctx) (p : exp) =
let (i, x, v) = freshDim () in let ctx' = upLocal ctx i VI v in
let t = infer ctx' (rbV (act p x ctx')) in ignore (extSet t);
let v0 = act p ezero ctx in let v1 = act p eone ctx in implv v0 (implv v1 t)
and inferInc t r = let a = freshName "a" in
VPi (t, (a, fun v -> VSub (t, r, VSystem (border (solve r One) v))))
and inferTransport (ctx : ctx) (p : exp) (i : exp) =
check ctx i VI;
let u0 = act p ezero ctx in
let u1 = act p eone ctx in
let (j, x, v) = freshDim () in let ctx' = upLocal ctx j VI v in
ignore (extKan (infer ctx' (rbV (act p x ctx'))));
List.iter (fun phi -> let rho = faceEnv phi ctx' in eqNf (act p ezero rho) (act p x rho)) (solve (eval i ctx) One);
implv u0 u1
and inferJ v t =
let x = freshName "x" in let y = freshName "y" in let pi = freshName "P" in let p = freshName "p" in
let k = extSet t in let t = VPi (v, (x, fun x -> VPi (v, (y, fun y -> implv (idv v x y) (VPre k))))) in
VPi (t, (pi, fun pi ->
VPi (v, (x, fun x ->
implv (app (app (app (pi, x), x), VRef x))
(VPi (v, (y, fun y ->
VPi (idv v x y, (p, fun p ->
app (app (app (pi, x), y), p))))))))))
and recUnit t = let x = freshName "x" in implv (app (t, VStar)) (VPi (VUnit, (x, fun x -> app (t, x))))
and recBool t = let x = freshName "x" in implv (app (t, VFalse)) (implv (app (t, VTrue)) (VPi (VBool, (x, fun x -> app (t, x)))))
and wtype a b = VW (a, (freshName "x", fun x -> app (b, x)))
and inferSup a b = let t = wtype a b in let x = freshName "x" in VPi (a, (x, fun x -> implv (implv (app (b, x)) t) t))
and inferIndW a b c = let t = wtype a b in
implv (VPi (a, (freshName "x", fun x ->
VPi (implv (app (b, x)) t, (freshName "f", fun f ->
implv (VPi (app (b, x), (freshName "b", fun b -> app (c, (app (f, b))))))
(app (c, VApp (VApp (VSup (a, b), x), f))))))))
(VPi (t, (freshName "w", fun w -> app (c, w))))
let rec salt (ns : ident Env.t) : exp -> exp = function
| EKan n -> EKan n
| EPre n -> EPre n
| EVar x -> EVar (freshVar ns x)
| EHole -> EHole
| EPi (a, (p, b)) -> saltTele ePi ns p a b
| ELam (a, (p, b)) -> saltTele eLam ns p a b
| EApp (f, x) -> EApp (salt ns f, salt ns x)
| ESig (a, (p, b)) -> saltTele eSig ns p a b
| EPair (r, a, b) -> EPair (r, salt ns a, salt ns b)
| EFst e -> EFst (salt ns e)
| ESnd e -> ESnd (salt ns e)
| EField (e, p) -> EField (salt ns e, p)
| EId e -> EId (salt ns e)
| ERef e -> ERef (salt ns e)
| EJ e -> EJ (salt ns e)
| EPathP e -> EPathP (salt ns e)
| ETransp (p, i) -> ETransp (salt ns p, salt ns i)
| EHComp (t, r, u, u0) -> EHComp (salt ns t, salt ns r, salt ns u, salt ns u0)
| EPLam e -> EPLam (salt ns e)
| EAppFormula (p, i) -> EAppFormula (salt ns p, salt ns i)
| EPartial e -> EPartial (salt ns e)
| EPartialP (t, r) -> EPartialP (salt ns t, salt ns r)
| ESub (a, i, u) -> ESub (salt ns a, salt ns i, salt ns u)
| ESystem xs -> ESystem (System.fold (fun k v -> System.add (freshFace ns k) (salt ns v)) xs System.empty)
| EInc (t, r) -> EInc (salt ns t, salt ns r)
| EOuc e -> EOuc (salt ns e)
| EDir d -> EDir d
| EI -> EI
| EAnd (a, b) -> EAnd (salt ns a, salt ns b)
| EOr (a, b) -> EOr (salt ns a, salt ns b)
| ENeg e -> ENeg (salt ns e)
| EEmpty -> EEmpty
| EIndEmpty e -> EIndEmpty (salt ns e)
| EUnit -> EUnit
| EStar -> EStar
| EIndUnit e -> EIndUnit (salt ns e)
| EBool -> EBool
| EFalse -> EFalse
| ETrue -> ETrue
| EIndBool e -> EIndBool (salt ns e)
| EW (a, (p, b)) -> saltTele eW ns p a b
| ESup (a, b) -> ESup (salt ns a, salt ns b)
| EIndW (a, b, c) -> EIndW (salt ns a, salt ns b, salt ns c)
and freshFace ns phi = Env.fold (fun k v -> Env.add (freshVar ns k) v) phi Env.empty
and saltTele ctor ns p a b = let x = fresh p in ctor x (salt ns a) (salt (Env.add p x ns) b)
let freshTele ns : tele -> tele = fun (p, e) -> let q = fresh p in let e' = salt !ns e in ns := Env.add p q !ns; (q, e')
let freshExp = salt Env.empty
let freshDecl : decl -> decl = function | Def (p, exp1, exp2) -> Def (p, (freshExp exp1), freshExp exp2) | Axiom (p, exp) -> Axiom (p, freshExp exp)
let ext x = x ^ ".per"
let empty : state = (Env.empty, Files.empty)
let getTerm e ctx = if !preeval then Value (eval e ctx) else Exp e
let checkDecl ctx d : ctx =
let x = getDeclName d in if Env.mem (ident x) ctx then raise (AlreadyDeclared x);
match d with
| Def (p, EHole, e) -> let t = infer ctx e in Env.add (ident p) (Global, Value t, getTerm e ctx) ctx
| Def (p, a, e) -> ignore (extSet (infer ctx a)); let t = eval a ctx in let v = ident p in check (upGlobal ctx v t (Var (v, t))) e t; Env.add (ident p) (Global, Value t, getTerm e ctx) ctx
| Axiom (p, a) -> ignore (extSet (infer ctx a)); let x = ident p in let t = eval a ctx in Env.add x (Global, Value t, Value (Var (x, t))) ctx
let getBoolVal opt = function
| "tt" | "true" -> true
| "ff" | "false" -> false
| value -> raise (UnknownOptionValue (opt, value))
open Exp
open Printer
let rec orFormula a b = match a, b with
| VDir One, _ | _, VDir One -> VDir One
| VDir Zero, f | f, VDir Zero -> f
| VOr (f, g), h -> orFormula f (orFormula g h)
| f, g -> if f = g then f else VOr (f, g)
let rec andFormula a b = match a, b with
| VDir Zero, _ | _, VDir Zero -> VDir Zero
| VDir One, f | f, VDir One -> f
| VAnd (f, g), h -> andFormula f (andFormula g h)
| f, g -> if f = g then f else VAnd (f, g)
let rec extAnd v = match v with
| Var (x, _) -> Conjunction.singleton (x, One)
| VNeg (Var (x, _)) -> Conjunction.singleton (x, Zero)
| VAnd (x, y) -> Conjunction.union (extAnd x) (extAnd y)
| VDir One -> Conjunction.empty
| _ -> raise (Failure "ExpectedConjunction")
let rec extOr v = match v with
| VOr (x, y) -> Disjunction.union (extOr x) (extOr y)
| VDir Zero -> Disjunction.empty
| k -> Disjunction.singleton (extAnd k)
let uniq t =
let super x y = not (Conjunction.equal x y) && Conjunction.subset y x in
Disjunction.filter (fun x -> not (Disjunction.exists (super x) t)) t
let unions t1 t2 =
Disjunction.fold (fun c1 res ->
Disjunction.fold (fun c2 res' ->
Disjunction.add (Conjunction.union c1 c2) res'
) t2 res
) t1 Disjunction.empty
|> uniq
let negConjunction c =
Conjunction.fold (fun (x, d) res ->
Disjunction.add (Conjunction.singleton (x, negDir d)) res
) c Disjunction.empty
let negDisjunction d =
Disjunction.fold (fun c res ->
unions res (negConjunction c)
) d (Disjunction.singleton Conjunction.empty)
let contrAtom : ident * dir -> value = function
| (x, Zero) -> VNeg (Var (x, VI))
| (x, One) -> Var (x, VI)
let contrAnd (t : conjunction) : value =
Conjunction.fold (fun e e' -> andFormula (contrAtom e) e') t (VDir One)
let contrOr (t : disjunction) : value =
Disjunction.fold (fun e e' -> orFormula (contrAnd e) e') t (VDir Zero)
let rec negFormula = function
| VDir d -> VDir (negDir d)
| VNeg n -> n
| v -> contrOr (negDisjunction (extOr v))
let evalAnd a b = contrOr (unions (extOr a) (extOr b))
let evalOr a b = contrOr (uniq (Disjunction.union (extOr a) (extOr b)))
let getFaceV xs = Env.fold (fun x d y -> andFormula y (contrAtom (x, d))) xs (VDir One)
let getFormulaV ts = System.fold (fun x _ v -> orFormula (getFaceV x) v) ts (VDir Zero)
open Printer
open Exp
exception Restart
exception IncompatibleFaces
exception InferError of exp
exception ExpectedPi of exp
exception ExpectedSig of exp
exception ExpectedPath of exp
exception ExpectedVSet of exp
exception Ineq of exp * exp
exception ExpectedSubtype of exp
exception Parser of int * string * string
exception ExpectedSystem of exp
exception ExpectedNeutral of exp
exception ExpectedFibrant of exp
exception UnknownCommand of string
exception VariableNotFound of ident
exception ExtractionError of string
exception AlreadyDeclared of string
exception UnknownPrimitive of string
exception ExpectedConjunction of exp
exception InvalidModuleName of string * string
exception UnknownOption of string
exception UnknownOptionValue of string * string
let prettyPrintError : exn -> unit = function
| Ineq (e1, e2) -> Printf.printf "Type mismatch:\n %s\nis not equal to\n %s\n" (showExp e1) (showExp e2)
| ExpectedConjunction v -> Printf.printf "“%s” expected to be conjunction\n" (showExp v)
| ExtractionError s -> Printf.printf "Error occured during extraction: %s\n" s
| ExpectedPath e -> Printf.printf "“%s” expected to be a path.\n" (showExp e)
| AlreadyDeclared p -> Printf.printf "“%s” is already declared.\n" p
| InferError e -> Printf.printf "Cannot infer type of\n %s\n" (showExp e)
| VariableNotFound p -> Printf.printf "Variable %s was not found\n" (showIdent p)
| InvalidModuleName (name, filename) -> Printf.printf "Module “%s” does not match name of its file: %s\n" name filename
| ExpectedVSet x -> Printf.printf " %s\nexpected to be universe\n" (showExp x)
| ExpectedFibrant x -> Printf.printf " %s\nexpected to be fibrant universe\n" (showExp x)
| ExpectedPi x -> Printf.printf " %s\nexpected to be Pi-type\n" (showExp x)
| ExpectedSig x -> Printf.printf " %s\nexpected to be Sigma-type\n" (showExp x)
| ExpectedSystem x -> Printf.printf " %s\nexpected to be a system\n" (showExp x)
| ExpectedSubtype x -> Printf.printf " %s\nexpected to be a cubical subtype\n" (showExp x)
| UnknownCommand s -> Printf.printf "Unknown command “%s”\n" s
| UnknownOption opt -> Printf.printf "Unknown option “%s”\n" opt
| UnknownOptionValue (opt, value) -> Printf.printf "Unknown value “%s” of option “%s”\n" value opt
| Parser (x, buf, filename) -> Printf.printf "Parsing error at line %d while parsing “%s”: “%s”\n" x filename buf
| IncompatibleFaces -> Printf.printf "Incompatible faces\n"
| Sys_error s -> print_endline s
| Restart -> raise Restart
| ex -> Printf.printf "Uncaught exception: %s\n" (Printexc.to_string ex)
let handleErrors (f : 'a -> 'b) (x : 'a) (default : 'b) : 'b = try f x with ex -> prettyPrintError ex; defaultlet (<<) f g x = f (g x)
let (>>) g f x = f (g x)
let initLast xs =
let rec func xs = function
| [] -> failwith "initLast: expected non-empty list"
| [y] -> (xs, y)
| y :: ys -> func (y :: xs) ys in
let (ys, y) = func [] xs in (List.rev ys, y)
let getDigit x = Char.chr (Z.to_int x + 0x80) |> Printf.sprintf "\xE2\x82%c"
let ten = Z.of_int 10
let rec showSubscript x =
if Z.lt x Z.zero then failwith "showSubscript: expected positive integer"
else if Z.equal x Z.zero then "" else let (y, d) = Z.div_rem x ten in
showSubscript y ^ getDigit d
let moduleSep = '/'
let getPath = String.split_on_char moduleSep >> String.concat Filename.dir_sep
let trace : bool ref = ref false
let indices : bool ref = ref false
let preeval : bool ref = ref true
let girard : bool ref = ref false
let verbose : bool ref = ref true
let irrelevance : bool ref = ref false
let traceHole _ _ = ()
type ident = Irrefutable | Ident of string * int64
module Ident =
struct
type t = ident
let compare x y =
match (x, y) with
| Irrefutable, Irrefutable -> 0
| Irrefutable, Ident _ -> -1
| Ident _, Irrefutable -> 1
| Ident (p, a), Ident (q, b) ->
if p = q then compare a b
else compare p q
end
module Env = Map.Make(Ident)
type dir = Zero | One
module Dir =
struct
type t = dir
let compare a b =
match a, b with
| One, Zero -> 1
| Zero, One -> -1
| _, _ -> 0
end
module Files = Set.Make(String)
let gidx : int64 ref = ref 0L
let gen () = gidx := Int64.succ !gidx; !gidx
let fresh : ident -> ident = function | Irrefutable -> let n = gen () in Ident ("x" ^ showSubscript (Z.of_int64 n), n) | Ident (p, _) -> Ident (p, gen ())
let freshName x = let n = gen () in Ident (x ^ showSubscript (Z.of_int64 n), n)
let matchIdent p : ident -> bool = function | Irrefutable -> false | Ident (q, _) -> p = q
let getDigit x = Char.chr (x + 0x80) |> Printf.sprintf "\xE2\x82%c"
module Atom =
struct
type t = ident * dir
let compare (a, x) (b, y) = if a = b then Dir.compare x y else Ident.compare a b
end
module Conjunction = Set.Make(Atom)
type conjunction = Conjunction.t
module Disjunction = Set.Make(Conjunction)
type disjunction = Disjunction.t
type face = dir Env.t
module Face =
struct
type t = face
let compare = Env.compare Dir.compare
end
type tag = (string option) ref
module System = Map.Make(Face)
let eps : face = Env.empty
let negDir : dir -> dir = function | Zero -> One | One -> Zero
let keys ts = List.of_seq (Seq.map fst (System.to_seq ts))
let intersectionWith f = System.merge (fun _ x y -> match x, y with | Some a, Some b -> Some (f a b) | _, _ -> None)
type exp =
| EPre of Z.t | EKan of Z.t (* cosmos *)
| EVar of ident | EHole (* variables *)
| EPi of exp * (ident * exp) | ELam of exp * (ident * exp) | EApp of exp * exp (* pi *)
| ESig of exp * (ident * exp) | EPair of tag * exp * exp (* sigma *)
| EFst of exp | ESnd of exp | EField of exp * string (* sigma *)
| EId of exp | ERef of exp | EJ of exp (* strict equality *)
| EPathP of exp | EPLam of exp | EAppFormula of exp * exp (* path equality *)
| EI | EDir of dir | EAnd of exp * exp | EOr of exp * exp | ENeg of exp (* CCHM interval *)
| ETransp of exp * exp | EHComp of exp * exp * exp * exp (* Kan operations *)
| EPartial of exp | EPartialP of exp * exp | ESystem of exp System.t (* partial functions *)
| ESub of exp * exp * exp | EInc of exp * exp | EOuc of exp (* cubical subtypes *)
| EEmpty | EIndEmpty of exp (* 𝟎 *)
| EUnit | EStar | EIndUnit of exp (* 𝟏 *)
| EBool | EFalse | ETrue | EIndBool of exp (* 𝟐 *)
| EW of exp * (ident * exp) | ESup of exp * exp | EIndW of exp * exp * exp (* W *)
type tele = ident * exp
type scope = Local | Global
type value =
| VKan of Z.t | VPre of Z.t
| Var of ident * value | VHole
| VPi of value * clos | VLam of value * clos | VApp of value * value
| VSig of value * clos | VPair of tag * value * value | VFst of value | VSnd of value
| VId of value | VRef of value | VJ of value
| VPathP of value | VPLam of value | VAppFormula of value * value
| VI | VDir of dir | VAnd of value * value | VOr of value * value | VNeg of value
| VTransp of value * value | VHComp of value * value * value * value
| VPartialP of value * value | VSystem of value System.t
| VSub of value * value * value | VInc of value * value | VOuc of value
| VEmpty | VIndEmpty of value
| VUnit | VStar | VIndUnit of value
| VBool | VFalse | VTrue | VIndBool of value
| VW of value * clos | VSup of value * value | VIndW of value * value * value
and clos = ident * (value -> value)
and term = Exp of exp | Value of value
and record = scope * term * term
and ctx = record Env.t
type state = ctx * Files.t
type command =
| Nope
| Eval of exp
| Action of string
| Command of string * exp
type decl =
| Def of string * exp * exp
| Axiom of string * exp
type line =
| Import of string list
| Option of string * string
| Decl of decl
type content = line list
type file = string * content
let eLam p a b = ELam (a, (p, b))
let ePi p a b = EPi (a, (p, b))
let eSig p a b = ESig (a, (p, b))
let eW p a b = EW (a, (p, b))
let ezero = EDir Zero
let eone = EDir One
let vzero = VDir Zero
let vone = VDir One
let isOne i = VApp (VApp (VId VI, VDir One), i)
let extFace x e = e (List.map (fun (p, v) -> Var (p, isOne v)) x)
let ident x = Ident (x, 0L)
let decl x = EVar (ident x)
let upVar p x ctx = match p with Irrefutable -> ctx | _ -> Env.add p x ctx
let upLocal ctx p t v = upVar p (Local, Value t, Value v) ctx
let upGlobal ctx p t v = upVar p (Global, Value t, Value v) ctx
let isGlobal : record -> bool = function Global, _, _ -> false | Local, _, _ -> true
let freshVar ns n = match Env.find_opt n ns with Some x -> x | None -> n
let mapFace fn phi = Env.fold (fun p d -> Env.add (fn p) d) phi Env.empty
let freshFace ns = mapFace (freshVar ns)
let rec rbV v = match v with
| VLam (t, g) -> rbVTele eLam t g
| VPair (r, u, v) -> EPair (r, rbV u, rbV v)
| VKan u -> EKan u
| VPi (t, g) -> rbVTele ePi t g
| VSig (t, g) -> rbVTele eSig t g
| VPre u -> EPre u
| VPLam f -> EPLam (rbV f)
| Var (x, _) -> EVar x
| VApp (f, x) -> EApp (rbV f, rbV x)
| VFst k -> EFst (rbV k)
| VSnd k -> ESnd (rbV k)
| VHole -> EHole
| VPathP v -> EPathP (rbV v)
| VPartialP (t, r) -> EPartialP (rbV t, rbV r)
| VSystem ts -> ESystem (System.map rbV ts)
| VSub (a, i, u) -> ESub (rbV a, rbV i, rbV u)
| VTransp (p, i) -> ETransp (rbV p, rbV i)
| VHComp (t, r, u, u0) -> EHComp (rbV t, rbV r, rbV u, rbV u0)
| VAppFormula (f, x) -> EAppFormula (rbV f, rbV x)
| VId v -> EId (rbV v)
| VRef v -> ERef (rbV v)
| VJ v -> EJ (rbV v)
| VI -> EI
| VDir d -> EDir d
| VAnd (u, v) -> EAnd (rbV u, rbV v)
| VOr (u, v) -> EOr (rbV u, rbV v)
| VNeg u -> ENeg (rbV u)
| VInc (t, r) -> EInc (rbV t, rbV r)
| VOuc v -> EOuc (rbV v)
| VEmpty -> EEmpty
| VIndEmpty v -> EIndEmpty (rbV v)
| VUnit -> EUnit
| VStar -> EStar
| VIndUnit v -> EIndUnit (rbV v)
| VBool -> EBool
| VFalse -> EFalse
| VTrue -> ETrue
| VIndBool v -> EIndBool (rbV v)
| VW (t, g) -> rbVTele eW t g
| VSup (a, b) -> ESup (rbV a, rbV b)
| VIndW (a, b, c) -> EIndW (rbV a, rbV b, rbV c)
and rbVTele ctor t (p, g) = let x = Var (p, t) in ctor p (rbV t) (rbV (g x))
let zeroPrim = ref "0"
let onePrim = ref "1"
let intervalPrim = ref "I"
let getVar x =
let xs = [
(!intervalPrim, EI);
(!zeroPrim, EDir Zero);
(!onePrim, EDir One);
("𝟎", EEmpty); ("empty", EEmpty);
("𝟏", EUnit); ("unit", EUnit); ("★", EStar); ("star", EStar);
("𝟐", EBool); ("bool", EBool); ("false", EFalse); ("0₂", EFalse); ("true", ETrue); ("1₂", ETrue)
] in match List.assoc_opt x xs with Some e -> e | None -> decl x
type formula = | Falsehood | Equation of ident * dir | Truth
exception ExpectedDir of string
let getDir x = if x = !zeroPrim then Zero else if x = !onePrim then One else raise (ExpectedDir x)
let face p e d : formula = match getVar p, e, getDir d with | EVar x, "=", d -> Equation (x, d) | EDir d1, "=", d2 -> if d1 = d2 then Truth else Falsehood | _, _, _ -> failwith "invalid face"
let extEquation : formula -> ident * dir = function | Equation (x, d) -> (x, d) | _ -> raise (Failure "extEquation")
let parseFace xs = if List.mem Falsehood xs then None else if List.mem Truth xs then Some eps else Some (Env.of_seq (Seq.map extEquation (List.to_seq xs)))
let parsePartial (xs, e) = Option.map (fun ys -> (ys, e)) (parseFace xs)
let impl a b = EPi (a, (Irrefutable, b))
let prod a b = ESig (a, (Irrefutable, b))
let rec telescope ctor e : tele list -> exp = function | [] -> e | (p, a) :: xs -> ctor p a (telescope ctor e xs)
let rec pLam e : ident list -> exp = function [] -> e | x :: xs -> EPLam (ELam (EI, (x, pLam e xs)))
let getDeclName : decl -> string = function Def (p, _, _) | Axiom (p, _) -> p
open Printer
open Error
open Check
open Exp
let help =
"Available commands:
<statement> infer type and normalize statement
:q quit
:r restart
:h display this message"
let init : state = empty
let st : state ref = ref init
let checkAndEval ctx e : value * value = (Check.infer ctx e, Check.eval e ctx)
let main ctx : command -> unit = function
| Eval e -> let (t, v) = checkAndEval ctx (freshExp e) in
Printf.printf "TYPE: %s\nEVAL: %s\n" (showExp (rbV t)) (showExp (rbV v))
| Action "q" -> exit 0
| Action "r" -> st := init; raise Restart
| Action "h" -> print_endline help
| Command (s, _) | Action s -> raise (UnknownCommand s)
| Nope -> ()
let check filename = st := handleErrors (Reader.checkFile !st) filename !st
let banner = "Per theorem prover [MLTT-80] version 5.3.20"
let loop () =
print_endline ("\n" ^ banner) ;
let (ctx, _) = !st in
try while true do
print_string "> ";
let line = read_line () in
handleErrors (fun x ->
let cmd = Reader.parseErr Parser.repl (Lexing.from_string x) "<stdin>" in
main ctx cmd) line ()
done with End_of_file -> ()
type cmdline =
| Check of string
| Lex of string
| Parse of string
| Prim of string * string
| Repl | Help | Trace
| Indices | Girard | Silent | Irrelevance
let help =
"\n invocation = per | per list
list = [] | command list
primitive = zero | one | interval
command = check <filename> | lex <filename>
| parse <filename> | girard
| trace | repl
| help "
let repl = ref false
let cmd : cmdline -> unit = function
| Check filename -> check filename
| Lex filename -> Reader.lex filename
| Parse filename -> Reader.parse filename
| Prim (prim, value) -> begin match prim with
| "zero" -> zeroPrim := value
| "one" -> onePrim := value
| "interval" -> intervalPrim := value
| _ -> raise (UnknownPrimitive prim)
end
| Help -> print_endline banner ; print_endline help
| Repl -> repl := true
| Silent -> verbose := false
| Indices -> indices := true
| Trace -> indices := true; trace := true
| Girard -> girard := true
| Irrelevance -> irrelevance := true
let rec parseArgs : string list -> cmdline list = function
| [] -> []
| "prim" :: prim :: value :: rest -> Prim (prim, value) :: parseArgs rest
| "check" :: filename :: rest -> Check filename :: parseArgs rest
| "lex" :: filename :: rest -> Lex filename :: parseArgs rest
| "parse" :: filename :: rest -> Parse filename :: parseArgs rest
| "help" :: rest -> Help :: parseArgs rest
| "trace" :: rest -> Trace :: parseArgs rest
| "indices" :: rest -> Indices :: parseArgs rest
| "irrelevance" :: rest -> Irrelevance :: parseArgs rest
| "silent" :: rest -> Silent :: parseArgs rest
| "girard" :: rest -> Girard :: parseArgs rest
| "repl" :: rest -> Repl :: parseArgs rest
| x :: xs -> Printf.printf "Unknown command “%s”\n" x; parseArgs xs
let defaults = function | [] -> [Help] | xs -> xs
let rec main () =
try Array.to_list Sys.argv |> List.tl |> parseArgs |> defaults |> List.iter cmd;
if !repl then loop () else () with Restart -> main ()
let () = main ()
open Exp
let showIdent : ident -> string = function
| Irrefutable -> "_"
| Ident (p, n) -> if !indices then p ^ "#" ^ Int64.to_string n else p
let showDir : dir -> string = function | Zero -> !zeroPrim | One -> !onePrim
let showFace phi =
if Env.is_empty phi then "(1 = 1)"
else Env.bindings phi
|> List.map (fun (x, d) -> Printf.sprintf "(%s = %s)" (showIdent x) (showDir d))
|> String.concat " "
let showSystem show xs =
System.bindings xs
|> List.map (fun (x, e) -> Printf.sprintf "%s → %s" (showFace x) (show e))
|> String.concat ", "
let rec ppExp paren e =
let x = match e with
| EKan n -> "U" ^ showSubscript n
| EPre n -> "V" ^ showSubscript n
| EVar p -> showIdent p
| EHole -> "?"
| EPi (a, (p, b)) -> showPiExp a p b
| ELam (a, (p, b)) -> Printf.sprintf "λ %s, %s" (showTeleExp (p, a)) (showExp b)
| EApp (f, x) -> Printf.sprintf "%s %s" (showExp f) (ppExp true x)
| ESig (a, (p, b)) -> Printf.sprintf "Σ %s, %s" (showTeleExp (p, a)) (showExp b)
| EPair (_, fst, snd) -> Printf.sprintf "(%s, %s)" (showExp fst) (showExp snd)
| EFst exp -> ppExp true exp ^ ".1"
| ESnd exp -> ppExp true exp ^ ".2"
| EField (exp, field) -> ppExp true exp ^ "." ^ field
| EPLam (ELam (_, (i, e))) -> Printf.sprintf "<%s> %s" (showIdent i) (showExp e)
| EPLam _ -> failwith "showExp: unreachable code was reached"
| EAppFormula (f, x) -> Printf.sprintf "%s @ %s" (ppExp true f) (ppExp true x)
| ESystem x -> Printf.sprintf "[%s]" (showSystem showExp x)
| ESub (a, i, u) -> Printf.sprintf "%s[%s ↦ %s]" (ppExp true a) (showExp i) (showExp u)
| EI -> !intervalPrim | EDir d -> showDir d
| EAnd (a, b) -> Printf.sprintf "%s ∧ %s" (ppExp true a) (ppExp true b)
| EOr (a, b) -> Printf.sprintf "%s ∨ %s" (ppExp true a) (ppExp true b)
| ENeg a -> Printf.sprintf "-%s" (ppExp paren a)
| ETransp (p, i) -> Printf.sprintf "transp %s %s" (ppExp true p) (ppExp true i)
| EPathP e -> "PathP " ^ ppExp true e
| EId e -> Printf.sprintf "Id %s" (ppExp true e)
| ERef e -> Printf.sprintf "ref %s" (ppExp true e)
| EJ e -> Printf.sprintf "idJ %s" (ppExp true e)
| EEmpty -> "𝟎" | EUnit -> "𝟏" | EBool -> "𝟐"
| EStar -> "★" | EFalse -> "0₂" | ETrue -> "1₂"
| EIndEmpty e -> Printf.sprintf "ind₀ %s" (ppExp true e)
| EIndUnit e -> Printf.sprintf "ind₁ %s" (ppExp true e)
| EIndBool e -> Printf.sprintf "ind₂ %s" (ppExp true e)
| ESup (a, b) -> Printf.sprintf "sup %s %s" (ppExp true a) (ppExp true b)
| EIndW (a, b, c) -> Printf.sprintf "indᵂ %s %s %s" (ppExp true a) (ppExp true b) (ppExp true c)
| EHComp (t, r, u, u0) -> Printf.sprintf "hcomp %s %s %s %s" (ppExp true t) (ppExp true r) (ppExp true u) (ppExp true u0)
| EPartial e -> Printf.sprintf "Partial %s" (ppExp true e)
| EPartialP (t, r) -> Printf.sprintf "PartialP %s %s" (ppExp true t) (ppExp true r)
| EInc (t, r) -> Printf.sprintf "inc %s %s" (ppExp true t) (ppExp true r)
| EOuc e -> Printf.sprintf "ouc %s" (ppExp true e)
| EW (a, (p, b)) -> Printf.sprintf "W %s, %s" (showTeleExp (p, a)) (showExp b)
in match e with | EVar _ | EFst _ | ESnd _ | EI | EPre _ | ESystem _ | EKan _
| EHole | EDir _ | EPair _ | ENeg _ | EW _ -> x | _ -> if paren then "(" ^ x ^ ")" else x
and showExp e = ppExp false e
and showTeleExp a = match a with | (p, x) -> Printf.sprintf "(%s : %s)" (showIdent p) (showExp x)
and showPiExp a p b = match p with
| Irrefutable -> Printf.sprintf "%s → %s" (ppExp true a) (showExp b)
| _ -> Printf.sprintf "Π %s, %s" (showTeleExp (p, a)) (showExp b)
type entry = {
mutable total_time : float;
mutable call_count : int;
}
let stats : (string, entry) Hashtbl.t = Hashtbl.create 50
let active_start : (string, float) Hashtbl.t = Hashtbl.create 50
let stack = ref []
let profiling_enabled = ref false
let start_prof () = profiling_enabled := true
let stop_prof () = profiling_enabled := false
let get_time () = Sys.time ()
let measure name f =
if not !profiling_enabled then f ()
else begin
let t0 = get_time () in
let parent = match !stack with p::_ -> Some p | [] -> None in
stack := name :: !stack;
let result = try f () with e ->
stack := List.tl !stack;
raise e
in
let t1 = get_time () in
let diff = t1 -. t0 in
stack := List.tl !stack;
let entry = try Hashtbl.find stats name with Not_found ->
let e = { total_time = 0.0; call_count = 0 } in
Hashtbl.add stats name e;
e
in
entry.total_time <- entry.total_time +. diff;
entry.call_count <- entry.call_count + 1;
result
end
let print_prof () =
let sorted = Hashtbl.fold (fun k v acc -> (k, v) :: acc) stats []
|> List.sort (fun (_, a) (_, b) -> compare b.total_time a.total_time)
in
let max_time = match sorted with (_, e)::_ -> e.total_time | [] -> 1.0 in
Printf.printf "\nOCaml Profile Results:\n";
List.iter (fun (name, entry) ->
let bar_len = int_of_float (entry.total_time /. max_time *. 40.0) in
let bar = String.make bar_len '=' ^ String.make (40 - bar_len) ' ' in
Printf.printf "%-50s [%s] %.6fs (x%d)\n" name bar entry.total_time entry.call_count
) sorted;
Printf.printf "\n"
open Printer
open Lexing
open Exp
open Error
open Check
let parseErr f lexbuf filename =
try f Lexer.main lexbuf
with Parser.Error ->
raise (Error.Parser (lexbuf.lex_curr_p.pos_lnum, lexeme lexbuf, filename))
let lex filename =
let chan = open_in filename in
let lexbuf = Lexing.from_channel chan in
Printf.printf "Lexing “%s”.\n" filename;
try while true do
let tok = Lexer.main lexbuf in
if tok = Parser.EOF then raise End_of_file
else print_string (Lexer.tokenToString tok ^ " ")
done with End_of_file -> close_in chan;
print_newline ()
let showDecl : decl -> string = function
| Def (p, exp1, exp2) -> Printf.sprintf "def %s : %s := %s" p (showExp exp1) (showExp exp2)
| Axiom (p, exp) -> Printf.sprintf "axiom %s : %s" p (showExp exp)
let showLine : line -> string = function
| Import p -> Printf.sprintf "import %s" (String.concat " " p)
| Option (opt, value) -> Printf.sprintf "option %s %s" opt value
| Decl d -> showDecl d
let showContent x = String.concat "\n" (List.map showLine x)
let showFile : file -> string = function | (p, x) -> Printf.sprintf "module %s where\n%s" p (showContent x)
let rec checkLine st : line -> state =
let (ctx, checked) = st in function
| Decl d -> if !verbose then begin Printf.printf "Checking: %s\n" (getDeclName d); flush_all () end; (checkDecl ctx (freshDecl d), checked)
| Option (opt, value) ->
begin match opt with
| "irrelevance" -> irrelevance := getBoolVal opt value
| "girard" -> girard := getBoolVal opt value
| "verbose" -> verbose := getBoolVal opt value
| "pre-eval" -> preeval := getBoolVal opt value
| _ -> raise (UnknownOption opt)
end; st
| Import xs -> List.fold_left (fun st x -> let path = ext x in
if Files.mem path checked then st else checkFile st path) st xs
and checkFile p path =
let (ctx, checked) = p in
let filename = Filename.basename path in
let chan = open_in path in
let (name, con) = parseErr Parser.file (Lexing.from_channel chan) path in close_in chan; if !verbose then begin Printf.printf "Parsed “%s” successfully.\n" filename; flush_all () end;
if ext name = filename then () else raise (InvalidModuleName (name, filename));
let res = checkContent (ctx, Files.add path checked) con in print_endline ("File “" ^ filename ^ "” checked."); res
and checkContent st xs = List.fold_left checkLine st xs
let parse filename =
let chan = open_in filename in
Printf.printf "Parsing “%s”.\n" filename;
Error.handleErrors
(fun chan ->
let lexbuf = Lexing.from_channel chan in
let file = parseErr Parser.file lexbuf filename in
print_endline (showFile file))
chan ()