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