reordering of lexicon status partially avoided to make it sure

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 02c959ef78abd300712faf1d2238aa654f1c9369..bae4a8f593628821b0f8d1181563aa7e496222b8 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -46,6 +46,7 @@ let level1_pattern =
 let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
 let term = Grammar.Entry.create level2_ast_grammar "term"
 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
+let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars"
 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
 let int_of_string s =
@@ -223,7 +224,7 @@ let level_of precedence associativity =
   in
   string_of_int precedence ^ assoc_string
 
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
@@ -420,13 +421,13 @@ END
 
 (* {{{ Grammar for ast patterns, notation level 2 *)
 EXTEND
-  GLOBAL: level2_ast term let_defs;
+  GLOBAL: level2_ast term let_defs protected_binder_vars;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
@@ -450,12 +451,18 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
+    | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, None, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
+    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [
@@ -489,11 +496,6 @@ EXTEND
         | _ -> failwith "Invalid index name."
     ]
   ];
-  induction_kind: [
-    [ "rec" -> `Inductive
-    | "corec" -> `CoInductive
-    ]
-  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -501,12 +503,6 @@ EXTEND
         index_name = OPT [ "on"; id = single_arg -> id ];
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
         SYMBOL <:unicode<def>> (* ≝ *); body = term ->
-          let body = fold_binder `Lambda args body in
-          let ty = 
-            match ty with 
-            | None -> None
-            | Some ty -> Some (fold_binder `Pi args ty)
-          in
           let rec position_of name p = function 
             | [] -> None, p
             | n :: _ when n = name -> Some p, p
@@ -526,7 +522,13 @@ EXTEND
             | None -> 0 
             | Some index_name -> find_arg index_name 0 args
           in
-          (name, ty), body, index
+          let args =
+           List.concat
+            (List.map
+             (function (names,ty) -> List.map (function x -> x,ty) names
+             ) args)
+          in
+           args, (name, ty), body, index
       ] SEP "and" ->
         defs
     ]
@@ -536,29 +538,35 @@ EXTEND
           l = LIST1 single_arg SEP SYMBOL "," -> l
         | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-    | LPAREN; 
-        vars = [
-            l =  LIST1 single_arg SEP SYMBOL "," -> l
-          | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
-      typ = OPT [ SYMBOL ":"; t = term -> t ]; 
-      RPAREN -> (vars, typ)
+    ]
+  ];
+  protected_binder_vars: [
+    [ LPAREN; vars = binder_vars; RPAREN -> vars 
+    ]
+  ];
+  maybe_protected_binder_vars: [
+    [ vars = binder_vars -> vars
+    | vars = protected_binder_vars -> vars
     ]
   ];
   term: LEVEL "10N" [ (* let in *)
     [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
-    | "let"; k = induction_kind; defs = let_defs; "in";
+    | LETCOREC; defs = let_defs; "in";
+      body = term ->
+        return_term loc (Ast.LetRec (`CoInductive, defs, body))
+    | LETREC; defs = let_defs; "in";
       body = term ->
-        return_term loc (Ast.LetRec (k, defs, body))
+        return_term loc (Ast.LetRec (`Inductive, defs, body))
     ]
   ];
   term: LEVEL "20R"  (* binder *)
     [
-      [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+      [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
           return_term loc (fold_cluster b vars typ body)
       | SYMBOL <:unicode<exists>> (* ∃ *);
-        (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+        (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
           return_term loc (fold_exists vars typ body)
       ]
     ];