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