src/Pure/Isar/constdefs.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 36865 7330e4eefbd7
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
wenzelm@14657
     1
(*  Title:      Pure/Isar/constdefs.ML
wenzelm@14657
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14657
     3
wenzelm@18779
     4
Old-style constant definitions, with type-inference and optional
wenzelm@14657
     5
structure context; specifications need to observe strictly sequential
wenzelm@14657
     6
dependencies; no support for overloading.
wenzelm@14657
     7
*)
wenzelm@14657
     8
wenzelm@14657
     9
signature CONSTDEFS =
wenzelm@14657
    10
sig
haftmann@29579
    11
  val add_constdefs: (binding * string option) list *
wenzelm@30211
    12
    ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
haftmann@29579
    13
  val add_constdefs_i: (binding * typ option) list *
wenzelm@30211
    14
    ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
wenzelm@14657
    15
end;
wenzelm@14657
    16
wenzelm@14657
    17
structure Constdefs: CONSTDEFS =
wenzelm@14657
    18
struct
wenzelm@14657
    19
wenzelm@14657
    20
(** add_constdefs(_i) **)
wenzelm@14657
    21
wenzelm@22710
    22
fun gen_constdef prep_vars prep_prop prep_att
wenzelm@18668
    23
    structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
wenzelm@14657
    24
  let
wenzelm@36865
    25
    val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead";
haftmann@35691
    26
wenzelm@26939
    27
    fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
wenzelm@14664
    28
wenzelm@36610
    29
    val thy_ctxt = ProofContext.init_global thy;
wenzelm@30763
    30
    val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
wenzelm@18948
    31
    val ((d, mx), var_ctxt) =
wenzelm@18668
    32
      (case raw_decl of
wenzelm@18948
    33
        NONE => ((NONE, NoSyn), struct_ctxt)
wenzelm@18668
    34
      | SOME raw_var =>
wenzelm@18948
    35
          struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
wenzelm@30763
    36
            ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
wenzelm@14657
    37
wenzelm@22710
    38
    val prop = prep_prop var_ctxt raw_prop;
wenzelm@35624
    39
    val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
wenzelm@28083
    40
    val _ =
wenzelm@30585
    41
      (case Option.map Name.of_binding d of
wenzelm@28083
    42
        NONE => ()
wenzelm@28083
    43
      | SOME c' =>
wenzelm@28083
    44
          if c <> c' then
wenzelm@28083
    45
            err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
wenzelm@28083
    46
          else ());
wenzelm@30434
    47
    val b = Binding.name c;
wenzelm@14657
    48
wenzelm@33455
    49
    val head = Const (Sign.full_bname thy c, T);
wenzelm@33455
    50
    val def = Term.subst_atomic [(Free (c, T), head)] prop;
wenzelm@30434
    51
    val name = Thm.def_binding_optional b raw_name;
wenzelm@14657
    52
    val atts = map (prep_att thy) raw_atts;
wenzelm@14664
    53
wenzelm@14664
    54
    val thy' =
wenzelm@14664
    55
      thy
wenzelm@30434
    56
      |> Sign.add_consts_i [(b, T, mx)]
wenzelm@30344
    57
      |> PureThy.add_defs false [((name, def), atts)]
wenzelm@33455
    58
      |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
wenzelm@35845
    59
        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
bulwahn@33756
    60
        Code.add_default_eqn thm);
wenzelm@17853
    61
  in ((c, T), thy') end;
wenzelm@14657
    62
wenzelm@22710
    63
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
wenzelm@14664
    64
  let
wenzelm@36610
    65
    val ctxt = ProofContext.init_global thy;
wenzelm@18668
    66
    val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
wenzelm@22710
    67
    val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
wenzelm@33389
    68
  in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
wenzelm@14657
    69
wenzelm@25352
    70
val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
wenzelm@25352
    71
val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
wenzelm@14657
    72
wenzelm@14657
    73
end;