src/Pure/Isar/constdefs.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18668 4a15c09bd46a
child 18765 97911ffe9222
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/constdefs.ML
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     4
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     5
Standard constant definitions, with type-inference and optional
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     6
structure context; specifications need to observe strictly sequential
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     7
dependencies; no support for overloading.
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     8
*)
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
     9
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    10
signature CONSTDEFS =
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    11
sig
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    12
  val add_constdefs: (string * string option) list *
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    13
    ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    14
    theory -> theory
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    15
  val add_constdefs_i: (string * typ option) list *
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18668
diff changeset
    16
    ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    17
    theory -> theory
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    18
end;
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    19
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    20
structure Constdefs: CONSTDEFS =
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    21
struct
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    22
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    23
(** add_constdefs(_i) **)
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    24
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    25
fun gen_constdef prep_vars prep_term prep_att
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    26
    structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    27
  let
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    28
    fun err msg ts =
17065
c1cd17010a1b replaced sign by thy;
wenzelm
parents: 15979
diff changeset
    29
      error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    30
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    31
    val (_, ctxt) = thy |> ProofContext.init |> ProofContext.add_fixes_i structs;
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    32
    val ((d, mx), ctxt') =
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    33
      (case raw_decl of
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    34
        NONE => ((NONE, NoSyn), ctxt)
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    35
      | SOME raw_var =>
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    36
          ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    37
            ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    38
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    39
    val prop = prep_term ctxt' raw_prop;
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    40
    val concl = Logic.strip_imp_concl prop;
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    41
    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    42
      err "Not a meta-equality (==):" [concl];
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    43
    val head = Term.head_of lhs;
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    44
    val (c, T) = Term.dest_Free head handle TERM _ =>
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    45
      err "Locally fixed variable required as head of definition:" [head];
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15010
diff changeset
    46
    val _ = (case d of NONE => () | SOME c' =>
14719
d1157ff6ffcb be liberal about constant names;
wenzelm
parents: 14664
diff changeset
    47
      if c <> c' then
d1157ff6ffcb be liberal about constant names;
wenzelm
parents: 14664
diff changeset
    48
        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    49
      else ());
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    50
17065
c1cd17010a1b replaced sign by thy;
wenzelm
parents: 15979
diff changeset
    51
    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    52
    val name = if raw_name = "" then Thm.def_name c else raw_name;
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    53
    val atts = map (prep_att thy) raw_atts;
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    54
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    55
    val thy' =
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    56
      thy
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    57
      |> Theory.add_consts_i [(c, T, mx)]
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    58
      |> PureThy.add_defs_i false [((name, def), atts)] |> snd;
17853
wenzelm
parents: 17065
diff changeset
    59
  in ((c, T), thy') end;
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    60
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    61
fun gen_constdefs prep_vars prep_term prep_att (raw_structs, specs) thy =
14664
148f6175fa78 improved messages;
wenzelm
parents: 14657
diff changeset
    62
  let
18638
e135f6a1b76c Specification.pretty_consts ctxt;
wenzelm
parents: 18615
diff changeset
    63
    val ctxt = ProofContext.init thy;
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    64
    val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    65
    val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
18638
e135f6a1b76c Specification.pretty_consts ctxt;
wenzelm
parents: 18615
diff changeset
    66
  in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    67
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    68
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18668
diff changeset
    69
  ProofContext.read_term_legacy Attrib.attribute;
18668
4a15c09bd46a uniform handling of fixes;
wenzelm
parents: 18638
diff changeset
    70
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
14657
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    71
c7cc01735801 'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff changeset
    72
end;