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