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