src/Pure/Isar/constdefs.ML
author wenzelm
Fri Apr 23 20:50:51 2004 +0200 (2004-04-23)
changeset 14664 148f6175fa78
parent 14657 c7cc01735801
child 14719 d1157ff6ffcb
permissions -rw-r--r--
improved messages;
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
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@14657
     5
wenzelm@14657
     6
Standard constant definitions, with type-inference and optional
wenzelm@14657
     7
structure context; specifications need to observe strictly sequential
wenzelm@14657
     8
dependencies; no support for overloading.
wenzelm@14657
     9
*)
wenzelm@14657
    10
wenzelm@14657
    11
signature CONSTDEFS =
wenzelm@14657
    12
sig
wenzelm@14657
    13
  val add_constdefs: (string list * string option) list *
wenzelm@14657
    14
    ((bstring * string option * Syntax.mixfix) option *
wenzelm@14657
    15
      ((bstring * Args.src list) * string)) list
wenzelm@14657
    16
    -> theory -> theory
wenzelm@14657
    17
  val add_constdefs_i: (string list * typ option) list *
wenzelm@14657
    18
    ((bstring * typ option * Syntax.mixfix) option *
wenzelm@14657
    19
      ((bstring * theory attribute list) * term)) list
wenzelm@14657
    20
    -> theory -> theory
wenzelm@14657
    21
end;
wenzelm@14657
    22
wenzelm@14657
    23
structure Constdefs: CONSTDEFS =
wenzelm@14657
    24
struct
wenzelm@14657
    25
wenzelm@14657
    26
(** add_constdefs(_i) **)
wenzelm@14657
    27
wenzelm@14664
    28
fun pretty_const sg (c, T) =
wenzelm@14664
    29
  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
wenzelm@14664
    30
    Pretty.quote (Sign.pretty_typ sg T)];
wenzelm@14664
    31
wenzelm@14664
    32
fun pretty_constdefs sg decls =
wenzelm@14664
    33
  Pretty.big_list "constants" (map (pretty_const sg) decls);
wenzelm@14664
    34
wenzelm@14657
    35
fun gen_constdef prep_typ prep_term prep_att
wenzelm@14657
    36
    structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =
wenzelm@14657
    37
  let
wenzelm@14664
    38
    val sign = Theory.sign_of thy;
wenzelm@14664
    39
    fun err msg ts =
wenzelm@14664
    40
      error (cat_lines (msg :: map (Sign.string_of_term sign) ts));
wenzelm@14664
    41
wenzelm@14657
    42
    val ctxt =
wenzelm@14657
    43
      ProofContext.init thy |> ProofContext.add_fixes
wenzelm@14657
    44
        (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs));
wenzelm@14657
    45
    val (ctxt', mx) =
wenzelm@14657
    46
      (case decl of None => (ctxt, Syntax.NoSyn) | Some (x, raw_T, mx) =>
wenzelm@14657
    47
        (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx));
wenzelm@14657
    48
wenzelm@14657
    49
    val prop = prep_term ctxt' raw_prop;
wenzelm@14664
    50
    val concl = Logic.strip_imp_concl prop;
wenzelm@14664
    51
    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
wenzelm@14664
    52
      err "Not a meta-equality (==):" [concl];
wenzelm@14664
    53
    val head = Term.head_of lhs;
wenzelm@14664
    54
    val (c, T) = Term.dest_Free head handle TERM _ =>
wenzelm@14664
    55
      err "Locally fixed variable required as head of definition:" [head];
wenzelm@14664
    56
    val _ = (case decl of None => () | Some (d, _, _) =>
wenzelm@14664
    57
      if c <> d then
wenzelm@14664
    58
        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d) []
wenzelm@14664
    59
      else ());
wenzelm@14657
    60
wenzelm@14664
    61
    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
wenzelm@14657
    62
    val name = if raw_name = "" then Thm.def_name c else raw_name;
wenzelm@14657
    63
    val atts = map (prep_att thy) raw_atts;
wenzelm@14664
    64
wenzelm@14664
    65
    val thy' =
wenzelm@14664
    66
      thy
wenzelm@14664
    67
      |> Theory.add_consts_i [(c, T, mx)]
wenzelm@14664
    68
      |> PureThy.add_defs_i false [((name, def), atts)] |> #1;
wenzelm@14664
    69
  in (thy', (c, T)) end;
wenzelm@14657
    70
wenzelm@14657
    71
fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
wenzelm@14664
    72
  let
wenzelm@14664
    73
    val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));
wenzelm@14664
    74
    val (thy', decls) = (thy, specs)
wenzelm@14664
    75
      |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
wenzelm@14664
    76
  in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
wenzelm@14657
    77
wenzelm@14657
    78
val add_constdefs = gen_constdefs ProofContext.read_vars
wenzelm@14657
    79
  ProofContext.read_typ ProofContext.read_term Attrib.global_attribute;
wenzelm@14657
    80
val add_constdefs_i = gen_constdefs ProofContext.cert_vars
wenzelm@14657
    81
  ProofContext.cert_typ ProofContext.cert_term (K I);
wenzelm@14657
    82
wenzelm@14657
    83
end;