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