matitaB/components/content_pres/cicNotationParser.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 module Ast = NotationPt
  31 module Env = NotationEnv
  32
  33 let prerr_endline _ = ()
  34
  35 exception Parse_error of string
  36 exception Level_not_found of int
  37
  38 let min_precedence = 0
  39 let max_precedence = 100
  40
  41 type ('a,'b,'c,'d,'e) grammars = {
  42   level1_pattern: 'a Grammar.Entry.e;
  43   level2_ast: 'b Grammar.Entry.e;
  44   level2_ast_grammar : Grammar.g;
  45   term: 'b Grammar.Entry.e;
  46   ident: 'e Grammar.Entry.e;
  47   sym_attributes: (string option * string option) Grammar.Entry.e;
  48   sym_table: (string * Stdpp.location Grammar.Entry.e) list;
  49   let_defs: 'c Grammar.Entry.e;
  50   let_codefs: 'c Grammar.Entry.e;
  51   protected_binder_vars: 'd Grammar.Entry.e;
  52   level2_meta: 'b Grammar.Entry.e;
  53 }
  54
  55 type checked_l1_pattern = CL1P of NotationPt.term * int
  56
  57 let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term
  58      ~refresh_uri_in_reference (CL1P (t,n))
  59 =
  60  CL1P (NotationUtil.refresh_uri_in_term ~refresh_uri_in_term
  61  ~refresh_uri_in_reference t, n)
  62
  63 type binding =
  64   | NoBinding
  65   | Binding of string * Env.value_type
  66   | Env of (string * Env.value_type) list
  67
  68 type db = {
  69   grammars:
  70     (int -> NotationPt.term,
  71     Ast.term,
  72     (Ast.term Ast.capture_variable list *
  73       Ast.term Ast.capture_variable * Ast.term * int) list,
  74     Ast.term list * Ast.term option, Env.ident_or_var) grammars;
  75   keywords: string list;
  76   items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list;
  77   loctable: (string option * string option) CicNotationLexer.LocalizeEnv.t ref
  78 }
  79
  80 let int_of_string s =
  81   try
  82     Pervasives.int_of_string s
  83   with Failure _ ->
  84     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  85
  86 (** {2 Grammar extension} *)
  87
  88 let level_of precedence =
  89   if precedence < min_precedence || precedence > max_precedence then
  90     raise (Level_not_found precedence);
  91   string_of_int precedence
  92
  93 let add_symbol_to_grammar_explicit level2_ast_grammar
  94     sym_attributes sym_table s =
  95   try
  96     let _ = List.assoc s sym_table
  97     in sym_table
  98   with Not_found ->
  99     let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in
 100     Grammar.extend
 101     [ Grammar.Entry.obj entry,
 102       None,
 103       [ None,
 104         Some (*Gramext.NonA*) Gramext.NonA,
 105         [ [Gramext.Stoken ("SYMBOL",s)], (* concrete l1 syntax *)
 106           (Gramext.action (fun _ loc -> None, loc))
 107         ; [Gramext.Stoken ("ATAG","")
 108           ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
 109           ;Gramext.Stoken ("SYMBOL","\005")
 110           ;Gramext.Stoken ("SYMBOL",s)
 111           ;Gramext.Stoken ("ATAGEND","")],
 112           (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
 113         ]]];
 114 (*  prerr_endline ("adding to grammar symbol " ^ s); *)
 115   (s,entry)::sym_table
 116
 117
 118 let add_symbol_to_grammar status s =
 119   let sym_attributes = status#notation_parser_db.grammars.sym_attributes in
 120   let sym_table = status#notation_parser_db.grammars.sym_table in
 121   let level2_ast_grammar =
 122     status#notation_parser_db.grammars.level2_ast_grammar
 123   in
 124   let sym_table =
 125     add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes sym_table s
 126   in
 127   let grammars =
 128     { status#notation_parser_db.grammars with sym_table = sym_table }
 129   in
 130   let notation_parser_db =
 131     { status#notation_parser_db with grammars = grammars } in
 132   status#set_notation_parser_db notation_parser_db
 133
 134 let gram_symbol status s =
 135   let sym_table = status#notation_parser_db.grammars.sym_table in
 136   let entry =
 137     try List.assoc s sym_table
 138     with Not_found ->
 139      (let syms = List.map fst (status#notation_parser_db.grammars.sym_table) in
 140       let syms = List.map (fun x -> "\"" ^ x ^ "\"") syms in
 141       prerr_endline ("new symbol non-terminals: " ^ (String.concat ", " syms));
 142       prerr_endline ("unable to find symbol \"" ^ s ^ "\""); assert false)
 143   in
 144   Gramext.Snterm (Grammar.Entry.obj entry)
 145
 146 let gram_ident status =
 147  Gramext.Snterm (Grammar.Entry.obj
 148   (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
 149   (*Gramext.Stoken ("IDENT", s)*)
 150 let gram_number s = Gramext.Stoken ("NUMBER", s)
 151 let gram_keyword s = Gramext.Stoken ("", s)
 152 let gram_term status = function
 153   | Ast.Self _ -> Gramext.Sself
 154   | Ast.Level precedence ->
 155       Gramext.Snterml
 156         (Grammar.Entry.obj
 157           (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
 158          level_of precedence)
 159 ;;
 160
 161 let gram_of_literal status =
 162   function
 163   | `Symbol (s,_) -> gram_symbol status s
 164   | `Keyword (s,_) -> gram_keyword s
 165   | `Number (s,_) -> gram_number s
 166
 167 let make_action status action bindings =
 168   let rec aux (vl : NotationEnv.t) =
 169     function
 170       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
 171     | NoBinding :: tl ->
 172         Gramext.action
 173          (fun (_,(loc: Ast.location)) ->
 174            let uri,desc =
 175              try
 176                CicNotationLexer.LocalizeEnv.find loc
 177                  !(status#notation_parser_db.loctable)
 178              with Not_found -> None, None
 179            in aux (("",(Env.NoType,
 180                Env.DisambiguationValue (loc,uri,desc)))::vl) tl)
 181     (* LUCA: DEFCON 3 BEGIN *)
 182     | Binding (name, Env.TermType l) :: tl ->
 183         Gramext.action
 184           (fun (v:Ast.term) ->
 185             aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
 186     | Binding (name, Env.StringType) :: tl ->
 187         Gramext.action
 188           (fun (v:Env.ident_or_var) ->
 189             aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
 190     | Binding (name, Env.NumType) :: tl ->
 191         Gramext.action
 192           (fun (v:string) ->
 193             aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
 194     | Binding (name, Env.OptType t) :: tl ->
 195         Gramext.action
 196           (fun (v:'a option) ->
 197             aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
 198     | Binding (name, Env.ListType t) :: tl ->
 199         Gramext.action
 200           (fun (v:'a list) ->
 201             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
 202     | Env _ :: tl ->
 203         Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl)
 204     | _ (* Binding (_,NoType) *) -> assert false
 205     (* LUCA: DEFCON 3 END *)
 206   in
 207     aux [] (List.rev bindings)
 208
 209 let flatten_opt =
 210   let rec aux acc =
 211     function
 212       [] -> List.rev acc
 213     | NoBinding :: tl -> aux acc tl
 214     | Env names :: tl -> aux (List.rev names @ acc) tl
 215     | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
 216   in
 217   aux []
 218
 219 (* given a level 1 pattern, adds productions for symbols when needed *)
 220 let update_sym_grammar status pattern =
 221   let rec aux status = function
 222     | Ast.AttributedTerm (_, t) -> aux status t
 223     | Ast.Literal l -> aux_literal status l
 224     | Ast.Layout l -> aux_layout status l
 225     | Ast.Magic m -> aux_magic status m
 226     | Ast.Variable v -> aux_variable status v
 227     | t ->
 228         prerr_endline (NotationPp.pp_term status t);
 229         assert false
 230   and aux_literal status =
 231     function
 232     | `Symbol (s,_) -> add_symbol_to_grammar status s
 233     | `Keyword _ -> status
 234     | `Number _ -> status
 235   and aux_layout status = function
 236     | Ast.Sub (p1, p2) -> aux (aux status p1) p2
 237     | Ast.Sup (p1, p2) -> aux (aux status p1) p2
 238     | Ast.Below (p1, p2) -> aux (aux status p1) p2
 239     | Ast.Above (p1, p2) -> aux (aux status p1) p2
 240     | Ast.Frac (p1, p2) -> aux (aux status p1) p2
 241     | Ast.InfRule (p1, p2, p3) -> aux (aux (aux status p1) p2) p3
 242     | Ast.Atop (p1, p2) -> aux (aux status p1) p2
 243     | Ast.Over (p1, p2) -> aux (aux status p1) p2
 244     | Ast.Root (p1, p2) -> aux (aux status p1) p2
 245     | Ast.Sqrt p -> aux status p
 246     | Ast.Break -> status
 247     | Ast.Box (_, pl) -> List.fold_left aux status pl
 248     | Ast.Group pl -> List.fold_left aux status pl
 249     | Ast.Mstyle (_,pl) -> List.fold_left aux status pl
 250     | Ast.Mpadded (_,pl) -> List.fold_left aux status pl
 251     | Ast.Maction l -> List.fold_left aux status l
 252   and aux_magic status magic =
 253     match magic with
 254     | Ast.Opt p -> aux status p
 255     | Ast.List0 (p, s)
 256     | Ast.List1 (p, s) ->
 257         let status =
 258           match s with None -> status | Some s' -> aux_literal status s'
 259         in
 260         aux status p
 261     | _ -> assert false
 262   and aux_variable status _ = status
 263   in
 264   aux status pattern
 265
 266   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
 267 let extract_term_production status pattern =
 268   let rec aux = function
 269     | Ast.AttributedTerm (_, t) -> aux t
 270     | Ast.Literal l -> aux_literal l
 271     | Ast.Layout l -> aux_layout l
 272     | Ast.Magic m -> aux_magic m
 273     | Ast.Variable v -> aux_variable v
 274     | t ->
 275         prerr_endline (NotationPp.pp_term status t);
 276         assert false
 277   and aux_literal =
 278     function
 279     | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
 280     | `Keyword (s,_) ->
 281         (* assumption: s will be registered as a keyword with the lexer *)
 282         [NoBinding, gram_keyword s]
 283     | `Number (s,_) -> [NoBinding, gram_number s]
 284   and aux_layout = function
 285     | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
 286     | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
 287     | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2
 288     | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2
 289     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2
 290     | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
 291     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2
 292     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2
 293     | Ast.Root (p1, p2) ->
 294         [NoBinding, gram_symbol status "\\root "] @ aux p2
 295         @ [NoBinding, gram_symbol status "\\of "] @ aux p1
 296     | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p
 297     | Ast.Break -> []
 298     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
 299     | Ast.Group pl -> List.flatten (List.map aux pl)
 300     | Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
 301     | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
 302     | Ast.Maction l -> List.flatten (List.map aux l)
 303   and aux_magic magic =
 304     match magic with
 305     | Ast.Opt p ->
 306         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
 307         let action (env_opt : NotationEnv.t option) (loc : Ast.location) =
 308           match env_opt with
 309           | Some env -> List.map Env.opt_binding_some env
 310           | None -> List.map Env.opt_binding_of_name p_names
 311         in
 312         [ Env (List.map Env.opt_declaration p_names),
 313           Gramext.srules
 314             [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
 315               Gramext.action action ] ]
 316     | Ast.List0 (p, _)
 317     | Ast.List1 (p, _) ->
 318         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
 319         let action (env_list : NotationEnv.t list) (loc : Ast.location) =
 320           NotationEnv.coalesce_env p_names env_list
 321         in
 322         let gram_of_list s =
 323           match magic with
 324           | Ast.List0 (_, None) -> Gramext.Slist0 s
 325           | Ast.List1 (_, None) -> Gramext.Slist1 s
 326           | Ast.List0 (_, Some l) ->
 327               Gramext.Slist0sep (s, gram_of_literal status l,true)
 328           | Ast.List1 (_, Some l) ->
 329               Gramext.Slist1sep (s, gram_of_literal status l,true)
 330           | _ -> assert false
 331         in
 332         [ Env (List.map Env.list_declaration p_names),
 333           Gramext.srules
 334             [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
 335               Gramext.action action ] ]
 336     | _ -> assert false
 337   and aux_variable =
 338     function
 339     | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
 340     | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) ->
 341         [Binding (s, Env.TermType level), gram_term status lv]
 342     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident status]
 343     | Ast.Ascription (p, s) -> assert false (* TODO *)
 344     | Ast.FreshVar _ -> assert false
 345   and inner_pattern p =
 346     let p_bindings, p_atoms = List.split (aux p) in
 347     let p_names = flatten_opt p_bindings in
 348     let action =
 349       make_action status
 350         (fun (env : NotationEnv.t) (loc : Ast.location) -> env) p_bindings
 351     in
 352     p_bindings, p_atoms, p_names, action
 353   in
 354   aux pattern
 355
 356 type rule_id = Grammar.token Gramext.g_symbol list
 357
 358 let compare_rule_id x y =
 359   let rec aux = function
 360     | [],[] -> 0
 361     | [],_ -> ~-1
 362     | _,[] -> 1
 363     | ((s1::tl1) as x),((s2::tl2) as y) ->
 364         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
 365         else Pervasives.compare x y
 366   in
 367     aux (x,y)
 368
 369
 370 let check_l1_pattern level1_pattern pponly level associativity =
 371   let variables = ref 0 in
 372   let symbols = ref 0 in
 373   let rec aux = function
 374     | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t)
 375     | Ast.Literal _ as l -> incr symbols; l
 376     | Ast.Layout l -> Ast.Layout (aux_layout l)
 377     | Ast.Magic m -> Ast.Magic (aux_magic m)
 378     | Ast.Variable v -> (aux_variable v)
 379     | t -> assert false
 380   and aux_layout = function
 381     | Ast.Sub (p1, p2)   -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
 382     | Ast.Sup (p1, p2)   -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (p1, p2)
 383     | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
 384     | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
 385     | Ast.Frac (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
 386     | 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)
 387     | Ast.Atop (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
 388     | Ast.Over (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
 389     | Ast.Root (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
 390     | Ast.Sqrt p -> Ast.Sqrt (aux p)
 391     | Ast.Break as t -> t
 392     | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
 393     | Ast.Group pl -> Ast.Group (List.map aux pl)
 394     | Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
 395     | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
 396     | Ast.Maction l as t ->
 397         if not pponly then
 398         raise(Parse_error("Maction can be used only in output notations"))
 399         else t
 400   and aux_magic magic =
 401     match magic with
 402     | Ast.Opt p -> Ast.Opt (aux p)
 403     | Ast.List0 (p, x) -> Ast.List0 (aux p, x)
 404     | Ast.List1 (p, x) -> Ast.List1 (aux p, x)
 405     | _ -> assert false
 406   and aux_variable =
 407     function
 408     | Ast.NumVar _ as t -> Ast.Variable t
 409     | Ast.TermVar (s,Ast.Self _) when associativity <> Gramext.NonA ->
 410         incr variables;
 411         if !variables > 2 then
 412           raise (Parse_error ("Exactly 2 variables must be specified in an "^
 413           "associative notation"));
 414         (match !variables, associativity with
 415         | 1,Gramext.LeftA ->
 416              Ast.Variable (Ast.TermVar (s, Ast.Self level))
 417         | 1,Gramext.RightA ->
 418              Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
 419         | 2,Gramext.LeftA ->
 420              Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
 421         | 2,Gramext.RightA ->
 422              Ast.Variable (Ast.TermVar (s, Ast.Level (level-1)))
 423         | _ -> assert false)
 424     | Ast.TermVar (s,Ast.Level _) when associativity <> Gramext.NonA ->
 425           raise (Parse_error ("Variables can not be declared with a " ^
 426             "precedence in an associative notation"))
 427        (*avoid camlp5 divergence due to non-Sself recursion at the same level *)
 428     | Ast.TermVar (s,Ast.Level l) when l<=level && !variables=0 && !symbols=0->
 429        raise(Parse_error("Left recursive rule with precedence not greater " ^
 430         "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
 431     | Ast.TermVar _ as t -> incr variables; Ast.Variable t
 432     | Ast.IdentVar _ as t -> Ast.Variable t
 433     | Ast.Ascription _ -> assert false (* TODO *)
 434     | Ast.FreshVar _ -> assert false
 435   in
 436   if associativity <> Gramext.NonA && level = min_precedence then
 437     raise (Parse_error ("You can not specify an associative notation " ^
 438     "at level "^string_of_int min_precedence ^ "; increase it"));
 439   let cp = aux level1_pattern in
 440 (*   prerr_endline ("checked_pattern: " ^ NotationPp.pp_term cp); *)
 441   if !variables <> 2 && associativity <> Gramext.NonA then
 442     raise (Parse_error ("Exactly 2 variables must be specified in an "^
 443      "associative notation"));
 444   CL1P (cp,level)
 445 ;;
 446
 447 (** {2 Grammar} *)
 448
 449 let fold_cluster binder terms ty body =
 450   List.fold_right
 451     (fun term body -> Ast.Binder (binder, (term, ty), body))
 452     terms body  (* terms are names: either Ident or FreshVar *)
 453
 454 let fold_exists terms ty body =
 455   List.fold_right
 456     (fun term body ->
 457       let lambda = Ast.Binder (`Lambda, (term, ty), body) in
 458       Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
 459     terms body
 460
 461 let fold_binder binder pt_names body =
 462   List.fold_right
 463     (fun (names, ty) body -> fold_cluster binder names ty body)
 464     pt_names body
 465
 466 let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
 467 let return_term_of_level loc term l =
 468   Ast.AttributedTerm (`Loc loc, term l)
 469
 470 (** {2 API implementation} *)
 471
 472 let exc_located_wrapper f =
 473   try
 474     f ()
 475   with
 476   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 477       raise (HExtlib.Localized (floc, Parse_error msg))
 478   | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
 479       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 480   | Stdpp.Exc_located (floc, exn) ->
 481       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 482
 483 let parse_level1_pattern grammars precedence lexbuf =
 484   exc_located_wrapper
 485     (fun () -> Grammar.Entry.parse grammars.level1_pattern (Obj.magic lexbuf) precedence)
 486
 487 let parse_level2_ast grammars lexbuf =
 488   exc_located_wrapper
 489     (fun () ->
 490             Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf))
 491
 492 let parse_level2_meta grammars lexbuf =
 493   exc_located_wrapper
 494     (fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
 495
 496   (* create empty precedence level for "term" *)
 497 let initialize_grammars loctable grammars =
 498   let dummy_action =
 499     Gramext.action (fun _ ->
 500       failwith "internal error, lexer generated a dummy token")
 501   in
 502   (* Needed since campl4 on "delete_rule" remove the precedence level if it gets
 503    * empty after the deletion. The lexer never generate the Stoken below. *)
 504   let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
 505   let mk_level_list first last =
 506     let rec aux acc = function
 507       | i when i < first -> acc
 508       | i ->
 509           aux
 510             ((Some (level_of i), Some Gramext.NonA, dummy_prod)
 511              :: acc)
 512             (i - 1)
 513     in
 514     aux [] last
 515   in
 516   Grammar.extend
 517     [ Grammar.Entry.obj (grammars.term: 'a Grammar.Entry.e),
 518       None,
 519       mk_level_list min_precedence max_precedence ];
 520 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
 521   begin
 522   let level1_pattern = grammars.level1_pattern in
 523 EXTEND
 524   GLOBAL: level1_pattern;
 525
 526   level1_pattern: [
 527     [ p = l1_pattern; EOI -> fun l -> NotationUtil.boxify (p l) ]
 528   ];
 529   l1_pattern: [
 530     [ p = LIST1 l1_simple_pattern ->
 531         fun l -> List.map (fun x -> x l) p ]
 532   ];
 533   literal: [
 534     [ s = SYMBOL -> `Symbol (s, (None,None))
 535     | k = QKEYWORD -> `Keyword (k, (None,None))
 536     | n = NUMBER -> `Number (n,(None,None))
 537     ]
 538   ];
 539   sep:       [ [ "sep";      sep = literal -> sep ] ];
 540   l1_magic_pattern: [
 541     [ "list0"; p = l1_simple_pattern; sep = OPT sep ->
 542             fun l -> Ast.List0 (p l, sep)
 543     | "list1"; p = l1_simple_pattern; sep = OPT sep ->
 544             fun l -> Ast.List1 (p l, sep)
 545     | "opt";   p = l1_simple_pattern -> fun l -> Ast.Opt (p l)
 546     ]
 547   ];
 548   l1_pattern_variable: [
 549     [ "term"; precedence = NUMBER; id = IDENT ->
 550         Ast.TermVar (id, Ast.Level (int_of_string precedence))
 551     | "number"; id = IDENT -> Ast.NumVar id
 552     | "ident"; id = IDENT -> Ast.IdentVar id
 553     ]
 554   ];
 555   mstyle: [
 556     [ id = IDENT;
 557       v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
 558   mpadded: [
 559     [ id = IDENT;
 560       v = [ PERCENTAGE ] -> id, v]];
 561   l1_simple_pattern:
 562     [ "layout" LEFTA
 563       [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF ->
 564           return_term_of_level loc
 565             (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
 566       | p1 = SELF; SYMBOL "\\sup "; p2 = SELF ->
 567           return_term_of_level loc
 568             (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
 569       | p1 = SELF; SYMBOL "\\below "; p2 = SELF ->
 570           return_term_of_level loc
 571             (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
 572       | p1 = SELF; SYMBOL "\\above "; p2 = SELF ->
 573           return_term_of_level loc
 574             (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
 575       | p1 = SELF; SYMBOL "\\over "; p2 = SELF ->
 576           return_term_of_level loc
 577             (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
 578       | p1 = SELF; SYMBOL "\\atop "; p2 = SELF ->
 579           return_term_of_level loc
 580             (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
 581       | p1 = SELF; SYMBOL "\\frac "; p2 = SELF ->
 582           return_term_of_level loc
 583             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
 584       | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF ->
 585           return_term_of_level loc
 586             (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
 587       | SYMBOL "\\sqrt "; p = SELF ->
 588           return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
 589       | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF ->
 590           return_term_of_level loc
 591             (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
 592       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
 593           return_term_of_level loc
 594             (fun l -> Ast.Layout (Ast.Box ((Ast.H, false, false), p l)))
 595       | "vbox"; LPAREN; p = l1_pattern; RPAREN ->
 596           return_term_of_level loc
 597             (fun l -> Ast.Layout (Ast.Box ((Ast.V, false, false), p l)))
 598       | "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
 599           return_term_of_level loc
 600             (fun l -> Ast.Layout (Ast.Box ((Ast.HV, false, false), p l)))
 601       | "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
 602           return_term_of_level loc
 603             (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
 604       | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
 605       | "mstyle"; m = LIST1 mstyle ; LPAREN; t = l1_pattern; RPAREN ->
 606           return_term_of_level loc
 607             (fun l ->
 608                Ast.Layout (Ast.Mstyle (m, t l)))
 609       | "mpadded"; m = LIST1 mpadded ; LPAREN; t = l1_pattern; RPAREN ->
 610           return_term_of_level loc
 611             (fun l ->
 612                Ast.Layout (Ast.Mpadded (m, t l)))
 613       | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
 614            return_term_of_level loc
 615             (fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
 616               NotationUtil.group (x l)) m)))
 617       | LPAREN; p = l1_pattern; RPAREN ->
 618           return_term_of_level loc (fun l -> NotationUtil.group (p l))
 619       ]
 620     | "simple" NONA
 621       [ i = IDENT ->
 622          return_term_of_level loc
 623            (fun l -> Ast.Variable (Ast.TermVar (i,Ast.Self l)))
 624       | m = l1_magic_pattern ->
 625              return_term_of_level loc (fun l -> Ast.Magic (m l))
 626       | v = l1_pattern_variable ->
 627              return_term_of_level loc (fun _ -> Ast.Variable v)
 628       | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
 629       ]
 630     ];
 631   END
 632   end;
 633 (* }}} *)
 634 (* {{{ Grammar for ast magics, notation level 2 *)
 635   begin
 636   let level2_meta = grammars.level2_meta in
 637 EXTEND
 638   GLOBAL: level2_meta;
 639   l2_variable: [
 640     [ "term"; precedence = NUMBER; id = IDENT ->
 641         Ast.TermVar (id,Ast.Level (int_of_string precedence))
 642     | "number"; id = IDENT -> Ast.NumVar id
 643     | "ident"; id = IDENT -> Ast.IdentVar id
 644     | "fresh"; id = IDENT -> Ast.FreshVar id
 645     | "anonymous" -> Ast.TermVar ("_",Ast.Self 0) (* is the level relevant?*)
 646     | id = IDENT -> Ast.TermVar (id,Ast.Self 0)
 647     ]
 648   ];
 649   l2_magic: [
 650     [ "fold"; kind = [ "left" -> `Left | "right" -> `Right ];
 651       base = level2_meta; "rec"; id = IDENT; recursive = level2_meta ->
 652         Ast.Fold (kind, base, [id], recursive)
 653     | "default"; some = level2_meta; none = level2_meta ->
 654         Ast.Default (some, none)
 655     | "if"; p_test = level2_meta;
 656       "then"; p_true = level2_meta;
 657       "else"; p_false = level2_meta ->
 658         Ast.If (p_test, p_true, p_false)
 659     | "fail" -> Ast.Fail
 660     ]
 661   ];
 662   level2_meta: [
 663     [ magic = l2_magic -> Ast.Magic magic
 664     | var = l2_variable -> Ast.Variable var
 665     | blob = UNPARSED_AST ->
 666         parse_level2_ast grammars (Ulexing.from_utf8_string blob)
 667     ]
 668   ];
 669 END
 670   end;
 671 (* }}} *)
 672 (* {{{ Grammar for ast patterns, notation level 2 *)
 673   begin
 674   let level2_ast = grammars.level2_ast in
 675   let term = grammars.term in
 676   let atag_attributes = grammars.sym_attributes in
 677   let let_defs = grammars.let_defs in
 678   let let_codefs = grammars.let_codefs in
 679   let ident = grammars.ident in
 680   let protected_binder_vars = grammars.protected_binder_vars in
 681 EXTEND
 682   GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident atag_attributes;
 683   level2_ast: [ [ p = term -> p ] ];
 684   sort: [
 685     [ "Prop" -> `Prop
 686     | "Set" -> `Set
 687     | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
 688     | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
 689     ]
 690   ];
 691   meta_subst: [
 692     [ s = SYMBOL "_" -> None
 693     | p = term -> Some p ]
 694   ];
 695   meta_substs: [
 696     [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ]
 697   ];
 698   possibly_typed_name: [
 699     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
 700         id, Some typ
 701     | arg = single_arg -> arg, None
 702     | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
 703     | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
 704     | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
 705         Ast.Ident (id, `Ambiguous), Some typ
 706     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
 707         Ast.Ident ("_", `Ambiguous), Some typ
 708     ]
 709   ];
 710   match_pattern: [
 711     [ SYMBOL "_" -> Ast.Wildcard
 712     | id = IDENT -> Ast.Pattern (id, None, [])
 713     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
 714        Ast.Pattern (id, None, vars)
 715     | id = IDENT; vars = LIST1 possibly_typed_name ->
 716        Ast.Pattern (id, None, vars)
 717     ]
 718   ];
 719   binder: [
 720     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
 721     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
 722     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
 723     ]
 724   ];
 725   gident: [
 726     [ id = IDENT ->
 727        try
 728          let uri,_ = CicNotationLexer.LocalizeEnv.find loc
 729            !loctable in
 730          match uri with
 731          | Some u ->
 732             prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u);
 733                          id, `Uri u
 734          | None ->
 735             prerr_endline ("identificatore ambiguo: " ^ id);
 736                          id, `Ambiguous
 737        with
 738        | Not_found ->
 739             prerr_endline ("identificatore non trovato: " ^ id);
 740                        id, `Ambiguous ]];
 741   gnum: [
 742     [ n = NUMBER ->
 743        try
 744          match CicNotationLexer.LocalizeEnv.find loc !loctable with
 745          | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr)
 746          | _ -> n,None
 747        with
 748        | Not_found -> n,None ]];
 749   arg: [
 750     [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
 751       SYMBOL ":"; ty = term; RPAREN ->
 752         List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty
 753     | (name,uri) = gident -> [Ast.Ident (name,uri)], None
 754     | blob = UNPARSED_META ->
 755         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
 756         match meta with
 757         | Ast.Variable (Ast.FreshVar _) -> [meta], None
 758         | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
 759         | _ -> failwith "Invalid bound name."
 760    ]
 761   ];
 762   single_arg: [
 763     [ (name,uri) = gident -> Ast.Ident (name,uri)
 764     | blob = UNPARSED_META ->
 765         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
 766         match meta with
 767         | Ast.Variable (Ast.FreshVar _)
 768         | Ast.Variable (Ast.IdentVar _) -> meta
 769         | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
 770         | _ -> failwith "Invalid index name."
 771     ]
 772   ];
 773   ident: [
 774     [ name = IDENT -> Env.Ident name
 775     | blob = UNPARSED_META ->
 776         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
 777         match meta with
 778         | Ast.Variable (Ast.FreshVar _) ->
 779            (* it makes sense: extend Env.ident_or_var *)
 780             assert false
 781         | Ast.Variable (Ast.IdentVar name) -> Env.Var name
 782         | Ast.Variable (Ast.TermVar ("_",_)) -> Env.Var "_"
 783         | _ -> failwith ("Invalid index name: " ^ blob)
 784     ]
 785   ];
 786   let_defs: [
 787     [ defs = LIST1 [
 788         name = single_arg;
 789         args = LIST1 arg;
 790         index_name = OPT [ "on"; id = single_arg -> id ];
 791         ty = OPT [ SYMBOL ":" ; p = term -> p ];
 792         SYMBOL <:unicode<def>> (* ≝ *); body = term ->
 793           let rec position_of name p = function
 794             | [] -> None, p
 795             | n :: _ when n = name -> Some p, p
 796             | _ :: tl -> position_of name (p + 1) tl
 797           in
 798           let rec find_arg name n = function
 799             | [] ->
 800                 (* CSC: new NCicPp.status is the best I can do here
 801                    without changing the return type *)
 802                 Ast.fail loc (sprintf "Argument %s not found"
 803                   (NotationPp.pp_term (new NCicPp.status None) name))
 804             | (l,_) :: tl ->
 805                 (match position_of name 0 l with
 806                 | None, len -> find_arg name (n + len) tl
 807                 | Some where, len -> n + where)
 808           in
 809           let index =
 810             match index_name with
 811             | None -> 0
 812             | Some index_name -> find_arg index_name 0 args
 813           in
 814           let args =
 815            List.concat
 816             (List.map
 817              (function (names,ty) -> List.map (function x -> x,ty) names
 818              ) args)
 819           in
 820            args, (name, ty), body, index
 821       ] SEP "and" ->
 822         defs
 823     ]
 824   ];
 825   binder_vars: [
 826     [ vars = [ l =
 827         [ l = LIST1 single_arg SEP SYMBOL "," -> l
 828         | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," ->
 829             List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
 830       ] -> l ];
 831       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
 832     ]
 833   ];
 834   protected_binder_vars: [
 835     [ LPAREN; vars = binder_vars; RPAREN -> vars
 836     ]
 837   ];
 838   maybe_protected_binder_vars: [
 839     [ vars = binder_vars -> vars
 840     | vars = protected_binder_vars -> vars
 841     ]
 842   ];
 843   term: LEVEL "10"
 844   [
 845     [ "let";
 846      var =
 847       [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
 848           id, Some typ
 849       | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
 850           Ast.Ident (id,uri), ty ];
 851       SYMBOL <:unicode<def>> (* ≝ *);
 852       p1 = term; "in"; p2 = term ->
 853         return_term loc (Ast.LetIn (var, p1, p2))
 854     | LETCOREC; defs = let_defs; "in";
 855       body = term ->
 856         return_term loc (Ast.LetRec (`CoInductive, defs, body))
 857     | LETREC; defs = let_defs; "in";
 858       body = term ->
 859         return_term loc (Ast.LetRec (`Inductive, defs, body))
 860     ]
 861   ];
 862   term: LEVEL "20"
 863     [
 864       [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
 865           return_term loc (fold_cluster b vars typ body)
 866       ]
 867     ];
 868   term: LEVEL "70"
 869     [
 870       [ p1 = term; p2 = term LEVEL "71" ->
 871           let rec aux = function
 872             | Ast.Appl (hd :: tl)
 873             | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
 874                 aux hd @ tl
 875             | term -> [term]
 876           in
 877           return_term loc (Ast.Appl (aux p1 @ [p2]))
 878       ]
 879     ];
 880   term: LEVEL "90"
 881     [
 882       [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri))
 883       | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
 884       | u = URI -> return_term loc (Ast.Ident
 885                      (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
 886       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
 887       | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr))
 888       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
 889       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
 890       | PLACEHOLDER -> return_term loc Ast.UserInput
 891       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
 892       | m = META; s = meta_substs ->
 893           return_term loc (Ast.Meta (int_of_string m, s))
 894       | s = sort -> return_term loc (Ast.Sort s)
 895       | "match"; t = term;
 896         indty_ident = OPT [ "in"; id = IDENT -> id, None ];
 897         outtyp = OPT [ "return"; ty = term -> ty ];
 898         "with"; SYMBOL "[";
 899         patterns = LIST0 [
 900           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 901           rhs = term ->
 902             lhs, rhs
 903         ] SEP SYMBOL "|";
 904         SYMBOL "]" ->
 905           return_term loc (Ast.Case (t, indty_ident, outtyp, patterns))
 906       | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
 907           return_term loc (Ast.Cast (p1, p2))
 908       | LPAREN; p = term; RPAREN -> p
 909       | blob = UNPARSED_META ->
 910           parse_level2_meta grammars (Ulexing.from_utf8_string blob)
 911       ]
 912     ];
 913 END
 914   end;
 915 (* }}} *)
 916   grammars
 917 ;;
 918
 919 let initial_grammars loctable keywords =
 920   let lexers = CicNotationLexer.mk_lexers loctable keywords in
 921   let level1_pattern_grammar =
 922     Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in
 923   let level2_ast_grammar =
 924     Grammar.gcreate lexers.CicNotationLexer.level2_ast_lexer in
 925   let level2_meta_grammar =
 926     Grammar.gcreate lexers.CicNotationLexer.level2_meta_lexer in
 927   let level1_pattern =
 928     Grammar.Entry.create level1_pattern_grammar "level1_pattern" in
 929   let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
 930   let term = Grammar.Entry.create level2_ast_grammar "term" in
 931   let ident = Grammar.Entry.create level2_ast_grammar "ident" in
 932   (* unexpanded TeX macros terminated by a space (see comment in
 933    * CicNotationLexer) *)
 934   let initial_symbols =
 935     ["\\sub ";"\\sup ";"\\below ";"\\above ";"\\frac "
 936     ;"\\infrule ";"\\atop ";"\\over ";"\\root ";"\\of ";"\\sqrt "] in
 937   let sym_attributes =
 938     Grammar.Entry.create level2_ast_grammar "atag_attributes" in
 939   let sym_table =
 940     List.fold_left
 941       (add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes)
 942       [] initial_symbols
 943   in
 944   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
 945   let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
 946   let protected_binder_vars =
 947     Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
 948   let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
 949   initialize_grammars loctable
 950   { level1_pattern=level1_pattern;
 951     level2_ast=level2_ast;
 952     term=term;
 953     ident=ident;
 954     sym_table=sym_table;
 955     sym_attributes=sym_attributes;
 956     let_defs=let_defs;
 957     let_codefs=let_codefs;
 958     protected_binder_vars=protected_binder_vars;
 959     level2_meta=level2_meta;
 960     level2_ast_grammar=level2_ast_grammar;
 961   }
 962 ;;
 963
 964 class type g_status =
 965  object
 966   method notation_parser_db: db
 967  end
 968
 969 class status0 ~keywords:kwds =
 970  object
 971   val db =
 972     let lt = ref CicNotationLexer.LocalizeEnv.empty in
 973     { grammars = initial_grammars lt kwds; keywords = kwds;
 974       items = []; loctable = lt }
 975   method notation_parser_db = db
 976   method set_notation_parser_db v = {< db = v >}
 977   method set_notation_parser_status
 978    : 'status. #g_status as 'status -> 'self
 979    = fun o -> {< db = o#notation_parser_db >}
 980   method reset_loctable () =
 981     db.loctable := CicNotationLexer.LocalizeEnv.empty
 982  end
 983
 984 class virtual status uid ~keywords:kwds =
 985  object
 986   inherit NCic.status uid
 987   inherit status0 kwds
 988  end
 989
 990 let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
 991         (* move inside constructor XXX *)
 992   let add1item status (level, level1_pattern, action) =
 993     let status = update_sym_grammar status level1_pattern in
 994     let p_bindings, p_atoms =
 995       List.split (extract_term_production status level1_pattern)
 996     in
 997     Grammar.extend
 998       [ Grammar.Entry.obj
 999         (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
1000         Some (Gramext.Level level),
1001         [ None,
1002           Some (*Gramext.NonA*) Gramext.NonA,
1003           [ p_atoms, (* concrete l1 syntax *)
1004             (make_action status
1005               (fun (env: NotationEnv.t) (loc: Ast.location) ->
1006                 (action env loc))
1007               p_bindings) ]]];
1008     status
1009   in
1010   let current_item =
1011     let level = level_of precedence in
1012     level, level1_pattern, action in
1013   let keywords = NotationUtil.keywords_of_term level1_pattern @
1014     status#notation_parser_db.keywords in
1015   let items = current_item :: status#notation_parser_db.items in
1016   let status = status#set_notation_parser_status (new status0 ~keywords) in
1017   let status = status#set_notation_parser_db
1018     {status#notation_parser_db with items = items} in
1019   List.fold_left add1item status items
1020 ;;
1021
1022
1023 let parse_level1_pattern status =
1024   parse_level1_pattern status#notation_parser_db.grammars
1025 let parse_level2_ast status =
1026   parse_level2_ast status#notation_parser_db.grammars
1027 let parse_level2_meta status =
1028   parse_level2_meta status#notation_parser_db.grammars
1029
1030 let level2_ast_grammar status =
1031   status#notation_parser_db.grammars.level2_ast_grammar
1032 let term status = status#notation_parser_db.grammars.term
1033 let let_defs status = status#notation_parser_db.grammars.let_defs
1034 let let_codefs status = status#notation_parser_db.grammars.let_codefs
1035 let protected_binder_vars status =
1036   status#notation_parser_db.grammars.protected_binder_vars
1037
1038 (** {2 Debugging} *)
1039
1040 let print_l2_pattern status =
1041   Grammar.print_entry Format.std_formatter
1042     (Grammar.Entry.obj status#notation_parser_db.grammars.term);
1043   Format.pp_print_flush Format.std_formatter ();
1044   flush stdout
1045
1046 (* vim:set encoding=utf8 foldmethod=marker: *)