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 "coercions" -> G.IPCoercions
 465       | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
 466       | IDENT "procedural" -> G.IPProcedural
 467       | IDENT "nodefaults" -> G.IPNoDefaults
 468       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 469       | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
 470       | IDENT "comments" -> G.IPComments
 471       | IDENT "cr" -> G.IPCR
 472       ] -> params
 473    ]
 474 ];
 475   by_continuation: [
 476     [ 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)
 477     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 478             "done" -> BYC_weproved (ty,None,t1)
 479     | "done" -> BYC_done
 480     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 481       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 482       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 483     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 484               BYC_wehaveand (id1,t1,id2,t2)
 485     ]
 486 ];
 487   rewriting_step_continuation : [
 488     [ "done" -> true
 489     | -> false
 490     ]
 491 ];
 492   atomic_tactical:
 493     [ "sequence" LEFTA
 494       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 495           let ts =
 496             match t1 with
 497             | G.Seq (_, l) -> l @ [ t2 ]
 498             | _ -> [ t1; t2 ]
 499           in
 500           G.Seq (loc, ts)
 501       ]
 502     | "then" NONA
 503       [ tac = SELF; SYMBOL ";";
 504         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 505           (G.Then (loc, tac, tacs))
 506       ]
 507     | "loops" RIGHTA
 508       [ IDENT "do"; count = int; tac = SELF ->
 509           G.Do (loc, count, tac)
 510       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 511       ]
 512     | "simple" NONA
 513       [ IDENT "first";
 514         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 515           G.First (loc, tacs)
 516       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 517       | IDENT "solve";
 518         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 519           G.Solve (loc, tacs)
 520       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 521       | LPAREN; tac = SELF; RPAREN -> tac
 522       | tac = tactic -> tac
 523         ]
 524       ];
 525   punctuation_tactical:
 526     [
 527       [ SYMBOL "[" -> G.Branch loc
 528       | SYMBOL "|" -> G.Shift loc
 529       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 530       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 531       | SYMBOL "]" -> G.Merge loc
 532       | SYMBOL ";" -> G.Semicolon loc
 533       | SYMBOL "." -> G.Dot loc
 534       ]
 535     ];
 536   non_punctuation_tactical:
 537     [ "simple" NONA
 538       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 539       | IDENT "unfocus" -> G.Unfocus loc
 540       | IDENT "skip" -> G.Skip loc
 541       ]
 542       ];
 543   ntheorem_flavour: [
 544     [ [ IDENT "ndefinition"  ] -> `Definition
 545     | [ IDENT "nfact"        ] -> `Fact
 546     | [ IDENT "nlemma"       ] -> `Lemma
 547     | [ IDENT "nremark"      ] -> `Remark
 548     | [ IDENT "ntheorem"     ] -> `Theorem
 549     ]
 550   ];
 551   theorem_flavour: [
 552     [ [ IDENT "definition"  ] -> `Definition
 553     | [ IDENT "fact"        ] -> `Fact
 554     | [ IDENT "lemma"       ] -> `Lemma
 555     | [ IDENT "remark"      ] -> `Remark
 556     | [ IDENT "theorem"     ] -> `Theorem
 557     ]
 558   ];
 559   inline_flavour: [
 560      [ attr = theorem_flavour -> attr
 561      | [ IDENT "axiom"     ]  -> `Axiom
 562      | [ IDENT "variant"   ]  -> `Variant
 563      ]
 564   ];
 565   inductive_spec: [ [
 566     fst_name = IDENT;
 567       params = LIST0 protected_binder_vars;
 568     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 569     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 570     tl = OPT [ "with";
 571         types = LIST1 [
 572           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 573          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 574             (name, true, typ, constructors) ] SEP "with" -> types
 575       ] ->
 576         let params =
 577           List.fold_right
 578             (fun (names, typ) acc ->
 579               (List.map (fun name -> (name, typ)) names) @ acc)
 580             params []
 581         in
 582         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 583         let tl_ind_types = match tl with None -> [] | Some types -> types in
 584         let ind_types = fst_ind_type :: tl_ind_types in
 585         (params, ind_types)
 586     ] ];
 587
 588     record_spec: [ [
 589       name = IDENT;
 590       params = LIST0 protected_binder_vars;
 591        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 592        fields = LIST0 [
 593          name = IDENT ;
 594          coercion = [
 595              SYMBOL ":" -> false,0
 596            | SYMBOL ":"; SYMBOL ">" -> true,0
 597            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 598          ];
 599          ty = term ->
 600            let b,n = coercion in
 601            (name,ty,b,n)
 602        ] SEP SYMBOL ";"; SYMBOL "}" ->
 603         let params =
 604           List.fold_right
 605             (fun (names, typ) acc ->
 606               (List.map (fun name -> (name, typ)) names) @ acc)
 607             params []
 608         in
 609         (params,name,typ,fields)
 610     ] ];
 611
 612     macro: [
 613       [ [ IDENT "check"   ]; t = term ->
 614           G.Check (loc, t)
 615       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 616           G.Eval (loc, kind, t)
 617       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 618            G.Inline (loc, suri, params)
 619       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 620            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 621       | IDENT "auto"; params = auto_params ->
 622           G.AutoInteractive (loc,params)
 623       | [ IDENT "whelp"; "match" ] ; t = term ->
 624           G.WMatch (loc,t)
 625       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 626           G.WInstance (loc,t)
 627       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 628           G.WLocate (loc,id)
 629       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 630           G.WElim (loc, t)
 631       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 632           G.WHint (loc,t)
 633       ]
 634     ];
 635     alias_spec: [
 636       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 637         let alpha = "[a-zA-Z]" in
 638         let num = "[0-9]+" in
 639         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 640         let decoration = "\\'" in
 641         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 642         let rex = Str.regexp ("^"^ident^"$") in
 643         if Str.string_match rex id 0 then
 644           if (try ignore (UriManager.uri_of_string uri); true
 645               with UriManager.IllFormedUri _ -> false) ||
 646              (try ignore (NReference.reference_of_string uri); true
 647               with NReference.IllFormedReference _ -> false)
 648           then
 649             L.Ident_alias (id, uri)
 650           else
 651             raise
 652              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 653         else
 654           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 655             Printf.sprintf "Not a valid identifier: %s" id)))
 656       | IDENT "symbol"; symbol = QSTRING;
 657         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 658         SYMBOL "="; dsc = QSTRING ->
 659           let instance =
 660             match instance with Some i -> i | None -> 0
 661           in
 662           L.Symbol_alias (symbol, instance, dsc)
 663       | IDENT "num";
 664         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 665         SYMBOL "="; dsc = QSTRING ->
 666           let instance =
 667             match instance with Some i -> i | None -> 0
 668           in
 669           L.Number_alias (instance, dsc)
 670       ]
 671      ];
 672     argument: [
 673       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 674         id = IDENT ->
 675           N.IdentArg (List.length l, id)
 676       ]
 677     ];
 678     associativity: [
 679       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 680       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 681       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 682       ]
 683     ];
 684     precedence: [
 685       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 686     ];
 687     notation: [
 688       [ dir = OPT direction; s = QSTRING;
 689         assoc = OPT associativity; prec = precedence;
 690         IDENT "for";
 691         p2 =
 692           [ blob = UNPARSED_AST ->
 693               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 694                 (CicNotationParser.parse_level2_ast
 695                   (Ulexing.from_utf8_string blob))
 696           | blob = UNPARSED_META ->
 697               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 698                 (CicNotationParser.parse_level2_meta
 699                   (Ulexing.from_utf8_string blob))
 700           ] ->
 701             let assoc =
 702               match assoc with
 703               | None -> default_associativity
 704               | Some assoc -> assoc
 705             in
 706             let p1 =
 707               add_raw_attribute ~text:s
 708                 (CicNotationParser.parse_level1_pattern prec
 709                   (Ulexing.from_utf8_string s))
 710             in
 711             (dir, p1, assoc, prec, p2)
 712       ]
 713     ];
 714     level3_term: [
 715       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 716       | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
 717       | IMPLICIT -> N.ImplicitPattern
 718       | id = IDENT -> N.VarPattern id
 719       | LPAREN; terms = LIST1 SELF; RPAREN ->
 720           (match terms with
 721           | [] -> assert false
 722           | [term] -> term
 723           | terms -> N.ApplPattern terms)
 724       ]
 725     ];
 726     interpretation: [
 727       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 728           (s, args, t)
 729       ]
 730     ];
 731
 732     include_command: [ [
 733         IDENT "include" ; path = QSTRING ->
 734           loc,path,true,L.WithPreferences
 735       | IDENT "include" ; IDENT "source" ; path = QSTRING ->
 736           loc,path,false,L.WithPreferences
 737       | IDENT "include'" ; path = QSTRING ->
 738           loc,path,true,L.WithoutPreferences
 739      ]];
 740
 741   grafite_command: [ [
 742       IDENT "set"; n = QSTRING; v = QSTRING ->
 743         G.Set (loc, n, v)
 744     | IDENT "drop" -> G.Drop loc
 745     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 746     | IDENT "qed" -> G.Qed loc
 747     | IDENT "nqed" -> G.NQed loc
 748     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 749       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 750         G.Obj (loc,
 751           N.Theorem
 752             (`Variant,name,typ,Some (N.Ident (newname, None))))
 753     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 754       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 755         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 756     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 757       body = term ->
 758         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
 759     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 760       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 761         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 762     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 763       body = term ->
 764         G.Obj (loc,
 765           N.Theorem (flavour, name, N.Implicit, Some body))
 766     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 767         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 768     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 769         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 770     | LETCOREC ; defs = let_defs ->
 771         mk_rec_corec false `CoInductive defs loc
 772     | LETREC ; defs = let_defs ->
 773         mk_rec_corec false `Inductive defs loc
 774     | NLETCOREC ; defs = let_defs ->
 775         mk_rec_corec true `CoInductive defs loc
 776     | NLETREC ; defs = let_defs ->
 777         mk_rec_corec true `Inductive defs loc
 778     | IDENT "inductive"; spec = inductive_spec ->
 779         let (params, ind_types) = spec in
 780         G.Obj (loc, N.Inductive (params, ind_types))
 781     | IDENT "ninductive"; spec = inductive_spec ->
 782         let (params, ind_types) = spec in
 783         G.NObj (loc, N.Inductive (params, ind_types))
 784     | IDENT "coinductive"; spec = inductive_spec ->
 785         let (params, ind_types) = spec in
 786         let ind_types = (* set inductive flags to false (coinductive) *)
 787           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 788             ind_types
 789         in
 790         G.Obj (loc, N.Inductive (params, ind_types))
 791     | IDENT "ncoinductive"; spec = inductive_spec ->
 792         let (params, ind_types) = spec in
 793         let ind_types = (* set inductive flags to false (coinductive) *)
 794           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 795             ind_types
 796         in
 797         G.NObj (loc, N.Inductive (params, ind_types))
 798     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
 799         strict = [ SYMBOL <:unicode<lt>> -> true
 800                  | SYMBOL <:unicode<leq>> -> false ];
 801         u2 = tactic_term ->
 802         let u1 =
 803           match u1 with
 804           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 805               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 806           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 807               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 808           | _ -> raise (Failure "only a sort can be constrained")
 809         in
 810         let u2 =
 811           match u2 with
 812           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
 813               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 814           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
 815               NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
 816           | _ -> raise (Failure "only a sort can be constrained")
 817         in
 818          G.NUnivConstraint (loc, strict,u1,u2)
 819     | IDENT "coercion" ;
 820       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 821       arity = OPT int ; saturations = OPT int;
 822       composites = OPT (IDENT "nocomposites") ->
 823         let arity = match arity with None -> 0 | Some x -> x in
 824         let saturations = match saturations with None -> 0 | Some x -> x in
 825         let composites = match composites with None -> true | Some _ -> false in
 826         G.Coercion
 827          (loc, t, composites, arity, saturations)
 828     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 829         G.PreferCoercion (loc, t)
 830     | IDENT "pump" ; steps = int ->
 831         G.Pump(loc,steps)
 832     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 833         G.UnificationHint (loc, t, n)
 834     | IDENT "inverter"; name = IDENT; IDENT "for";
 835         indty = tactic_term; paramspec = inverter_param_list ->
 836           G.Inverter
 837             (loc, name, indty, paramspec)
 838     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 839         G.Obj (loc, N.Record (params,name,ty,fields))
 840     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 841         G.NObj (loc, N.Record (params,name,ty,fields))
 842     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 843        let uris = List.map UriManager.uri_of_string uris in
 844         G.Default (loc,what,uris)
 845     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 846       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 847                    refl = tactic_term -> refl ] ;
 848       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 849                    sym = tactic_term -> sym ] ;
 850       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 851                    trans = tactic_term -> trans ] ;
 852       "as" ; id = IDENT ->
 853        G.Relation (loc,id,a,aeq,refl,sym,trans)
 854   ]];
 855   lexicon_command: [ [
 856       IDENT "alias" ; spec = alias_spec ->
 857         L.Alias (loc, spec)
 858     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 859         L.Notation (loc, dir, l1, assoc, prec, l2)
 860     | IDENT "interpretation"; id = QSTRING;
 861       (symbol, args, l3) = interpretation ->
 862         L.Interpretation (loc, id, (symbol, args), l3)
 863   ]];
 864   executable: [
 865     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 866     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 867         G.Tactic (loc, Some tac, punct)
 868     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 869     | tac = ntactic; punct = punctuation_tactical ->
 870         G.NTactic (loc, tac, punct)
 871     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 872         G.NTactic (loc, G.NId loc, punct)
 873     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 874         G.NonPunctuationTactical (loc, tac, punct)
 875     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
 876         G.NNonPunctuationTactical (loc, tac, punct)
 877     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 878     ]
 879   ];
 880   comment: [
 881     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 882        G.Code (loc, ex)
 883     | str = NOTE ->
 884        G.Note (loc, str)
 885     ]
 886   ];
 887   statement: [
 888     [ ex = executable ->
 889        fun ?(never_include=false) ~include_paths status ->
 890           let stm = G.Executable (loc, ex) in
 891           !grafite_callback status stm;
 892           status, LSome stm
 893     | com = comment ->
 894        fun ?(never_include=false) ~include_paths status ->
 895           let stm = G.Comment (loc, com) in
 896           !grafite_callback status stm;
 897           status, LSome stm
 898     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
 899        fun ?(never_include=false) ~include_paths status ->
 900           let stm =
 901              G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
 902           in
 903           !grafite_callback status stm;
 904           let _root, buri, fullpath, _rrelpath =
 905             Librarian.baseuri_of_script ~include_paths fname
 906           in
 907           let status =
 908             if never_include then raise (NoInclusionPerformed fullpath)
 909             else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
 910           in
 911           let stm =
 912              G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
 913           in
 914           status, LSome stm
 915     | scom = lexicon_command ; SYMBOL "." ->
 916        fun ?(never_include=false) ~include_paths status ->
 917           !lexicon_callback status scom;
 918           let status = LE.eval_command status scom in
 919           status, LNone loc
 920     | EOI -> raise End_of_file
 921     ]
 922   ];
 923 END
 924 (* }}} *)
 925 ;;
 926
 927 let _ = initialize_parser () ;;
 928
 929 let exc_located_wrapper f =
 930   try
 931     f ()
 932   with
 933   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 934   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 935       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 936   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 937       raise
 938        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 939   | Stdpp.Exc_located (floc, exn) ->
 940       raise
 941        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 942
 943 let parse_statement lexbuf =
 944   exc_located_wrapper
 945     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 946
 947 let statement () = !grafite_parser.statement
 948
 949 let history = ref [] ;;
 950
 951 let push () =
 952   LexiconSync.push ();
 953   history := !grafite_parser :: !history;
 954   grafite_parser := initial_parser ();
 955   initialize_parser ()
 956 ;;
 957
 958 let pop () =
 959   LexiconSync.pop ();
 960   match !history with
 961   | [] -> assert false
 962   | gp :: tail ->
 963       grafite_parser := gp;
 964       history := tail
 965 ;;
 966
 967 (* vim:set foldmethod=marker: *)
 968
 969