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