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