X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=05504f511f3c149913256f7740cffb861b231730;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=7b515472d2ef386385855a7d78abbf6543513618;hpb=50afaf262195266d156f594cff7e92a6e8898b3e;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7b515472d..05504f511 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 ]
   ];
@@ -143,8 +148,8 @@ EXTEND
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (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 ->
@@ -157,7 +162,7 @@ EXTEND
         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
@@ -170,10 +175,10 @@ EXTEND
 	   | None         -> None, [], Some Ast.UserInput
 	   | Some pattern -> pattern   
 	in
-	GrafiteAst.Elim (loc, what, using, pattern, num, idents)
+	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" ->
@@ -189,17 +194,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 "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"; 
@@ -460,10 +465,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 ->
@@ -501,11 +506,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))
         ] ->
@@ -661,13 +666,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