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