Various imrpovements

CHANGES.md

@@ -1,4 +1,5 @@
 ## Catt
+- Improve efficiency by storing partially checked terms
 - Computation of cylinder compositions as a builtin
 - Computation of cone compositions as a builtin
 

coq_plugin/src/export.ml

@@ -20,6 +20,12 @@ let rec catt_var_to_coq_name v =
   | Var.Plus v -> catt_var_to_coq_name v ^ "_plus"
   | Var.Bridge v -> catt_var_to_coq_name v ^ "_bridge"
 
+let counter = ref 0
+
+let anon () =
+  incr counter;
+  Printf.sprintf "anonymous_term_%d" !counter
+
 let c_Q env sigma =
   let gr = Coqlib.lib_ref "core.eq.type" in
   Evd.fresh_global env sigma gr
@@ -280,7 +286,11 @@ end = struct
     match retrieve_lambda value sigma with
     | Some res -> res
     | None ->
-        let name = clean_name (Tm.full_name tm) in
+        let name =
+          match Tm.full_name tm with
+          | Some name -> clean_name name
+          | None -> anon ()
+        in
         let ctx = Tm.ctx tm in
         let tm = Tm.develop tm in
         let env, sigma, tm =

lib/builtin.ml

@@ -16,33 +16,39 @@ module Memo = struct
     check_coh (Br []) (Arr (Obj, Var (Db 0), Var (Db 0))) ("builtin_id", 0, [])
 end
 
-let rec ps_comp i =
-  match i with
-  | i when i <= 0 -> Error.fatal "builtin composition with less than 0 argument"
-  | i when i = 1 -> Br [ Br [] ]
-  | i -> ( match ps_comp (i - 1) with Br l -> Br (Br [] :: l))
+module Comp = struct
+  let tdb i = Var (Var.Db i)
+  let tree i = Br (List.init i (fun _ -> Br []))
+  let x i = if i = 0 then (tdb 0, Obj) else (tdb ((2 * i) - 1), Obj)
+  let f i = (tdb (2 * i), Arr (Obj, fst @@ x (i - 1), fst @@ x i))
 
-let comp_n arity =
-  let build_comp i =
-    let ps = ps_comp i in
-    let pp_data = (Printf.sprintf "builtin_comp%i" arity, 0, []) in
-    Coh.check_noninv ps (Var (Db 0)) (Var (Db 0)) pp_data
-  in
-  Memo.find arity build_comp
+  let comp_n arity =
+    let build_comp i =
+      let ps = tree i in
+      let pp_data = (Printf.sprintf "builtin_comp%i" arity, 0, []) in
+      Coh.check_noninv ps (fst (x 0)) (fst (x 0)) pp_data
+    in
+    Memo.find arity build_comp
 
-let arity_comp s expl =
-  let n = List.length s in
-  if expl || !Settings.explicit_substitutions then (n - 1) / 2 else n
+  let arity_comp s expl =
+    let n = List.length s in
+    if expl || !Settings.explicit_substitutions then (n - 1) / 2 else n
 
-let comp s expl =
-  let arity = arity_comp s expl in
-  comp_n arity
+  let comp s expl =
+    let arity = arity_comp s expl in
+    comp_n arity
 
-let bcomp x y f z g =
-  let comp = comp_n 2 in
-  let sub = [ (g, true); (z, false); (f, true); (y, false); (x, false) ] in
-  Coh (comp, sub)
+  let bcomp x y f z g =
+    let comp = comp_n 2 in
+    let sub = [ (g, true); (z, false); (f, true); (y, false); (x, false) ] in
+    Coh (comp, sub)
+end
 
+let ps_comp = Comp.tree
+let comp_n = Comp.comp_n
+let arity_comp = Comp.arity_comp
+let comp = Comp.comp
+let bcomp = Comp.bcomp
 let id = Memo.id
 
 let id_all_max ps =
@@ -84,16 +90,14 @@ let unbiased_unitor ps t =
     let coh = Coh.check_noninv ps t t ("endo", 0, []) in
     Coh (coh, id_all_max ps)
   in
-  let a =
-    UnnamedTm.ty (check_unnamed_term (Ctx.check (Unchecked.ps_to_ctx bdry)) t)
-  in
+  let a = Tm.ty (check_term (Ctx.check (Unchecked.ps_to_ctx bdry)) t) in
   let da = Unchecked.dim_ty a in
   let sub_base = Unchecked.ty_to_sub_ps a in
   let tgt = Coh (Suspension.coh (Some da) (id ()), (t, true) :: sub_base) in
   Coh.check_inv bdry src tgt ("unbiased_unitor", 0, [])
 
 let tdb i = Var (Var.Db i)
