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 statement =
  43   ?never_include:bool -> include_paths:string list -> LE.status ->
  44     LE.status * ast_statement localized_option
  45
  46 type parser_status = {
  47   grammar : Grammar.g;
  48   term : N.term Grammar.Entry.e;
  49   statement : statement Grammar.Entry.e;
  50 }
  51
  52 let grafite_callback = ref (fun _ _ -> ())
  53 let set_grafite_callback cb = grafite_callback := cb
  54
  55 let lexicon_callback = ref (fun _ _ -> ())
  56 let set_lexicon_callback cb = lexicon_callback := cb
  57
  58 let initial_parser () =
  59   let grammar = CicNotationParser.level2_ast_grammar () in
  60   let term = CicNotationParser.term () in
  61   let statement = Grammar.Entry.create grammar "statement" in
  62   { grammar = grammar; term = term; statement = statement }
  63 ;;
  64
  65 let grafite_parser = ref (initial_parser ())
  66
  67 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
  68
  69 let default_associativity = Gramext.NonA
  70
  71 let mk_rec_corec ng ind_kind defs loc =
  72  (* In case of mutual definitions here we produce just
  73     the syntax tree for the first one. The others will be
  74     generated from the completely specified term just before
  75     insertion in the environment. We use the flavour
  76     `MutualDefinition to rememer this. *)
  77   let name,ty =
  78     match defs with
  79     | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
  80         let ty =
  81          List.fold_right
  82           (fun var ty -> N.Binder (`Pi,var,ty)
  83           ) params ty
  84         in
  85          name,ty
  86     | (_,(N.Ident (name, None), None),_,_) :: _ ->
  87         name, N.Implicit
  88     | _ -> assert false
  89   in
  90   let body = N.Ident (name,None) in
  91   let flavour =
  92    if List.length defs = 1 then
  93     `Definition
  94    else
  95     `MutualDefinition
  96   in
  97    if ng then
  98     G.NObj (loc, N.Theorem(flavour, name, ty,
  99      Some (N.LetRec (ind_kind, defs, body))))
 100    else
 101     G.Obj (loc, N.Theorem(flavour, name, ty,
 102      Some (N.LetRec (ind_kind, defs, body))))
 103
 104 type by_continuation =
 105    BYC_done
 106  | BYC_weproved of N.term * string option * N.term option
 107  | BYC_letsuchthat of string * N.term * string * N.term
 108  | BYC_wehaveand of string * N.term * string * N.term
 109
 110 let initialize_parser () =
 111   (* {{{ parser initialization *)
 112   let term = !grafite_parser.term in
 113   let statement = !grafite_parser.statement in
 114   let let_defs = CicNotationParser.let_defs () in
 115   let protected_binder_vars = CicNotationParser.protected_binder_vars () in
 116 EXTEND
 117   GLOBAL: term statement;
 118   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
 119   tactic_term: [ [ t = term LEVEL "90" -> t ] ];
 120   new_name: [
 121     [ id = IDENT -> Some id
 122     | SYMBOL "_" -> None ]
 123     ];
 124   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
 125   tactic_term_list1: [
 126     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
 127   ];
 128   reduction_kind: [
 129     [ IDENT "normalize" -> `Normalize
 130     | IDENT "simplify" -> `Simpl
 131     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
 132     | IDENT "whd" -> `Whd ]
 133   ];
 134   sequent_pattern_spec: [
 135    [ hyp_paths =
 136       LIST0
 137        [ id = IDENT ;
 138          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
 139          (id,match path with Some p -> p | None -> N.UserInput) ];
 140      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
 141       let goal_path =
 142        match goal_path, hyp_paths with
 143           None, [] -> Some N.UserInput
 144         | None, _::_ -> None
 145         | Some goal_path, _ -> Some goal_path
 146       in
 147        hyp_paths,goal_path
 148    ]
 149   ];
 150   pattern_spec: [
 151     [ res = OPT [
 152        "in";
 153        wanted_and_sps =
 154         [ "match" ; wanted = tactic_term ;
 155           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 156            Some wanted,sps
 157         | sps = sequent_pattern_spec ->
 158            None,Some sps
 159         ] ->
 160          let wanted,hyp_paths,goal_path =
 161           match wanted_and_sps with
 162              wanted,None -> wanted, [], Some N.UserInput
 163            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 164          in
 165           wanted, hyp_paths, goal_path ] ->
 166       match res with
 167          None -> None,[],Some N.UserInput
 168        | Some ps -> ps]
 169   ];
 170   inverter_param_list: [
 171     [ params = tactic_term ->
 172       let deannotate = function
 173         | N.AttributedTerm (_,t) | t -> t
 174       in match deannotate params with
 175       | N.Implicit -> [false]
 176       | N.UserInput -> [true]
 177       | N.Appl l ->
 178          List.map (fun x -> match deannotate x with
 179            | N.Implicit -> false
 180            | N.UserInput -> true
 181            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
 182       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
 183   ];
 184   direction: [
 185     [ SYMBOL ">" -> `LeftToRight
 186     | SYMBOL "<" -> `RightToLeft ]
 187   ];
 188   int: [ [ num = NUMBER -> int_of_string num ] ];
 189   intros_names: [
 190    [ idents = OPT ident_list0 ->
 191       match idents with None -> [] | Some idents -> idents
 192    ]
 193   ];
 194   intros_spec: [
 195     [ OPT [ IDENT "names" ];
 196       num = OPT [ num = int -> num ];
 197       idents = intros_names ->
 198         num, idents
 199     ]
 200   ];
 201   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 202   ntactic: [
 203     [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
 204     | IDENT "nassert";
 205        seqs = LIST0 [
 206         hyps = LIST0
 207          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 208          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 209                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 210             id,`Def (bo,ty)];
 211         SYMBOL <:unicode<vdash>>;
 212         concl = tactic_term -> (List.rev hyps,concl) ] ->
 213          G.NAssert (loc, seqs)
 214     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 215         G.NCases (loc, what, where)
 216     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 217         G.NChange (loc, what, with_what)
 218     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 219         G.NElim (loc, what, where)
 220     | IDENT "ngeneralize"; p=pattern_spec ->
 221         G.NGeneralize (loc, p)
 222     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 223         where = pattern_spec ->
 224         G.NLetIn (loc,where,t,name)
 225     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 226         G.NRewrite (loc, dir, what, where)
 227     | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
 228       where = pattern_spec ->
 229         let delta = match delta with None -> true | _ -> false in
 230         G.NEval (loc, where, `Whd delta)
 231     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
 232     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
 233     | SYMBOL "*" -> G.NCase1 (loc,"_")
 234     | SYMBOL "*"; n=IDENT ->
 235         G.NCase1 (loc,n)
 236     ]
 237   ];
 238   tactic: [
 239     [ IDENT "absurd"; t = tactic_term ->
 240         G.Absurd (loc, t)
 241     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 242         G.ApplyRule (loc, t)
 243     | IDENT "apply"; t = tactic_term ->
 244         G.Apply (loc, t)
 245     | IDENT "applyP"; t = tactic_term ->
 246         G.ApplyP (loc, t)
 247     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 248         G.ApplyS (loc, t, params)
 249     | IDENT "assumption" ->
 250         G.Assumption loc
 251     | IDENT "autobatch";  params = auto_params ->
 252         G.AutoBatch (loc,params)
 253     | IDENT "cases"; what = tactic_term;
 254       pattern = OPT pattern_spec;
 255       specs = intros_spec ->
 256         let pattern = match pattern with
 257            | None         -> None, [], Some N.UserInput
 258            | Some pattern -> pattern
 259         in
 260         G.Cases (loc, what, pattern, specs)
 261     | IDENT "clear"; ids = LIST1 IDENT ->
 262         G.Clear (loc, ids)
 263     | IDENT "clearbody"; id = IDENT ->
 264         G.ClearBody (loc,id)
 265     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 266         G.Change (loc, what, t)
 267     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 268       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 269         let times = match times with None -> 1 | Some i -> i in
 270         G.Compose (loc, t1, t2, times, specs)
 271     | IDENT "constructor"; n = int ->
 272         G.Constructor (loc, n)
 273     | IDENT "contradiction" ->
 274         G.Contradiction loc
 275     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 276         G.Cut (loc, ident, t)
 277     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 278         let idents = match idents with None -> [] | Some idents -> idents in
 279         G.Decompose (loc, idents)
 280     | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
 281     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 282         G.Destruct (loc, xts)
 283     | IDENT "elim"; what = tactic_term; using = using;
 284        pattern = OPT pattern_spec;
 285        ispecs = intros_spec ->
 286         let pattern = match pattern with
 287            | None         -> None, [], Some N.UserInput
 288            | Some pattern -> pattern
 289           in
 290           G.Elim (loc, what, using, pattern, ispecs)
 291     | IDENT "elimType"; what = tactic_term; using = using;
 292       (num, idents) = intros_spec ->
 293         G.ElimType (loc, what, using, (num, idents))
 294     | IDENT "exact"; t = tactic_term ->
 295         G.Exact (loc, t)
 296     | IDENT "exists" ->
 297         G.Exists loc
 298     | IDENT "fail" -> G.Fail loc
 299     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 300         let (pt,_,_) = p in
 301           if pt <> None then
 302             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 303               ("the pattern cannot specify the term to replace, only its"
 304               ^ " paths in the hypotheses and in the conclusion")))
 305        else
 306          G.Fold (loc, kind, t, p)
 307     | IDENT "fourier" ->
 308         G.Fourier loc
 309     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 310         let idents = match idents with None -> [] | Some idents -> idents in
 311         G.FwdSimpl (loc, hyp, idents)
 312     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 313        G.Generalize (loc,p,id)
 314     | IDENT "id" -> G.IdTac loc
 315     | IDENT "intro"; ident = OPT IDENT ->
 316         let idents = match ident with None -> [] | Some id -> [Some id] in
 317         G.Intros (loc, (Some 1, idents))
 318     | IDENT "intros"; specs = intros_spec ->
 319         G.Intros (loc, specs)
 320     | IDENT "inversion"; t = tactic_term ->
 321         G.Inversion (loc, t)
 322     | IDENT "lapply";
 323       linear = OPT [ IDENT "linear" ];
 324       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 325       what = tactic_term;
 326       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 327       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 328         let linear = match linear with None -> false | Some _ -> true in
 329         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 330         G.LApply (loc, linear, depth, to_what, what, ident)
 331     | IDENT "left" -> G.Left loc
 332     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 333         G.LetIn (loc, t, where)
 334     | kind = reduction_kind; p = pattern_spec ->
 335         G.Reduce (loc, kind, p)
 336     | IDENT "reflexivity" ->
 337         G.Reflexivity loc
 338     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 339         G.Replace (loc, p, t)
 340     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 341        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 342        let (pt,_,_) = p in
 343         if pt <> None then
 344          raise
 345           (HExtlib.Localized (loc,
 346            (CicNotationParser.Parse_error
 347             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 348         else
 349          let n = match xnames with None -> [] | Some names -> names in
 350          G.Rewrite (loc, d, t, p, n)
 351     | IDENT "right" ->
 352         G.Right loc
 353     | IDENT "ring" ->
 354         G.Ring loc
 355     | IDENT "split" ->
 356         G.Split loc
 357     | IDENT "symmetry" ->
 358         G.Symmetry loc
 359     | IDENT "transitivity"; t = tactic_term ->
 360         G.Transitivity (loc, t)
 361      (* Produzioni Aggiunte *)
 362     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 363         G.Assume (loc, id, t)
 364     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 365       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 366                 t' = tactic_term -> t']->
 367         G.Suppose (loc, t, id, t1)
 368     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 369       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 370       id2 = IDENT ; RPAREN ->
 371         G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 372     | just =
 373        [ IDENT "using"; t=tactic_term -> `Term t
 374        | params = auto_params -> `Auto params] ;
 375       cont=by_continuation ->
 376        (match cont with
 377            BYC_done -> G.Bydone (loc, just)
 378          | BYC_weproved (ty,id,t1) ->
 379             G.By_just_we_proved(loc, just, ty, id, t1)
 380          | BYC_letsuchthat (id1,t1,id2,t2) ->
 381             G.ExistsElim (loc, just, id1, t1, id2, t2)
 382          | BYC_wehaveand (id1,t1,id2,t2) ->
 383             G.AndElim (loc, just, id1, t1, id2, t2))
 384     | 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']->
 385         G.We_need_to_prove (loc, t, id, t1)
 386     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 387         G.We_proceed_by_cases_on (loc, t, t1)
 388     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 389         G.We_proceed_by_induction_on (loc, t, t1)
 390     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 391         G.Byinduction(loc, t, id)
 392     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 393         G.Thesisbecomes(loc, t)
 394     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 395         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 396          G.Case(loc,id,params)
 397       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 398     | IDENT "conclude";
 399       termine = tactic_term;
 400       SYMBOL "=" ;
 401       t1=tactic_term ;
 402       t2 =
 403        [ IDENT "using"; t=tactic_term -> `Term t
 404        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 405        | IDENT "proof" -> `Proof
 406        | params = auto_params -> `Auto params];
 407       cont = rewriting_step_continuation ->
 408        G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 409     | IDENT "obtain" ; name = IDENT;
 410       termine = tactic_term;
 411       SYMBOL "=" ;
 412       t1=tactic_term ;
 413       t2 =
 414        [ IDENT "using"; t=tactic_term -> `Term t
 415        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 416        | IDENT "proof" -> `Proof
 417        | params = auto_params -> `Auto params];
 418       cont = rewriting_step_continuation ->
 419        G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 420     | SYMBOL "=" ;
 421       t1=tactic_term ;
 422       t2 =
 423        [ IDENT "using"; t=tactic_term -> `Term t
 424        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 425        | IDENT "proof" -> `Proof
 426        | params = auto_params -> `Auto params];
 427       cont = rewriting_step_continuation ->
 428        G.RewritingStep(loc, None, t1, t2, cont)
 429   ]
 430 ];
 431   auto_fixed_param: [
 432    [ IDENT "paramodulation"
 433    | IDENT "depth"
 434    | IDENT "width"
 435    | IDENT "size"
 436    | IDENT "timeout"
 437    | IDENT "library"
 438    | IDENT "type"
 439    | IDENT "all"
 440    ]
 441 ];
 442   auto_params: [
 443    [ params =
 444       LIST0 [
 445          i = auto_fixed_param -> i,""
 446        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 447               string_of_int v | v = IDENT -> v ] -> i,v ];
 448       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 449       (match tl with Some l -> l | None -> []),
 450       params
 451    ]
 452 ];
 453   inline_params:[
 454    [ params = LIST0
 455       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
 456       | IDENT "procedural" -> G.IPProcedural
 457       | flavour = inline_flavour -> G.IPAs flavour
 458       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 459       | IDENT "nodefaults" -> G.IPNoDefaults
 460       ] -> params
 461    ]
 462 ];
 463   by_continuation: [
 464     [ 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)
 465     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 466             "done" -> BYC_weproved (ty,None,t1)
 467     | "done" -> BYC_done
 468     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 469       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 470       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 471     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 472               BYC_wehaveand (id1,t1,id2,t2)
 473     ]
 474 ];
 475   rewriting_step_continuation : [
 476     [ "done" -> true
 477     | -> false
 478     ]
 479 ];
 480   atomic_tactical:
 481     [ "sequence" LEFTA
 482       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 483           let ts =
 484             match t1 with
 485             | G.Seq (_, l) -> l @ [ t2 ]
 486             | _ -> [ t1; t2 ]
 487           in
 488           G.Seq (loc, ts)
 489       ]
 490     | "then" NONA
 491       [ tac = SELF; SYMBOL ";";
 492         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 493           (G.Then (loc, tac, tacs))
 494       ]
 495     | "loops" RIGHTA
 496       [ IDENT "do"; count = int; tac = SELF ->
 497           G.Do (loc, count, tac)
 498       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 499       ]
 500     | "simple" NONA
 501       [ IDENT "first";
 502         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 503           G.First (loc, tacs)
 504       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 505       | IDENT "solve";
 506         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 507           G.Solve (loc, tacs)
 508       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 509       | LPAREN; tac = SELF; RPAREN -> tac
 510       | tac = tactic -> tac
 511         ]
 512       ];
 513   punctuation_tactical:
 514     [
 515       [ SYMBOL "[" -> G.Branch loc
 516       | SYMBOL "|" -> G.Shift loc
 517       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 518       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 519       | SYMBOL "]" -> G.Merge loc
 520       | SYMBOL ";" -> G.Semicolon loc
 521       | SYMBOL "." -> G.Dot loc
 522       ]
 523     ];
 524   non_punctuation_tactical:
 525     [ "simple" NONA
 526       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 527       | IDENT "unfocus" -> G.Unfocus loc
 528       | IDENT "skip" -> G.Skip loc
 529       ]
 530       ];
 531   ntheorem_flavour: [
 532     [ [ IDENT "ndefinition"  ] -> `Definition
 533     | [ IDENT "nfact"        ] -> `Fact
 534     | [ IDENT "nlemma"       ] -> `Lemma
 535     | [ IDENT "nremark"      ] -> `Remark
 536     | [ IDENT "ntheorem"     ] -> `Theorem
 537     ]
 538   ];
 539   theorem_flavour: [
 540     [ [ IDENT "definition"  ] -> `Definition
 541     | [ IDENT "fact"        ] -> `Fact
 542     | [ IDENT "lemma"       ] -> `Lemma
 543     | [ IDENT "remark"      ] -> `Remark
 544     | [ IDENT "theorem"     ] -> `Theorem
 545     ]
 546   ];
 547   inline_flavour: [
 548      [ attr = theorem_flavour -> attr
 549      | [ IDENT "axiom"     ]  -> `Axiom
 550      | [ IDENT "variant"   ]  -> `Variant
 551      ]
 552   ];
 553   inductive_spec: [ [
 554     fst_name = IDENT;
 555       params = LIST0 protected_binder_vars;
 556     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 557     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 558     tl = OPT [ "with";
 559         types = LIST1 [
 560           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 561          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 562             (name, true, typ, constructors) ] SEP "with" -> types
 563       ] ->
 564         let params =
 565           List.fold_right
 566             (fun (names, typ) acc ->
 567               (List.map (fun name -> (name, typ)) names) @ acc)
 568             params []
 569         in
 570         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 571         let tl_ind_types = match tl with None -> [] | Some types -> types in
 572         let ind_types = fst_ind_type :: tl_ind_types in
 573         (params, ind_types)
 574     ] ];
 575
 576     record_spec: [ [
 577       name = IDENT;
 578       params = LIST0 protected_binder_vars;
 579        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 580        fields = LIST0 [
 581          name = IDENT ;
 582          coercion = [
 583              SYMBOL ":" -> false,0
 584            | SYMBOL ":"; SYMBOL ">" -> true,0
 585            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 586          ];
 587          ty = term ->
 588            let b,n = coercion in
 589            (name,ty,b,n)
 590        ] SEP SYMBOL ";"; SYMBOL "}" ->
 591         let params =
 592           List.fold_right
 593             (fun (names, typ) acc ->
 594               (List.map (fun name -> (name, typ)) names) @ acc)
 595             params []
 596         in
 597         (params,name,typ,fields)
 598     ] ];
 599
 600     macro: [
 601       [ [ IDENT "check"   ]; t = term ->
 602           G.Check (loc, t)
 603       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 604           G.Eval (loc, kind, t)
 605       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 606            G.Inline (loc, suri, params)
 607       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 608            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 609       | IDENT "auto"; params = auto_params ->
 610           G.AutoInteractive (loc,params)
 611       | [ IDENT "whelp"; "match" ] ; t = term ->
 612           G.WMatch (loc,t)
 613       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 614           G.WInstance (loc,t)
 615       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 616           G.WLocate (loc,id)
 617       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 618           G.WElim (loc, t)
 619       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 620           G.WHint (loc,t)
 621       ]
 622     ];
 623     alias_spec: [
 624       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 625         let alpha = "[a-zA-Z]" in
 626         let num = "[0-9]+" in
 627         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 628         let decoration = "\\'" in
 629         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 630         let rex = Str.regexp ("^"^ident^"$") in
 631         if Str.string_match rex id 0 then
 632           if (try ignore (UriManager.uri_of_string uri); true
 633               with UriManager.IllFormedUri _ -> false) ||
 634              (try ignore (NReference.reference_of_string uri); true
 635               with NReference.IllFormedReference _ -> false)
 636           then
 637             L.Ident_alias (id, uri)
 638           else
 639             raise
 640              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 641         else
 642           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 643             Printf.sprintf "Not a valid identifier: %s" id)))
 644       | IDENT "symbol"; symbol = QSTRING;
 645         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 646         SYMBOL "="; dsc = QSTRING ->
 647           let instance =
 648             match instance with Some i -> i | None -> 0
 649           in
 650           L.Symbol_alias (symbol, instance, dsc)
 651       | IDENT "num";
 652         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 653         SYMBOL "="; dsc = QSTRING ->
 654           let instance =
 655             match instance with Some i -> i | None -> 0
 656           in
 657           L.Number_alias (instance, dsc)
 658       ]
 659     ];
 660     argument: [
 661       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 662         id = IDENT ->
 663           N.IdentArg (List.length l, id)
 664       ]
 665     ];
 666     associativity: [
 667       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 668       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 669       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 670       ]
 671     ];
 672     precedence: [
 673       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 674     ];
 675     notation: [
 676       [ dir = OPT direction; s = QSTRING;
 677         assoc = OPT associativity; prec = precedence;
 678         IDENT "for";
 679         p2 =
 680           [ blob = UNPARSED_AST ->
 681               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 682                 (CicNotationParser.parse_level2_ast
 683                   (Ulexing.from_utf8_string blob))
 684           | blob = UNPARSED_META ->
 685               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 686                 (CicNotationParser.parse_level2_meta
 687                   (Ulexing.from_utf8_string blob))
 688           ] ->
 689             let assoc =
 690               match assoc with
 691               | None -> default_associativity
 692               | Some assoc -> assoc
 693             in
 694             let p1 =
 695               add_raw_attribute ~text:s
 696                 (CicNotationParser.parse_level1_pattern prec
 697                   (Ulexing.from_utf8_string s))
 698             in
 699             (dir, p1, assoc, prec, p2)
 700       ]
 701     ];
 702     level3_term: [
 703       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 704       | id = IDENT -> N.VarPattern id
 705       | SYMBOL "_" -> N.ImplicitPattern
 706       | LPAREN; terms = LIST1 SELF; RPAREN ->
 707           (match terms with
 708           | [] -> assert false
 709           | [term] -> term
 710           | terms -> N.ApplPattern terms)
 711       ]
 712     ];
 713     interpretation: [
 714       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 715           (s, args, t)
 716       ]
 717     ];
 718
 719     include_command: [ [
 720         IDENT "include" ; path = QSTRING ->
 721           loc,path,L.WithPreferences
 722       | IDENT "include'" ; path = QSTRING ->
 723           loc,path,L.WithoutPreferences
 724      ]];
 725
 726   grafite_command: [ [
 727       IDENT "set"; n = QSTRING; v = QSTRING ->
 728         G.Set (loc, n, v)
 729     | IDENT "drop" -> G.Drop loc
 730     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 731     | IDENT "qed" -> G.Qed loc
 732     | IDENT "nqed" -> G.NQed loc
 733     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 734       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 735         G.Obj (loc,
 736           N.Theorem
 737             (`Variant,name,typ,Some (N.Ident (newname, None))))
 738     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 739       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 740         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 741     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 742       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 743         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 744     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 745       body = term ->
 746         G.Obj (loc,
 747           N.Theorem (flavour, name, N.Implicit, Some body))
 748     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 749         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 750     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 751         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 752     | LETCOREC ; defs = let_defs ->
 753         mk_rec_corec false `CoInductive defs loc
 754     | LETREC ; defs = let_defs ->
 755         mk_rec_corec false `Inductive defs loc
 756     | NLETCOREC ; defs = let_defs ->
 757         mk_rec_corec true `CoInductive defs loc
 758     | NLETREC ; defs = let_defs ->
 759         mk_rec_corec true `Inductive defs loc
 760     | IDENT "inductive"; spec = inductive_spec ->
 761         let (params, ind_types) = spec in
 762         G.Obj (loc, N.Inductive (params, ind_types))
 763     | IDENT "ninductive"; spec = inductive_spec ->
 764         let (params, ind_types) = spec in
 765         G.NObj (loc, N.Inductive (params, ind_types))
 766     | IDENT "coinductive"; spec = inductive_spec ->
 767         let (params, ind_types) = spec in
 768         let ind_types = (* set inductive flags to false (coinductive) *)
 769           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 770             ind_types
 771         in
 772         G.Obj (loc, N.Inductive (params, ind_types))
 773     | IDENT "ncoinductive"; spec = inductive_spec ->
 774         let (params, ind_types) = spec in
 775         let ind_types = (* set inductive flags to false (coinductive) *)
 776           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 777             ind_types
 778         in
 779         G.NObj (loc, N.Inductive (params, ind_types))
 780     | IDENT "coercion" ;
 781       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 782       arity = OPT int ; saturations = OPT int;
 783       composites = OPT (IDENT "nocomposites") ->
 784         let arity = match arity with None -> 0 | Some x -> x in
 785         let saturations = match saturations with None -> 0 | Some x -> x in
 786         let composites = match composites with None -> true | Some _ -> false in
 787         G.Coercion
 788          (loc, t, composites, arity, saturations)
 789     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 790         G.PreferCoercion (loc, t)
 791     | IDENT "pump" ; steps = int ->
 792         G.Pump(loc,steps)
 793     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 794         G.UnificationHint (loc, t, n)
 795     | IDENT "inverter"; name = IDENT; IDENT "for";
 796         indty = tactic_term; paramspec = inverter_param_list ->
 797           G.Inverter
 798             (loc, name, indty, paramspec)
 799     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 800         G.Obj (loc, N.Record (params,name,ty,fields))
 801     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 802         G.NObj (loc, N.Record (params,name,ty,fields))
 803     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 804        let uris = List.map UriManager.uri_of_string uris in
 805         G.Default (loc,what,uris)
 806     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 807       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 808                    refl = tactic_term -> refl ] ;
 809       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 810                    sym = tactic_term -> sym ] ;
 811       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 812                    trans = tactic_term -> trans ] ;
 813       "as" ; id = IDENT ->
 814        G.Relation (loc,id,a,aeq,refl,sym,trans)
 815   ]];
 816   lexicon_command: [ [
 817       IDENT "alias" ; spec = alias_spec ->
 818         L.Alias (loc, spec)
 819     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 820         L.Notation (loc, dir, l1, assoc, prec, l2)
 821     | IDENT "interpretation"; id = QSTRING;
 822       (symbol, args, l3) = interpretation ->
 823         L.Interpretation (loc, id, (symbol, args), l3)
 824   ]];
 825   executable: [
 826     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 827     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 828         G.Tactic (loc, Some tac, punct)
 829     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 830     | tac = ntactic; punct = punctuation_tactical ->
 831         G.NTactic (loc, tac, punct)
 832     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 833         G.NTactic (loc, G.NId loc, punct)
 834     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 835         G.NonPunctuationTactical (loc, tac, punct)
 836     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 837     ]
 838   ];
 839   comment: [
 840     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 841        G.Code (loc, ex)
 842     | str = NOTE ->
 843        G.Note (loc, str)
 844     ]
 845   ];
 846   statement: [
 847     [ ex = executable ->
 848        fun ?(never_include=false) ~include_paths status ->
 849           let stm = G.Executable (loc, ex) in
 850           !grafite_callback status stm;
 851           status, LSome stm
 852     | com = comment ->
 853        fun ?(never_include=false) ~include_paths status ->
 854           let stm = G.Comment (loc, com) in
 855           !grafite_callback status stm;
 856           status, LSome stm
 857     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 858        fun ?(never_include=false) ~include_paths status ->
 859           let stm =
 860              G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
 861           in
 862           !grafite_callback status stm;
 863           let _root, buri, fullpath, _rrelpath =
 864             Librarian.baseuri_of_script ~include_paths fname
 865           in
 866           let stm =
 867              G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
 868           in
 869           let status =
 870             if never_include then raise (NoInclusionPerformed fullpath)
 871             else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
 872           in
 873           status, LSome stm
 874     | scom = lexicon_command ; SYMBOL "." ->
 875        fun ?(never_include=false) ~include_paths status ->
 876           !lexicon_callback status scom;
 877           let status = LE.eval_command status scom in
 878           status, LNone loc
 879     | EOI -> raise End_of_file
 880     ]
 881   ];
 882 END
 883 (* }}} *)
 884 ;;
 885
 886 let _ = initialize_parser () ;;
 887
 888 let exc_located_wrapper f =
 889   try
 890     f ()
 891   with
 892   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 893   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 894       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 895   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 896       raise
 897        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 898   | Stdpp.Exc_located (floc, exn) ->
 899       raise
 900        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 901
 902 let parse_statement lexbuf =
 903   exc_located_wrapper
 904     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 905
 906 let statement () = !grafite_parser.statement
 907
 908 let history = ref [] ;;
 909
 910 let push () =
 911   LexiconSync.push ();
 912   history := !grafite_parser :: !history;
 913   grafite_parser := initial_parser ();
 914   initialize_parser ()
 915 ;;
 916
 917 let pop () =
 918   LexiconSync.pop ();
 919   match !history with
 920   | [] -> assert false
 921   | gp :: tail ->
 922       grafite_parser := gp;
 923       history := tail
 924 ;;
 925
 926 (* vim:set foldmethod=marker: *)
 927
 928