helm/ocaml/cic_notation/grafiteParser.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 open Printf
  27
  28 let grammar = CicNotationParser.level2_ast_grammar
  29
  30 let term = CicNotationParser.term
  31 let statement = Grammar.Entry.create grammar "statement"
  32
  33 let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
  34
  35 let default_precedence = 50
  36 let default_associativity = Gramext.NonA
  37
  38 EXTEND
  39   GLOBAL: term statement;
  40   arg: [
  41    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
  42       SYMBOL ":"; ty = term; RPAREN -> names,ty
  43    | name = IDENT -> [name],CicNotationPt.Implicit
  44    ]
  45   ];
  46   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  47   tactic_term: [ [ t = term -> t ] ];
  48   ident_list0: [
  49     [ SYMBOL "["; idents = LIST0 IDENT SEP SYMBOL ";"; SYMBOL "]" -> idents ]
  50   ];
  51   tactic_term_list1: [
  52     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
  53   ];
  54   reduction_kind: [
  55     [ IDENT "reduce" -> `Reduce
  56     | IDENT "simplify" -> `Simpl
  57     | IDENT "whd" -> `Whd
  58     | IDENT "normalize" -> `Normalize ]
  59   ];
  60   sequent_pattern_spec: [
  61    [ hyp_paths =
  62       LIST0
  63        [ id = IDENT ;
  64          path = OPT [SYMBOL ":" ; path = term -> path ] ->
  65          (id,match path with Some p -> p | None -> CicNotationPt.UserInput) ]
  66        SEP SYMBOL ";";
  67      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
  68       let goal_path =
  69        match goal_path with
  70           None -> CicNotationPt.UserInput
  71         | Some goal_path -> goal_path
  72       in
  73        hyp_paths,goal_path
  74    ]
  75   ];
  76   pattern_spec: [
  77     [ res = OPT [
  78        "in";
  79        wanted_and_sps =
  80         [ "match" ; wanted = term ;
  81           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
  82            Some wanted,sps
  83         | sps = sequent_pattern_spec ->
  84            None,Some sps
  85         ] ->
  86          let wanted,hyp_paths,goal_path =
  87           match wanted_and_sps with
  88              wanted,None -> wanted, [], CicNotationPt.UserInput
  89            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
  90          in
  91           wanted, hyp_paths, goal_path ] ->
  92       match res with
  93          None -> None,[],CicNotationPt.UserInput
  94        | Some ps -> ps]
  95   ];
  96   direction: [
  97     [ SYMBOL ">" -> `LeftToRight
  98     | SYMBOL "<" -> `RightToLeft ]
  99   ];
 100   int: [ [ num = NUMBER -> int_of_string num ] ];
 101   tactic: [
 102     [ IDENT "absurd"; t = tactic_term ->
 103         GrafiteAst.Absurd (loc, t)
 104     | IDENT "apply"; t = tactic_term ->
 105         GrafiteAst.Apply (loc, t)
 106     | IDENT "assumption" ->
 107         GrafiteAst.Assumption loc
 108     | IDENT "auto";
 109       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 110       width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
 111       paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
 112           GrafiteAst.Auto (loc,depth,width,paramodulation)
 113     | IDENT "clear"; id = IDENT ->
 114         GrafiteAst.Clear (loc,id)
 115     | IDENT "clearbody"; id = IDENT ->
 116         GrafiteAst.ClearBody (loc,id)
 117     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 118         GrafiteAst.Change (loc, what, t)
 119     | IDENT "compare"; t = tactic_term ->
 120         GrafiteAst.Compare (loc,t)
 121     | IDENT "constructor"; n = int ->
 122         GrafiteAst.Constructor (loc, n)
 123     | IDENT "contradiction" ->
 124         GrafiteAst.Contradiction loc
 125     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 126         GrafiteAst.Cut (loc, ident, t)
 127     | IDENT "decide"; IDENT "equality" ->
 128         GrafiteAst.DecideEquality loc
 129     | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
 130       OPT "names"; num = OPT [num = int -> num];
 131       idents = OPT ident_list0 ->
 132         let idents = match idents with None -> [] | Some idents -> idents in
 133         let types = match types with None -> [] | Some types -> types in
 134         let to_spec id = GrafiteAst.Ident id in
 135         GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
 136     | IDENT "discriminate"; t = tactic_term ->
 137         GrafiteAst.Discriminate (loc, t)
 138     | IDENT "elim"; what = tactic_term;
 139       using = OPT [ "using"; using = tactic_term -> using ];
 140       OPT "names"; num = OPT [num = int -> num];
 141       idents = OPT ident_list0 ->
 142         let idents = match idents with None -> [] | Some idents -> idents in
 143         GrafiteAst.Elim (loc, what, using, num, idents)
 144     | IDENT "elimType"; what = tactic_term;
 145       using = OPT [ "using"; using = tactic_term -> using ];
 146       OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
 147         let idents = match idents with None -> [] | Some idents -> idents in
 148         GrafiteAst.ElimType (loc, what, using, num, idents)
 149     | IDENT "exact"; t = tactic_term ->
 150         GrafiteAst.Exact (loc, t)
 151     | IDENT "exists" ->
 152         GrafiteAst.Exists loc
 153     | IDENT "fail" -> GrafiteAst.Fail loc
 154     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 155         let (pt,_,_) = p in
 156           if pt <> None then
 157             raise (CicNotationParser.Parse_error
 158               (loc, "the pattern cannot specify the term to replace, only its"
 159               ^ " paths in the hypotheses and in the conclusion"))
 160         else
 161          GrafiteAst.Fold (loc, kind, t, p)
 162     | IDENT "fourier" ->
 163         GrafiteAst.Fourier loc
 164     | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
 165         let idents = match idents with None -> [] | Some idents -> idents in
 166         GrafiteAst.FwdSimpl (loc, hyp, idents)
 167     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 168        GrafiteAst.Generalize (loc,p,id)
 169     | IDENT "goal"; n = int ->
 170         GrafiteAst.Goal (loc, n)
 171     | IDENT "id" -> GrafiteAst.IdTac loc
 172     | IDENT "injection"; t = tactic_term ->
 173         GrafiteAst.Injection (loc, t)
 174     | IDENT "intro"; ident = OPT IDENT ->
 175         let idents = match ident with None -> [] | Some id -> [id] in
 176         GrafiteAst.Intros (loc, Some 1, idents)
 177     | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
 178         let idents = match idents with None -> [] | Some idents -> idents in
 179         GrafiteAst.Intros (loc, num, idents)
 180     | IDENT "lapply";
 181       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 182       what = tactic_term;
 183       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 184       ident = OPT [ "using" ; ident = IDENT -> ident ] ->
 185         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 186         GrafiteAst.LApply (loc, depth, to_what, what, ident)
 187     | IDENT "left" -> GrafiteAst.Left loc
 188     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 189         GrafiteAst.LetIn (loc, t, where)
 190     | kind = reduction_kind; p = pattern_spec ->
 191         GrafiteAst.Reduce (loc, kind, p)
 192     | IDENT "reflexivity" ->
 193         GrafiteAst.Reflexivity loc
 194     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 195         GrafiteAst.Replace (loc, p, t)
 196     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
 197        let (pt,_,_) = p in
 198         if pt <> None then
 199          raise
 200           (CicNotationParser.Parse_error
 201             (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))
 202         else
 203          GrafiteAst.Rewrite (loc, d, t, p)
 204     | IDENT "right" ->
 205         GrafiteAst.Right loc
 206     | IDENT "ring" ->
 207         GrafiteAst.Ring loc
 208     | IDENT "split" ->
 209         GrafiteAst.Split loc
 210     | IDENT "symmetry" ->
 211         GrafiteAst.Symmetry loc
 212     | IDENT "transitivity"; t = tactic_term ->
 213         GrafiteAst.Transitivity (loc, t)
 214     ]
 215   ];
 216   tactical:
 217     [ "sequence" LEFTA
 218       [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
 219          match tacticals with
 220             [] -> assert false
 221           | [tac] -> tac
 222           | l -> GrafiteAst.Seq (loc, l)
 223       ]
 224     | "then" NONA
 225       [ tac = tactical; SYMBOL ";";
 226         SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" ->
 227           (GrafiteAst.Then (loc, tac, tacs))
 228       ]
 229     | "loops" RIGHTA
 230       [ IDENT "do"; count = int; tac = tactical ->
 231           GrafiteAst.Do (loc, count, tac)
 232       | IDENT "repeat"; tac = tactical ->
 233           GrafiteAst.Repeat (loc, tac)
 234       ]
 235     | "simple" NONA
 236       [ IDENT "first";
 237         SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" ->
 238           GrafiteAst.First (loc, tacs)
 239       | IDENT "try"; tac = NEXT ->
 240           GrafiteAst.Try (loc, tac)
 241       | IDENT "solve";
 242         SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" ->
 243           GrafiteAst.Solve (loc, tacs)
 244       | LPAREN; tac = tactical; RPAREN -> tac
 245       | tac = tactic -> GrafiteAst.Tactic (loc, tac)
 246       ]
 247     ];
 248   theorem_flavour: [
 249     [ [ IDENT "definition"  ] -> `Definition
 250     | [ IDENT "fact"        ] -> `Fact
 251     | [ IDENT "lemma"       ] -> `Lemma
 252     | [ IDENT "remark"      ] -> `Remark
 253     | [ IDENT "theorem"     ] -> `Theorem
 254     ]
 255   ];
 256   inductive_spec: [ [
 257     fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
 258     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 259     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 260     tl = OPT [ "with";
 261       types = LIST1 [
 262         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 263        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 264           (name, true, typ, constructors) ] SEP "with" -> types
 265     ] ->
 266       let params =
 267         List.fold_right
 268           (fun (names, typ) acc ->
 269             (List.map (fun name -> (name, typ)) names) @ acc)
 270           params []
 271       in
 272       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 273       let tl_ind_types = match tl with None -> [] | Some types -> types in
 274       let ind_types = fst_ind_type :: tl_ind_types in
 275       (params, ind_types)
 276   ] ];
 277
 278   record_spec: [ [
 279     name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
 280      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 281      fields = LIST0 [
 282        name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty)
 283      ] SEP SYMBOL ";"; SYMBOL "}" ->
 284       let params =
 285         List.fold_right
 286           (fun (names, typ) acc ->
 287             (List.map (fun name -> (name, typ)) names) @ acc)
 288           params []
 289       in
 290       (params,name,typ,fields)
 291   ] ];
 292
 293   macro: [
 294     [ [ IDENT "quit"  ] -> GrafiteAst.Quit loc
 295 (*     | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
 296     | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
 297 (*     | [ IDENT "undo"   ]; steps = OPT NUMBER ->
 298         GrafiteAst.Undo (loc, int_opt steps)
 299     | [ IDENT "redo"   ]; steps = OPT NUMBER ->
 300         GrafiteAst.Redo (loc, int_opt steps) *)
 301     | [ IDENT "check"   ]; t = term ->
 302         GrafiteAst.Check (loc, t)
 303     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
 304     | [ IDENT "whelp"; "match" ] ; t = term ->
 305         GrafiteAst.WMatch (loc,t)
 306     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 307         GrafiteAst.WInstance (loc,t)
 308     | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT ->
 309         GrafiteAst.WLocate (loc,id)
 310     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 311         GrafiteAst.WElim (loc, t)
 312     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 313         GrafiteAst.WHint (loc,t)
 314     | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
 315     ]
 316   ];
 317   alias_spec: [
 318     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 319       let alpha = "[a-zA-Z]" in
 320       let num = "[0-9]+" in
 321       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 322       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 323       let rex = Str.regexp ("^"^ident^"$") in
 324       if Str.string_match rex id 0 then
 325         if (try ignore (UriManager.uri_of_string uri); true
 326             with UriManager.IllFormedUri _ -> false)
 327         then
 328           GrafiteAst.Ident_alias (id, uri)
 329         else
 330           raise (CicNotationParser.Parse_error (loc,sprintf "Not a valid uri: %s" uri))
 331       else
 332         raise (CicNotationParser.Parse_error (loc,
 333           sprintf "Not a valid identifier: %s" id))
 334     | IDENT "symbol"; symbol = QSTRING;
 335       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 336       SYMBOL "="; dsc = QSTRING ->
 337         let instance =
 338           match instance with Some i -> i | None -> 0
 339         in
 340         GrafiteAst.Symbol_alias (symbol, instance, dsc)
 341     | IDENT "num";
 342       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 343       SYMBOL "="; dsc = QSTRING ->
 344         let instance =
 345           match instance with Some i -> i | None -> 0
 346         in
 347         GrafiteAst.Number_alias (instance, dsc)
 348     ]
 349   ];
 350   argument: [
 351     [ id = IDENT -> CicNotationPt.IdentArg (0, id)
 352     | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
 353       SYMBOL "."; id = IDENT ->
 354         CicNotationPt.IdentArg (List.length l, id)
 355     ]
 356   ];
 357   associativity: [
 358     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 359     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 360     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 361     ]
 362   ];
 363   precedence: [
 364     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 365   ];
 366   notation: [
 367     [ s = QSTRING;
 368       assoc = OPT associativity; prec = OPT precedence;
 369       IDENT "for";
 370       p2 =
 371         [ blob = UNPARSED_AST ->
 372             add_raw_attribute ~text:(sprintf "@{%s}" blob)
 373               (CicNotationParser.parse_level2_ast (Stream.of_string blob))
 374         | blob = UNPARSED_META ->
 375             add_raw_attribute ~text:(sprintf "${%s}" blob)
 376               (CicNotationParser.parse_level2_meta (Stream.of_string blob))
 377         ] ->
 378           let assoc =
 379             match assoc with
 380             | None -> default_associativity
 381             | Some assoc -> assoc
 382           in
 383           let prec =
 384             match prec with
 385             | None -> default_precedence
 386             | Some prec -> prec
 387           in
 388           (add_raw_attribute ~text:s
 389             (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
 390            assoc, prec, p2)
 391     ]
 392   ];
 393   level3_term: [
 394     [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
 395     | id = IDENT -> CicNotationPt.VarPattern id
 396     | SYMBOL "_" -> CicNotationPt.ImplicitPattern
 397     | LPAREN; terms = LIST1 SELF; RPAREN ->
 398         (match terms with
 399         | [] -> assert false
 400         | [term] -> term
 401         | terms -> CicNotationPt.ApplPattern terms)
 402     ]
 403   ];
 404   interpretation: [
 405     [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
 406         (s, args, t)
 407     ]
 408   ];
 409   command: [ [
 410       IDENT "set"; n = QSTRING; v = QSTRING ->
 411         GrafiteAst.Set (loc, n, v)
 412     | IDENT "drop" -> GrafiteAst.Drop loc
 413     | IDENT "qed" -> GrafiteAst.Qed loc
 414     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 415       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 416         GrafiteAst.Obj (loc,
 417           GrafiteAst.Theorem
 418             (`Variant,name,typ,Some (CicNotationPt.Ident (newname, None))))
 419     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 420       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 421         GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
 422     | flavour = theorem_flavour; name = IDENT;
 423       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 424         GrafiteAst.Obj (loc,
 425           GrafiteAst.Theorem (flavour, name, CicNotationPt.Implicit, body))
 426     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 427         defs = CicNotationParser.let_defs ->
 428           let name,ty =
 429             match defs with
 430             | ((CicNotationPt.Ident (name, None), Some ty),_,_) :: _ -> name,ty
 431             | ((CicNotationPt.Ident (name, None), None),_,_) :: _ ->
 432                 name, CicNotationPt.Implicit
 433             | _ -> assert false
 434           in
 435           let body = CicNotationPt.Ident (name,None) in
 436           GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty,
 437             Some (CicNotationPt.LetRec (ind_kind, defs, body))))
 438     | [ IDENT "inductive" ]; spec = inductive_spec ->
 439         let (params, ind_types) = spec in
 440         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
 441     | [ IDENT "coinductive" ]; spec = inductive_spec ->
 442         let (params, ind_types) = spec in
 443         let ind_types = (* set inductive flags to false (coinductive) *)
 444           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 445             ind_types
 446         in
 447         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
 448     | IDENT "coercion" ; name = IDENT ->
 449         GrafiteAst.Coercion (loc, CicNotationPt.Ident (name,Some []))
 450     | IDENT "coercion" ; name = URI ->
 451         GrafiteAst.Coercion (loc, CicNotationPt.Uri (name,Some []))
 452     | IDENT "alias" ; spec = alias_spec ->
 453         GrafiteAst.Alias (loc, spec)
 454     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 455         GrafiteAst.Obj (loc,GrafiteAst.Record (params,name,ty,fields))
 456     | IDENT "include" ; path = QSTRING ->
 457         GrafiteAst.Include (loc,path)
 458     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 459        let uris = List.map UriManager.uri_of_string uris in
 460         GrafiteAst.Default (loc,what,uris)
 461     | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
 462         GrafiteAst.Notation (loc, l1, assoc, prec, l2)
 463     | IDENT "interpretation"; id = QSTRING;
 464       (symbol, args, l3) = interpretation ->
 465         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
 466
 467     | IDENT "dump" -> GrafiteAst.Dump loc
 468     | IDENT "render"; u = URI ->
 469         GrafiteAst.Render (loc, UriManager.uri_of_string u)
 470   ]];
 471   executable: [
 472     [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 473     | tac = tactical; SYMBOL "." -> GrafiteAst.Tactical (loc, tac)
 474     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 475     ]
 476   ];
 477   comment: [
 478     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 479        GrafiteAst.Code (loc, ex)
 480     | str = NOTE ->
 481        GrafiteAst.Note (loc, str)
 482     ]
 483   ];
 484   statement: [
 485     [ ex = executable -> GrafiteAst.Executable (loc,ex)
 486     | com = comment -> GrafiteAst.Comment (loc, com)
 487     | EOI -> raise End_of_file
 488     ]
 489   ];
 490 END
 491
 492 let exc_located_wrapper f =
 493   try
 494     f ()
 495   with
 496   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 497   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 498       raise (CicNotationParser.Parse_error (floc, msg))
 499   | Stdpp.Exc_located (floc, exn) ->
 500       raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn)))
 501
 502 let parse_statement stream =
 503   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
 504