src/Pure/Isar/constdefs.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29579 cb520b766e00
child 30211 556d1810cdad
child 30240 5b25fee0362c
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/constdefs.ML
     2     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     3 
     4 Old-style constant definitions, with type-inference and optional
     5 structure context; specifications need to observe strictly sequential
     6 dependencies; no support for overloading.
     7 *)
     8 
     9 signature CONSTDEFS =
    10 sig
    11   val add_constdefs: (binding * string option) list *
    12     ((binding * string option * mixfix) option *
    13       (Attrib.binding * string)) list -> theory -> theory
    14   val add_constdefs_i: (binding * typ option) list *
    15     ((binding * typ option * mixfix) option *
    16       ((binding * attribute list) * term)) list -> theory -> theory
    17 end;
    18 
    19 structure Constdefs: CONSTDEFS =
    20 struct
    21 
    22 (** add_constdefs(_i) **)
    23 
    24 fun gen_constdef prep_vars prep_prop prep_att
    25     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
    26   let
    27     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
    28 
    29     val thy_ctxt = ProofContext.init thy;
    30     val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
    31     val ((d, mx), var_ctxt) =
    32       (case raw_decl of
    33         NONE => ((NONE, NoSyn), struct_ctxt)
    34       | SOME raw_var =>
    35           struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
    36             ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    37 
    38     val prop = prep_prop var_ctxt raw_prop;
    39     val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    40     val _ =
    41       (case Option.map Binding.base_name d of
    42         NONE => ()
    43       | SOME c' =>
    44           if c <> c' then
    45             err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
    46           else ());
    47 
    48     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
    49     val name = Thm.def_name_optional c (Binding.base_name raw_name);
    50     val atts = map (prep_att thy) raw_atts;
    51 
    52     val thy' =
    53       thy
    54       |> Sign.add_consts_i [(c, T, mx)]
    55       |> PureThy.add_defs false [((Binding.name name, def), atts)]
    56       |-> (fn [thm] => Code.add_default_eqn thm);
    57   in ((c, T), thy') end;
    58 
    59 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    60   let
    61     val ctxt = ProofContext.init thy;
    62     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
    63     val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
    64   in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
    65 
    66 val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
    67 val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
    68 
    69 end;