components/grafite_parser/grafiteParser.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 let out = ref ignore
  29 let set_callback f = out := f
  30
  31 module Ast = CicNotationPt
  32
  33 exception NoInclusionPerformed of string (* full path *)
  34
  35 type 'a localized_option =
  36    LSome of 'a
  37  | LNone of GrafiteAst.loc
  38
  39 type ast_statement =
  40   (CicNotationPt.term, CicNotationPt.term,
  41    CicNotationPt.term GrafiteAst.reduction,
  42    CicNotationPt.term CicNotationPt.obj, string)
  43     GrafiteAst.statement
  44
  45 type statement =
  46   ?never_include:bool ->
  47   include_paths:string list ->
  48   LexiconEngine.status ->
  49     LexiconEngine.status * ast_statement localized_option
  50
  51 let grammar = CicNotationParser.level2_ast_grammar
  52
  53 let term = CicNotationParser.term
  54 let statement = Grammar.Entry.create grammar "statement"
  55
  56 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
  57
  58 let default_precedence = 50
  59 let default_associativity = Gramext.NonA
  60
  61 type by_continuation =
  62    BYC_done
  63  | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
  64  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  65  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
  66
  67 EXTEND
  68   GLOBAL: term statement;
  69   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  70   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
  71   new_name: [
  72     [ id = IDENT -> Some id
  73     | SYMBOL "_" -> None ]
  74     ];
  75   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
  76   tactic_term_list1: [
  77     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
  78   ];
  79   reduction_kind: [
  80     [ IDENT "normalize" -> `Normalize
  81     | IDENT "simplify" -> `Simpl
  82     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
  83     | IDENT "whd" -> `Whd ]
  84   ];
  85   sequent_pattern_spec: [
  86    [ hyp_paths =
  87       LIST0
  88        [ id = IDENT ;
  89          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
  90          (id,match path with Some p -> p | None -> Ast.UserInput) ];
  91      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
  92       let goal_path =
  93        match goal_path, hyp_paths with
  94           None, [] -> Some Ast.UserInput
  95         | None, _::_ -> None
  96         | Some goal_path, _ -> Some goal_path
  97       in
  98        hyp_paths,goal_path
  99    ]
 100   ];
 101   pattern_spec: [
 102     [ res = OPT [
 103        "in";
 104        wanted_and_sps =
 105         [ "match" ; wanted = tactic_term ;
 106           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 107            Some wanted,sps
 108         | sps = sequent_pattern_spec ->
 109            None,Some sps
 110         ] ->
 111          let wanted,hyp_paths,goal_path =
 112           match wanted_and_sps with
 113              wanted,None -> wanted, [], Some Ast.UserInput
 114            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 115          in
 116           wanted, hyp_paths, goal_path ] ->
 117       match res with
 118          None -> None,[],Some Ast.UserInput
 119        | Some ps -> ps]
 120   ];
 121   direction: [
 122     [ SYMBOL ">" -> `LeftToRight
 123     | SYMBOL "<" -> `RightToLeft ]
 124   ];
 125   int: [ [ num = NUMBER -> int_of_string num ] ];
 126   intros_names: [
 127    [ idents = OPT ident_list0 ->
 128       match idents with None -> [] | Some idents -> idents
 129    ]
 130   ];
 131   intros_spec: [
 132     [ OPT [ IDENT "names" ];
 133       num = OPT [ num = int -> num ];
 134       idents = intros_names ->
 135         num, idents
 136     ]
 137   ];
 138   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 139   tactic: [
 140     [ IDENT "absurd"; t = tactic_term ->
 141         GrafiteAst.Absurd (loc, t)
 142     | IDENT "apply"; t = tactic_term ->
 143         GrafiteAst.Apply (loc, t)
 144     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 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"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
 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     | "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" ; "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" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 284         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
 285     | "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 = OPT [
 293        start =
 294         [ IDENT "conclude" -> None
 295         | IDENT "obtain" ; name = IDENT -> Some name ] ;
 296        termine = tactic_term -> start, termine];
 297       SYMBOL "=" ;
 298       t1=tactic_term ;
 299       t2 =
 300        [ IDENT "exact"; t=tactic_term -> `Term t
 301        | IDENT "using"; term=tactic_term -> `SolveWith term
 302        | IDENT "proof" -> `Proof
 303        | params = auto_params -> `Auto params];
 304       cont = rewriting_step_continuation ->
 305        GrafiteAst.RewritingStep(loc, start, t1, t2, cont)
 306   ]
 307 ];
 308   auto_params: [
 309    [ params =
 310       LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
 311               string_of_int v | v = IDENT -> v ] -> i,v ];
 312       tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] ->
 313       (match tl with Some l -> l | None -> []),
 314       params
 315    ]
 316 ];
 317   by_continuation: [
 318     [ 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)
 319     | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 320             "done" -> BYC_weproved (ty,None,t1)
 321     | "done" -> BYC_done
 322     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 323       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 324     | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 325               BYC_wehaveand (id1,t1,id2,t2)
 326     ]
 327 ];
 328   rewriting_step_continuation : [
 329     [ "done" -> true
 330     | -> false
 331     ]
 332 ];
 333   atomic_tactical:
 334     [ "sequence" LEFTA
 335       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 336           let ts =
 337             match t1 with
 338             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 339             | _ -> [ t1; t2 ]
 340           in
 341           GrafiteAst.Seq (loc, ts)
 342       ]
 343     | "then" NONA
 344       [ tac = SELF; SYMBOL ";";
 345         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 346           (GrafiteAst.Then (loc, tac, tacs))
 347       ]
 348     | "loops" RIGHTA
 349       [ IDENT "do"; count = int; tac = SELF ->
 350           GrafiteAst.Do (loc, count, tac)
 351       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 352       ]
 353     | "simple" NONA
 354       [ IDENT "first";
 355         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 356           GrafiteAst.First (loc, tacs)
 357       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 358       | IDENT "solve";
 359         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 360           GrafiteAst.Solve (loc, tacs)
 361       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 362       | LPAREN; tac = SELF; RPAREN -> tac
 363       | tac = tactic -> tac
 364       ]
 365     ];
 366   punctuation_tactical:
 367     [
 368       [ SYMBOL "[" -> GrafiteAst.Branch loc
 369       | SYMBOL "|" -> GrafiteAst.Shift loc
 370       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 371       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 372       | SYMBOL "]" -> GrafiteAst.Merge loc
 373       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 374       | SYMBOL "." -> GrafiteAst.Dot loc
 375       ]
 376     ];
 377   non_punctuation_tactical:
 378     [ "simple" NONA
 379       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 380       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 381       | IDENT "skip" -> GrafiteAst.Skip loc
 382       ]
 383     ];
 384   theorem_flavour: [
 385     [ [ IDENT "definition"  ] -> `Definition
 386     | [ IDENT "fact"        ] -> `Fact
 387     | [ IDENT "lemma"       ] -> `Lemma
 388     | [ IDENT "remark"      ] -> `Remark
 389     | [ IDENT "theorem"     ] -> `Theorem
 390     ]
 391   ];
 392   inductive_spec: [ [
 393     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
 394     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 395     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 396     tl = OPT [ "with";
 397       types = LIST1 [
 398         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 399        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 400           (name, true, typ, constructors) ] SEP "with" -> types
 401     ] ->
 402       let params =
 403         List.fold_right
 404           (fun (names, typ) acc ->
 405             (List.map (fun name -> (name, typ)) names) @ acc)
 406           params []
 407       in
 408       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 409       let tl_ind_types = match tl with None -> [] | Some types -> types in
 410       let ind_types = fst_ind_type :: tl_ind_types in
 411       (params, ind_types)
 412   ] ];
 413
 414   record_spec: [ [
 415     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
 416      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 417      fields = LIST0 [
 418        name = IDENT ;
 419        coercion = [
 420            SYMBOL ":" -> false,0
 421          | SYMBOL ":"; SYMBOL ">" -> true,0
 422          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 423        ];
 424        ty = term ->
 425          let b,n = coercion in
 426          (name,ty,b,n)
 427      ] SEP SYMBOL ";"; SYMBOL "}" ->
 428       let params =
 429         List.fold_right
 430           (fun (names, typ) acc ->
 431             (List.map (fun name -> (name, typ)) names) @ acc)
 432           params []
 433       in
 434       (params,name,typ,fields)
 435   ] ];
 436
 437   macro: [
 438     [ [ IDENT "check"   ]; t = term ->
 439         GrafiteAst.Check (loc, t)
 440     | [ IDENT "inline"];
 441         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 442         suri = QSTRING; prefix = OPT QSTRING ->
 443          let style = match style with
 444             | None       -> GrafiteAst.Declarative
 445             | Some depth -> GrafiteAst.Procedural depth
 446          in
 447          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 448          GrafiteAst.Inline (loc,style,suri,prefix)
 449     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 450          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 451     | IDENT "auto"; params = auto_params ->
 452         GrafiteAst.AutoInteractive (loc,params)
 453     | [ IDENT "whelp"; "match" ] ; t = term ->
 454         GrafiteAst.WMatch (loc,t)
 455     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 456         GrafiteAst.WInstance (loc,t)
 457     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 458         GrafiteAst.WLocate (loc,id)
 459     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 460         GrafiteAst.WElim (loc, t)
 461     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 462         GrafiteAst.WHint (loc,t)
 463     ]
 464   ];
 465   alias_spec: [
 466     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 467       let alpha = "[a-zA-Z]" in
 468       let num = "[0-9]+" in
 469       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 470       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 471       let rex = Str.regexp ("^"^ident^"$") in
 472       if Str.string_match rex id 0 then
 473         if (try ignore (UriManager.uri_of_string uri); true
 474             with UriManager.IllFormedUri _ -> false)
 475         then
 476           LexiconAst.Ident_alias (id, uri)
 477         else
 478           raise
 479            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 480       else
 481         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 482           Printf.sprintf "Not a valid identifier: %s" id)))
 483     | IDENT "symbol"; symbol = QSTRING;
 484       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 485       SYMBOL "="; dsc = QSTRING ->
 486         let instance =
 487           match instance with Some i -> i | None -> 0
 488         in
 489         LexiconAst.Symbol_alias (symbol, instance, dsc)
 490     | IDENT "num";
 491       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 492       SYMBOL "="; dsc = QSTRING ->
 493         let instance =
 494           match instance with Some i -> i | None -> 0
 495         in
 496         LexiconAst.Number_alias (instance, dsc)
 497     ]
 498   ];
 499   argument: [
 500     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 501       id = IDENT ->
 502         Ast.IdentArg (List.length l, id)
 503     ]
 504   ];
 505   associativity: [
 506     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 507     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 508     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 509     ]
 510   ];
 511   precedence: [
 512     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 513   ];
 514   notation: [
 515     [ dir = OPT direction; s = QSTRING;
 516       assoc = OPT associativity; prec = OPT precedence;
 517       IDENT "for";
 518       p2 =
 519         [ blob = UNPARSED_AST ->
 520             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 521               (CicNotationParser.parse_level2_ast
 522                 (Ulexing.from_utf8_string blob))
 523         | blob = UNPARSED_META ->
 524             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 525               (CicNotationParser.parse_level2_meta
 526                 (Ulexing.from_utf8_string blob))
 527         ] ->
 528           let assoc =
 529             match assoc with
 530             | None -> default_associativity
 531             | Some assoc -> assoc
 532           in
 533           let prec =
 534             match prec with
 535             | None -> default_precedence
 536             | Some prec -> prec
 537           in
 538           let p1 =
 539             add_raw_attribute ~text:s
 540               (CicNotationParser.parse_level1_pattern
 541                 (Ulexing.from_utf8_string s))
 542           in
 543           (dir, p1, assoc, prec, p2)
 544     ]
 545   ];
 546   level3_term: [
 547     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 548     | id = IDENT -> Ast.VarPattern id
 549     | SYMBOL "_" -> Ast.ImplicitPattern
 550     | LPAREN; terms = LIST1 SELF; RPAREN ->
 551         (match terms with
 552         | [] -> assert false
 553         | [term] -> term
 554         | terms -> Ast.ApplPattern terms)
 555     ]
 556   ];
 557   interpretation: [
 558     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 559         (s, args, t)
 560     ]
 561   ];
 562
 563   include_command: [ [
 564       IDENT "include" ; path = QSTRING ->
 565         loc,path,LexiconAst.WithPreferences
 566     | IDENT "include'" ; path = QSTRING ->
 567         loc,path,LexiconAst.WithoutPreferences
 568    ]];
 569
 570   grafite_command: [ [
 571       IDENT "set"; n = QSTRING; v = QSTRING ->
 572         GrafiteAst.Set (loc, n, v)
 573     | IDENT "drop" -> GrafiteAst.Drop loc
 574     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 575     | IDENT "qed" -> GrafiteAst.Qed loc
 576     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 577       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 578         GrafiteAst.Obj (loc,
 579           Ast.Theorem
 580             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 581     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 582       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 583         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 584     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 585       body = term ->
 586         GrafiteAst.Obj (loc,
 587           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 588     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 589         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 590     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 591         defs = CicNotationParser.let_defs ->
 592          (* In case of mutual definitions here we produce just
 593             the syntax tree for the first one. The others will be
 594             generated from the completely specified term just before
 595             insertion in the environment. We use the flavour
 596             `MutualDefinition to rememer this. *)
 597           let name,ty =
 598             match defs with
 599             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
 600                 let ty =
 601                  List.fold_right
 602                   (fun var ty -> Ast.Binder (`Pi,var,ty)
 603                   ) params ty
 604                 in
 605                  name,ty
 606             | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
 607                 name, Ast.Implicit
 608             | _ -> assert false
 609           in
 610           let body = Ast.Ident (name,None) in
 611           let flavour =
 612            if List.length defs = 1 then
 613             `Definition
 614            else
 615             `MutualDefinition
 616           in
 617            GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
 618              Some (Ast.LetRec (ind_kind, defs, body))))
 619     | IDENT "inductive"; spec = inductive_spec ->
 620         let (params, ind_types) = spec in
 621         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 622     | IDENT "coinductive"; spec = inductive_spec ->
 623         let (params, ind_types) = spec in
 624         let ind_types = (* set inductive flags to false (coinductive) *)
 625           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 626             ind_types
 627         in
 628         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 629     | IDENT "coercion" ; suri = URI ; arity = OPT int ;
 630       saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
 631         let arity = match arity with None -> 0 | Some x -> x in
 632         let saturations = match saturations with None -> 0 | Some x -> x in
 633         let composites = match composites with None -> true | Some _ -> false in
 634         GrafiteAst.Coercion
 635          (loc, UriManager.uri_of_string suri, composites, arity, saturations)
 636     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 637         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 638     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 639        let uris = List.map UriManager.uri_of_string uris in
 640         GrafiteAst.Default (loc,what,uris)
 641     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 642       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; "by" ;
 643                    refl = tactic_term -> refl ] ;
 644       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ;
 645                    sym = tactic_term -> sym ] ;
 646       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ;
 647                    trans = tactic_term -> trans ] ;
 648       "as" ; id = IDENT ->
 649        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 650   ]];
 651   lexicon_command: [ [
 652       IDENT "alias" ; spec = alias_spec ->
 653         LexiconAst.Alias (loc, spec)
 654     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 655         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 656     | IDENT "interpretation"; id = QSTRING;
 657       (symbol, args, l3) = interpretation ->
 658         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 659   ]];
 660   executable: [
 661     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 662     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 663         GrafiteAst.Tactic (loc, Some tac, punct)
 664     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 665     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 666         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 667     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 668     ]
 669   ];
 670   comment: [
 671     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 672        GrafiteAst.Code (loc, ex)
 673     | str = NOTE ->
 674        GrafiteAst.Note (loc, str)
 675     ]
 676   ];
 677   statement: [
 678     [ ex = executable ->
 679        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 680     | com = comment ->
 681        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 682     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 683        fun ?(never_include=false) ~include_paths status ->
 684         let _root, buri, fullpath, _rrelpath =
 685           Librarian.baseuri_of_script ~include_paths fname
 686         in
 687         let status =
 688          if never_include then raise (NoInclusionPerformed fullpath)
 689          else LexiconEngine.eval_command status
 690                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 691         in
 692          !out fname;
 693          status,
 694           LSome
 695           (GrafiteAst.Executable
 696            (loc,GrafiteAst.Command
 697             (loc,GrafiteAst.Include (iloc,buri))))
 698     | scom = lexicon_command ; SYMBOL "." ->
 699        fun ?(never_include=false) ~include_paths status ->
 700         let status = LexiconEngine.eval_command status scom in
 701          status,LNone loc
 702     | EOI -> raise End_of_file
 703     ]
 704   ];
 705 END
 706
 707 let exc_located_wrapper f =
 708   try
 709     f ()
 710   with
 711   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 712   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 713       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 714   | Stdpp.Exc_located (floc, exn) ->
 715       raise
 716        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 717
 718 let parse_statement lexbuf =
 719   exc_located_wrapper
 720     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
 721