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