From 08a7b7a3fda9edeccb77ff34328e17cd370b8fe0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 15 Mar 2026 04:27:06 +0000 Subject: [PATCH] core-logic: format --- src/core-logic/const.ml | 3 +- src/core-logic/const.mli | 10 ++-- src/core-logic/level.mli | 11 ++-- src/core-logic/reduce.ml | 22 ++++---- src/core-logic/reduce.mli | 18 +++---- src/core-logic/str_const.mli | 3 +- src/core-logic/t_builtins.mli | 10 ++-- src/core-logic/term.ml | 18 +++---- src/core-logic/term.mli | 96 +++++++++++++++++------------------ 9 files changed, 94 insertions(+), 97 deletions(-) diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml index 46b1c639..430050f0 100644 --- a/src/core-logic/const.ml +++ b/src/core-logic/const.ml @@ -26,5 +26,4 @@ let pp out (a : t) = a.c_ops.pp out a.c_view let ser ~ser_t (self : t) = self.c_ops.ser ser_t self.c_view let make c_view c_ops ~ty:c_ty : t = { c_view; c_ops; c_ty } -type decoders = - (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list +type decoders = (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli index 8fdd2f2d..948aa98a 100644 --- a/src/core-logic/const.mli +++ b/src/core-logic/const.mli @@ -1,6 +1,6 @@ (** Constants. - Constants are logical symbols, defined by the user thanks to an open type *) + Constants are logical symbols, defined by the user thanks to an open type *) open Types_ @@ -24,10 +24,8 @@ val make : view -> Ops.t -> ty:term -> t val ser : ser_t:(term -> Ser_value.t) -> t -> string * Ser_value.t val ty : t -> term -type decoders = - (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list -(** Decoders for constants: given a term store, return a list - of supported tags, and for each tag, a decoder for constants - that have this particular tag. *) +type decoders = (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list +(** Decoders for constants: given a term store, return a list of supported tags, + and for each tag, a decoder for constants that have this particular tag. *) include EQ_HASH_PRINT with type t := t diff --git a/src/core-logic/level.mli b/src/core-logic/level.mli index 41416052..f1cdecc7 100644 --- a/src/core-logic/level.mli +++ b/src/core-logic/level.mli @@ -42,16 +42,15 @@ val as_int : t -> int option (** {2 Judgements} - These are little proofs of some symbolic properties of levels, even - those which contain variables. *) + These are little proofs of some symbolic properties of levels, even those + which contain variables. *) val judge_leq : store -> t -> t -> bool -(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower - or equal to [l2] *) +(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower or equal to + [l2] *) val judge_eq : store -> t -> t -> bool -(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2] - and [judge_leq l2 l1] *) +(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2] and [judge_leq l2 l1] *) val judge_is_zero : store -> t -> bool (** [judge_is_zero st l] is [true] iff [l <= 0] holds *) diff --git a/src/core-logic/reduce.ml b/src/core-logic/reduce.ml index f90f55ea..037eae61 100644 --- a/src/core-logic/reduce.ml +++ b/src/core-logic/reduce.ml @@ -9,8 +9,8 @@ module T2_tbl = CCHashtbl.Make (struct 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]. *) +(** 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 @@ -34,17 +34,18 @@ let whnf ?(cache = T.Tbl.create 16) store 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. *) +(** 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 + if T.equal e1 e2 then + true + else ( (* canonical order to halve cache size *) let key = if T.compare e1 e2 <= 0 then @@ -60,11 +61,13 @@ let def_eq store e1 e2 = 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 + 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 @@ -74,6 +77,7 @@ let def_eq store e1 e2 = | 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 diff --git a/src/core-logic/reduce.mli b/src/core-logic/reduce.mli index a252518f..5ea78c20 100644 --- a/src/core-logic/reduce.mli +++ b/src/core-logic/reduce.mli @@ -1,13 +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. *) +(** [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. +(** [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. *) + 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/str_const.mli b/src/core-logic/str_const.mli index 086172c5..a1e1d7a8 100644 --- a/src/core-logic/str_const.mli +++ b/src/core-logic/str_const.mli @@ -1,7 +1,6 @@ (** Basic string constants. - These constants are a string name, coupled with a type. -*) + These constants are a string name, coupled with a type. *) open Types_ diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli index 7f16873c..5641783d 100644 --- a/src/core-logic/t_builtins.mli +++ b/src/core-logic/t_builtins.mli @@ -27,12 +27,12 @@ val is_eq : t -> bool val is_bool : t -> bool val abs : store -> t -> bool * t -(** [abs t] returns an "absolute value" for the term, along with the - sign of [t]. +(** [abs t] returns an "absolute value" for the term, along with the sign of + [t]. - The idea is that we want to turn [not a] into [(false, a)], - or [(a != b)] into [(false, a=b)]. For terms without a negation this - should return [(true, t)]. *) + The idea is that we want to turn [not a] into [(false, a)], or [(a != b)] + into [(false, a=b)]. For terms without a negation this should return + [(true, t)]. *) val as_bool_val : t -> bool option diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml index c9613f9f..f8c85b3c 100644 --- a/src/core-logic/term.ml +++ b/src/core-logic/term.ml @@ -404,9 +404,9 @@ module Make_ = struct map_shallow_ e ~make ~f:(fun inbind u -> loop u (if inbind then - k + 1 - else - k)) + k + 1 + else + k)) ) in assert (n >= 0); @@ -441,9 +441,9 @@ module Make_ = struct map_shallow_ e ~make ~f:(fun inb u -> aux u (if inb then - k + 1 - else - k)) + k + 1 + else + k)) in T_int_tbl.add cache_ (e, k) r; r) @@ -610,9 +610,9 @@ module Make_ = struct map_shallow_ e ~make ~f:(fun inb u -> loop (if inb then - k + 1 - else - k) + k + 1 + else + k) u) | Some u -> let u = db_shift_ ~make u k in diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli index 4fec61dd..8b938736 100644 --- a/src/core-logic/term.mli +++ b/src/core-logic/term.mli @@ -1,11 +1,11 @@ (** Core logic terms. - The core terms are expressions in the calculus of constructions, - with no universe polymorphism nor cumulativity. It should be fast, with hashconsing; - and simple enough (no inductives, no universe trickery). + The core terms are expressions in the calculus of constructions, with no + universe polymorphism nor cumulativity. It should be fast, with hashconsing; + and simple enough (no inductives, no universe trickery). - It is intended to be the foundation for user-level terms and types and formulas. -*) + It is intended to be the foundation for user-level terms and types and + formulas. *) open Types_ @@ -19,9 +19,9 @@ type t = term type store (** The store for terms. - The store is responsible for allocating unique IDs to terms, and - enforcing their hashconsing (so that syntactic equality is just a pointer - comparison). *) + The store is responsible for allocating unique IDs to terms, and enforcing + their hashconsing (so that syntactic equality is just a pointer comparison). +*) (** View. @@ -61,31 +61,30 @@ val as_type : t -> Level.t option val as_type_exn : t -> Level.t val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit -(** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included. - It must {b not} traverse [t] as a tree, but rather as a - perfectly shared DAG. +(** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included. It must + {b not} traverse [t] as a tree, but rather as a perfectly shared DAG. - For example, in: - {[ - let x = 2 in - let y = f x x in - let z = g y x in - z = z - ]} + For example, in: + {[ + let x = 2 in + let y = f x x in + let z = g y x in + z = z + ]} - the DAG has the following nodes: + the DAG has the following nodes: - {[ n1: 2 - n2: f n1 n1 - n3: g n2 n1 - n4: = n3 n3 - ]} - *) + {[ + n1: 2 + n2: f n1 n1 + n3: g n2 n1 + n4: = n3 n3 + ]} *) val iter_shallow : f:(bool -> t -> unit) -> t -> unit -(** [iter_shallow f e] iterates on immediate subterms of [e], - calling [f trdb e'] for each subterm [e'], with [trdb = true] iff - [e'] is directly under a binder. *) +(** [iter_shallow f e] iterates on immediate subterms of [e], calling + [f trdb e'] for each subterm [e'], with [trdb = true] iff [e'] is directly + under a binder. *) val map_shallow : store -> f:(bool -> t -> t) -> t -> t val exists_shallow : f:(bool -> t -> bool) -> t -> bool @@ -101,12 +100,11 @@ val is_a_type : t -> bool (** [is_a_type t] is true if [is_ty (ty t)] *) val is_closed : t -> bool -(** Is the term closed (all bound variables are paired with a binder)? - time: O(1) *) +(** Is the term closed (all bound variables are paired with a binder)? time: + O(1) *) val has_fvars : t -> bool -(** Does the term contain free variables? - time: O(1) *) +(** Does the term contain free variables? time: O(1) *) val ty : t -> t (** Return the type of this term. *) @@ -142,33 +140,33 @@ val open_lambda_exn : store -> t -> var * t (** De bruijn indices *) module DB : sig val lam_db : ?var_name:string -> store -> var_ty:t -> t -> t - (** [lam_db store ~var_ty bod] is [\ _:var_ty. bod]. Not DB shifting is done. *) + (** [lam_db store ~var_ty bod] is [\ _:var_ty. bod]. Not DB shifting is done. + *) val pi_db : ?var_name:string -> store -> var_ty:t -> t -> t - (** [pi_db store ~var_ty bod] is [pi _:var_ty. bod]. Not DB shifting is done. *) + (** [pi_db store ~var_ty bod] is [pi _:var_ty. bod]. Not DB shifting is done. + *) val subst_db0 : store -> t -> by:t -> t - (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with - the term [by]. This is useful, for example, to implement beta-reduction. + (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with the term + [by]. This is useful, for example, to implement beta-reduction. For example, with [t] being [_[0] = (\x. _[2] _[1] x[0])], - [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])]. - *) + [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])]. *) val shift : store -> t -> by:int -> t - (** [shift store t ~by] shifts all bound variables in [t] that are not - closed on, by amount [by] (which must be >= 0). + (** [shift store t ~by] shifts all bound variables in [t] that are not closed + on, by amount [by] (which must be >= 0). - For example, with term [t] being [\x. _[1] _[2] x[0]], - [shift store t ~by:5] is [\x. _[6] _[7] x[0]]. *) + For example, with term [t] being [\x. _[1] _[2] x[0]], + [shift store t ~by:5] is [\x. _[6] _[7] x[0]]. *) val abs_on : store -> var -> t -> t - (** [abs_on store v t] is the term [t[v := _[0]]]. It replaces [v] with - the bound variable with the same type as [v], and the DB index 0, - and takes care of shifting if [v] occurs under binders. + (** [abs_on store v t] is the term [t[v := _[0]]]. It replaces [v] with the + bound variable with the same type as [v], and the DB index 0, and takes + care of shifting if [v] occurs under binders. - For example, [abs_on store x (\y. x+y)] is [\y. _[1] y]. - *) + For example, [abs_on store x (\y. x+y)] is [\y. _[1] y]. *) end (**/**) @@ -188,8 +186,8 @@ module Internal_ : sig t val def_eq_ref : (store -> t -> t -> bool) ref - (** Definitional equality hook. Defaults to syntactic equality. - Overwritten by [Reduce] at init time. *) + (** Definitional equality hook. Defaults to syntactic equality. Overwritten by + [Reduce] at init time. *) end (**/**)