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