]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.ml
parameter sintax added to axiom statement
[helm.git] / helm / software / components / content_pres / cicNotationParser.ml
index d110bda9a65d10b6cabfc0074a798e5bd7040786..587c22e4a07b8b9a39fea3225069c4a73454e01f 100644 (file)
@@ -33,21 +33,45 @@ module Env = CicNotationEnv
 exception Parse_error of string
 exception Level_not_found of int
 
-let level1_pattern_grammar =
-  Grammar.gcreate CicNotationLexer.level1_pattern_lexer
-let level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexer
-let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
-
 let min_precedence = 0
 let max_precedence = 100
 
-let level1_pattern =
-  Grammar.Entry.create level1_pattern_grammar "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"
+type ('a,'b,'c,'d) grammars = {
+  level1_pattern: 'a Grammar.Entry.e;
+  level2_ast: 'b Grammar.Entry.e;
+  level2_ast_grammar : Grammar.g;
+  term: 'b Grammar.Entry.e;
+  let_defs: 'c Grammar.Entry.e;
+  protected_binder_vars: 'd Grammar.Entry.e;
+  level2_meta: 'b Grammar.Entry.e;
+}
+
+let initial_grammars () =
+  let level1_pattern_grammar = 
+    Grammar.gcreate (CicNotationLexer.level1_pattern_lexer ()) in
+  let level2_ast_grammar = 
+    Grammar.gcreate (CicNotationLexer.level2_ast_lexer ()) in
+  let level2_meta_grammar = 
+    Grammar.gcreate (CicNotationLexer.level2_meta_lexer ()) in
+  let level1_pattern =
+    Grammar.Entry.create level1_pattern_grammar "level1_pattern" in
+  let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
+  let term = Grammar.Entry.create level2_ast_grammar "term" in
+  let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+  let protected_binder_vars = 
+    Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
+  let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
+  { level1_pattern=level1_pattern;
+    level2_ast=level2_ast;
+    term=term;
+    let_defs=let_defs;
+    protected_binder_vars=protected_binder_vars;
+    level2_meta=level2_meta;
+    level2_ast_grammar=level2_ast_grammar;
+}
+;;
+
+let grammars = ref (initial_grammars ());;
 
 let int_of_string s =
   try
@@ -57,11 +81,22 @@ let int_of_string s =
 
 (** {2 Grammar extension} *)
 
+let level_of precedence =
+  if precedence < min_precedence || precedence > max_precedence then
+    raise (Level_not_found precedence);
+  string_of_int precedence 
+
 let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
 let gram_ident s = Gramext.Stoken ("IDENT", s)
 let gram_number s = Gramext.Stoken ("NUMBER", s)
 let gram_keyword s = Gramext.Stoken ("", s)
-let gram_term = Gramext.Sself
+let gram_term = function
+  | Ast.Self _ -> Gramext.Sself
+  | Ast.Level precedence ->
+      Gramext.Snterml 
+        (Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e), 
+         level_of precedence)
+;;
 
 let gram_of_literal =
   function
@@ -80,10 +115,10 @@ let make_action action bindings =
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
     (* LUCA: DEFCON 3 BEGIN *)
