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