feat(level): implement level comparison

src/core-logic/level.ml

@@ -7,27 +7,27 @@ type view = level_view =
   | L_max of level * level  (** max *)
   | L_imax of level * level  (** impredicative max. *)
 
-and t = level = { l_view: level_view; mutable l_id: int }
+and t = level = { l_view: level_view; mutable l_id: int; mutable l_flags: int }
 
 let[@inline] view (self : t) : view = self.l_view
 let[@inline] equal (a : t) (b : t) : bool = a == b
 let[@inline] hash (a : t) : int = Hash.int a.l_id
 let[@inline] compare a b : int = compare a.l_id b.l_id
 
+let equal_view (a : view) (b : view) : bool =
+  match a, b with
+  | L_zero, L_zero -> true
+  | L_succ a, L_succ b -> equal a b
+  | L_var a, L_var b -> String.equal a b
+  | L_imax (a1, a2), L_imax (b1, b2) | L_max (a1, a2), L_max (b1, b2) ->
+    equal a1 b1 && equal a2 b2
+  | (L_zero | L_succ _ | L_var _ | L_max _ | L_imax _), _ -> false
+
 (* hashconsing *)
 module H_cons = Hashcons.Make (struct
   type nonrec t = t
 
-  let equal (a : t) (b : t) : bool =
-    a == b
-    ||
-    match view a, view b with
-    | L_zero, L_zero -> true
-    | L_succ a, L_succ b -> equal a b
-    | L_var a, L_var b -> String.equal a b
-    | L_imax (a1, a2), L_imax (b1, b2) | L_max (a1, a2), L_max (b1, b2) ->
-      equal a1 b1 && equal a2 b2
-    | (L_zero | L_succ _ | L_var _ | L_max _ | L_imax _), _ -> false
+  let[@inline] equal a b = a == b || equal_view (view a) (view b)
 
   let hash a : int =
     match view a with
@@ -62,22 +62,49 @@ let rec pp out (self : t) : unit =
 
 let to_string = Fmt.to_string pp
 
-type store = { h_cons: H_cons.t }
+(* 5 bits in [t.id] are used to store which store it belongs to, so we have
+   a chance of detecting when the user passes a term to the wrong store *)
+let store_id_bits = 5
+let store_id_mask = (1 lsl store_id_bits) - 1
+
+type store = { h_cons: H_cons.t; id: int }
 
 module Store = struct
   type t = store
 
-  let create () : store = { h_cons = H_cons.create ~size:64 () }
+  let _id = ref 0
+
+  let create () : store =
+    let id = !_id land store_id_mask in
+    incr _id;
+    { h_cons = H_cons.create ~size:64 (); id }
 end
 
-let make_ (self : store) (l_view : view) : t =
-  let lvl = { l_view; l_id = -1 } in
-  H_cons.hashcons self.h_cons lvl
+let[@inline] is_ground (self : t) : bool = self.l_flags lsl store_id_bits != 0
 
-let zero self : t = make_ self L_zero
-let succ self t : t = make_ self (L_succ t)
-let one self = succ self @@ zero self
-let var self n : t = make_ self (L_var n)
+let is_ground_view_ (view : view) : bool =
+  match view with
+  | L_zero -> true
+  | L_succ a -> is_ground a
+  | L_var _ -> false
+  | L_max (a, b) | L_imax (a, b) -> is_ground a && is_ground b
+
+let make_ (self : store) (l_view : view) : t =
+  let lvl = { l_view; l_id = -1; l_flags = 0 } in
+  let lvl' = H_cons.hashcons self.h_cons lvl in
+  if lvl == lvl' then (
+    let ground = is_ground_view_ l_view in
+    lvl.l_flags <-
+      (Util.int_of_bool ground lsl store_id_bits)
+      lor (lvl.l_id lsl store_id_bits)
+  );
+  lvl'
+
+let[@inline] zero self : t = make_ self L_zero
+let[@inline] succ self t : t = make_ self (L_succ t)
+let[@inline] one self = succ self @@ zero self
+let[@inline] var self n : t = make_ self (L_var n)
+let[@inline] store_id (self : t) : int = self.l_flags land store_id_mask
 
 let rec max self a b : t =
   if equal a b then
@@ -123,6 +150,23 @@ let[@inline] is_zero l =
   | L_zero -> true
   | _ -> false
 
+(** [subst_v store lvl v u] replaces [v] with [u] in [lvl] *)
+let subst_v (self : store) (lvl : t) (v : string) (u : t) =
+  let rec loop lvl : t =
+    if is_ground lvl then
+      lvl
+    else (
+      match view lvl with
+      | L_var v' when v = v' -> u
+      | L_var _ -> lvl
+      | L_zero -> assert false
+      | L_succ a -> succ self (loop a)
+      | L_max (a, b) -> max self (loop a) (loop b)
+      | L_imax (a, b) -> imax self (loop a) (loop b)
+    )
+  in
+  loop lvl
+
 let is_one l =
   match view l with
   | L_succ a -> is_zero a