-    | Binding (name, Env.TermType) :: tl ->
+    | Binding (name, Env.TermType l) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
-            aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+            aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
     | Binding (name, Env.StringType) :: tl ->
         Gramext.action
           (fun (v:string) ->
@@ -135,20 +170,24 @@ let extract_term_production pattern =
         [NoBinding, gram_keyword s]
     | `Number s -> [NoBinding, gram_number s]
   and aux_layout = function
-    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
-    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
-    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
-    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
-    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
-    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
-    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2
+    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
+    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2
+    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2
+    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2
+    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2
     | Ast.Root (p1, p2) ->
-        [NoBinding, gram_symbol "\\root"] @ aux p2
-        @ [NoBinding, gram_symbol "\\of"] @ aux p1
-    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+        [NoBinding, gram_symbol "\\root "] @ aux p2
+        @ [NoBinding, gram_symbol "\\of "] @ aux p1
+    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
     | Ast.Break -> []
     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
     | Ast.Group pl -> List.flatten (List.map aux pl)
+    | Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
+    | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
+    | Ast.Maction l -> List.flatten (List.map aux l)
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
@@ -165,20 +204,6 @@ let extract_term_production pattern =
     | Ast.List0 (p, _)
     | Ast.List1 (p, _) ->
         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-(*         let env0 = List.map list_binding_of_name p_names in
-        let grow_env_entry env n v =
-          List.map
-            (function
-              | (n', (ty, ListValue vl)) as entry ->
-                  if n' = n then n', (ty, ListValue (v :: vl)) else entry
-              | _ -> assert false)
-            env
-        in
-        let grow_env env_i env =
-          List.fold_left
-            (fun env (n, (_, v)) -> grow_env_entry env n v)
-            env env_i
-        in *)
         let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
           CicNotationEnv.coalesce_env p_names env_list
         in
@@ -186,8 +211,8 @@ let extract_term_production pattern =
           match magic with
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -198,7 +223,8 @@ let extract_term_production pattern =
   and aux_variable =
     function
     | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
-    | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+    | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) -> 
+        [Binding (s, Env.TermType level), gram_term lv]
     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
     | Ast.Ascription (p, s) -> assert false (* TODO *)
     | Ast.FreshVar _ -> assert false
@@ -213,34 +239,118 @@ let extract_term_production pattern =
   in
   aux pattern
 
-let level_of precedence associativity =
-  if precedence < min_precedence || precedence > max_precedence then
-    raise (Level_not_found precedence);
-  let assoc_string =
-    match associativity with
-    | Gramext.NonA -> "N"
-    | Gramext.LeftA -> "L"
-    | Gramext.RightA -> "R"
-  in
-  string_of_int precedence ^ assoc_string
+type rule_id = Grammar.token Gramext.g_symbol list
 
-type rule_id = Token.t Gramext.g_symbol list
+let compare_rule_id x y =
+  let rec aux = function
+    | [],[] -> 0
+    | [],_ -> ~-1
+    | _,[] -> 1
+    | ((s1::tl1) ),((s2::tl2) ) ->
+        if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+        else 
+          let res = 
+            try Pervasives.compare s1 s2 
+            with Invalid_argument _ -> 0 
+          in
+           if res = 0 then aux (tl1, tl2) else res 
+  in
+    aux (x,y)
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
-let owned_keywords = Hashtbl.create 23
+let initial_owned_keywords () = Hashtbl.create 23
+let owned_keywords = ref (initial_owned_keywords ())
 
-let extend level1_pattern ~precedence ~associativity action =
+type checked_l1_pattern = CL1P of CicNotationPt.term * int
+
+let check_l1_pattern level1_pattern pponly level associativity =
+  let variables = ref 0 in
+  let symbols = ref 0 in
+  let rec aux = function
+    | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t)
+    | Ast.Literal _ as l -> incr symbols; l
+    | Ast.Layout l -> Ast.Layout (aux_layout l)
+    | Ast.Magic m -> Ast.Magic (aux_magic m)
+    | Ast.Variable v -> (aux_variable v)
+    | t -> assert false
+  and aux_layout = function
+    | Ast.Sub (p1, p2)   -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
+    | Ast.Sup (p1, p2)   -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (p1, p2)
+    | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
+    | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
+    | Ast.Frac (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+    | Ast.InfRule (p1, p2, p3)  -> let p1 = aux p1 in let p2 = aux p2 in let p3 = aux p3 in Ast.InfRule (p1, p2, p3)
+    | Ast.Atop (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
+    | Ast.Over (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
+    | Ast.Root (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
+    | Ast.Sqrt p -> Ast.Sqrt (aux p)
+    | Ast.Break as t -> t 
+    | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
+    | Ast.Group pl -> Ast.Group (List.map aux pl)
+    | Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
+    | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
+    | Ast.Maction l as t -> 
+        if not pponly then 
+        raise(Parse_error("Maction can be used only in output notations")) 
+        else t
+  and aux_magic magic =
+    match magic with
+    | Ast.Opt p -> Ast.Opt (aux p)
+    | Ast.List0 (p, x) -> Ast.List0 (aux p, x)
+    | Ast.List1 (p, x) -> Ast.List1 (aux p, x)
+    | _ -> assert false
+  and aux_variable =
+    function
+    | Ast.NumVar _ as t -> Ast.Variable t
+    | Ast.TermVar (s,Ast.Self _) when associativity <> Gramext.NonA -> 
+        incr variables; 
+        if !variables > 2 then
+          raise (Parse_error ("Exactly 2 variables must be specified in an "^
+          "associative notation"));
+        (match !variables, associativity with
+        | 1,Gramext.LeftA -> 
+             Ast.Variable (Ast.TermVar (s, Ast.Self level))
+        | 1,Gramext.RightA -> 
+             Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+        | 2,Gramext.LeftA ->
+             Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+        | 2,Gramext.RightA -> 
+             Ast.Variable (Ast.TermVar (s, Ast.Level (level-1)))
+        | _ -> assert false)
+    | Ast.TermVar (s,Ast.Level _) when associativity <> Gramext.NonA -> 
+          raise (Parse_error ("Variables can not be declared with a " ^ 
+            "precedence in an associative notation"))
+       (*avoid camlp5 divergence due to non-Sself recursion at the same level *)
+    | Ast.TermVar (s,Ast.Level l) when l<=level && !variables=0 && !symbols=0-> 
+       raise(Parse_error("Left recursive rule with precedence not greater " ^
+        "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
+    | Ast.TermVar _ as t -> incr variables; Ast.Variable t
+    | Ast.IdentVar _ as t -> Ast.Variable t
+    | Ast.Ascription _ -> assert false (* TODO *)
+    | Ast.FreshVar _ -> assert false
+  in
+  if associativity <> Gramext.NonA && level = min_precedence then
+    raise (Parse_error ("You can not specify an associative notation " ^
+    "at level "^string_of_int min_precedence ^ "; increase it"));
+  let cp = aux level1_pattern in
+(*   prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *)
+  if !variables <> 2 && associativity <> Gramext.NonA then
+    raise (Parse_error ("Exactly 2 variables must be specified in an "^
+     "associative notation"));
+  CL1P (cp,level)
+;;
+
+let extend (CL1P (level1_pattern,precedence)) action =
   let p_bindings, p_atoms =
     List.split (extract_term_production level1_pattern)
   in
-  let level = level_of precedence associativity in
-(*   let p_names = flatten_opt p_bindings in *)
+  let level = level_of precedence in
   let _ =
     Grammar.extend
-      [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
+      [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e),
         Some (Gramext.Level level),
         [ None,
-          Some associativity,
+          Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, 
             (make_action
               (fun (env: CicNotationEnv.t) (loc: Ast.location) ->
@@ -250,20 +360,20 @@ let extend level1_pattern ~precedence ~associativity action =
   let keywords = CicNotationUtil.keywords_of_term level1_pattern in
   let rule_id = p_atoms in
   List.iter CicNotationLexer.add_level2_ast_keyword keywords;
-  Hashtbl.add owned_keywords rule_id keywords;  (* keywords may be [] *)
+  Hashtbl.add !owned_keywords rule_id keywords;  (* keywords may be [] *)
   rule_id
 
 let delete rule_id =
   let atoms = rule_id in
   (try
-    let keywords = Hashtbl.find owned_keywords rule_id in
+    let keywords = Hashtbl.find !owned_keywords rule_id in
     List.iter CicNotationLexer.remove_level2_ast_keyword keywords
   with Not_found -> assert false);
-  Grammar.delete_rule term atoms
+  Grammar.delete_rule !grammars.term atoms
 
 (** {2 Grammar} *)
 
-let parse_level1_pattern_ref = ref (fun _ -> assert false)
+let parse_level1_pattern_ref = ref (fun _ -> assert false)
 let parse_level2_ast_ref = ref (fun _ -> assert false)
 let parse_level2_meta_ref = ref (fun _ -> assert false)
 
@@ -285,9 +395,11 @@ let fold_binder binder pt_names body =
     pt_names body
 
 let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
+let return_term_of_level loc term l = 
+  Ast.AttributedTerm (`Loc loc, term l)
 
   (* create empty precedence level for "term" *)
