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