diff options
| -rw-r--r-- | contrib/subtac/eterm.ml | 27 | ||||
| -rw-r--r-- | contrib/subtac/eterm.mli | 3 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 23 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 14 |
5 files changed, 57 insertions, 14 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index c2d7a59f1b..6e522d499a 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) (** - Get types of existentials ; - Flatten dependency tree (prefix order) ; @@ -129,12 +130,34 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None +let evar_dependencies evm ev = + let one_step deps = + Intset.fold (fun ev s -> + let evi = Evd.find evm ev in + Intset.union (Evarutil.evars_of_evar_info evi) s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Intset.equal deps deps' then deps + else aux deps' + in aux (Intset.singleton ev) + +let sort_dependencies evl = + List.sort (fun (_, _, deps) (_, _, deps') -> + if Intset.subset deps deps' then (* deps' depends on deps *) -1 + else if Intset.subset deps' deps then 1 + else Intset.compare deps deps') + evl + let eterm_obligations env name isevars evm fs ?status t ty = - (* 'Serialize' the evars, we assume that the types of the existentials - refer to previous existentials in the list only *) + (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Sign.named_context_length nc in let evl = List.rev (to_list evm) in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> id, ev) sevl in let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index e197024ff4..a2010c9016 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -16,6 +16,9 @@ open Util val mkMetas : int -> constr list +val evar_dependencies : evar_map -> int -> Intset.t +val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list + (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 63a56f0d13..5491607153 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1054,7 +1054,28 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = with e when precatchable_exception e -> (evd,false) - +let evars_of_term c = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, _) -> Intset.add n acc + | _ -> fold_constr evrec acc c + in + evrec Intset.empty c + +let evars_of_named_context nc = + List.fold_right (fun (_, b, t) s -> + Option.fold_left (fun s t -> + Intset.union s (evars_of_term t)) + s b) nc Intset.empty + +let evars_of_evar_info evi = + Intset.union (evars_of_term evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> evars_of_term b) + (evars_of_named_context (named_context_of_val evi.evar_hyps))) + (* [check_evars] fails if some unresolved evar remains *) (* it assumes that the defined existentials have already been substituted *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d11e1fa2a5..ab9f8bebb1 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -94,6 +94,10 @@ val is_unification_pattern_evar : env -> existential -> constr list -> bool val is_unification_pattern : env -> constr -> constr array -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr +val evars_of_term : constr -> Intset.t +val evars_of_named_context : named_context -> Intset.t +val evars_of_evar_info : evar_info -> Intset.t + (***********************************************************) (* Value/Type constraints *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 115e47ae18..e9bd15b119 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -61,14 +61,6 @@ let init_setoid () = (** Typeclasses instance search tactic / eauto *) -let evars_of_term init c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) -> Intset.add n acc - | _ -> fold_constr evrec acc c - in - evrec init c - let intersects s t = Intset.exists (fun el -> Intset.mem el t) s @@ -183,14 +175,14 @@ let rec catchable = function | e -> Logic.catchable_exception e let is_dep gl gls = - let evs = evars_of_term Intset.empty gl.evar_concl in + let evs = Evarutil.evars_of_term gl.evar_concl in if evs = Intset.empty then false else List.fold_left (fun b gl -> if b then b else - let evs' = evars_of_term Intset.empty gl.evar_concl in + let evs' = Evarutil.evars_of_term gl.evar_concl in intersects evs evs') false gls @@ -455,7 +447,7 @@ let rec merge_deps deps = function let split_evars evm = Evd.fold (fun ev evi acc -> - let deps = evars_of_term (Intset.singleton ev) evi.evar_concl in + let deps = Intset.union (Intset.singleton ev) (Evarutil.evars_of_term evi.evar_concl) in merge_deps deps acc) evm [] |