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 EXTEND
  64   GLOBAL: term statement;
  65   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  66   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
  67   ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
  68   tactic_term_list1: [
  69     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
  70   ];
  71   reduction_kind: [
  72     [ IDENT "normalize" -> `Normalize
  73     | IDENT "reduce" -> `Reduce
  74     | IDENT "simplify" -> `Simpl
  75     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
  76     | IDENT "whd" -> `Whd ]
  77   ];
  78   sequent_pattern_spec: [
  79    [ hyp_paths =
  80       LIST0
  81        [ id = IDENT ;
  82          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
  83          (id,match path with Some p -> p | None -> Ast.UserInput) ];
  84      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
  85       let goal_path =
  86        match goal_path, hyp_paths with
  87           None, [] -> Some Ast.UserInput
  88         | None, _::_ -> None
  89         | Some goal_path, _ -> Some goal_path
  90       in
  91        hyp_paths,goal_path
  92    ]
  93   ];
  94   pattern_spec: [
  95     [ res = OPT [
  96        "in";
  97        wanted_and_sps =
  98         [ "match" ; wanted = tactic_term ;
  99           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 100            Some wanted,sps
 101         | sps = sequent_pattern_spec ->
 102            None,Some sps
 103         ] ->
 104          let wanted,hyp_paths,goal_path =
 105           match wanted_and_sps with
 106              wanted,None -> wanted, [], Some Ast.UserInput
 107            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 108          in
 109           wanted, hyp_paths, goal_path ] ->
 110       match res with
 111          None -> None,[],Some Ast.UserInput
 112        | Some ps -> ps]
 113   ];
 114   direction: [
 115     [ SYMBOL ">" -> `LeftToRight
 116     | SYMBOL "<" -> `RightToLeft ]
 117   ];
 118   int: [ [ num = NUMBER -> int_of_string num ] ];
 119   intros_names: [
 120    [ idents = OPT ident_list0 ->
 121       match idents with None -> [] | Some idents -> idents
 122    ]
 123   ];
 124   intros_spec: [
 125     [ OPT [ IDENT "names" ];
 126       num = OPT [ num = int -> num ];
 127       idents = intros_names ->
 128         num, idents
 129     ]
 130   ];
 131   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 132   tactic: [
 133     [ IDENT "absurd"; t = tactic_term ->
 134         GrafiteAst.Absurd (loc, t)
 135     | IDENT "apply"; t = tactic_term ->
 136         GrafiteAst.Apply (loc, t)
 137     | IDENT "applyS"; t = tactic_term ; params =
 138         LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
 139           string_of_int v | v = IDENT -> v ] -> i,v ] ->
 140         GrafiteAst.ApplyS (loc, t, params)
 141     | IDENT "assumption" ->
 142         GrafiteAst.Assumption loc
 143     | IDENT "auto"; params = auto_params ->
 144         GrafiteAst.Auto (loc,params)
 145     | IDENT "cases"; what = tactic_term;
 146       (num, idents) = intros_spec ->
 147         GrafiteAst.Cases (loc, what, idents)
 148     | IDENT "clear"; ids = LIST1 IDENT ->
 149         GrafiteAst.Clear (loc, ids)
 150     | IDENT "clearbody"; id = IDENT ->
 151         GrafiteAst.ClearBody (loc,id)
 152     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 153         GrafiteAst.Change (loc, what, t)
 154     | IDENT "constructor"; n = int ->
 155         GrafiteAst.Constructor (loc, n)
 156     | IDENT "contradiction" ->
 157         GrafiteAst.Contradiction loc
 158     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 159         GrafiteAst.Cut (loc, ident, t)
 160     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
 161         let idents = match idents with None -> [] | Some idents -> idents in
 162         GrafiteAst.Decompose (loc, idents)
 163     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
 164     | IDENT "destruct"; t = tactic_term ->
 165         GrafiteAst.Destruct (loc, t)
 166     | IDENT "elim"; what = tactic_term; using = using;
 167        (num, idents) = intros_spec ->
 168         let pattern = Some what, [], Some Ast.UserInput in
 169         GrafiteAst.Elim (loc, pattern, using, num, idents)
 170     | IDENT "elim"; pattern = pattern_spec; using = using;
 171       (num, idents) = intros_spec ->
 172         GrafiteAst.Elim (loc, pattern, using, num, idents)
 173     | IDENT "elimType"; what = tactic_term; using = using;
 174       (num, idents) = intros_spec ->
 175         GrafiteAst.ElimType (loc, what, using, num, idents)
 176     | IDENT "exact"; t = tactic_term ->
 177         GrafiteAst.Exact (loc, t)
 178     | IDENT "exists" ->
 179         GrafiteAst.Exists loc
 180     | IDENT "fail" -> GrafiteAst.Fail loc
 181     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 182         let (pt,_,_) = p in
 183           if pt <> None then
 184             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 185               ("the pattern cannot specify the term to replace, only its"
 186               ^ " paths in the hypotheses and in the conclusion")))
 187         else
 188          GrafiteAst.Fold (loc, kind, t, p)
 189     | IDENT "fourier" ->
 190         GrafiteAst.Fourier loc
 191     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
 192         let idents = match idents with None -> [] | Some idents -> idents in
 193         GrafiteAst.FwdSimpl (loc, hyp, idents)
 194     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 195        GrafiteAst.Generalize (loc,p,id)
 196     | IDENT "goal"; n = int ->
 197         GrafiteAst.Goal (loc, n)
 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; IDENT "end" ->
 338           GrafiteAst.Do (loc, count, tac)
 339       | IDENT "repeat"; tac = SELF; IDENT "end" -> 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 -> GrafiteAst.Tactic (loc, 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   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       | tac = atomic_tactical LEVEL "loops" -> tac
 371       ]
 372     ];
 373   theorem_flavour: [
 374     [ [ IDENT "definition"  ] -> `Definition
 375     | [ IDENT "fact"        ] -> `Fact
 376     | [ IDENT "lemma"       ] -> `Lemma
 377     | [ IDENT "remark"      ] -> `Remark
 378     | [ IDENT "theorem"     ] -> `Theorem
 379     ]
 380   ];
 381   inductive_spec: [ [
 382     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
 383     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 384     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 385     tl = OPT [ "with";
 386       types = LIST1 [
 387         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 388        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 389           (name, true, typ, constructors) ] SEP "with" -> types
 390     ] ->
 391       let params =
 392         List.fold_right
 393           (fun (names, typ) acc ->
 394             (List.map (fun name -> (name, typ)) names) @ acc)
 395           params []
 396       in
 397       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 398       let tl_ind_types = match tl with None -> [] | Some types -> types in
 399       let ind_types = fst_ind_type :: tl_ind_types in
 400       (params, ind_types)
 401   ] ];
 402
 403   record_spec: [ [
 404     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
 405      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 406      fields = LIST0 [
 407        name = IDENT ;
 408        coercion = [
 409            SYMBOL ":" -> false,0
 410          | SYMBOL ":"; SYMBOL ">" -> true,0
 411          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 412        ];
 413        ty = term ->
 414          let b,n = coercion in
 415          (name,ty,b,n)
 416      ] SEP SYMBOL ";"; SYMBOL "}" ->
 417       let params =
 418         List.fold_right
 419           (fun (names, typ) acc ->
 420             (List.map (fun name -> (name, typ)) names) @ acc)
 421           params []
 422       in
 423       (params,name,typ,fields)
 424   ] ];
 425
 426   macro: [
 427     [ [ IDENT "check"   ]; t = term ->
 428         GrafiteAst.Check (loc, t)
 429     | [ IDENT "inline"];
 430         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 431         suri = QSTRING; prefix = OPT QSTRING ->
 432          let style = match style with
 433             | None       -> GrafiteAst.Declarative
 434             | Some depth -> GrafiteAst.Procedural depth
 435          in
 436          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 437          GrafiteAst.Inline (loc,style,suri,prefix)
 438     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
 439     | [ IDENT "whelp"; "match" ] ; t = term ->
 440         GrafiteAst.WMatch (loc,t)
 441     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 442         GrafiteAst.WInstance (loc,t)
 443     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 444         GrafiteAst.WLocate (loc,id)
 445     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 446         GrafiteAst.WElim (loc, t)
 447     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 448         GrafiteAst.WHint (loc,t)
 449     ]
 450   ];
 451   alias_spec: [
 452     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 453       let alpha = "[a-zA-Z]" in
 454       let num = "[0-9]+" in
 455       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 456       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 457       let rex = Str.regexp ("^"^ident^"$") in
 458       if Str.string_match rex id 0 then
 459         if (try ignore (UriManager.uri_of_string uri); true
 460             with UriManager.IllFormedUri _ -> false)
 461         then
 462           LexiconAst.Ident_alias (id, uri)
 463         else
 464           raise
 465            (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
 466       else
 467         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 468           sprintf "Not a valid identifier: %s" id)))
 469     | IDENT "symbol"; symbol = QSTRING;
 470       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 471       SYMBOL "="; dsc = QSTRING ->
 472         let instance =
 473           match instance with Some i -> i | None -> 0
 474         in
 475         LexiconAst.Symbol_alias (symbol, instance, dsc)
 476     | IDENT "num";
 477       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 478       SYMBOL "="; dsc = QSTRING ->
 479         let instance =
 480           match instance with Some i -> i | None -> 0
 481         in
 482         LexiconAst.Number_alias (instance, dsc)
 483     ]
 484   ];
 485   argument: [
 486     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 487       id = IDENT ->
 488         Ast.IdentArg (List.length l, id)
 489     ]
 490   ];
 491   associativity: [
 492     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 493     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 494     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 495     ]
 496   ];
 497   precedence: [
 498     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 499   ];
 500   notation: [
 501     [ dir = OPT direction; s = QSTRING;
 502       assoc = OPT associativity; prec = OPT precedence;
 503       IDENT "for";
 504       p2 =
 505         [ blob = UNPARSED_AST ->
 506             add_raw_attribute ~text:(sprintf "@{%s}" blob)
 507               (CicNotationParser.parse_level2_ast
 508                 (Ulexing.from_utf8_string blob))
 509         | blob = UNPARSED_META ->
 510             add_raw_attribute ~text:(sprintf "${%s}" blob)
 511               (CicNotationParser.parse_level2_meta
 512                 (Ulexing.from_utf8_string blob))
 513         ] ->
 514           let assoc =
 515             match assoc with
 516             | None -> default_associativity
 517             | Some assoc -> assoc
 518           in
 519           let prec =
 520             match prec with
 521             | None -> default_precedence
 522             | Some prec -> prec
 523           in
 524           let p1 =
 525             add_raw_attribute ~text:s
 526               (CicNotationParser.parse_level1_pattern
 527                 (Ulexing.from_utf8_string s))
 528           in
 529           (dir, p1, assoc, prec, p2)
 530     ]
 531   ];
 532   level3_term: [
 533     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 534     | id = IDENT -> Ast.VarPattern id
 535     | SYMBOL "_" -> Ast.ImplicitPattern
 536     | LPAREN; terms = LIST1 SELF; RPAREN ->
 537         (match terms with
 538         | [] -> assert false
 539         | [term] -> term
 540         | terms -> Ast.ApplPattern terms)
 541     ]
 542   ];
 543   interpretation: [
 544     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 545         (s, args, t)
 546     ]
 547   ];
 548
 549   include_command: [ [
 550       IDENT "include" ; path = QSTRING ->
 551         loc,path,LexiconAst.WithPreferences
 552     | IDENT "include'" ; path = QSTRING ->
 553         loc,path,LexiconAst.WithoutPreferences
 554    ]];
 555
 556   grafite_command: [ [
 557       IDENT "set"; n = QSTRING; v = QSTRING ->
 558         GrafiteAst.Set (loc, n, v)
 559     | IDENT "drop" -> GrafiteAst.Drop loc
 560     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 561     | IDENT "qed" -> GrafiteAst.Qed loc
 562     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 563       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 564         GrafiteAst.Obj (loc,
 565           Ast.Theorem
 566             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 567     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 568       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 569         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 570     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 571       body = term ->
 572         GrafiteAst.Obj (loc,
 573           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 574     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 575         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 576     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 577         defs = CicNotationParser.let_defs ->
 578          (* In case of mutual definitions here we produce just
 579             the syntax tree for the first one. The others will be
 580             generated from the completely specified term just before
 581             insertion in the environment. We use the flavour
 582             `MutualDefinition to rememer this. *)
 583           let name,ty =
 584             match defs with
 585             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
 586                 let ty =
 587                  List.fold_right
 588                   (fun var ty -> Ast.Binder (`Pi,var,ty)
 589                   ) params ty
 590                 in
 591                  name,ty
 592             | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
 593                 name, Ast.Implicit
 594             | _ -> assert false
 595           in
 596           let body = Ast.Ident (name,None) in
 597           let flavour =
 598            if List.length defs = 1 then
 599             `Definition
 600            else
 601             `MutualDefinition
 602           in
 603            GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
 604              Some (Ast.LetRec (ind_kind, defs, body))))
 605     | IDENT "inductive"; spec = inductive_spec ->
 606         let (params, ind_types) = spec in
 607         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 608     | IDENT "coinductive"; spec = inductive_spec ->
 609         let (params, ind_types) = spec in
 610         let ind_types = (* set inductive flags to false (coinductive) *)
 611           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 612             ind_types
 613         in
 614         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 615     | IDENT "coercion" ; suri = URI ; arity = OPT int ->
 616         let arity = match arity with None -> 0 | Some x -> x in
 617         GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
 618     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 619         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 620     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 621        let uris = List.map UriManager.uri_of_string uris in
 622         GrafiteAst.Default (loc,what,uris)
 623     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 624       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 625                    refl = tactic_term -> refl ] ;
 626       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 627                    sym = tactic_term -> sym ] ;
 628       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 629                    trans = tactic_term -> trans ] ;
 630       "as" ; id = IDENT ->
 631        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 632   ]];
 633   lexicon_command: [ [
 634       IDENT "alias" ; spec = alias_spec ->
 635         LexiconAst.Alias (loc, spec)
 636     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 637         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 638     | IDENT "interpretation"; id = QSTRING;
 639       (symbol, args, l3) = interpretation ->
 640         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 641   ]];
 642   executable: [
 643     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 644     | tac = tactical; punct = punctuation_tactical ->
 645         GrafiteAst.Tactical (loc, tac, Some punct)
 646     | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
 647     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 648     ]
 649   ];
 650   comment: [
 651     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 652        GrafiteAst.Code (loc, ex)
 653     | str = NOTE ->
 654        GrafiteAst.Note (loc, str)
 655     ]
 656   ];
 657   statement: [
 658     [ ex = executable ->
 659        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 660     | com = comment ->
 661        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 662     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 663        fun ~include_paths status ->
 664         let buri, fullpath =
 665           DependenciesParser.baseuri_of_script ~include_paths fname
 666         in
 667         let status =
 668          LexiconEngine.eval_command status
 669            (LexiconAst.Include (iloc,buri,mode,fullpath))
 670         in
 671          status,
 672           LSome
 673           (GrafiteAst.Executable
 674            (loc,GrafiteAst.Command
 675             (loc,GrafiteAst.Include (iloc,buri))))
 676     | scom = lexicon_command ; SYMBOL "." ->
 677        fun ~include_paths status ->
 678         let status = LexiconEngine.eval_command status scom in
 679          status,LNone loc
 680     | EOI -> raise End_of_file
 681     ]
 682   ];
 683 END
 684
 685 let exc_located_wrapper f =
 686   try
 687     f ()
 688   with
 689   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 690   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 691       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 692   | Stdpp.Exc_located (floc, exn) ->
 693       raise
 694        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 695
 696 let parse_statement lexbuf =
 697   exc_located_wrapper
 698     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))