src/Pure/Isar/constdefs.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 20885 e0223c1bd7e8
child 22710 f44439cdce77
permissions -rw-r--r--
Attrib.internal: morphism;
wenzelm@14657
     1
(*  Title:      Pure/Isar/constdefs.ML
wenzelm@14657
     2
    ID:         $Id$
wenzelm@14657
     3
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14657
     4
wenzelm@18779
     5
Old-style constant definitions, with type-inference and optional
wenzelm@14657
     6
structure context; specifications need to observe strictly sequential
wenzelm@14657
     7
dependencies; no support for overloading.
wenzelm@14657
     8
*)
wenzelm@14657
     9
wenzelm@14657
    10
signature CONSTDEFS =
wenzelm@14657
    11
sig
wenzelm@18668
    12
  val add_constdefs: (string * string option) list *
wenzelm@18668
    13
    ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
wenzelm@18668
    14
    theory -> theory
wenzelm@18668
    15
  val add_constdefs_i: (string * typ option) list *
wenzelm@18728
    16
    ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
wenzelm@18668
    17
    theory -> theory
wenzelm@14657
    18
end;
wenzelm@14657
    19
wenzelm@14657
    20
structure Constdefs: CONSTDEFS =
wenzelm@14657
    21
struct
wenzelm@14657
    22
wenzelm@14657
    23
(** add_constdefs(_i) **)
wenzelm@14657
    24
wenzelm@18668
    25
fun gen_constdef prep_vars prep_term prep_att
wenzelm@18668
    26
    structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
wenzelm@14657
    27
  let
wenzelm@18948
    28
    fun err msg ts = error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
wenzelm@14664
    29
wenzelm@18948
    30
    val thy_ctxt = ProofContext.init thy;
wenzelm@18948
    31
    val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
wenzelm@18948
    32
    val ((d, mx), var_ctxt) =
wenzelm@18668
    33
      (case raw_decl of
wenzelm@18948
    34
        NONE => ((NONE, NoSyn), struct_ctxt)
wenzelm@18668
    35
      | SOME raw_var =>
wenzelm@18948
    36
          struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
wenzelm@18668
    37
            ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
wenzelm@14657
    38
wenzelm@18948
    39
    val prop = prep_term var_ctxt raw_prop;
wenzelm@18948
    40
    val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
skalberg@15531
    41
    val _ = (case d of NONE => () | SOME c' =>
wenzelm@14719
    42
      if c <> c' then
wenzelm@14719
    43
        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
wenzelm@14664
    44
      else ());
wenzelm@14657
    45
wenzelm@17065
    46
    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
wenzelm@20885
    47
    val name = Thm.def_name_optional c raw_name;
wenzelm@14657
    48
    val atts = map (prep_att thy) raw_atts;
wenzelm@14664
    49
wenzelm@14664
    50
    val thy' =
wenzelm@14664
    51
      thy
wenzelm@14664
    52
      |> Theory.add_consts_i [(c, T, mx)]
wenzelm@18668
    53
      |> PureThy.add_defs_i false [((name, def), atts)] |> snd;
wenzelm@17853
    54
  in ((c, T), thy') end;
wenzelm@14657
    55
wenzelm@18668
    56
fun gen_constdefs prep_vars prep_term prep_att (raw_structs, specs) thy =
wenzelm@14664
    57
  let
wenzelm@18638
    58
    val ctxt = ProofContext.init thy;
wenzelm@18668
    59
    val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
wenzelm@18668
    60
    val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
wenzelm@20885
    61
  in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
wenzelm@14657
    62
wenzelm@18668
    63
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
wenzelm@18728
    64
  ProofContext.read_term_legacy Attrib.attribute;
wenzelm@18668
    65
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
wenzelm@14657
    66
wenzelm@14657
    67
end;