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