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