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