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 type 'a localized_option =
  34    LSome of 'a
  35  | LNone of GrafiteAst.loc
  36
  37 type ast_statement =
  38   (CicNotationPt.term, CicNotationPt.term,
  39    CicNotationPt.term GrafiteAst.reduction,
  40    CicNotationPt.term CicNotationPt.obj, string)
  41     GrafiteAst.statement
  42
  43 type statement =
  44   include_paths:string list ->
  45   LexiconEngine.status ->
  46     LexiconEngine.status * ast_statement localized_option
  47
  48 let grammar = CicNotationParser.level2_ast_grammar
  49
  50 let term = CicNotationParser.term
  51 let statement = Grammar.Entry.create grammar "statement"
  52
  53 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
  54
  55 let default_precedence = 50
  56 let default_associativity = Gramext.NonA
  57
  58 type by_continuation =
  59    BYC_done
  60  | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
  61  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  62  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
  63
  64 EXTEND
  65   GLOBAL: term statement;
  66   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  67   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
  68   new_name: [
  69     [ id = IDENT -> Some id
  70     | SYMBOL "_" -> None ]
  71     ];
  72   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
  73   tactic_term_list1: [
  74     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
  75   ];
  76   reduction_kind: [
  77     [ IDENT "normalize" -> `Normalize
  78     | IDENT "reduce" -> `Reduce
  79     | IDENT "simplify" -> `Simpl
  80     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
  81     | IDENT "whd" -> `Whd ]
  82   ];
  83   sequent_pattern_spec: [
  84    [ hyp_paths =
  85       LIST0
  86        [ id = IDENT ;
  87          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
  88          (id,match path with Some p -> p | None -> Ast.UserInput) ];
  89      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
  90       let goal_path =
  91        match goal_path, hyp_paths with
  92           None, [] -> Some Ast.UserInput
  93         | None, _::_ -> None
  94         | Some goal_path, _ -> Some goal_path
  95       in
  96        hyp_paths,goal_path
  97    ]
  98   ];
  99   pattern_spec: [
 100     [ res = OPT [
 101        "in";
 102        wanted_and_sps =
 103         [ "match" ; wanted = tactic_term ;
 104           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 105            Some wanted,sps
 106         | sps = sequent_pattern_spec ->
 107            None,Some sps
 108         ] ->
 109          let wanted,hyp_paths,goal_path =
 110           match wanted_and_sps with
 111              wanted,None -> wanted, [], Some Ast.UserInput
 112            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 113          in
 114           wanted, hyp_paths, goal_path ] ->
 115       match res with
 116          None -> None,[],Some Ast.UserInput
 117        | Some ps -> ps]
 118   ];
 119   direction: [
 120     [ SYMBOL ">" -> `LeftToRight
 121     | SYMBOL "<" -> `RightToLeft ]
 122   ];
 123   int: [ [ num = NUMBER -> int_of_string num ] ];
 124   intros_names: [
 125    [ idents = OPT ident_list0 ->
 126       match idents with None -> [] | Some idents -> idents
 127    ]
 128   ];
 129   intros_spec: [
 130     [ OPT [ IDENT "names" ];
 131       num = OPT [ num = int -> num ];
 132       idents = intros_names ->
 133         num, idents
 134     ]
 135   ];
 136   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 137   tactic: [
 138     [ IDENT "absurd"; t = tactic_term ->
 139         GrafiteAst.Absurd (loc, t)
 140     | IDENT "apply"; t = tactic_term ->
 141         GrafiteAst.Apply (loc, t)
 142     | IDENT "applyS"; t = tactic_term ; params =
 143         LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
 144           string_of_int v | v = IDENT -> v ] -> i,v ] ->
 145         GrafiteAst.ApplyS (loc, t, params)
 146     | IDENT "assumption" ->
 147         GrafiteAst.Assumption loc
 148     | IDENT "autobatch";  params = auto_params ->
 149         GrafiteAst.AutoBatch (loc,params)
 150     | IDENT "cases"; what = tactic_term;
 151       specs = intros_spec ->
 152         GrafiteAst.Cases (loc, what, specs)
 153     | IDENT "clear"; ids = LIST1 IDENT ->
 154         GrafiteAst.Clear (loc, ids)
 155     | IDENT "clearbody"; id = IDENT ->
 156         GrafiteAst.ClearBody (loc,id)
 157     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 158         GrafiteAst.Change (loc, what, t)
 159     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 160       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 161         let times = match times with None -> 1 | Some i -> i in
 162         GrafiteAst.Compose (loc, t1, t2, times, specs)
 163     | IDENT "constructor"; n = int ->
 164         GrafiteAst.Constructor (loc, n)
 165     | IDENT "contradiction" ->
 166         GrafiteAst.Contradiction loc
 167     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 168         GrafiteAst.Cut (loc, ident, t)
 169     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 170         let idents = match idents with None -> [] | Some idents -> idents in
 171         GrafiteAst.Decompose (loc, idents)
 172     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
 173     | IDENT "destruct"; t = tactic_term ->
 174         GrafiteAst.Destruct (loc, t)
 175     | IDENT "elim"; what = tactic_term; using = using;
 176        pattern = OPT pattern_spec;
 177        (num, idents) = intros_spec ->
 178         let pattern = match pattern with
 179            | None         -> None, [], Some Ast.UserInput
 180            | Some pattern -> pattern
 181         in
 182         GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
 183     | IDENT "elimType"; what = tactic_term; using = using;
 184       (num, idents) = intros_spec ->
 185         GrafiteAst.ElimType (loc, what, using, (num, idents))
 186     | IDENT "exact"; t = tactic_term ->
 187         GrafiteAst.Exact (loc, t)
 188     | IDENT "exists" ->
 189         GrafiteAst.Exists loc
 190     | IDENT "fail" -> GrafiteAst.Fail loc
 191     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 192         let (pt,_,_) = p in
 193           if pt <> None then
 194             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 195               ("the pattern cannot specify the term to replace, only its"
 196               ^ " paths in the hypotheses and in the conclusion")))
 197         else
 198          GrafiteAst.Fold (loc, kind, t, p)
 199     | IDENT "fourier" ->
 200         GrafiteAst.Fourier loc
 201     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 202         let idents = match idents with None -> [] | Some idents -> idents in
 203         GrafiteAst.FwdSimpl (loc, hyp, idents)
 204     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 205        GrafiteAst.Generalize (loc,p,id)
 206     | IDENT "id" -> GrafiteAst.IdTac loc
 207     | IDENT "intro"; ident = OPT IDENT ->
 208         let idents = match ident with None -> [] | Some id -> [Some id] in
 209         GrafiteAst.Intros (loc, (Some 1, idents))
 210     | IDENT "intros"; specs = intros_spec ->
 211         GrafiteAst.Intros (loc, specs)
 212     | IDENT "inversion"; t = tactic_term ->
 213         GrafiteAst.Inversion (loc, t)
 214     | IDENT "lapply";
 215       linear = OPT [ IDENT "linear" ];
 216       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 217       what = tactic_term;
 218       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 219       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 220         let linear = match linear with None -> false | Some _ -> true in
 221         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 222         GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
 223     | IDENT "left" -> GrafiteAst.Left loc
 224     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 225         GrafiteAst.LetIn (loc, t, where)
 226     | kind = reduction_kind; p = pattern_spec ->
 227         GrafiteAst.Reduce (loc, kind, p)
 228     | IDENT "reflexivity" ->
 229         GrafiteAst.Reflexivity loc
 230     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 231         GrafiteAst.Replace (loc, p, t)
 232     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 233        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 234        let (pt,_,_) = p in
 235         if pt <> None then
 236          raise
 237           (HExtlib.Localized (loc,
 238            (CicNotationParser.Parse_error
 239             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 240         else
 241          let n = match xnames with None -> [] | Some names -> names in
 242          GrafiteAst.Rewrite (loc, d, t, p, n)
 243     | IDENT "right" ->
 244         GrafiteAst.Right loc
 245     | IDENT "ring" ->
 246         GrafiteAst.Ring loc
 247     | IDENT "split" ->
 248         GrafiteAst.Split loc
 249     | IDENT "subst" ->
 250         GrafiteAst.Subst loc
 251     | IDENT "symmetry" ->
 252         GrafiteAst.Symmetry loc
 253     | IDENT "transitivity"; t = tactic_term ->
 254         GrafiteAst.Transitivity (loc, t)
 255      (* Produzioni Aggiunte *)
 256     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 257         GrafiteAst.Assume (loc, id, t)
 258     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
 259         GrafiteAst.Suppose (loc, t, id, t1)
 260     | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
 261       cont=by_continuation ->
 262        let t' = match t with LNone _ -> None | LSome t -> Some t in
 263        (match cont with
 264            BYC_done -> GrafiteAst.Bydone (loc, t')
 265          | BYC_weproved (ty,id,t1) ->
 266             GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
 267          | BYC_letsuchthat (id1,t1,id2,t2) ->
 268            (* (match t with
 269                 LNone floc ->
 270                  raise (HExtlib.Localized
 271                   (floc,CicNotationParser.Parse_error
 272                     "tactic_term expected here"))
 273               | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
 274          | BYC_wehaveand (id1,t1,id2,t2) ->
 275             (match t with
 276                 LNone floc ->
 277                  raise (HExtlib.Localized
 278                   (floc,CicNotationParser.Parse_error
 279                     "tactic_term expected here"))
 280               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
 281     | 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']->
 282         GrafiteAst.We_need_to_prove (loc, t, id, t1)
 283     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 284         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
 285     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 286         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
 287     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 288         GrafiteAst.Byinduction(loc, t, id)
 289     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 290         GrafiteAst.Thesisbecomes(loc, t)
 291     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 292         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 293          GrafiteAst.Case(loc,id,params)
 294     | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params  ] ; cont=rewriting_step_continuation ->
 295      GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
 296     | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
 297       cont=rewriting_step_continuation  ->
 298      GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
 299   ]
 300 ];
 301   auto_params: [
 302    [ params =
 303       LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
 304        string_of_int v | v = IDENT -> v ] -> i,v ] ->
 305       params
 306    ]
 307 ];
 308   auto_params': [
 309    [ LPAREN; params = auto_params; RPAREN -> params
 310    | -> []
 311    ]
 312 ];
 313   by_continuation: [
 314     [ IDENT "we" ; IDENT "proved" ; 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)
 315     | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 316             IDENT "done" -> BYC_weproved (ty,None,t1)
 317     | IDENT "done" -> BYC_done
 318     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 319       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 320     | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 321               BYC_wehaveand (id1,t1,id2,t2)
 322     ]
 323 ];
 324   rewriting_step_continuation : [
 325     [ IDENT "done" -> true
 326     | -> false
 327     ]
 328 ];
 329   atomic_tactical:
 330     [ "sequence" LEFTA
 331       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 332           let ts =
 333             match t1 with
 334             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 335             | _ -> [ t1; t2 ]
 336           in
 337           GrafiteAst.Seq (loc, ts)
 338       ]
 339     | "then" NONA
 340       [ tac = SELF; SYMBOL ";";
 341         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 342           (GrafiteAst.Then (loc, tac, tacs))
 343       ]
 344     | "loops" RIGHTA
 345       [ IDENT "do"; count = int; tac = SELF ->
 346           GrafiteAst.Do (loc, count, tac)
 347       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 348       ]
 349     | "simple" NONA
 350       [ IDENT "first";
 351         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 352           GrafiteAst.First (loc, tacs)
 353       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 354       | IDENT "solve";
 355         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 356           GrafiteAst.Solve (loc, tacs)
 357       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 358       | LPAREN; tac = SELF; RPAREN -> tac
 359       | tac = tactic -> tac
 360       ]
 361     ];
 362   punctuation_tactical:
 363     [
 364       [ SYMBOL "[" -> GrafiteAst.Branch loc
 365       | SYMBOL "|" -> GrafiteAst.Shift loc
 366       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 367       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 368       | SYMBOL "]" -> GrafiteAst.Merge loc
 369       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 370       | SYMBOL "." -> GrafiteAst.Dot loc
 371       ]
 372     ];
 373   non_punctuation_tactical:
 374     [ "simple" NONA
 375       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 376       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 377       | IDENT "skip" -> GrafiteAst.Skip loc
 378       ]
 379     ];
 380   theorem_flavour: [
 381     [ [ IDENT "definition"  ] -> `Definition
 382     | [ IDENT "fact"        ] -> `Fact
 383     | [ IDENT "lemma"       ] -> `Lemma
 384     | [ IDENT "remark"      ] -> `Remark
 385     | [ IDENT "theorem"     ] -> `Theorem
 386     ]
 387   ];
 388   inductive_spec: [ [
 389     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
 390     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 391     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 392     tl = OPT [ "with";
 393       types = LIST1 [
 394         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 395        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 396           (name, true, typ, constructors) ] SEP "with" -> types
 397     ] ->
 398       let params =
 399         List.fold_right
 400           (fun (names, typ) acc ->
 401             (List.map (fun name -> (name, typ)) names) @ acc)
 402           params []
 403       in
 404       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 405       let tl_ind_types = match tl with None -> [] | Some types -> types in
 406       let ind_types = fst_ind_type :: tl_ind_types in
 407       (params, ind_types)
 408   ] ];
 409
 410   record_spec: [ [
 411     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
 412      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 413      fields = LIST0 [
 414        name = IDENT ;
 415        coercion = [
 416            SYMBOL ":" -> false,0
 417          | SYMBOL ":"; SYMBOL ">" -> true,0
 418          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 419        ];
 420        ty = term ->
 421          let b,n = coercion in
 422          (name,ty,b,n)
 423      ] SEP SYMBOL ";"; SYMBOL "}" ->
 424       let params =
 425         List.fold_right
 426           (fun (names, typ) acc ->
 427             (List.map (fun name -> (name, typ)) names) @ acc)
 428           params []
 429       in
 430       (params,name,typ,fields)
 431   ] ];
 432
 433   macro: [
 434     [ [ IDENT "check"   ]; t = term ->
 435         GrafiteAst.Check (loc, t)
 436     | [ IDENT "inline"];
 437         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 438         suri = QSTRING; prefix = OPT QSTRING ->
 439          let style = match style with
 440             | None       -> GrafiteAst.Declarative
 441             | Some depth -> GrafiteAst.Procedural depth
 442          in
 443          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 444          GrafiteAst.Inline (loc,style,suri,prefix)
 445     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
 446     | IDENT "auto"; params = auto_params ->
 447         GrafiteAst.AutoInteractive (loc,params)
 448     | [ IDENT "whelp"; "match" ] ; t = term ->
 449         GrafiteAst.WMatch (loc,t)
 450     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 451         GrafiteAst.WInstance (loc,t)
 452     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 453         GrafiteAst.WLocate (loc,id)
 454     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 455         GrafiteAst.WElim (loc, t)
 456     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 457         GrafiteAst.WHint (loc,t)
 458     ]
 459   ];
 460   alias_spec: [
 461     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 462       let alpha = "[a-zA-Z]" in
 463       let num = "[0-9]+" in
 464       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 465       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 466       let rex = Str.regexp ("^"^ident^"$") in
 467       if Str.string_match rex id 0 then
 468         if (try ignore (UriManager.uri_of_string uri); true
 469             with UriManager.IllFormedUri _ -> false)
 470         then
 471           LexiconAst.Ident_alias (id, uri)
 472         else
 473           raise
 474            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 475       else
 476         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 477           Printf.sprintf "Not a valid identifier: %s" id)))
 478     | IDENT "symbol"; symbol = QSTRING;
 479       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 480       SYMBOL "="; dsc = QSTRING ->
 481         let instance =
 482           match instance with Some i -> i | None -> 0
 483         in
 484         LexiconAst.Symbol_alias (symbol, instance, dsc)
 485     | IDENT "num";
 486       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 487       SYMBOL "="; dsc = QSTRING ->
 488         let instance =
 489           match instance with Some i -> i | None -> 0
 490         in
 491         LexiconAst.Number_alias (instance, dsc)
 492     ]
 493   ];
 494   argument: [
 495     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 496       id = IDENT ->
 497         Ast.IdentArg (List.length l, id)
 498     ]
 499   ];
 500   associativity: [
 501     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 502     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 503     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 504     ]
 505   ];
 506   precedence: [
 507     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 508   ];
 509   notation: [
 510     [ dir = OPT direction; s = QSTRING;
 511       assoc = OPT associativity; prec = OPT precedence;
 512       IDENT "for";
 513       p2 =
 514         [ blob = UNPARSED_AST ->
 515             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 516               (CicNotationParser.parse_level2_ast
 517                 (Ulexing.from_utf8_string blob))
 518         | blob = UNPARSED_META ->
 519             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 520               (CicNotationParser.parse_level2_meta
 521                 (Ulexing.from_utf8_string blob))
 522         ] ->
 523           let assoc =
 524             match assoc with
 525             | None -> default_associativity
 526             | Some assoc -> assoc
 527           in
 528           let prec =
 529             match prec with
 530             | None -> default_precedence
 531             | Some prec -> prec
 532           in
 533           let p1 =
 534             add_raw_attribute ~text:s
 535               (CicNotationParser.parse_level1_pattern
 536                 (Ulexing.from_utf8_string s))
 537           in
 538           (dir, p1, assoc, prec, p2)
 539     ]
 540   ];
 541   level3_term: [
 542     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 543     | id = IDENT -> Ast.VarPattern id
 544     | SYMBOL "_" -> Ast.ImplicitPattern
 545     | LPAREN; terms = LIST1 SELF; RPAREN ->
 546         (match terms with
 547         | [] -> assert false
 548         | [term] -> term
 549         | terms -> Ast.ApplPattern terms)
 550     ]
 551   ];
 552   interpretation: [
 553     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 554         (s, args, t)
 555     ]
 556   ];
 557
 558   include_command: [ [
 559       IDENT "include" ; path = QSTRING ->
 560         loc,path,LexiconAst.WithPreferences
 561     | IDENT "include'" ; path = QSTRING ->
 562         loc,path,LexiconAst.WithoutPreferences
 563    ]];
 564
 565   grafite_command: [ [
 566       IDENT "set"; n = QSTRING; v = QSTRING ->
 567         GrafiteAst.Set (loc, n, v)
 568     | IDENT "drop" -> GrafiteAst.Drop loc
 569     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 570     | IDENT "qed" -> GrafiteAst.Qed loc
 571     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 572       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 573         GrafiteAst.Obj (loc,
 574           Ast.Theorem
 575             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 576     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 577       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 578         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 579     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 580       body = term ->
 581         GrafiteAst.Obj (loc,
 582           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 583     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 584         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 585     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 586         defs = CicNotationParser.let_defs ->
 587          (* In case of mutual definitions here we produce just
 588             the syntax tree for the first one. The others will be
 589             generated from the completely specified term just before
 590             insertion in the environment. We use the flavour
 591             `MutualDefinition to rememer this. *)
 592           let name,ty =
 593             match defs with
 594             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
 595                 let ty =
 596                  List.fold_right
 597                   (fun var ty -> Ast.Binder (`Pi,var,ty)
 598                   ) params ty
 599                 in
 600                  name,ty
 601             | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
 602                 name, Ast.Implicit
 603             | _ -> assert false
 604           in
 605           let body = Ast.Ident (name,None) in
 606           let flavour =
 607            if List.length defs = 1 then
 608             `Definition
 609            else
 610             `MutualDefinition
 611           in
 612            GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
 613              Some (Ast.LetRec (ind_kind, defs, body))))
 614     | IDENT "inductive"; spec = inductive_spec ->
 615         let (params, ind_types) = spec in
 616         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 617     | IDENT "coinductive"; spec = inductive_spec ->
 618         let (params, ind_types) = spec in
 619         let ind_types = (* set inductive flags to false (coinductive) *)
 620           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 621             ind_types
 622         in
 623         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 624     | IDENT "coercion" ; suri = URI ; arity = OPT int ->
 625         let arity = match arity with None -> 0 | Some x -> x in
 626         GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
 627     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 628         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 629     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 630        let uris = List.map UriManager.uri_of_string uris in
 631         GrafiteAst.Default (loc,what,uris)
 632     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 633       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 634                    refl = tactic_term -> refl ] ;
 635       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 636                    sym = tactic_term -> sym ] ;
 637       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 638                    trans = tactic_term -> trans ] ;
 639       "as" ; id = IDENT ->
 640        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 641   ]];
 642   lexicon_command: [ [
 643       IDENT "alias" ; spec = alias_spec ->
 644         LexiconAst.Alias (loc, spec)
 645     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 646         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 647     | IDENT "interpretation"; id = QSTRING;
 648       (symbol, args, l3) = interpretation ->
 649         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 650   ]];
 651   executable: [
 652     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 653     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 654         GrafiteAst.Tactic (loc, Some tac, punct)
 655     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 656     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 657         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 658     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 659     ]
 660   ];
 661   comment: [
 662     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 663        GrafiteAst.Code (loc, ex)
 664     | str = NOTE ->
 665        GrafiteAst.Note (loc, str)
 666     ]
 667   ];
 668   statement: [
 669     [ ex = executable ->
 670        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 671     | com = comment ->
 672        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 673     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 674        fun ~include_paths status ->
 675         let buri, fullpath =
 676           DependenciesParser.baseuri_of_script ~include_paths fname
 677         in
 678         let status =
 679          LexiconEngine.eval_command status
 680            (LexiconAst.Include (iloc,buri,mode,fullpath))
 681         in
 682          !out fname;
 683          status,
 684           LSome
 685           (GrafiteAst.Executable
 686            (loc,GrafiteAst.Command
 687             (loc,GrafiteAst.Include (iloc,buri))))
 688     | scom = lexicon_command ; SYMBOL "." ->
 689        fun ~include_paths status ->
 690         let status = LexiconEngine.eval_command status scom in
 691          status,LNone loc
 692     | EOI -> raise End_of_file
 693     ]
 694   ];
 695 END
 696
 697 let exc_located_wrapper f =
 698   try
 699     f ()
 700   with
 701   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 702   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 703       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 704   | Stdpp.Exc_located (floc, exn) ->
 705       raise
 706        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 707
 708 let parse_statement lexbuf =
 709   exc_located_wrapper
 710     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))