core-logic: add def_eq + whnf

src/core-logic/reduce.ml

@@ -0,0 +1,81 @@
+open Types_
+module T = Term
+
+(* Pair-keyed table for def_eq cache *)
+module T2_tbl = CCHashtbl.Make (struct
+  type t = term * term
+
+  let equal (a1, b1) (a2, b2) = T.equal a1 a2 && T.equal b1 b2
+  let hash (a, b) = CCHash.combine3 91 (T.hash a) (T.hash b)
+end)
+
+(** Weak head normal form.
+    Beta-reduces at the head until stuck. Memoised via [cache]. *)
+let whnf ?(cache = T.Tbl.create 16) store e =
+  let rec loop e =
+    match T.Tbl.find_opt cache e with
+    | Some v -> v
+    | None ->
+      let v = step e in
+      T.Tbl.add cache e v;
+      v
+  and step e =
+    match T.view e with
+    | E_app (f, a) ->
+      let f' = loop f in
+      (match T.view f' with
+      | E_lam (_, _, body) -> loop (T.DB.subst_db0 store body ~by:a)
+      | _ ->
+        if f == f' then
+          e
+        else
+          T.app store f' a)
+    | _ -> e
+  in
+  loop e
+
+(** Definitional equality: WHNF both sides, then compare structurally.
+    Uses [Level.judge_eq] for universe levels.
+    Memoised via pair cache to handle sharing in DAGs. *)
+let def_eq store e1 e2 =
+  let whnf_cache = T.Tbl.create 16 in
+  let eq_cache : bool T2_tbl.t = T2_tbl.create 16 in
+  let whnf = whnf ~cache:whnf_cache store in
+
+  let rec go e1 e2 =
+    if T.equal e1 e2 then true
+    else
+      (* canonical order to halve cache size *)
+      let key =
+        if T.compare e1 e2 <= 0 then
+          e1, e2
+        else
+          e2, e1
+      in
+      match T2_tbl.find_opt eq_cache key with
+      | Some b -> b
+      | None ->
+        (* assume true while recursing (for coinductive guard on open terms) *)
+        T2_tbl.add eq_cache key true;
+        let r = check e1 e2 in
+        T2_tbl.replace eq_cache key r;
+        r
+  and check e1 e2 =
+    let e1 = whnf e1 in
+    let e2 = whnf e2 in
+    if T.equal e1 e2 then true
+    else
+      match T.view e1, T.view e2 with
+      | E_type l1, E_type l2 -> Level.judge_eq (T.Store.lvl_store store) l1 l2
+      | E_var v1, E_var v2 -> Var.equal v1 v2
+      | E_const c1, E_const c2 -> Const.equal c1 c2
+      | E_bound_var b1, E_bound_var b2 -> Bvar.equal b1 b2
+      | E_app (f1, a1), E_app (f2, a2) -> go f1 f2 && go a1 a2
+      | E_lam (_, ty1, b1), E_lam (_, ty2, b2) -> go ty1 ty2 && go b1 b2
+      | E_pi (_, ty1, b1), E_pi (_, ty2, b2) -> go ty1 ty2 && go b1 b2
+      | _ -> false
+  in
+  go e1 e2
+
+(* Install into the kernel *)
+let () = T.Internal_.def_eq_ref := def_eq

src/core-logic/reduce.mli

@@ -0,0 +1,13 @@
+val whnf : ?cache:Term.t Term.Tbl.t -> Term.store -> Term.t -> Term.t
+(** [whnf store e] reduces [e] to weak head normal form by beta-reducing at
+    the head until stuck. The optional [cache] is a memoisation table; pass
+    the same table across calls to amortise work over a DAG. *)
+
+val def_eq : Term.store -> Term.t -> Term.t -> bool
+(** [def_eq store a b] is true iff [a] and [b] are definitionally equal:
+    both sides are reduced to WHNF and then compared structurally, using
+    [Level.judge_eq] for universe levels. Results are memoised internally
+    on the shared DAG structure.
+
+    Note: this is installed as the kernel's equality check ([Term.Internal_.def_eq_ref])
+    when this module is loaded. *)

src/core-logic/sidekick_core_logic.ml

@@ -6,6 +6,7 @@ module Subst = Subst
 module T_builtins = T_builtins
 module Store = Term.Store
 module Level = Level
+module Reduce = Reduce
 
 (* TODO: move to separate library? *)
 module Str_const = Str_const

src/core-logic/term.ml

@@ -454,8 +454,11 @@ module Make_ = struct
     else
       aux e 0
 
-  (* TODO: have beta-reduction here; level checking; and pluggable reduction
-     rules (in the store) so we can reduce quotients and recursors *)
+  (* Definitional equality: installed by Reduce, defaults to syntactic equality *)
+  let def_eq_ref : (store -> term -> term -> bool) ref =
+    ref (fun _ a b -> equal a b)
+
+  (* TODO: pluggable reduction rules (in the store) for quotients and recursors *)
 
   (** compute the type of [view]. *)
   let compute_ty_ (self : store) ~make (view : view) : term =
@@ -485,9 +488,8 @@ module Make_ = struct
       let ty_a = ty a in
       (match ty_f.view with
       | E_pi (_, ty_arg_f, ty_bod_f) ->
-        (* check that the expected type matches *)
-        (* FIXME: replace [equal] with definitional equality *)
-        if not (equal ty_arg_f ty_a) then
+        (* check that the expected type matches, using definitional equality *)
+        if not (!def_eq_ref self ty_arg_f ty_a) then
           Error.errorf
             "@[<2>cannot @[apply `%a`@]@ @[to `%a`@],@ expected argument type: \
              `%a`@ @[actual: `%a`@]@]"
@@ -718,4 +720,6 @@ module Internal_ = struct
 
   let subst_ store ~recursive t subst =
     subst_ ~make:(make_ store) ~recursive t subst
+
+  let def_eq_ref = def_eq_ref
 end

src/core-logic/term.mli

@@ -186,6 +186,10 @@ module Internal_ : sig
     t ->
     f:(recurse:(t -> t) -> t -> t option) ->
     t
+
+  val def_eq_ref : (store -> t -> t -> bool) ref
+  (** Definitional equality hook. Defaults to syntactic equality.
+      Overwritten by [Reduce] at init time. *)
 end
 
 (**/**)