summaryrefslogtreecommitdiff
path: root/tactics/eauto.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /tactics/eauto.ml4
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r--tactics/eauto.ml437
1 files changed, 18 insertions, 19 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2effe103..1503ca9a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: eauto.ml4 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: eauto.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -74,11 +74,11 @@ let prolog_tac l n gl =
let n =
match n with
| ArgArg n -> n
- | _ -> error "Prolog called with a non closed argument"
+ | _ -> error "Prolog called with a non closed argument."
in
try (prolog l n gl)
with UserError ("Refiner.tclFIRST",_) ->
- errorlabstrm "Prolog.prolog" (str "Prolog failed")
+ errorlabstrm "Prolog.prolog" (str "Prolog failed.")
TACTIC EXTEND prolog
| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
@@ -111,7 +111,7 @@ let rec e_trivial_fail_db mod_delta db_list local_db goal =
let d = pf_last_hyp g' in
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db mod_delta db_list
- (add_hint_list hintl local_db) g'))) ::
+ (Hint_db.add_list hintl local_db) g'))) ::
(List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) )
in
tclFIRST (List.map tclCOMPLETE tacl) goal
@@ -124,10 +124,9 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
let hintl =
if occur_existential concl then
- list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list)
+ list_map_append (Hint_db.map_all hdc) (local_db::db_list)
else
- list_map_append (fun (st, db) ->
- Hint_db.map_auto (hdc,concl) db) (local_db::db_list)
+ list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
in
let tac_of_hint =
fun {pri=b; pat = p; code=t} ->
@@ -160,12 +159,12 @@ and e_my_find_search_delta db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
let hintl =
if occur_existential concl then
- list_map_append (fun (st, db) ->
- let flags = {auto_unif_flags with modulo_delta = st} in
+ list_map_append (fun db ->
+ let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) ->
- let flags = {auto_unif_flags with modulo_delta = st} in
+ list_map_append (fun db ->
+ let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
let tac_of_hint =
@@ -285,8 +284,7 @@ module SearchProblem = struct
let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
in
-
- let ldb = add_hint_list hintl (List.hd s.localdb) in
+ let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
{ depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
localdb = ldb :: List.tl s.localdb })
@@ -333,7 +331,7 @@ let e_depth_search debug p db_list local_db gl =
let tac = if debug then Search.debug_depth_first else Search.depth_first in
let s = tac (make_initial_state p gl db_list local_db) in
s.tacres
- with Not_found -> error "EAuto: depth first search failed"
+ with Not_found -> error "eauto: depth first search failed."
let e_breadth_search debug n db_list local_db gl =
try
@@ -342,7 +340,7 @@ let e_breadth_search debug n db_list local_db gl =
in
let s = tac (make_initial_state n gl db_list local_db) in
s.tacres
- with Not_found -> error "EAuto: breadth first search failed"
+ with Not_found -> error "eauto: breadth first search failed."
let e_search_auto debug (in_depth,p) lems db_list gl =
let local_db = make_local_hint_db true lems gl in
@@ -361,7 +359,7 @@ let eauto debug np lems dbnames =
List.map
(fun x ->
try searchtable_map x
- with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+ with Not_found -> error ("No such Hint database: "^x^"."))
("core"::dbnames)
in
tclTRY (e_search_auto debug np lems db_list)
@@ -379,12 +377,12 @@ let gen_eauto d np lems = function
let make_depth = function
| None -> !default_search_depth
| Some (ArgArg d) -> d
- | _ -> error "EAuto called with a non closed argument"
+ | _ -> error "eauto called with a non closed argument."
let make_dimension n = function
| None -> (true,make_depth n)
| Some (ArgArg d) -> (false,d)
- | _ -> error "EAuto called with a non closed argument"
+ | _ -> error "eauto called with a non closed argument."
open Genarg
@@ -452,7 +450,8 @@ let autosimpl db cl =
else []
in
let unfolds = List.concat (List.map (fun dbname ->
- let ((ids, csts), _) = searchtable_map dbname in
+ let db = searchtable_map dbname in
+ let (ids, csts) = Hint_db.transparent_state db in
unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
in unfold_option unfolds cl