helm/software/components/grafite_parser/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 (* $Id$ *)
  27
  28 module N  = CicNotationPt
  29 module G  = GrafiteAst
  30 module L  = LexiconAst
  31 module LE = LexiconEngine
  32
  33 exception NoInclusionPerformed of string (* full path *)
  34
  35 type 'a localized_option =
  36    LSome of 'a
  37  | LNone of G.loc
  38
  39 type ast_statement =
  40   (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement
  41
  42 type 'status statement =
  43   ?never_include:bool ->
  44     (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
  45   include_paths:string list -> (#LE.status as 'status) ->
  46     'status * ast_statement localized_option
  47
  48 type 'status parser_status = {
  49   grammar : Grammar.g;
  50   term : N.term Grammar.Entry.e;
  51   statement : #LE.status as 'status statement Grammar.Entry.e;
  52 }
  53
  54 let grafite_callback = ref (fun _ -> ())
  55 let set_grafite_callback cb = grafite_callback := cb
  56
  57 let lexicon_callback = ref (fun _ -> ())
  58 let set_lexicon_callback cb = lexicon_callback := cb
  59
  60 let initial_parser () =
  61   let grammar = CicNotationParser.level2_ast_grammar () in
  62   let term = CicNotationParser.term () in
  63   let statement = Grammar.Entry.create grammar "statement" in
  64   { grammar = grammar; term = term; statement = statement }
  65 ;;
  66
  67 let grafite_parser = ref (initial_parser ())
  68
  69 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
  70
  71 let default_associativity = Gramext.NonA
  72
  73 let mk_rec_corec ind_kind defs loc =
  74  (* In case of mutual definitions here we produce just
  75     the syntax tree for the first one. The others will be
  76     generated from the completely specified term just before
  77     insertion in the environment. We use the flavour
  78     `MutualDefinition to rememer this. *)
  79   let name,ty =
  80     match defs with
  81     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
  82         let ty = match ty with Some ty -> ty | None -> N.Implicit in
  83         let ty =
  84          List.fold_right
  85           (fun var ty -> N.Binder (`Pi,var,ty)
  86           ) params ty
  87         in
  88          name,ty
  89     | _ -> assert false
  90   in
  91   let body = N.Ident (name,None) in
  92   let flavour =
  93    if List.length defs = 1 then
  94     `Definition
  95    else
  96     `MutualDefinition
  97   in
  98    (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body))))
  99
 100 let nmk_rec_corec ind_kind defs loc =
 101  let loc,t = mk_rec_corec ind_kind defs loc in
 102   G.NObj (loc,t)
 103
 104 let mk_rec_corec ind_kind defs loc =
 105  let loc,t = mk_rec_corec ind_kind defs loc in
 106   G.Obj (loc,t)
 107
 108 let npunct_of_punct = function
 109   | G.Branch loc -> G.NBranch loc
 110   | G.Shift loc -> G.NShift loc
 111   | G.Pos (loc, i) -> G.NPos (loc, i)
 112   | G.Wildcard loc -> G.NWildcard loc
 113   | G.Merge loc -> G.NMerge loc
 114   | G.Semicolon loc -> G.NSemicolon loc
 115   | G.Dot loc -> G.NDot loc
 116 ;;
 117 let nnon_punct_of_punct = function
 118   | G.Skip loc -> G.NSkip loc
 119   | G.Unfocus loc -> G.NUnfocus loc
 120   | G.Focus (loc,l) -> G.NFocus (loc,l)
 121 ;;
 122 let npunct_of_punct = function
 123   | G.Branch loc -> G.NBranch loc
 124   | G.Shift loc -> G.NShift loc
 125   | G.Pos (loc, i) -> G.NPos (loc, i)
 126   | G.Wildcard loc -> G.NWildcard loc
 127   | G.Merge loc -> G.NMerge loc
 128   | G.Semicolon loc -> G.NSemicolon loc
 129   | G.Dot loc -> G.NDot loc
 130 ;;
 131
 132 type by_continuation =
 133    BYC_done
 134  | BYC_weproved of N.term * string option * N.term option
 135  | BYC_letsuchthat of string * N.term * string * N.term
 136  | BYC_wehaveand of string * N.term * string * N.term
 137
 138 let initialize_parser () =
 139   (* {{{ parser initialization *)
 140   let term = !grafite_parser.term in
 141   let statement = !grafite_parser.statement in
 142   let let_defs = CicNotationParser.let_defs () in
 143   let protected_binder_vars = CicNotationParser.protected_binder_vars () in
 144 EXTEND
 145   GLOBAL: term statement;
 146   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
 147   tactic_term: [ [ t = term LEVEL "90" -> t ] ];
 148   new_name: [
 149     [ SYMBOL "_" -> None
 150     | id = IDENT -> Some id ]
 151     ];
 152   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
 153   tactic_term_list1: [
 154     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
 155   ];
 156   reduction_kind: [
 157     [ IDENT "normalize" -> `Normalize
 158     | IDENT "simplify" -> `Simpl
 159     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
 160     | IDENT "whd" -> `Whd ]
 161   ];
 162   nreduction_kind: [
 163     [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
 164        let delta = match delta with None -> true | _ -> false in
 165         `Normalize delta
 166     (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
 167     | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
 168        let delta = match delta with None -> true | _ -> false in
 169         `Whd delta]
 170   ];
 171   sequent_pattern_spec: [
 172    [ hyp_paths =
 173       LIST0
 174        [ id = IDENT ;
 175          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
 176          (id,match path with Some p -> p | None -> N.UserInput) ];
 177      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
 178       let goal_path =
 179        match goal_path, hyp_paths with
 180           None, [] -> Some N.UserInput
 181         | None, _::_ -> None
 182         | Some goal_path, _ -> Some goal_path
 183       in
 184        hyp_paths,goal_path
 185    ]
 186   ];
 187   pattern_spec: [
 188     [ res = OPT [
 189        "in";
 190        wanted_and_sps =
 191         [ "match" ; wanted = tactic_term ;
 192           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 193            Some wanted,sps
 194         | sps = sequent_pattern_spec ->
 195            None,Some sps
 196         ] ->
 197          let wanted,hyp_paths,goal_path =
 198           match wanted_and_sps with
 199              wanted,None -> wanted, [], Some N.UserInput
 200            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 201          in
 202           wanted, hyp_paths, goal_path ] ->
 203       match res with
 204          None -> None,[],Some N.UserInput
 205        | Some ps -> ps]
 206   ];
 207   inverter_param_list: [
 208     [ params = tactic_term ->
 209       let deannotate = function
 210         | N.AttributedTerm (_,t) | t -> t
 211       in match deannotate params with
 212       | N.Implicit -> [false]
 213       | N.UserInput -> [true]
 214       | N.Appl l ->
 215          List.map (fun x -> match deannotate x with
 216            | N.Implicit -> false
 217            | N.UserInput -> true
 218            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
 219       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
 220   ];
 221   direction: [
 222     [ SYMBOL ">" -> `LeftToRight
 223     | SYMBOL "<" -> `RightToLeft ]
 224   ];
 225   int: [ [ num = NUMBER -> int_of_string num ] ];
 226   intros_names: [
 227    [ idents = OPT ident_list0 ->
 228       match idents with None -> [] | Some idents -> idents
 229    ]
 230   ];
 231   intros_spec: [
 232     [ OPT [ IDENT "names" ];
 233       num = OPT [ num = int -> num ];
 234       idents = intros_names ->
 235         num, idents
 236     ]
 237   ];
 238   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 239   ntactic: [
 240     [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
 241     | IDENT "nassert";
 242        seqs = LIST0 [
 243         hyps = LIST0
 244          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 245          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 246                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 247             id,`Def (bo,ty)];
 248         SYMBOL <:unicode<vdash>>;
 249         concl = tactic_term -> (List.rev hyps,concl) ] ->
 250          G.NAssert (loc, seqs)
 251     | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
 252     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 253         G.NCases (loc, what, where)
 254     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 255         G.NChange (loc, what, with_what)
 256     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 257         G.NElim (loc, what, where)
 258     | IDENT "ngeneralize"; p=pattern_spec ->
 259         G.NGeneralize (loc, p)
 260     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 261         where = pattern_spec ->
 262         G.NLetIn (loc,where,t,name)
 263     | kind = nreduction_kind; p = pattern_spec ->
 264         G.NReduce (loc, kind, p)
 265     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 266         G.NRewrite (loc, dir, what, where)
 267     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
 268     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
 269     | SYMBOL "*" -> G.NCase1 (loc,"_")
 270     | SYMBOL "*"; n=IDENT ->
 271         G.NCase1 (loc,n)
 272     ]
 273   ];
 274   tactic: [
 275     [ IDENT "absurd"; t = tactic_term ->
 276         G.Absurd (loc, t)
 277     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 278         G.ApplyRule (loc, t)
 279     | IDENT "apply"; t = tactic_term ->
 280         G.Apply (loc, t)
 281     | IDENT "applyP"; t = tactic_term ->
 282         G.ApplyP (loc, t)
 283     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 284         G.ApplyS (loc, t, params)
 285     | IDENT "assumption" ->
 286         G.Assumption loc
 287     | IDENT "autobatch";  params = auto_params ->
 288         G.AutoBatch (loc,params)
 289     | IDENT "cases"; what = tactic_term;
 290       pattern = OPT pattern_spec;
 291       specs = intros_spec ->
 292         let pattern = match pattern with
 293            | None         -> None, [], Some N.UserInput
 294            | Some pattern -> pattern
 295         in
 296         G.Cases (loc, what, pattern, specs)
 297     | IDENT "clear"; ids = LIST1 IDENT ->
 298         G.Clear (loc, ids)
 299     | IDENT "clearbody"; id = IDENT ->
 300         G.ClearBody (loc,id)
 301     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 302         G.Change (loc, what, t)
 303     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 304       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 305         let times = match times with None -> 1 | Some i -> i in
 306         G.Compose (loc, t1, t2, times, specs)
 307     | IDENT "constructor"; n = int ->
 308         G.Constructor (loc, n)
 309     | IDENT "contradiction" ->
 310         G.Contradiction loc
 311     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 312         G.Cut (loc, ident, t)
 313     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 314         let idents = match idents with None -> [] | Some idents -> idents in
 315         G.Decompose (loc, idents)
 316     | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
 317     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 318         G.Destruct (loc, xts)
 319     | IDENT "elim"; what = tactic_term; using = using;
 320        pattern = OPT pattern_spec;
 321        ispecs = intros_spec ->
 322         let pattern = match pattern with
 323            | None         -> None, [], Some N.UserInput
 324            | Some pattern -> pattern
 325           in
 326           G.Elim (loc, what, using, pattern, ispecs)
 327     | IDENT "elimType"; what = tactic_term; using = using;
 328       (num, idents) = intros_spec ->
 329         G.ElimType (loc, what, using, (num, idents))
 330     | IDENT "exact"; t = tactic_term ->
 331         G.Exact (loc, t)
 332     | IDENT "exists" ->
 333         G.Exists loc
 334     | IDENT "fail" -> G.Fail loc
 335     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 336         let (pt,_,_) = p in
 337           if pt <> None then
 338             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 339               ("the pattern cannot specify the term to replace, only its"
 340               ^ " paths in the hypotheses and in the conclusion")))
 341        else
 342          G.Fold (loc, kind, t, p)
 343     | IDENT "fourier" ->
 344         G.Fourier loc
 345     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 346         let idents = match idents with None -> [] | Some idents -> idents in
 347         G.FwdSimpl (loc, hyp, idents)
 348     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 349        G.Generalize (loc,p,id)
 350     | IDENT "id" -> G.IdTac loc
 351     | IDENT "intro"; ident = OPT IDENT ->
 352         let idents = match ident with None -> [] | Some id -> [Some id] in
 353         G.Intros (loc, (Some 1, idents))
 354     | IDENT "intros"; specs = intros_spec ->
 355         G.Intros (loc, specs)
 356     | IDENT "inversion"; t = tactic_term ->
 357         G.Inversion (loc, t)
 358     | IDENT "lapply";
 359       linear = OPT [ IDENT "linear" ];
 360       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 361       what = tactic_term;
 362       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 363       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 364         let linear = match linear with None -> false | Some _ -> true in
 365         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 366         G.LApply (loc, linear, depth, to_what, what, ident)
 367     | IDENT "left" -> G.Left loc
 368     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 369         G.LetIn (loc, t, where)
 370     | kind = reduction_kind; p = pattern_spec ->
 371         G.Reduce (loc, kind, p)
 372     | IDENT "reflexivity" ->
 373         G.Reflexivity loc
 374     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 375         G.Replace (loc, p, t)
 376     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 377        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 378        let (pt,_,_) = p in
 379         if pt <> None then
 380          raise
 381           (HExtlib.Localized (loc,
 382            (CicNotationParser.Parse_error
 383             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 384         else
 385          let n = match xnames with None -> [] | Some names -> names in
 386          G.Rewrite (loc, d, t, p, n)
 387     | IDENT "right" ->
 388         G.Right loc
 389     | IDENT "ring" ->
 390         G.Ring loc
 391     | IDENT "split" ->
 392         G.Split loc
 393     | IDENT "symmetry" ->
 394         G.Symmetry loc
 395     | IDENT "transitivity"; t = tactic_term ->
 396         G.Transitivity (loc, t)
 397      (* Produzioni Aggiunte *)
 398     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 399         G.Assume (loc, id, t)
 400     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 401       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 402                 t' = tactic_term -> t']->
 403         G.Suppose (loc, t, id, t1)
 404     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 405       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 406       id2 = IDENT ; RPAREN ->
 407         G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 408     | just =
 409        [ IDENT "using"; t=tactic_term -> `Term t
 410        | params = auto_params -> `Auto params] ;
 411       cont=by_continuation ->
 412        (match cont with
 413            BYC_done -> G.Bydone (loc, just)
 414          | BYC_weproved (ty,id,t1) ->
 415             G.By_just_we_proved(loc, just, ty, id, t1)
 416          | BYC_letsuchthat (id1,t1,id2,t2) ->
 417             G.ExistsElim (loc, just, id1, t1, id2, t2)
 418          | BYC_wehaveand (id1,t1,id2,t2) ->
 419             G.AndElim (loc, just, id1, t1, id2, t2))
 420     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
 421         G.We_need_to_prove (loc, t, id, t1)
 422     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 423         G.We_proceed_by_cases_on (loc, t, t1)
 424     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 425         G.We_proceed_by_induction_on (loc, t, t1)
 426     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 427         G.Byinduction(loc, t, id)
 428     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 429         G.Thesisbecomes(loc, t)
 430     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 431         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 432          G.Case(loc,id,params)
 433       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 434     | IDENT "conclude";
 435       termine = tactic_term;
 436       SYMBOL "=" ;
 437       t1=tactic_term ;
 438       t2 =
 439        [ IDENT "using"; t=tactic_term -> `Term t
 440        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 441        | IDENT "proof" -> `Proof
 442        | params = auto_params -> `Auto params];
 443       cont = rewriting_step_continuation ->
 444        G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 445     | IDENT "obtain" ; name = IDENT;
 446       termine = tactic_term;
 447       SYMBOL "=" ;
 448       t1=tactic_term ;
 449       t2 =
 450        [ IDENT "using"; t=tactic_term -> `Term t
 451        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 452        | IDENT "proof" -> `Proof
 453        | params = auto_params -> `Auto params];
 454       cont = rewriting_step_continuation ->
 455        G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 456     | SYMBOL "=" ;
 457       t1=tactic_term ;
 458       t2 =
 459        [ IDENT "using"; t=tactic_term -> `Term t
 460        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 461        | IDENT "proof" -> `Proof
 462        | params = auto_params -> `Auto params];
 463       cont = rewriting_step_continuation ->
 464        G.RewritingStep(loc, None, t1, t2, cont)
 465   ]
 466 ];
 467   auto_fixed_param: [
 468    [ IDENT "paramodulation"
 469    | IDENT "depth"
 470    | IDENT "width"
 471    | IDENT "size"
 472    | IDENT "timeout"
 473    | IDENT "library"
 474    | IDENT "type"
 475    | IDENT "all"
 476    ]
 477 ];
 478   auto_params: [
 479    [ params =
 480       LIST0 [
 481          i = auto_fixed_param -> i,""
 482        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 483               string_of_int v | v = IDENT -> v ] -> i,v ];
 484       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 485       (match tl with Some l -> l | None -> []),
 486       params
 487    ]
 488 ];
 489   inline_params:[
 490    [ params = LIST0
 491       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
 492       | flavour = inline_flavour -> G.IPAs flavour
 493       | IDENT "coercions" -> G.IPCoercions
 494       | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
 495       | IDENT "procedural" -> G.IPProcedural
 496       | IDENT "nodefaults" -> G.IPNoDefaults
 497       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 498       | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
 499       | IDENT "comments" -> G.IPComments
 500       | IDENT "cr" -> G.IPCR
 501       ] -> params
 502    ]
 503 ];
 504   by_continuation: [
 505     [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
 506     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 507             "done" -> BYC_weproved (ty,None,t1)
 508     | "done" -> BYC_done
 509     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 510       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 511       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 512     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 513               BYC_wehaveand (id1,t1,id2,t2)
 514     ]
 515 ];
 516   rewriting_step_continuation : [
 517     [ "done" -> true
 518     | -> false
 519     ]
 520 ];
 521   atomic_tactical:
 522     [ "sequence" LEFTA
 523       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 524           let ts =
 525             match t1 with
 526             | G.Seq (_, l) -> l @ [ t2 ]
 527             | _ -> [ t1; t2 ]
 528           in
 529           G.Seq (loc, ts)
 530       ]
 531     | "then" NONA
 532       [ tac = SELF; SYMBOL ";";
 533         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 534           (G.Then (loc, tac, tacs))
 535       ]
 536     | "loops" RIGHTA
 537       [ IDENT "do"; count = int; tac = SELF ->
 538           G.Do (loc, count, tac)
 539       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 540       ]
 541     | "simple" NONA
 542       [ IDENT "first";
 543         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 544           G.First (loc, tacs)
 545       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 546       | IDENT "solve";
 547         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 548           G.Solve (loc, tacs)
 549       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 550       | LPAREN; tac = SELF; RPAREN -> tac
 551       | tac = tactic -> tac
 552         ]
 553       ];
 554   npunctuation_tactical:
 555     [
 556       [ SYMBOL "[" -> G.NBranch loc
 557       | SYMBOL "|" -> G.NShift loc
 558       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
 559       | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
 560       | SYMBOL "]" -> G.NMerge loc
 561       | SYMBOL ";" -> G.NSemicolon loc
 562       | SYMBOL "." -> G.NDot loc
 563       ]
 564     ];
 565   punctuation_tactical:
 566     [
 567       [ SYMBOL "[" -> G.Branch loc
 568       | SYMBOL "|" -> G.Shift loc
 569       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 570       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 571       | SYMBOL "]" -> G.Merge loc
 572       | SYMBOL ";" -> G.Semicolon loc
 573       | SYMBOL "." -> G.Dot loc
 574       ]
 575     ];
 576   non_punctuation_tactical:
 577     [ "simple" NONA
 578       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 579       | IDENT "unfocus" -> G.Unfocus loc
 580       | IDENT "skip" -> G.Skip loc
 581       ]
 582       ];
 583   ntheorem_flavour: [
 584     [ [ IDENT "ndefinition"  ] -> `Definition
 585     | [ IDENT "nfact"        ] -> `Fact
 586     | [ IDENT "nlemma"       ] -> `Lemma
 587     | [ IDENT "nremark"      ] -> `Remark
 588     | [ IDENT "ntheorem"     ] -> `Theorem
 589     ]
 590   ];
 591   theorem_flavour: [
 592     [ [ IDENT "definition"  ] -> `Definition
 593     | [ IDENT "fact"        ] -> `Fact
 594     | [ IDENT "lemma"       ] -> `Lemma
 595     | [ IDENT "remark"      ] -> `Remark
 596     | [ IDENT "theorem"     ] -> `Theorem
 597     ]
 598   ];
 599   inline_flavour: [
 600      [ attr = theorem_flavour -> attr
 601      | [ IDENT "axiom"     ]  -> `Axiom
 602      | [ IDENT "variant"   ]  -> `Variant
 603      ]
 604   ];
 605   inductive_spec: [ [
 606     fst_name = IDENT;
 607       params = LIST0 protected_binder_vars;
 608     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 609     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 610     tl = OPT [ "with";
 611         types = LIST1 [
 612           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 613          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 614             (name, true, typ, constructors) ] SEP "with" -> types
 615       ] ->
 616         let params =
 617           List.fold_right
 618             (fun (names, typ) acc ->
 619               (List.map (fun name -> (name, typ)) names) @ acc)
 620             params []
 621         in
 622         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 623         let tl_ind_types = match tl with None -> [] | Some types -> types in
 624         let ind_types = fst_ind_type :: tl_ind_types in
 625         (params, ind_types)
 626     ] ];
 627
 628     record_spec: [ [
 629       name = IDENT;
 630       params = LIST0 protected_binder_vars;
 631        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 632        fields = LIST0 [
 633          name = IDENT ;
 634          coercion = [
 635              SYMBOL ":" -> false,0
 636            | SYMBOL ":"; SYMBOL ">" -> true,0
 637            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 638          ];
 639          ty = term ->
 640            let b,n = coercion in
 641            (name,ty,b,n)
 642        ] SEP SYMBOL ";"; SYMBOL "}" ->
 643         let params =
 644           List.fold_right
 645             (fun (names, typ) acc ->
 646               (List.map (fun name -> (name, typ)) names) @ acc)
 647             params []
 648         in
 649         (params,name,typ,fields)
 650     ] ];
 651
 652     macro: [
 653       [ [ IDENT "check"   ]; t = term ->
 654           G.Check (loc, t)
 655       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 656           G.Eval (loc, kind, t)
 657       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 658            G.Inline (loc, suri, params)
 659       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 660            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 661       | IDENT "auto"; params = auto_params ->
 662           G.AutoInteractive (loc,params)
 663       | [ IDENT "whelp"; "match" ] ; t = term ->
 664           G.WMatch (loc,t)
 665       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 666           G.WInstance (loc,t)
 667       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 668           G.WLocate (loc,id)
 669       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 670           G.WElim (loc, t)
 671       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 672           G.WHint (loc,t)
 673       ]
 674     ];
 675     alias_spec: [
 676       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 677         let alpha = "[a-zA-Z]" in
 678         let num = "[0-9]+" in
 679         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 680         let decoration = "\\'" in
 681         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 682         let rex = Str.regexp ("^"^ident^"$") in
 683         if Str.string_match rex id 0 then
 684           if (try ignore (UriManager.uri_of_string uri); true
 685               with UriManager.IllFormedUri _ -> false) ||
 686              (try ignore (NReference.reference_of_string uri); true
 687               with NReference.IllFormedReference _ -> false)
 688           then
 689             L.Ident_alias (id, uri)
 690           else
 691             raise
 692              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 693         else
 694           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 695             Printf.sprintf "Not a valid identifier: %s" id)))
 696       | IDENT "symbol"; symbol = QSTRING;
 697         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 698         SYMBOL "="; dsc = QSTRING ->
 699           let instance =
 700             match instance with Some i -> i | None -> 0
 701           in
 702           L.Symbol_alias (symbol, instance, dsc)
 703       | IDENT "num";
 704         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 705         SYMBOL "="; dsc = QSTRING ->
 706           let instance =
 707             match instance with Some i -> i | None -> 0
 708           in
 709           L.Number_alias (instance, dsc)
 710       ]
 711      ];
 712     argument: [
 713       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 714         id = IDENT ->
 715           N.IdentArg (List.length l, id)
 716       ]
 717     ];
 718     associativity: [
 719       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 720       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 721       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 722       ]
 723     ];
 724     precedence: [
 725       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 726     ];
 727     notation: [
 728       [ dir = OPT direction; s = QSTRING;
 729         assoc = OPT associativity; prec = precedence;
 730         IDENT "for";
 731         p2 =
 732           [ blob = UNPARSED_AST ->
 733               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 734                 (CicNotationParser.parse_level2_ast
 735                   (Ulexing.from_utf8_string blob))
 736           | blob = UNPARSED_META ->
 737               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 738                 (CicNotationParser.parse_level2_meta
 739                   (Ulexing.from_utf8_string blob))
 740           ] ->
 741             let assoc =
 742               match assoc with
 743               | None -> default_associativity
 744               | Some assoc -> assoc
 745             in
 746             let p1 =
 747               add_raw_attribute ~text:s
 748                 (CicNotationParser.parse_level1_pattern prec
 749                   (Ulexing.from_utf8_string s))
 750             in
 751             (dir, p1, assoc, prec, p2)
 752       ]
 753     ];
 754     level3_term: [
 755       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 756       | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
 757       | IMPLICIT -> N.ImplicitPattern
 758       | id = IDENT -> N.VarPattern id
 759       | LPAREN; terms = LIST1 SELF; RPAREN ->
 760           (match terms with
 761           | [] -> assert false
 762           | [term] -> term
 763           | terms -> N.ApplPattern terms)
 764       ]
 765     ];
 766     interpretation: [
 767       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 768           (s, args, t)
 769       ]
 770     ];
 771
 772     include_command: [ [
 773         IDENT "include" ; path = QSTRING ->
 774           loc,path,true,L.WithPreferences
 775       | IDENT "include" ; IDENT "source" ; path = QSTRING ->
 776           loc,path,false,L.WithPreferences
 777       | IDENT "include'" ; path = QSTRING ->
 778           loc,path,true,L.WithoutPreferences
 779      ]];
 780
 781   grafite_ncommand: [ [
 782       IDENT "nqed" -> G.NQed loc
 783     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 784       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 785         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 786     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 787       body = term ->
 788         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
 789     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 790         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 791     | NLETCOREC ; defs = let_defs ->
 792         nmk_rec_corec `CoInductive defs loc
 793     | NLETREC ; defs = let_defs ->
 794         nmk_rec_corec `Inductive defs loc
 795     | IDENT "ninductive"; spec = inductive_spec ->
 796         let (params, ind_types) = spec in
 797         G.NObj (loc, N.Inductive (params, ind_types))
 798     | IDENT "ncoinductive"; spec = inductive_spec ->
 799         let (params, ind_types) = spec in
 800         let ind_types = (* set inductive flags to false (coinductive) *)
 801           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 802             ind_types
 803         in
 804         G.NObj (loc, N.Inductive (params, ind_types))
 805     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
 806         strict = [ SYMBOL <:unicode<lt>> -> true
 807                  | SYMBOL <:unicode<leq>> -> false ];
 808         u2 = tactic_term ->
 809         let u1 =
 810           match u1 with
 811           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 812               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 813           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 814               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 815           | _ -> raise (Failure "only a sort can be constrained")
 816         in
 817         let u2 =
 818           match u2 with
 819           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 820               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 821           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 822               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 823           | _ -> raise (Failure "only a sort can be constrained")
 824         in
 825          G.NUnivConstraint (loc, strict,u1,u2)
 826     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 827         G.UnificationHint (loc, t, n)
 828     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 829         G.NObj (loc, N.Record (params,name,ty,fields))
 830   ]];
 831
 832   grafite_command: [ [
 833       IDENT "set"; n = QSTRING; v = QSTRING ->
 834         G.Set (loc, n, v)
 835     | IDENT "drop" -> G.Drop loc
 836     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 837     | IDENT "qed" -> G.Qed loc
 838     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 839       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 840         G.Obj (loc,
 841           N.Theorem
 842             (`Variant,name,typ,Some (N.Ident (newname, None))))
 843     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 844       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 845         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 846     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 847       body = term ->
 848         G.Obj (loc,
 849           N.Theorem (flavour, name, N.Implicit, Some body))
 850     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 851         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 852     | LETCOREC ; defs = let_defs ->
 853         mk_rec_corec `CoInductive defs loc
 854     | LETREC ; defs = let_defs ->
 855         mk_rec_corec `Inductive defs loc
 856     | IDENT "inductive"; spec = inductive_spec ->
 857         let (params, ind_types) = spec in
 858         G.Obj (loc, N.Inductive (params, ind_types))
 859     | IDENT "coinductive"; spec = inductive_spec ->
 860         let (params, ind_types) = spec in
 861         let ind_types = (* set inductive flags to false (coinductive) *)
 862           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 863             ind_types
 864         in
 865         G.Obj (loc, N.Inductive (params, ind_types))
 866     | IDENT "coercion" ;
 867       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 868       arity = OPT int ; saturations = OPT int;
 869       composites = OPT (IDENT "nocomposites") ->
 870         let arity = match arity with None -> 0 | Some x -> x in
 871         let saturations = match saturations with None -> 0 | Some x -> x in
 872         let composites = match composites with None -> true | Some _ -> false in
 873         G.Coercion
 874          (loc, t, composites, arity, saturations)
 875     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 876         G.PreferCoercion (loc, t)
 877     | IDENT "pump" ; steps = int ->
 878         G.Pump(loc,steps)
 879     | IDENT "inverter"; name = IDENT; IDENT "for";
 880         indty = tactic_term; paramspec = inverter_param_list ->
 881           G.Inverter
 882             (loc, name, indty, paramspec)
 883     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 884         G.Obj (loc, N.Record (params,name,ty,fields))
 885     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 886        let uris = List.map UriManager.uri_of_string uris in
 887         G.Default (loc,what,uris)
 888     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 889       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 890                    refl = tactic_term -> refl ] ;
 891       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 892                    sym = tactic_term -> sym ] ;
 893       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 894                    trans = tactic_term -> trans ] ;
 895       "as" ; id = IDENT ->
 896        G.Relation (loc,id,a,aeq,refl,sym,trans)
 897   ]];
 898   lexicon_command: [ [
 899       IDENT "alias" ; spec = alias_spec ->
 900         L.Alias (loc, spec)
 901     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 902         L.Notation (loc, dir, l1, assoc, prec, l2)
 903     | IDENT "interpretation"; id = QSTRING;
 904       (symbol, args, l3) = interpretation ->
 905         L.Interpretation (loc, id, (symbol, args), l3)
 906   ]];
 907   executable: [
 908     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 909     | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
 910     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 911         G.Tactic (loc, Some tac, punct)
 912     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 913     | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 914         G.NTactic (loc, [tac; npunct_of_punct punct])
 915     | tac = ntactic; punct = punctuation_tactical ->
 916         G.NTactic (loc, [tac; npunct_of_punct punct])
 917     | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
 918         G.NTactic (loc, [punct])
 919     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 920         G.NonPunctuationTactical (loc, tac, punct)
 921     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 922         SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 923           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 924     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 925         punct = punctuation_tactical ->
 926           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 927     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 928     ]
 929   ];
 930   comment: [
 931     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 932        G.Code (loc, ex)
 933     | str = NOTE ->
 934        G.Note (loc, str)
 935     ]
 936   ];
 937   statement: [
 938     [ ex = executable ->
 939        fun ?(never_include=false) ~include_paths status ->
 940           let stm = G.Executable (loc, ex) in
 941           !grafite_callback stm;
 942           status, LSome stm
 943     | com = comment ->
 944        fun ?(never_include=false) ~include_paths status ->
 945           let stm = G.Comment (loc, com) in
 946           !grafite_callback stm;
 947           status, LSome stm
 948     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
 949        fun ?(never_include=false) ~include_paths status ->
 950           let stm =
 951              G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
 952           in
 953           !grafite_callback stm;
 954           let _root, buri, fullpath, _rrelpath =
 955             Librarian.baseuri_of_script ~include_paths fname
 956           in
 957           let status =
 958             if never_include then raise (NoInclusionPerformed fullpath)
 959             else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
 960           in
 961           let stm =
 962              G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
 963           in
 964           status, LSome stm
 965     | scom = lexicon_command ; SYMBOL "." ->
 966        fun ?(never_include=false) ~include_paths status ->
 967           !lexicon_callback scom;
 968           let status = LE.eval_command status scom in
 969           status, LNone loc
 970     | EOI -> raise End_of_file
 971     ]
 972   ];
 973 END
 974 (* }}} *)
 975 ;;
 976
 977 let _ = initialize_parser () ;;
 978
 979 let exc_located_wrapper f =
 980   try
 981     f ()
 982   with
 983   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 984   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 985       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 986   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 987       raise
 988        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 989   | Stdpp.Exc_located (floc, exn) ->
 990       raise
 991        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 992
 993 let parse_statement lexbuf =
 994   exc_located_wrapper
 995     (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
 996
 997 let statement () = Obj.magic !grafite_parser.statement
 998
 999 let history = ref [] ;;
1000
1001 let push () =
1002   LexiconSync.push ();
1003   history := !grafite_parser :: !history;
1004   grafite_parser := initial_parser ();
1005   initialize_parser ()
1006 ;;
1007
1008 let pop () =
1009   LexiconSync.pop ();
1010   match !history with
1011   | [] -> assert false
1012   | gp :: tail ->
1013       grafite_parser := gp;
1014       history := tail
1015 ;;
1016
1017 (* vim:set foldmethod=marker: *)
1018
1019