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