X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=4dcc772975b9e28287d3840b90bd640de4a067cf;hb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;hp=0c4ae0220719a998a664edb95b2e9b69f41f86e0;hpb=29aacd800408d16b9cb58dd58e603e31aa2ad511;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 0c4ae0220..4dcc77297 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -25,11 +25,28 @@
 
 open Printf
 
+open CicNotationEnv
+open CicNotationPt
+
 exception Parse_error of Token.flocation * string
 exception Level_not_found of int
 
 let grammar = Grammar.gcreate CicNotationLexer.notation_lexer
 
+let min_precedence = 0
+let max_precedence = 100
+let default_precedence = 50
+
+let let_in_prec = 10
+let binder_prec = 20
+let apply_prec = 70
+let simple_prec = 90
+
+let let_in_assoc = Gramext.NonA
+let binder_assoc = Gramext.RightA
+let apply_assoc = Gramext.LeftA
+let simple_assoc = Gramext.NonA
+
 let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
 let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
 let level3_term = Grammar.Entry.create grammar "level3_term"
@@ -37,13 +54,10 @@ let l2_pattern = Grammar.Entry.create grammar "l2_pattern"
 let notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *)
 let interpretation =
   Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *)
+let phrase = Grammar.Entry.create grammar "phrase"
 
 let return_term loc term = ()
 
-let loc_of_floc = function
-  | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
-      (loc_begin, loc_end)
-
 let fail floc msg =
   let (x, y) = loc_of_floc floc in
   failwith (sprintf "Error at characters %d - %d: %s" x y msg)
@@ -54,17 +68,197 @@ let int_of_string s =
   with Failure _ ->
     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
 
