Refactor/more kernel perf

lib/kernel.ml

@@ -94,7 +94,7 @@ and Ctx : sig
   val forget : t -> Unchecked_types(Coh).ctx
   val check : Unchecked_types(Coh).ctx -> t
   val check_notin : t -> Var.t -> unit
-  val check_equal : t -> t -> unit
+  val _check_equal : t -> t -> unit
 end = struct
   type t = { c : (Var.t * Ty.t) list; unchecked : Unchecked_types(Coh).ctx }
 
@@ -119,7 +119,7 @@ end = struct
   let forget c = c.unchecked
   let to_string ctx = Unchecked.ctx_to_string (forget ctx)
 
-  let check_equal ctx1 ctx2 =
+  let _check_equal ctx1 ctx2 =
     if ctx1 == ctx2 then ()
     else Unchecked.check_equal_ctx (forget ctx1) (forget ctx2)
 
@@ -308,7 +308,7 @@ and Ty : sig
 
   val to_string : t -> string
   val free_vars : t -> Var.t list
-  val is_full : t -> bool
+  val is_full : Ctx.t -> t -> bool
   val is_obj : t -> bool
   val check_equal : t -> t -> unit
   val morphism : Tm.t -> Tm.t -> Ty.t
@@ -318,13 +318,12 @@ and Ty : sig
   val retrieve_arrow : t -> t * Tm.t * Tm.t
   val under_type : t -> t
   val target : t -> Tm.t
-  val ctx : t -> Ctx.t
   val dim : t -> int
 end = struct
   (** A type exepression. *)
   type expr = Obj | Arr of t * Tm.t * Tm.t
 
-  and t = { c : Ctx.t; e : expr; unchecked : Unchecked_types(Coh).ty }
+  and t = { e : expr; unchecked : Unchecked_types(Coh).ty }
 
   open Unchecked (Coh)
   module Unchecked = Make (Coh)
@@ -357,7 +356,7 @@ end = struct
               Arr (a, u, v)
           | Meta_ty _ -> raise MetaVariable
         in
-        let ty = { c; e; unchecked = t } in
+        let ty = { e; unchecked = t } in
         Hashtbl.add tbl (c, t) ty;
         ty
 
@@ -368,30 +367,25 @@ end = struct
     | Arr (t, u, v) ->
         List.unions [ free_vars t; Tm.free_vars u; Tm.free_vars v ]
 
-  let is_full t = List.included (Ctx.domain t.c) (free_vars t)
+  let is_full c t = List.included (Ctx.domain c) (free_vars t)
   let forget t = t.unchecked
   let to_string ty = Unchecked.ty_to_string (forget ty)
 
   (** Test for equality. *)
-  let check_equal ty1 ty2 =
-    Ctx.check_equal ty1.c ty2.c;
-    Unchecked.check_equal_ty (forget ty1) (forget ty2)
+  let check_equal ty1 ty2 = Unchecked.check_equal_ty (forget ty1) (forget ty2)
 
   let morphism t1 t2 =
     let a1 = Tm.ty t1 in
     let a2 = Tm.ty t2 in
     check_equal a1 a2;
     {
-      c = a1.c;
       e = Arr (a1, t1, t2);
       unchecked = Arr (forget a1, Tm.forget t1, Tm.forget t2);
     }
 
   let apply_sub t s =
-    Ctx.check_equal t.c (Sub.tgt s);
     check (Sub.src s) (Unchecked.ty_apply_sub (forget t) (Sub.forget s))
 
-  let ctx t = t.c
   let rec dim t = match t.e with Obj -> 0 | Arr (a, _, _) -> 1 + dim a
 end
 
@@ -402,7 +396,7 @@ and Tm : sig
   val to_var : t -> Var.t
   val typ : t -> Ty.t
   val free_vars : t -> Var.t list
-  val is_full : t -> bool
+  val is_full : Ctx.t -> t -> bool
   val forget : t -> Unchecked_types(Coh).tm
   val check : Ctx.t -> ?ty:Ty.t -> Unchecked_types(Coh).tm -> t
   val apply_sub : t -> Sub.t -> t
