helm/software/components/grafite_parser/grafiteParser.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 let out = ref ignore
  29 let set_callback f = out := f
  30
  31 module Ast = CicNotationPt
  32
  33 exception NoInclusionPerformed of string (* full path *)
  34
  35 type 'a localized_option =
  36    LSome of 'a
  37  | LNone of GrafiteAst.loc
  38
  39 type ast_statement =
  40   (CicNotationPt.term, CicNotationPt.term,
  41    CicNotationPt.term GrafiteAst.reduction,
  42    CicNotationPt.term CicNotationPt.obj, string)
  43     GrafiteAst.statement
  44
  45 type statement =
  46   ?never_include:bool ->
  47   include_paths:string list ->
  48   LexiconEngine.status ->
  49     LexiconEngine.status * ast_statement localized_option
  50
  51 type parser_status = {
  52   grammar : Grammar.g;
  53   term : CicNotationPt.term Grammar.Entry.e;
  54   statement : statement Grammar.Entry.e;
  55 }
  56
  57 let initial_parser () =
  58   let grammar = CicNotationParser.level2_ast_grammar () in
  59   let term = CicNotationParser.term () in
  60   let statement = Grammar.Entry.create grammar "statement" in
  61   { grammar = grammar; term = term; statement = statement }
  62 ;;
  63
  64 let grafite_parser = ref (initial_parser ())
  65
  66 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
  67
  68 let default_associativity = Gramext.NonA
  69
  70 let mk_rec_corec ind_kind defs loc =
  71  (* In case of mutual definitions here we produce just
  72     the syntax tree for the first one. The others will be
  73     generated from the completely specified term just before
  74     insertion in the environment. We use the flavour
  75     `MutualDefinition to rememer this. *)
  76   let name,ty =
  77     match defs with
  78     | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
  79         let ty =
  80          List.fold_right
  81           (fun var ty -> Ast.Binder (`Pi,var,ty)
  82           ) params ty
  83         in
  84          name,ty
  85     | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
  86         name, Ast.Implicit
  87     | _ -> assert false
  88   in
  89   let body = Ast.Ident (name,None) in
  90   let flavour =
  91    if List.length defs = 1 then
  92     `Definition
  93    else
  94     `MutualDefinition
  95   in
  96    GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
  97      Some (Ast.LetRec (ind_kind, defs, body))))
  98
  99 type by_continuation =
 100    BYC_done
 101  | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
 102  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
 103  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
 104
 105 let initialize_parser () =
 106   (* {{{ parser initialization *)
 107   let term = !grafite_parser.term in
 108   let statement = !grafite_parser.statement in
 109   let let_defs = CicNotationParser.let_defs () in
 110   let protected_binder_vars = CicNotationParser.protected_binder_vars () in
 111 EXTEND
 112   GLOBAL: term statement;
 113   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
 114   tactic_term: [ [ t = term LEVEL "90" -> t ] ];
 115   new_name: [
 116     [ id = IDENT -> Some id
 117     | SYMBOL "_" -> None ]
 118     ];
 119   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
 120   tactic_term_list1: [
 121     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
 122   ];
 123   reduction_kind: [
 124     [ IDENT "normalize" -> `Normalize
 125     | IDENT "simplify" -> `Simpl
 126     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
 127     | IDENT "whd" -> `Whd ]
 128   ];
 129   sequent_pattern_spec: [
 130    [ hyp_paths =
 131       LIST0
 132        [ id = IDENT ;
 133          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
 134          (id,match path with Some p -> p | None -> Ast.UserInput) ];
 135      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
 136       let goal_path =
 137        match goal_path, hyp_paths with
 138           None, [] -> Some Ast.UserInput
 139         | None, _::_ -> None
 140         | Some goal_path, _ -> Some goal_path
 141       in
 142        hyp_paths,goal_path
 143    ]
 144   ];
 145   pattern_spec: [
 146     [ res = OPT [
 147        "in";
 148        wanted_and_sps =
 149         [ "match" ; wanted = tactic_term ;
 150           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 151            Some wanted,sps
 152         | sps = sequent_pattern_spec ->
 153            None,Some sps
 154         ] ->
 155          let wanted,hyp_paths,goal_path =
 156           match wanted_and_sps with
 157              wanted,None -> wanted, [], Some Ast.UserInput
 158            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 159          in
 160           wanted, hyp_paths, goal_path ] ->
 161       match res with
 162          None -> None,[],Some Ast.UserInput
 163        | Some ps -> ps]
 164   ];
 165   direction: [
 166     [ SYMBOL ">" -> `LeftToRight
 167     | SYMBOL "<" -> `RightToLeft ]
 168   ];
 169   int: [ [ num = NUMBER -> int_of_string num ] ];
 170   intros_names: [
 171    [ idents = OPT ident_list0 ->
 172       match idents with None -> [] | Some idents -> idents
 173    ]
 174   ];
 175   intros_spec: [
 176     [ OPT [ IDENT "names" ];
 177       num = OPT [ num = int -> num ];
 178       idents = intros_names ->
 179         num, idents
 180     ]
 181   ];
 182   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 183   ntactic: [
 184     [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
 185     | IDENT "nassert";
 186        seqs = LIST0 [
 187         hyps = LIST0
 188          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 189          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 190                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 191             id,`Def (bo,ty)];
 192         SYMBOL <:unicode<vdash>>;
 193         concl = tactic_term -> (List.rev hyps,concl) ] ->
 194          GrafiteAst.NAssert (loc, seqs)
 195     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 196         GrafiteAst.NCases (loc, what, where)
 197     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 198         GrafiteAst.NChange (loc, what, with_what)
 199     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 200         GrafiteAst.NElim (loc, what, where)
 201     | IDENT "ngeneralize"; p=pattern_spec ->
 202         GrafiteAst.NGeneralize (loc, p)
 203     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 204         where = pattern_spec ->
 205         GrafiteAst.NLetIn (loc,where,t,name)
 206     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 207         GrafiteAst.NRewrite (loc, dir, what, where)
 208     | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
 209       where = pattern_spec ->
 210         let delta = match delta with None -> true | _ -> false in
 211         GrafiteAst.NEval (loc, where, `Whd delta)
 212     | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
 213     | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
 214     | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
 215     | SYMBOL "*"; n=IDENT ->
 216         GrafiteAst.NCase1 (loc,n)
 217     ]
 218   ];
 219   tactic: [
 220     [ IDENT "absurd"; t = tactic_term ->
 221         GrafiteAst.Absurd (loc, t)
 222     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 223         GrafiteAst.ApplyRule (loc, t)
 224     | IDENT "apply"; t = tactic_term ->
 225         GrafiteAst.Apply (loc, t)
 226     | IDENT "applyP"; t = tactic_term ->
 227         GrafiteAst.ApplyP (loc, t)
 228     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 229         GrafiteAst.ApplyS (loc, t, params)
 230     | IDENT "assumption" ->
 231         GrafiteAst.Assumption loc
 232     | IDENT "autobatch";  params = auto_params ->
 233         GrafiteAst.AutoBatch (loc,params)
 234     | IDENT "cases"; what = tactic_term;
 235       pattern = OPT pattern_spec;
 236       specs = intros_spec ->
 237         let pattern = match pattern with
 238            | None         -> None, [], Some Ast.UserInput
 239            | Some pattern -> pattern
 240         in
 241         GrafiteAst.Cases (loc, what, pattern, specs)
 242     | IDENT "clear"; ids = LIST1 IDENT ->
 243         GrafiteAst.Clear (loc, ids)
 244     | IDENT "clearbody"; id = IDENT ->
 245         GrafiteAst.ClearBody (loc,id)
 246     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 247         GrafiteAst.Change (loc, what, t)
 248     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 249       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 250         let times = match times with None -> 1 | Some i -> i in
 251         GrafiteAst.Compose (loc, t1, t2, times, specs)
 252     | IDENT "constructor"; n = int ->
 253         GrafiteAst.Constructor (loc, n)
 254     | IDENT "contradiction" ->
 255         GrafiteAst.Contradiction loc
 256     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 257         GrafiteAst.Cut (loc, ident, t)
 258     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 259         let idents = match idents with None -> [] | Some idents -> idents in
 260         GrafiteAst.Decompose (loc, idents)
 261     | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
 262     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 263         GrafiteAst.Destruct (loc, xts)
 264     | IDENT "elim"; what = tactic_term; using = using;
 265        pattern = OPT pattern_spec;
 266        ispecs = intros_spec ->
 267         let pattern = match pattern with
 268            | None         -> None, [], Some Ast.UserInput
 269            | Some pattern -> pattern
 270         in
 271         GrafiteAst.Elim (loc, what, using, pattern, ispecs)
 272     | IDENT "elimType"; what = tactic_term; using = using;
 273       (num, idents) = intros_spec ->
 274         GrafiteAst.ElimType (loc, what, using, (num, idents))
 275     | IDENT "exact"; t = tactic_term ->
 276         GrafiteAst.Exact (loc, t)
 277     | IDENT "exists" ->
 278         GrafiteAst.Exists loc
 279     | IDENT "fail" -> GrafiteAst.Fail loc
 280     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 281         let (pt,_,_) = p in
 282           if pt <> None then
 283             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 284               ("the pattern cannot specify the term to replace, only its"
 285               ^ " paths in the hypotheses and in the conclusion")))
 286         else
 287          GrafiteAst.Fold (loc, kind, t, p)
 288     | IDENT "fourier" ->
 289         GrafiteAst.Fourier loc
 290     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 291         let idents = match idents with None -> [] | Some idents -> idents in
 292         GrafiteAst.FwdSimpl (loc, hyp, idents)
 293     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 294        GrafiteAst.Generalize (loc,p,id)
 295     | IDENT "id" -> GrafiteAst.IdTac loc
 296     | IDENT "intro"; ident = OPT IDENT ->
 297         let idents = match ident with None -> [] | Some id -> [Some id] in
 298         GrafiteAst.Intros (loc, (Some 1, idents))
 299     | IDENT "intros"; specs = intros_spec ->
 300         GrafiteAst.Intros (loc, specs)
 301     | IDENT "inversion"; t = tactic_term ->
 302         GrafiteAst.Inversion (loc, t)
 303     | IDENT "lapply";
 304       linear = OPT [ IDENT "linear" ];
 305       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 306       what = tactic_term;
 307       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 308       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 309         let linear = match linear with None -> false | Some _ -> true in
 310         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 311         GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
 312     | IDENT "left" -> GrafiteAst.Left loc
 313     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 314         GrafiteAst.LetIn (loc, t, where)
 315     | kind = reduction_kind; p = pattern_spec ->
 316         GrafiteAst.Reduce (loc, kind, p)
 317     | IDENT "reflexivity" ->
 318         GrafiteAst.Reflexivity loc
 319     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 320         GrafiteAst.Replace (loc, p, t)
 321     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 322        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 323        let (pt,_,_) = p in
 324         if pt <> None then
 325          raise
 326           (HExtlib.Localized (loc,
 327            (CicNotationParser.Parse_error
 328             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 329         else
 330          let n = match xnames with None -> [] | Some names -> names in
 331          GrafiteAst.Rewrite (loc, d, t, p, n)
 332     | IDENT "right" ->
 333         GrafiteAst.Right loc
 334     | IDENT "ring" ->
 335         GrafiteAst.Ring loc
 336     | IDENT "split" ->
 337         GrafiteAst.Split loc
 338     | IDENT "symmetry" ->
 339         GrafiteAst.Symmetry loc
 340     | IDENT "transitivity"; t = tactic_term ->
 341         GrafiteAst.Transitivity (loc, t)
 342      (* Produzioni Aggiunte *)
 343     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 344         GrafiteAst.Assume (loc, id, t)
 345     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 346       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 347                 t' = tactic_term -> t']->
 348         GrafiteAst.Suppose (loc, t, id, t1)
 349     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 350       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 351       id2 = IDENT ; RPAREN ->
 352         GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 353     | just =
 354        [ IDENT "using"; t=tactic_term -> `Term t
 355        | params = auto_params -> `Auto params] ;
 356       cont=by_continuation ->
 357        (match cont with
 358            BYC_done -> GrafiteAst.Bydone (loc, just)
 359          | BYC_weproved (ty,id,t1) ->
 360             GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
 361          | BYC_letsuchthat (id1,t1,id2,t2) ->
 362             GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
 363          | BYC_wehaveand (id1,t1,id2,t2) ->
 364             GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
 365     | 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']->
 366         GrafiteAst.We_need_to_prove (loc, t, id, t1)
 367     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 368         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
 369     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 370         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
 371     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 372         GrafiteAst.Byinduction(loc, t, id)
 373     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 374         GrafiteAst.Thesisbecomes(loc, t)
 375     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 376         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 377          GrafiteAst.Case(loc,id,params)
 378       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 379     | IDENT "conclude";
 380       termine = tactic_term;
 381       SYMBOL "=" ;
 382       t1=tactic_term ;
 383       t2 =
 384        [ IDENT "using"; t=tactic_term -> `Term t
 385        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 386        | IDENT "proof" -> `Proof
 387        | params = auto_params -> `Auto params];
 388       cont = rewriting_step_continuation ->
 389        GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 390     | IDENT "obtain" ; name = IDENT;
 391       termine = tactic_term;
 392       SYMBOL "=" ;
 393       t1=tactic_term ;
 394       t2 =
 395        [ IDENT "using"; t=tactic_term -> `Term t
 396        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 397        | IDENT "proof" -> `Proof
 398        | params = auto_params -> `Auto params];
 399       cont = rewriting_step_continuation ->
 400        GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 401     | SYMBOL "=" ;
 402       t1=tactic_term ;
 403       t2 =
 404        [ IDENT "using"; t=tactic_term -> `Term t
 405        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 406        | IDENT "proof" -> `Proof
 407        | params = auto_params -> `Auto params];
 408       cont = rewriting_step_continuation ->
 409        GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
 410   ]
 411 ];
 412   auto_fixed_param: [
 413    [ IDENT "paramodulation"
 414    | IDENT "depth"
 415    | IDENT "width"
 416    | IDENT "size"
 417    | IDENT "timeout"
 418    | IDENT "library"
 419    | IDENT "type"
 420    | IDENT "steps"
 421    | IDENT "all"
 422    ]
 423 ];
 424   auto_params: [
 425    [ params =
 426       LIST0 [
 427          i = auto_fixed_param -> i,""
 428        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 429               string_of_int v | v = IDENT -> v ] -> i,v ];
 430       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 431       (match tl with Some l -> l | None -> []),
 432       params
 433    ]
 434 ];
 435   by_continuation: [
 436     [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
 437     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 438             "done" -> BYC_weproved (ty,None,t1)
 439     | "done" -> BYC_done
 440     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 441       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 442       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 443     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 444               BYC_wehaveand (id1,t1,id2,t2)
 445     ]
 446 ];
 447   rewriting_step_continuation : [
 448     [ "done" -> true
 449     | -> false
 450     ]
 451 ];
 452   atomic_tactical:
 453     [ "sequence" LEFTA
 454       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 455           let ts =
 456             match t1 with
 457             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 458             | _ -> [ t1; t2 ]
 459           in
 460           GrafiteAst.Seq (loc, ts)
 461       ]
 462     | "then" NONA
 463       [ tac = SELF; SYMBOL ";";
 464         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 465           (GrafiteAst.Then (loc, tac, tacs))
 466       ]
 467     | "loops" RIGHTA
 468       [ IDENT "do"; count = int; tac = SELF ->
 469           GrafiteAst.Do (loc, count, tac)
 470       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 471       ]
 472     | "simple" NONA
 473       [ IDENT "first";
 474         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 475           GrafiteAst.First (loc, tacs)
 476       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 477       | IDENT "solve";
 478         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 479           GrafiteAst.Solve (loc, tacs)
 480       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 481       | LPAREN; tac = SELF; RPAREN -> tac
 482       | tac = tactic -> tac
 483       ]
 484     ];
 485   punctuation_tactical:
 486     [
 487       [ SYMBOL "[" -> GrafiteAst.Branch loc
 488       | SYMBOL "|" -> GrafiteAst.Shift loc
 489       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 490       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 491       | SYMBOL "]" -> GrafiteAst.Merge loc
 492       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 493       | SYMBOL "." -> GrafiteAst.Dot loc
 494       ]
 495     ];
 496   non_punctuation_tactical:
 497     [ "simple" NONA
 498       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 499       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 500       | IDENT "skip" -> GrafiteAst.Skip loc
 501       ]
 502     ];
 503   ntheorem_flavour: [
 504     [ [ IDENT "ntheorem"     ] -> `Theorem
 505     ]
 506   ];
 507   theorem_flavour: [
 508     [ [ IDENT "definition"  ] -> `Definition
 509     | [ IDENT "fact"        ] -> `Fact
 510     | [ IDENT "lemma"       ] -> `Lemma
 511     | [ IDENT "remark"      ] -> `Remark
 512     | [ IDENT "theorem"     ] -> `Theorem
 513     ]
 514   ];
 515   inline_flavour: [
 516      [ attr = theorem_flavour -> attr
 517      | [ IDENT "axiom"     ]  -> `Axiom
 518      | [ IDENT "mutual"    ]  -> `MutualDefinition
 519      ]
 520   ];
 521   inductive_spec: [ [
 522     fst_name = IDENT;
 523       params = LIST0 protected_binder_vars;
 524     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 525     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 526     tl = OPT [ "with";
 527       types = LIST1 [
 528         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 529        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 530           (name, true, typ, constructors) ] SEP "with" -> types
 531     ] ->
 532       let params =
 533         List.fold_right
 534           (fun (names, typ) acc ->
 535             (List.map (fun name -> (name, typ)) names) @ acc)
 536           params []
 537       in
 538       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 539       let tl_ind_types = match tl with None -> [] | Some types -> types in
 540       let ind_types = fst_ind_type :: tl_ind_types in
 541       (params, ind_types)
 542   ] ];
 543
 544   record_spec: [ [
 545     name = IDENT;
 546     params = LIST0 protected_binder_vars;
 547      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 548      fields = LIST0 [
 549        name = IDENT ;
 550        coercion = [
 551            SYMBOL ":" -> false,0
 552          | SYMBOL ":"; SYMBOL ">" -> true,0
 553          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 554        ];
 555        ty = term ->
 556          let b,n = coercion in
 557          (name,ty,b,n)
 558      ] SEP SYMBOL ";"; SYMBOL "}" ->
 559       let params =
 560         List.fold_right
 561           (fun (names, typ) acc ->
 562             (List.map (fun name -> (name, typ)) names) @ acc)
 563           params []
 564       in
 565       (params,name,typ,fields)
 566   ] ];
 567
 568   macro: [
 569     [ [ IDENT "check"   ]; t = term ->
 570         GrafiteAst.Check (loc, t)
 571     | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 572         GrafiteAst.Eval (loc, kind, t)
 573     | [ IDENT "inline"];
 574         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 575         suri = QSTRING; prefix = OPT QSTRING;
 576         flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
 577          let style = match style with
 578             | None       -> GrafiteAst.Declarative
 579             | Some depth -> GrafiteAst.Procedural depth
 580          in
 581          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 582          GrafiteAst.Inline (loc,style,suri,prefix, flavour)
 583     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 584          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 585     | IDENT "auto"; params = auto_params ->
 586         GrafiteAst.AutoInteractive (loc,params)
 587     | [ IDENT "whelp"; "match" ] ; t = term ->
 588         GrafiteAst.WMatch (loc,t)
 589     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 590         GrafiteAst.WInstance (loc,t)
 591     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 592         GrafiteAst.WLocate (loc,id)
 593     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 594         GrafiteAst.WElim (loc, t)
 595     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 596         GrafiteAst.WHint (loc,t)
 597     ]
 598   ];
 599   alias_spec: [
 600     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 601       let alpha = "[a-zA-Z]" in
 602       let num = "[0-9]+" in
 603       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 604       let decoration = "\\'" in
 605       let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 606       let rex = Str.regexp ("^"^ident^"$") in
 607       if Str.string_match rex id 0 then
 608         if (try ignore (UriManager.uri_of_string uri); true
 609             with UriManager.IllFormedUri _ -> false)
 610         then
 611           LexiconAst.Ident_alias (id, uri)
 612         else
 613           raise
 614            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 615       else
 616         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 617           Printf.sprintf "Not a valid identifier: %s" id)))
 618     | IDENT "symbol"; symbol = QSTRING;
 619       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 620       SYMBOL "="; dsc = QSTRING ->
 621         let instance =
 622           match instance with Some i -> i | None -> 0
 623         in
 624         LexiconAst.Symbol_alias (symbol, instance, dsc)
 625     | IDENT "num";
 626       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 627       SYMBOL "="; dsc = QSTRING ->
 628         let instance =
 629           match instance with Some i -> i | None -> 0
 630         in
 631         LexiconAst.Number_alias (instance, dsc)
 632     ]
 633   ];
 634   argument: [
 635     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 636       id = IDENT ->
 637         Ast.IdentArg (List.length l, id)
 638     ]
 639   ];
 640   associativity: [
 641     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 642     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 643     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 644     ]
 645   ];
 646   precedence: [
 647     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 648   ];
 649   notation: [
 650     [ dir = OPT direction; s = QSTRING;
 651       assoc = OPT associativity; prec = precedence;
 652       IDENT "for";
 653       p2 =
 654         [ blob = UNPARSED_AST ->
 655             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 656               (CicNotationParser.parse_level2_ast
 657                 (Ulexing.from_utf8_string blob))
 658         | blob = UNPARSED_META ->
 659             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 660               (CicNotationParser.parse_level2_meta
 661                 (Ulexing.from_utf8_string blob))
 662         ] ->
 663           let assoc =
 664             match assoc with
 665             | None -> default_associativity
 666             | Some assoc -> assoc
 667           in
 668           let p1 =
 669             add_raw_attribute ~text:s
 670               (CicNotationParser.parse_level1_pattern prec
 671                 (Ulexing.from_utf8_string s))
 672           in
 673           (dir, p1, assoc, prec, p2)
 674     ]
 675   ];
 676   level3_term: [
 677     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 678     | id = IDENT -> Ast.VarPattern id
 679     | SYMBOL "_" -> Ast.ImplicitPattern
 680     | LPAREN; terms = LIST1 SELF; RPAREN ->
 681         (match terms with
 682         | [] -> assert false
 683         | [term] -> term
 684         | terms -> Ast.ApplPattern terms)
 685     ]
 686   ];
 687   interpretation: [
 688     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 689         (s, args, t)
 690     ]
 691   ];
 692
 693   include_command: [ [
 694       IDENT "include" ; path = QSTRING ->
 695         loc,path,LexiconAst.WithPreferences
 696     | IDENT "include'" ; path = QSTRING ->
 697         loc,path,LexiconAst.WithoutPreferences
 698    ]];
 699
 700   grafite_command: [ [
 701       IDENT "set"; n = QSTRING; v = QSTRING ->
 702         GrafiteAst.Set (loc, n, v)
 703     | IDENT "drop" -> GrafiteAst.Drop loc
 704     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 705     | IDENT "qed" -> GrafiteAst.Qed loc
 706     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 707       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 708         GrafiteAst.Obj (loc,
 709           Ast.Theorem
 710             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 711     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 712       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 713         GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
 714     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 715       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 716         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 717     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 718       body = term ->
 719         GrafiteAst.Obj (loc,
 720           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 721     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 722         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 723     | LETCOREC ; defs = let_defs ->
 724         mk_rec_corec `CoInductive defs loc
 725     | LETREC ; defs = let_defs ->
 726         mk_rec_corec `Inductive defs loc
 727     | IDENT "inductive"; spec = inductive_spec ->
 728         let (params, ind_types) = spec in
 729         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 730     | IDENT "coinductive"; spec = inductive_spec ->
 731         let (params, ind_types) = spec in
 732         let ind_types = (* set inductive flags to false (coinductive) *)
 733           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 734             ind_types
 735         in
 736         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 737     | IDENT "coercion" ;
 738       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 739       arity = OPT int ; saturations = OPT int;
 740       composites = OPT (IDENT "nocomposites") ->
 741         let arity = match arity with None -> 0 | Some x -> x in
 742         let saturations = match saturations with None -> 0 | Some x -> x in
 743         let composites = match composites with None -> true | Some _ -> false in
 744         GrafiteAst.Coercion
 745          (loc, t, composites, arity, saturations)
 746     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 747         GrafiteAst.PreferCoercion (loc, t)
 748     | IDENT "pump" ; steps = int ->
 749         GrafiteAst.Pump(loc,steps)
 750     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 751         GrafiteAst.UnificationHint (loc, t, n)
 752     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 753         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 754     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 755        let uris = List.map UriManager.uri_of_string uris in
 756         GrafiteAst.Default (loc,what,uris)
 757     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 758       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 759                    refl = tactic_term -> refl ] ;
 760       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 761                    sym = tactic_term -> sym ] ;
 762       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 763                    trans = tactic_term -> trans ] ;
 764       "as" ; id = IDENT ->
 765        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 766   ]];
 767   lexicon_command: [ [
 768       IDENT "alias" ; spec = alias_spec ->
 769         LexiconAst.Alias (loc, spec)
 770     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 771         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 772     | IDENT "interpretation"; id = QSTRING;
 773       (symbol, args, l3) = interpretation ->
 774         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 775   ]];
 776   executable: [
 777     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 778     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 779         GrafiteAst.Tactic (loc, Some tac, punct)
 780     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 781     | tac = ntactic; punct = punctuation_tactical ->
 782         GrafiteAst.NTactic (loc, tac, punct)
 783     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 784         GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
 785     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 786         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 787     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 788     ]
 789   ];
 790   comment: [
 791     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 792        GrafiteAst.Code (loc, ex)
 793     | str = NOTE ->
 794        GrafiteAst.Note (loc, str)
 795     ]
 796   ];
 797   statement: [
 798     [ ex = executable ->
 799        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 800     | com = comment ->
 801        fun ?(never_include=false) ~include_paths status ->
 802                status,LSome (GrafiteAst.Comment (loc, com))
 803     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 804        !out fname;
 805        fun ?(never_include=false) ~include_paths status ->
 806         let _root, buri, fullpath, _rrelpath =
 807           Librarian.baseuri_of_script ~include_paths fname
 808         in
 809         let status =
 810          if never_include then raise (NoInclusionPerformed fullpath)
 811          else LexiconEngine.eval_command status
 812                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 813         in
 814          status,
 815           LSome
 816           (GrafiteAst.Executable
 817            (loc,GrafiteAst.Command
 818             (loc,GrafiteAst.Include (iloc,buri))))
 819     | scom = lexicon_command ; SYMBOL "." ->
 820        fun ?(never_include=false) ~include_paths status ->
 821         let status = LexiconEngine.eval_command status scom in
 822          status,LNone loc
 823     | EOI -> raise End_of_file
 824     ]
 825   ];
 826 END
 827 (* }}} *)
 828 ;;
 829
 830 let _ = initialize_parser () ;;
 831
 832 let exc_located_wrapper f =
 833   try
 834     f ()
 835   with
 836   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 837   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 838       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 839   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 840       raise
 841        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 842   | Stdpp.Exc_located (floc, exn) ->
 843       raise
 844        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 845
 846 let parse_statement lexbuf =
 847   exc_located_wrapper
 848     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 849
 850 let statement () = !grafite_parser.statement
 851
 852 let history = ref [] ;;
 853
 854 let push () =
 855   LexiconSync.push ();
 856   history := !grafite_parser :: !history;
 857   grafite_parser := initial_parser ();
 858   initialize_parser ()
 859 ;;
 860
 861 let pop () =
 862   LexiconSync.pop ();
 863   match !history with
 864   | [] -> assert false
 865   | gp :: tail ->
 866       grafite_parser := gp;
 867       history := tail
 868 ;;
 869
 870 (* vim:set foldmethod=marker: *)
 871
 872