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