src/Pure/Isar/constdefs.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15570 8d8c70b41bab
child 15705 b5edb9dcec9a
permissions -rw-r--r--
*** empty log message ***
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@14657
     5
Standard 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@14657
    12
  val add_constdefs: (string list * string option) list *
wenzelm@14657
    13
    ((bstring * string option * Syntax.mixfix) option *
wenzelm@15703
    14
      ((bstring * Attrib.src list) * string)) list
wenzelm@14657
    15
    -> theory -> theory
wenzelm@14657
    16
  val add_constdefs_i: (string list * typ option) list *
wenzelm@14657
    17
    ((bstring * typ option * Syntax.mixfix) option *
wenzelm@14657
    18
      ((bstring * theory attribute list) * term)) list
wenzelm@14657
    19
    -> theory -> theory
wenzelm@14657
    20
end;
wenzelm@14657
    21
wenzelm@14657
    22
structure Constdefs: CONSTDEFS =
wenzelm@14657
    23
struct
wenzelm@14657
    24
wenzelm@14657
    25
(** add_constdefs(_i) **)
wenzelm@14657
    26
wenzelm@14664
    27
fun pretty_const sg (c, T) =
wenzelm@14664
    28
  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
wenzelm@14664
    29
    Pretty.quote (Sign.pretty_typ sg T)];
wenzelm@14664
    30
wenzelm@14664
    31
fun pretty_constdefs sg decls =
wenzelm@14664
    32
  Pretty.big_list "constants" (map (pretty_const sg) decls);
wenzelm@14664
    33
wenzelm@14657
    34
fun gen_constdef prep_typ prep_term prep_att
wenzelm@14657
    35
    structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =
wenzelm@14657
    36
  let
wenzelm@14664
    37
    val sign = Theory.sign_of thy;
wenzelm@14664
    38
    fun err msg ts =
wenzelm@14664
    39
      error (cat_lines (msg :: map (Sign.string_of_term sign) ts));
wenzelm@14664
    40
wenzelm@14657
    41
    val ctxt =
wenzelm@14657
    42
      ProofContext.init thy |> ProofContext.add_fixes
skalberg@15570
    43
        (List.concat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs));
wenzelm@14719
    44
    val (ctxt', d, mx) =
skalberg@15531
    45
      (case decl of NONE => (ctxt, NONE, Syntax.NoSyn) | SOME (x, raw_T, mx) =>
wenzelm@14719
    46
        let
wenzelm@14719
    47
          val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx;
skalberg@15570
    48
          val T = Option.map (prep_typ ctxt) raw_T;
skalberg@15531
    49
        in (ProofContext.add_fixes_liberal [(x', T, SOME mx')] ctxt, SOME x', mx') end);
wenzelm@14657
    50
wenzelm@14657
    51
    val prop = prep_term ctxt' raw_prop;
wenzelm@14664
    52
    val concl = Logic.strip_imp_concl prop;
wenzelm@14664
    53
    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
wenzelm@14664
    54
      err "Not a meta-equality (==):" [concl];
wenzelm@14664
    55
    val head = Term.head_of lhs;
wenzelm@14664
    56
    val (c, T) = Term.dest_Free head handle TERM _ =>
wenzelm@14664
    57
      err "Locally fixed variable required as head of definition:" [head];
skalberg@15531
    58
    val _ = (case d of NONE => () | SOME c' =>
wenzelm@14719
    59
      if c <> c' then
wenzelm@14719
    60
        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
wenzelm@14664
    61
      else ());
wenzelm@14657
    62
wenzelm@14664
    63
    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
wenzelm@14657
    64
    val name = if raw_name = "" then Thm.def_name c else raw_name;
wenzelm@14657
    65
    val atts = map (prep_att thy) raw_atts;
wenzelm@14664
    66
wenzelm@14664
    67
    val thy' =
wenzelm@14664
    68
      thy
wenzelm@14664
    69
      |> Theory.add_consts_i [(c, T, mx)]
wenzelm@14664
    70
      |> PureThy.add_defs_i false [((name, def), atts)] |> #1;
wenzelm@14664
    71
  in (thy', (c, T)) end;
wenzelm@14657
    72
wenzelm@14657
    73
fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
wenzelm@14664
    74
  let
wenzelm@14664
    75
    val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));
wenzelm@14664
    76
    val (thy', decls) = (thy, specs)
wenzelm@14664
    77
      |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
wenzelm@14664
    78
  in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
wenzelm@14657
    79
wenzelm@14719
    80
val add_constdefs = gen_constdefs ProofContext.read_vars_liberal
wenzelm@14719
    81
  ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;
wenzelm@14719
    82
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal
wenzelm@14657
    83
  ProofContext.cert_typ ProofContext.cert_term (K I);
wenzelm@14657
    84
wenzelm@14657
    85
end;