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