Kernel Performance Improvements

dune-workspace

@@ -0,0 +1,9 @@
+(lang dune 3.7)
+
+(context default)
+(context
+  (default
+     (name profiling)
+     (instrument_with landmarks)
+     (env
+       (_ (env-vars ("OCAML_LANDMARKS" "output=profile.txt"))))))

flake.nix

@@ -192,6 +192,8 @@
               ocamlformat
               ocp-indent
               ocamlformat-rpc-lib
+              landmarks
+              landmarks-ppx
               utop
             ]);
 

lib/builtin.ml

@@ -12,7 +12,7 @@ module Memo = struct
       Hashtbl.add tbl i res;
       res
 
-  let id =
+  let id _ =
     check_coh (Br []) (Arr (Obj, Var (Db 0), Var (Db 0))) ("builtin_id", 0, [])
 end
 
@@ -46,7 +46,7 @@ let id_all_max ps =
     let t = Var (Db 0) in
     match l with
     | [] -> [ (t, false) ]
-    | Br [] :: l -> (Coh (id, [ (t, true) ]), true) :: (t, false) :: id_map l
+    | Br [] :: l -> (Coh (id (), [ (t, true) ]), true) :: (t, false) :: id_map l
     | _ -> Error.fatal "identity must be inserted on maximal argument"
   in
   let rec aux i ps =
@@ -71,5 +71,5 @@ let unbiased_unitor ps 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
+  let tgt = Coh (Suspension.coh (Some da) (id ()), (t, true) :: sub_base) in
   Coh.check_inv bdry src tgt ("unbiased_unitor", 0, [])

lib/builtin.mli

@@ -7,5 +7,5 @@ val ps_comp : int -> ps
 val comp_n : int -> Coh.t
 val comp : subR -> bool -> Coh.t
 val arity_comp : subR -> bool -> int
-val id : Coh.t
+val id : unit -> Coh.t
 val unbiased_unitor : ps -> tm -> Coh.t

lib/dune

@@ -7,4 +7,5 @@
  (name catt)
  (public_name catt)
  (modules_without_implementation raw_types)
- (libraries base))
+ (libraries base)
+ (instrumentation (backend landmarks --auto)))

lib/inverse.ml

@@ -105,7 +105,7 @@ and cancel_all_linear_comp t =
         let id_src_t =
           let sub_base = Unchecked.ty_to_sub_ps ty_base in
           let id =
-            Suspension.coh (Some (Unchecked.dim_ty ty_base)) Builtin.id
+            Suspension.coh (Some (Unchecked.dim_ty ty_base)) (Builtin.id ())
           in
           Coh (id, (src_t, true) :: sub_base)
         in
@@ -164,7 +164,7 @@ and compute_witness_coh_inv c s ~ps ~pp_data ~d ~sub_base ~u ~v =
     Coh (comp, c_c_inv)
   in
   let tgt_wit =
-    let id = Suspension.coh (Some (d - 1)) Builtin.id in
+    let id = Suspension.coh (Some (d - 1)) (Builtin.id ()) in
     let sub_id_u = (u, true) :: sub_base in
     Coh (id, sub_id_u)
   in