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