-open CicNotationPt
+(** {2 Grammar extension} *)
+
+let symbol s = Gramext.Stoken ("SYMBOL", s)
+let ident s = Gramext.Stoken ("IDENT", s)
+let number s = Gramext.Stoken ("NUMBER", s)
+let term = Gramext.Sself
+
+let g_symbol_of_literal =
+  function
+  | `Symbol s -> symbol s
+  | `Keyword s -> ident s
+  | `Number s -> number s
+
+type binding =
+  | NoBinding
+  | Binding of string * value_type
+  | Env of (string * value_type) list
+
+let make_action action bindings =
+  let rec aux (vl : CicNotationEnv.t) =
+    function
+      [] -> Gramext.action (fun (loc: location) -> action vl loc)
+    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+    (* LUCA: DEFCON 5 BEGIN *)
+    | Binding (name, TermType) :: tl ->
+        Gramext.action
+          (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
+    | Binding (name, StringType) :: tl ->
+        Gramext.action
+          (fun (v:string) ->
+            aux ((name, (StringType, StringValue v)) :: vl) tl)
+    | Binding (name, NumType) :: tl ->
+        Gramext.action
+          (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
+    | Binding (name, OptType t) :: tl ->
+        Gramext.action
+          (fun (v:'a option) ->
+            aux ((name, (OptType t, OptValue v)) :: vl) tl)
+    | Binding (name, ListType t) :: tl ->
+        Gramext.action
+          (fun (v:'a list) ->
+            aux ((name, (ListType t, ListValue v)) :: vl) tl)
+    | Env _ :: tl ->
+        Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
+    (* LUCA: DEFCON 5 END *)
+  in
+    aux [] (List.rev bindings)
 
-let boxify = function
-  | [ a ] -> a
-  | l -> Layout (Box (H, l))
+let flatten_opt =
+  let rec aux acc =
+    function
+      [] -> List.rev acc
+    | NoBinding :: tl -> aux acc tl
+    | Env names :: tl -> aux (List.rev names @ acc) tl
+    | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
+  in
+  aux []
+
+  (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
+let extract_term_production pattern =
+  let rec aux = function
+    | AttributedTerm (_, t) -> aux t
+    | Literal l -> aux_literal l
+    | Layout l -> aux_layout l
+    | Magic m -> aux_magic m
+    | Variable v -> aux_variable v
+    | t ->
+        prerr_endline (CicNotationPp.pp_term t);
+        assert false
+  and aux_literal =
+    function
+    | `Symbol s -> [NoBinding, symbol s]
+    | `Keyword s -> [NoBinding, ident s]
+    | `Number s -> [NoBinding, number s]
+  and aux_layout = function
+    | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
+    | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
+    | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
+    | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
+    | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
+    | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
+    | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
+    | Root (p1, p2) ->
+        [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
+        @ aux p1
+    | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
+(*     | Break -> [] *)
+    | Box (_, pl) -> List.flatten (List.map aux pl)
+  and aux_magic magic =
+    match magic with
+    | Opt p ->
+        let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
+        let action (env_opt : CicNotationEnv.t option) (loc : location) =
+          match env_opt with
+          | Some env -> List.map opt_binding_some env
+          | None -> List.map opt_binding_of_name p_names
+        in
+        [ Env (List.map opt_declaration p_names),
+          Gramext.srules
+            [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
+              Gramext.action action ] ]
+    | List0 (p, _)
+    | 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 : location) =
+          CicNotationEnv.coalesce_env p_names env_list
+        in
+        let g_symbol s =
+          match magic with
+          | List0 (_, None) -> Gramext.Slist0 s
+          | List1 (_, None) -> Gramext.Slist1 s
+          | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l)
+          | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l)
+          | _ -> assert false
+        in
+        [ Env (List.map list_declaration p_names),
+          Gramext.srules
+            [ [ g_symbol (Gramext.srules [ p_atoms, p_action ]) ],
+              Gramext.action action ] ]
+    | _ -> assert false
+  and aux_variable =
+    function
+    | NumVar s -> [Binding (s, NumType), number ""]
+    | TermVar s -> [Binding (s, TermType), term]
+    | IdentVar s -> [Binding (s, StringType), ident ""]
+    | Ascription (p, s) -> assert false (* TODO *)
+    | FreshVar _ -> assert false
+  and inner_pattern p =
+    let p_bindings, p_atoms = List.split (aux p) in
+    let p_names = flatten_opt p_bindings in
+    let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in
+    let action =
+      make_action (fun (env : CicNotationEnv.t) (loc : location) -> env)
+        p_bindings
+    in
+    p_bindings, p_atoms, p_names, action
+  in
+  aux pattern
+
+let level_of_int precedence =
+  if precedence < min_precedence || precedence > max_precedence then
+    raise (Level_not_found precedence);
+  string_of_int precedence
+
+type rule_id = Token.t Gramext.g_symbol list
+
+let extend level1_pattern ?(precedence = default_precedence)
+  ?associativity action
+=
+  let p_bindings, p_atoms =
+    List.split (extract_term_production level1_pattern)
+  in
+  let level = level_of_int precedence in
+  let p_names = flatten_opt p_bindings in
+  let _ =
+    prerr_endline (string_of_int (List.length p_bindings));
+    Grammar.extend
+      [ Grammar.Entry.obj (l2_pattern: 'a Grammar.Entry.e),
+        Some (Gramext.Level level),
+        [ None,
+          associativity,
+          [ p_atoms, 
+            (make_action
+              (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
+              p_bindings) ]]]
+  in
+  p_atoms
+
+let delete atoms = Grammar.delete_rule l2_pattern atoms
+
+(** {2 Grammar} *)
 
 let fold_binder binder pt_names body =
-  let fold_cluster binder names ty body =
+  let fold_cluster binder terms ty body =
     List.fold_right
-      (fun name body -> Binder (binder, (Cic.Name name, ty), body))
-      names body
+      (fun term body -> Binder (binder, (term, ty), body))
+      terms body  (* terms are names: either Ident or FreshVar *)
   in
   List.fold_right
     (fun (names, ty) body -> fold_cluster binder names ty body)
@@ -72,13 +266,27 @@ let fold_binder binder pt_names body =
 
 let return_term loc term = AttributedTerm (`Loc loc, term)
 
+let _ = (* create empty precedence level for "l2_pattern" *)
+  let mk_level_list first last =
+    let rec aux acc = function
+      | i when i < first -> acc
+      | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
+    in
+    aux [] last
+  in
+  Grammar.extend
+    [ Grammar.Entry.obj (l2_pattern: 'a Grammar.Entry.e),
+      None,
+      mk_level_list min_precedence max_precedence ]
+
 EXTEND
   GLOBAL: level1_pattern level2_pattern level3_term
           l2_pattern
-          notation interpretation;
+          notation interpretation
+          phrase;
 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
-  level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ];
-  l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
+  level1_pattern: [ [ p = l1_simple_pattern -> p ] ];
+  l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
   literal: [
     [ s = SYMBOL -> `Symbol s
     | k = KEYWORD -> `Keyword k
@@ -95,8 +303,7 @@ EXTEND
     ]
   ];
   l1_pattern_variable: [
-    [ id = IDENT -> TermVar id
-    | SYMBOL "\\TERM"; id = IDENT -> TermVar id
+    [ SYMBOL "\\TERM"; id = IDENT -> TermVar id
     | SYMBOL "\\NUM"; id = IDENT -> NumVar id
     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
     ]
@@ -111,38 +318,42 @@ EXTEND
           return_term loc (Layout (Below (p1, p2)))
       | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF ->
           return_term loc (Layout (Above (p1, p2)))
-      | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
-        SYMBOL "]" ->
-          return_term loc (Layout (Over (boxify p1, boxify p2)))
-      | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
-        SYMBOL "]" ->
-          return_term loc (Layout (Atop (boxify p1, boxify p2)))
+      | p1 = SELF; SYMBOL "\\OVER"; p2 = SELF ->
+          return_term loc (Layout (Over (p1, p2)))
+      | p1 = SELF; SYMBOL "\\ATOP"; p2 = SELF ->
+          return_term loc (Layout (Atop (p1, p2)))
 (*       | SYMBOL "\\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 (Layout (Frac (p1, p2)))
       | SYMBOL "\\SQRT"; p = SELF -> return_term loc (Layout (Sqrt p))
-      | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
-          return_term loc (Layout (Root (arg, Layout (Box (H, index)))))
-      | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
-          return_term loc (Layout (Box (H, p)))
-      | SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
-          return_term loc (Layout (Box (V, p)))
-      | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
-      | SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
-          return_term loc (boxify p)
-      | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
-          return_term loc (Variable (Ascription (Layout (Box (H, p)), id)))
+      | SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
+          return_term loc (Layout (Root (arg, index)));
+      | SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box ((H, false, false), p)))
+      | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box ((V, false, false), p)))
+      | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box ((HV, false, false), p)))
+      | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box ((HOV, false, false), p)))
+(*       | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *)
+(*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
+      | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (CicNotationUtil.boxify p)
+      | p = SELF; SYMBOL "\\AS"; id = IDENT ->
+          return_term loc (Variable (Ascription (p, id)))
       ]
     | "simple" NONA
-      [ m = l1_magic_pattern -> return_term loc (Magic m)
+      [ i = IDENT -> return_term loc (Ident (i, None))
+      | m = l1_magic_pattern -> return_term loc (Magic m)
       | v = l1_pattern_variable -> return_term loc (Variable v)
       | l = literal -> return_term loc (Literal l)
       ]
     ];
 (* }}} *)
 (* {{{ Grammar for ast patterns, notation level 2 *)
-  level2_pattern: [ [ p = l2_pattern; EOI -> p ] ];
+  level2_pattern: [ [ p = l2_pattern -> p ] ];
   sort: [
     [ SYMBOL "\\PROP" -> `Prop
     | SYMBOL "\\SET" -> `Set
@@ -150,17 +361,26 @@ EXTEND
     ]
   ];
   explicit_subst: [
-    [ (* TODO explicit substitution *)
+    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+      SYMBOL "[";
+      substs = LIST1 [
+        i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = l2_pattern -> (i, t)
+      ] SEP SYMBOL ";";
+      SYMBOL "]" ->
+        substs
     ]
   ];
   meta_subst: [
-    [ (* TODO meta substitution *)
-    ]
+    [ s = SYMBOL "_" -> None
+    | p = l2_pattern -> Some p ]
+  ];
+  meta_substs: [
+    [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ]
   ];
   possibly_typed_name: [
-    [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
-        Cic.Name id, Some typ
-    | id = IDENT -> Cic.Name id, None
+    [ SYMBOL "("; id = bound_name; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
+        id, Some typ
+    | id = bound_name -> id, None
     ]
   ];
   match_pattern: [
@@ -176,13 +396,18 @@ EXTEND
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
   ];
+  bound_name: [
+    [ i = IDENT -> Ident (i, None)
+    | SYMBOL "\\FRESH"; i = IDENT -> Variable (FreshVar i)
+    ]
+  ];
   bound_names: [
-    [ vars = LIST1 IDENT SEP SYMBOL ",";
+    [ vars = LIST1 bound_name SEP SYMBOL ",";
       ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
         [ vars, ty ]
     | clusters = LIST1 [
         SYMBOL "(";
-        vars = LIST1 IDENT SEP SYMBOL ",";
+        vars = LIST1 bound_name SEP SYMBOL ",";
         ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
         SYMBOL ")" ->
           vars, ty
@@ -197,8 +422,8 @@ EXTEND
   ];
   let_defs: [
     [ defs = LIST1 [
-        name = IDENT; args = bound_names;
-        index_name = OPT [ IDENT "on"; id = IDENT -> id ];
+        name = bound_name; args = bound_names;
+        index_name = OPT [ IDENT "on"; id = bound_name -> id ];
         ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
         SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
           let body = fold_binder `Lambda args body in
@@ -213,7 +438,9 @@ EXTEND
             | _ :: tl -> position_of name (p + 1) tl
           in
           let rec find_arg name n = function 
-            | [] -> fail loc (sprintf "Argument %s not found" name)
+            | [] ->
+                fail loc (sprintf "Argument %s not found"
+                  (CicNotationPp.pp_term name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -224,13 +451,14 @@ EXTEND
             | None -> 0 
             | Some name -> find_arg name 0 args
           in
-          (Cic.Name name, ty), body, index
+          (name, ty), body, index
       ] SEP IDENT "and" ->
         defs
     ]
   ];
   l2_pattern_variable: [
-    [ SYMBOL "\\NUM"; id = IDENT -> NumVar id
+    [ SYMBOL "\\TERM"; id = IDENT -> TermVar id
+    | SYMBOL "\\NUM"; id = IDENT -> NumVar id
     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
     | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
     ]
@@ -238,16 +466,18 @@ EXTEND
   l2_magic_pattern: [
     [ SYMBOL "\\FOLD";
       kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
-      base = l2_pattern;
-      SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern ->
+      DELIM "\\["; base = l2_pattern; DELIM "\\]";
+      SYMBOL "\\LAMBDA"; id = IDENT;
+      DELIM "\\["; recursive = l2_pattern; DELIM "\\]" ->
         Fold (kind, base, [id], recursive)
-    | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern ->
+    | SYMBOL "\\DEFAULT";
+      DELIM "\\["; some = l2_pattern; DELIM "\\]";
+      DELIM "\\["; none = l2_pattern; DELIM "\\]" ->
         Default (some, none)
     ]
   ];
-  l2_pattern:
-    [ "0" [ ]
-    | "10" NONA (* let in *)
+  l2_pattern: LEVEL "10"  (* let in *)
+    [ "10" NONA
       [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
         p1 = l2_pattern; "in"; p2 = l2_pattern ->
           return_term loc (LetIn (var, p1, p2))
@@ -255,15 +485,15 @@ EXTEND
         body = l2_pattern ->
           return_term loc (LetRec (k, defs, body))
       ]
-    | "20" RIGHTA (* binder *)
+    ];
+  l2_pattern: LEVEL "20"  (* binder *)
+    [ "20" RIGHTA
       [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
           return_term loc (fold_binder b names body)
       ]
-    | "30" [ ]
-    | "40" [ ]
-    | "50" [ ]
-    | "60" [ ]
-    | "70" LEFTA (* apply *)
+    ];
+  l2_pattern: LEVEL "70"  (* apply *)
+    [ "70" LEFTA
       [ p1 = l2_pattern; p2 = l2_pattern ->
           let rec aux = function
             | Appl (hd :: tl)
@@ -273,15 +503,17 @@ EXTEND
           in
           return_term loc (Appl (aux p1 @ [p2]))
       ]
-    | "80" [ ]
-    | "90" NONA (* simple *)
+    ];
+  l2_pattern: LEVEL "90"  (* simple *)
+    [ "90" NONA
       [ id = IDENT -> return_term loc (Ident (id, None))
       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+      | s = CSYMBOL -> return_term loc (Symbol (s, 0))
       | u = URI -> return_term loc (Uri (u, None))
-      | n = NUMBER -> prerr_endline "number"; return_term loc (Num (n, 0))
+      | n = NUMBER -> return_term loc (Num (n, 0))
       | IMPLICIT -> return_term loc (Implicit)
       | m = META -> return_term loc (Meta (int_of_string m, []))
-      | m = META; s = meta_subst -> return_term loc (Meta (int_of_string m, s))
+      | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
       | s = sort -> return_term loc (Sort s)
       | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
         IDENT "match"; t = l2_pattern;
@@ -300,20 +532,19 @@ EXTEND
       | v = l2_pattern_variable -> return_term loc (Variable v)
       | m = l2_magic_pattern -> return_term loc (Magic m)
       ]
-    | "100" [ ]
     ];
 (* }}} *)
 (* {{{ Grammar for interpretation, notation level 3 *)
   argument: [
-    [ id = IDENT -> IdentArg id
-    | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a)
-    | SYMBOL <:unicode<eta>> (* η *); id = IDENT; SYMBOL "."; a = SELF ->
-        EtaArg (Some id, a)
+    [ id = IDENT -> IdentArg (0, id)
+    | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
+      SYMBOL "."; id = IDENT ->
+        IdentArg (List.length l, id)
     ]
   ];
   level3_term: [
-    [ u = URI -> UriPattern u
-    | a = argument -> ArgPattern a
+    [ u = URI -> UriPattern (UriManager.uri_of_string u)
+    | id = IDENT -> VarPattern id
     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
         (match terms with
         | [] -> assert false
@@ -324,26 +555,42 @@ EXTEND
 (* }}} *)
 (* {{{ Notation glues *)
   associativity: [
-    [ IDENT "left";  IDENT "associative" -> `Left
-    | IDENT "right"; IDENT "associative" -> `Right
+    [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
+    | IDENT "right"; IDENT "associative" -> Gramext.RightA
+    | IDENT "non"; IDENT "associative" -> Gramext.NonA
     ]
   ];
-  precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ];
+  precedence: [
+    [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+  ];
   notation: [
-    [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern;
-      assoc = OPT associativity; prec = OPT precedence ->
-        ()
+    [ p1 = level1_pattern;
+      assoc = OPT associativity; prec = OPT precedence;
+      IDENT "for"; p2 = level2_pattern ->
+        (p1, assoc, prec, p2)
     ]
   ];
   interpretation: [
-    [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
-      t = level3_term ->
-        ()
+    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+        (s, args, t)
+    ]
+  ];
+(* }}} *)
+(* {{{ Top-level phrases *)
+  phrase: [
+    [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2
+    | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." ->
+        Notation (l1, assoc, prec, l2)
+    | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." ->
+        Interpretation ((symbol, args), l3)
+    | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u)
     ]
   ];
 (* }}} *)
 END
 
+(** {2 API implementation} *)
+
 let exc_located_wrapper f =
   try
     f ()
@@ -355,202 +602,14 @@ let exc_located_wrapper f =
 
 let parse_syntax_pattern stream =
   exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
-
 let parse_ast_pattern stream =
   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
-
 let parse_interpretation stream =
   exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
+let parse_phrase stream =
+  exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream)
 
-(** {2 Grammar extension} *)
-
-type associativity_kind = [ `Left | `Right | `None ]
-
-let symbol s = Gramext.Stoken ("SYMBOL", s)
-let ident s = Gramext.Stoken ("IDENT", s)
-let number s = Gramext.Stoken ("NUMBER", s)
-let term = Gramext.Sself
-
-type env_type = (string * (value_type * value)) list
-
-type binding =
-  | NoBinding
-  | Binding of string * value_type
-  | Env
-
-let rec pp_value =
-  function
-  | TermValue _ -> "@TERM@"
-  | StringValue s -> sprintf "\"%s\"" s
-  | NumValue n -> n
-  | OptValue (Some v) -> "Some " ^ pp_value v
-  | OptValue None -> "None"
-  | ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
-
-let rec pp_value_type =
-  function
-  | TermType -> "Term"
-  | StringType -> "String"
-  | NumType -> "Number"
-  | OptType t -> "Maybe " ^ pp_value_type t
-  | ListType l -> "List " ^ pp_value_type l
-
-let pp_env env =
-  String.concat "; "
-    (List.map
-      (fun (name, (ty, value)) ->
-        sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
-      env)
-
-let make_action action bindings =
-  let rec aux (vl : env_type) =
-    function
-      [] ->
-        prerr_endline "aux: make_action";
-        Gramext.action (fun (loc: location) -> action vl loc)
-    | NoBinding :: tl ->
-        prerr_endline "aux: none";
-        Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 3 BEGIN *)
-    | Binding (name, TermType) :: tl ->
-        prerr_endline "aux: term";
-        Gramext.action
-          (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl)
-    | Binding (name, StringType) :: tl ->
-        prerr_endline "aux: string";
-        Gramext.action
-          (fun (v:string) ->
-            aux ((name, (StringType, (StringValue v))) :: vl) tl)
-    | Binding (name, NumType) :: tl ->
-        prerr_endline "aux: num";
-        Gramext.action
-          (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl)
-    | Binding (name, OptType t) :: tl ->
-        prerr_endline "aux: opt";
-        Gramext.action
-          (fun (v:'a option) ->
-            aux ((name, (OptType t, (OptValue v))) :: vl) tl)
-    | Binding (name, ListType t) :: tl ->
-        prerr_endline "aux: list";
-        Gramext.action
-          (fun (v:'a list) ->
-            aux ((name, (ListType t, (ListValue v))) :: vl) tl)
-    | Env :: tl ->
-        prerr_endline "aux: env";
-        Gramext.action (fun (v:env_type) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 3 END *)
-  in
-    aux [] (List.rev bindings)
-
-let flatten_opt =
-  let rec aux acc =
-    function
-      [] -> List.rev acc
-    | (NoBinding | Env) :: tl -> aux acc tl
-    | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
-  in
-  aux []
-
-  (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
-let extract_term_production pattern =
-  let rec aux = function
-    | Literal l -> aux_literal l
-    | Layout l -> aux_layout l
-    | Magic m -> aux_magic m
-    | Variable v -> aux_variable v
-    | _ -> assert false
-  and aux_literal =
-    function
-    | `Symbol s -> [NoBinding, symbol s]
-    | `Keyword s -> [NoBinding, ident s]
-    | `Number s -> [NoBinding, number s]
-  and aux_layout = function
-    | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
-    | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
-    | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
-    | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
-    | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
-    | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
-    | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
-    | Root (p1, p2) ->
-        [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
-        @ aux p1
-    | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
-    | Box (_, pl) -> List.flatten (List.map aux pl)
-  and aux_magic = function
-    | Opt p ->
-        let p_bindings, p_atoms = List.split (aux p) in
-        let p_names = flatten_opt p_bindings in
-        [ Env,
-          Gramext.srules
-            [ [ Gramext.Sopt
-                  (Gramext.srules
-                    [ p_atoms,
-                      (make_action
-                        (fun (env : env_type) (loc : location) ->
-                          prerr_endline "inner opt action";
-                          env)
-                        p_bindings)])],
-              Gramext.action
-                (fun (env_opt : env_type option) (loc : location) ->
-                  Printf.printf "|p_names|=%d\n" (List.length p_names) ;
-                  flush stdout ;
-                  match env_opt with
-                    Some env ->
-                      Printf.printf "|env|=%d\n" (List.length env) ;
-                      flush stdout ;
-                      prerr_endline "opt action (Some _)";
-                      List.map
-                        (fun (name, (typ, v)) ->
-                          (name, (OptType typ, OptValue (Some v))))
-                        env
-                  | None -> 
-                      prerr_endline "opt action (None)";
-                      List.map
-                        (fun (name, typ) ->
-                          (name, (OptType typ, OptValue None)))
-                        p_names) ]]
-    | _ -> assert false
-  and aux_variable =
-    function
-    | NumVar s -> [Binding (s, NumType), number ""]
-    | TermVar s -> [Binding (s, TermType), term]
-    | IdentVar s -> [Binding (s, StringType), ident ""]
-    | Ascription (p, s) -> assert false (* TODO *)
-    | FreshVar _ -> assert false
-  in
-  aux pattern
-
-let level_of_int precedence =
-  (* TODO "mod" test to be removed as soon as we add all 100 levels *)
-  if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
-    raise (Level_not_found precedence);
-  string_of_int precedence
-
-type rule_id = Token.t Gramext.g_symbol list
-
-let extend level1_pattern ?(precedence = 0) ?associativity action =
-  let p_bindings, p_atoms =
-    List.split (extract_term_production level1_pattern)
-  in
-  let level = level_of_int precedence in
-  let p_names = flatten_opt p_bindings in
-  let entry = Grammar.Entry.obj (l2_pattern: 'a Grammar.Entry.e) in
-  let _ =
-    prerr_endline (string_of_int (List.length p_bindings));
-    Grammar.extend
-      [ entry, Some (Gramext.Level level),
-        [ Some level,  (* TODO should we put None here? *)
-          associativity,
-          [ p_atoms, 
-            (make_action
-              (fun (env: env_type) (loc: location) -> (action env loc))
-              p_bindings) ]]]
-  in
-  p_atoms
-
-let delete atoms = Grammar.delete_rule l2_pattern atoms
+(** {2 Debugging} *)
 
 let print_l2_pattern () =
   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);