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