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.ml12
-rw-r--r--pretyping/cbv.ml1
-rw-r--r--pretyping/coercion.ml146
-rw-r--r--pretyping/coercion.mli12
-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.ml6
-rw-r--r--pretyping/nativenorm.ml24
-rw-r--r--pretyping/nativenorm.mli3
-rw-r--r--pretyping/pretyping.ml118
-rw-r--r--pretyping/pretyping.mli6
-rw-r--r--pretyping/program.ml3
-rw-r--r--pretyping/recordops.ml67
-rw-r--r--pretyping/recordops.mli10
-rw-r--r--pretyping/reductionops.ml43
-rw-r--r--pretyping/reductionops.mli12
-rw-r--r--pretyping/retyping.ml16
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--pretyping/typeclasses.ml13
-rw-r--r--pretyping/typing.ml31
-rw-r--r--pretyping/typing.mli3
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/vnorm.ml2
27 files changed, 400 insertions, 254 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 aa6ec1c941..29d6726262 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
| exception Evarconv.UnableToUnify _ -> sigma, current
| sigma -> sigma, current
else
- let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
+ let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
sigma, j.uj_val
in
sigma, (current, try_find_ind !!(pb.env) sigma indt names))
@@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
match tycon with
- | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma
- ~flags:(default_flags_of TransparentState.full) j p
+ | Some p ->
+ let (evd,v,_trace) =
+ Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma
+ ~flags:(default_flags_of TransparentState.full) j p
+ in
+ (evd,v)
| None -> sigma, j
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
@@ -2160,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 c980d204ca..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
@@ -136,20 +135,6 @@ let lift_args n sign =
in
liftrec (List.length sign) sign
-let mu env evdref t =
- let rec aux v =
- let v' = hnf env !evdref v in
- match disc_subset !evdref v' with
- | Some (u, p) ->
- let f, ct = aux u in
- let p = hnf_nodelta env !evdref p in
- (Some (fun x ->
- app_opt env evdref
- f (papp evdref sig_proj1 [| u; p; x |])),
- ct)
- | None -> (None, v)
- in aux t
-
let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
: (EConstr.constr -> EConstr.constr) option
=
@@ -367,36 +352,97 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
+type coercion_trace =
+ | IdCoe
+ | PrimProjCoe of {
+ proj : Projection.Repr.t;
+ args : econstr list;
+ previous : coercion_trace;
+ }
+ | Coe of {
+ head : econstr;
+ args : econstr list;
+ previous : coercion_trace;
+ }
+ | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace }
+
+let empty_coercion_trace = IdCoe
+
+(* similar to iterated apply_coercion_args *)
+let rec reapply_coercions sigma trace c = match trace with
+ | IdCoe -> c
+ | PrimProjCoe { proj; args; previous } ->
+ let c = reapply_coercions sigma previous c in
+ let args = args@[c] in
+ let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in
+ applist (mkProj (Projection.make proj false, head), args)
+ | Coe {head; args; previous} ->
+ let c = reapply_coercions sigma previous c in
+ let args = args@[c] in
+ applist (head, args)
+ | ProdCoe { na; ty; dom; body } ->
+ let x = reapply_coercions sigma dom (mkRel 1) in
+ let c = beta_applist sigma (lift 1 c, [x]) in
+ let c = reapply_coercions sigma body c in
+ mkLambda (na, ty, c)
+
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
- let j,t,evd =
+ let j,t,trace,evd =
List.fold_left
- (fun (ja,typ_cl,sigma) i ->
+ (fun (ja,typ_cl,trace,sigma) i ->
let isid = i.coe_is_identity in
let isproj = i.coe_is_projection in
let sigma, c = new_global sigma i.coe_value in
let typ = Retyping.get_type_of env sigma c in
let fv = make_judge c typ in
- let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
- let sigma, jres =
- apply_coercion_args env sigma true isproj argl fv
+ let argl = class_args_of env sigma typ_cl in
+ let trace =
+ if isid then trace
+ else match isproj with
+ | None -> Coe {head=fv.uj_val;args=argl;previous=trace}
+ | Some proj ->
+ let args = List.skipn (Projection.Repr.npars proj) argl in
+ PrimProjCoe {proj; args; previous=trace }
in
- (if isid then
+ let argl = argl@[ja.uj_val] in
+ let sigma, jres = apply_coercion_args env sigma true isproj argl fv in
+ let jres =
+ if isid then
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
else
- jres),
- jres.uj_type,sigma)
- (hj,typ_cl,sigma) p
- in evd, j
+ jres
+ in
+ jres, jres.uj_type, trace, sigma)
+ (hj,typ_cl,IdCoe,sigma) p
+ in evd, j, trace
+
+let mu env evdref t =
+ let rec aux v =
+ let v' = hnf env !evdref v in
+ match disc_subset !evdref v' with
+ | Some (u, p) ->
+ let f, ct, trace = aux u in
+ let p = hnf_nodelta env !evdref p in
+ let p1 = delayed_force sig_proj1 in
+ let evd, p1 = Evarutil.new_global !evdref p1 in
+ evdref := evd;
+ (Some (fun x ->
+ app_opt env evdref
+ f (mkApp (p1, [| u; p; x |]))),
+ ct,
+ Coe {head=p1; args=[u;p]; previous=trace})
+ | None -> (None, v, IdCoe)
+ in aux t
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core ~program_mode env evd j =
let t = whd_all env evd j.uj_type in
match EConstr.kind evd t with
- | Prod _ -> (evd,j)
+ | Prod _ -> (evd,j,IdCoe)
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product env evd ev in
- (evd',{ uj_val = j.uj_val; uj_type = t })
+ (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe)
| _ ->
try let t,p =
lookup_path_to_fun_from env evd j.uj_type in
@@ -405,11 +451,11 @@ let inh_app_fun_core ~program_mode env evd j =
if program_mode then
try
let evdref = ref evd in
- let coercef, t = mu env evdref t in
+ let coercef, t, trace = mu env evdref t in
let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
- (!evdref, res)
+ (!evdref, res, trace)
with NoSubtacCoercion | NoCoercion ->
- (evd,j)
+ (evd,j,IdCoe)
else raise NoCoercion
(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
@@ -417,10 +463,10 @@ let inh_app_fun ~program_mode resolve_tc env evd j =
try inh_app_fun_core ~program_mode env evd j
with
| NoCoercion when not resolve_tc
- || not (get_use_typeclasses_for_conversion ()) -> (evd, j)
+ || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe)
| NoCoercion ->
try inh_app_fun_core ~program_mode env (saturate_evd env evd) j
- with NoCoercion -> (evd, j)
+ with NoCoercion -> (evd, j, IdCoe)
let type_judgment env sigma j =
match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -430,7 +476,7 @@ let type_judgment env sigma j =
let inh_tosort_force ?loc env evd j =
try
let t,p = lookup_path_to_sort_from env evd j.uj_type in
- let evd,j1 = apply_coercion env evd p j t in
+ let evd,j1,_trace = apply_coercion env evd p j t in
let j2 = Environ.on_judgment_type (whd_evar evd) j1 in
(evd,type_judgment env evd j2)
with Not_found | NoCoercion ->
@@ -449,7 +495,7 @@ let inh_coerce_to_sort ?loc env evd j =
let inh_coerce_to_base ?loc ~program_mode env evd j =
if program_mode then
let evdref = ref evd in
- let ct, typ' = mu env evdref j.uj_type in
+ let ct, typ', trace = mu env evdref j.uj_type in
let res =
{ uj_val = (app_coercion env evdref ct j.uj_val);
uj_type = typ' }
@@ -459,7 +505,7 @@ let inh_coerce_to_base ?loc ~program_mode env evd j =
let inh_coerce_to_prod ?loc ~program_mode env evd t =
if program_mode then
let evdref = ref evd in
- let _, typ' = mu env evdref t in
+ let _, typ', _trace = mu env evdref t in
!evdref, typ'
else (evd, t)
@@ -468,24 +514,24 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 =
then
raise NoCoercion
else
- let evd, v', t' =
+ let evd, v', t', trace =
try
let t2,t1,p = lookup_path_between env evd (t,c1) in
- let evd,j =
+ let evd,j,trace =
apply_coercion env evd p
{uj_val = v; uj_type = t} t2
in
- evd, j.uj_val, j.uj_type
+ evd, j.uj_val, j.uj_type, trace
with Not_found -> raise NoCoercion
in
- try (unify_leq_delay ~flags env evd t' c1, v')
+ try (unify_leq_delay ~flags env evd t' c1, v', trace)
with UnableToUnify _ -> raise NoCoercion
let default_flags_of env =
default_flags_of TransparentState.full
let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 =
- try (unify_leq_delay ~flags env evd t c1, v)
+ try (unify_leq_delay ~flags env evd t c1, v, IdCoe)
with UnableToUnify (best_failed_evd,e) ->
try inh_coerce_to_fail flags env evd rigidonly v t c1
with NoCoercion ->
@@ -505,24 +551,27 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid
| na -> na) name in
let open Context.Rel.Declaration in
let env1 = push_rel (LocalAssum (name,u1)) env in
- let (evd', v1) =
+ let (evd', v1, trace1) =
inh_conv_coerce_to_fail ?loc env1 evd rigidonly
(mkRel 1) (lift 1 u1) (lift 1 t1) in
let v2 = beta_applist evd' (lift 1 v,[v1]) in
let t2 = Retyping.get_type_of env1 evd' v2 in
- let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
- (evd'', mkLambda (name, u1, v2'))
+ let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
+ let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in
+ (evd'', mkLambda (name, u1, v2'), trace)
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t =
- let (evd', val') =
+ let (evd', val', otrace) =
try
- inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t
+ let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in
+ (evd', val', Some trace)
with NoCoercionNoUnifier (best_failed_evd,e) ->
try
if program_mode then
- coerce_itf ?loc env evd cj.uj_val cj.uj_type t
+ let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in
+ (evd', val', None)
else raise NoSubtacCoercion
with
| NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
@@ -533,11 +582,12 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd
if evd' == evd then
error_actual_type ?loc env best_failed_evd cj t e
else
- inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t
+ let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in
+ (evd', val', Some trace)
with NoCoercionNoUnifier (_evd,_error) ->
error_actual_type ?loc env best_failed_evd cj t e
in
- (evd',{ uj_val = val'; uj_type = t })
+ (evd',{ uj_val = val'; uj_type = t },otrace)
let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) =
inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index fe93a26f4f..b92f3709cc 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -16,13 +16,19 @@ open Glob_term
(** {6 Coercions. } *)
+type coercion_trace
+
+val empty_coercion_trace : coercion_trace
+
+val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t
+
(** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type a product; it returns [j] if no coercion is applicable.
resolve_tc=false disables resolving type classes (as the last
resort before failing) *)
val inh_app_fun : program_mode:bool -> bool ->
- env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment * coercion_trace
(** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
@@ -48,11 +54,11 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
env -> evar_map -> ?flags:Evarconv.unify_flags ->
- unsafe_judgment -> types -> evar_map * unsafe_judgment
+ unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
env -> evar_map -> ?flags:Evarconv.unify_flags ->
- unsafe_judgment -> types -> evar_map * unsafe_judgment
+ unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
(** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
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..a4406aeba1 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;
- Inductive.type_of_inductive env (specif,u)
+ Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
+ Inductive.type_of_inductive (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 bfdb471c46..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
@@ -361,7 +360,7 @@ let adjust_evar_source sigma na c =
(* coerce to tycon if any *)
let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function
- | None -> sigma, j
+ | None -> sigma, j, Some Coercion.empty_coercion_trace
| Some t ->
Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
@@ -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
@@ -604,16 +603,18 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
module Default =
struct
+ let discard_trace (sigma,t,otrace) = sigma, t
+
let pretype_ref self (ref, u) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
let sigma, t_ref = pretype_ref ?loc sigma env ref u in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon
let pretype_var self id =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in
let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
(* Ne faudrait-il pas s'assurer que hyps est bien un
@@ -626,7 +627,7 @@ struct
let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = Retyping.get_judgment_of !!env sigma c in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma =
let sigma, ty =
@@ -757,12 +758,12 @@ struct
iraise (e, info));
make_judge (mkCoFix cofix) ftys.(i)
in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon
let pretype_sort self s =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
let sigma, j = pretype_sort ?loc sigma s in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
let pretype_app self (f, args) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -771,12 +772,15 @@ struct
let floc = loc_of_glob_constr f in
let length = List.length args in
let nargs_before_bidi =
+ if Option.is_empty tycon then length
+ (* We apply bidirectionality hints only if an expected type is specified *)
+ else
(* if `f` is a global, we retrieve bidirectionality hints *)
- try
- let (gr,_) = destRef sigma fj.uj_val in
- Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints
- with DestKO ->
- length
+ try
+ let (gr,_) = destRef sigma fj.uj_val in
+ Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints
+ with DestKO ->
+ length
in
let candargs =
(* Bidirectional typechecking hint:
@@ -813,24 +817,38 @@ struct
else fun f v -> applist (f, [v])
| _ -> fun _ f v -> applist (f, [v])
in
- let rec apply_rec env sigma n resj candargs bidiargs = function
- | [] -> sigma, resj, List.rev bidiargs
+ let refresh_template env sigma resj =
+ (* Special case for inductive type applications that must be
+ refreshed right away. *)
+ match EConstr.kind sigma resj.uj_val with
+ | App (f,args) ->
+ if Termops.is_template_polymorphic_ind !!env sigma f then
+ let c = mkApp (f, args) in
+ let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
+ let t = Retyping.get_type_of !!env sigma c in
+ sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
+ else sigma, resj
+ | _ -> sigma, resj
+ in
+ let rec apply_rec env sigma n resj resj_before_bidi candargs bidiargs = function
+ | [] -> sigma, resj, resj_before_bidi, List.rev bidiargs
| c::rest ->
let bidi = n >= nargs_before_bidi in
let argloc = loc_of_glob_constr c in
- let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
+ let sigma, resj, trace = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
let resty = whd_all !!env sigma resj.uj_type in
match EConstr.kind sigma resty with
| Prod (na,c1,c2) ->
- let tycon = Some c1 in
let (sigma, hj), bidiargs =
- if bidi && Option.has_some tycon then
+ if bidi then
(* We want to get some typing information from the context before
typing the argument, so we replace it by an existential
variable *)
let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in
- (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs
- else pretype tycon env sigma c, bidiargs
+ (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs
+ else
+ let tycon = Some c1 in
+ pretype tycon env sigma c, bidiargs
in
let sigma, candargs, ujval =
match candargs with
@@ -845,29 +863,18 @@ struct
in
let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in
let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
- let j = { uj_val = value; uj_type = typ } in
- apply_rec env sigma (n+1) j candargs bidiargs rest
+ let resj = { uj_val = value; uj_type = typ } in
+ let resj_before_bidi = if bidi then resj_before_bidi else resj in
+ apply_rec env sigma (n+1) resj resj_before_bidi candargs bidiargs rest
| _ ->
let sigma, hj = pretype empty_tycon env sigma c in
error_cant_apply_not_functional
?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
in
- let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in
- let sigma, resj =
- match EConstr.kind sigma resj.uj_val with
- | App (f,args) ->
- if Termops.is_template_polymorphic_ind !!env sigma f then
- (* Special case for inductive type applications that must be
- refreshed right away. *)
- let c = mkApp (f, args) in
- let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
- let t = Retyping.get_type_of !!env sigma c in
- sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
- else sigma, resj
- | _ -> sigma, resj
- in
- let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
- let refine_arg sigma (newarg,origarg) =
+ let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in
+ let sigma, resj = refresh_template env sigma resj in
+ let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
+ let refine_arg n (sigma,t) (newarg,origarg,trace) =
(* Refine an argument (originally `origarg`) represented by an evar
(`newarg`) to use typing information from the context *)
(* Recover the expected type of the argument *)
@@ -876,12 +883,25 @@ struct
let sigma, j = pretype (Some ty) env sigma origarg in
(* Unify the (possibly refined) existential variable with the
(typechecked) original value *)
- Evarconv.unify_delay !!env sigma newarg (j_val j)
+ let sigma = Evarconv.unify_delay !!env sigma newarg (j_val j) in
+ sigma, app_f n (Coercion.reapply_coercions sigma trace t) (j_val j)
in
(* We now refine any arguments whose typing was delayed for
bidirectionality *)
- let sigma = List.fold_left refine_arg sigma bidiargs in
- (sigma, t)
+ let t = resj_before_bidi.uj_val in
+ let sigma, t = List.fold_left_i refine_arg nargs_before_bidi (sigma,t) bidiargs in
+ (* If we did not get a coercion trace (e.g. with `Program` coercions, we
+ replaced user-provided arguments with inferred ones. Otherwise, we apply
+ the coercion trace to the user-provided arguments. *)
+ let resj =
+ match otrace with
+ | None -> resj
+ | Some trace ->
+ let resj = { resj with uj_val = t } in
+ let sigma, resj = refresh_template env sigma resj in
+ { resj with uj_val = Coercion.reapply_coercions sigma trace t }
+ in
+ (sigma, resj)
let pretype_lambda self (name, bk, c1, c2) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -903,7 +923,7 @@ struct
let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in
let name = get_name var' in
let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
let pretype_prod self (name, bk, c1, c2) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -929,7 +949,7 @@ struct
let (e, info) = CErrors.push e in
let info = Option.cata (Loc.add_loc info) info loc in
iraise (e, info) in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
let pretype_letin self (name, c1, t, c2) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1122,7 +1142,7 @@ struct
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
let cj = { uj_val = v; uj_type = p } in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
let pretype_cast self (c, k) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1165,7 +1185,7 @@ struct
in
let v = mkCast (cj.uj_val, k, tval) in
sigma, { uj_val = v; uj_type = tval }
- in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
+ in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
let pretype_int self i =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1174,7 +1194,7 @@ struct
with Invalid_argument _ ->
user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
let pretype_float self f =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1183,7 +1203,7 @@ struct
with Invalid_argument _ ->
user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.")
in
- inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+ discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
(* [pretype_type valcon env sigma c] coerces [c] into a type *)
let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with
@@ -1269,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 35e182840b..879c007198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open CErrors
open Util
open Pp
open Names
-open Globnames
open Constr
open Mod_subst
open Reductionops
@@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) =
(Option.Smart.map (subst_constant subst))
projs
in
- let id' = subst_constructor subst id in
+ let id' = Globnames.subst_constructor subst id in
if projs' == projs && id' == id then obj else
(id',kl,projs')
@@ -139,7 +138,7 @@ let find_primitive_projection c =
*)
type obj_typ = {
- o_ORIGIN : Constant.t;
+ o_ORIGIN : GlobRef.t;
o_DEF : constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option; (* position of trivial argument if any *)
@@ -190,13 +189,13 @@ 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 (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"
- (fun (sign,env,t,con,proji_sp) ->
+ (fun (sign,env,t,ref,proji_sp) ->
let env = Termops.push_rels_assum sign env in
- let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in
+ let con_pp = Nametab.pr_global_env Id.Set.empty ref in
let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in
let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
@@ -204,11 +203,17 @@ let warn_projection_no_head_constant =
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
(* Intended to always succeed *)
-let compute_canonical_projections env ~warn (con,ind) =
- let o_CTX = Environ.constant_context env con in
- let u = Univ.make_abstract_instance o_CTX in
- let o_DEF = mkConstU (con, u) in
- let c = Environ.constant_value_in env (con,u) in
+let compute_canonical_projections env ~warn (gref,ind) =
+ let o_CTX = Environ.universes_of_global env gref in
+ let o_DEF, c =
+ match gref with
+ | GlobRef.ConstRef con ->
+ let u = Univ.make_abstract_instance o_CTX in
+ mkConstU (con, u), Environ.constant_value_in env (con,u)
+ | GlobRef.VarRef id ->
+ mkVar id, Option.get (Environ.named_body id env)
+ | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false
+ in
let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let t = EConstr.Unsafe.to_constr t in
@@ -227,10 +232,10 @@ let compute_canonical_projections env ~warn (con,ind) =
match cs_pattern_of_constr nenv t with
| patt, o_INJ, o_TCOMPS ->
((GlobRef.ConstRef proji_sp, (patt, t)),
- { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+ { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
- | exception Not_found ->
- if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+ | exception DestKO ->
+ if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
acc
) acc spopt
else acc
@@ -266,12 +271,17 @@ let register_canonical_structure ~warn env sigma o =
warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
)
-let subst_canonical_structure subst (cst,ind as obj) =
+type cs = GlobRef.t * inductive
+
+let subst_canonical_structure subst (gref,ind as obj) =
(* invariant: cst is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
- let cst' = subst_constant subst cst in
- let ind' = subst_ind subst ind in
- if cst' == cst && ind' == ind then obj else (cst',ind')
+ match gref with
+ | GlobRef.ConstRef cst ->
+ let cst' = subst_constant subst cst in
+ let ind' = subst_ind subst ind in
+ if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind')
+ | _ -> assert false
(*s High-level declaration of a canonical structure *)
@@ -282,15 +292,20 @@ let error_not_structure ref description =
description))
let check_and_decompose_canonical_structure env sigma ref =
- let sp =
+ let vc =
match ref with
- GlobRef.ConstRef sp -> sp
- | _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
+ | GlobRef.ConstRef sp ->
+ let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
+ begin match Environ.constant_opt_value_in env (sp, u) with
+ | Some vc -> vc
+ | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+ | GlobRef.VarRef id ->
+ begin match Environ.named_body id env with
+ | Some b -> b
+ | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+ | GlobRef.IndRef _ | GlobRef.ConstructRef _ ->
+ error_not_structure ref (str "Expected an instance of a record or structure.")
in
- let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
- let vc = match Environ.constant_opt_value_in env (sp, u) with
- | Some vc -> vc
- | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
let body = EConstr.Unsafe.to_constr body in
let f,args = match kind body with
@@ -308,7 +323,7 @@ let check_and_decompose_canonical_structure env sigma ref =
let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
- (sp,indsp)
+ (ref,indsp)
let lookup_canonical_conversion (proj,pat) =
assoc_pat pat (GlobRef.Map.find proj !object_table)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index aaba7cc3e5..fd156adc2c 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -73,7 +73,7 @@ type cs_pattern =
| Default_cs
type obj_typ = {
- o_ORIGIN : Constant.t;
+ o_ORIGIN : GlobRef.t;
o_DEF : constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option; (** position of trivial argument *)
@@ -87,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
val pr_cs_pattern : cs_pattern -> Pp.t
+type cs = GlobRef.t * inductive
+
val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
- Constant.t * inductive -> unit
-val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive
+ cs -> unit
+val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
val is_open_canonical_projection :
Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit ->
((GlobRef.t * cs_pattern) * obj_typ) list
-val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive
+val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4d4fe13983..838bf22c66 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);
@@ -1712,7 +1707,7 @@ let splay_arity env sigma c =
let l, c = splay_prod env sigma c in
match EConstr.kind sigma c with
| Sort s -> l,s
- | _ -> invalid_arg "splay_arity"
+ | _ -> raise Reduction.NotArity
let sort_of_arity env sigma c = snd (splay_arity env sigma c)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e72f5f2793..c539ec55ed 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr
val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
+val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr
+
val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t
+(** Raises [Reduction.NotArity] *)
+
val sort_of_arity : env -> evar_map -> constr -> ESorts.t
+(** Raises [Reduction.NotArity] *)
+
val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
-val splay_prod_assum :
- env -> evar_map -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
type 'a miota_args = {
mP : constr; (** the result type *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d2af957b54..87fe4cfcda 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma =
| _ -> decomp_sort env sigma (type_of env t)
and type_of_global_reference_knowing_parameters env c args =
- let argtyps =
- Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
match EConstr.kind sigma c with
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
let mip = lookup_mind_specif env ind in
- EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
- ~polyprop env (mip, u) argtyps
- with Reduction.NotArity -> retype_error NotAnArity)
+ let paramtyps = Array.map_to_list (fun arg () ->
+ let t = type_of env arg in
+ let s = try Reductionops.sort_of_arity env sigma t
+ with Reduction.NotArity -> retype_error NotAnArity
+ in
+ Sorts.univ_of_sort (ESorts.kind sigma s))
+ args
+ in
+ EConstr.of_constr
+ (Inductive.type_of_inductive_knowing_parameters
+ ~polyprop (mip, u) paramtyps)
| Construct (cstr, u) ->
let u = EInstance.kind sigma u in
EConstr.of_constr (type_of_constructor env (cstr, u))
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..f067c075bf 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
@@ -36,8 +38,11 @@ let meta_type evd mv =
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
- let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
- Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+ let paramstyp = Array.map_to_list (fun j () ->
+ let s = Reductionops.sort_of_arity env sigma j.uj_type in
+ Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl
+ in
+ Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
let type_judgment env sigma j =
match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -253,6 +258,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 +292,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 ty, csts = Inductive.constrained_type_of_inductive (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 48d5fac321..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
@@ -1290,7 +1289,7 @@ let is_mimick_head sigma ts f =
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
- let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
+ let (evd',j',_trace) = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
(evd',j'.uj_val)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 885fc8980d..b04e59734d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
let type_of_ind env (ind, u) =
- type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
+ type_of_inductive (Inductive.lookup_mind_specif env ind, u)
let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
let rtbl = mip.mind_reloc_tbl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:11:17 +0000