From 37411ed50f416a62c94540a99c4a0d08d3644789 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 15 Mar 2026 04:24:54 +0000 Subject: [PATCH] core-logic: add def_eq + whnf --- src/core-logic/reduce.ml | 81 +++++++++++++++++++++++++++ src/core-logic/reduce.mli | 13 +++++ src/core-logic/sidekick_core_logic.ml | 1 + src/core-logic/term.ml | 14 +++-- src/core-logic/term.mli | 4 ++ 5 files changed, 108 insertions(+), 5 deletions(-) create mode 100644 src/core-logic/reduce.ml create mode 100644 src/core-logic/reduce.mli diff --git a/src/core-logic/reduce.ml b/src/core-logic/reduce.ml new file mode 100644 index 00000000..f90f55ea --- /dev/null +++ b/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 diff --git a/src/core-logic/reduce.mli b/src/core-logic/reduce.mli new file mode 100644 index 00000000..a252518f --- /dev/null +++ b/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. *) diff --git a/src/core-logic/sidekick_core_logic.ml b/src/core-logic/sidekick_core_logic.ml index 977f2f20..56cc3ed5 100644 --- a/src/core-logic/sidekick_core_logic.ml +++ b/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 diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml index a7f546f5..c9613f9f 100644 --- a/src/core-logic/term.ml +++ b/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 diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli index 6309788f..4fec61dd 100644 --- a/src/core-logic/term.mli +++ b/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 (**/**)