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