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