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