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