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    ]
 421 ];
 422   auto_params: [
 423    [ params =
 424       LIST0 [
 425          i = auto_fixed_param -> i,""
 426        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 427               string_of_int v | v = IDENT -> v ] -> i,v ];
 428       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 429       (match tl with Some l -> l | None -> []),
 430       params
 431    ]
 432 ];
 433   by_continuation: [
 434     [ 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)
 435     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 436             "done" -> BYC_weproved (ty,None,t1)
 437     | "done" -> BYC_done
 438     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 439       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 440       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 441     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 442               BYC_wehaveand (id1,t1,id2,t2)
 443     ]
 444 ];
 445   rewriting_step_continuation : [
 446     [ "done" -> true
 447     | -> false
 448     ]
 449 ];
 450   atomic_tactical:
 451     [ "sequence" LEFTA
 452       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 453           let ts =
 454             match t1 with
 455             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 456             | _ -> [ t1; t2 ]
 457           in
 458           GrafiteAst.Seq (loc, ts)
 459       ]
 460     | "then" NONA
 461       [ tac = SELF; SYMBOL ";";
 462         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 463           (GrafiteAst.Then (loc, tac, tacs))
 464       ]
 465     | "loops" RIGHTA
 466       [ IDENT "do"; count = int; tac = SELF ->
 467           GrafiteAst.Do (loc, count, tac)
 468       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 469       ]
 470     | "simple" NONA
 471       [ IDENT "first";
 472         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 473           GrafiteAst.First (loc, tacs)
 474       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 475       | IDENT "solve";
 476         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 477           GrafiteAst.Solve (loc, tacs)
 478       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 479       | LPAREN; tac = SELF; RPAREN -> tac
 480       | tac = tactic -> tac
 481       ]
 482     ];
 483   punctuation_tactical:
 484     [
 485       [ SYMBOL "[" -> GrafiteAst.Branch loc
 486       | SYMBOL "|" -> GrafiteAst.Shift loc
 487       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 488       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 489       | SYMBOL "]" -> GrafiteAst.Merge loc
 490       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 491       | SYMBOL "." -> GrafiteAst.Dot loc
 492       ]
 493     ];
 494   non_punctuation_tactical:
 495     [ "simple" NONA
 496       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 497       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 498       | IDENT "skip" -> GrafiteAst.Skip loc
 499       ]
 500     ];
 501   ntheorem_flavour: [
 502     [ [ IDENT "ntheorem"     ] -> `Theorem
 503     ]
 504   ];
 505   theorem_flavour: [
 506     [ [ IDENT "definition"  ] -> `Definition
 507     | [ IDENT "fact"        ] -> `Fact
 508     | [ IDENT "lemma"       ] -> `Lemma
 509     | [ IDENT "remark"      ] -> `Remark
 510     | [ IDENT "theorem"     ] -> `Theorem
 511     ]
 512   ];
 513   inline_flavour: [
 514      [ attr = theorem_flavour -> attr
 515      | [ IDENT "axiom"     ]  -> `Axiom
 516      | [ IDENT "mutual"    ]  -> `MutualDefinition
 517      ]
 518   ];
 519   inductive_spec: [ [
 520     fst_name = IDENT;
 521       params = LIST0 protected_binder_vars;
 522     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 523     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 524     tl = OPT [ "with";
 525       types = LIST1 [
 526         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 527        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 528           (name, true, typ, constructors) ] SEP "with" -> types
 529     ] ->
 530       let params =
 531         List.fold_right
 532           (fun (names, typ) acc ->
 533             (List.map (fun name -> (name, typ)) names) @ acc)
 534           params []
 535       in
 536       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 537       let tl_ind_types = match tl with None -> [] | Some types -> types in
 538       let ind_types = fst_ind_type :: tl_ind_types in
 539       (params, ind_types)
 540   ] ];
 541
 542   record_spec: [ [
 543     name = IDENT;
 544     params = LIST0 protected_binder_vars;
 545      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 546      fields = LIST0 [
 547        name = IDENT ;
 548        coercion = [
 549            SYMBOL ":" -> false,0
 550          | SYMBOL ":"; SYMBOL ">" -> true,0
 551          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 552        ];
 553        ty = term ->
 554          let b,n = coercion in
 555          (name,ty,b,n)
 556      ] SEP SYMBOL ";"; SYMBOL "}" ->
 557       let params =
 558         List.fold_right
 559           (fun (names, typ) acc ->
 560             (List.map (fun name -> (name, typ)) names) @ acc)
 561           params []
 562       in
 563       (params,name,typ,fields)
 564   ] ];
 565
 566   macro: [
 567     [ [ IDENT "check"   ]; t = term ->
 568         GrafiteAst.Check (loc, t)
 569     | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 570         GrafiteAst.Eval (loc, kind, t)
 571     | [ IDENT "inline"];
 572         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 573         suri = QSTRING; prefix = OPT QSTRING;
 574         flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
 575          let style = match style with
 576             | None       -> GrafiteAst.Declarative
 577             | Some depth -> GrafiteAst.Procedural depth
 578          in
 579          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 580          GrafiteAst.Inline (loc,style,suri,prefix, flavour)
 581     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 582          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 583     | IDENT "auto"; params = auto_params ->
 584         GrafiteAst.AutoInteractive (loc,params)
 585     | [ IDENT "whelp"; "match" ] ; t = term ->
 586         GrafiteAst.WMatch (loc,t)
 587     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 588         GrafiteAst.WInstance (loc,t)
 589     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 590         GrafiteAst.WLocate (loc,id)
 591     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 592         GrafiteAst.WElim (loc, t)
 593     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 594         GrafiteAst.WHint (loc,t)
 595     ]
 596   ];
 597   alias_spec: [
 598     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 599       let alpha = "[a-zA-Z]" in
 600       let num = "[0-9]+" in
 601       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 602       let decoration = "\\'" in
 603       let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 604       let rex = Str.regexp ("^"^ident^"$") in
 605       if Str.string_match rex id 0 then
 606         if (try ignore (UriManager.uri_of_string uri); true
 607             with UriManager.IllFormedUri _ -> false)
 608         then
 609           LexiconAst.Ident_alias (id, uri)
 610         else
 611           raise
 612            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 613       else
 614         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 615           Printf.sprintf "Not a valid identifier: %s" id)))
 616     | IDENT "symbol"; symbol = QSTRING;
 617       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 618       SYMBOL "="; dsc = QSTRING ->
 619         let instance =
 620           match instance with Some i -> i | None -> 0
 621         in
 622         LexiconAst.Symbol_alias (symbol, instance, dsc)
 623     | IDENT "num";
 624       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 625       SYMBOL "="; dsc = QSTRING ->
 626         let instance =
 627           match instance with Some i -> i | None -> 0
 628         in
 629         LexiconAst.Number_alias (instance, dsc)
 630     ]
 631   ];
 632   argument: [
 633     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 634       id = IDENT ->
 635         Ast.IdentArg (List.length l, id)
 636     ]
 637   ];
 638   associativity: [
 639     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 640     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 641     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 642     ]
 643   ];
 644   precedence: [
 645     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 646   ];
 647   notation: [
 648     [ dir = OPT direction; s = QSTRING;
 649       assoc = OPT associativity; prec = precedence;
 650       IDENT "for";
 651       p2 =
 652         [ blob = UNPARSED_AST ->
 653             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 654               (CicNotationParser.parse_level2_ast
 655                 (Ulexing.from_utf8_string blob))
 656         | blob = UNPARSED_META ->
 657             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 658               (CicNotationParser.parse_level2_meta
 659                 (Ulexing.from_utf8_string blob))
 660         ] ->
 661           let assoc =
 662             match assoc with
 663             | None -> default_associativity
 664             | Some assoc -> assoc
 665           in
 666           let p1 =
 667             add_raw_attribute ~text:s
 668               (CicNotationParser.parse_level1_pattern prec
 669                 (Ulexing.from_utf8_string s))
 670           in
 671           (dir, p1, assoc, prec, p2)
 672     ]
 673   ];
 674   level3_term: [
 675     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 676     | id = IDENT -> Ast.VarPattern id
 677     | SYMBOL "_" -> Ast.ImplicitPattern
 678     | LPAREN; terms = LIST1 SELF; RPAREN ->
 679         (match terms with
 680         | [] -> assert false
 681         | [term] -> term
 682         | terms -> Ast.ApplPattern terms)
 683     ]
 684   ];
 685   interpretation: [
 686     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 687         (s, args, t)
 688     ]
 689   ];
 690
 691   include_command: [ [
 692       IDENT "include" ; path = QSTRING ->
 693         loc,path,LexiconAst.WithPreferences
 694     | IDENT "include'" ; path = QSTRING ->
 695         loc,path,LexiconAst.WithoutPreferences
 696    ]];
 697
 698   grafite_command: [ [
 699       IDENT "set"; n = QSTRING; v = QSTRING ->
 700         GrafiteAst.Set (loc, n, v)
 701     | IDENT "drop" -> GrafiteAst.Drop loc
 702     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 703     | IDENT "qed" -> GrafiteAst.Qed loc
 704     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 705       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 706         GrafiteAst.Obj (loc,
 707           Ast.Theorem
 708             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 709     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 710       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 711         GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
 712     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 713       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 714         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 715     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 716       body = term ->
 717         GrafiteAst.Obj (loc,
 718           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 719     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 720         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 721     | LETCOREC ; defs = let_defs ->
 722         mk_rec_corec `CoInductive defs loc
 723     | LETREC ; defs = let_defs ->
 724         mk_rec_corec `Inductive defs loc
 725     | IDENT "inductive"; spec = inductive_spec ->
 726         let (params, ind_types) = spec in
 727         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 728     | IDENT "coinductive"; spec = inductive_spec ->
 729         let (params, ind_types) = spec in
 730         let ind_types = (* set inductive flags to false (coinductive) *)
 731           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 732             ind_types
 733         in
 734         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 735     | IDENT "coercion" ;
 736       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 737       arity = OPT int ; saturations = OPT int;
 738       composites = OPT (IDENT "nocomposites") ->
 739         let arity = match arity with None -> 0 | Some x -> x in
 740         let saturations = match saturations with None -> 0 | Some x -> x in
 741         let composites = match composites with None -> true | Some _ -> false in
 742         GrafiteAst.Coercion
 743          (loc, t, composites, arity, saturations)
 744     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 745         GrafiteAst.PreferCoercion (loc, t)
 746     | IDENT "pump" ; steps = int ->
 747         GrafiteAst.Pump(loc,steps)
 748     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 749         GrafiteAst.UnificationHint (loc, t, n)
 750     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 751         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 752     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 753        let uris = List.map UriManager.uri_of_string uris in
 754         GrafiteAst.Default (loc,what,uris)
 755     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 756       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 757                    refl = tactic_term -> refl ] ;
 758       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 759                    sym = tactic_term -> sym ] ;
 760       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 761                    trans = tactic_term -> trans ] ;
 762       "as" ; id = IDENT ->
 763        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 764   ]];
 765   lexicon_command: [ [
 766       IDENT "alias" ; spec = alias_spec ->
 767         LexiconAst.Alias (loc, spec)
 768     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 769         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 770     | IDENT "interpretation"; id = QSTRING;
 771       (symbol, args, l3) = interpretation ->
 772         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 773   ]];
 774   executable: [
 775     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 776     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 777         GrafiteAst.Tactic (loc, Some tac, punct)
 778     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 779     | tac = ntactic; punct = punctuation_tactical ->
 780         GrafiteAst.NTactic (loc, tac, punct)
 781     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 782         GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
 783     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 784         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 785     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 786     ]
 787   ];
 788   comment: [
 789     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 790        GrafiteAst.Code (loc, ex)
 791     | str = NOTE ->
 792        GrafiteAst.Note (loc, str)
 793     ]
 794   ];
 795   statement: [
 796     [ ex = executable ->
 797        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 798     | com = comment ->
 799        fun ?(never_include=false) ~include_paths status ->
 800                status,LSome (GrafiteAst.Comment (loc, com))
 801     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 802        !out fname;
 803        fun ?(never_include=false) ~include_paths status ->
 804         let _root, buri, fullpath, _rrelpath =
 805           Librarian.baseuri_of_script ~include_paths fname
 806         in
 807         let status =
 808          if never_include then raise (NoInclusionPerformed fullpath)
 809          else LexiconEngine.eval_command status
 810                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 811         in
 812          status,
 813           LSome
 814           (GrafiteAst.Executable
 815            (loc,GrafiteAst.Command
 816             (loc,GrafiteAst.Include (iloc,buri))))
 817     | scom = lexicon_command ; SYMBOL "." ->
 818        fun ?(never_include=false) ~include_paths status ->
 819         let status = LexiconEngine.eval_command status scom in
 820          status,LNone loc
 821     | EOI -> raise End_of_file
 822     ]
 823   ];
 824 END
 825 (* }}} *)
 826 ;;
 827
 828 let _ = initialize_parser () ;;
 829
 830 let exc_located_wrapper f =
 831   try
 832     f ()
 833   with
 834   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 835   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 836       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 837   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 838       raise
 839        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 840   | Stdpp.Exc_located (floc, exn) ->
 841       raise
 842        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 843
 844 let parse_statement lexbuf =
 845   exc_located_wrapper
 846     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 847
 848 let statement () = !grafite_parser.statement
 849
 850 let history = ref [] ;;
 851
 852 let push () =
 853   LexiconSync.push ();
 854   history := !grafite_parser :: !history;
 855   grafite_parser := initial_parser ();
 856   initialize_parser ()
 857 ;;
 858
 859 let pop () =
 860   LexiconSync.pop ();
 861   match !history with
 862   | [] -> assert false
 863   | gp :: tail ->
 864       grafite_parser := gp;
 865       history := tail
 866 ;;
 867
 868 (* vim:set foldmethod=marker: *)
 869
 870