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