(*  Title:      Pure/Isar/constdefs.ML

     ID:         $Id$

     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)

 Standard constant definitions, with type-inference and optional

 structure context; specifications need to observe strictly sequential

 dependencies; no support for overloading.

 *)

 signature CONSTDEFS =

 sig

   val add_constdefs: (string list * string option) list *

     ((bstring * string option * Syntax.mixfix) option *

       ((bstring * Attrib.src list) * string)) list

     -> theory -> theory

   val add_constdefs_i: (string list * typ option) list *

     ((bstring * typ option * Syntax.mixfix) option *

       ((bstring * theory attribute list) * term)) list

     -> theory -> theory

 end;

 structure Constdefs: CONSTDEFS =

 struct

 (** add_constdefs(_i) **)

 fun pretty_const sg (c, T) =

   Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,

     Pretty.quote (Sign.pretty_typ sg T)];

 fun pretty_constdefs sg decls =

   Pretty.big_list "constants" (map (pretty_const sg) decls);

 fun gen_constdef prep_typ prep_term prep_att

     structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =

   let

     val sign = Theory.sign_of thy;

     fun err msg ts =

       error (cat_lines (msg :: map (Sign.string_of_term sign) ts));

     val ctxt =

       ProofContext.init thy |> ProofContext.add_fixes

         (List.concat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs));

     val (ctxt', d, mx) =

       (case decl of NONE => (ctxt, NONE, Syntax.NoSyn) | SOME (x, raw_T, mx) =>

         let

           val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx;

           val T = Option.map (prep_typ ctxt) raw_T;

         in (ProofContext.add_fixes_liberal [(x', T, SOME mx')] ctxt, SOME x', mx') end);

     val prop = prep_term ctxt' raw_prop;

     val concl = Logic.strip_imp_concl prop;

     val (lhs, _) = Logic.dest_equals concl handle TERM _ =>

       err "Not a meta-equality (==):" [concl];

     val head = Term.head_of lhs;

     val (c, T) = Term.dest_Free head handle TERM _ =>

       err "Locally fixed variable required as head of definition:" [head];

     val _ = (case d of NONE => () | SOME c' =>

       if c <> c' then

         err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []

       else ());

     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;

     val name = if raw_name = "" then Thm.def_name c else raw_name;

     val atts = map (prep_att thy) raw_atts;

     val thy' =

       thy

       |> Theory.add_consts_i [(c, T, mx)]

       |> PureThy.add_defs_i false [((name, def), atts)] |> #1;

   in (thy', (c, T)) end;

 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =

   let

     val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));

     val (thy', decls) = (thy, specs)

       |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);

   in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;

 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal

   ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;

 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal

   ProofContext.cert_typ ProofContext.cert_term (K I);

 end;