changed auto_tac params type and all derivate tactics like applyS and

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index df18135ac56370767d77c3896855f2f3c62fbba8..0b13980161ba6f27dc6e3e7b7c37b2664421c556 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -78,7 +78,6 @@ EXTEND
   ];
   reduction_kind: [
     [ IDENT "normalize" -> `Normalize
-    | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
     | IDENT "whd" -> `Whd ]
@@ -142,9 +141,7 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
-    | IDENT "applyS"; t = tactic_term ; params = 
-        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
-          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+    | IDENT "applyS"; t = tactic_term ; params = auto_params ->
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
@@ -172,7 +169,7 @@ EXTEND
     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
-    | IDENT "demodulate" -> GrafiteAst.Demodulate loc
+    | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
         GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
@@ -258,7 +255,7 @@ EXTEND
         GrafiteAst.Assume (loc, id, t)
     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
         GrafiteAst.Suppose (loc, t, id, t1)
-    | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
+    | "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
       cont=by_continuation ->
        let t' = match t with LNone _ -> None | LSome t -> Some t in
        (match cont with
@@ -281,58 +278,47 @@ EXTEND
               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
         GrafiteAst.We_need_to_prove (loc, t, id, t1)
-    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+    | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
-    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+    | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
-    | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+    | "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
         GrafiteAst.Byinduction(loc, t, id)
     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
         GrafiteAst.Thesisbecomes(loc, t)
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
         GrafiteAst.Case(loc,id,params)
-    | start =
-       [ IDENT "conclude" -> None
-       | IDENT "obtain" ; name = IDENT -> Some name ] ;
-      termine = tactic_term ;
+    | start = OPT [
+       start = 
+        [ IDENT "conclude" -> None
+        | IDENT "obtain" ; name = IDENT -> Some name ] ;
+       termine = tactic_term -> start, termine];
       SYMBOL "=" ;
       t1=tactic_term ;
-      IDENT "by" ;
       t2 =
-       [ t=tactic_term -> `Term t
-       | SYMBOL "_" ; params = auto_params' -> `Auto params
-       | IDENT "proof" -> `Proof] ;
+       [ IDENT "exact"; t=tactic_term -> `Term t
+       | IDENT "using"; term=tactic_term -> `SolveWith term
+       | IDENT "proof" -> `Proof
+       | params = auto_params -> `Auto params];
       cont = rewriting_step_continuation ->
-       GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
-    | SYMBOL "=" ;
-      t1=tactic_term ;
-      IDENT "by" ;
-      t2=
-       [ t=tactic_term -> `Term t
-       | SYMBOL "_" ; params = auto_params' -> `Auto params
-       | IDENT "proof" -> `Proof] ;
-      cont=rewriting_step_continuation ->
-       GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+       GrafiteAst.RewritingStep(loc, start, 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 ] ->
+              string_of_int v | v = IDENT -> v ] -> i,v ]; 
+      tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] ->
+      (match tl with Some l -> l | None -> []),
       params
    ]
-];
-  auto_params': [
-   [ LPAREN; params = auto_params; RPAREN -> 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)
     | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; 
-            IDENT "done" -> BYC_weproved (ty,None,t1)
-    | IDENT "done" -> BYC_done
+            "done" -> BYC_weproved (ty,None,t1)
+    | "done" -> BYC_done
     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
     | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
@@ -340,7 +326,7 @@ EXTEND
     ]
 ];
   rewriting_step_continuation : [
-    [ IDENT "done" -> true
+    [ "done" -> true
     | -> false
     ]
 ];
@@ -653,11 +639,11 @@ EXTEND
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
-      refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
+      refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; "by" ;
                    refl = tactic_term -> refl ] ;
-      sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+      sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ;
                    sym = tactic_term -> sym ] ;
-      trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+      trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ;
                    trans = tactic_term -> trans ] ;
       "as" ; id = IDENT ->
        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)