create and use Coh.apply in the kernel

Author: thibautbenjamin

lib/functorialisation.ml

@@ -52,15 +52,6 @@ let rec next_round l =
       (v :: vars, (Var.Bridge v, n - 1) :: left)
   | _ -> Error.fatal "cannot functorialise a negative number of times."
 
-let pp_data_rename pp names =
-  let name, susp, func = pp in
-  let rec rename f =
-    match f with
-    | [] -> []
-    | (x, i) :: f -> (Display_maps.var_apply_sub x names, i) :: rename f
-  in
-  (name, susp, List.map rename func)
-
 (* Functorialised coherences with respect to locally maximal variables are
    coherences. This function updates the list of variables in the resulting
    coherence that come from a functorialisation *)
@@ -204,15 +195,12 @@ and ctx c l =
 (* Functorialisation of a coherence once with respect to a list of
    variables *)
 and coh_depth0 coh l =
-  let ps, t, pp = Coh.forget coh in
-  let ctxf = ctx (Unchecked.ps_to_ctx ps) l in
-  let names = Unchecked.db_level_sub_inv ctxf in
-  let psf = PS.forget (PS.mk (Ctx.check ctxf)) in
-  let ty = ty t l (Coh (coh, Unchecked.identity_ps ps)) in
-  let ty = Unchecked.ty_apply_sub ty names in
-  let pp = pp_data l pp in
-  let pp = pp_data_rename pp names in
-  (check_coh psf ty pp, names)
+  let ps, _, _ = Coh.forget coh in
+  Coh.apply
+    (fun c -> ctx c l)
+    (fun t -> ty t l (Coh (coh, Unchecked.identity_ps ps)))
+    (fun pp -> pp_data l pp)
+    coh
 
 and coh coh l =
   let ps, ty, _ = Coh.forget coh in

lib/inverse.ml

@@ -11,9 +11,11 @@ let ty t =
 
 let coh c =
   if not (Coh.is_inv c) then raise CohNonInv;
-  let ps, t, (name, susp, func) = Coh.forget c in
-  let ty_inv = ty t in
-  check_coh ps ty_inv (name ^ "^-1", susp, func)
+  Coh.apply_ps
+    (fun ps -> ps)
+    (fun t -> ty t)
+    (fun (name, susp, func) -> (name ^ "^-1", susp, func))
+    c
 
 let rec compute_inverse t =
   match t with

lib/kernel.ml

@@ -564,13 +564,7 @@ end = struct
     let db_sub = Unchecked.db_level_sub_inv c in
     let c, _, _ = Unchecked.db_levels c in
     let c = Ctx.check c in
-    let name, susp, func = fun_pp_data pp_data in
-    let rec rename f =
-      match f with
-      | [] -> []
-      | (x, i) :: f -> (Display_maps.var_apply_sub x db_sub, i) :: rename f
-    in
-    let pp_data = (name, susp, List.map rename func) in
+    let pp_data = Display_maps.pp_data_rename (fun_pp_data pp_data) db_sub in
     let tm = Unchecked.tm_apply_sub (fun_tm (UnnamedTm.forget tm)) db_sub in
     (check c pp_data tm, db_sub)
 end
@@ -612,6 +606,20 @@ and Coh : sig
   val func_data : t -> (Var.t * int) list list
   val check_equal : t -> t -> unit
   val dim : t -> int
