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