diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_setoid.ml4 | 23 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 37 | ||||
| -rw-r--r-- | tactics/eauto.mli | 3 |
3 files changed, 40 insertions, 23 deletions
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 84c1937ea8..9aa4451870 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -74,7 +74,8 @@ let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") (* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *) -let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") +(* let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") *) +let coq_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, mkProp)) let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") @@ -112,7 +113,7 @@ let build_signature isevars env m cstrs finalcstr = (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in let mk_relty ty obj = - let relty = mkApp (Lazy.force coq_relation, [| ty |]) in + let relty = coq_relation ty in match obj with | None -> new_evar isevars env relty | Some (p, (a, r, oldt, newt)) -> r @@ -256,17 +257,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t = let relargs, args = array_chop (Array.length args - 2) args in let rel = mkApp (r, relargs) in let typ = pf_type_of gl rel in - (match kind_of_term typ with - | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation) - || eq_constr relation (Lazy.force coq_relationT) -> - (c, (carrier, rel, args.(0), args.(1))) - | _ when isArity typ -> - let (ctx, ar) = destArity typ in - (match ctx with - [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> - (c, (sx, rel, args.(0), args.(1))) - | _ -> error "Only binary relations are supported") - | _ -> error "Not a relation") + (if isArity typ then + let (ctx, ar) = destArity typ in + (match ctx with + [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> + (c, (sx, rel, args.(0), args.(1))) + | _ -> error "Only binary relations are supported") + else error "Not a relation") | _ -> error "Not a relation" in if left2right then res diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 70ec9d046e..da477f2a32 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -241,15 +241,19 @@ module SearchProblem = struct let success s = (sig_it (fst s.tacres)) = [] - let rec filter_tactics (glls,v) = function - | [] -> [] - | (tac,pptac) :: tacl -> - try - let (lgls,ptl) = apply_tac_list tac glls in - let v' p = v (ptl p) in - ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl - with e when Logic.catchable_exception e -> - filter_tactics (glls,v) tacl + let filter_tactics (glls,v) l = +(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) + let rec aux = function + | [] -> [] + | (tac,pptac) :: tacl -> + try + let (lgls,ptl) = apply_tac_list tac glls in + let v' p = v (ptl p) in +(* msg (hov 0 (pptac ++ str"\n")); *) + ((lgls,v'),pptac) :: aux tacl + with e when Logic.catchable_exception e -> + aux tacl + in aux l (* Ordering of states is lexicographic on depth (greatest first) then number of remaining goals. *) @@ -498,7 +502,7 @@ let valid evm p res_sigma l = !res_sigma (l, Evd.create_evar_defs !res_sigma) in raise (Found (snd evd')) -let resolve_all_evars debug (mode, depth) env p evd = +let resolve_all_evars_once debug (mode, depth) env p evd = let evm = Evd.evars_of evd in let goals = Evd.fold @@ -513,3 +517,16 @@ let resolve_all_evars debug (mode, depth) env p evd = let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in res_sigma := Evarutil.nf_evars (sig_sig gls'); try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd' + +let has_undefined p evd = + Evd.fold (fun ev evi has -> has || + (evi.evar_body = Evar_empty && p ev evi)) + (Evd.evars_of evd) false + +let rec resolve_all_evars debug m env p evd = + let rec aux n evd = + if has_undefined p evd && n > 0 then + let evd' = resolve_all_evars_once debug m env p evd in + aux (pred n) evd' + else evd + in aux 3 evd diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 940648c2eb..a1ff899053 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -61,6 +61,9 @@ end val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> goal list sigma * validation +val resolve_all_evars_once : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs -> + evar_defs + val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs -> evar_defs |