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"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 174         GrafiteAst.Destruct (loc, xts)
 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 "symmetry" ->
 250         GrafiteAst.Symmetry loc
 251     | IDENT "transitivity"; t = tactic_term ->
 252         GrafiteAst.Transitivity (loc, t)
 253      (* Produzioni Aggiunte *)
 254     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 255         GrafiteAst.Assume (loc, id, t)
 256     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
 257         GrafiteAst.Suppose (loc, t, id, t1)
 258     | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
 259       cont=by_continuation ->
 260        let t' = match t with LNone _ -> None | LSome t -> Some t in
 261        (match cont with
 262            BYC_done -> GrafiteAst.Bydone (loc, t')
 263          | BYC_weproved (ty,id,t1) ->
 264             GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
 265          | BYC_letsuchthat (id1,t1,id2,t2) ->
 266            (* (match t with
 267                 LNone floc ->
 268                  raise (HExtlib.Localized
 269                   (floc,CicNotationParser.Parse_error
 270                     "tactic_term expected here"))
 271               | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
 272          | BYC_wehaveand (id1,t1,id2,t2) ->
 273             (match t with
 274                 LNone floc ->
 275                  raise (HExtlib.Localized
 276                   (floc,CicNotationParser.Parse_error
 277                     "tactic_term expected here"))
 278               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
 279     | 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']->
 280         GrafiteAst.We_need_to_prove (loc, t, id, t1)
 281     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 282         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
 283     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 284         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
 285     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 286         GrafiteAst.Byinduction(loc, t, id)
 287     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 288         GrafiteAst.Thesisbecomes(loc, t)
 289     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 290         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 291          GrafiteAst.Case(loc,id,params)
 292     | start =
 293        [ IDENT "conclude" -> None
 294        | IDENT "obtain" ; name = IDENT -> Some name ] ;
 295       termine = tactic_term ;
 296       SYMBOL "=" ;
 297       t1=tactic_term ;
 298       IDENT "by" ;
 299       t2 =
 300        [ t=tactic_term -> `Term t
 301        | SYMBOL "_" ; params = auto_params' -> `Auto params
 302        | IDENT "proof" -> `Proof] ;
 303       cont = rewriting_step_continuation ->
 304        GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
 305     | SYMBOL "=" ;
 306       t1=tactic_term ;
 307       IDENT "by" ;
 308       t2=
 309        [ t=tactic_term -> `Term t
 310        | SYMBOL "_" ; params = auto_params' -> `Auto params
 311        | IDENT "proof" -> `Proof] ;
 312       cont=rewriting_step_continuation ->
 313        GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
 314   ]
 315 ];
 316   auto_params: [
 317    [ params =
 318       LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
 319        string_of_int v | v = IDENT -> v ] -> i,v ] ->
 320       params
 321    ]
 322 ];
 323   auto_params': [
 324    [ LPAREN; params = auto_params; RPAREN -> params
 325    | -> []
 326    ]
 327 ];
 328   by_continuation: [
 329     [ 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)
 330     | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 331             IDENT "done" -> BYC_weproved (ty,None,t1)
 332     | IDENT "done" -> BYC_done
 333     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 334       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 335     | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 336               BYC_wehaveand (id1,t1,id2,t2)
 337     ]
 338 ];
 339   rewriting_step_continuation : [
 340     [ IDENT "done" -> true
 341     | -> false
 342     ]
 343 ];
 344   atomic_tactical:
 345     [ "sequence" LEFTA
 346       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 347           let ts =
 348             match t1 with
 349             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 350             | _ -> [ t1; t2 ]
 351           in
 352           GrafiteAst.Seq (loc, ts)
 353       ]
 354     | "then" NONA
 355       [ tac = SELF; SYMBOL ";";
 356         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 357           (GrafiteAst.Then (loc, tac, tacs))
 358       ]
 359     | "loops" RIGHTA
 360       [ IDENT "do"; count = int; tac = SELF ->
 361           GrafiteAst.Do (loc, count, tac)
 362       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 363       ]
 364     | "simple" NONA
 365       [ IDENT "first";
 366         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 367           GrafiteAst.First (loc, tacs)
 368       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 369       | IDENT "solve";
 370         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 371           GrafiteAst.Solve (loc, tacs)
 372       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 373       | LPAREN; tac = SELF; RPAREN -> tac
 374       | tac = tactic -> tac
 375       ]
 376     ];
 377   punctuation_tactical:
 378     [
 379       [ SYMBOL "[" -> GrafiteAst.Branch loc
 380       | SYMBOL "|" -> GrafiteAst.Shift loc
 381       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 382       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 383       | SYMBOL "]" -> GrafiteAst.Merge loc
 384       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 385       | SYMBOL "." -> GrafiteAst.Dot loc
 386       ]
 387     ];
 388   non_punctuation_tactical:
 389     [ "simple" NONA
 390       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 391       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 392       | IDENT "skip" -> GrafiteAst.Skip loc
 393       ]
 394     ];
 395   theorem_flavour: [
 396     [ [ IDENT "definition"  ] -> `Definition
 397     | [ IDENT "fact"        ] -> `Fact
 398     | [ IDENT "lemma"       ] -> `Lemma
 399     | [ IDENT "remark"      ] -> `Remark
 400     | [ IDENT "theorem"     ] -> `Theorem
 401     ]
 402   ];
 403   inductive_spec: [ [
 404     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
 405     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 406     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 407     tl = OPT [ "with";
 408       types = LIST1 [
 409         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 410        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 411           (name, true, typ, constructors) ] SEP "with" -> types
 412     ] ->
 413       let params =
 414         List.fold_right
 415           (fun (names, typ) acc ->
 416             (List.map (fun name -> (name, typ)) names) @ acc)
 417           params []
 418       in
 419       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 420       let tl_ind_types = match tl with None -> [] | Some types -> types in
 421       let ind_types = fst_ind_type :: tl_ind_types in
 422       (params, ind_types)
 423   ] ];
 424
 425   record_spec: [ [
 426     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
 427      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 428      fields = LIST0 [
 429        name = IDENT ;
 430        coercion = [
 431            SYMBOL ":" -> false,0
 432          | SYMBOL ":"; SYMBOL ">" -> true,0
 433          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 434        ];
 435        ty = term ->
 436          let b,n = coercion in
 437          (name,ty,b,n)
 438      ] SEP SYMBOL ";"; SYMBOL "}" ->
 439       let params =
 440         List.fold_right
 441           (fun (names, typ) acc ->
 442             (List.map (fun name -> (name, typ)) names) @ acc)
 443           params []
 444       in
 445       (params,name,typ,fields)
 446   ] ];
 447
 448   macro: [
 449     [ [ IDENT "check"   ]; t = term ->
 450         GrafiteAst.Check (loc, t)
 451     | [ IDENT "inline"];
 452         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 453         suri = QSTRING; prefix = OPT QSTRING ->
 454          let style = match style with
 455             | None       -> GrafiteAst.Declarative
 456             | Some depth -> GrafiteAst.Procedural depth
 457          in
 458          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 459          GrafiteAst.Inline (loc,style,suri,prefix)
 460     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 461          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 462     | IDENT "auto"; params = auto_params ->
 463         GrafiteAst.AutoInteractive (loc,params)
 464     | [ IDENT "whelp"; "match" ] ; t = term ->
 465         GrafiteAst.WMatch (loc,t)
 466     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 467         GrafiteAst.WInstance (loc,t)
 468     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 469         GrafiteAst.WLocate (loc,id)
 470     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 471         GrafiteAst.WElim (loc, t)
 472     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 473         GrafiteAst.WHint (loc,t)
 474     ]
 475   ];
 476   alias_spec: [
 477     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 478       let alpha = "[a-zA-Z]" in
 479       let num = "[0-9]+" in
 480       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 481       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 482       let rex = Str.regexp ("^"^ident^"$") in
 483       if Str.string_match rex id 0 then
 484         if (try ignore (UriManager.uri_of_string uri); true
 485             with UriManager.IllFormedUri _ -> false)
 486         then
 487           LexiconAst.Ident_alias (id, uri)
 488         else
 489           raise
 490            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 491       else
 492         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 493           Printf.sprintf "Not a valid identifier: %s" id)))
 494     | IDENT "symbol"; symbol = QSTRING;
 495       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 496       SYMBOL "="; dsc = QSTRING ->
 497         let instance =
 498           match instance with Some i -> i | None -> 0
 499         in
 500         LexiconAst.Symbol_alias (symbol, instance, dsc)
 501     | IDENT "num";
 502       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 503       SYMBOL "="; dsc = QSTRING ->
 504         let instance =
 505           match instance with Some i -> i | None -> 0
 506         in
 507         LexiconAst.Number_alias (instance, dsc)
 508     ]
 509   ];
 510   argument: [
 511     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 512       id = IDENT ->
 513         Ast.IdentArg (List.length l, id)
 514     ]
 515   ];
 516   associativity: [
 517     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 518     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 519     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 520     ]
 521   ];
 522   precedence: [
 523     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 524   ];
 525   notation: [
 526     [ dir = OPT direction; s = QSTRING;
 527       assoc = OPT associativity; prec = OPT precedence;
 528       IDENT "for";
 529       p2 =
 530         [ blob = UNPARSED_AST ->
 531             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 532               (CicNotationParser.parse_level2_ast
 533                 (Ulexing.from_utf8_string blob))
 534         | blob = UNPARSED_META ->
 535             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 536               (CicNotationParser.parse_level2_meta
 537                 (Ulexing.from_utf8_string blob))
 538         ] ->
 539           let assoc =
 540             match assoc with
 541             | None -> default_associativity
 542             | Some assoc -> assoc
 543           in
 544           let prec =
 545             match prec with
 546             | None -> default_precedence
 547             | Some prec -> prec
 548           in
 549           let p1 =
 550             add_raw_attribute ~text:s
 551               (CicNotationParser.parse_level1_pattern
 552                 (Ulexing.from_utf8_string s))
 553           in
 554           (dir, p1, assoc, prec, p2)
 555     ]
 556   ];
 557   level3_term: [
 558     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 559     | id = IDENT -> Ast.VarPattern id
 560     | SYMBOL "_" -> Ast.ImplicitPattern
 561     | LPAREN; terms = LIST1 SELF; RPAREN ->
 562         (match terms with
 563         | [] -> assert false
 564         | [term] -> term
 565         | terms -> Ast.ApplPattern terms)
 566     ]
 567   ];
 568   interpretation: [
 569     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 570         (s, args, t)
 571     ]
 572   ];
 573
 574   include_command: [ [
 575       IDENT "include" ; path = QSTRING ->
 576         loc,path,LexiconAst.WithPreferences
 577     | IDENT "include'" ; path = QSTRING ->
 578         loc,path,LexiconAst.WithoutPreferences
 579    ]];
 580
 581   grafite_command: [ [
 582       IDENT "set"; n = QSTRING; v = QSTRING ->
 583         GrafiteAst.Set (loc, n, v)
 584     | IDENT "drop" -> GrafiteAst.Drop loc
 585     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 586     | IDENT "qed" -> GrafiteAst.Qed loc
 587     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 588       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 589         GrafiteAst.Obj (loc,
 590           Ast.Theorem
 591             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 592     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 593       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 594         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 595     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 596       body = term ->
 597         GrafiteAst.Obj (loc,
 598           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 599     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 600         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 601     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 602         defs = CicNotationParser.let_defs ->
 603          (* In case of mutual definitions here we produce just
 604             the syntax tree for the first one. The others will be
 605             generated from the completely specified term just before
 606             insertion in the environment. We use the flavour
 607             `MutualDefinition to rememer this. *)
 608           let name,ty =
 609             match defs with
 610             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
 611                 let ty =
 612                  List.fold_right
 613                   (fun var ty -> Ast.Binder (`Pi,var,ty)
 614                   ) params ty
 615                 in
 616                  name,ty
 617             | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
 618                 name, Ast.Implicit
 619             | _ -> assert false
 620           in
 621           let body = Ast.Ident (name,None) in
 622           let flavour =
 623            if List.length defs = 1 then
 624             `Definition
 625            else
 626             `MutualDefinition
 627           in
 628            GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
 629              Some (Ast.LetRec (ind_kind, defs, body))))
 630     | IDENT "inductive"; spec = inductive_spec ->
 631         let (params, ind_types) = spec in
 632         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 633     | IDENT "coinductive"; spec = inductive_spec ->
 634         let (params, ind_types) = spec in
 635         let ind_types = (* set inductive flags to false (coinductive) *)
 636           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 637             ind_types
 638         in
 639         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 640     | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
 641         let arity = match arity with None -> 0 | Some x -> x in
 642         let saturations = match saturations with None -> 0 | Some x -> x in
 643         GrafiteAst.Coercion
 644          (loc, UriManager.uri_of_string suri, true, arity, saturations)
 645     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 646         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 647     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 648        let uris = List.map UriManager.uri_of_string uris in
 649         GrafiteAst.Default (loc,what,uris)
 650     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 651       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 652                    refl = tactic_term -> refl ] ;
 653       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 654                    sym = tactic_term -> sym ] ;
 655       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 656                    trans = tactic_term -> trans ] ;
 657       "as" ; id = IDENT ->
 658        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 659   ]];
 660   lexicon_command: [ [
 661       IDENT "alias" ; spec = alias_spec ->
 662         LexiconAst.Alias (loc, spec)
 663     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 664         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 665     | IDENT "interpretation"; id = QSTRING;
 666       (symbol, args, l3) = interpretation ->
 667         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 668   ]];
 669   executable: [
 670     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 671     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 672         GrafiteAst.Tactic (loc, Some tac, punct)
 673     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 674     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 675         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 676     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 677     ]
 678   ];
 679   comment: [
 680     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 681        GrafiteAst.Code (loc, ex)
 682     | str = NOTE ->
 683        GrafiteAst.Note (loc, str)
 684     ]
 685   ];
 686   statement: [
 687     [ ex = executable ->
 688        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 689     | com = comment ->
 690        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 691     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 692        fun ~include_paths status ->
 693         let buri, fullpath =
 694           DependenciesParser.baseuri_of_script ~include_paths fname
 695         in
 696         let status =
 697          LexiconEngine.eval_command status
 698            (LexiconAst.Include (iloc,buri,mode,fullpath))
 699         in
 700          !out fname;
 701          status,
 702           LSome
 703           (GrafiteAst.Executable
 704            (loc,GrafiteAst.Command
 705             (loc,GrafiteAst.Include (iloc,buri))))
 706     | scom = lexicon_command ; SYMBOL "." ->
 707        fun ~include_paths status ->
 708         let status = LexiconEngine.eval_command status scom in
 709          status,LNone loc
 710     | EOI -> raise End_of_file
 711     ]
 712   ];
 713 END
 714
 715 let exc_located_wrapper f =
 716   try
 717     f ()
 718   with
 719   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 720   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 721       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 722   | Stdpp.Exc_located (floc, exn) ->
 723       raise
 724        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 725
 726 let parse_statement lexbuf =
 727   exc_located_wrapper
 728     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))