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       | IDENT "comments" -> G.IPComments
 470       | IDENT "coercions" -> G.IPCoercions
 471       | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
 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