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