X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteParser.ml;h=e480efd34f1cbfbc77656716ee0f4f9ff0b59f66;hb=7be6aeb94aa8da17732511a4844bd108976f947f;hp=5b9cea37a8cf9aac01fd186e7b214cd25735af3b;hpb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index 5b9cea37a..e480efd34 100644
--- a/helm/ocaml/grafite_parser/grafiteParser.ml
+++ b/helm/ocaml/grafite_parser/grafiteParser.ml
@@ -23,14 +23,23 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 module Ast = CicNotationPt
 
+type 'a localized_option =
+   LSome of 'a
+ | LNone of Token.flocation
+
 type statement =
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
-    GrafiteAst.statement
+ include_paths:string list ->
+ LexiconEngine.status ->
+  LexiconEngine.status *
+  (CicNotationPt.term, CicNotationPt.term,
+   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+    GrafiteAst.statement localized_option
 
 let grammar = CicNotationParser.level2_ast_grammar
 
@@ -57,7 +66,8 @@ EXTEND
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
   reduction_kind: [
-    [ IDENT "normalize" -> `Normalize
+    [ IDENT "demodulate" -> `Demodulate
+    | IDENT "normalize" -> `Normalize
     | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
     | IDENT "unfold"; t = OPT term -> `Unfold t
@@ -353,7 +363,7 @@ EXTEND
         if (try ignore (UriManager.uri_of_string uri); true
             with UriManager.IllFormedUri _ -> false)
         then
-          GrafiteAst.Ident_alias (id, uri)
+          LexiconAst.Ident_alias (id, uri)
         else 
           raise
            (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
@@ -366,14 +376,14 @@ EXTEND
         let instance =
           match instance with Some i -> i | None -> 0
         in
-        GrafiteAst.Symbol_alias (symbol, instance, dsc)
+        LexiconAst.Symbol_alias (symbol, instance, dsc)
     | IDENT "num";
       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
       SYMBOL "="; dsc = QSTRING ->
         let instance =
           match instance with Some i -> i | None -> 0
         in
-        GrafiteAst.Number_alias (instance, dsc)
+        LexiconAst.Number_alias (instance, dsc)
     ]
   ];
   argument: [
@@ -439,7 +449,12 @@ EXTEND
         (s, args, t)
     ]
   ];
-  command: [ [
+  
+  include_command: [ [
+      IDENT "include" ; path = QSTRING -> loc,path
+   ]];
+
+  grafite_command: [ [
       IDENT "set"; n = QSTRING; v = QSTRING ->
         GrafiteAst.Set (loc, n, v)
     | IDENT "drop" -> GrafiteAst.Drop loc
@@ -480,27 +495,23 @@ EXTEND
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
     | IDENT "coercion" ; suri = URI ->
         GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
-    | IDENT "alias" ; spec = alias_spec ->
-        GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
-    | IDENT "include" ; path = QSTRING ->
-        GrafiteAst.Include (loc,path)
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
+  ]];
+  lexicon_command: [ [
+      IDENT "alias" ; spec = alias_spec ->
+        LexiconAst.Alias (loc, spec)
     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
-        GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
+        LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
-        GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
-
-    | IDENT "dump" -> GrafiteAst.Dump loc
-    | IDENT "render"; u = URI ->
-        GrafiteAst.Render (loc, UriManager.uri_of_string u)
+        LexiconAst.Interpretation (loc, id, (symbol, args), l3)
   ]];
   executable: [
-    [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
+    [ 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)
@@ -515,8 +526,25 @@ EXTEND
     ]
   ];
   statement: [
-    [ ex = executable -> GrafiteAst.Executable (loc,ex)
-    | com = comment -> GrafiteAst.Comment (loc, com)
+    [ ex = executable ->
+       fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+    | com = comment ->
+       fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+    | (iloc,fname) = include_command ; SYMBOL "."  ->
+       fun ~include_paths status ->
+        let path = DependenciesParser.baseuri_of_script ~include_paths fname in
+        let status =
+         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+        in
+         status,
+          LSome
+          (GrafiteAst.Executable
+           (loc,GrafiteAst.Command
+            (loc,GrafiteAst.Include (iloc,path))))
+    | scom = lexicon_command ; SYMBOL "." ->
+       fun ~include_paths status ->
+        let status = LexiconEngine.eval_command status scom in
+         status,LNone loc
     | EOI -> raise End_of_file
     ]
   ];
@@ -536,22 +564,3 @@ let exc_located_wrapper f =
 let parse_statement lexbuf =
   exc_located_wrapper
     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
-
-let parse_dependencies lexbuf = 
-  let tok_stream,_ =
-    CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
-  in
-  let rec parse acc = 
-    (parser
-    | [< '("URI", u) >] ->
-        parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc)
-    | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
-        parse (GrafiteAst.IncludeDep fname :: acc)
-    | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
-        parse (GrafiteAst.BaseuriDep baseuri :: acc)
-    | [< '("EOI", _) >] -> acc
-    | [< 'tok >] -> parse acc
-    | [<  >] -> acc) tok_stream
-  in
-  List.rev (parse [])
-