@@ -136,3 +180,48 @@ let as_int self : _ option =
     None
 
 let is_int self : bool = Option.is_some (as_int self)
+
+let leq_judge st l1 l2 : bool =
+  assert (store_id l1 = st.id);
+  assert (store_id l2 = st.id);
+
+  (* [l <= l' + n] *)
+  let rec prove_rec ~max_inst (l : t) (l' : t) n : bool =
+    let prove = prove_rec ~max_inst in
+    match l.l_view, l'.l_view with
+    | L_zero, _ when n >= 0 -> true
+    | _ when equal l l' && n >= 0 -> true
+    | L_succ l, _ -> prove l l' (n - 1)
+    | _, L_succ l' -> prove l l' (n + 1)
+    | _, L_max (l1, l2) -> prove l l1 n || prove l l2 n
+    | L_max (l1, l2), _ -> prove l1 l' n && prove l2 l' n
+    | L_imax (_l1, { l_view = L_zero; _ }), _ -> prove (zero st) l' n
+    | L_imax (l1, ({ l_view = L_succ _; _ } as l2)), _ ->
+      prove (max st l1 l2) l' n
+    | L_imax (l1, { l_view = L_imax (l2, l3); _ }), _ ->
+      prove (max st (imax st l1 l3) (imax st l2 l3)) l' n
+    | _, L_imax (l1, { l_view = L_imax (l2, l3); _ }) ->
+      prove l (max st (imax st l1 l3) (imax st l2 l3)) n
+    | L_imax (l1, { l_view = L_max (l2, l3); _ }), _ ->
+      prove (max st (imax st l1 l2) (imax st l1 l3)) l' n
+    | _, L_imax (l1, { l_view = L_max (l2, l3); _ }) ->
+      prove l (max st (imax st l1 l2) (imax st l1 l3)) n
+    | (L_var v, _ | _, L_var v) when max_inst > 0 ->
+      (* replace [v] as [0] and [succ v], prove in both cases *)
+      (let v' = zero st in
+       prove_rec ~max_inst:(max_inst - 1) (subst_v st l v v')
+         (subst_v st l' v v') n)
+      &&
+      let v' = succ st (var st v) in
+      prove_rec ~max_inst:(max_inst - 1) (subst_v st l v v')
+        (subst_v st l' v v') n
+    | _ -> false
+  in
+
+  equal l1 l2
+  ||
+  let l2, n = as_offset l2 in
+  prove_rec ~max_inst:10 l1 l2 n
+
+let eq_judge st l1 l2 : bool =
+  equal l1 l2 || (leq_judge st l1 l2 && leq_judge st l2 l1)

src/core-logic/level.mli

@@ -39,3 +39,13 @@ val is_zero : t -> bool
 val is_one : t -> bool
 val is_int : t -> bool
 val as_int : t -> int option
+
+(** {2 Equivalence} *)
+
+val leq_judge : store -> t -> t -> bool
+(** [leq_judge st l1 l2] is [true] if [l1] is proven to be lower
+    or equal to [l2] *)
+
+val eq_judge : store -> t -> t -> bool
+(** [eq_judge st l1 l2] is [true] iff [leq_judge l1 l2]
+    and [leq_judge l2 l1] *)

src/core-logic/term.ml

@@ -556,10 +556,7 @@ module Make_ = struct
       let has_fvars = compute_has_fvars_ e in
       e2.flags <-
         (compute_db_depth_ e lsl (1 + store_id_bits))
-        lor (if has_fvars then
-              1 lsl store_id_bits
-            else
-              0)
+        lor (Util.int_of_bool has_fvars lsl store_id_bits)
         lor self.s_uid;
       Store.check_e_uid self e2
     );

src/core-logic/types_.ml

@@ -10,7 +10,7 @@ type level_view =
   | L_max of level * level  (** max *)
   | L_imax of level * level  (** impredicative max. *)
 
-and level = { l_view: level_view; mutable l_id: int }
+and level = { l_view: level_view; mutable l_id: int; mutable l_flags: int }
 (** A level expression *)
 
 type term_view =

src/util/Util.ml

@@ -16,6 +16,12 @@ let pp_pair ?(sep = " ") pp1 pp2 out t =
 let pp_array ?(sep = " ") pp out l = Fmt.array ~sep:(pp_sep sep) pp out l
 let flat_map_l_arr f l = CCList.flat_map (fun x -> CCArray.to_list @@ f x) l
 
+let[@inline] int_of_bool (b : bool) : int =
+  if b then
+    1
+  else
+    0
+
 let array_iteri2 ~f a b =
   let open Array in
   if length a <> length b then invalid_arg "iteri2";

src/util/Util.mli

@@ -13,6 +13,7 @@ val flat_map_l_arr : ('a -> 'b array) -> 'a list -> 'b list
 val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
 (** [array_of_list_map f l] is the same as [Array.of_list @@ List.map f l] *)
 
+val int_of_bool : bool -> int
 val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
 val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t
 val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t