aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml13
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/cbv.ml1
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/detyping.ml9
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evarsolve.ml66
-rw-r--r--pretyping/glob_ops.ml5
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/nativenorm.ml24
-rw-r--r--pretyping/nativenorm.mli3
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/pretyping.mli6
-rw-r--r--pretyping/program.ml3
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/reductionops.ml41
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--pretyping/typeclasses.ml13
-rw-r--r--pretyping/typing.ml22
-rw-r--r--pretyping/typing.mli3
-rw-r--r--pretyping/unification.ml13
22 files changed, 144 insertions, 114 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 36f35a67c3..59ca418a39 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Globnames
-open Term
open Constr
open Context
open Environ
@@ -78,14 +77,14 @@ let rename_type ty ref =
let rec rename_type_aux c = function
| [] -> c
| rename :: rest as renamings ->
- match kind_of_type c with
- | ProdType (old, s, t) ->
+ match Constr.kind c with
+ | Prod (old, s, t) ->
mkProd (name_override old rename, s, rename_type_aux t rest)
- | LetInType(old, s, b, t) ->
+ | LetIn (old, s, b, t) ->
mkLetIn (old ,s, b, rename_type_aux t renamings)
- | CastType (t,_) -> rename_type_aux t renamings
- | SortType _ -> c
- | AtomicType _ -> c in
+ | Cast (t,_, _) -> rename_type_aux t renamings
+ | _ -> c
+ in
try rename_type_aux ty (arguments_names ref)
with Not_found -> ty
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cbd04a76ad..29d6726262 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid =
let IndType (indf, _) =
try find_rectype env sigma (lift (-(List.length realargs)) ty)
with Not_found -> error_case_not_inductive env sigma
- {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty}
+ {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty}
in
let (ind,u), params = dest_ind_family indf in
let params = List.map EConstr.of_constr params in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2b7ccbbcad..11c97221ec 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk =
let get_debug_cbv = Goptions.declare_bool_option_and_ref
~depr:false
~value:false
- ~name:"cbv visited constants display"
~key:["Debug";"Cbv"]
(* Reduction of primitives *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c7f9a8f00..c4aa3479bf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -36,7 +36,6 @@ open Globnames
let get_use_typeclasses_for_conversion =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"use typeclass resolution during conversion"
~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
~value:true
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 037006bc47..83078660c5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value
let () = declare_bool_option
{ optdepr = false;
- optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
optread = force_wildcard;
optwrite = (:=) wildcard_value }
@@ -237,7 +236,6 @@ let fast_name_generation = ref false
let () = declare_bool_option {
optdepr = false;
- optname = "fast bound name generation algorithm";
optkey = ["Fast";"Name";"Printing"];
optread = (fun () -> !fast_name_generation);
optwrite = (:=) fast_name_generation;
@@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
optread = synthetize_type;
optwrite = (:=) synth_type_value }
@@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
optread = reverse_matching;
optwrite = (:=) reverse_matching_value }
@@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value
let () = declare_bool_option
{ optdepr = false;
- optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
@@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "factorization of \"match\" patterns in printing";
optkey = ["Printing";"Factorizable";"Match";"Patterns"];
optread = (fun () -> !print_factorize_match_patterns);
optwrite = (fun b -> print_factorize_match_patterns := b) }
@@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "possible use of \"match\" default pattern in printing";
optkey = ["Printing";"Allow";"Match";"Default";"Clause"];
optread = (fun () -> !print_allow_match_default_clause);
optwrite = (fun b -> print_allow_match_default_clause := b) }
@@ -696,7 +689,7 @@ let detype_universe sigma u =
if Univ.Level.is_set l then GSet else
GType (hack_qualid_of_univ_level sigma l) in
(s, n) in
- Univ.Universe.map fn u
+ List.map fn (Univ.Universe.repr u)
let detype_sort sigma = function
| SProp -> UNamed [GSProp,0]
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3bd52088c7..c67019c7ac 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -50,8 +50,6 @@ let default_flags env =
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to Evarconv unification";
optkey = ["Debug";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
@@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option {
let debug_ho_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print higher-order unification debug information";
optkey = ["Debug";"HO";"Unification"];
optread = (fun () -> !debug_ho_unification);
optwrite = (fun a -> debug_ho_unification:=a);
@@ -269,7 +265,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let sk2 = Stack.append_app args sk2 in
lookup_canonical_conversion (proji, Const_cs c2), sk2
| _ ->
- let (c2, _) = Termops.global_of_constr sigma t2 in
+ let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
lookup_canonical_conversion (proji, Const_cs c2),sk2
with Not_found ->
let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b54a713a16..aafd662f7d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -311,21 +311,47 @@ let eq_alias a b = match a, b with
| VarAlias id1, VarAlias id2 -> Id.equal id1 id2
| _ -> false
-type aliasing = EConstr.t option * alias list
+type 'a aliasing = 'a option * alias list
let empty_aliasing = None, []
let make_aliasing c = Some c, []
let push_alias (alias, l) a = (alias, a :: l)
+
+module Alias =
+struct
+type t = { mutable lift : int; mutable data : EConstr.t }
+
+let make c = { lift = 0; data = c }
+
+let lift n { lift; data } = { lift = lift + n; data }
+
+let eval alias =
+ let c = EConstr.Vars.lift alias.lift alias.data in
+ let () = alias.lift <- 0 in
+ let () = alias.data <- c in
+ c
+
+let repr sigma alias = match EConstr.kind sigma alias.data with
+| Rel n -> Some (RelAlias (n + alias.lift))
+| Var id -> Some (VarAlias id)
+| _ -> None
+
+end
+
let lift_aliasing n (alias, l) =
let map a = match a with
| VarAlias _ -> a
| RelAlias m -> RelAlias (m + n)
in
- (Option.map (fun c -> lift n c) alias, List.map map l)
+ (Option.map (fun c -> Alias.lift n c) alias, List.map map l)
+
+let cast_aliasing (alias, l) = match alias with
+| None -> (None, l)
+| Some c -> (Some (Alias.make c), l)
type aliases = {
- rel_aliases : aliasing Int.Map.t;
- var_aliases : aliasing Id.Map.t;
+ rel_aliases : Alias.t aliasing Int.Map.t;
+ var_aliases : EConstr.t aliasing Id.Map.t;
(** Only contains [VarAlias] *)
}
@@ -359,13 +385,14 @@ let compute_rel_aliases var_aliases rels sigma =
| Var id' ->
let aliases_of_n =
try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in
- Int.Map.add n (push_alias aliases_of_n (VarAlias id')) aliases
+ Int.Map.add n (push_alias (cast_aliasing aliases_of_n) (VarAlias id')) aliases
| Rel p ->
let aliases_of_n =
try Int.Map.find (p+n) aliases with Not_found -> empty_aliasing in
Int.Map.add n (push_alias aliases_of_n (RelAlias (p+n))) aliases
| _ ->
- Int.Map.add n (make_aliasing (lift n (mkCast(t,DEFAULTcast,u)))) aliases)
+ let alias = Alias.lift n (Alias.make @@ mkCast(t,DEFAULTcast, u)) in
+ Int.Map.add n (make_aliasing alias) aliases)
| LocalAssum _ -> aliases)
)
rels
@@ -387,7 +414,7 @@ let lift_aliases n aliases =
let get_alias_chain_of sigma aliases x = match x with
| RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing)
- | VarAlias id -> (try Id.Map.find id aliases.var_aliases with Not_found -> empty_aliasing)
+ | VarAlias id -> (try cast_aliasing (Id.Map.find id aliases.var_aliases) with Not_found -> empty_aliasing)
let normalize_alias_opt_alias sigma aliases x =
match get_alias_chain_of sigma aliases x with
@@ -420,13 +447,14 @@ let extend_alias sigma decl { var_aliases; rel_aliases } =
| Var id' ->
let aliases_of_binder =
try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in
- Int.Map.add 1 (push_alias aliases_of_binder (VarAlias id')) rel_aliases
+ Int.Map.add 1 (push_alias (cast_aliasing aliases_of_binder) (VarAlias id')) rel_aliases
| Rel p ->
let aliases_of_binder =
try Int.Map.find (p+1) rel_aliases with Not_found -> empty_aliasing in
Int.Map.add 1 (push_alias aliases_of_binder (RelAlias (p+1))) rel_aliases
| _ ->
- Int.Map.add 1 (make_aliasing (lift 1 t)) rel_aliases)
+ let alias = Alias.lift 1 (Alias.make t) in
+ Int.Map.add 1 (make_aliasing alias) rel_aliases)
| LocalAssum _ -> rel_aliases in
{ var_aliases; rel_aliases }
@@ -434,7 +462,7 @@ let expand_alias_once sigma aliases x =
match get_alias_chain_of sigma aliases x with
| None, [] -> None
| Some a, [] -> Some a
- | _, l -> Some (of_alias (List.last l))
+ | _, l -> Some (Alias.make (of_alias (List.last l)))
let expansions_of_var sigma aliases x =
let (_, l) = get_alias_chain_of sigma aliases x in
@@ -442,9 +470,9 @@ let expansions_of_var sigma aliases x =
let expansion_of_var sigma aliases x =
match get_alias_chain_of sigma aliases x with
- | None, [] -> (false, of_alias x)
- | Some a, _ -> (true, a)
- | None, a :: _ -> (true, of_alias a)
+ | None, [] -> (false, Some x)
+ | Some a, _ -> (true, Alias.repr sigma a)
+ | None, a :: _ -> (true, Some a)
let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
| Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n))
@@ -482,10 +510,10 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
match ck with
| VarAlias id -> acc4 := Id.Set.add id !acc4
| RelAlias n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3);
- match EConstr.kind sigma c' with
- | Var id -> acc2 := Id.Set.add id !acc2
- | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
- | _ -> frec (aliases,depth) c end
+ match c' with
+ | Some (VarAlias id) -> acc2 := Id.Set.add id !acc2
+ | Some (RelAlias n) -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
+ | None -> frec (aliases,depth) c end
| Const _ | Ind _ | Construct _ ->
acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
| _ ->
@@ -971,7 +999,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
with Not_found ->
match expand_alias_once evd aliases t with
| None -> raise Not_found
- | Some c -> aux k (lift k c) in
+ | Some c -> aux k (Alias.eval (Alias.lift k c)) in
try
let c = aux 0 c_in_env_extended_with_k_binders in
Invertible (UniqueProjection (c,!effects))
@@ -1223,7 +1251,7 @@ let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t =
let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
match to_alias evd t with
| Some t ->
- let expanded, t' = expansion_of_var evd aliases t in
+ let expanded, _ = expansion_of_var evd aliases t in
if expanded then
(* t is a local definition, we keep it only if appears in the list *)
(* of let-in variables effectively occurring on the right-hand side, *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 02c2fc4a13..0969b3cc03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
- | Implicit, Implicit -> true
- | (Explicit | Implicit), _ -> false
+ | NonMaxImplicit, NonMaxImplicit -> true
+ | MaxImplicit, MaxImplicit -> true
+ | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
let case_style_eq s1 s2 = let open Constr in match s1, s2 with
| LetStyle, LetStyle -> true
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 44323441b6..485a19421d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
type cases_pattern = [ `any ] cases_pattern_g
-type binding_kind = Explicit | Implicit
+type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
(** Representation of an internalized (or in other words globalized) term. *)
type 'a glob_constr_r =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 36b405e981..816a8c4703 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -28,14 +28,14 @@ open Context.Rel.Declaration
let type_of_inductive env (ind,u) =
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
Inductive.type_of_inductive env (specif,u)
(* Return type as quoted by the user *)
let type_of_constructor env (cstr,u) =
let (mib,_ as specif) =
Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps;
Inductive.type_of_constructor (cstr,u) specif
(* Return constructor types in user form *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2db674d397..97fffbd7c8 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -26,6 +26,10 @@ open Context.Rel.Declaration
exception Find_at of int
+(* timing *)
+
+let timing_enabled = ref false
+
(* profiling *)
let profiling_enabled = ref false
@@ -79,6 +83,12 @@ let get_profiling_enabled () =
let set_profiling_enabled b =
profiling_enabled := b
+let get_timing_enabled () =
+ !timing_enabled
+
+let set_timing_enabled b =
+ timing_enabled := b
+
let invert_tag cst tag reloc_tbl =
try
for j = 0 to Array.length reloc_tbl - 1 do
@@ -496,19 +506,23 @@ let native_norm env sigma c ty =
let ml_filename, prefix = Nativelib.get_ml_filename () in
let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
let profile = get_profiling_enabled () in
+ let print_timing = get_timing_enabled () in
+ let tc0 = Sys.time () in
let fn = Nativelib.compile ml_filename code ~profile:profile in
- if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
+ let tc1 = Sys.time () in
+ let time_info = Format.sprintf "native_compute: Compilation done in %.5f@." (tc1 -. tc0) in
+ if print_timing then Feedback.msg_info (Pp.str time_info);
let profiler_pid = if profile then start_profiler () else None in
let t0 = Sys.time () in
Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd);
let t1 = Sys.time () in
if profile then stop_profiler profiler_pid;
- let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ let time_info = Format.sprintf "native_compute: Evaluation done in %.5f@." (t1 -. t0) in
+ if print_timing then Feedback.msg_info (Pp.str time_info);
let res = nf_val env sigma !Nativelib.rt1 ty in
let t2 = Sys.time () in
- let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ let time_info = Format.sprintf "native_compute: Reification done in %.5f@." (t2 -. t1) in
+ if print_timing then Feedback.msg_info (Pp.str time_info);
EConstr.of_constr res
let native_conv_generic pb sigma t =
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 02de034fcb..458fe70e2c 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -20,6 +20,9 @@ val set_profile_filename : string -> unit
val get_profiling_enabled : unit -> bool
val set_profiling_enabled : bool -> unit
+val get_timing_enabled : unit -> bool
+val set_timing_enabled : bool -> unit
+
val native_norm : env -> evar_map -> constr -> types -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bf61d44a10..ac1a4e88ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,7 @@ open Evarconv
module NamedDecl = Context.Named.Declaration
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint
let (!!) env = GlobEnv.env env
@@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix =
let is_strict_universe_declarations =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"strict universe declaration"
~key:["Strict";"Universe";"Declaration"]
~value:true
@@ -446,7 +445,7 @@ let pretype_ref ?loc sigma env ref us =
Pretype_errors.error_var_not_found ?loc !!env sigma id)
| ref ->
let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
- let ty = unsafe_type_of !!env sigma c in
+ let sigma, ty = type_of !!env sigma c in
sigma, make_judge c ty
let interp_sort ?loc evd : glob_sort -> _ = function
@@ -1290,7 +1289,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
in
let env = GlobEnv.make ~hypnaming env sigma lvar in
let sigma', c', c'_ty = match kind with
- | WithoutTypeConstraint ->
+ | WithoutTypeConstraint | UnknownIfTermOrType ->
let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18e416596e..ee57f690a1 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
val search_guard :
?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint =
+ | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *)
+ | IsType (** Necessarily a type *)
+ | OfType of types (** A term of the expected type *)
+ | WithoutTypeConstraint (** A term of unknown expected type *)
type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..9c478844aa 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -78,7 +78,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "preferred transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
@@ -86,7 +85,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program cases";
optkey = ["Program";"Cases"];
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
@@ -94,7 +92,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program generalized coercion";
optkey = ["Program";"Generalized";"Coercion"];
optread = (fun () -> !program_generalized_coercion);
optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3b918b5396..879c007198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,7 +189,7 @@ let rec cs_pattern_of_constr env t =
let _, params = Inductive.find_rectype env ty in
Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
- | _ -> Const_cs (Globnames.global_of_constr t) , None, []
+ | _ -> Const_cs (fst @@ destRef t) , None, []
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
@@ -234,7 +234,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
((GlobRef.ConstRef proji_sp, (patt, t)),
{ o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
- | exception Not_found ->
+ | exception DestKO ->
if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
acc
) acc spopt
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4d4fe13983..bfee07e7f0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -32,8 +32,6 @@ exception Elimconst
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Generate weak constraints between Irrelevant universes";
optkey = ["Cumulativity";"Weak";"Constraints"];
optread = (fun () -> not !UState.drop_weak_constraints);
optwrite = (fun a -> UState.drop_weak_constraints:=not a);
@@ -722,32 +720,31 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
let open UnivProblem in
- try
- let (cst_mod,_) = Constant.repr2 reference in
- let cst = Constant.make2 cst_mod (Label.of_id id) in
+ let (cst_mod,_) = Constant.repr2 reference in
+ let cst = Constant.make2 cst_mod (Label.of_id id) in
+ if not (Environ.mem_constant cst env) then bd
+ else
let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
match constant_opt_value_in env (cst,u) with
| None -> bd
| Some t ->
let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
begin match csts with
- | Some csts ->
- let subst = Set.fold (fun cst acc ->
- let l, r = match cst with
- | ULub (u, v) | UWeak (u, v) -> u, v
- | UEq (u, v) | ULe (u, v) ->
- let get u = Option.get (Universe.level u) in
- get u, get v
- in
- Univ.LMap.add l r acc)
- csts Univ.LMap.empty
- in
- let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
- mkConstU (cst, EInstance.make inst)
- | None -> bd
+ | Some csts ->
+ let subst = Set.fold (fun cst acc ->
+ let l, r = match cst with
+ | ULub (u, v) | UWeak (u, v) -> u, v
+ | UEq (u, v) | ULe (u, v) ->
+ let get u = Option.get (Universe.level u) in
+ get u, get v
+ in
+ Univ.LMap.add l r acc)
+ csts Univ.LMap.empty
+ in
+ let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+ mkConstU (cst, EInstance.make inst)
+ | None -> bd
end
- with
- | Not_found -> bd
let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
let nbodies = Array.length bodies in
@@ -973,8 +970,6 @@ module CredNative = RedNative(CNativeEntries)
let debug_RAKAM = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states of the Reductionops abstract machine";
optkey = ["Debug";"RAKAM"];
optread = (fun () -> !debug_RAKAM);
optwrite = (fun a -> debug_RAKAM:=a);
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 10e8cf7e0f..4afed07eda 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
let pattern_occs loccs_trm = begin fun env sigma c ->
let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
try
- let _ = Typing.unsafe_type_of env sigma abstr_trm in
+ let sigma, _ = Typing.type_of env sigma abstr_trm in
(sigma, applist(abstr_trm, List.map snd loccs_trm))
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
@@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
error_cannot_recognize ref
| _ ->
- try
- if GlobRef.equal (fst (global_of_constr sigma c)) ref
- then it_mkProd_or_LetIn t l
- else raise Not_found
- with Not_found ->
+ if isRefX sigma ref c
+ then it_mkProd_or_LetIn t l
+ else
try
let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
elimrec env t' l
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..aa2e96c2d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
let get_typeclasses_unique_solutions =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"check that typeclasses proof search returns unique solutions"
~key:["Typeclasses";"Unique";"Solutions"]
~value:false
@@ -107,9 +106,9 @@ let class_info env sigma c =
not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
let global_class_of_constr env sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.find gr !classes, u
- with Not_found -> not_a_class env sigma c
+ with DestKO | Not_found -> not_a_class env sigma c
let dest_class_app env sigma c =
let cl, args = EConstr.decompose_app sigma c in
@@ -125,9 +124,9 @@ let class_of_constr env sigma c =
with e when CErrors.noncritical e -> None
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
@@ -140,9 +139,9 @@ let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_maybe_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index a15134f58d..b4c19775a7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -27,6 +27,8 @@ open Arguments_renaming
open Pretype_errors
open Context.Rel.Declaration
+module GR = Names.GlobRef
+
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
@@ -253,6 +255,9 @@ let judge_of_type u =
let judge_of_relative env v =
Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
+let type_of_variable env id =
+ EConstr.of_constr (type_of_variable env id)
+
let judge_of_variable env id =
Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
@@ -284,37 +289,36 @@ let judge_of_letin env name defj typj j =
{ uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ;
uj_type = subst1 defj.uj_val j.uj_type }
-let check_hyps_inclusion env sigma f x hyps =
+let check_hyps_inclusion env sigma x hyps =
let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
- let f x = EConstr.Unsafe.to_constr (f x) in
- Typeops.check_hyps_inclusion env ~evars f x hyps
+ Typeops.check_hyps_inclusion env ~evars x hyps
let type_of_constant env sigma (c,u) =
let open Declarations in
let cb = Environ.lookup_constant c env in
- let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+ let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Environ.constant_type env (c,u) in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c)))
let type_of_inductive env sigma (ind,u) =
let open Declarations in
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
let type_of_constructor env sigma ((ind,_ as ctor),u) =
let open Declarations in
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor)))
let judge_of_int env v =
Environ.on_judgment EConstr.of_constr (judge_of_int env v)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1b07b2bb78..fd2dc7c2fc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
(** Typecheck a term has a given type (assuming the type is OK) *)
val check : env -> evar_map -> constr -> types -> evar_map
+(** Type of a variable. *)
+val type_of_variable : env -> variable -> types
+
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6486435ca2..5b87603d54 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname = "Unification is keyed";
optkey = ["Keyed";"Unification"];
optread = (fun () -> !keyed_unification);
optwrite = (fun a -> keyed_unification:=a);
@@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to tactic unification";
optkey = ["Debug";"Tactic";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
@@ -1274,12 +1271,14 @@ let applyHead env evd n c =
else
match EConstr.kind evd (whd_all env evd cty) with
| Prod (_,c1,c2) ->
- let (evd',evar) =
- Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
- apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+ let (evd,evar) =
+ Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1
+ in
+ apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd
| _ -> user_err Pp.(str "Apply_Head_Then")
in
- apprec n c (Typing.unsafe_type_of env evd c) evd
+ let evd, t = Typing.type_of env evd c in
+ apprec n c t evd
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:07:36 +0000