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