components/grafite_parser/grafiteParser.ml

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