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         hyps = LIST0
 187          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 188          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 189                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 190             id,`Def (bo,ty)];
 191         SYMBOL <:unicode<vdash>>;
 192         concl = tactic_term ->
 193          GrafiteAst.NAssert (loc, hyps, concl)
 194     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 195         GrafiteAst.NCases (loc, what, where)
 196     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 197         GrafiteAst.NChange (loc, what, with_what)
 198     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 199         GrafiteAst.NElim (loc, what, where)
 200     | IDENT "ngeneralize"; p=pattern_spec ->
 201         GrafiteAst.NGeneralize (loc, p)
 202     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 203         where = pattern_spec ->
 204         GrafiteAst.NLetIn (loc,where,t,name)
 205     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 206         GrafiteAst.NRewrite (loc, dir, what, where)
 207     | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
 208       where = pattern_spec ->
 209         let delta = match delta with None -> true | _ -> false in
 210         GrafiteAst.NEval (loc, where, `Whd delta)
 211     | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
 212     | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
 213     | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
 214     | SYMBOL "*"; n=IDENT ->
 215         GrafiteAst.NCase1 (loc,n)
 216     ]
 217   ];
 218   tactic: [
 219     [ IDENT "absurd"; t = tactic_term ->
 220         GrafiteAst.Absurd (loc, t)
 221     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 222         GrafiteAst.ApplyRule (loc, t)
 223     | IDENT "apply"; t = tactic_term ->
 224         GrafiteAst.Apply (loc, t)
 225     | IDENT "applyP"; t = tactic_term ->
 226         GrafiteAst.ApplyP (loc, t)
 227     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 228         GrafiteAst.ApplyS (loc, t, params)
 229     | IDENT "assumption" ->
 230         GrafiteAst.Assumption loc
 231     | IDENT "autobatch";  params = auto_params ->
 232         GrafiteAst.AutoBatch (loc,params)
 233     | IDENT "cases"; what = tactic_term;
 234       pattern = OPT pattern_spec;
 235       specs = intros_spec ->
 236         let pattern = match pattern with
 237            | None         -> None, [], Some Ast.UserInput
 238            | Some pattern -> pattern
 239         in
 240         GrafiteAst.Cases (loc, what, pattern, specs)
 241     | IDENT "clear"; ids = LIST1 IDENT ->
 242         GrafiteAst.Clear (loc, ids)
 243     | IDENT "clearbody"; id = IDENT ->
 244         GrafiteAst.ClearBody (loc,id)
 245     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 246         GrafiteAst.Change (loc, what, t)
 247     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 248       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 249         let times = match times with None -> 1 | Some i -> i in
 250         GrafiteAst.Compose (loc, t1, t2, times, specs)
 251     | IDENT "constructor"; n = int ->
 252         GrafiteAst.Constructor (loc, n)
 253     | IDENT "contradiction" ->
 254         GrafiteAst.Contradiction loc
 255     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 256         GrafiteAst.Cut (loc, ident, t)
 257     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 258         let idents = match idents with None -> [] | Some idents -> idents in
 259         GrafiteAst.Decompose (loc, idents)
 260     | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
 261     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 262         GrafiteAst.Destruct (loc, xts)
 263     | IDENT "elim"; what = tactic_term; using = using;
 264        pattern = OPT pattern_spec;
 265        ispecs = intros_spec ->
 266         let pattern = match pattern with
 267            | None         -> None, [], Some Ast.UserInput
 268            | Some pattern -> pattern
 269         in
 270         GrafiteAst.Elim (loc, what, using, pattern, ispecs)
 271     | IDENT "elimType"; what = tactic_term; using = using;
 272       (num, idents) = intros_spec ->
 273         GrafiteAst.ElimType (loc, what, using, (num, idents))
 274     | IDENT "exact"; t = tactic_term ->
 275         GrafiteAst.Exact (loc, t)
 276     | IDENT "exists" ->
 277         GrafiteAst.Exists loc
 278     | IDENT "fail" -> GrafiteAst.Fail loc
 279     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 280         let (pt,_,_) = p in
 281           if pt <> None then
 282             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 283               ("the pattern cannot specify the term to replace, only its"
 284               ^ " paths in the hypotheses and in the conclusion")))
 285         else
 286          GrafiteAst.Fold (loc, kind, t, p)
 287     | IDENT "fourier" ->
 288         GrafiteAst.Fourier loc
 289     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 290         let idents = match idents with None -> [] | Some idents -> idents in
 291         GrafiteAst.FwdSimpl (loc, hyp, idents)
 292     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 293        GrafiteAst.Generalize (loc,p,id)
 294     | IDENT "id" -> GrafiteAst.IdTac loc
 295     | IDENT "intro"; ident = OPT IDENT ->
 296         let idents = match ident with None -> [] | Some id -> [Some id] in
 297         GrafiteAst.Intros (loc, (Some 1, idents))
 298     | IDENT "intros"; specs = intros_spec ->
 299         GrafiteAst.Intros (loc, specs)
 300     | IDENT "inversion"; t = tactic_term ->
 301         GrafiteAst.Inversion (loc, t)
 302     | IDENT "lapply";
 303       linear = OPT [ IDENT "linear" ];
 304       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 305       what = tactic_term;
 306       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 307       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 308         let linear = match linear with None -> false | Some _ -> true in
 309         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 310         GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
 311     | IDENT "left" -> GrafiteAst.Left loc
 312     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 313         GrafiteAst.LetIn (loc, t, where)
 314     | kind = reduction_kind; p = pattern_spec ->
 315         GrafiteAst.Reduce (loc, kind, p)
 316     | IDENT "reflexivity" ->
 317         GrafiteAst.Reflexivity loc
 318     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 319         GrafiteAst.Replace (loc, p, t)
 320     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 321        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 322        let (pt,_,_) = p in
 323         if pt <> None then
 324          raise
 325           (HExtlib.Localized (loc,
 326            (CicNotationParser.Parse_error
 327             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 328         else
 329          let n = match xnames with None -> [] | Some names -> names in
 330          GrafiteAst.Rewrite (loc, d, t, p, n)
 331     | IDENT "right" ->
 332         GrafiteAst.Right loc
 333     | IDENT "ring" ->
 334         GrafiteAst.Ring loc
 335     | IDENT "split" ->
 336         GrafiteAst.Split loc
 337     | IDENT "symmetry" ->
 338         GrafiteAst.Symmetry loc
 339     | IDENT "transitivity"; t = tactic_term ->
 340         GrafiteAst.Transitivity (loc, t)
 341      (* Produzioni Aggiunte *)
 342     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 343         GrafiteAst.Assume (loc, id, t)
 344     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 345       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 346                 t' = tactic_term -> t']->
 347         GrafiteAst.Suppose (loc, t, id, t1)
 348     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 349       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 350       id2 = IDENT ; RPAREN ->
 351         GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 352     | just =
 353        [ IDENT "using"; t=tactic_term -> `Term t
 354        | params = auto_params -> `Auto params] ;
 355       cont=by_continuation ->
 356        (match cont with
 357            BYC_done -> GrafiteAst.Bydone (loc, just)
 358          | BYC_weproved (ty,id,t1) ->
 359             GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
 360          | BYC_letsuchthat (id1,t1,id2,t2) ->
 361             GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
 362          | BYC_wehaveand (id1,t1,id2,t2) ->
 363             GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
 364     | 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']->
 365         GrafiteAst.We_need_to_prove (loc, t, id, t1)
 366     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 367         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
 368     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 369         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
 370     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 371         GrafiteAst.Byinduction(loc, t, id)
 372     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 373         GrafiteAst.Thesisbecomes(loc, t)
 374     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 375         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 376          GrafiteAst.Case(loc,id,params)
 377       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 378     | IDENT "conclude";
 379       termine = tactic_term;
 380       SYMBOL "=" ;
 381       t1=tactic_term ;
 382       t2 =
 383        [ IDENT "using"; t=tactic_term -> `Term t
 384        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 385        | IDENT "proof" -> `Proof
 386        | params = auto_params -> `Auto params];
 387       cont = rewriting_step_continuation ->
 388        GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 389     | IDENT "obtain" ; name = IDENT;
 390       termine = tactic_term;
 391       SYMBOL "=" ;
 392       t1=tactic_term ;
 393       t2 =
 394        [ IDENT "using"; t=tactic_term -> `Term t
 395        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 396        | IDENT "proof" -> `Proof
 397        | params = auto_params -> `Auto params];
 398       cont = rewriting_step_continuation ->
 399        GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 400     | SYMBOL "=" ;
 401       t1=tactic_term ;
 402       t2 =
 403        [ IDENT "using"; t=tactic_term -> `Term t
 404        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 405        | IDENT "proof" -> `Proof
 406        | params = auto_params -> `Auto params];
 407       cont = rewriting_step_continuation ->
 408        GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
 409   ]
 410 ];
 411   auto_fixed_param: [
 412    [ IDENT "paramodulation"
 413    | IDENT "depth"
 414    | IDENT "width"
 415    | IDENT "size"
 416    | IDENT "timeout"
 417    | IDENT "library"
 418    | IDENT "type"
 419    ]
 420 ];
 421   auto_params: [
 422    [ params =
 423       LIST0 [
 424          i = auto_fixed_param -> i,""
 425        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 426               string_of_int v | v = IDENT -> v ] -> i,v ];
 427       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 428       (match tl with Some l -> l | None -> []),
 429       params
 430    ]
 431 ];
 432   by_continuation: [
 433     [ 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)
 434     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 435             "done" -> BYC_weproved (ty,None,t1)
 436     | "done" -> BYC_done
 437     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 438       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 439       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 440     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 441               BYC_wehaveand (id1,t1,id2,t2)
 442     ]
 443 ];
 444   rewriting_step_continuation : [
 445     [ "done" -> true
 446     | -> false
 447     ]
 448 ];
 449   atomic_tactical:
 450     [ "sequence" LEFTA
 451       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 452           let ts =
 453             match t1 with
 454             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
 455             | _ -> [ t1; t2 ]
 456           in
 457           GrafiteAst.Seq (loc, ts)
 458       ]
 459     | "then" NONA
 460       [ tac = SELF; SYMBOL ";";
 461         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 462           (GrafiteAst.Then (loc, tac, tacs))
 463       ]
 464     | "loops" RIGHTA
 465       [ IDENT "do"; count = int; tac = SELF ->
 466           GrafiteAst.Do (loc, count, tac)
 467       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
 468       ]
 469     | "simple" NONA
 470       [ IDENT "first";
 471         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 472           GrafiteAst.First (loc, tacs)
 473       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
 474       | IDENT "solve";
 475         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 476           GrafiteAst.Solve (loc, tacs)
 477       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
 478       | LPAREN; tac = SELF; RPAREN -> tac
 479       | tac = tactic -> tac
 480       ]
 481     ];
 482   punctuation_tactical:
 483     [
 484       [ SYMBOL "[" -> GrafiteAst.Branch loc
 485       | SYMBOL "|" -> GrafiteAst.Shift loc
 486       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
 487       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
 488       | SYMBOL "]" -> GrafiteAst.Merge loc
 489       | SYMBOL ";" -> GrafiteAst.Semicolon loc
 490       | SYMBOL "." -> GrafiteAst.Dot loc
 491       ]
 492     ];
 493   non_punctuation_tactical:
 494     [ "simple" NONA
 495       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
 496       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
 497       | IDENT "skip" -> GrafiteAst.Skip loc
 498       ]
 499     ];
 500   ntheorem_flavour: [
 501     [ [ IDENT "ntheorem"     ] -> `Theorem
 502     ]
 503   ];
 504   theorem_flavour: [
 505     [ [ IDENT "definition"  ] -> `Definition
 506     | [ IDENT "fact"        ] -> `Fact
 507     | [ IDENT "lemma"       ] -> `Lemma
 508     | [ IDENT "remark"      ] -> `Remark
 509     | [ IDENT "theorem"     ] -> `Theorem
 510     ]
 511   ];
 512   inline_flavour: [
 513      [ attr = theorem_flavour -> attr
 514      | [ IDENT "axiom"     ]  -> `Axiom
 515      | [ IDENT "mutual"    ]  -> `MutualDefinition
 516      ]
 517   ];
 518   inductive_spec: [ [
 519     fst_name = IDENT;
 520       params = LIST0 protected_binder_vars;
 521     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 522     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 523     tl = OPT [ "with";
 524       types = LIST1 [
 525         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 526        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 527           (name, true, typ, constructors) ] SEP "with" -> types
 528     ] ->
 529       let params =
 530         List.fold_right
 531           (fun (names, typ) acc ->
 532             (List.map (fun name -> (name, typ)) names) @ acc)
 533           params []
 534       in
 535       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 536       let tl_ind_types = match tl with None -> [] | Some types -> types in
 537       let ind_types = fst_ind_type :: tl_ind_types in
 538       (params, ind_types)
 539   ] ];
 540
 541   record_spec: [ [
 542     name = IDENT;
 543     params = LIST0 protected_binder_vars;
 544      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 545      fields = LIST0 [
 546        name = IDENT ;
 547        coercion = [
 548            SYMBOL ":" -> false,0
 549          | SYMBOL ":"; SYMBOL ">" -> true,0
 550          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 551        ];
 552        ty = term ->
 553          let b,n = coercion in
 554          (name,ty,b,n)
 555      ] SEP SYMBOL ";"; SYMBOL "}" ->
 556       let params =
 557         List.fold_right
 558           (fun (names, typ) acc ->
 559             (List.map (fun name -> (name, typ)) names) @ acc)
 560           params []
 561       in
 562       (params,name,typ,fields)
 563   ] ];
 564
 565   macro: [
 566     [ [ IDENT "check"   ]; t = term ->
 567         GrafiteAst.Check (loc, t)
 568     | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 569         GrafiteAst.Eval (loc, kind, t)
 570     | [ IDENT "inline"];
 571         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 572         suri = QSTRING; prefix = OPT QSTRING;
 573         flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
 574          let style = match style with
 575             | None       -> GrafiteAst.Declarative
 576             | Some depth -> GrafiteAst.Procedural depth
 577          in
 578          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 579          GrafiteAst.Inline (loc,style,suri,prefix, flavour)
 580     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 581          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 582     | IDENT "auto"; params = auto_params ->
 583         GrafiteAst.AutoInteractive (loc,params)
 584     | [ IDENT "whelp"; "match" ] ; t = term ->
 585         GrafiteAst.WMatch (loc,t)
 586     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 587         GrafiteAst.WInstance (loc,t)
 588     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 589         GrafiteAst.WLocate (loc,id)
 590     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 591         GrafiteAst.WElim (loc, t)
 592     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 593         GrafiteAst.WHint (loc,t)
 594     ]
 595   ];
 596   alias_spec: [
 597     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 598       let alpha = "[a-zA-Z]" in
 599       let num = "[0-9]+" in
 600       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 601       let decoration = "\\'" in
 602       let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 603       let rex = Str.regexp ("^"^ident^"$") in
 604       if Str.string_match rex id 0 then
 605         if (try ignore (UriManager.uri_of_string uri); true
 606             with UriManager.IllFormedUri _ -> false)
 607         then
 608           LexiconAst.Ident_alias (id, uri)
 609         else
 610           raise
 611            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 612       else
 613         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 614           Printf.sprintf "Not a valid identifier: %s" id)))
 615     | IDENT "symbol"; symbol = QSTRING;
 616       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 617       SYMBOL "="; dsc = QSTRING ->
 618         let instance =
 619           match instance with Some i -> i | None -> 0
 620         in
 621         LexiconAst.Symbol_alias (symbol, instance, dsc)
 622     | IDENT "num";
 623       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 624       SYMBOL "="; dsc = QSTRING ->
 625         let instance =
 626           match instance with Some i -> i | None -> 0
 627         in
 628         LexiconAst.Number_alias (instance, dsc)
 629     ]
 630   ];
 631   argument: [
 632     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 633       id = IDENT ->
 634         Ast.IdentArg (List.length l, id)
 635     ]
 636   ];
 637   associativity: [
 638     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 639     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 640     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 641     ]
 642   ];
 643   precedence: [
 644     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 645   ];
 646   notation: [
 647     [ dir = OPT direction; s = QSTRING;
 648       assoc = OPT associativity; prec = precedence;
 649       IDENT "for";
 650       p2 =
 651         [ blob = UNPARSED_AST ->
 652             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 653               (CicNotationParser.parse_level2_ast
 654                 (Ulexing.from_utf8_string blob))
 655         | blob = UNPARSED_META ->
 656             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 657               (CicNotationParser.parse_level2_meta
 658                 (Ulexing.from_utf8_string blob))
 659         ] ->
 660           let assoc =
 661             match assoc with
 662             | None -> default_associativity
 663             | Some assoc -> assoc
 664           in
 665           let p1 =
 666             add_raw_attribute ~text:s
 667               (CicNotationParser.parse_level1_pattern prec
 668                 (Ulexing.from_utf8_string s))
 669           in
 670           (dir, p1, assoc, prec, p2)
 671     ]
 672   ];
 673   level3_term: [
 674     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 675     | id = IDENT -> Ast.VarPattern id
 676     | SYMBOL "_" -> Ast.ImplicitPattern
 677     | LPAREN; terms = LIST1 SELF; RPAREN ->
 678         (match terms with
 679         | [] -> assert false
 680         | [term] -> term
 681         | terms -> Ast.ApplPattern terms)
 682     ]
 683   ];
 684   interpretation: [
 685     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 686         (s, args, t)
 687     ]
 688   ];
 689
 690   include_command: [ [
 691       IDENT "include" ; path = QSTRING ->
 692         loc,path,LexiconAst.WithPreferences
 693     | IDENT "include'" ; path = QSTRING ->
 694         loc,path,LexiconAst.WithoutPreferences
 695    ]];
 696
 697   grafite_command: [ [
 698       IDENT "set"; n = QSTRING; v = QSTRING ->
 699         GrafiteAst.Set (loc, n, v)
 700     | IDENT "drop" -> GrafiteAst.Drop loc
 701     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 702     | IDENT "qed" -> GrafiteAst.Qed loc
 703     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 704       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 705         GrafiteAst.Obj (loc,
 706           Ast.Theorem
 707             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 708     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 709       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 710         GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
 711     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 712       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 713         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 714     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 715       body = term ->
 716         GrafiteAst.Obj (loc,
 717           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 718     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 719         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 720     | LETCOREC ; defs = let_defs ->
 721         mk_rec_corec `CoInductive defs loc
 722     | LETREC ; defs = let_defs ->
 723         mk_rec_corec `Inductive defs loc
 724     | IDENT "inductive"; spec = inductive_spec ->
 725         let (params, ind_types) = spec in
 726         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 727     | IDENT "coinductive"; spec = inductive_spec ->
 728         let (params, ind_types) = spec in
 729         let ind_types = (* set inductive flags to false (coinductive) *)
 730           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 731             ind_types
 732         in
 733         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 734     | IDENT "coercion" ;
 735       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 736       arity = OPT int ; saturations = OPT int;
 737       composites = OPT (IDENT "nocomposites") ->
 738         let arity = match arity with None -> 0 | Some x -> x in
 739         let saturations = match saturations with None -> 0 | Some x -> x in
 740         let composites = match composites with None -> true | Some _ -> false in
 741         GrafiteAst.Coercion
 742          (loc, t, composites, arity, saturations)
 743     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 744         GrafiteAst.PreferCoercion (loc, t)
 745     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 746         GrafiteAst.UnificationHint (loc, t, n)
 747     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 748         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 749     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 750        let uris = List.map UriManager.uri_of_string uris in
 751         GrafiteAst.Default (loc,what,uris)
 752     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 753       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 754                    refl = tactic_term -> refl ] ;
 755       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 756                    sym = tactic_term -> sym ] ;
 757       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 758                    trans = tactic_term -> trans ] ;
 759       "as" ; id = IDENT ->
 760        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 761   ]];
 762   lexicon_command: [ [
 763       IDENT "alias" ; spec = alias_spec ->
 764         LexiconAst.Alias (loc, spec)
 765     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 766         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 767     | IDENT "interpretation"; id = QSTRING;
 768       (symbol, args, l3) = interpretation ->
 769         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 770   ]];
 771   executable: [
 772     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 773     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 774         GrafiteAst.Tactic (loc, Some tac, punct)
 775     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 776     | tac = ntactic; punct = punctuation_tactical ->
 777         GrafiteAst.NTactic (loc, tac, punct)
 778     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 779         GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
 780     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 781         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 782     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 783     ]
 784   ];
 785   comment: [
 786     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 787        GrafiteAst.Code (loc, ex)
 788     | str = NOTE ->
 789        GrafiteAst.Note (loc, str)
 790     ]
 791   ];
 792   statement: [
 793     [ ex = executable ->
 794        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 795     | com = comment ->
 796        fun ?(never_include=false) ~include_paths status ->
 797                status,LSome (GrafiteAst.Comment (loc, com))
 798     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 799        !out fname;
 800        fun ?(never_include=false) ~include_paths status ->
 801         let _root, buri, fullpath, _rrelpath =
 802           Librarian.baseuri_of_script ~include_paths fname
 803         in
 804         let status =
 805          if never_include then raise (NoInclusionPerformed fullpath)
 806          else LexiconEngine.eval_command status
 807                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 808         in
 809          status,
 810           LSome
 811           (GrafiteAst.Executable
 812            (loc,GrafiteAst.Command
 813             (loc,GrafiteAst.Include (iloc,buri))))
 814     | scom = lexicon_command ; SYMBOL "." ->
 815        fun ?(never_include=false) ~include_paths status ->
 816         let status = LexiconEngine.eval_command status scom in
 817          status,LNone loc
 818     | EOI -> raise End_of_file
 819     ]
 820   ];
 821 END
 822 (* }}} *)
 823 ;;
 824
 825 let _ = initialize_parser () ;;
 826
 827 let exc_located_wrapper f =
 828   try
 829     f ()
 830   with
 831   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 832   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 833       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 834   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 835       raise
 836        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 837   | Stdpp.Exc_located (floc, exn) ->
 838       raise
 839        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 840
 841 let parse_statement lexbuf =
 842   exc_located_wrapper
 843     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 844
 845 let statement () = !grafite_parser.statement
 846
 847 let history = ref [] ;;
 848
 849 let push () =
 850   LexiconSync.push ();
 851   history := !grafite_parser :: !history;
 852   grafite_parser := initial_parser ();
 853   initialize_parser ()
 854 ;;
 855
 856 let pop () =
 857   LexiconSync.pop ();
 858   match !history with
 859   | [] -> assert false
 860   | gp :: tail ->
 861       grafite_parser := gp;
 862       history := tail
 863 ;;
 864
 865 (* vim:set foldmethod=marker: *)
 866
 867