X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=24d1b3feb441b864d977807b931196e1c3ea33f5;hb=ca2a604c2817deb118d595611b94a0d77978eab6;hp=3653c46069adc15ff3a2be2aa7edc7ca9693ea1f;hpb=c2d8fcd86793151c8cf24f45fc3064b97f16f596;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 3653c4606..24d1b3feb 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -25,7 +25,8 @@
 
 (* $Id$ *)
 
-open Printf
+let out = ref ignore
+let set_callback f = out := f
 
 module Ast = CicNotationPt
 
@@ -64,7 +65,11 @@ EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
-  ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+  new_name: [
+    [ id = IDENT -> Some id
+    | SYMBOL "_" -> None ]
+    ];
+  ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
   tactic_term_list1: [
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
@@ -140,35 +145,44 @@ EXTEND
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto"; params = auto_params ->
-        GrafiteAst.Auto (loc,params)
+    | IDENT "autobatch";  params = auto_params ->
+        GrafiteAst.AutoBatch (loc,params)
     | IDENT "cases"; what = tactic_term;
-      (num, idents) = intros_spec ->
-	GrafiteAst.Cases (loc, what, idents)
+      specs = intros_spec ->
+        GrafiteAst.Cases (loc, what, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
+    | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
+      OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+        let times = match times with None -> 1 | Some i -> i in
+        GrafiteAst.Compose (loc, t1, t2, times, specs)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | 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 "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
-    | IDENT "elim"; what = tactic_term; using = using;
-      (num, idents) = intros_spec ->
-	GrafiteAst.Elim (loc, what, using, num, idents)
+    | IDENT "elim"; what = tactic_term; using = using; 
+       pattern = OPT pattern_spec;
+       (num, idents) = intros_spec ->
+	let pattern = match pattern with
+	   | None         -> None, [], Some Ast.UserInput
+	   | Some pattern -> pattern   
+	in
+	GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
-	GrafiteAst.ElimType (loc, what, using, num, idents)
+	GrafiteAst.ElimType (loc, what, using, (num, idents))
     | IDENT "exact"; t = tactic_term ->
         GrafiteAst.Exact (loc, t)
     | IDENT "exists" ->
@@ -184,19 +198,17 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
        GrafiteAst.Generalize (loc,p,id)
-    | IDENT "goal"; n = int ->
-        GrafiteAst.Goal (loc, n)
     | IDENT "id" -> GrafiteAst.IdTac loc
     | IDENT "intro"; ident = OPT IDENT ->
-        let idents = match ident with None -> [] | Some id -> [id] in
-        GrafiteAst.Intros (loc, Some 1, idents)
-    | IDENT "intros"; (num, idents) = intros_spec ->
-        GrafiteAst.Intros (loc, num, idents)
+        let idents = match ident with None -> [] | Some id -> [Some id] in
+        GrafiteAst.Intros (loc, (Some 1, idents))
+    | IDENT "intros"; specs = intros_spec ->
+        GrafiteAst.Intros (loc, specs)
     | IDENT "inversion"; t = tactic_term ->
         GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
@@ -279,11 +291,28 @@ EXTEND
     | 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 ; 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 (start,termine), t1, t2, cont)
-    | 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)
+    | start =
+       [ IDENT "conclude" -> None
+       | IDENT "obtain" ; name = IDENT -> Some name ] ;
+      termine = tactic_term ;
+      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, 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)
   ]
 ];
   auto_params: [
@@ -330,9 +359,9 @@ EXTEND
           (GrafiteAst.Then (loc, tac, tacs))
       ]
     | "loops" RIGHTA
-      [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
+      [ IDENT "do"; count = int; tac = SELF ->
           GrafiteAst.Do (loc, count, tac)
-      | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
+      | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
       ]
     | "simple" NONA
       [ IDENT "first";
@@ -344,7 +373,7 @@ EXTEND
           GrafiteAst.Solve (loc, tacs)
       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
       | LPAREN; tac = SELF; RPAREN -> tac
-      | tac = tactic -> GrafiteAst.Tactic (loc, tac)
+      | tac = tactic -> tac
       ]
     ];
   punctuation_tactical:
@@ -358,12 +387,11 @@ EXTEND
       | SYMBOL "." -> GrafiteAst.Dot loc
       ]
     ];
-  tactical:
+  non_punctuation_tactical:
     [ "simple" NONA
       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
       | IDENT "skip" -> GrafiteAst.Skip loc
-      | tac = atomic_tactical LEVEL "loops" -> tac
       ]
     ];
   theorem_flavour: [
@@ -432,6 +460,8 @@ EXTEND
 	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
 	 GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | IDENT "auto"; params = auto_params ->
+        GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
@@ -458,10 +488,10 @@ EXTEND
           LexiconAst.Ident_alias (id, uri)
         else 
           raise
-           (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
+           (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
       else
         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
-          sprintf "Not a valid identifier: %s" id)))
+          Printf.sprintf "Not a valid identifier: %s" id)))
     | IDENT "symbol"; symbol = QSTRING;
       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
       SYMBOL "="; dsc = QSTRING ->
@@ -499,11 +529,11 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            add_raw_attribute ~text:(sprintf "@{%s}" blob)
+            add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
               (CicNotationParser.parse_level2_ast
                 (Ulexing.from_utf8_string blob))
         | blob = UNPARSED_META ->
-            add_raw_attribute ~text:(sprintf "${%s}" blob)
+            add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
               (CicNotationParser.parse_level2_meta
                 (Ulexing.from_utf8_string blob))
         ] ->
@@ -637,9 +667,11 @@ EXTEND
   ]];
   executable: [
     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
-    | tac = tactical; punct = punctuation_tactical ->
-        GrafiteAst.Tactical (loc, tac, Some punct)
-    | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
+    | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
+        GrafiteAst.Tactic (loc, Some tac, punct)
+    | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+    | tac = non_punctuation_tactical; punct = punctuation_tactical ->
+        GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
     ]
   ];
@@ -657,13 +689,14 @@ EXTEND
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
-        let buri, fullpath = 
+	let buri, fullpath = 
           DependenciesParser.baseuri_of_script ~include_paths fname 
         in
         let status =
          LexiconEngine.eval_command status 
            (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
+	 !out fname;
          status,
           LSome
           (GrafiteAst.Executable