diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 478 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 143 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 22 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 59 | ||||
| -rw-r--r-- | pretyping/evd.mli | 11 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 15 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 4 |
9 files changed, 78 insertions, 659 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml deleted file mode 100644 index 7cbaf124a7..0000000000 --- a/pretyping/clenv.ml +++ /dev/null @@ -1,478 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pp -open Util -open Names -open Nameops -open Term -open Termops -open Namegen -open Sign -open Environ -open Evd -open Reduction -open Reductionops -open Rawterm -open Pattern -open Tacred -open Pretype_errors -open Evarutil -open Unification -open Mod_subst -open Coercion.Default - -(* Abbreviations *) - -let pf_env gls = Global.env_of_context gls.it.evar_hyps -let pf_hyps gls = named_context_of_val gls.it.evar_hyps -let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c -let pf_concl gl = gl.it.evar_concl - -(******************************************************************) -(* Clausal environments *) - -type clausenv = { - env : env; - evd : evar_map; - templval : constr freelisted; - templtyp : constr freelisted } - -let cl_env ce = ce.env -let cl_sigma ce = ce.evd - -let subst_clenv sub clenv = - { templval = map_fl (subst_mps sub) clenv.templval; - templtyp = map_fl (subst_mps sub) clenv.templtyp; - evd = subst_evar_defs_light sub clenv.evd; - env = clenv.env } - -let clenv_nf_meta clenv c = nf_meta clenv.evd c -let clenv_term clenv c = meta_instance clenv.evd c -let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv -let clenv_value clenv = meta_instance clenv.evd clenv.templval -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 (cl_env ce) (cl_sigma ce) c - -exception NotExtensibleClause - -let clenv_push_prod cl = - let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in - let rec clrec typ = match kind_of_term typ with - | Cast (t,_,_) -> clrec t - | Prod (na,t,u) -> - let mv = new_meta () in - let dep = dependent (mkRel 1) u in - let na' = if dep then na else Anonymous in - let e' = meta_declare mv t ~name:na' cl.evd in - let concl = if dep then subst1 (mkMeta mv) u else u in - let def = applist (cl.templval.rebus,[mkMeta mv]) in - { templval = mk_freelisted def; - templtyp = mk_freelisted concl; - evd = e'; - env = cl.env } - | _ -> raise NotExtensibleClause - in clrec typ - -(* Instantiate the first [bound] products of [t] with metas (all products if - [bound] is [None]; unfold local defs *) - -let clenv_environments evd bound t = - let rec clrec (e,metas) n t = - match n, kind_of_term t with - | (Some 0, _) -> (e, List.rev metas, t) - | (n, Cast (t,_,_)) -> clrec (e,metas) n t - | (n, Prod (na,t1,t2)) -> - let mv = new_meta () in - let dep = dependent (mkRel 1) t2 in - let na' = if dep then na else Anonymous in - let e' = meta_declare mv t1 ~name:na' e in - clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) - (if dep then (subst1 (mkMeta mv) t2) else t2) - | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) - | (n, _) -> (e, List.rev metas, t) - in - clrec (evd,[]) bound t - -(* Instantiate the first [bound] products of [t] with evars (all products if - [bound] is [None]; unfold local defs *) - -let clenv_environments_evars env evd bound t = - let rec clrec (e,ts) n t = - match n, kind_of_term t with - | (Some 0, _) -> (e, List.rev ts, t) - | (n, Cast (t,_,_)) -> clrec (e,ts) n t - | (n, Prod (na,t1,t2)) -> - let e',constr = Evarutil.new_evar e env t1 in - let dep = dependent (mkRel 1) t2 in - clrec (e', constr::ts) (Option.map ((+) (-1)) n) - (if dep then (subst1 constr t2) else t2) - | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t) - | (n, _) -> (e, List.rev ts, t) - in - clrec (evd,[]) bound t - -let clenv_conv_leq env sigma t c bound = - let ty = Retyping.get_type_of env sigma c in - let evd = Evd.create_goal_evar_defs sigma in - let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in - let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in - let evars = Evarconv.consider_remaining_unif_problems env evars in - let args = List.map (whd_evar evars) args in - check_evars env sigma evars (applist (c,args)); - args - -let mk_clenv_from_env environ sigma n (c,cty) = - let evd = create_goal_evar_defs sigma 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 = evd; - env = environ } - -let mk_clenv_from_n gls n (c,cty) = - mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty) - -let mk_clenv_from gls = mk_clenv_from_n gls None - -let mk_clenv_rename_from_n gls n (c,t) = - mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t) - -let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) - -(******************************************************************) - -(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions - * mv0, or if one of the free vars on mv1's freelist mentions - * mv0 *) - -let mentions clenv mv0 = - let rec menrec mv1 = - mv0 = mv1 || - let mlist = - try match meta_opt_fvalue clenv.evd mv1 with - | Some (b,_) -> b.freemetas - | None -> Metaset.empty - with Not_found -> Metaset.empty in - meta_exists menrec mlist - in menrec - -let error_incompatible_inst clenv mv = - let na = meta_name clenv.evd mv in - match na with - Name id -> - errorlabstrm "clenv_assign" - (str "An incompatible instantiation has already been found for " ++ - pr_id id) - | _ -> - anomaly "clenv_assign: non dependent metavar already assigned" - -(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) -let clenv_assign mv rhs clenv = - let rhs_fls = mk_freelisted rhs in - if meta_exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv_assign: circularity in unification"; - try - if meta_defined clenv.evd mv then - if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then - error_incompatible_inst clenv mv - else - clenv - else - let st = (ConvUpToEta 0,TypeNotProcessed) in - {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} - with Not_found -> - error "clenv_assign: undefined meta" - - - -(* [clenv_dependent hyps_only clenv] - * returns a list of the metavars which appear in the template of clenv, - * and which are dependent, This is computed by taking the metavars in cval, - * in right-to-left order, and collecting the metavars which appear - * in their types, and adding in all the metavars appearing in the - * type of clenv. - * If [hyps_only] then metavariables occurring in the type are _excluded_ *) - -(* [clenv_metavars clenv mv] - * returns a list of the metavars which appear in the type of - * the metavar mv. The list is unordered. *) - -let clenv_metavars evd mv = - (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas - -let dependent_metas clenv mvs conclmetas = - List.fold_right - (fun mv deps -> - Metaset.union deps (clenv_metavars clenv.evd mv)) - mvs conclmetas - -let duplicated_metas c = - let rec collrec (one,more as acc) c = - match kind_of_term c with - | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more) - | _ -> fold_constr collrec acc c - in - snd (collrec ([],[]) c) - -let clenv_dependent hyps_only clenv = - let mvs = undefined_metas clenv.evd in - let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in - let deps = dependent_metas clenv mvs ctyp_mvs in - let nonlinear = duplicated_metas (clenv_value clenv) in - (* Make the assumption that duplicated metas have internal dependencies *) - List.filter - (fun mv -> if Metaset.mem mv deps - then not (hyps_only && Metaset.mem mv ctyp_mvs) - else List.mem mv nonlinear) - mvs - -let clenv_missing ce = clenv_dependent true ce - -(******************************************************************) - -let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv = - { clenv with - evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd } - -let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = - { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } - -let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = - if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then - clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl) - (clenv_unify_meta_types ~flags:flags clenv) - else - clenv_unify allow_K CUMUL ~flags:flags - (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv - -(* [clenv_pose_metas_as_evars clenv dep_mvs] - * For each dependent evar in the clause-env which does not have a value, - * pose a value for it by constructing a fresh evar. We do this in - * left-to-right order, so that every evar's type is always closed w.r.t. - * metas. - - * Node added 14/4/08 [HH]: before this date, evars were collected in - clenv_dependent by collect_metas in the fold_constr order which is - (almost) the left-to-right order of dependencies in term. However, - due to K-redexes, collect_metas was sometimes missing some metas. - The call to collect_metas has been replaced by a call to - undefined_metas, but then the order was the one of definition of - the metas (numbers in increasing order) which is _not_ the - dependency order when a clenv_fchain occurs (because clenv_fchain - plugs a term with a list of consecutive metas in place of a - a priori - - arbitrary metavariable belonging to another sequence of consecutive metas: - e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of - (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2). - To ensure the dependency order, we check that the type of each meta - to pose is already meta-free, otherwise we postpone the transformation, - hoping that no cycle may happen. - - Another approach could have been to use decimal numbers for metas so that - in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2) - then making the numeric order match the dependency order. -*) - -let clenv_pose_metas_as_evars clenv dep_mvs = - let rec fold clenv = function - | [] -> clenv - | mv::mvs -> - let ty = clenv_meta_type clenv mv in - (* Postpone the evar-ization if dependent on another meta *) - (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta ty then fold clenv (mvs@[mv]) - else - let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in - let clenv = clenv_assign mv evar {clenv with evd=evd} in - fold clenv mvs in - fold clenv dep_mvs - -let evar_clenv_unique_resolver = clenv_unique_resolver - -(******************************************************************) - -let connect_clenv gls clenv = - { clenv with - evd = evars_reset_evd gls.sigma clenv.evd; - env = Global.env_of_context gls.it.evar_hyps } - -(* [clenv_fchain mv clenv clenv'] - * - * Resolves the value of "mv" (which must be undefined) in clenv to be - * the template of clenv' be the value "c", applied to "n" fresh - * metavars, whose types are chosen by destructing "clf", which should - * be a clausale forme generated from the type of "c". The process of - * resolution can cause unification of already-existing metavars, and - * of the fresh ones which get created. This operation is a composite - * of operations which pose new metavars, perform unification on - * terms, and make bindings. - - Otherwise said, from - - [clenv] = [env;sigma;metas |- c:T] - [clenv'] = [env';sigma';metas' |- d:U] - [mv] = [mi] of type [Ti] in [metas] - - then, if the unification of [Ti] and [U] produces map [rho], the - chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for - [rho'] being [rho;mi:=d]. - - In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. -*) -let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv = - (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) - let clenv' = - { templval = clenv.templval; - templtyp = clenv.templtyp; - evd = - evar_merge (meta_merge clenv.evd nextclenv.evd) clenv.evd; - env = nextclenv.env } in - (* unify the type of the template of [nextclenv] with the type of [mv] *) - let clenv'' = - clenv_unify allow_K ~flags:flags CUMUL - (clenv_term clenv' nextclenv.templtyp) - (clenv_meta_type clenv' mv) - clenv' in - (* assign the metavar *) - let clenv''' = - clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv'' - in - clenv''' - -(***************************************************************) -(* Bindings *) - -type arg_bindings = constr explicit_bindings - -(* [clenv_independent clenv] - * returns a list of metavariables which appear in the term cval, - * and which are not dependent. That is, they do not appear in - * the types of other metavars which are in cval, nor in the type - * of cval, ctyp. *) - -let clenv_independent clenv = - let mvs = collect_metas (clenv_value clenv) in - let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in - let deps = dependent_metas clenv mvs ctyp_mvs in - List.filter (fun mv -> not (Metaset.mem mv deps)) mvs - -let check_bindings bl = - match list_duplicates (List.map pi2 bl) with - | NamedHyp s :: _ -> - errorlabstrm "" - (str "The variable " ++ pr_id s ++ - str " occurs more than once in binding list."); - | AnonHyp n :: _ -> - errorlabstrm "" - (str "The position " ++ int n ++ - str " occurs more than once in binding list.") - | [] -> () - -let meta_of_binder clause loc mvs = function - | NamedHyp s -> meta_with_name clause.evd s - | AnonHyp n -> - try List.nth mvs (n-1) - with (Failure _|Invalid_argument _) -> - errorlabstrm "" (str "No such binder.") - -let error_already_defined b = - match b with - | NamedHyp id -> - errorlabstrm "" - (str "Binder name \"" ++ pr_id id ++ - str"\" already defined with incompatible value.") - | AnonHyp n -> - anomalylabstrm "" - (str "Position " ++ int n ++ str" already defined.") - -let clenv_unify_binding_type clenv c t u = - if isMeta (fst (whd_stack clenv.evd u)) then - (* Not enough information to know if some subtyping is needed *) - CoerceToType, clenv, c - else - (* Enough information so as to try a coercion now *) - try - let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in - TypeProcessed, { clenv with evd = evd }, c - with - | PretypeError (_,NotClean _) as e -> raise e - | e when precatchable_exception e -> - TypeNotProcessed, clenv, c - -let clenv_assign_binding clenv k c = - let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) 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 clenv_match_args bl clenv = - if bl = [] then - clenv - else - let mvs = clenv_independent clenv in - check_bindings bl; - List.fold_left - (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 c) - clenv bl - -let clenv_constrain_last_binding c clenv = - let all_mvs = collect_metas clenv.templval.rebus in - let k = - try list_last all_mvs - with Failure _ -> anomaly "clenv_constrain_with_bindings" in - clenv_assign_binding clenv k c - -let clenv_constrain_dep_args hyps_only bl clenv = - if bl = [] then - clenv - else - let occlist = clenv_dependent hyps_only clenv in - if List.length occlist = List.length bl then - List.fold_left2 clenv_assign_binding clenv occlist bl - else - errorlabstrm "" - (strbrk "Not the right number of missing arguments (expected " ++ - int (List.length occlist) ++ str ").") - -(****************************************************************) -(* Clausal environment for an application *) - -let make_clenv_binding_gen hyps_only n gls (c,t) = function - | ImplicitBindings largs -> - let clause = mk_clenv_from_n gls n (c,t) in - clenv_constrain_dep_args hyps_only largs clause - | ExplicitBindings lbind -> - let clause = mk_clenv_rename_from_n gls n (c,t) in - clenv_match_args lbind clause - | NoBindings -> - mk_clenv_from_n gls n (c,t) - -let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls -let make_clenv_binding = make_clenv_binding_gen false None - -(****************************************************************) -(* Pretty-print *) - -let pr_clenv clenv = - h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map clenv.evd) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli deleted file mode 100644 index 4f7ac40920..0000000000 --- a/pretyping/clenv.mli +++ /dev/null @@ -1,143 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(*i*) -open Util -open Names -open Term -open Sign -open Environ -open Evd -open Evarutil -open Mod_subst -open Rawterm -open Unification -(*i*) - -(***************************************************************) -(* The Type of Constructions clausale environments. *) - -(* [env] is the typing context - * [evd] is the mapping from metavar and evar numbers to their types - * and values. - * [templval] is the template which we are trying to fill out. - * [templtyp] is its type. - *) -type clausenv = { - env : env; - evd : evar_map; - templval : constr freelisted; - templtyp : constr freelisted } - -(* Substitution is not applied on templenv (because [subst_clenv] is - applied only on hints which typing env is overwritten by the - goal env) *) -val subst_clenv : substitution -> clausenv -> clausenv - -(* subject of clenv (instantiated) *) -val clenv_value : clausenv -> constr -(* type of clenv (instantiated) *) -val clenv_type : clausenv -> types -(* substitute resolved metas *) -val clenv_nf_meta : clausenv -> constr -> constr -(* type of a meta in clenv context *) -val clenv_meta_type : clausenv -> metavariable -> types - -val mk_clenv_from : evar_info sigma -> constr * types -> clausenv -val mk_clenv_from_n : - evar_info sigma -> int option -> constr * types -> clausenv -val mk_clenv_type_of : evar_info sigma -> constr -> clausenv -val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv - -(***************************************************************) -(* linking of clenvs *) - -val connect_clenv : evar_info sigma -> clausenv -> clausenv -val clenv_fchain : - ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv - -(***************************************************************) -(* Unification with clenvs *) - -(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) -val clenv_unify : - bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv - -(* unifies the concl of the goal with the type of the clenv *) -val clenv_unique_resolver : - bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv - -(* same as above ([allow_K=false]) but replaces remaining metas - with fresh evars if [evars_flag] is [true] *) -val evar_clenv_unique_resolver : - bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv - -val clenv_dependent : bool -> clausenv -> metavariable list - -val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv - -(***************************************************************) -(* 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 - start from the rightmost argument of the template. *) -val clenv_independent : clausenv -> metavariable list -val clenv_missing : clausenv -> metavariable list - -val clenv_constrain_last_binding : constr -> clausenv -> clausenv - -(* defines metas corresponding to the name of the bindings *) -val clenv_match_args : arg_bindings -> clausenv -> clausenv - -val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv - -(* start with a clenv to refine with a given term with bindings *) - -(* the arity of the lemma is fixed *) -(* 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 -> constr bindings -> - clausenv -val make_clenv_binding : - 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 - it produces the unification pattern [ccl]; [sigma'] is [sigma] - extended with [lmetas]; if [n] is defined, it limits the size of - the list even if [ccl] is still a product; otherwise, it stops when - [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] - and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and - [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] - and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) -val clenv_environments : - evar_map -> int option -> types -> evar_map * constr list * types - -(* [clenv_environments_evars env sigma n t] does the same but returns - a list of Evar's defined in [env] and extends [sigma] accordingly *) -val clenv_environments_evars : - env -> evar_map -> int option -> types -> evar_map * constr list * types - -(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) -val clenv_conv_leq : - env -> evar_map -> types -> constr -> int -> constr list - -(* if the clause is a product, add an extra meta for this product *) -exception NotExtensibleClause -val clenv_push_prod : clausenv -> clausenv - -(***************************************************************) -(* Pretty-print *) -val pr_clenv : clausenv -> Pp.std_ppcmds - diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 24850b4baf..6d37cf80f5 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -150,12 +150,11 @@ let evars_to_metas sigma (emap, c) = (* The list of non-instantiated existential declarations *) let non_instantiated sigma = - let listev = to_list sigma in - List.fold_left - (fun l (ev,evi) -> - if evi.evar_body = Evar_empty then - ((ev,nf_evar_info sigma evi)::l) else l) - [] listev + List.rev begin + Evd.fold_undefined begin fun ev evi l -> + (ev,nf_evar_info sigma evi)::l + end sigma [] + end (**********************) (* Creating new evars *) @@ -478,6 +477,10 @@ type clear_dependency_error = exception ClearDependencyError of identifier * clear_dependency_error +open Store.Field + +let cleared = Store.field () + let rec check_and_clear_in_constr evdref err ids c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of @@ -539,6 +542,13 @@ let rec check_and_clear_in_constr evdref err ids c = let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in + (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) + let evi = Evd.find !evdref evk in + let extra = evi.evar_extra in + let extra' = cleared.set true extra in + let evi' = { evi with evar_extra = extra' } in + evdref := Evd.add !evdref evk evi' ; + (* spiwack: /hacking session *) mkEvar(evk', Array.of_list nargs) end diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 205ca8bd64..39f8dd05ac 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -193,6 +193,10 @@ type clear_dependency_error = exception ClearDependencyError of identifier * clear_dependency_error +(* spiwack: marks an evar that has been "defined" by clear. + used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) +val cleared : bool Store.Field.t + val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> identifier list -> named_context_val * types diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a9b42f052b..5b4a3f214d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -51,7 +51,7 @@ type evar_info = { evar_body : evar_body; evar_filter : bool list; evar_source : hole_kind located; - evar_extra : Dyn.t option} + evar_extra : Store.t } let make_evar hyps ccl = { evar_concl = ccl; @@ -59,7 +59,7 @@ let make_evar hyps ccl = { evar_body = Evar_empty; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); evar_source = (dummy_loc,InternalHole); - evar_extra = None + evar_extra = Store.empty } let evar_concl evi = evi.evar_concl @@ -93,26 +93,31 @@ module ExistentialSet = Intset (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar + module EvarInfoMap = struct - type t = evar_info ExistentialMap.t + type t = evar_info ExistentialMap.t - let empty = ExistentialMap.empty + let empty = ExistentialMap.empty + let is_empty = ExistentialMap.is_empty let to_list evc = (* Workaround for change in Map.fold behavior *) + (* spiwack: seems to arrange the items in decreasing order. + Which would also be the behaviour of a naive [fold]. + I don't understand above comment. *) let l = ref [] in ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc; !l let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc [] let find evc k = ExistentialMap.find k evc - let remove evc k = ExistentialMap.remove k evc + let remove evc k = ExistentialMap.remove k evc let mem evc k = ExistentialMap.mem k evc let fold = ExistentialMap.fold let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false let add evd evk newinfo = ExistentialMap.add evk newinfo evd - let equal = ExistentialMap.equal + let map = ExistentialMap.map let define evd evk body = let oldinfo = @@ -182,6 +187,14 @@ module EvarInfoMap = struct try Some (existential_value sigma ev) with NotInstantiatedEvar -> None + (* Combinators on undefined evars. *) + let fold_undefined f = ExistentialMap.fold begin fun ev evi acc -> + match evar_body evi with + | Evar_empty -> f ev evi acc + | _ -> acc + end + + let undefined evm = fold_undefined ExistentialMap.add evm empty end (*******************************************************************) @@ -336,7 +349,23 @@ module EvarMap = struct (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty) || not (UniverseMap.equal (=) sm1 sm2)) - let merge e e' = fold (fun n v sigma -> add sigma n v) e' e + (* spiwack: used to workaround a bug in clenv: evar_merge + could merge an "old" version of an evar map into + a more up to date and erase evar definitions (in the case + of [constructor_tac] it actually erased a goal in some cases). + This is due to the fact that [open_constr] carry around their own + sigma which can be outdated by other operations. *) + let add_if_more_recent evd evk newinfo = + if newinfo.evar_body = Evar_empty && mem evd evk then + evd + else + add evd evk newinfo + + let merge e e' = fold (fun n v sigma -> add_if_more_recent sigma n v) e' e + + (* combinators on undefined values *) + let undefined (sigma,sm) = (EvarInfoMap.undefined sigma,sm) + let fold_undefined f (sigma,_) = EvarInfoMap.fold_undefined f sigma end @@ -441,7 +470,6 @@ let progress_evar_map d1 d2 = (* spiwack: tentative. It might very well not be the semantics we want for merging evar_map *) let merge d1 d2 = { -(* d1 with evars = EvarMap.merge d1.evars d2.evars*) evars = EvarMap.merge d1.evars d2.evars ; conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ; last_mods = ExistentialSet.union d1.last_mods d2.last_mods ; @@ -488,7 +516,7 @@ let subst_evar_defs_light sub evd = assert (evd.conv_pbs = []); { evd with metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; - evars = ExistentialMap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars + evars = EvarInfoMap.map (subst_evar_info sub) (fst evd.evars), (snd evd.evars) } let subst_evar_map = subst_evar_defs_light @@ -536,7 +564,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = evar_body = Evar_empty; evar_filter = filter; evar_source = src; - evar_extra = None} } + evar_extra = Store.empty } } let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk @@ -546,12 +574,10 @@ let is_undefined_evar evd c = match kind_of_term c with | _ -> false let undefined_evars evd = - let evars = - EvarMap.fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then - EvarMap.add sigma evk evi else sigma) - evd.evars EvarMap.empty - in - { evd with evars = evars } + let evars = EvarMap.undefined evd.evars in + { evd with evars = evars } + +let fold_undefined f evd = EvarMap.fold_undefined f evd.evars (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) @@ -694,7 +720,6 @@ let meta_with_name evd id = strbrk "\" occurs more than once in clause.") -(* spiwack: we should try and replace this List.fold_left by a Metamap.fold. *) let meta_merge evd1 evd2 = {evd2 with metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b82e6d998d..f895ead42c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -123,7 +123,7 @@ type evar_info = { evar_body : evar_body; evar_filter : bool list; evar_source : hole_kind located; - evar_extra : Dyn.t option} + evar_extra : Store.t } val eq_evar_info : evar_info -> evar_info -> bool @@ -185,6 +185,15 @@ val evars_reset_evd : evar_map -> evar_map -> evar_map for moving to evarutils *) val is_undefined_evar : evar_map -> constr -> bool val undefined_evars : evar_map -> evar_map +(* [fold_undefined f m] iterates ("folds") function [f] over the undefined + evars (that is, whose value is [Evar_empty]) of map [m]. + Making it effectively equivalent to {!Evd.fold} applies to + [f] and [undefined_evars m] *) +(* spiwack: at the moment, [fold_undefined] is defined rather naively. + But we can hope to enable some optimisation in the future, as + an evar_map contains typically few undefined evars compared to all + its evars. *) +val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a val evar_declare : named_context_val -> evar -> types -> ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> evar_map diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index cea33c1e98..6aa00c5f25 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -21,7 +21,6 @@ Typeclasses Classops Coercion Unification -Clenv Detyping Indrec Cases diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4ec5cf1f17..88d4a4d6b3 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -355,18 +355,15 @@ let is_implicit_arg k = calls (e.g. when doing apply in an External hint in typeclass_instances). Would be solved by having real evars-as-goals. *) -let ((bool_in : bool -> Dyn.t), - (bool_out : Dyn.t -> bool)) = Dyn.create "bool" - -let bool_false = bool_in false +let resolvable = Store.field () +open Store.Field let is_resolvable evi = - match evi.evar_extra with - Some t -> if Dyn.tag t = "bool" then bool_out t else true - | None -> true + Option.default true (resolvable.get evi.evar_extra) let mark_unresolvable evi = - { evi with evar_extra = Some bool_false } + let t = resolvable.set false evi.evar_extra in + { evi with evar_extra = t } let mark_unresolvables sigma = Evd.fold (fun ev evi evs -> @@ -374,7 +371,7 @@ let mark_unresolvables sigma = sigma Evd.empty let has_typeclasses evd = - Evd.fold (fun ev evi has -> has || + Evd.fold_undefined (fun ev evi has -> has || (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi)) evd false diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 997b28c105..e53be5c0bf 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -77,10 +77,6 @@ val is_implicit_arg : hole_kind -> bool val instance_constructor : typeclass -> constr list -> constr * types -(* Use evar_extra for marking resolvable evars. *) -val bool_in : bool -> Dyn.t -val bool_out : Dyn.t -> bool - val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map |