aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml33
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/context.mli10
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/names.ml21
-rw-r--r--kernel/nativecode.ml7
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/nativevalues.ml3
-rw-r--r--kernel/pre_env.ml18
-rw-r--r--kernel/reduction.ml29
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--kernel/uGraph.mli3
-rw-r--r--kernel/univ.ml4
-rw-r--r--kernel/vars.ml2
-rw-r--r--kernel/vars.mli4
18 files changed, 69 insertions, 80 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf50..eecceb32a7 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,7 +107,16 @@ type constr = t
type existential = existential_key * constr array
type rec_declaration = Name.t array * constr array * constr array
type fixpoint = (int array * int) * rec_declaration
+ (* The array of [int]'s tells for each component of the array of
+ mutual fixpoints the number of lambdas to skip before finding the
+ recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+ (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+ the recursive argument);
+ The second component [int] tells which component of the block is
+ returned *)
type cofixpoint = int * rec_declaration
+ (* The component [int] tells which component of the block of
+ cofixpoint is returned *)
type types = constr
@@ -115,7 +124,7 @@ type types = constr
(* Term constructors *)
(*********************)
-(* Constructs a DeBrujin index with number n *)
+(* Constructs a de Bruijn index with number n *)
let rels =
[|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8;
Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
@@ -978,28 +987,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash)
let case_info_hash = CaseinfoHash.hash
-module Hsorts =
- Hashcons.Make(
- struct
- open Sorts
-
- type t = Sorts.t
- type u = universe -> universe
- let hashcons huniv = function
- Prop c -> Prop c
- | Type u -> Type (huniv u)
- let eq s1 s2 =
- s1 == s2 ||
- match (s1,s2) with
- (Prop c1, Prop c2) -> c1 == c2
- | (Type u1, Type u2) -> u1 == u2
- |_ -> false
- let hash = function
- | Prop Null -> 0 | Prop Pos -> 1
- | Type u -> 2 + Universe.hash u
- end)
-
-(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
let hcons =
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 700c235e6a..e0954160f9 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -70,7 +70,7 @@ type types = constr
(** {6 Term constructors. } *)
-(** Constructs a DeBrujin index (DB indices begin at 1) *)
+(** Constructs a de Bruijn index (DB indices begin at 1) *)
val mkRel : int -> constr
(** Constructs a Variable *)
diff --git a/kernel/context.mli b/kernel/context.mli
index 0c666a25d9..24e69ebd6e 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -214,7 +214,7 @@ sig
val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt
end
- (** Rel-context is represented as a list of declarations.
+ (** Named-context is represented as a list of declarations.
Inner-most declarations are at the beginning of the list.
Outer-most declarations are at the end of the list. *)
type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
@@ -223,7 +223,7 @@ sig
(** empty named-context *)
val empty : ('c, 't) pt
- (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ (** Return a new named-context enriched by with a given inner-most declaration. *)
val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
(** Return the number of {e local declarations} in a given named-context. *)
@@ -233,7 +233,7 @@ sig
@raise Not_found if the designated identifier is not bound in a given named-context. *)
val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt
- (** Check whether given two rel-contexts are equal. *)
+ (** Check whether given two named-contexts are equal. *)
val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
(** Map all terms in a given named-context. *)
@@ -253,8 +253,8 @@ sig
(** Return the set of all identifiers bound in a given named-context. *)
val to_vars : ('c, 't) pt -> Id.Set.t
- (** [instance_from_named_context Ω] builds an instance [args] such
- that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+ (** [to_instance Ω] builds an instance [args] such
+ that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7821ea20ff..71e228b19c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -77,7 +77,7 @@ type typing_flags = {
}
(* some contraints are in constant_constraints, some other may be in
- * the OpaueDef *)
+ * the OpaqueDef *)
type constant_body = {
const_hyps : Context.Named.t; (** New: younger hyp at top *)
const_body : constant_def;
diff --git a/kernel/names.ml b/kernel/names.ml
index ee8d838da1..811b4a62a5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -162,21 +162,8 @@ module DirPath =
struct
type t = module_ident list
- let rec compare (p1 : t) (p2 : t) =
- if p1 == p2 then 0
- else begin match p1, p2 with
- | [], [] -> 0
- | [], _ -> -1
- | _, [] -> 1
- | id1 :: p1, id2 :: p2 ->
- let c = Id.compare id1 id2 in
- if Int.equal c 0 then compare p1 p2 else c
- end
-
- let rec equal p1 p2 = p1 == p2 || match p1, p2 with
- | [], [] -> true
- | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2
- | _ -> false
+ let compare = List.compare Id.compare
+ let equal = List.equal Id.equal
let rec hash accu = function
| [] -> accu
@@ -191,7 +178,7 @@ struct
let empty = []
- let is_empty d = match d with [] -> true | _ -> false
+ let is_empty = List.is_empty
let to_string = function
| [] -> "<>"
@@ -555,7 +542,6 @@ module KerPair = struct
end
module SyntacticOrd = struct
- type t = kernel_pair
let compare x y = match x, y with
| Same knx, Same kny -> KerName.compare knx kny
| Dual (knux,kncx), Dual (knuy,kncy) ->
@@ -878,7 +864,6 @@ struct
let hash (c, b) = (if b then 0 else 1) + Constant.hash c
module SyntacticOrd = struct
- type t = constant * bool
let compare (c, b) (c', b') =
if b = b' then Constant.SyntacticOrd.compare c c' else -1
let equal (c, b as x) (c', b' as x') =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 33bd7d8ddc..ba80ff590d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -16,6 +16,8 @@ open Nativeinstr
open Nativelambda
open Pre_env
+[@@@ocaml.warning "-32-37"]
+
(** This file defines the mllambda code generation phase of the native
compiler. mllambda represents a fragment of ML, and can easily be printed
to OCaml code. *)
@@ -1848,9 +1850,10 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
and compile_rel env sigma univ auxdefs n =
- let n = Context.Rel.length env.env_rel_context - n in
let open Context.Rel.Declaration in
- match Context.Rel.lookup n env.env_rel_context with
+ let decl = Context.Rel.lookup n env.env_rel_context in
+ let n = Context.Rel.length env.env_rel_context - n in
+ match decl with
| LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3c0afe3805..3593d94c2c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -141,7 +141,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- (* TODO change 0 when we can have deBruijn *)
+ (* TODO change 0 when we can have de Bruijn *)
fst (conv_val env pb 0 !rt1 !rt2 univs)
end
| _ -> anomaly (Pp.str "Compilation failure")
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 366f9a0a6d..fcb75c661e 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -16,6 +16,9 @@ open Nativeinstr
module RelDecl = Context.Rel.Declaration
+(* I'm not messing with this stuff. *)
+[@@@ocaml.warning "-32"]
+
(** This file defines the lambda code generation phase of the native compiler *)
exception NotClosed
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 965ed67b07..8d5f6388cb 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -334,6 +334,7 @@ let l_or accu x y =
if is_int x && is_int y then no_check_l_or x y
else accu x y
+[@@@ocaml.warning "-37"]
type coq_carry =
| Caccu of t
| C0 of t
@@ -430,7 +431,7 @@ let addmuldiv accu x y z =
if is_int x && is_int y && is_int z then no_check_addmuldiv x y z
else accu x y z
-
+[@@@ocaml.warning "-34"]
type coq_bool =
| Baccu of t
| Btrue
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index d14a254d32..48d7ee9ec3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -68,8 +68,8 @@ type named_context_val = {
}
type env = {
- env_globals : globals;
- env_named_context : named_context_val;
+ env_globals : globals; (* globals = constants + inductive types + modules + module-types *)
+ env_named_context : named_context_val; (* section variables *)
env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
@@ -161,19 +161,7 @@ let map_named_val f ctxt =
else { env_named_ctx = ctx; env_named_map = map }
let push_named d env =
-(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
- assert (env.env_rel_context = []); *)
- { env_globals = env.env_globals;
- env_named_context = push_named_context_val d env.env_named_context;
- env_rel_context = env.env_rel_context;
- env_rel_val = env.env_rel_val;
- env_nb_rel = env.env_nb_rel;
- env_stratification = env.env_stratification;
- env_typing_flags = env.env_typing_flags;
- env_conv_oracle = env.env_conv_oracle;
- retroknowledge = env.retroknowledge;
- indirect_pterms = env.indirect_pterms;
- }
+ {env with env_named_context = push_named_context_val d env.env_named_context}
let lookup_named id env =
fst (Id.Map.find id env.env_named_context.env_named_map)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d7f77edae..ba714ada20 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -107,7 +107,15 @@ let pure_stack lfts stk =
(****************************************************************************)
let whd_betaiota env t =
- whd_val (create_clos_infos betaiota env) (inject t)
+ match kind_of_term t with
+ | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+ Prod _|Lambda _|Fix _|CoFix _) -> t
+ | App (c, _) ->
+ begin match kind_of_term c with
+ | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
+ | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+ end
+ | _ -> whd_val (create_clos_infos betaiota env) (inject t)
let nf_betaiota env t =
norm_val (create_clos_infos betaiota env) (inject t)
@@ -116,18 +124,33 @@ let whd_betaiotazeta env x =
match kind_of_term x with
| (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> x
+ | App (c, _) ->
+ begin match kind_of_term c with
+ | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
+ | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ end
| _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
let whd_all env t =
match kind_of_term t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> t
+ | App (c, _) ->
+ begin match kind_of_term c with
+ | Ind _ | Construct _ | Evar _ | Meta _ -> t
+ | _ -> whd_val (create_clos_infos all env) (inject t)
+ end
| _ -> whd_val (create_clos_infos all env) (inject t)
let whd_allnolet env t =
match kind_of_term t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
+ | App (c, _) ->
+ begin match kind_of_term c with
+ | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
+ | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+ end
| _ -> whd_val (create_clos_infos allnolet env) (inject t)
(********************************************************************)
@@ -464,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (FInd (ind1,u1), FInd (ind2,u2)) ->
if eq_ind ind1 ind2
then
- (let cuniv = convert_instances false u1 u2 cuniv in
+ (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
else raise NotConvertible
| (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
if Int.equal j1 j2 && eq_ind ind1 ind2
then
- (let cuniv = convert_instances false u1 u2 cuniv in
+ (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
else raise NotConvertible
diff --git a/kernel/term.ml b/kernel/term.ml
index e5a681375d..03562d9f31 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -169,7 +169,7 @@ let hcons_types = Constr.hcons
exception DestKO
-(* Destructs a DeBrujin index *)
+(* Destructs a de Bruijn index *)
let destRel c = match kind_of_term c with
| Rel n -> n
| _ -> raise DestKO
diff --git a/kernel/term.mli b/kernel/term.mli
index a9bb677050..241ef322fa 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,7 +127,7 @@ val is_small : sorts -> bool
exception DestKO
-(** Destructs a DeBrujin index *)
+(** Destructs a de Bruijn index *)
val destRel : constr -> int
(** Destructs an existential variable *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f43b01d1bb..eeb9c421a1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -223,7 +223,7 @@ let rec unzip ctx j =
let feedback_completion_typecheck =
let open Feedback in
Option.iter (fun state_id ->
- feedback ~id:(State state_id) Feedback.Complete)
+ feedback ~id:state_id Feedback.Complete)
let infer_declaration ~trust env kn dcl =
match dcl with
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1cb..c8ac7df5c6 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -61,3 +61,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
val dump_universes :
(constraint_type -> string -> string -> unit) ->
universes -> unit
+
+(** {6 Debugging} *)
+val check_universes_invariants : universes -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09f884ecd0..afe9cbe8d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -440,10 +440,6 @@ struct
let set = make Level.set
let type1 = hcons (Level.set, 1)
- let is_prop = function
- | (l,0) -> Level.is_prop l
- | _ -> false
-
let is_small = function
| (l,0) -> Level.is_small l
| _ -> false
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4affb5f9fb..f1c0a4f08a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -27,7 +27,7 @@ let closedn n c =
in
try closed_rec n c; true with LocalOccur -> false
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
let closed0 c = closedn 0 c
diff --git a/kernel/vars.mli b/kernel/vars.mli
index adeac422e0..df5c55118f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -11,10 +11,10 @@ open Constr
(** {6 Occur checks } *)
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *)
val closedn : int -> constr -> bool
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
val closed0 : constr -> bool
(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:02:19 +0000