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

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 933397067..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 5 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 5 END *)
+    (* LUCA: DEFCON 3 END *)
   in
     aux [] (List.rev bindings)
 
@@ -271,6 +269,13 @@ let fold_cluster binder terms ty body =
     (fun term body -> Ast.Binder (binder, (term, ty), body))
     terms body  (* terms are names: either Ident or FreshVar *)
 
+let fold_exists terms ty body =
+  List.fold_right
+    (fun term body ->
+      let lambda = Ast.Binder (`Lambda, (term, ty), body) in
+      Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+    terms body
+
 let fold_binder binder pt_names body =
   List.fold_right
     (fun (names, ty) body -> fold_cluster binder names ty body)
@@ -404,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
@@ -417,7 +423,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];
@@ -452,7 +458,7 @@ EXTEND
   ];
   binder: [
     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
-    | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+(*     | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
@@ -463,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
@@ -473,9 +479,10 @@ 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 _) -> meta
+        | Ast.Variable (Ast.FreshVar _)
+        | Ast.Variable (Ast.IdentVar _) -> meta
         | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
         | _ -> failwith "Invalid index name."
     ]
@@ -548,6 +555,9 @@ EXTEND
     [
       [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           return_term loc (fold_cluster b vars typ body)
+      | SYMBOL <:unicode<exists>> (* ∃ *);
+        (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          return_term loc (fold_exists vars typ body)
       ]
     ];
   term: LEVEL "70L"  (* apply *)
@@ -576,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>> (* ⇒ *);
@@ -590,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
@@ -607,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;