-let _ =
+let initialize_grammars () =
   let dummy_action =
     Gramext.action (fun _ ->
       failwith "internal error, lexer generated a dummy token")
@@ -300,25 +412,29 @@ let _ =
       | i when i < first -> acc
       | i ->
           aux
-            ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod)
-             :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod)
-             :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod)
+            ((Some (level_of i), Some Gramext.NonA, dummy_prod)
              :: acc)
             (i - 1)
     in
     aux [] last
   in
   Grammar.extend
-    [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
+    [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e),
       None,
-      mk_level_list min_precedence max_precedence ]
-
+      mk_level_list min_precedence max_precedence ];
 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
+  begin
+  let level1_pattern = !grammars.level1_pattern in
 EXTEND
   GLOBAL: level1_pattern;
 
-  level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ];
-  l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
+  level1_pattern: [ 
+    [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ] 
+  ];
+  l1_pattern: [ 
+    [ p = LIST1 l1_simple_pattern -> 
+        fun l -> List.map (fun x -> x l) p ] 
+  ];
   literal: [
     [ s = SYMBOL -> `Symbol s
     | k = QKEYWORD -> `Keyword k
@@ -326,74 +442,113 @@ EXTEND
     ]
   ];
   sep:       [ [ "sep";      sep = literal -> sep ] ];
