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