diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 17 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 6 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 1 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 16 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
6 files changed, 30 insertions, 22 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a65cc24ff6..99e3c4e1d6 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -354,7 +354,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, @@ -411,12 +411,11 @@ let clenv_unify_binding_type clenv c t u = | e when precatchable_exception e -> TypeNotProcessed, clenv, c -let clenv_assign_binding clenv k (sigma,c) = +let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let clenv' = { clenv with evd = Evd.merge clenv.evd sigma} in - let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in - let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in - { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } + let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in + { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd } let clenv_match_args bl clenv = if bl = [] then @@ -425,13 +424,13 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,b,(sigma,c as sc)) -> + (fun clenv (loc,b,c) -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else - clenv_assign_binding clenv k sc) + clenv_assign_binding clenv k c) clenv bl let clenv_constrain_last_binding c clenv = @@ -439,7 +438,7 @@ let clenv_constrain_last_binding c clenv = let k = try list_last all_mvs with Failure _ -> anomaly "clenv_constrain_with_bindings" in - clenv_assign_binding clenv k (Evd.empty,c) + clenv_assign_binding clenv k c let clenv_constrain_dep_args hyps_only bl clenv = if bl = [] then diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 5571efbc57..4f7ac40920 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -86,7 +86,7 @@ val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to @@ -107,10 +107,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (* the optional int tells how many prods of the lemma have to be used *) (* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int option -> constr * constr -> open_constr bindings -> + evar_info sigma -> int option -> constr * constr -> constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> open_constr bindings -> clausenv + evar_info sigma -> constr * constr -> constr bindings -> clausenv (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where [lmetas] is a list of metas to be applied to a proof of [t] so that diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index dc1784f40c..a33c81b097 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1241,6 +1241,15 @@ let check_evars env initial_sigma evd c = | _ -> iter_constr proc_rec c in proc_rec c +(* This returns the evars of [sigma] that are not in [sigma0] and + [sigma] minus these evars *) + +let subtract_evars sigma0 sigma = + Evd.fold (fun evk ev (sigma,sigma' as acc) -> + if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else + (Evd.remove sigma evk,Evd.add sigma' evk ev)) + sigma (sigma,Evd.empty) + (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr @@ -1376,4 +1385,3 @@ let pr_tycon_type env (abs, t) = let pr_tycon env = function None -> str "None" | Some t -> pr_tycon_type env t - diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4bfef79983..205ca8bd64 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -90,6 +90,7 @@ val solve_simple_eqn : new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_map -> constr -> unit +val subtract_evars : evar_map -> evar_map -> evar_map * evar_map val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5bc868894..b741c9a413 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -703,9 +703,9 @@ let plain_instance s c = empty map). *) -let instance s c = +let instance sigma s c = (* if s = [] then c else *) - local_strong whd_betaiota Evd.empty (plain_instance s c) + local_strong whd_betaiota sigma (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -902,21 +902,21 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv in valrec mv -let meta_instance env b = +let meta_instance sigma b = let c_sigma = List.map - (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) + (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) in - if c_sigma = [] then b.rebus else instance c_sigma b.rebus + if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus -let nf_meta env c = meta_instance env (mk_freelisted c) +let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) @@ -924,7 +924,7 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9e5ced8a28..0b9e69d95b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -210,7 +210,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr val whd_meta : (metavariable * constr) list -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr -val instance : (metavariable * constr) list -> constr -> constr +val instance :evar_map -> (metavariable * constr) list -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function (*s Heuristic for Conversion with Evar *) |