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