diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/clenv.ml | 7 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 15 | ||||
-rw-r--r-- | pretyping/evd.mli | 4 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 13 | ||||
-rw-r--r-- | pretyping/retyping.ml | 15 | ||||
-rw-r--r-- | pretyping/retyping.mli | 3 | ||||
-rw-r--r-- | pretyping/termops.ml | 2 | ||||
-rw-r--r-- | pretyping/termops.mli | 2 | ||||
-rw-r--r-- | pretyping/unification.ml | 15 |
10 files changed, 47 insertions, 31 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 |