aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml4
-rw-r--r--kernel/cbytegen.mli3
-rw-r--r--kernel/clambda.ml4
-rw-r--r--kernel/clambda.mli3
-rw-r--r--kernel/constr.ml8
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/names.ml44
-rw-r--r--kernel/names.mli38
-rw-r--r--kernel/uGraph.ml15
-rw-r--r--kernel/uGraph.mli5
-rw-r--r--kernel/univ.ml15
-rw-r--r--kernel/univ.mli2
12 files changed, 88 insertions, 55 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 70dc6867ac..a771945dd2 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -829,6 +829,8 @@ let is_univ_copy max u =
else
false
+let dump_bytecode = ref false
+
let dump_bytecodes init code fvs =
let open Pp in
(str "code =" ++ fnl () ++
@@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
reloc, init_code
in
let fv = List.rev (!(reloc.in_env).fv_rev) in
- (if !Flags.dump_bytecode then
+ (if !dump_bytecode then
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive msg ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index abab58b60b..1c4cdcbeb4 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool ->
(** Shortcut of the previous function used during module strengthening *)
val compile_alias : Names.Constant.t -> body_code
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 7b637c20e6..641d424e2c 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -807,7 +807,7 @@ and lambda_of_args env start args =
(*********************************)
-
+let dump_lambda = ref false
let optimize_lambda lam =
let lam = simplify subst_id lam in
@@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c =
Renv.push_rels env (Array.of_list ids);
let lam = lambda_of_constr env c in
let lam = if optimize then optimize_lambda lam else lam in
- if !Flags.dump_lambda then
+ if !dump_lambda then
Feedback.msg_debug (pp_lam lam);
lam
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 89b7fd8e3b..6cf46163e3 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -25,3 +25,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda
(*spiwack: compiling function to insert dynamic decompilation before
matching integers (in case they are in processor representation) *)
val int31_escape_before_match : bool -> lambda -> lambda
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 4f062d72f0..bc486210df 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -654,7 +654,7 @@ let map_with_binders g f l c0 = match kind c0 with
let bl' = CArray.Fun1.smartmap f l' bl in
mkCoFix (ln,(lna,tl',bl'))
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
Univ.Instance.t -> Univ.Instance.t -> bool
type constr_compare_fn = int -> constr -> constr -> bool
@@ -692,10 +692,10 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
| Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
| Const (c1,u1), Const (c2,u2) ->
(* The args length currently isn't used but may as well pass it. *)
- Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2
- | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2
+ Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
+ | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2
| Construct (c1,u1), Construct (c2,u2) ->
- eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2
+ eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 0d464840c7..b35ea66536 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -413,7 +413,7 @@ val compare_head : constr_compare_fn -> constr_compare_fn
(** Convert a global reference applied to 2 instances. The int says
how many arguments are given (as we can only use cumulativity for
fully applied inductives/constructors) .*)
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
Univ.Instance.t -> Univ.Instance.t -> bool
(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
diff --git a/kernel/names.ml b/kernel/names.ml
index a3aa71f24f..58d311dd58 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -701,22 +701,6 @@ end
module Constrmap = Map.Make(ConstructorOrdered)
module Constrmap_env = Map.Make(ConstructorOrdered_env)
-type global_reference =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
-
-(* Better to have it here that in closure, since used in grammar.cma *)
-type evaluable_global_reference =
- | EvalVarRef of Id.t
- | EvalConstRef of Constant.t
-
-let eq_egr e1 e2 = match e1, e2 with
- EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
- | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
- | _, _ -> false
-
(** {6 Hash-consing of name objects } *)
module Hind = Hashcons.Make(
@@ -904,6 +888,34 @@ end
type projection = Projection.t
+module GlobRef = struct
+
+ type t =
+ | VarRef of variable (** A reference to the section-context. *)
+ | ConstRef of Constant.t (** A reference to the environment. *)
+ | IndRef of inductive (** A reference to an inductive type. *)
+ | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+
+ let equal gr1 gr2 =
+ gr1 == gr2 || match gr1,gr2 with
+ | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2
+ | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
+ | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
+ | VarRef v1, VarRef v2 -> Id.equal v1 v2
+ | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
+
+end
+
+type evaluable_global_reference =
+ | EvalVarRef of Id.t
+ | EvalConstRef of Constant.t
+
+(* Better to have it here that in closure, since used in grammar.cma *)
+let eq_egr e1 e2 = match e1, e2 with
+ EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
+ | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
+ | _, _ -> false
+
let constant_of_kn = Constant.make1
let constant_of_kn_equiv = Constant.make
let make_con = Constant.make3
diff --git a/kernel/names.mli b/kernel/names.mli
index 96e020aedd..566fcd0f91 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -500,21 +500,6 @@ val constructor_user_hash : constructor -> int
val constructor_syntactic_ord : constructor -> constructor -> int
val constructor_syntactic_hash : constructor -> int
-(** {6 Global reference is a kernel side type for all references together } *)
-type global_reference =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
-
-(** Better to have it here that in Closure, since required in grammar.cma *)
-type evaluable_global_reference =
- | EvalVarRef of Id.t
- | EvalConstRef of Constant.t
-
-val eq_egr : evaluable_global_reference -> evaluable_global_reference
- -> bool
-
(** {6 Hash-consing } *)
val hcons_con : Constant.t -> Constant.t
@@ -749,6 +734,29 @@ end
type projection = Projection.t
[@@ocaml.deprecated "Alias for [Projection.t]"]
+(** {6 Global reference is a kernel side type for all references together } *)
+
+(* XXX: Should we define GlobRefCan GlobRefUser? *)
+module GlobRef : sig
+
+ type t =
+ | VarRef of variable (** A reference to the section-context. *)
+ | ConstRef of Constant.t (** A reference to the environment. *)
+ | IndRef of inductive (** A reference to an inductive type. *)
+ | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+
+ val equal : t -> t -> bool
+
+end
+
+(** Better to have it here that in Closure, since required in grammar.cma *)
+(* XXX: Move to a module *)
+type evaluable_global_reference =
+ | EvalVarRef of Id.t
+ | EvalConstRef of Constant.t
+
+val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool
+
val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
[@@ocaml.deprecated "Same as [Constant.make]"]
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d1644614d..e6b27077ba 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -21,7 +21,7 @@ open Univ
(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
(* Universes are stratified by a partial ordering $\le$.
@@ -557,8 +557,7 @@ let get_explanation strict u v g =
else match traverse strict u with Some exp -> exp | None -> assert false
let get_explanation strict u v g =
- if !Flags.univ_print then Some (get_explanation strict u v g)
- else None
+ Some (lazy (get_explanation strict u v g))
(* To compare two nodes, we simply do a forward search.
We implement two improvements:
@@ -768,18 +767,18 @@ let normalize_universes g =
g.entries g
let constraints_of_universes g =
+ let module UF = Unionfind.Make (LSet) (LMap) in
+ let uf = UF.create () in
let constraints_of u v acc =
match v with
| Canonical {univ=u; ltle} ->
UMap.fold (fun v strict acc->
let typ = if strict then Lt else Le in
Constraint.add (u,typ,v) acc) ltle acc
- | Equiv v -> Constraint.add (u,Eq,v) acc
+ | Equiv v -> UF.union u v uf; acc
in
- UMap.fold constraints_of g.entries Constraint.empty
-
-let constraints_of_universes g =
- constraints_of_universes (normalize_universes g)
+ let csts = UMap.fold constraints_of g.entries Constraint.empty in
+ csts, UF.partition uf
(** [sort_universes g] builds a totally ordered universe graph. The
output graph should imply the input graph (and the implication
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index d4fba63fb3..cca2eb472b 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,10 @@ val empty_universes : t
val sort_universes : t -> t
-val constraints_of_universes : t -> Constraint.t
+(** [constraints_of_universes g] returns [csts] and [partition] where
+ [csts] are the non-Eq constraints and [partition] is the partition
+ of the universes into equivalence classes. *)
+val constraints_of_universes : t -> Constraint.t * LSet.t list
val check_subtype : AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ea3a522953..8e19fa4e52 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -541,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with
(* Universe inconsistency: error raised when trying to enforce a relation
that would create a cycle in the graph of universes. *)
-type univ_inconsistency = constraint_type * universe * universe * explanation option
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,make u,make v,p))
(* Constraints and sets of constraints. *)
@@ -1235,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) =
| Eq -> str"=" | Lt -> str"<" | Le -> str"<="
in
let reason = match p with
- | None | Some [] -> mt()
+ | None -> mt()
| Some p ->
- str " because" ++ spc() ++ pr_uni v ++
+ let p = Lazy.force p in
+ if p = [] then mt ()
+ else
+ str " because" ++ spc() ++ pr_uni v ++
prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
- p ++
+ p ++
(if Universe.equal (snd (List.last p)) u then mt() else
- (spc() ++ str "= " ++ pr_uni u))
+ (spc() ++ str "= " ++ pr_uni u))
in
str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
pr_rel o ++ spc() ++ pr_uni v ++ reason
diff --git a/kernel/univ.mli b/kernel/univ.mli
index aaed899bf4..b68bbdf359 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -205,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function
Constraint.t...
*)
type explanation = (constraint_type * Universe.t) list
-type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
+type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 19:25:43 +0000