@@ -425,7 +419,7 @@ end = struct
     let fvty = Ty.free_vars tm.ty in
     match tm.e with Var x -> x :: fvty | Coh (_, sub) -> Sub.free_vars sub
 
-  let is_full tm = List.included (Ctx.domain (Ty.ctx tm.ty)) (free_vars tm)
+  let is_full c tm = List.included (Ctx.domain c) (free_vars tm)
   let forget tm = tm.unchecked
 
   let check c ?ty t =
@@ -439,7 +433,7 @@ end = struct
       | None -> (
           match t with
           | Var x ->
-              let e, ty = (Var x, Ty.check c (Ty.forget (Ctx.ty_var c x))) in
+              let e, ty = (Var x, Ctx.ty_var c x) in
               { ty; e; unchecked = t }
           | Meta_tm _ -> raise MetaVariable
           | Coh (coh, s) ->
@@ -456,14 +450,12 @@ end = struct
         tm
 
   let apply_sub t sub =
-    Ctx.check_equal (Sub.tgt sub) (Ty.ctx t.ty);
     let c = Sub.src sub in
     let ty = Ty.apply_sub t.ty sub in
     let t = Unchecked.tm_apply_sub (forget t) (Sub.forget sub) in
     check c ~ty t
 
   let preimage t sub =
-    Ctx.check_equal (Sub.src sub) (Ty.ctx t.ty);
     let c = Sub.tgt sub in
     let t = Unchecked.tm_sub_preimage (forget t) (Sub.forget sub) in
     check c t
@@ -525,21 +517,21 @@ end = struct
   let is_inv = function Inv (_, _) -> true | NonInv (_, _) -> false
 
   let algebraic ps ty name =
-    if Ty.is_full ty then (
-      Ctx.check_equal (PS.to_ctx ps) (Ty.ctx ty);
-      Inv ({ ps; ty }, name))
+    let ctx = PS.to_ctx ps in
+    if Ty.is_full ctx ty then Inv ({ ps; ty }, name)
     else
       let _, src, tgt =
         try Ty.retrieve_arrow ty with IsObj -> raise NotAlgebraic
       in
       try
         let src_inclusion = PS.source ps in
         let src = Tm.preimage src src_inclusion in
-        if not (Tm.is_full src) then raise NotAlgebraic
+        if not (Tm.is_full (Sub.tgt src_inclusion) src) then raise NotAlgebraic
         else
           let tgt_inclusion = PS.target ps in
           let tgt = Tm.preimage tgt tgt_inclusion in
-          if not (Tm.is_full tgt) then raise NotAlgebraic
+          if not (Tm.is_full (Sub.tgt tgt_inclusion) tgt) then
+            raise NotAlgebraic
           else NonInv ({ ps; src; tgt; total_ty = ty }, name)
       with NotInImage -> raise NotAlgebraic
 
@@ -579,10 +571,10 @@ end = struct
         let bdry = PS.bdry ps in
         let cbdry = PS.to_ctx bdry in
         let src = Tm.check cbdry src_unchkd in
-        if not (Tm.is_full src) then raise NotAlgebraic
+        if not (Tm.is_full cbdry src) then raise NotAlgebraic
         else
           let tgt = Tm.check cbdry tgt_unchkd in
-          if not (Tm.is_full tgt) then raise NotAlgebraic
+          if not (Tm.is_full cbdry tgt) then raise NotAlgebraic
           else
             let total_ty =
               Ty.morphism
@@ -602,7 +594,7 @@ end = struct
         let src = Tm.check ctx src_unchkd in
         let tgt = Tm.check ctx tgt_unchkd in
         let ty = Ty.morphism src tgt in
-        if Ty.is_full ty then (
+        if Ty.is_full ctx ty then (
           let coh = Inv ({ ps; ty }, name) in
           Hashtbl.add tbl_inv (ps_unchkd, src_unchkd, tgt_unchkd) coh;
           coh)