-(*   row_sep:   [ [ "rowsep";   sep = literal -> sep ] ];
-  field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *)
   l1_magic_pattern: [
-    [ "list0"; p = l1_simple_pattern; sep = OPT sep -> Ast.List0 (p, sep)
-    | "list1"; p = l1_simple_pattern; sep = OPT sep -> Ast.List1 (p, sep)
-    | "opt";   p = l1_simple_pattern -> Ast.Opt p
+    [ "list0"; p = l1_simple_pattern; sep = OPT sep -> 
+            fun l -> Ast.List0 (p l, sep)
+    | "list1"; p = l1_simple_pattern; sep = OPT sep -> 
+            fun l -> Ast.List1 (p l, sep)
+    | "opt";   p = l1_simple_pattern -> fun l -> Ast.Opt (p l)
     ]
   ];
   l1_pattern_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; id = IDENT -> 
+        Ast.TermVar (id, Ast.Level (int_of_string precedence))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     ]
   ];
+  mstyle: [ 
+    [ id = IDENT; 
+      v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
+  mpadded: [ 
+    [ id = IDENT; 
+      v = [ PERCENTAGE ] -> id, v]];
   l1_simple_pattern:
     [ "layout" LEFTA
-      [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Sub (p1, p2)))
-      | p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Sup (p1, p2)))
-      | p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Below (p1, p2)))
-      | p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Above (p1, p2)))
-      | p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Over (p1, p2)))
-      | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Atop (p1, p2)))
-(*       | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
-          return_term loc (Array (p, csep, rsep)) *)
-      | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
-          return_term loc (Ast.Layout (Ast.Frac (p1, p2)))
-      | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Ast.Layout (Ast.Sqrt p))
-      | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
-          return_term loc (Ast.Layout (Ast.Root (arg, index)))
+      [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\sup "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\below "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\above "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\over "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\atop "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
+      | p1 = SELF; SYMBOL "\\frac "; p2 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
+      | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
+      | SYMBOL "\\sqrt "; p = SELF -> 
+          return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
+      | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (Ast.Layout (Ast.Box ((Ast.H, false, false), p)))
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Box ((Ast.H, false, false), p l)))
       | "vbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (Ast.Layout (Ast.Box ((Ast.V, false, false), p)))
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Box ((Ast.V, false, false), p l)))
       | "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (Ast.Layout (Ast.Box ((Ast.HV, false, false), p)))
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Box ((Ast.HV, false, false), p l)))
       | "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p)))
