From 93f3964d1110b8d858f069751aba5d51f32a686e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 15 Mar 2026 04:27:32 +0000 Subject: [PATCH] update ciclib+format --- src/ciclib/const.mli | 2 +- src/ciclib/level.mli | 11 +++++------ src/ciclib/term.ml | 12 ++++++------ src/ciclib/term.mli | 32 ++++++++++++++++---------------- 4 files changed, 28 insertions(+), 29 deletions(-) diff --git a/src/ciclib/const.mli b/src/ciclib/const.mli index 5c81332d..1bb0b5f1 100644 --- a/src/ciclib/const.mli +++ b/src/ciclib/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_ diff --git a/src/ciclib/level.mli b/src/ciclib/level.mli index 7cec98fc..4840dde9 100644 --- a/src/ciclib/level.mli +++ b/src/ciclib/level.mli @@ -39,16 +39,15 @@ val subst : subst -> t -> t (** {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 : 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 : 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 : t -> bool (** [judge_is_zero st l] is [true] iff [l <= 0] holds *) diff --git a/src/ciclib/term.ml b/src/ciclib/term.ml index dd34d4be..86af3df6 100644 --- a/src/ciclib/term.ml +++ b/src/ciclib/term.ml @@ -190,9 +190,9 @@ let db_shift_ (e : term) (n : int) = map_shallow e ~f:(fun inbind u -> loop u (if inbind then - k + 1 - else - k)) + k + 1 + else + k)) ) in assert (n >= 0); @@ -225,9 +225,9 @@ let db_replace_ e (env : t list) : term = map_shallow e ~f:(fun inb u -> aux u (if inb then - k + 1 - else - k)) + k + 1 + else + k)) ) in if is_closed e then diff --git a/src/ciclib/term.mli b/src/ciclib/term.mli index e033db17..97c71881 100644 --- a/src/ciclib/term.mli +++ b/src/ciclib/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_ @@ -41,9 +41,9 @@ val as_type : t -> Level.t option val as_type_exn : t -> Level.t 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 : f:(bool -> t -> t) -> t -> t val exists_shallow : f:(bool -> t -> bool) -> t -> bool @@ -53,8 +53,8 @@ val is_type : t -> bool (** [is_type t] is true iff [view t] is [Type _] *) 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) *) (** {2 Creation} *) @@ -75,8 +75,8 @@ val subst_level : Level.subst -> t -> t (** De bruijn indices *) module DB : sig val subst_db0 : 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])]. *) @@ -84,9 +84,9 @@ module DB : sig val subst_db_l : t -> t list -> t val shift : t -> by:int -> t - (** [shift t ~by] shifts all bound variables in [t] that are not - closed on, by amount [by] (which must be >= 0). + (** [shift 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 t ~by:5] is [\x. _[6] _[7] x[0]]. *) + For example, with term [t] being [\x. _[1] _[2] x[0]], [shift t ~by:5] is + [\x. _[6] _[7] x[0]]. *) end