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 `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))))
  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"; tac = SELF -> G.NTry (loc,tac)
 268     | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
 269     | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
 270     | IDENT "nassumption" -> G.NAssumption loc
 271     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
 272     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
 273     | SYMBOL "*" -> G.NCase1 (loc,"_")
 274     | SYMBOL "*"; n=IDENT ->
 275         G.NCase1 (loc,n)
 276     ]
 277   ];
 278   tactic: [
 279     [ IDENT "absurd"; t = tactic_term ->
 280         G.Absurd (loc, t)
 281     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 282         G.ApplyRule (loc, t)
 283     | IDENT "apply"; t = tactic_term ->
 284         G.Apply (loc, t)
 285     | IDENT "applyP"; t = tactic_term ->
 286         G.ApplyP (loc, t)
 287     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 288         G.ApplyS (loc, t, params)
 289     | IDENT "assumption" ->
 290         G.Assumption loc
 291     | IDENT "autobatch";  params = auto_params ->
 292         G.AutoBatch (loc,params)
 293     | IDENT "cases"; what = tactic_term;
 294       pattern = OPT pattern_spec;
 295       specs = intros_spec ->
 296         let pattern = match pattern with
 297            | None         -> None, [], Some N.UserInput
 298            | Some pattern -> pattern
 299         in
 300         G.Cases (loc, what, pattern, specs)
 301     | IDENT "clear"; ids = LIST1 IDENT ->
 302         G.Clear (loc, ids)
 303     | IDENT "clearbody"; id = IDENT ->
 304         G.ClearBody (loc,id)
 305     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 306         G.Change (loc, what, t)
 307     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 308       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 309         let times = match times with None -> 1 | Some i -> i in
 310         G.Compose (loc, t1, t2, times, specs)
 311     | IDENT "constructor"; n = int ->
 312         G.Constructor (loc, n)
 313     | IDENT "contradiction" ->
 314         G.Contradiction loc
 315     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 316         G.Cut (loc, ident, t)
 317     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 318         let idents = match idents with None -> [] | Some idents -> idents in
 319         G.Decompose (loc, idents)
 320     | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
 321     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 322         G.Destruct (loc, xts)
 323     | IDENT "elim"; what = tactic_term; using = using;
 324        pattern = OPT pattern_spec;
 325        ispecs = intros_spec ->
 326         let pattern = match pattern with
 327            | None         -> None, [], Some N.UserInput
 328            | Some pattern -> pattern
 329           in
 330           G.Elim (loc, what, using, pattern, ispecs)
 331     | IDENT "elimType"; what = tactic_term; using = using;
 332       (num, idents) = intros_spec ->
 333         G.ElimType (loc, what, using, (num, idents))
 334     | IDENT "exact"; t = tactic_term ->
 335         G.Exact (loc, t)
 336     | IDENT "exists" ->
 337         G.Exists loc
 338     | IDENT "fail" -> G.Fail loc
 339     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 340         let (pt,_,_) = p in
 341           if pt <> None then
 342             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 343               ("the pattern cannot specify the term to replace, only its"
 344               ^ " paths in the hypotheses and in the conclusion")))
 345        else
 346          G.Fold (loc, kind, t, p)
 347     | IDENT "fourier" ->
 348         G.Fourier loc
 349     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 350         let idents = match idents with None -> [] | Some idents -> idents in
 351         G.FwdSimpl (loc, hyp, idents)
 352     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 353        G.Generalize (loc,p,id)
 354     | IDENT "id" -> G.IdTac loc
 355     | IDENT "intro"; ident = OPT IDENT ->
 356         let idents = match ident with None -> [] | Some id -> [Some id] in
 357         G.Intros (loc, (Some 1, idents))
 358     | IDENT "intros"; specs = intros_spec ->
 359         G.Intros (loc, specs)
 360     | IDENT "inversion"; t = tactic_term ->
 361         G.Inversion (loc, t)
 362     | IDENT "lapply";
 363       linear = OPT [ IDENT "linear" ];
 364       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 365       what = tactic_term;
 366       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 367       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 368         let linear = match linear with None -> false | Some _ -> true in
 369         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 370         G.LApply (loc, linear, depth, to_what, what, ident)
 371     | IDENT "left" -> G.Left loc
 372     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 373         G.LetIn (loc, t, where)
 374     | kind = reduction_kind; p = pattern_spec ->
 375         G.Reduce (loc, kind, p)
 376     | IDENT "reflexivity" ->
 377         G.Reflexivity loc
 378     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 379         G.Replace (loc, p, t)
 380     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 381        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 382        let (pt,_,_) = p in
 383         if pt <> None then
 384          raise
 385           (HExtlib.Localized (loc,
 386            (CicNotationParser.Parse_error
 387             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 388         else
 389          let n = match xnames with None -> [] | Some names -> names in
 390          G.Rewrite (loc, d, t, p, n)
 391     | IDENT "right" ->
 392         G.Right loc
 393     | IDENT "ring" ->
 394         G.Ring loc
 395     | IDENT "split" ->
 396         G.Split loc
 397     | IDENT "symmetry" ->
 398         G.Symmetry loc
 399     | IDENT "transitivity"; t = tactic_term ->
 400         G.Transitivity (loc, t)
 401      (* Produzioni Aggiunte *)
 402     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 403         G.Assume (loc, id, t)
 404     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 405       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 406                 t' = tactic_term -> t']->
 407         G.Suppose (loc, t, id, t1)
 408     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 409       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 410       id2 = IDENT ; RPAREN ->
 411         G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 412     | just =
 413        [ IDENT "using"; t=tactic_term -> `Term t
 414        | params = auto_params -> `Auto params] ;
 415       cont=by_continuation ->
 416        (match cont with
 417            BYC_done -> G.Bydone (loc, just)
 418          | BYC_weproved (ty,id,t1) ->
 419             G.By_just_we_proved(loc, just, ty, id, t1)
 420          | BYC_letsuchthat (id1,t1,id2,t2) ->
 421             G.ExistsElim (loc, just, id1, t1, id2, t2)
 422          | BYC_wehaveand (id1,t1,id2,t2) ->
 423             G.AndElim (loc, just, id1, t1, id2, t2))
 424     | 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']->
 425         G.We_need_to_prove (loc, t, id, t1)
 426     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 427         G.We_proceed_by_cases_on (loc, t, t1)
 428     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 429         G.We_proceed_by_induction_on (loc, t, t1)
 430     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 431         G.Byinduction(loc, t, id)
 432     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 433         G.Thesisbecomes(loc, t)
 434     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 435         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 436          G.Case(loc,id,params)
 437       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 438     | IDENT "conclude";
 439       termine = tactic_term;
 440       SYMBOL "=" ;
 441       t1=tactic_term ;
 442       t2 =
 443        [ IDENT "using"; t=tactic_term -> `Term t
 444        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 445        | IDENT "proof" -> `Proof
 446        | params = auto_params -> `Auto params];
 447       cont = rewriting_step_continuation ->
 448        G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 449     | IDENT "obtain" ; name = IDENT;
 450       termine = tactic_term;
 451       SYMBOL "=" ;
 452       t1=tactic_term ;
 453       t2 =
 454        [ IDENT "using"; t=tactic_term -> `Term t
 455        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 456        | IDENT "proof" -> `Proof
 457        | params = auto_params -> `Auto params];
 458       cont = rewriting_step_continuation ->
 459        G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 460     | SYMBOL "=" ;
 461       t1=tactic_term ;
 462       t2 =
 463        [ IDENT "using"; t=tactic_term -> `Term t
 464        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 465        | IDENT "proof" -> `Proof
 466        | params = auto_params -> `Auto params];
 467       cont = rewriting_step_continuation ->
 468        G.RewritingStep(loc, None, t1, t2, cont)
 469   ]
 470 ];
 471   auto_fixed_param: [
 472    [ IDENT "paramodulation"
 473    | IDENT "depth"
 474    | IDENT "width"
 475    | IDENT "size"
 476    | IDENT "timeout"
 477    | IDENT "library"
 478    | IDENT "type"
 479    | IDENT "all"
 480    ]
 481 ];
 482   auto_params: [
 483    [ params =
 484       LIST0 [
 485          i = auto_fixed_param -> i,""
 486        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 487               string_of_int v | v = IDENT -> v ] -> i,v ];
 488       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 489       (match tl with Some l -> l | None -> []),
 490       params
 491    ]
 492 ];
 493   inline_params:[
 494    [ params = LIST0
 495       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
 496       | flavour = inline_flavour -> G.IPAs flavour
 497       | IDENT "coercions" -> G.IPCoercions
 498       | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
 499       | IDENT "procedural" -> G.IPProcedural
 500       | IDENT "nodefaults" -> G.IPNoDefaults
 501       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 502       | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
 503       | IDENT "comments" -> G.IPComments
 504       | IDENT "cr" -> G.IPCR
 505       ] -> params
 506    ]
 507 ];
 508   by_continuation: [
 509     [ 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)
 510     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 511             "done" -> BYC_weproved (ty,None,t1)
 512     | "done" -> BYC_done
 513     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 514       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 515       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 516     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 517               BYC_wehaveand (id1,t1,id2,t2)
 518     ]
 519 ];
 520   rewriting_step_continuation : [
 521     [ "done" -> true
 522     | -> false
 523     ]
 524 ];
 525   atomic_tactical:
 526     [ "sequence" LEFTA
 527       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 528           let ts =
 529             match t1 with
 530             | G.Seq (_, l) -> l @ [ t2 ]
 531             | _ -> [ t1; t2 ]
 532           in
 533           G.Seq (loc, ts)
 534       ]
 535     | "then" NONA
 536       [ tac = SELF; SYMBOL ";";
 537         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 538           (G.Then (loc, tac, tacs))
 539       ]
 540     | "loops" RIGHTA
 541       [ IDENT "do"; count = int; tac = SELF ->
 542           G.Do (loc, count, tac)
 543       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 544       ]
 545     | "simple" NONA
 546       [ IDENT "first";
 547         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 548           G.First (loc, tacs)
 549       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 550       | IDENT "solve";
 551         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 552           G.Solve (loc, tacs)
 553       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 554       | LPAREN; tac = SELF; RPAREN -> tac
 555       | tac = tactic -> tac
 556         ]
 557       ];
 558   npunctuation_tactical:
 559     [
 560       [ SYMBOL "[" -> G.NBranch loc
 561       | SYMBOL "|" -> G.NShift loc
 562       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
 563       | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
 564       | SYMBOL "]" -> G.NMerge loc
 565       | SYMBOL ";" -> G.NSemicolon loc
 566       | SYMBOL "." -> G.NDot loc
 567       ]
 568     ];
 569   punctuation_tactical:
 570     [
 571       [ SYMBOL "[" -> G.Branch loc
 572       | SYMBOL "|" -> G.Shift loc
 573       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 574       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 575       | SYMBOL "]" -> G.Merge loc
 576       | SYMBOL ";" -> G.Semicolon loc
 577       | SYMBOL "." -> G.Dot loc
 578       ]
 579     ];
 580   non_punctuation_tactical:
 581     [ "simple" NONA
 582       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 583       | IDENT "unfocus" -> G.Unfocus loc
 584       | IDENT "skip" -> G.Skip loc
 585       ]
 586       ];
 587   ntheorem_flavour: [
 588     [ [ IDENT "ndefinition"  ] -> `Definition
 589     | [ IDENT "nfact"        ] -> `Fact
 590     | [ IDENT "nlemma"       ] -> `Lemma
 591     | [ IDENT "nremark"      ] -> `Remark
 592     | [ IDENT "ntheorem"     ] -> `Theorem
 593     ]
 594   ];
 595   theorem_flavour: [
 596     [ [ IDENT "definition"  ] -> `Definition
 597     | [ IDENT "fact"        ] -> `Fact
 598     | [ IDENT "lemma"       ] -> `Lemma
 599     | [ IDENT "remark"      ] -> `Remark
 600     | [ IDENT "theorem"     ] -> `Theorem
 601     ]
 602   ];
 603   inline_flavour: [
 604      [ attr = theorem_flavour -> attr
 605      | [ IDENT "axiom"     ]  -> `Axiom
 606      | [ IDENT "variant"   ]  -> `Variant
 607      ]
 608   ];
 609   inductive_spec: [ [
 610     fst_name = IDENT;
 611       params = LIST0 protected_binder_vars;
 612     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 613     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 614     tl = OPT [ "with";
 615         types = LIST1 [
 616           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 617          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 618             (name, true, typ, constructors) ] SEP "with" -> types
 619       ] ->
 620         let params =
 621           List.fold_right
 622             (fun (names, typ) acc ->
 623               (List.map (fun name -> (name, typ)) names) @ acc)
 624             params []
 625         in
 626         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 627         let tl_ind_types = match tl with None -> [] | Some types -> types in
 628         let ind_types = fst_ind_type :: tl_ind_types in
 629         (params, ind_types)
 630     ] ];
 631
 632     record_spec: [ [
 633       name = IDENT;
 634       params = LIST0 protected_binder_vars;
 635        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 636        fields = LIST0 [
 637          name = IDENT ;
 638          coercion = [
 639              SYMBOL ":" -> false,0
 640            | SYMBOL ":"; SYMBOL ">" -> true,0
 641            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 642          ];
 643          ty = term ->
 644            let b,n = coercion in
 645            (name,ty,b,n)
 646        ] SEP SYMBOL ";"; SYMBOL "}" ->
 647         let params =
 648           List.fold_right
 649             (fun (names, typ) acc ->
 650               (List.map (fun name -> (name, typ)) names) @ acc)
 651             params []
 652         in
 653         (params,name,typ,fields)
 654     ] ];
 655
 656     nmacro: [
 657       [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
 658       ]
 659     ];
 660
 661     macro: [
 662       [ [ IDENT "check"   ]; t = term ->
 663           G.Check (loc, t)
 664       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 665           G.Eval (loc, kind, t)
 666       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 667            G.Inline (loc, suri, params)
 668       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 669            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 670       | IDENT "auto"; params = auto_params ->
 671           G.AutoInteractive (loc,params)
 672       | [ IDENT "whelp"; "match" ] ; t = term ->
 673           G.WMatch (loc,t)
 674       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 675           G.WInstance (loc,t)
 676       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 677           G.WLocate (loc,id)
 678       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 679           G.WElim (loc, t)
 680       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 681           G.WHint (loc,t)
 682       ]
 683     ];
 684     alias_spec: [
 685       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 686         let alpha = "[a-zA-Z]" in
 687         let num = "[0-9]+" in
 688         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 689         let decoration = "\\'" in
 690         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 691         let rex = Str.regexp ("^"^ident^"$") in
 692         if Str.string_match rex id 0 then
 693           if (try ignore (UriManager.uri_of_string uri); true
 694               with UriManager.IllFormedUri _ -> false) ||
 695              (try ignore (NReference.reference_of_string uri); true
 696               with NReference.IllFormedReference _ -> false)
 697           then
 698             L.Ident_alias (id, uri)
 699           else
 700             raise
 701              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 702         else
 703           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 704             Printf.sprintf "Not a valid identifier: %s" id)))
 705       | IDENT "symbol"; symbol = QSTRING;
 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.Symbol_alias (symbol, instance, dsc)
 712       | IDENT "num";
 713         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 714         SYMBOL "="; dsc = QSTRING ->
 715           let instance =
 716             match instance with Some i -> i | None -> 0
 717           in
 718           L.Number_alias (instance, dsc)
 719       ]
 720      ];
 721     argument: [
 722       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 723         id = IDENT ->
 724           N.IdentArg (List.length l, id)
 725       ]
 726     ];
 727     associativity: [
 728       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 729       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 730       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 731       ]
 732     ];
 733     precedence: [
 734       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 735     ];
 736     notation: [
 737       [ dir = OPT direction; s = QSTRING;
 738         assoc = OPT associativity; prec = precedence;
 739         IDENT "for";
 740         p2 =
 741           [ blob = UNPARSED_AST ->
 742               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 743                 (CicNotationParser.parse_level2_ast
 744                   (Ulexing.from_utf8_string blob))
 745           | blob = UNPARSED_META ->
 746               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 747                 (CicNotationParser.parse_level2_meta
 748                   (Ulexing.from_utf8_string blob))
 749           ] ->
 750             let assoc =
 751               match assoc with
 752               | None -> default_associativity
 753               | Some assoc -> assoc
 754             in
 755             let p1 =
 756               add_raw_attribute ~text:s
 757                 (CicNotationParser.parse_level1_pattern prec
 758                   (Ulexing.from_utf8_string s))
 759             in
 760             (dir, p1, assoc, prec, p2)
 761       ]
 762     ];
 763     level3_term: [
 764       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 765       | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
 766       | IMPLICIT -> N.ImplicitPattern
 767       | id = IDENT -> N.VarPattern id
 768       | LPAREN; terms = LIST1 SELF; RPAREN ->
 769           (match terms with
 770           | [] -> assert false
 771           | [term] -> term
 772           | terms -> N.ApplPattern terms)
 773       ]
 774     ];
 775     interpretation: [
 776       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 777           (s, args, t)
 778       ]
 779     ];
 780
 781     include_command: [ [
 782         IDENT "include" ; path = QSTRING ->
 783           loc,path,true,L.WithPreferences
 784       | IDENT "include" ; IDENT "source" ; path = QSTRING ->
 785           loc,path,false,L.WithPreferences
 786       | IDENT "include'" ; path = QSTRING ->
 787           loc,path,true,L.WithoutPreferences
 788      ]];
 789
 790   grafite_ncommand: [ [
 791       IDENT "nqed" -> G.NQed loc
 792     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 793       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 794         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 795     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 796       body = term ->
 797         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
 798     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 799         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 800     | NLETCOREC ; defs = let_defs ->
 801         nmk_rec_corec `CoInductive defs loc
 802     | NLETREC ; defs = let_defs ->
 803         nmk_rec_corec `Inductive defs loc
 804     | IDENT "ninductive"; spec = inductive_spec ->
 805         let (params, ind_types) = spec in
 806         G.NObj (loc, N.Inductive (params, ind_types))
 807     | IDENT "ncoinductive"; spec = inductive_spec ->
 808         let (params, ind_types) = spec in
 809         let ind_types = (* set inductive flags to false (coinductive) *)
 810           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 811             ind_types
 812         in
 813         G.NObj (loc, N.Inductive (params, ind_types))
 814     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
 815         strict = [ SYMBOL <:unicode<lt>> -> true
 816                  | SYMBOL <:unicode<leq>> -> false ];
 817         u2 = tactic_term ->
 818         let u1 =
 819           match u1 with
 820           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 821               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 822           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 823               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 824           | _ -> raise (Failure "only a sort can be constrained")
 825         in
 826         let u2 =
 827           match u2 with
 828           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 829               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 830           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 831               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 832           | _ -> raise (Failure "only a sort can be constrained")
 833         in
 834          G.NUnivConstraint (loc, strict,u1,u2)
 835     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 836         G.UnificationHint (loc, t, n)
 837     | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
 838         SYMBOL <:unicode<def>>; t = term; "on";
 839         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
 840         "to"; target = term ->
 841           G.NCoercion(loc,name,t,ty,(id,source),target)
 842     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 843         G.NObj (loc, N.Record (params,name,ty,fields))
 844     | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
 845       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
 846         G.NCopy (loc,s,NUri.uri_of_string u,
 847           List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
 848   ]];
 849
 850   grafite_command: [ [
 851       IDENT "set"; n = QSTRING; v = QSTRING ->
 852         G.Set (loc, n, v)
 853     | IDENT "drop" -> G.Drop loc
 854     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 855     | IDENT "qed" -> G.Qed loc
 856     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 857       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 858         G.Obj (loc,
 859           N.Theorem
 860             (`Variant,name,typ,Some (N.Ident (newname, None))))
 861     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 862       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 863         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 864     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 865       body = term ->
 866         G.Obj (loc,
 867           N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
 868     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 869         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 870     | LETCOREC ; defs = let_defs ->
 871         mk_rec_corec `CoInductive defs loc
 872     | LETREC ; defs = let_defs ->
 873         mk_rec_corec `Inductive defs loc
 874     | IDENT "inductive"; spec = inductive_spec ->
 875         let (params, ind_types) = spec in
 876         G.Obj (loc, N.Inductive (params, ind_types))
 877     | IDENT "coinductive"; spec = inductive_spec ->
 878         let (params, ind_types) = spec in
 879         let ind_types = (* set inductive flags to false (coinductive) *)
 880           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 881             ind_types
 882         in
 883         G.Obj (loc, N.Inductive (params, ind_types))
 884     | IDENT "coercion" ;
 885       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 886       arity = OPT int ; saturations = OPT int;
 887       composites = OPT (IDENT "nocomposites") ->
 888         let arity = match arity with None -> 0 | Some x -> x in
 889         let saturations = match saturations with None -> 0 | Some x -> x in
 890         let composites = match composites with None -> true | Some _ -> false in
 891         G.Coercion
 892          (loc, t, composites, arity, saturations)
 893     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 894         G.PreferCoercion (loc, t)
 895     | IDENT "pump" ; steps = int ->
 896         G.Pump(loc,steps)
 897     | IDENT "inverter"; name = IDENT; IDENT "for";
 898         indty = tactic_term; paramspec = inverter_param_list ->
 899           G.Inverter
 900             (loc, name, indty, paramspec)
 901     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 902         G.Obj (loc, N.Record (params,name,ty,fields))
 903     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 904        let uris = List.map UriManager.uri_of_string uris in
 905         G.Default (loc,what,uris)
 906     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 907       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 908                    refl = tactic_term -> refl ] ;
 909       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 910                    sym = tactic_term -> sym ] ;
 911       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 912                    trans = tactic_term -> trans ] ;
 913       "as" ; id = IDENT ->
 914        G.Relation (loc,id,a,aeq,refl,sym,trans)
 915   ]];
 916   lexicon_command: [ [
 917       IDENT "alias" ; spec = alias_spec ->
 918         L.Alias (loc, spec)
 919     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 920         L.Notation (loc, dir, l1, assoc, prec, l2)
 921     | IDENT "interpretation"; id = QSTRING;
 922       (symbol, args, l3) = interpretation ->
 923         L.Interpretation (loc, id, (symbol, args), l3)
 924   ]];
 925   executable: [
 926     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 927     | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
 928     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 929         G.Tactic (loc, Some tac, punct)
 930     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 931     | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 932         G.NTactic (loc, [tac; npunct_of_punct punct])
 933     | tac = ntactic; punct = punctuation_tactical ->
 934         G.NTactic (loc, [tac; npunct_of_punct punct])
 935     | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
 936         G.NTactic (loc, [punct])
 937     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 938         G.NonPunctuationTactical (loc, tac, punct)
 939     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 940         SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 941           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 942     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 943         punct = punctuation_tactical ->
 944           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 945     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 946     | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
 947     ]
 948   ];
 949   comment: [
 950     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 951        G.Code (loc, ex)
 952     | str = NOTE ->
 953        G.Note (loc, str)
 954     ]
 955   ];
 956   statement: [
 957     [ ex = executable ->
 958        fun ?(never_include=false) ~include_paths status ->
 959           let stm = G.Executable (loc, ex) in
 960           !grafite_callback stm;
 961           status, LSome stm
 962     | com = comment ->
 963        fun ?(never_include=false) ~include_paths status ->
 964           let stm = G.Comment (loc, com) in
 965           !grafite_callback stm;
 966           status, LSome stm
 967     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
 968        fun ?(never_include=false) ~include_paths status ->
 969         let _root, buri, fullpath, _rrelpath =
 970           Librarian.baseuri_of_script ~include_paths fname in
 971         if never_include then raise (NoInclusionPerformed fullpath)
 972         else
 973          begin
 974           let stm =
 975            G.Executable
 976             (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
 977           !grafite_callback stm;
 978           let status =
 979            LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
 980           let stm =
 981            G.Executable
 982             (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
 983           in
 984            status, LSome stm
 985          end
 986     | scom = lexicon_command ; SYMBOL "." ->
 987        fun ?(never_include=false) ~include_paths status ->
 988           !lexicon_callback scom;
 989           let status = LE.eval_command status scom in
 990           status, LNone loc
 991     | EOI -> raise End_of_file
 992     ]
 993   ];
 994 END
 995 (* }}} *)
 996 ;;
 997
 998 let _ = initialize_parser () ;;
 999
1000 let exc_located_wrapper f =
1001   try
1002     f ()
1003   with
1004   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1005   | Stdpp.Exc_located (floc, Stream.Error msg) ->
1006       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1007   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1008       raise
1009        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1010   | Stdpp.Exc_located (floc, exn) ->
1011       raise
1012        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1013
1014 let parse_statement lexbuf =
1015   exc_located_wrapper
1016     (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1017
1018 let statement () = Obj.magic !grafite_parser.statement
1019
1020 let history = ref [] ;;
1021
1022 let push () =
1023   LexiconSync.push ();
1024   history := !grafite_parser :: !history;
1025   grafite_parser := initial_parser ();
1026   initialize_parser ()
1027 ;;
1028
1029 let pop () =
1030   LexiconSync.pop ();
1031   match !history with
1032   | [] -> assert false
1033   | gp :: tail ->
1034       grafite_parser := gp;
1035       history := tail
1036 ;;
1037
1038 (* vim:set foldmethod=marker: *)
1039
1040