src/Pure/Isar/constdefs.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 22796 34c316d7b630
child 24219 e558fe311376
permissions -rw-r--r--
tuned Pure/General/name_space.ML
     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_prop 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_prop 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       |> Sign.add_consts_i [(c, T, mx)]
    53       |> PureThy.add_defs_i false [((name, def), atts)]
    54       |-> (fn [thm] => CodegenData.add_func false thm);
    55   in ((c, T), thy') end;
    56 
    57 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    58   let
    59     val ctxt = ProofContext.init thy;
    60     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
    61     val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
    62   in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
    63 
    64 val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
    65   ProofContext.read_prop_legacy Attrib.attribute;
    66 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_prop (K I);
    67 
    68 end;