-      | "break" -> return_term loc (Ast.Layout Ast.Break)
-(*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
+      | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
+      | "mstyle"; m = LIST1 mstyle ; LPAREN; t = l1_pattern; RPAREN ->
+          return_term_of_level loc 
+            (fun l -> 
+               Ast.Layout (Ast.Mstyle (m, t l)))
+      | "mpadded"; m = LIST1 mpadded ; LPAREN; t = l1_pattern; RPAREN ->
+          return_term_of_level loc 
+            (fun l -> 
+               Ast.Layout (Ast.Mpadded (m, t l)))
+      | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
+           return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
+              CicNotationUtil.group (x l)) m)))
       | LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.group p)
+          return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
       ]
     | "simple" NONA
-      [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
-      | m = l1_magic_pattern -> return_term loc (Ast.Magic m)
-      | v = l1_pattern_variable -> return_term loc (Ast.Variable v)
-      | l = literal -> return_term loc (Ast.Literal l)
+      [ i = IDENT -> 
+         return_term_of_level loc 
+           (fun l -> Ast.Variable (Ast.TermVar (i,Ast.Self l)))
+      | m = l1_magic_pattern -> 
+             return_term_of_level loc (fun l -> Ast.Magic (m l))
+      | v = l1_pattern_variable -> 
+             return_term_of_level loc (fun _ -> Ast.Variable v)
+      | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
       ]
     ];
   END
+  end;
 (* }}} *)
-
 (* {{{ Grammar for ast magics, notation level 2 *)
+  begin
+  let level2_meta = !grammars.level2_meta in
 EXTEND
   GLOBAL: level2_meta;
   l2_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; id = IDENT -> 
+        Ast.TermVar (id,Ast.Level (int_of_string precedence))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     | "fresh"; id = IDENT -> Ast.FreshVar id
-    | "anonymous" -> Ast.TermVar "_"
-    | id = IDENT -> Ast.TermVar id
+    | "anonymous" -> Ast.TermVar ("_",Ast.Self 0) (* is the level relevant?*)
+    | id = IDENT -> Ast.TermVar (id,Ast.Self 0)
     ]
   ];
   l2_magic: [
@@ -417,21 +572,28 @@ EXTEND
     ]
   ];
 END
+  end;
 (* }}} *)
