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