# HG changeset patch # User wenzelm # Date 1268949392 -3600 # Node ID 0c71e0d72d7a6ac35136c1f2110a537a3f8da6dd # Parent 7b7ae5aa396dde63e180cbed80511d54659c3ae3 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification; diff -r 7b7ae5aa396d -r 0c71e0d72d7a src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Tue Mar 16 16:27:28 2010 +0100 +++ b/src/Pure/Isar/typedecl.ML Thu Mar 18 22:56:32 2010 +0100 @@ -6,50 +6,64 @@ signature TYPEDECL = sig - val typedecl_wrt: term list -> binding * string list * mixfix -> - local_theory -> typ * local_theory - val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory - val typedecl_global: binding * string list * mixfix -> theory -> typ * theory + val predeclare_constraints: binding * (string * sort) list * mixfix -> + local_theory -> string * local_theory + val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory + val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory end; structure Typedecl: TYPEDECL = struct -fun typedecl_wrt terms (b, vs, mx) lthy = +(* primitives *) + +fun object_logic_arity name thy = + (case Object_Logic.get_base_sort thy of + NONE => thy + | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy); + +fun basic_typedecl (b, n, mx) lthy = + let val name = Local_Theory.full_name lthy b in + lthy + |> Local_Theory.theory (Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) + |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)] + |> Local_Theory.type_alias b name + |> pair name + end; + + +(* syntactic version -- useful for internalizing additional types/terms beforehand *) + +fun predeclare_constraints (b, raw_args, mx) = + basic_typedecl (b, length raw_args, mx) ##> + fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args; + + +(* regular version -- without dependencies on type parameters of the context *) + +fun typedecl (b, raw_args, mx) lthy = let fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b)); - val _ = has_duplicates (op =) vs andalso err "Duplicate parameters"; - val name = Local_Theory.full_name lthy b; - val n = length vs; - - val args_ctxt = lthy |> fold Variable.declare_constraints terms; - val args = map (fn a => TFree (a, ProofContext.default_sort args_ctxt (a, ~1))) vs; - val T = Type (name, args); + val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters"; + val args = raw_args + |> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S)); + val T = Type (Local_Theory.full_name lthy b, map TFree args); val bad_args = #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T)) |> filter_out Term.is_TVar; val _ = not (null bad_args) andalso err ("Locally fixed type arguments " ^ - commas_quote (map (Syntax.string_of_typ args_ctxt) bad_args)); - - val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy); + commas_quote (map (Syntax.string_of_typ lthy) bad_args)); in lthy - |> Local_Theory.theory - (Sign.add_types [(b, n, NoSyn)] #> - (case base_sort of - NONE => I - | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))) - |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)] - |> Local_Theory.type_alias b name + |> basic_typedecl (b, length args, mx) + |> snd |> Variable.declare_typ T |> pair T end; -val typedecl = typedecl_wrt []; - fun typedecl_global decl = Theory_Target.init NONE #> typedecl decl