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