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