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