aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml396
1 files changed, 246 insertions, 150 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c86a4e3e48..c894d96a78 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -28,7 +28,6 @@ open Names
open Evd
open Term
open Vars
-open Context
open Termops
open Reductionops
open Environ
@@ -37,17 +36,20 @@ open Typeops
open Globnames
open Nameops
open Evarutil
+open Evardefine
open Pretype_errors
open Glob_term
open Glob_ops
open Evarconv
open Pattern
open Misctypes
+open Sigma.Notations
+open Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
type ltac_var_map = {
ltac_constrs : var_map;
ltac_uconstrs : uconstr_var_map;
@@ -56,6 +58,8 @@ type ltac_var_map = {
}
type glob_constr_ltac_closure = ltac_var_map * glob_constr
type pure_open_constr = evar_map * constr
+type 'a delayed_open =
+ { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
(************************************************************************)
(* This concerns Cases *)
@@ -104,24 +108,59 @@ let search_guard ~tflags loc env possible_indexes fixdefs =
user_err_loc (loc,"search_guard", Pp.str errmsg)
with Found indexes -> indexes)
-(* To embed constr in glob_constr *)
-let ((constr_in : constr -> Dyn.t),
- (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
-
+(* To force universe name declaration before use *)
+
+let strict_universe_declarations = ref true
+let is_strict_universe_declarations () = !strict_universe_declarations
+
+let _ =
+ Goptions.(declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "strict universe declaration";
+ optkey = ["Strict";"Universe";"Declaration"];
+ optread = is_strict_universe_declarations;
+ optwrite = (:=) strict_universe_declarations })
+
+let _ =
+ Goptions.(declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "minimization to Set";
+ optkey = ["Universe";"Minimization";"ToSet"];
+ optread = Universes.is_set_minimization;
+ optwrite = (:=) Universes.set_minimization })
+
(** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd s =
+let interp_universe_level_name evd (loc,s) =
let names, _ = Universes.global_universe_names () in
- try
- let id = try Id.of_string s with _ -> raise Not_found in
- evd, Idmap.find id names
- with Not_found ->
- try let level = Evd.universe_of_name evd s in
- evd, level
- with Not_found ->
- new_univ_level_variable ~name:s univ_rigid evd
-
-let interp_universe evd = function
- | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
+ if CString.string_contains s "." then
+ match List.rev (CString.split '.' s) with
+ | [] -> anomaly (str"Invalid universe name " ++ str s)
+ | n :: dp ->
+ let num = int_of_string n in
+ let dp = DirPath.make (List.map Id.of_string dp) in
+ let level = Univ.Level.make dp num in
+ let evd =
+ try Evd.add_global_univ evd level
+ with UGraph.AlreadyDeclared -> evd
+ in evd, level
+ else
+ try
+ let level = Evd.universe_of_name evd s in
+ evd, level
+ with Not_found ->
+ try
+ let id = try Id.of_string s with _ -> raise Not_found in
+ evd, snd (Idmap.find id names)
+ with Not_found ->
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ~loc ~name:s univ_rigid evd
+ else user_err_loc (loc, "interp_universe_level_name",
+ Pp.(str "Undeclared universe: " ++ str s))
+
+let interp_universe ?loc evd = function
+ | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
evd, Univ.Universe.make l
| l ->
List.fold_left (fun (evd, u) l ->
@@ -129,15 +168,15 @@ let interp_universe evd = function
(evd', Univ.sup u (Univ.Universe.make l)))
(evd, Univ.Universe.type0m) l
-let interp_universe_level evd = function
- | None -> new_univ_level_variable univ_rigid evd
- | Some s -> interp_universe_level_name evd s
+let interp_universe_level loc evd = function
+ | None -> new_univ_level_variable ~loc univ_rigid evd
+ | Some (loc,s) -> interp_universe_level_name evd (loc,s)
-let interp_sort evd = function
+let interp_sort ?loc evd = function
| GProp -> evd, Prop Null
| GSet -> evd, Prop Pos
| GType n ->
- let evd, u = interp_universe evd n in
+ let evd, u = interp_universe ?loc evd n in
evd, Type u
let interp_elimination_sort = function
@@ -153,22 +192,25 @@ type inference_flags = {
expand_evars : bool
}
+let frozen_holes (sigma, sigma') =
+ (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
+
let pending_holes (sigma, sigma') =
let fold evk _ accu =
if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
in
Evd.fold_undefined fold sigma' Evar.Set.empty
-let apply_typeclasses env evdref pending fail_evar =
- let filter_pending evk = Evar.Set.mem evk pending in
+let apply_typeclasses env evdref frozen fail_evar =
+ let filter_frozen = frozen in
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
- then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk)
- else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk))
+ then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
+ else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
~split:true ~fail:fail_evar env !evdref;
if Flags.is_program_mode () then (* Try optionally solving the obligations *)
evdref := Typeclasses.resolve_typeclasses
- ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref
+ ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
let apply_inference_hook hook evdref pending =
evdref := Evar.Set.fold (fun evk sigma ->
@@ -189,9 +231,9 @@ let apply_heuristics env evdref fail_evar =
with e when Errors.noncritical e ->
let e = Errors.push e in if fail_evar then iraise e
-let check_typeclasses_instances_are_solved env current_sigma pending =
+let check_typeclasses_instances_are_solved env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
- apply_typeclasses env (ref current_sigma) pending true
+ apply_typeclasses env (ref current_sigma) frozen true
let check_extra_evars_are_solved env current_sigma pending =
Evar.Set.iter
@@ -203,26 +245,45 @@ let check_extra_evars_are_solved env current_sigma pending =
| _ ->
error_unsolvable_implicit loc env current_sigma evk None) pending
-let check_evars_are_solved env current_sigma pending =
- check_typeclasses_instances_are_solved env current_sigma pending;
+(* [check_evars] fails if some unresolved evar remains *)
+
+let check_evars env initial_sigma sigma c =
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (evk,_ as ev) ->
+ (match existential_opt_value sigma ev with
+ | Some c -> proc_rec c
+ | None ->
+ if not (Evd.mem initial_sigma evk) then
+ let (loc,k) = evar_source evk sigma in
+ match k with
+ | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+ | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None)
+ | _ -> Constr.iter proc_rec c
+ in proc_rec c
+
+let check_evars_are_solved env current_sigma frozen pending =
+ check_typeclasses_instances_are_solved env current_sigma frozen;
check_problems_are_solved env current_sigma;
check_extra_evars_are_solved env current_sigma pending
(* Try typeclasses, hooks, unification heuristics ... *)
let solve_remaining_evars flags env current_sigma pending =
+ let frozen = frozen_holes pending in
let pending = pending_holes pending in
let evdref = ref current_sigma in
- if flags.use_typeclasses then apply_typeclasses env evdref pending false;
+ if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
apply_inference_hook (Option.get flags.use_hook env) evdref pending;
if flags.use_unif_heuristics then apply_heuristics env evdref false;
- if flags.fail_evar then check_evars_are_solved env !evdref pending;
+ if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
!evdref
let check_evars_are_solved env current_sigma pending =
+ let frozen = frozen_holes pending in
let pending = pending_holes pending in
- check_evars_are_solved env current_sigma pending
+ check_evars_are_solved env current_sigma frozen pending
let process_inference_flags flags env initial_sigma (sigma,c) =
let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
@@ -279,9 +340,21 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
str"It cannot be used in a binder.")
else n
+let ltac_interp_name_env k0 lvar env =
+ (* envhd is the initial part of the env when pretype was called first *)
+ (* (in practice is is probably 0, but we have to grant the
+ specification of pretype which accepts to start with a non empty
+ rel_context) *)
+ (* tail is the part of the env enriched by pretyping *)
+ let n = Context.Rel.length (rel_context env) - k0 in
+ let ctxt,_ = List.chop n (rel_context env) in
+ let env = pop_rel_context n env in
+ let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
+ push_rel_context ctxt env
+
let invert_ltac_bound_name lvar env id0 id =
- let id = Id.Map.find id lvar.ltac_idents in
- try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ let id' = Id.Map.find id lvar.ltac_idents in
+ try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
with Not_found ->
errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
str " depends on pattern variable name " ++ pr_id id ++
@@ -294,17 +367,14 @@ let protected_get_type_of env sigma c =
(str "Cannot reinterpret " ++ quote (print_constr c) ++
str " in the current environment.")
-let pretype_id pretype loc env evdref lvar id =
+let pretype_id pretype k0 loc env evdref lvar id =
let sigma = !evdref in
(* Look for the binder of [id] *)
try
- let id =
- try Id.Map.find id lvar.ltac_idents
- with Not_found -> id
- in
let (n,_,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
+ let env = ltac_interp_name_env k0 lvar env in
(* Check if [id] is an ltac variable *)
try
let (ids,c) = Id.Map.find id lvar.ltac_constrs in
@@ -327,13 +397,15 @@ let pretype_id pretype loc env evdref lvar id =
with Not_found ->
(* Check if [id] is a ltac variable not bound to a term *)
(* and build a nice error message *)
- if Id.Map.mem id lvar.ltac_genargs then
+ if Id.Map.mem id lvar.ltac_genargs then begin
+ let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
user_err_loc (loc,"",
- str "Variable " ++ pr_id id ++ str " should be bound to a term.");
+ str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+ bound to a " ++ Geninterp.Val.pr typ ++ str ".")
+ end;
(* Check if [id] is a section or goal variable *)
try
- let (_,_,typ) = lookup_named id env in
- { uj_val = mkVar id; uj_type = typ }
+ { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) }
with Not_found ->
(* [id] not found, standard error message *)
error_var_not_found_loc loc id
@@ -344,37 +416,41 @@ let evar_kind_of_term sigma c =
(*************************************************************************)
(* Main pretyping function *)
-let interp_universe_level_name evd = function
+let interp_universe_level_name loc evd l =
+ match l with
| GProp -> evd, Univ.Level.prop
| GSet -> evd, Univ.Level.set
- | GType s -> interp_universe_level evd s
+ | GType s -> interp_universe_level loc evd s
let pretype_global loc rigid env evd gr us =
let evd, instance =
match us with
| None -> evd, None
| Some l ->
- let _, ctx = Universes.unsafe_constr_of_global gr in
- let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
- let len = Array.length arr in
- if len != List.length l then
- user_err_loc (loc, "pretype",
- str "Universe instance should have length " ++ int len)
- else
- let evd, l' = List.fold_left (fun (evd, univs) l ->
- let evd, l = interp_universe_level_name evd l in
+ let _, ctx = Universes.unsafe_constr_of_global gr in
+ let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+ let len = Array.length arr in
+ if len != List.length l then
+ user_err_loc (loc, "pretype",
+ str "Universe instance should have length " ++ int len)
+ else
+ let evd, l' = List.fold_left (fun (evd, univs) l ->
+ let evd, l = interp_universe_level_name loc evd l in
(evd, l :: univs)) (evd, []) l
- in
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
+ user_err_loc (loc, "pretype",
+ str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
in
- Evd.fresh_global ~rigid ?names:instance env evd gr
+ Evd.fresh_global ~loc ~rigid ?names:instance env evd gr
let pretype_ref loc evdref env ref us =
match ref with
| VarRef id ->
(* Section variable *)
- (try let (_,_,ty) = lookup_named id env in
- make_judge (mkVar id) ty
+ (try make_judge (mkVar id) (get_type (lookup_named id env))
with Not_found ->
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
@@ -386,29 +462,26 @@ let pretype_ref loc evdref env ref us =
let ty = Typing.unsafe_type_of env evd c in
make_judge c ty
-let judge_of_Type evd s =
- let evd, s = interp_universe evd s in
+let judge_of_Type loc evd s =
+ let evd, s = interp_universe ~loc evd s in
let judge =
{ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
in
evd, judge
-let pretype_sort evdref = function
+let pretype_sort loc evdref = function
| GProp -> judge_of_prop
| GSet -> judge_of_set
- | GType s -> evd_comb1 judge_of_Type evdref s
+ | GType s -> evd_comb1 (judge_of_Type loc) evdref s
let new_type_evar env evdref loc =
- let e, s =
- evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
- in e
-
-let get_projection env cst =
- let cb = lookup_constant cst env in
- match cb.Declarations.const_proj with
- | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} ->
- (cst,mind,n,m,ty)
- | None -> raise Not_found
+ let sigma = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma ((e, _), sigma, _) =
+ Evarutil.new_type_evar env sigma
+ univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
+ in
+ evdref := Sigma.to_evar_map sigma;
+ e
let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
@@ -416,16 +489,11 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
-let is_GHole = function
- | GHole _ -> true
- | _ -> false
-
-let evars = ref Id.Map.empty
-
-let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
- let pretype_type = pretype_type resolve_tc in
- let pretype = pretype resolve_tc in
+ let pretype_type = pretype_type k0 resolve_tc in
+ let pretype = pretype k0 resolve_tc in
+ let open Context.Rel.Declaration in
match t with
| GRef (loc,ref,u) ->
inh_conv_coerce_to_tycon loc env evdref
@@ -434,7 +502,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
| GVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
- (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
+ (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
tycon
| GEvar (loc, id, inst) ->
@@ -445,12 +513,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
with Not_found ->
user_err_loc (loc,"",str "Unknown existential variable.") in
let hyps = evar_filtered_context (Evd.find !evdref evk) in
- let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in
+ let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = (Retyping.get_judgment_of env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
| GPatVar (loc,(someta,n)) ->
+ let env = ltac_interp_name_env k0 lvar env in
let ty =
match tycon with
| Some ty -> ty
@@ -459,6 +528,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (loc, k, naming, None) ->
+ let env = ltac_interp_name_env k0 lvar env in
let ty =
match tycon with
| Some ty -> ty
@@ -467,6 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
{ uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
| GHole (loc, k, _naming, Some arg) ->
+ let env = ltac_interp_name_env k0 lvar env in
let ty =
match tycon with
| Some ty -> ty
@@ -482,14 +553,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
[] -> ctxt
| (na,bk,None,ty)::bl ->
let ty' = pretype_type empty_valcon env evdref lvar ty in
- let dcl = (na,None,ty'.utj_val) in
- type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+ let dcl = LocalAssum (na, ty'.utj_val) in
+ let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
+ type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
let ty' = pretype_type empty_valcon env evdref lvar ty in
let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
- let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
- type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
- let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+ let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
+ let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
+ type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
+ let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
let larj =
Array.map2
(fun e ar ->
@@ -516,7 +589,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
(* we lift nbfix times the type in tycon, because of
* the nbfix variables pushed to newenv *)
let (ctxt,ty) =
- decompose_prod_n_assum (rel_context_length ctxt)
+ decompose_prod_n_assum (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
let nenv = push_rel_context ctxt newenv in
let j = pretype (mk_tycon ty) nenv evdref lvar def in
@@ -560,7 +633,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
inh_conv_coerce_to_tycon loc env evdref fixj tycon
| GSort (loc,s) ->
- let j = pretype_sort evdref s in
+ let j = pretype_sort loc evdref s in
inh_conv_coerce_to_tycon loc env evdref j tycon
| GApp (loc,f,args) ->
@@ -631,7 +704,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
match evar_kind_of_term !evdref resj.uj_val with
| App (f,args) ->
let f = whd_evar !evdref f in
- if isInd f && is_template_polymorphic env f then
+ if is_template_polymorphic env f then
(* Special case for inductive type applications that must be
refreshed right away. *)
let sigma = !evdref in
@@ -660,9 +733,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
(* The name specified by ltac is used also to create bindings. So
the substitution must also be applied on variables before they are
looked up in the rel context. *)
- let name = ltac_interp_name lvar name in
- let var = (name,None,j.utj_val) in
+ let var = LocalAssum (name, j.utj_val) in
let j' = pretype rng (push_rel var env) evdref lvar c2 in
+ let name = ltac_interp_name lvar name in
let resj = judge_of_abstraction env (orelse_name name name') j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -671,7 +744,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
(* The name specified by ltac is used also to create bindings. So
the substitution must also be applied on variables before they are
looked up in the rel context. *)
- let name = ltac_interp_name lvar name in
let j' = match name with
| Anonymous ->
let j = pretype_type empty_valcon env evdref lvar c2 in
@@ -681,6 +753,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let env' = push_rel_assum var env in
pretype_type empty_valcon env' evdref lvar c2
in
+ let name = ltac_interp_name lvar name in
let resj =
try
judge_of_product env name j j'
@@ -698,14 +771,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
pretype (mk_tycon tj.utj_val) env evdref lvar c
| _ -> pretype empty_tycon env evdref lvar c1
in
- let t = j.uj_type in
+ let t = evd_comb1 (Evarsolve.refresh_universes
+ ~onlyalg:true ~status:Evd.univ_flexible (Some false) env)
+ evdref j.uj_type in
(* The name specified by ltac is used also to create bindings. So
the substitution must also be applied on variables before they are
looked up in the rel context. *)
- let name = ltac_interp_name lvar name in
- let var = (name,Some j.uj_val,t) in
+ let var = LocalDef (name, j.uj_val, t) in
let tycon = lift_tycon 1 tycon in
let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+ let name = ltac_interp_name lvar name in
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
@@ -725,27 +800,27 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
if not (Int.equal (List.length nal) cs.cs_nargs) then
user_err_loc (loc,"", str "Destructing let on this type expects " ++
int cs.cs_nargs ++ str " variables.");
- let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
- let na = ltac_interp_name lvar na in
let fsign, record =
match get_projections env indf with
- | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
- (List.rev nal) cs.cs_args, false
+ | None ->
+ List.map2 set_name (List.rev nal) cs.cs_args, false
| Some ps ->
let rec aux n k names l =
match names, l with
- | na :: names, ((_, None, t) :: l) ->
+ | na :: names, (LocalAssum (_,t) :: l) ->
let proj = Projection.make ps.(cs.cs_nargs - k) true in
- (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t)
+ LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
:: aux (n+1) (k + 1) names l
- | na :: names, ((_, c, t) :: l) ->
- (na, c, t) :: aux (n+1) k names l
+ | na :: names, (decl :: l) ->
+ set_name na decl :: aux (n+1) k names l
| [], [] -> []
| _ -> assert false
- in aux 1 1 (List.rev nal) cs.cs_args, true
- in
+ in aux 1 1 (List.rev nal) cs.cs_args, true in
let obj ind p v f =
if not record then
+ let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
+ let nal = List.rev nal in
+ let fsign = List.map2 set_name nal fsign in
let f = it_mkLambda_or_LetIn f fsign in
let ci = make_case_info env (fst ind) LetStyle in
mkCase (ci, p, cj.uj_val,[|f|])
@@ -756,10 +831,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let arsgn =
let arsgn,_ = get_arity env indf in
if not !allow_anonymous_refs then
- List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ List.map (set_name Anonymous) arsgn
else arsgn
in
- let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in
let nar = List.length arsgn in
(match po with
| Some p ->
@@ -815,11 +890,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let arsgn,_ = get_arity env indf in
if not !allow_anonymous_refs then
(* Make dependencies from arity signature impossible *)
- List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ List.map (set_name Anonymous) arsgn
else arsgn
in
let nar = List.length arsgn in
- let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in
let pred,p = match po with
| Some p ->
let env_p = push_rel_context psign env in
@@ -831,25 +906,24 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
| None ->
let p = match tycon with
| Some ty -> ty
- | None -> new_type_evar env evdref loc
+ | None ->
+ let env = ltac_interp_name_env k0 lvar env in
+ new_type_evar env evdref loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
let p = nf_evar !evdref p in
let f cs b =
- let n = rel_context_length cs.cs_args in
+ let n = Context.Rel.length cs.cs_args in
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
let csgn =
if not !allow_anonymous_refs then
- List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
+ List.map (set_name Anonymous) cs.cs_args
else
- List.map
- (fun (n, b, t) ->
- match n with
- Name _ -> (n, b, t)
- | Anonymous -> (Name Namegen.default_non_dependent_ident, b, t))
- cs.cs_args
+ List.map (map_name (function Name _ as n -> n
+ | Anonymous -> Name Namegen.default_non_dependent_ident))
+ cs.cs_args
in
let env_c = push_rel_context csgn env in
let bj = pretype (mk_tycon pi) env_c evdref lvar b in
@@ -867,9 +941,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
inh_conv_coerce_to_tycon loc env evdref cj tycon
| GCases (loc,sty,po,tml,eqns) ->
- let (tml,eqns) =
- Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns
- in
Cases.compile_cases loc sty
((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
tycon env (* loc *) (po,tml,eqns)
@@ -889,23 +960,20 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
if not (occur_existential cty || occur_existential tval) then
- begin
- try
- ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
- with Reduction.NotConvertible ->
- error_actual_type_loc loc env !evdref cj tval
+ let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
+ if b then (evdref := evd; cj)
+ else
+ error_actual_type_loc loc env !evdref cj tval
(ConversionFailed (env,cty,tval))
- end
else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
str "unresolved arguments remain.")
| NATIVEcast ->
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
- let evars = Nativenorm.evars_of_evar_map !evdref in
begin
- try
- ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj
- with Reduction.NotConvertible ->
+ let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
+ if b then (evdref := evd; cj)
+ else
error_actual_type_loc loc env !evdref cj tval
(ConversionFailed (env,cty,tval))
end
@@ -916,13 +984,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
{ uj_val = v; uj_type = tval }
in inh_conv_coerce_to_tycon loc env evdref cj tycon
-and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
- let f (id,_,t) (subst,update) =
- let t = replace_vars subst t in
+and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
+ let f decl (subst,update) =
+ let id = get_id decl in
+ let t = replace_vars subst (get_type decl) in
let c, update =
try
let c = List.assoc id update in
- let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in
+ let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
c.uj_val, List.remove_assoc id update
with Not_found ->
try
@@ -930,7 +999,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
if is_conv env !evdref t t' then mkRel n, update else raise Not_found
with Not_found ->
try
- let (_,_,t') = lookup_named id env in
+ let t' = lookup_named id env |> get_type in
if is_conv env !evdref t t' then mkVar id, update else raise Not_found
with Not_found ->
user_err_loc (loc,"",str "Cannot interpret " ++
@@ -942,7 +1011,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
Array.map_of_list snd subst
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type resolve_tc valcon env evdref lvar = function
+and pretype_type k0 resolve_tc valcon env evdref lvar = function
| GHole (loc, knd, naming, None) ->
(match valcon with
| Some v ->
@@ -958,11 +1027,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function
{ utj_val = v;
utj_type = s }
| None ->
+ let env = ltac_interp_name_env k0 lvar env in
let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
{ utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
utj_type = s})
| c ->
- let j = pretype resolve_tc empty_tycon env evdref lvar c in
+ let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
let loc = loc_of_glob_constr c in
let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
match valcon with
@@ -975,13 +1045,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function
let ise_pretype_gen flags env sigma lvar kind c =
let evdref = ref sigma in
+ let k0 = Context.Rel.length (rel_context env) in
let c' = match kind with
| WithoutTypeConstraint ->
- (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+ (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
| OfType exptyp ->
- (pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+ (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
| IsType ->
- (pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val
+ (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val
in
process_inference_flags flags env sigma (!evdref,c')
@@ -1016,14 +1087,16 @@ let on_judgment f j =
let understand_judgment env sigma c =
let evdref = ref sigma in
- let j = pretype true empty_tycon env evdref empty_lvar c in
+ let k0 = Context.Rel.length (rel_context env) in
+ let j = pretype k0 true empty_tycon env evdref empty_lvar c in
let j = on_judgment (fun c ->
let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in
evdref := evd; c) j
in j, Evd.evar_universe_context !evdref
let understand_judgment_tcc env evdref c =
- let j = pretype true empty_tycon env evdref empty_lvar c in
+ let k0 = Context.Rel.length (rel_context env) in
+ let j = pretype k0 true empty_tycon env evdref empty_lvar c in
on_judgment (fun c ->
let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
evdref := evd; c) j
@@ -1051,3 +1124,26 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W
let understand_ltac flags env sigma lvar kind c =
ise_pretype_gen flags env sigma lvar kind c
+
+let constr_flags = {
+ use_typeclasses = true;
+ use_unif_heuristics = true;
+ use_hook = None;
+ fail_evar = true;
+ expand_evars = true }
+
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = constr_flags)
+ ?(expected_type = WithoutTypeConstraint) ist c =
+ { delayed = begin fun env sigma ->
+ let { closure; term } = c in
+ let vars = {
+ ltac_constrs = closure.typed;
+ ltac_uconstrs = closure.untyped;
+ ltac_idents = closure.idents;
+ ltac_genargs = Id.Map.empty;
+ } in
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end }
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:07:02 +0000