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 "steps"
 440    | IDENT "all"
 441    ]
 442 ];
 443   auto_params: [
 444    [ params =
 445       LIST0 [
 446          i = auto_fixed_param -> i,""
 447        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 448               string_of_int v | v = IDENT -> v ] -> i,v ];
 449       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 450       (match tl with Some l -> l | None -> []),
 451       params
 452    ]
 453 ];
 454   by_continuation: [
 455     [ 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)
 456     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 457             "done" -> BYC_weproved (ty,None,t1)
 458     | "done" -> BYC_done
 459     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 460       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 461       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 462     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 463               BYC_wehaveand (id1,t1,id2,t2)
 464     ]
 465 ];
 466   rewriting_step_continuation : [
 467     [ "done" -> true
 468     | -> false
 469     ]
 470 ];
 471   atomic_tactical:
 472     [ "sequence" LEFTA
 473       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 474           let ts =
 475             match t1 with
 476             | G.Seq (_, l) -> l @ [ t2 ]
 477             | _ -> [ t1; t2 ]
 478           in
 479           G.Seq (loc, ts)
 480       ]
 481     | "then" NONA
 482       [ tac = SELF; SYMBOL ";";
 483         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 484           (G.Then (loc, tac, tacs))
 485       ]
 486     | "loops" RIGHTA
 487       [ IDENT "do"; count = int; tac = SELF ->
 488           G.Do (loc, count, tac)
 489       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 490       ]
 491     | "simple" NONA
 492       [ IDENT "first";
 493         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 494           G.First (loc, tacs)
 495       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 496       | IDENT "solve";
 497         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 498           G.Solve (loc, tacs)
 499       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 500       | LPAREN; tac = SELF; RPAREN -> tac
 501       | tac = tactic -> tac
 502         ]
 503       ];
 504   punctuation_tactical:
 505     [
 506       [ SYMBOL "[" -> G.Branch loc
 507       | SYMBOL "|" -> G.Shift loc
 508       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 509       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 510       | SYMBOL "]" -> G.Merge loc
 511       | SYMBOL ";" -> G.Semicolon loc
 512       | SYMBOL "." -> G.Dot loc
 513       ]
 514     ];
 515   non_punctuation_tactical:
 516     [ "simple" NONA
 517       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 518       | IDENT "unfocus" -> G.Unfocus loc
 519       | IDENT "skip" -> G.Skip loc
 520       ]
 521       ];
 522   ntheorem_flavour: [
 523     [ [ IDENT "ndefinition"  ] -> `Definition
 524     | [ IDENT "nfact"        ] -> `Fact
 525     | [ IDENT "nlemma"       ] -> `Lemma
 526     | [ IDENT "nremark"      ] -> `Remark
 527     | [ IDENT "ntheorem"     ] -> `Theorem
 528     ]
 529   ];
 530   theorem_flavour: [
 531     [ [ IDENT "definition"  ] -> `Definition
 532     | [ IDENT "fact"        ] -> `Fact
 533     | [ IDENT "lemma"       ] -> `Lemma
 534     | [ IDENT "remark"      ] -> `Remark
 535     | [ IDENT "theorem"     ] -> `Theorem
 536     ]
 537   ];
 538   inline_flavour: [
 539      [ attr = theorem_flavour -> attr
 540      | [ IDENT "axiom"     ]  -> `Axiom
 541      | [ IDENT "mutual"    ]  -> `MutualDefinition
 542      ]
 543   ];
 544   inductive_spec: [ [
 545     fst_name = IDENT;
 546       params = LIST0 protected_binder_vars;
 547     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 548     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 549     tl = OPT [ "with";
 550         types = LIST1 [
 551           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 552          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 553             (name, true, typ, constructors) ] SEP "with" -> types
 554       ] ->
 555         let params =
 556           List.fold_right
 557             (fun (names, typ) acc ->
 558               (List.map (fun name -> (name, typ)) names) @ acc)
 559             params []
 560         in
 561         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 562         let tl_ind_types = match tl with None -> [] | Some types -> types in
 563         let ind_types = fst_ind_type :: tl_ind_types in
 564         (params, ind_types)
 565     ] ];
 566
 567     record_spec: [ [
 568       name = IDENT;
 569       params = LIST0 protected_binder_vars;
 570        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 571        fields = LIST0 [
 572          name = IDENT ;
 573          coercion = [
 574              SYMBOL ":" -> false,0
 575            | SYMBOL ":"; SYMBOL ">" -> true,0
 576            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 577          ];
 578          ty = term ->
 579            let b,n = coercion in
 580            (name,ty,b,n)
 581        ] SEP SYMBOL ";"; SYMBOL "}" ->
 582         let params =
 583           List.fold_right
 584             (fun (names, typ) acc ->
 585               (List.map (fun name -> (name, typ)) names) @ acc)
 586             params []
 587         in
 588         (params,name,typ,fields)
 589     ] ];
 590
 591     macro: [
 592       [ [ IDENT "check"   ]; t = term ->
 593           G.Check (loc, t)
 594       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 595           G.Eval (loc, kind, t)
 596       | [ IDENT "inline"];
 597           style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 598           suri = QSTRING; prefix = OPT QSTRING;
 599           flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
 600            let style = match style with
 601               | None       -> G.Declarative
 602               | Some depth -> G.Procedural depth
 603            in
 604            let prefix = match prefix with None -> "" | Some prefix -> prefix in
 605            G.Inline (loc,style,suri,prefix, flavour)
 606       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 607            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 608       | IDENT "auto"; params = auto_params ->
 609           G.AutoInteractive (loc,params)
 610       | [ IDENT "whelp"; "match" ] ; t = term ->
 611           G.WMatch (loc,t)
 612       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 613           G.WInstance (loc,t)
 614       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 615           G.WLocate (loc,id)
 616       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 617           G.WElim (loc, t)
 618       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 619           G.WHint (loc,t)
 620       ]
 621     ];
 622     alias_spec: [
 623       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 624         let alpha = "[a-zA-Z]" in
 625         let num = "[0-9]+" in
 626         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 627         let decoration = "\\'" in
 628         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 629         let rex = Str.regexp ("^"^ident^"$") in
 630         if Str.string_match rex id 0 then
 631           if (try ignore (UriManager.uri_of_string uri); true
 632               with UriManager.IllFormedUri _ -> false)
 633           then
 634             L.Ident_alias (id, uri)
 635           else
 636             raise
 637              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 638         else
 639           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 640             Printf.sprintf "Not a valid identifier: %s" id)))
 641       | IDENT "symbol"; symbol = QSTRING;
 642         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 643         SYMBOL "="; dsc = QSTRING ->
 644           let instance =
 645             match instance with Some i -> i | None -> 0
 646           in
 647           L.Symbol_alias (symbol, instance, dsc)
 648       | IDENT "num";
 649         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 650         SYMBOL "="; dsc = QSTRING ->
 651           let instance =
 652             match instance with Some i -> i | None -> 0
 653           in
 654           L.Number_alias (instance, dsc)
 655       ]
 656     ];
 657     argument: [
 658       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 659         id = IDENT ->
 660           N.IdentArg (List.length l, id)
 661       ]
 662     ];
 663     associativity: [
 664       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 665       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 666       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 667       ]
 668     ];
 669     precedence: [
 670       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 671     ];
 672     notation: [
 673       [ dir = OPT direction; s = QSTRING;
 674         assoc = OPT associativity; prec = precedence;
 675         IDENT "for";
 676         p2 =
 677           [ blob = UNPARSED_AST ->
 678               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 679                 (CicNotationParser.parse_level2_ast
 680                   (Ulexing.from_utf8_string blob))
 681           | blob = UNPARSED_META ->
 682               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 683                 (CicNotationParser.parse_level2_meta
 684                   (Ulexing.from_utf8_string blob))
 685           ] ->
 686             let assoc =
 687               match assoc with
 688               | None -> default_associativity
 689               | Some assoc -> assoc
 690             in
 691             let p1 =
 692               add_raw_attribute ~text:s
 693                 (CicNotationParser.parse_level1_pattern prec
 694                   (Ulexing.from_utf8_string s))
 695             in
 696             (dir, p1, assoc, prec, p2)
 697       ]
 698     ];
 699     level3_term: [
 700       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 701       | id = IDENT -> N.VarPattern id
 702       | SYMBOL "_" -> N.ImplicitPattern
 703       | LPAREN; terms = LIST1 SELF; RPAREN ->
 704           (match terms with
 705           | [] -> assert false
 706           | [term] -> term
 707           | terms -> N.ApplPattern terms)
 708       ]
 709     ];
 710     interpretation: [
 711       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 712           (s, args, t)
 713       ]
 714     ];
 715
 716     include_command: [ [
 717         IDENT "include" ; path = QSTRING ->
 718           loc,path,L.WithPreferences
 719       | IDENT "include'" ; path = QSTRING ->
 720           loc,path,L.WithoutPreferences
 721      ]];
 722
 723   grafite_command: [ [
 724       IDENT "set"; n = QSTRING; v = QSTRING ->
 725         G.Set (loc, n, v)
 726     | IDENT "drop" -> G.Drop loc
 727     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 728     | IDENT "qed" -> G.Qed loc
 729     | IDENT "nqed" -> G.NQed loc
 730     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 731       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 732         G.Obj (loc,
 733           N.Theorem
 734             (`Variant,name,typ,Some (N.Ident (newname, None))))
 735     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 736       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 737         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 738     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 739       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 740         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 741     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 742       body = term ->
 743         G.Obj (loc,
 744           N.Theorem (flavour, name, N.Implicit, Some body))
 745     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 746         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 747     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 748         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 749     | LETCOREC ; defs = let_defs ->
 750         mk_rec_corec false `CoInductive defs loc
 751     | LETREC ; defs = let_defs ->
 752         mk_rec_corec false `Inductive defs loc
 753     | NLETCOREC ; defs = let_defs ->
 754         mk_rec_corec true `CoInductive defs loc
 755     | NLETREC ; defs = let_defs ->
 756         mk_rec_corec true `Inductive defs loc
 757     | IDENT "inductive"; spec = inductive_spec ->
 758         let (params, ind_types) = spec in
 759         G.Obj (loc, N.Inductive (params, ind_types))
 760     | IDENT "ninductive"; spec = inductive_spec ->
 761         let (params, ind_types) = spec in
 762         G.NObj (loc, N.Inductive (params, ind_types))
 763     | IDENT "coinductive"; spec = inductive_spec ->
 764         let (params, ind_types) = spec in
 765         let ind_types = (* set inductive flags to false (coinductive) *)
 766           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 767             ind_types
 768         in
 769         G.Obj (loc, N.Inductive (params, ind_types))
 770     | IDENT "ncoinductive"; spec = inductive_spec ->
 771         let (params, ind_types) = spec in
 772         let ind_types = (* set inductive flags to false (coinductive) *)
 773           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 774             ind_types
 775         in
 776         G.NObj (loc, N.Inductive (params, ind_types))
 777     | IDENT "coercion" ;
 778       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 779       arity = OPT int ; saturations = OPT int;
 780       composites = OPT (IDENT "nocomposites") ->
 781         let arity = match arity with None -> 0 | Some x -> x in
 782         let saturations = match saturations with None -> 0 | Some x -> x in
 783         let composites = match composites with None -> true | Some _ -> false in
 784         G.Coercion
 785          (loc, t, composites, arity, saturations)
 786     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 787         G.PreferCoercion (loc, t)
 788     | IDENT "pump" ; steps = int ->
 789         G.Pump(loc,steps)
 790     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 791         G.UnificationHint (loc, t, n)
 792     | IDENT "inverter"; name = IDENT; IDENT "for";
 793         indty = tactic_term; paramspec = inverter_param_list ->
 794           G.Inverter
 795             (loc, name, indty, paramspec)
 796             | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 797         G.Obj (loc, N.Record (params,name,ty,fields))
 798     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 799        let uris = List.map UriManager.uri_of_string uris in
 800         G.Default (loc,what,uris)
 801     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 802       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 803                    refl = tactic_term -> refl ] ;
 804       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 805                    sym = tactic_term -> sym ] ;
 806       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 807                    trans = tactic_term -> trans ] ;
 808       "as" ; id = IDENT ->
 809        G.Relation (loc,id,a,aeq,refl,sym,trans)
 810   ]];
 811   lexicon_command: [ [
 812       IDENT "alias" ; spec = alias_spec ->
 813         L.Alias (loc, spec)
 814     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 815         L.Notation (loc, dir, l1, assoc, prec, l2)
 816     | IDENT "interpretation"; id = QSTRING;
 817       (symbol, args, l3) = interpretation ->
 818         L.Interpretation (loc, id, (symbol, args), l3)
 819   ]];
 820   executable: [
 821     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 822     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 823         G.Tactic (loc, Some tac, punct)
 824     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 825     | tac = ntactic; punct = punctuation_tactical ->
 826         G.NTactic (loc, tac, punct)
 827     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 828         G.NTactic (loc, G.NId loc, punct)
 829     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 830         G.NonPunctuationTactical (loc, tac, punct)
 831     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 832     ]
 833   ];
 834   comment: [
 835     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 836        G.Code (loc, ex)
 837     | str = NOTE ->
 838        G.Note (loc, str)
 839     ]
 840   ];
 841   statement: [
 842     [ ex = executable ->
 843        fun ?(never_include=false) ~include_paths status ->
 844           let stm = G.Executable (loc, ex) in
 845           !grafite_callback status stm;
 846           status, LSome stm
 847     | com = comment ->
 848        fun ?(never_include=false) ~include_paths status ->
 849           let stm = G.Comment (loc, com) in
 850           !grafite_callback status stm;
 851           status, LSome stm
 852     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 853        fun ?(never_include=false) ~include_paths status ->
 854           let stm =
 855              G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
 856           in
 857           !grafite_callback status stm;
 858           let _root, buri, fullpath, _rrelpath =
 859             Librarian.baseuri_of_script ~include_paths fname
 860           in
 861           let stm =
 862              G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
 863           in
 864           let status =
 865             if never_include then raise (NoInclusionPerformed fullpath)
 866             else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
 867           in
 868           status, LSome stm
 869     | scom = lexicon_command ; SYMBOL "." ->
 870        fun ?(never_include=false) ~include_paths status ->
 871           !lexicon_callback status scom;
 872           let status = LE.eval_command status scom in
 873           status, LNone loc
 874     | EOI -> raise End_of_file
 875     ]
 876   ];
 877 END
 878 (* }}} *)
 879 ;;
 880
 881 let _ = initialize_parser () ;;
 882
 883 let exc_located_wrapper f =
 884   try
 885     f ()
 886   with
 887   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 888   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 889       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 890   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 891       raise
 892        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 893   | Stdpp.Exc_located (floc, exn) ->
 894       raise
 895        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 896
 897 let parse_statement lexbuf =
 898   exc_located_wrapper
 899     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 900
 901 let statement () = !grafite_parser.statement
 902
 903 let history = ref [] ;;
 904
 905 let push () =
 906   LexiconSync.push ();
 907   history := !grafite_parser :: !history;
 908   grafite_parser := initial_parser ();
 909   initialize_parser ()
 910 ;;
 911
 912 let pop () =
 913   LexiconSync.pop ();
 914   match !history with
 915   | [] -> assert false
 916   | gp :: tail ->
 917       grafite_parser := gp;
 918       history := tail
 919 ;;
 920
 921 (* vim:set foldmethod=marker: *)
 922
 923