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 "depth"
 482    | IDENT "width"
 483    | IDENT "size"
 484    | IDENT "timeout"
 485    | IDENT "library"
 486    | IDENT "type"
 487    | IDENT "all"
 488    ]
 489 ];
 490   auto_params: [
 491    [ params =
 492       LIST0 [
 493          i = auto_fixed_param -> i,""
 494        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 495               string_of_int v | v = IDENT -> v ] -> i,v ];
 496       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 497       (match tl with Some l -> l | None -> []),
 498       params
 499    ]
 500 ];
 501   inline_params:[
 502    [ params = LIST0
 503       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
 504       | flavour = inline_flavour -> G.IPAs flavour
 505       | IDENT "coercions" -> G.IPCoercions
 506       | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
 507       | IDENT "procedural" -> G.IPProcedural
 508       | IDENT "nodefaults" -> G.IPNoDefaults
 509       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 510       | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
 511       | IDENT "comments" -> G.IPComments
 512       | IDENT "cr" -> G.IPCR
 513       ] -> params
 514    ]
 515 ];
 516   by_continuation: [
 517     [ 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)
 518     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 519             "done" -> BYC_weproved (ty,None,t1)
 520     | "done" -> BYC_done
 521     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 522       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 523       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 524     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 525               BYC_wehaveand (id1,t1,id2,t2)
 526     ]
 527 ];
 528   rewriting_step_continuation : [
 529     [ "done" -> true
 530     | -> false
 531     ]
 532 ];
 533   atomic_tactical:
 534     [ "sequence" LEFTA
 535       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 536           let ts =
 537             match t1 with
 538             | G.Seq (_, l) -> l @ [ t2 ]
 539             | _ -> [ t1; t2 ]
 540           in
 541           G.Seq (loc, ts)
 542       ]
 543     | "then" NONA
 544       [ tac = SELF; SYMBOL ";";
 545         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 546           (G.Then (loc, tac, tacs))
 547       ]
 548     | "loops" RIGHTA
 549       [ IDENT "do"; count = int; tac = SELF ->
 550           G.Do (loc, count, tac)
 551       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 552       ]
 553     | "simple" NONA
 554       [ IDENT "first";
 555         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 556           G.First (loc, tacs)
 557       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 558       | IDENT "solve";
 559         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 560           G.Solve (loc, tacs)
 561       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 562       | LPAREN; tac = SELF; RPAREN -> tac
 563       | tac = tactic -> tac
 564         ]
 565       ];
 566   npunctuation_tactical:
 567     [
 568       [ SYMBOL "[" -> G.NBranch loc
 569       | SYMBOL "|" -> G.NShift loc
 570       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
 571       | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
 572       | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
 573       | SYMBOL "]" -> G.NMerge loc
 574       | SYMBOL ";" -> G.NSemicolon loc
 575       | SYMBOL "." -> G.NDot loc
 576       ]
 577     ];
 578   punctuation_tactical:
 579     [
 580       [ SYMBOL "[" -> G.Branch loc
 581       | SYMBOL "|" -> G.Shift loc
 582       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 583       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 584       | SYMBOL "]" -> G.Merge loc
 585       | SYMBOL ";" -> G.Semicolon loc
 586       | SYMBOL "." -> G.Dot loc
 587       ]
 588     ];
 589   non_punctuation_tactical:
 590     [ "simple" NONA
 591       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 592       | IDENT "unfocus" -> G.Unfocus loc
 593       | IDENT "skip" -> G.Skip loc
 594       ]
 595       ];
 596   ntheorem_flavour: [
 597     [ [ IDENT "ndefinition"  ] -> `Definition
 598     | [ IDENT "nfact"        ] -> `Fact
 599     | [ IDENT "nlemma"       ] -> `Lemma
 600     | [ IDENT "nremark"      ] -> `Remark
 601     | [ IDENT "ntheorem"     ] -> `Theorem
 602     ]
 603   ];
 604   theorem_flavour: [
 605     [ [ IDENT "definition"  ] -> `Definition
 606     | [ IDENT "fact"        ] -> `Fact
 607     | [ IDENT "lemma"       ] -> `Lemma
 608     | [ IDENT "remark"      ] -> `Remark
 609     | [ IDENT "theorem"     ] -> `Theorem
 610     ]
 611   ];
 612   inline_flavour: [
 613      [ attr = theorem_flavour -> attr
 614      | [ IDENT "axiom"     ]  -> `Axiom
 615      | [ IDENT "variant"   ]  -> `Variant
 616      ]
 617   ];
 618   inductive_spec: [ [
 619     fst_name = IDENT;
 620       params = LIST0 protected_binder_vars;
 621     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 622     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 623     tl = OPT [ "with";
 624         types = LIST1 [
 625           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 626          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 627             (name, true, typ, constructors) ] SEP "with" -> types
 628       ] ->
 629         let params =
 630           List.fold_right
 631             (fun (names, typ) acc ->
 632               (List.map (fun name -> (name, typ)) names) @ acc)
 633             params []
 634         in
 635         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 636         let tl_ind_types = match tl with None -> [] | Some types -> types in
 637         let ind_types = fst_ind_type :: tl_ind_types in
 638         (params, ind_types)
 639     ] ];
 640
 641     record_spec: [ [
 642       name = IDENT;
 643       params = LIST0 protected_binder_vars;
 644        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 645        fields = LIST0 [
 646          name = IDENT ;
 647          coercion = [
 648              SYMBOL ":" -> false,0
 649            | SYMBOL ":"; SYMBOL ">" -> true,0
 650            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 651          ];
 652          ty = term ->
 653            let b,n = coercion in
 654            (name,ty,b,n)
 655        ] SEP SYMBOL ";"; SYMBOL "}" ->
 656         let params =
 657           List.fold_right
 658             (fun (names, typ) acc ->
 659               (List.map (fun name -> (name, typ)) names) @ acc)
 660             params []
 661         in
 662         (params,name,typ,fields)
 663     ] ];
 664
 665     nmacro: [
 666       [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
 667       | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
 668       ]
 669     ];
 670
 671     macro: [
 672       [ [ IDENT "check"   ]; t = term ->
 673           G.Check (loc, t)
 674       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 675           G.Eval (loc, kind, t)
 676       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 677            G.Inline (loc, suri, params)
 678       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 679            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 680       | IDENT "auto"; params = auto_params ->
 681           G.AutoInteractive (loc,params)
 682       | [ IDENT "whelp"; "match" ] ; t = term ->
 683           G.WMatch (loc,t)
 684       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 685           G.WInstance (loc,t)
 686       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 687           G.WLocate (loc,id)
 688       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 689           G.WElim (loc, t)
 690       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 691           G.WHint (loc,t)
 692       ]
 693     ];
 694     alias_spec: [
 695       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 696         let alpha = "[a-zA-Z]" in
 697         let num = "[0-9]+" in
 698         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 699         let decoration = "\\'" in
 700         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 701         let rex = Str.regexp ("^"^ident^"$") in
 702         if Str.string_match rex id 0 then
 703           if (try ignore (UriManager.uri_of_string uri); true
 704               with UriManager.IllFormedUri _ -> false) ||
 705              (try ignore (NReference.reference_of_string uri); true
 706               with NReference.IllFormedReference _ -> false)
 707           then
 708             L.Ident_alias (id, uri)
 709           else
 710             raise
 711              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 712         else
 713           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 714             Printf.sprintf "Not a valid identifier: %s" id)))
 715       | IDENT "symbol"; symbol = QSTRING;
 716         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 717         SYMBOL "="; dsc = QSTRING ->
 718           let instance =
 719             match instance with Some i -> i | None -> 0
 720           in
 721           L.Symbol_alias (symbol, instance, dsc)
 722       | IDENT "num";
 723         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 724         SYMBOL "="; dsc = QSTRING ->
 725           let instance =
 726             match instance with Some i -> i | None -> 0
 727           in
 728           L.Number_alias (instance, dsc)
 729       ]
 730      ];
 731     argument: [
 732       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 733         id = IDENT ->
 734           N.IdentArg (List.length l, id)
 735       ]
 736     ];
 737     associativity: [
 738       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 739       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 740       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 741       ]
 742     ];
 743     precedence: [
 744       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 745     ];
 746     notation: [
 747       [ dir = OPT direction; s = QSTRING;
 748         assoc = OPT associativity; prec = precedence;
 749         IDENT "for";
 750         p2 =
 751           [ blob = UNPARSED_AST ->
 752               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 753                 (CicNotationParser.parse_level2_ast
 754                   (Ulexing.from_utf8_string blob))
 755           | blob = UNPARSED_META ->
 756               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 757                 (CicNotationParser.parse_level2_meta
 758                   (Ulexing.from_utf8_string blob))
 759           ] ->
 760             let assoc =
 761               match assoc with
 762               | None -> default_associativity
 763               | Some assoc -> assoc
 764             in
 765             let p1 =
 766               add_raw_attribute ~text:s
 767                 (CicNotationParser.parse_level1_pattern prec
 768                   (Ulexing.from_utf8_string s))
 769             in
 770             (dir, p1, assoc, prec, p2)
 771       ]
 772     ];
 773     level3_term: [
 774       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 775       | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
 776       | IMPLICIT -> N.ImplicitPattern
 777       | id = IDENT -> N.VarPattern id
 778       | LPAREN; terms = LIST1 SELF; RPAREN ->
 779           (match terms with
 780           | [] -> assert false
 781           | [term] -> term
 782           | terms -> N.ApplPattern terms)
 783       ]
 784     ];
 785     interpretation: [
 786       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 787           (s, args, t)
 788       ]
 789     ];
 790
 791     include_command: [ [
 792         IDENT "include" ; path = QSTRING ->
 793           loc,path,true,L.WithPreferences
 794       | IDENT "include" ; IDENT "source" ; path = QSTRING ->
 795           loc,path,false,L.WithPreferences
 796       | IDENT "include'" ; path = QSTRING ->
 797           loc,path,true,L.WithoutPreferences
 798      ]];
 799
 800   grafite_ncommand: [ [
 801       IDENT "nqed" -> G.NQed loc
 802     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 803       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 804         G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
 805     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 806       body = term ->
 807         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
 808     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 809         G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
 810     | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
 811     | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
 812       paramspec = OPT inverter_param_list ;
 813       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
 814         G.NInverter (loc,name,indty,paramspec,outsort)
 815     | NLETCOREC ; defs = let_defs ->
 816         nmk_rec_corec `CoInductive defs loc
 817     | NLETREC ; defs = let_defs ->
 818         nmk_rec_corec `Inductive defs loc
 819     | IDENT "ninductive"; spec = inductive_spec ->
 820         let (params, ind_types) = spec in
 821         G.NObj (loc, N.Inductive (params, ind_types))
 822     | IDENT "ncoinductive"; spec = inductive_spec ->
 823         let (params, ind_types) = spec in
 824         let ind_types = (* set inductive flags to false (coinductive) *)
 825           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 826             ind_types
 827         in
 828         G.NObj (loc, N.Inductive (params, ind_types))
 829     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
 830         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
 831         let urify = function
 832           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 833               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 834           | _ -> raise (Failure "only a Type[…] sort can be constrained")
 835         in
 836         let u1 = urify u1 in
 837         let u2 = urify u2 in
 838          G.NUnivConstraint (loc,u1,u2)
 839     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 840         G.UnificationHint (loc, t, n)
 841     | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
 842         SYMBOL <:unicode<def>>; t = term; "on";
 843         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
 844         "to"; target = term ->
 845           G.NCoercion(loc,name,t,ty,(id,source),target)
 846     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 847         G.NObj (loc, N.Record (params,name,ty,fields))
 848     | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
 849       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
 850         G.NCopy (loc,s,NUri.uri_of_string u,
 851           List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
 852   ]];
 853
 854   grafite_command: [ [
 855       IDENT "set"; n = QSTRING; v = QSTRING ->
 856         G.Set (loc, n, v)
 857     | IDENT "drop" -> G.Drop loc
 858     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 859     | IDENT "qed" -> G.Qed loc
 860     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 861       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 862         G.Obj (loc,
 863           N.Theorem
 864             (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
 865     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 866       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 867         G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
 868     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 869       body = term ->
 870         G.Obj (loc,
 871           N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
 872     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 873         G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
 874     | LETCOREC ; defs = let_defs ->
 875         mk_rec_corec `CoInductive defs loc
 876     | LETREC ; defs = let_defs ->
 877         mk_rec_corec `Inductive defs loc
 878     | IDENT "inductive"; spec = inductive_spec ->
 879         let (params, ind_types) = spec in
 880         G.Obj (loc, N.Inductive (params, ind_types))
 881     | IDENT "coinductive"; spec = inductive_spec ->
 882         let (params, ind_types) = spec in
 883         let ind_types = (* set inductive flags to false (coinductive) *)
 884           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 885             ind_types
 886         in
 887         G.Obj (loc, N.Inductive (params, ind_types))
 888     | IDENT "coercion" ;
 889       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 890       arity = OPT int ; saturations = OPT int;
 891       composites = OPT (IDENT "nocomposites") ->
 892         let arity = match arity with None -> 0 | Some x -> x in
 893         let saturations = match saturations with None -> 0 | Some x -> x in
 894         let composites = match composites with None -> true | Some _ -> false in
 895         G.Coercion
 896          (loc, t, composites, arity, saturations)
 897     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 898         G.PreferCoercion (loc, t)
 899     | IDENT "pump" ; steps = int ->
 900         G.Pump(loc,steps)
 901     | IDENT "inverter"; name = IDENT; IDENT "for";
 902         indty = tactic_term; paramspec = inverter_param_list ->
 903           G.Inverter
 904             (loc, name, indty, paramspec)
 905     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 906         G.Obj (loc, N.Record (params,name,ty,fields))
 907     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 908        let uris = List.map UriManager.uri_of_string uris in
 909         G.Default (loc,what,uris)
 910     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 911       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 912                    refl = tactic_term -> refl ] ;
 913       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 914                    sym = tactic_term -> sym ] ;
 915       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 916                    trans = tactic_term -> trans ] ;
 917       "as" ; id = IDENT ->
 918        G.Relation (loc,id,a,aeq,refl,sym,trans)
 919   ]];
 920   lexicon_command: [ [
 921       IDENT "alias" ; spec = alias_spec ->
 922         L.Alias (loc, spec)
 923     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 924         L.Notation (loc, dir, l1, assoc, prec, l2)
 925     | IDENT "interpretation"; id = QSTRING;
 926       (symbol, args, l3) = interpretation ->
 927         L.Interpretation (loc, id, (symbol, args), l3)
 928   ]];
 929   executable: [
 930     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 931     | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
 932     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 933         G.Tactic (loc, Some tac, punct)
 934     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 935     | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 936         G.NTactic (loc, [tac; npunct_of_punct punct])
 937     | tac = ntactic; punct = punctuation_tactical ->
 938         G.NTactic (loc, [tac; npunct_of_punct punct])
 939     | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
 940         G.NTactic (loc, [punct])
 941     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 942         G.NonPunctuationTactical (loc, tac, punct)
 943     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 944         SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 945           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 946     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
 947         punct = punctuation_tactical ->
 948           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
 949     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 950     | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
 951     ]
 952   ];
 953   comment: [
 954     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 955        G.Code (loc, ex)
 956     | str = NOTE ->
 957        G.Note (loc, str)
 958     ]
 959   ];
 960   statement: [
 961     [ ex = executable ->
 962        fun ?(never_include=false) ~include_paths status ->
 963           let stm = G.Executable (loc, ex) in
 964           !grafite_callback stm;
 965           status, LSome stm
 966     | com = comment ->
 967        fun ?(never_include=false) ~include_paths status ->
 968           let stm = G.Comment (loc, com) in
 969           !grafite_callback stm;
 970           status, LSome stm
 971     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
 972        fun ?(never_include=false) ~include_paths status ->
 973         let _root, buri, fullpath, _rrelpath =
 974           Librarian.baseuri_of_script ~include_paths fname in
 975         if never_include then raise (NoInclusionPerformed fullpath)
 976         else
 977          begin
 978           let stm =
 979            G.Executable
 980             (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
 981           !grafite_callback stm;
 982           let status =
 983            LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
 984           let stm =
 985            G.Executable
 986             (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
 987           in
 988            status, LSome stm
 989          end
 990     | scom = lexicon_command ; SYMBOL "." ->
 991        fun ?(never_include=false) ~include_paths status ->
 992           !lexicon_callback scom;
 993           let status = LE.eval_command status scom in
 994           status, LNone loc
 995     | EOI -> raise End_of_file
 996     ]
 997   ];
 998 END
 999 (* }}} *)
1000 ;;
1001
1002 let _ = initialize_parser () ;;
1003
1004 let exc_located_wrapper f =
1005   try
1006     f ()
1007   with
1008   | Ploc.Exc (_, End_of_file) -> raise End_of_file
1009   | Ploc.Exc (floc, Stream.Error msg) ->
1010       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1011   | Ploc.Exc (floc, HExtlib.Localized(_,exn)) ->
1012       raise
1013        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1014   | Ploc.Exc (floc, exn) ->
1015       raise
1016        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1017
1018 let parse_statement lexbuf =
1019   exc_located_wrapper
1020     (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1021
1022 let statement () = Obj.magic !grafite_parser.statement
1023
1024 let history = ref [] ;;
1025
1026 let push () =
1027   LexiconSync.push ();
1028   history := !grafite_parser :: !history;
1029   grafite_parser := initial_parser ();
1030   initialize_parser ()
1031 ;;
1032
1033 let pop () =
1034   LexiconSync.pop ();
1035   match !history with
1036   | [] -> assert false
1037   | gp :: tail ->
1038       grafite_parser := gp;
1039       history := tail
1040 ;;
1041
1042 (* vim:set foldmethod=marker: *)
1043
1044