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

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 24d1b3feb..df18135ac 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -30,6 +30,8 @@ let set_callback f = out := f
 
 module Ast = CicNotationPt
 
+exception NoInclusionPerformed of string (* full path *)
+
 type 'a localized_option =
    LSome of 'a
  | LNone of GrafiteAst.loc
@@ -41,6 +43,7 @@ type ast_statement =
     GrafiteAst.statement
 
 type statement =
+  ?never_include:bool -> 
   include_paths:string list ->
   LexiconEngine.status ->
     LexiconEngine.status * ast_statement localized_option
@@ -170,8 +173,8 @@ EXTEND
 	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 "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+        GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->
@@ -246,8 +249,6 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst" ->
-        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
@@ -459,7 +460,8 @@ EXTEND
 	 in
 	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
 	 GrafiteAst.Inline (loc,style,suri,prefix)
-    | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
+         if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term -> 
@@ -638,9 +640,13 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; 
+      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
         let arity = match arity with None -> 0 | Some x -> x in
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+        let saturations = match saturations with None -> 0 | Some x -> x in
+        let composites = match composites with None -> true | Some _ -> false in
+        GrafiteAst.Coercion
+         (loc, UriManager.uri_of_string suri, composites, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
@@ -684,17 +690,18 @@ EXTEND
   ];
   statement: [
     [ ex = executable ->
-       fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+       fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
-       fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+       fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
-       fun ~include_paths status ->
-	let buri, fullpath = 
-          DependenciesParser.baseuri_of_script ~include_paths fname 
+       fun ?(never_include=false) ~include_paths status ->
+	let _root, buri, fullpath, _rrelpath = 
+          Librarian.baseuri_of_script ~include_paths fname 
         in
         let status =
-         LexiconEngine.eval_command status 
-           (LexiconAst.Include (iloc,buri,mode,fullpath))
+         if never_include then raise (NoInclusionPerformed fullpath)
+         else LexiconEngine.eval_command status 
+                (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
 	 !out fname;
          status,
@@ -703,7 +710,7 @@ EXTEND
            (loc,GrafiteAst.Command
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
-       fun ~include_paths status ->
+       fun ?(never_include=false) ~include_paths status ->
 	let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file
@@ -725,3 +732,4 @@ let exc_located_wrapper f =
 let parse_statement lexbuf =
   exc_located_wrapper
     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+