aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/clenv.ml7
-rw-r--r--pretyping/evarutil.ml2
-rw-r--r--pretyping/evd.ml15
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/reductionops.ml13
-rw-r--r--pretyping/retyping.ml15
-rw-r--r--pretyping/retyping.mli3
-rw-r--r--pretyping/termops.ml2
-rw-r--r--pretyping/termops.mli2
-rw-r--r--pretyping/unification.ml15
-rw-r--r--tactics/refine.ml5
-rw-r--r--toplevel/command.ml2
12 files changed, 52 insertions, 33 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 05c64521a..69b5db5e6 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -62,8 +62,7 @@ let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
-let clenv_get_type_of ce c =
- Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) (metas_of ce.evd) c
+let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
@@ -135,10 +134,10 @@ let clenv_conv_leq env sigma t c bound =
let mk_clenv_from_env environ sigma n (c,cty) =
let evd = create_goal_evar_defs sigma in
- let (env,args,concl) = clenv_environments evd n cty in
+ let (evd,args,concl) = clenv_environments evd n cty in
{ templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
templtyp = mk_freelisted concl;
- evd = env;
+ evd = evd;
env = environ }
let mk_clenv_from_n gls n (c,cty) =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3511db6e4..d455ec6fe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1146,7 +1146,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
let evc = nf_isevar evd evi.evar_concl in
match evi.evar_body with
| Evar_defined body ->
- let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evd (metas_of evd) body) in
+ let ty = nf_isevar evd (Retyping.get_type_of evenv evd body) in
add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
| Evar_empty -> (* Resulted in a constraint *)
evd
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 79bbbf10e..0f2f4655b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -630,15 +630,24 @@ let meta_defined evd mv =
| Clval _ -> true
| Cltyp _ -> false
-let meta_fvalue evd mv =
+let try_meta_fvalue evd mv =
match Metamap.find mv evd.metas with
| Clval(_,b,_) -> b
- | Cltyp _ -> anomaly "meta_fvalue: meta has no value"
-
+ | Cltyp _ -> raise Not_found
+
+let meta_fvalue evd mv =
+ try try_meta_fvalue evd mv
+ with Not_found -> anomaly "meta_fvalue: meta has no value"
+
+let meta_value evd mv =
+ (fst (try_meta_fvalue evd mv)).rebus
+
let meta_ftype evd mv =
match Metamap.find mv evd.metas with
| Cltyp (_,b) -> b
| Clval(_,_,b) -> b
+
+let meta_type evd mv = (meta_ftype evd mv).rebus
let meta_declare mv v ?(name=Anonymous) evd =
{ evd with metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 406914440..e5cf8e269 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -209,9 +209,11 @@ val meta_list : evar_defs -> (metavariable * clbinding) list
val meta_defined : evar_defs -> metavariable -> bool
(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
meta has no value *)
+val meta_value : evar_defs -> metavariable -> constr
val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status
val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option
-val meta_ftype : evar_defs -> metavariable -> constr freelisted
+val meta_type : evar_defs -> metavariable -> types
+val meta_ftype : evar_defs -> metavariable -> types freelisted
val meta_name : evar_defs -> metavariable -> name
val meta_with_name : evar_defs -> identifier -> metavariable
val meta_declare :
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 38ac3485b..859f8bb21 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -145,6 +145,10 @@ let rec whd_app_state sigma (x, stack as s) =
| _ -> s)
| _ -> s
+let safe_meta_value sigma ev =
+ try Some (Evd.meta_value sigma ev)
+ with Not_found -> None
+
let appterm_of_stack (f,s) = (f,list_of_stack s)
let whd_stack sigma x =
@@ -319,6 +323,10 @@ let rec whd_state_gen flags env sigma =
(match safe_evar_value sigma ev with
| Some body -> whrec (body, stack)
| None -> s)
+ | Meta ev ->
+ (match safe_meta_value sigma ev with
+ | Some body -> whrec (body, stack)
+ | None -> s)
| Const const when red_delta flags ->
(match constant_opt_value env const with
| Some body -> whrec (body, stack)
@@ -409,6 +417,11 @@ let local_whd_state_gen flags sigma =
Some c -> whrec (c,stack)
| None -> s)
+ | Meta ev ->
+ (match safe_meta_value sigma ev with
+ Some c -> whrec (c,stack)
+ | None -> s)
+
| x -> s
in
whrec
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3323c75b4..eeee0c313 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -44,11 +44,11 @@ let type_of_var env id =
with Not_found ->
anomaly ("type_of: variable "^(string_of_id id)^" unbound")
-let retype sigma metamap =
+let retype sigma =
let rec type_of env cstr=
match kind_of_term cstr with
| Meta n ->
- (try strip_outer_cast (List.assoc n metamap)
+ (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
| Rel n ->
let (_,_,ty) = lookup_rel n env in
@@ -140,10 +140,10 @@ let retype sigma metamap =
in type_of, sort_of, sort_family_of,
type_of_global_reference_knowing_parameters
-let get_sort_of env sigma t = let _,f,_,_ = retype sigma [] in f env t
-let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c
+let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t
+let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c
let type_of_global_reference_knowing_parameters env sigma c args =
- let _,_,_,f = retype sigma [] in f env c args
+ let _,_,_,f = retype sigma in f env c args
let type_of_global_reference_knowing_conclusion env sigma c conclty =
let conclty = nf_evar sigma conclty in
@@ -162,10 +162,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
(* We are outside the kernel: we take fresh universes *)
(* to avoid tactics and co to refresh universes themselves *)
let get_type_of env sigma c =
- let f,_,_,_ = retype sigma [] in refresh_universes (f env c)
-
-let get_type_of_with_meta env sigma metamap c =
- let f,_,_,_ = retype sigma metamap in refresh_universes (f env c)
+ let f,_,_,_ = retype sigma in refresh_universes (f env c)
(* Makes an assumption from a constr *)
let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 52e5d7049..be42fd858 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -25,9 +25,6 @@ val get_type_of : env -> evar_map -> constr -> types
val get_sort_of : env -> evar_map -> types -> sorts
val get_sort_family_of : env -> evar_map -> types -> sorts_family
-val get_type_of_with_meta :
- env -> evar_map -> Termops.meta_type_map -> constr -> types
-
(* Makes an assumption from a constr *)
val get_assumption_of : env -> evar_map -> constr -> types
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a49f27ac5..b7a4fc925 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1074,7 +1074,7 @@ let assums_of_rel_context sign =
| None -> (na, t)::l)
sign ~init:[]
-let fold_map_rel_context f env sign =
+let map_rel_context_in_env f env sign =
let rec aux env acc = function
| d::sign ->
aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index efa31b124..f9d432907 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -267,7 +267,7 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
val assums_of_rel_context : rel_context -> (name * constr) list
val lift_rel_context : int -> rel_context -> rel_context
val substl_rel_context : constr list -> rel_context -> rel_context
-val fold_map_rel_context :
+val map_rel_context_in_env :
(env -> constr -> constr) -> env -> rel_context -> rel_context
val map_rel_context_with_binders :
(int -> constr -> constr) -> rel_context -> rel_context
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4134f89b2..0b3eedcb8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -485,22 +485,21 @@ let w_coerce_to_type env evd c cty mvty =
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
- let cty = get_type_of_with_meta env ( evd) (metas_of evd) c in
+ let cty = get_type_of env evd c in
let mvty = Typing.meta_type evd mv in
w_coerce_to_type env evd c cty mvty
let unify_to_type env evd flags c u =
let sigma = evd in
let c = refresh_universes c in
- let t = get_type_of_with_meta env sigma (metas_of evd) c in
+ let t = get_type_of env sigma c in
let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
- try unify_0 env sigma Cumul flags t u
- with e when precatchable_exception e -> ([],[])
+ unify_0 env sigma Cumul flags t u
let unify_type env evd flags mv c =
let mvty = Typing.meta_type evd mv in
- if occur_meta_or_existential mvty then
+ if occur_meta_or_existential mvty or is_arity env evd mvty then
unify_to_type env evd flags c mvty
else ([],[])
@@ -593,7 +592,7 @@ let w_merge env with_types flags (metas,evars) evd =
let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =
unify_0 sp_env ( evd') Cumul flags
- (Retyping.get_type_of_with_meta sp_env ( evd') (metas_of evd') c) ev.evar_concl in
+ (Retyping.get_type_of sp_env evd' c) ev.evar_concl in
let evd'' = w_merge_rec evd' mc ec [] in
if ( evd') == ( evd'')
then Evd.define sp c evd''
@@ -621,8 +620,8 @@ let check_types env evd flags subst m n =
if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
unify_0_with_initial_metas subst true env ( evd) topconv
flags
- (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
- (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
+ (Retyping.get_type_of env sigma m)
+ (Retyping.get_type_of env sigma n)
else
subst
diff --git a/tactics/refine.ml b/tactics/refine.ml
index e37ffaf09..1a61c982b 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -101,7 +101,10 @@ let replace_by_meta env sigma = function
| Lambda (Anonymous,c1,c2) when isCast c2 ->
let _,_,t = destCast c2 in mkArrow c1 t
| _ -> (* (App _ | Case _) -> *)
- Retyping.get_type_of_with_meta env sigma mm c
+ let sigma' =
+ List.fold_right (fun (m,t) sigma -> Evd.meta_declare m t sigma)
+ mm sigma in
+ Retyping.get_type_of env sigma' c
(*
| Fix ((_,j),(v,_,_)) ->
v.(j) (* en pleine confiance ! *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 70087ecbf..6e000bc74 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1132,7 +1132,7 @@ let look_for_mutual_statements thms =
let n = List.length thms in
let inds = List.map (fun (id,(t,_) as x) ->
let (hyps,ccl) = decompose_prod_assum t in
- let whnf_hyp_hds = fold_map_rel_context
+ let whnf_hyp_hds = map_rel_context_in_env
(fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
(Global.env()) hyps in
let ind_hyps =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 01:14:54 +0000