+
+  val apply_ps :
+    (ps -> ps) ->
+    (Unchecked_types(Coh)(Tm).ty -> Unchecked_types(Coh)(Tm).ty) ->
+    (pp_data -> pp_data) ->
+    t ->
+    t
+
+  val apply :
+    (Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
+    (Unchecked_types(Coh)(Tm).ty -> Unchecked_types(Coh)(Tm).ty) ->
+    (pp_data -> pp_data) ->
+    t ->
+    t * Unchecked_types(Coh)(Tm).sub
 end = struct
   type cohInv = { ps : PS.t; ty : Ty.t }
 
@@ -638,6 +646,7 @@ end = struct
 
   open Unchecked (Coh) (Tm)
   module Unchecked = Make (Coh) (Tm)
+  module Display_maps = Unchecked.Display_maps
 
   let ps = function Inv (data, _) -> data.ps | NonInv (data, _) -> data.ps
 
@@ -774,6 +783,22 @@ end = struct
           Ty.check_equal d1.total_ty d2.total_ty
       | Inv _, NonInv _ | NonInv _, Inv _ ->
           raise (NotEqual (to_string coh1, to_string coh2))
+
+  let apply_ps fun_ps fun_ty fun_pp_data coh =
+    let ps, ty, pp = forget coh in
+    let ps = fun_ps ps in
+    let pp_data = fun_pp_data pp in
+    let ty = fun_ty ty in
+    check ps ty pp_data
+
+  let apply fun_ctx fun_ty fun_pp_data coh =
+    let ps, ty, pp = forget coh in
+    let ctx = fun_ctx (Unchecked.ps_to_ctx ps) in
+    let ps = PS.forget (PS.mk (Ctx.check ctx)) in
+    let db_sub = Unchecked.db_level_sub_inv ctx in
+    let pp_data = Display_maps.pp_data_rename (fun_pp_data pp) db_sub in
+    let ty = Unchecked.ty_apply_sub (fun_ty ty) db_sub in
+    (check ps ty pp_data, db_sub)
 end
 
 module U = Unchecked (Coh) (Tm)

lib/kernel.mli

@@ -33,6 +33,20 @@ module rec Coh : sig
     * Unchecked_types(Coh)(Tm).ty
 
   val func_data : t -> (Var.t * int) list list
+
+  val apply_ps :
+    (ps -> ps) ->
+    (Unchecked_types(Coh)(Tm).ty -> Unchecked_types(Coh)(Tm).ty) ->
+    (pp_data -> pp_data) ->
+    t ->
+    t
+
+  val apply :
+    (Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
+    (Unchecked_types(Coh)(Tm).ty -> Unchecked_types(Coh)(Tm).ty) ->
+    (pp_data -> pp_data) ->
+    t ->
+    t * Unchecked_types(Coh)(Tm).sub
 end
 
 and Ty : sig

lib/opposite.ml

@@ -77,11 +77,12 @@ and sub s op_data =
   | (x, (t, e)) :: s -> (x, (tm t op_data, e)) :: sub s op_data
 
 and coh c op_data equiv =
-  let p, t, pp_data = Coh.forget c in
-  let op_p = ps p op_data in
-  let op_t = ty t op_data in
-  let t' = Unchecked.ty_sub_preimage op_t (Unchecked.sub_ps_to_sub equiv) in
-  check_coh op_p t' (op_pp_data pp_data op_data)
+  Coh.apply_ps
+    (fun p -> ps p op_data)
+    (fun t ->
+      Unchecked.ty_sub_preimage (ty t op_data) (Unchecked.sub_ps_to_sub equiv))
+    (fun pp -> op_pp_data pp op_data)
+    c
 
 and ctx c op_data =
   match c with

lib/suspension.ml

@@ -17,9 +17,7 @@ let sub = iter_option Unchecked.suspend_sub
 let coh i coh =
   match i with
   | None | Some 0 -> coh
-  | Some _ ->
-      let p, t, ppd = Coh.forget coh in
-      check_coh (ps i p) (ty i t) (pp_data i ppd)
+  | Some _ -> Coh.apply_ps (ps i) (ty i) (pp_data i) coh
 
 let checked_tm i t =
   match i with

lib/unchecked.ml

@@ -718,8 +718,8 @@ struct
               "image of a variable by a display map must be a variable"
 
       (* Pullback of a substitution along a display map. Returns the resulting
-       * context with the right canonical inclusion. The left canonical inclusion is
-       *  the identity. *)
+         * context with the right canonical inclusion. The left canonical inclusion is
+         *  the identity. *)
       let rec pullback c1 sub c2 dm =
         match (c2, dm) with
         | [], [] -> (c1, [])
@@ -737,7 +737,7 @@ struct
                context"
 
       (* Universal property of the pullback, gluing substitutions s1 and s2. Requires
-       * the inr canonical inclusion, the second context and the display map *)
+         * the inr canonical inclusion, the second context and the display map *)
       let rec glue s1 s2 inr c2 dm =
         match (s2, c2, dm) with
         | [], [], [] -> s1
@@ -761,6 +761,15 @@ struct
             Error.fatal
               "wrong data pullback gluing: substitution must be point to the \
                context"
+
+      let pp_data_rename pp names =
+        let name, susp, func = pp in
+        let rec rename f =
+          match f with
+          | [] -> []
+          | (x, i) :: f -> (var_apply_sub x names, i) :: rename f
+        in
+        (name, susp, List.map rename func)
     end
   end
 end

lib/unchecked.mli

@@ -97,6 +97,7 @@ end) : sig
       val var_apply_sub : Var.t -> sub -> Var.t
       val pullback : ctx -> sub -> ctx -> sub -> ctx * sub
       val glue : sub -> sub -> sub -> ctx -> sub -> sub
+      val pp_data_rename : pp_data -> sub -> pp_data
     end
   end
 end