X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteParser.ml;h=d32eb32656313b90df47f9eef3c0c170f88594e0;hb=53b993e769b2223b3f6c9a052d4b014e83bc6d01;hp=64db522950c31e50e788c07878ced0dc5775d2d9;hpb=a696aae5ea794cd43fd3d83d37a0345d2a1387b3;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index 64db52295..d32eb3265 100644
--- a/helm/ocaml/grafite_parser/grafiteParser.ml
+++ b/helm/ocaml/grafite_parser/grafiteParser.ml
@@ -27,10 +27,17 @@ 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
 
@@ -72,9 +79,9 @@ EXTEND
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
       let goal_path =
        match goal_path, hyp_paths with
-          None, [] -> Ast.UserInput
-        | None, _::_ -> Ast.Implicit
-        | Some goal_path, _ -> goal_path
+          None, [] -> Some Ast.UserInput
+        | None, _::_ -> None
+        | Some goal_path, _ -> Some goal_path
       in
        hyp_paths,goal_path
    ]
@@ -91,12 +98,12 @@ EXTEND
         ] ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
-             wanted,None -> wanted, [], Ast.UserInput
+             wanted,None -> wanted, [], Some Ast.UserInput
            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
          in
           wanted, hyp_paths, goal_path ] ->
       match res with
-         None -> None,[],Ast.UserInput
+         None -> None,[],Some Ast.UserInput
        | Some ps -> ps]
   ];
   direction: [
@@ -183,6 +190,8 @@ EXTEND
         GrafiteAst.Intros (loc, Some 1, idents)
     | IDENT "intros"; (num, idents) = intros_spec ->
         GrafiteAst.Intros (loc, num, idents)
+    | IDENT "inversion"; t = tactic_term ->
+        GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       what = tactic_term; 
@@ -304,7 +313,9 @@ EXTEND
     name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
-       name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) 
+       name = IDENT ; 
+       coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; 
+       ty = term -> (name,ty,coercion) 
      ] SEP SYMBOL ";"; SYMBOL "}" -> 
       let params =
         List.fold_right
@@ -349,7 +360,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)))
@@ -362,14 +373,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: [
@@ -435,7 +446,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
@@ -474,31 +490,25 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true)
-    | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true)
-    | IDENT "alias" ; spec = alias_spec ->
-        GrafiteAst.Alias (loc, spec)
+    | IDENT "coercion" ; suri = URI ->
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
     | 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)
@@ -513,8 +523,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
     ]
   ];
@@ -534,22 +561,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 [])
-