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