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