-
 (* {{{ Grammar for ast patterns, notation level 2 *)
+  begin
+  let level2_ast = !grammars.level2_ast in
+  let term = !grammars.term in
+  let let_defs = !grammars.let_defs in
+  let protected_binder_vars = !grammars.protected_binder_vars in
 EXTEND
   GLOBAL: level2_ast term let_defs protected_binder_vars;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
+    | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
-    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+    [ SYMBOL "\\subst ";  (* to avoid catching frequent "a [1]" cases *)
       SYMBOL "[";
       substs = LIST1 [
         i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
@@ -451,21 +613,25 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
+    | id = PIDENT -> Ast.Ident (id, None), None
     | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident (id, None), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
         Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, None, []
+    [ SYMBOL "_" -> Ast.Wildcard
+    | id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
-    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
     ]
   ];
   binder: [
     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
-(*     | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
@@ -479,7 +645,7 @@ EXTEND
         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
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
@@ -490,15 +656,10 @@ EXTEND
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
         | _ -> failwith "Invalid index name."
     ]
   ];
-  induction_kind: [
-    [ "rec" -> `Inductive
-    | "corec" -> `CoInductive
-    ]
-  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -537,9 +698,11 @@ EXTEND
     ]
   ];
   binder_vars: [
-    [ vars = [
-          l = LIST1 single_arg SEP SYMBOL "," -> l
-        | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
+    [ vars = [ l =
+        [ l = LIST1 single_arg SEP SYMBOL "," -> l
+        | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
+            List.map (fun x -> Ast.Ident(x,None)) l
+      ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
   ];
@@ -552,27 +715,34 @@ EXTEND
     | vars = protected_binder_vars -> vars
     ]
   ];
-  term: LEVEL "10N" [ (* let in *)
-    [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+  term: LEVEL "10"
+  [
+    [ "let"; 
+     var = 
+      [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
+         id, Some typ
+      | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+         Ast.Ident(id,None), ty ];
+      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 (k, defs, body))
+        return_term loc (Ast.LetRec (`CoInductive, defs, body))
+    | LETREC; defs = let_defs; "in";
+      body = term ->
+        return_term loc (Ast.LetRec (`Inductive, defs, body))
     ]
   ];
-  term: LEVEL "20R"  (* binder *)
+  term: LEVEL "20"
     [
-      [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
+      [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
           return_term loc (fold_cluster b vars typ body)
-      | SYMBOL <:unicode<exists>> (* ∃ *);
-        (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
-          return_term loc (fold_exists vars typ body)
       ]
     ];
-  term: LEVEL "70L"  (* apply *)
+  term: LEVEL "70"
     [
-      [ p1 = term; p2 = term ->
+      [ p1 = term; p2 = term LEVEL "71" ->
           let rec aux = function
             | Ast.Appl (hd :: tl)
             | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
@@ -582,15 +752,17 @@ EXTEND
           return_term loc (Ast.Appl (aux p1 @ [p2]))
       ]
     ];
-  term: LEVEL "90N"  (* simple *)
+  term: LEVEL "90"
     [
       [ id = IDENT -> return_term loc (Ast.Ident (id, None))
       | id = IDENT; s = explicit_subst ->
           return_term loc (Ast.Ident (id, Some s))
       | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
       | u = URI -> return_term loc (Ast.Uri (u, None))
+      | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
       | n = NUMBER -> return_term loc (Ast.Num (n, 0))
-      | IMPLICIT -> return_term loc (Ast.Implicit)
+      | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+      | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
       | m = META; s = meta_substs ->
@@ -615,7 +787,31 @@ EXTEND
       ]
     ];
 END
+  end
 (* }}} *)
+;;
+
+let _ = initialize_grammars ();;
+
+let history = ref [];;
+
+let push () =
+  CicNotationLexer.push ();
+  history := (!owned_keywords,!grammars) :: !history;
+  owned_keywords := (initial_owned_keywords ());
+  grammars := initial_grammars ();
+  initialize_grammars ()
+;;
+
+let pop () =
+  CicNotationLexer.pop ();
+  match !history with
+  | [] -> assert false
+  | (kw,gram) :: old_history ->
+      owned_keywords := kw;
+      grammars := gram;
+      history := old_history
+;;
 
 (** {2 API implementation} *)
 
@@ -623,22 +819,24 @@ let exc_located_wrapper f =
   try
     f ()
   with
-  | Stdpp.Exc_located (floc, Stream.Error msg) ->
+  | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
+      raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
+  | Ploc.Exc (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 
-let parse_level1_pattern lexbuf =
+let parse_level1_pattern precedence lexbuf =
   exc_located_wrapper
-    (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+    (fun () -> Grammar.Entry.parse !grammars.level1_pattern (Obj.magic lexbuf) precedence)
 
 let parse_level2_ast lexbuf =
   exc_located_wrapper
-    (fun () -> Grammar.Entry.parse level2_ast (Obj.magic lexbuf))
+    (fun () -> Grammar.Entry.parse !grammars.level2_ast (Obj.magic lexbuf))
 
 let parse_level2_meta lexbuf =
   exc_located_wrapper
-    (fun () -> Grammar.Entry.parse level2_meta (Obj.magic lexbuf))
+    (fun () -> Grammar.Entry.parse !grammars.level2_meta (Obj.magic lexbuf))
 
 let _ =
   parse_level1_pattern_ref := parse_level1_pattern;
@@ -647,13 +845,19 @@ let _ =
 
 let parse_term lexbuf =
   exc_located_wrapper
-    (fun () -> (Grammar.Entry.parse term (Obj.magic lexbuf)))
+    (fun () -> (Grammar.Entry.parse !grammars.term (Obj.magic lexbuf)))
+
+let level2_ast_grammar () = !grammars.level2_ast_grammar
+let term  () = !grammars.term
+let let_defs  () = !grammars.let_defs
+let protected_binder_vars  () = !grammars.protected_binder_vars
+
 
 (** {2 Debugging} *)
 
 let print_l2_pattern () =
-  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
+  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj !grammars.term);
   Format.pp_print_flush Format.std_formatter ();
-  flush stdout
+  flush stdout  
 
 (* vim:set encoding=utf8 foldmethod=marker: *)