X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=32b6b0a9068312564dcc8c65648b12892a6f4bc3;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=45ff3d23306e8131883eaf5a0ce13f97e55a41db;hpb=6627bb6bb1c3ae3ce70bcfe4d59997a94bec8b18;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 45ff3d233..32b6b0a90 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -46,8 +46,6 @@ let term = Grammar.Entry.create level2_ast_grammar "term"
 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
-let return_term loc term = ()
-
 let int_of_string s =
   try
     Pervasives.int_of_string s
@@ -78,7 +76,7 @@ let make_action action bindings =
     function
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 4 BEGIN *)
+    (* LUCA: DEFCON 3 BEGIN *)
     | Binding (name, Env.TermType) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
@@ -101,7 +99,7 @@ let make_action action bindings =
             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
     | Env _ :: tl ->
         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 4 END *)
+    (* LUCA: DEFCON 3 END *)
   in
     aux [] (List.rev bindings)
 
@@ -411,7 +409,8 @@ EXTEND
   level2_meta: [
     [ magic = l2_magic -> Ast.Magic magic
     | var = l2_variable -> Ast.Variable var
-    | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
+    | blob = UNPARSED_AST ->
+        !parse_level2_ast_ref (Ulexing.from_utf8_string blob)
     ]
   ];
 END
@@ -424,7 +423,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];
@@ -470,7 +469,7 @@ EXTEND
         List.map (fun n -> Ast.Ident (n, None)) names, Some ty
     | name = IDENT -> [Ast.Ident (name, None)], None
     | blob = UNPARSED_META ->
-        let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+        let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
         | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
@@ -480,7 +479,7 @@ EXTEND
   single_arg: [
     [ name = IDENT -> Ast.Ident (name, None)
     | blob = UNPARSED_META ->
-        let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+        let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
@@ -587,9 +586,9 @@ EXTEND
       | m = META; s = meta_substs ->
           return_term loc (Ast.Meta (int_of_string m, s))
       | s = sort -> return_term loc (Ast.Sort s)
-      | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
-        "match"; t = term;
+      | "match"; t = term;
         indty_ident = OPT [ "in"; id = IDENT -> id, None ];
+        outtyp = OPT [ "return"; ty = term -> ty ];
         "with"; SYMBOL "[";
         patterns = LIST0 [
           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
@@ -601,7 +600,8 @@ EXTEND
       | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
           return_term loc (Ast.Cast (p1, p2))
       | LPAREN; p = term; RPAREN -> p
-      | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
+      | blob = UNPARSED_META ->
+          !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
       ]
     ];
 END
@@ -618,12 +618,17 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (floc, exn) ->
       raise (Parse_error (floc, (Printexc.to_string exn)))
 
-let parse_level1_pattern stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
-let parse_level2_ast stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream)
-let parse_level2_meta stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta stream)
+let parse_level1_pattern lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+
+let parse_level2_ast lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level2_ast (Obj.magic lexbuf))
+
+let parse_level2_meta lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level2_meta (Obj.magic lexbuf))
 
 let _ =
   parse_level1_pattern_ref := parse_level1_pattern;