The rewritingstep declarative command now takes also a list of arguments

that are passed to paramodulation (after adding paramodulation=1 and
timeout=3 if these parameters are not already forced by the user).

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 26a65b53139f4dc8ba26e576b34ac3ba2cfae405..a4d357702925e86a5fb8b4b5e8d643e3b77f54fa 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -98,7 +98,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
   | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
   | RewritingStep of
-     loc * 'term option * 'term  * 'term option * Cic.name option
+     loc * 'term option * 'term  *
+      [ `Term of 'term | `Auto of (string * string) list ] * Cic.name option
   
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 98e57b5c4458e532334114deac4f1469f3e1fdc9..f7325f54fb05b74689b1631c8e97399f31775355 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -169,7 +169,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
   | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")"
   | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" 
-  | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id)
+  | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)  | `Term term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id)
   | Case (_, id, args) ->
      "case" ^ id ^
        String.concat " "

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index ae4eac52082e91e30f5ad602f230836b162438b3..4c2a631761679fb8a01fa808d93af4212cba4bf6 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -334,10 +334,10 @@ let disambiguate_tactic
        let metasenv,cic'= disambiguate_term context metasenv term2 in
         let metasenv,cic'' =
         match term3 with
-           None -> metasenv,None
-         | Some t -> 
+           `Auto _ as t -> metasenv,t
+         | `Term t -> 
             let metasenv,t = disambiguate_term context metasenv t in
-             metasenv,Some t in
+             metasenv,`Term t in
        metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
 

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index b41ae8ebcd8468c14415e86ca2e17c7eed149cc4..4c1ddffb20c07617f96b4da6fbb3340aa8b2ceb4 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -133,9 +133,7 @@ EXTEND
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto"; params = 
-        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
-          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+    | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
@@ -270,11 +268,19 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
         GrafiteAst.Case(loc,id,params)
-    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ; cont=rewriting_step_continuation ->
+    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params  ] ; cont=rewriting_step_continuation ->
      GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
-    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ; cont=rewriting_step_continuation  ->
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params ] ;
+      cont=rewriting_step_continuation  ->
      GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
+];
+  auto_params: [
+   [ params =
+      LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+       string_of_int v | v = IDENT -> v ] -> i,v ] ->
+      params
+   ]
 ];
   by_continuation: [
     [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index b1b38a9492e76cb5526c24c870382696a5f50314..7e276a8bcef73f63b273e9ed00ae3f61541f7d09 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -148,9 +148,18 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude =
    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
   let just =
    match just with
-      None ->
-       Tactics.auto ~dbd ~params:["paramodulation","1"; "timeout","3"] ~universe
-    | Some just -> Tactics.apply just 
+      `Auto params ->
+        let params =
+         if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+          ("paramodulation","1")::params
+         else params in
+        let params =
+         if not (List.exists (fun (k,_) -> k = "timeout") params) then
+          ("timeout","3")::params
+         else params
+        in
+         Tactics.auto ~dbd ~params ~universe
+    | `Term just -> Tactics.apply just 
   in
    match lhs with
       None ->

diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
index e9ec4f9df8663522fb5e937e3f151fc7137127c2..64147b778d55a4c90f9bda0ffef6243d1ea4515e 100644 (file)
--- a/components/tactics/declarative.mli
+++ b/components/tactics/declarative.mli
@@ -53,4 +53,4 @@ val andelim :
 
 val rewritingstep :
  dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term ->
-  Cic.term option -> Cic.name option -> ProofEngineTypes.tactic
+  [ `Term of Cic.term | `Auto of (string * string) list ] -> Cic.name option -> ProofEngineTypes.tactic