-let wcomp = ref (fun _ -> Error.fatal "Uninitialised forward reference")
+let wcomp = ref (fun _ -> Error.fatal "Uninitialised forward reference wcomp")
 
 (*
   (a *_n b) *_0 g -> (a *_0 g) *_n (b *_0 g)

lib/builtin.mli

@@ -3,6 +3,12 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types(Coh)(Tm)
 
+module Comp : sig
+  val tree : int -> ps
+  val x : int -> constr
+  val f : int -> constr
+end
+
 val wcomp : (tm * ty -> int -> tm * ty -> tm * ty) ref
 val ps_comp : int -> ps
 val comp_n : int -> Coh.t

lib/command.ml

@@ -47,8 +47,8 @@ let check l e t =
         Some ty
   in
   let c = Kernel.Ctx.check c in
-  let tm = Kernel.check_unnamed_term c ?ty e in
-  let ty = Kernel.UnnamedTm.ty tm in
+  let tm = Kernel.check_term c ?ty e in
+  let ty = Kernel.Tm.ty tm in
   (e, ty)
 
 let exec_check_builtin b =

lib/cones.ml

@@ -208,7 +208,7 @@ module Codim1 = struct
     in
     let tm, _ = wcomp tm_1 1 tm_2 in
     let name = Printf.sprintf "builtin_conecomp(%d,%d,%d)" 2 1 2 in
-    check_term (Ctx.check ctx) (name, 0, []) tm
+    check_term (Ctx.check ctx) ~name:(name, 0, []) tm
 
   let intch n =
     let with_type ctx x = (Var x, fst (List.assoc x ctx)) in
@@ -263,15 +263,15 @@ module Codim1 = struct
               (Suspension.sub (Some 1)
                  (Opposite.sub (Cone.bdry_left (n - 1) (n - 2)) op_data))
           in
-          check_term (Ctx.check ctx_comp) (name, 0, []) (App (comp, sub))
+          check_term (Ctx.check ctx_comp) ~name:(name, 0, []) (App (comp, sub))
         in
         let intch = intch n in
         let socomp = (Tm.develop suspopcomp, Tm.ty suspopcomp) in
         let tm, _ =
           if n mod 2 = 0 then wcomp socomp (n - 1) intch
           else wcomp intch (n - 1) socomp
         in
-        check_term (Ctx.check ctx_comp) (name, 0, []) tm
+        check_term (Ctx.check ctx_comp) ~name:(name, 0, []) tm
 end
 
 module Composition = struct
@@ -369,7 +369,7 @@ module Composition = struct
         let ctx, _, _ = Unchecked.db_levels ctx in
         let tm = Unchecked.tm_apply_sub (Tm.develop tm) names in
         let name = Printf.sprintf "builtin_conecomp(%d,%d,%d)" n k m in
-        let res = check_term (Ctx.check ctx) (name, 0, []) tm in
+        let res = check_term (Ctx.check ctx) ~name:(name, 0, []) tm in
         Hashtbl.add tbl (n, m, k) res;
         res
 end

lib/construct.ml

@@ -2,7 +2,11 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types (Coh) (Tm)
 
-type constr = tm * ty
+let to_tm (tm, _) = tm
+let to_ty (_, ty) = ty
+let characteristic_sub_ps (tm, ty) = (tm, true) :: Unchecked.ty_to_sub_ps ty
+let dim (_, ty) = Unchecked.dim_ty ty
+let arr (tm1, ty1) (tm2, _) = Arr (ty1, tm1, tm2)
 
 let rec bdry n (t, ty) =
   match (n, ty) with
@@ -11,7 +15,52 @@ let rec bdry n (t, ty) =
   | _, Arr (b, s, _) -> bdry (n - 1) (s, b)
   | _, _ -> assert false
 
-let _src n t = fst (bdry n t)
+let coh_app coh tms =
+  let elaborate ps tms =
+    let rec aux_list psl tms =
+      match (psl, tms) with
+      | [], t :: tms -> ([ (fst t, true) ], tms, snd t)
+      | [ ps ], tms -> (
+          let s, tms, ty = aux ps tms in
+          match ty with
+          | Arr (ty, src, tgt) -> (s @ [ (tgt, false); (src, false) ], tms, ty)
+          | _ -> assert false)
+      | ps :: psl, tms -> (
+          let s, tms, _ = aux_list psl tms in
+          let sub_ps, tms, ty = aux ps tms in
+          match ty with
+          | Arr (ty, _, tgt) -> (sub_ps @ ((tgt, false) :: s), tms, ty)
+          | _ -> assert false)
+      | _ -> assert false
+    and aux ps tms = match ps with Br l -> aux_list l tms in
+    let sub_ps, _, _ = aux ps tms in
+    sub_ps
+  in
+  let ps, ty, _ = Coh.forget coh in
+  let sub = elaborate ps tms in
+  (Coh (coh, sub), Unchecked.ty_apply_sub_ps ty sub)
+
+let of_coh coh =
+  let ps, ty, _ = Coh.forget coh in
+  let id = Unchecked.identity_ps ps in
+  (Coh (coh, id), ty)
+
+let make_sub ctx list =
+  List.map2 (fun (x, (_, b)) t -> (x, (fst t, b))) ctx list
+
+let tm_app_sub tm sub =
+  let ty = Tm.ty tm in
+  (App (tm, sub), Unchecked.ty_apply_sub ty sub)
+
+let of_tm tm =
+  let c = Tm.ctx tm in
+  tm_app_sub tm (Unchecked.identity c)
+
+let tm_app tm sub =
+  let sub = make_sub (Tm.ctx tm) sub in
+  tm_app_sub tm sub
+
+let src n t = fst (bdry n t)
 let tgt n t = snd (bdry n t)
 let wcomp = Functorialisation.wcomp
 let () = Builtin.wcomp := wcomp
@@ -84,3 +133,103 @@ let intch_comp_mn a b c =
 
 let opposite (t, ty) op_data = (Opposite.tm t op_data, Opposite.ty ty op_data)
 let inv (t, ty) = (Inverse.compute_inverse t, Inverse.ty ty)
+
+let id constr =
+  let d = dim constr in
+  ( Coh (Suspension.coh (Some d) (Builtin.id ()), characteristic_sub_ps constr),
+    arr constr constr )
+
+let rec id_n n constr =
+  match n with
+  | 0 -> constr
+  | n when n > 0 -> id (id_n (n - 1) constr)
+  | _ -> Error.fatal "call to id_n with a negative argument"
+
+let apply_sub (tm, ty) sigma =
+  (Unchecked.tm_apply_sub tm sigma, Unchecked.ty_apply_sub ty sigma)
+
+let apply_sub_ps (tm, ty) sigma =
+  (Unchecked.tm_apply_sub_ps tm sigma, Unchecked.ty_apply_sub_ps ty sigma)
+
+let rename (tm, ty) sigma =
+  (Unchecked.tm_rename tm sigma, Unchecked.ty_rename ty sigma)
+
+let inverse (tm, ty) = (Inverse.compute_inverse tm, Inverse.ty ty)
+let suspend i (tm, ty) = (Suspension.tm (Some i) tm, Suspension.ty (Some i) ty)
+
+let functorialise (tm, ty) vars =
+  (Functorialisation.tm_one_step_tm tm vars, Functorialisation.ty ty vars tm)
+
+(* TODO: more optimised implementation of this function *)
+let comp_n constrs =
+  let constrs_rev = List.rev constrs in
+  let first = function [] -> assert false | h :: _ -> h in
+  let rec glue_subs = function
+    | [ c ] -> characteristic_sub_ps c
+    | c :: constrs ->
+        (to_tm c, true) :: (to_tm (tgt 1 c), false) :: glue_subs constrs
+    | [] -> assert false
+  in
+  let l = List.length constrs in
+  let c = first constrs in
+  let d = dim c in
+  ( Coh (Suspension.coh (Some (d - 1)) (Builtin.comp_n l), glue_subs constrs_rev),
+    arr (src 1 c) (tgt 1 (first constrs_rev)) )
+
+let comp c1 c2 = comp_n [ c1; c2 ]
+let comp3 c1 c2 c3 = comp_n [ c1; c2; c3 ]
+let op dims (tm, ty) = (Opposite.tm tm dims, Opposite.ty ty dims)
+
+let drop n xs =
+  let rec aux xs counter =
+    match xs with
+    | [] -> []
+    | h :: tl -> if counter > 0 then h :: aux tl (counter - 1) else []
+  in
+  aux xs (List.length xs - n)
+
+let characteristic_sub_ps_composite constrs =
+  let rec aux = function
+    | [] -> assert false
+    | [ constr ] -> characteristic_sub_ps constr
+    | constr :: tail ->
+        [ (to_tm constr, true); (to_tm @@ tgt 1 constr, false) ] @ aux tail
+  in
+  aux @@ List.rev constrs
+
+let glue_subs_along k subs =
+  let rec aux = function
+    | [] -> assert false
+    | [ sub ] -> sub
+    | sub :: subs -> drop ((2 * k) + 1) sub @ aux subs
+  in
+  aux @@ List.rev subs
+
+let rec whisk_n n dims =
+  let l = List.length dims in
+  let comp = Builtin.comp_n l in
+  let func_data =
+    List.rev
+    @@ List.mapi (fun idx dim -> (Var.Db (2 * (idx + 1)), dim - 1)) dims
+  in
+  let whisk = Functorialisation.coh_successively comp func_data in
+  Suspension.checked_tm (Some n) whisk
+
+and wcomp_n k constrs =
+  let dims_adjusted = List.map (fun c -> dim c - k) constrs in
+  let whisk = whisk_n k dims_adjusted in
+  let whisk_sub_ps =
+    glue_subs_along k (List.map characteristic_sub_ps constrs)
+  in
+  let whisk_sub = Unchecked.sub_ps_to_sub whisk_sub_ps in
+  (App (whisk, whisk_sub), Unchecked.ty_apply_sub_ps (Tm.ty whisk) whisk_sub_ps)
+
+let witness constr =
+  let tm = to_tm constr in
+  let d = dim constr in
+  let ty =
+    arr (wcomp constr (d - 1) (inverse constr)) (id_n 1 (src 1 constr))
+  in
+  (Inverse.compute_witness tm, ty)
+
+let develop (tm, ty) = (Unchecked.develop_tm tm, Unchecked.develop_ty ty)

lib/construct.mli

@@ -2,11 +2,40 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types(Coh)(Tm)
 
-type constr = tm * ty
-
+val to_tm : constr -> tm
+val to_ty : constr -> ty
+val arr : constr -> constr -> ty
+val characteristic_sub_ps : constr -> sub_ps
+val coh_app : Coh.t -> constr list -> constr
+val of_coh : Coh.t -> constr
+val make_sub : ctx -> constr list -> sub
+val tm_app_sub : Tm.t -> sub -> constr
+val tm_app : Tm.t -> constr list -> constr
+val of_tm : Tm.t -> constr
 val wcomp : constr -> int -> constr -> constr
 val wcomp3 : constr -> int -> constr -> int -> constr -> constr
 val intch_comp_nm : constr -> constr -> constr -> constr
 val intch_comp_mn : constr -> constr -> constr -> constr
 val opposite : constr -> op_data -> constr
 val inv : constr -> constr
+val functorialise : constr -> Var.t list -> constr
+val id : constr -> constr
+val id_n : int -> constr -> constr
+val dim : constr -> int
+val apply_sub : constr -> sub -> constr
+val apply_sub_ps : constr -> sub_ps -> constr
+val rename : constr -> (Var.t * tm) list -> constr
+val bdry : int -> constr -> constr * constr
+val src : int -> constr -> constr
+val tgt : int -> constr -> constr
+val inverse : constr -> constr
+val suspend : int -> constr -> constr
+val comp_n : constr list -> constr
+val comp : constr -> constr -> constr
+val comp3 : constr -> constr -> constr -> constr
+val op : int list -> constr -> constr
+val witness : constr -> constr
+val glue_subs_along : int -> 'a list list -> 'a list
+val wcomp_n : int -> constr list -> constr
+val characteristic_sub_ps_composite : constr list -> sub_ps
+val develop : constr -> constr

lib/cubical_composite.ml

@@ -412,7 +412,7 @@ let coh_depth1 coh l =
   in
   let comp = Suspension.coh (Some d) (Builtin.comp_n 3) in
   let ctx = F.ctx (Unchecked.ps_to_ctx ps) l in
-  let pp_data = F.pp_data l pp_data in
-  check_term (Ctx.check ctx) pp_data (Coh (comp, comp_sub_ps))
+  let name = F.pp_data l pp_data in
+  check_term (Ctx.check ctx) ~name (Coh (comp, comp_sub_ps))
 
 let init () = F.coh_depth1 := coh_depth1