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