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