helm/software/components/grafite_parser/grafiteParser.ml

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