# HG changeset patch # User haftmann # Date 1266833420 -3600 # Node ID 4f4d5bf4ea08dc4b82983d8a68a606276644fff9 # Parent 4f6760122b2aba1978f528fb3bd914abeaf67ebc proper distinction of code datatypes and abstypes diff -r 4f6760122b2a -r 4f4d5bf4ea08 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Mon Feb 22 10:28:49 2010 +0100 +++ b/src/HOL/Code_Evaluation.thy Mon Feb 22 11:10:20 2010 +0100 @@ -76,7 +76,8 @@ andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; in if need_inst then add_term_of tyco raw_vs thy else thy end; in - Code.type_interpretation ensure_term_of + Code.datatype_interpretation ensure_term_of + #> Code.abstype_interpretation ensure_term_of end *} @@ -114,7 +115,7 @@ val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; in - Code.type_interpretation ensure_term_of_code + Code.datatype_interpretation ensure_term_of_code end *} diff -r 4f6760122b2a -r 4f4d5bf4ea08 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Mon Feb 22 10:28:49 2010 +0100 +++ b/src/HOL/Typerep.thy Mon Feb 22 11:10:20 2010 +0100 @@ -70,7 +70,8 @@ add_typerep @{type_name fun} #> Typedef.interpretation ensure_typerep -#> Code.type_interpretation (ensure_typerep o fst) +#> Code.datatype_interpretation (ensure_typerep o fst) +#> Code.abstype_interpretation (ensure_typerep o fst) end *} diff -r 4f6760122b2a -r 4f4d5bf4ea08 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Feb 22 10:28:49 2010 +0100 +++ b/src/Pure/Isar/code.ML Mon Feb 22 11:10:20 2010 +0100 @@ -49,10 +49,13 @@ val add_signature_cmd: string * string -> theory -> theory val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory + val datatype_interpretation: + (string * ((string * sort) list * (string * typ list) list) + -> theory -> theory) -> theory -> theory val add_abstype: string * typ -> string * typ -> theory -> Proof.state val add_abstype_cmd: string -> string -> theory -> Proof.state - val type_interpretation: - (string * ((string * sort) list * (string * typ list) list) + val abstype_interpretation: + (string * ((string * sort) list * ((string * typ) * (string * thm))) -> theory -> theory) -> theory -> theory val add_eqn: thm -> theory -> theory val add_nbe_eqn: thm -> theory -> theory @@ -63,8 +66,8 @@ val del_eqns: string -> theory -> theory val add_case: thm -> theory -> theory val add_undefined: string -> theory -> theory - val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) - val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option + val get_type: theory -> string -> ((string * sort) list * (string * typ list) list) + val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option val is_constr: theory -> string -> bool val is_abstr: theory -> string -> bool val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert @@ -163,21 +166,21 @@ signatures: int Symtab.table * typ Symtab.table, functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table (*with explicit history*), - datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table + types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table (*with explicit history*), cases: (int * (int * string list)) Symtab.table * unit Symtab.table }; -fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) = +fun make_spec (history_concluded, ((signatures, functions), (types, cases))) = Spec { history_concluded = history_concluded, - signatures = signatures, functions = functions, datatypes = datatypes, cases = cases }; + signatures = signatures, functions = functions, types = types, cases = cases }; fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures, - functions = functions, datatypes = datatypes, cases = cases }) = - make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases)))); + functions = functions, types = types, cases = cases }) = + make_spec (f (history_concluded, ((signatures, functions), (types, cases)))); fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1, - datatypes = datatypes1, cases = (cases1, undefs1) }, + types = types1, cases = (cases1, undefs1) }, Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2, - datatypes = datatypes2, cases = (cases2, undefs2) }) = + types = types2, cases = (cases2, undefs2) }) = let val signatures = (Symtab.merge (op =) (tycos1, tycos2), Symtab.merge typ_equiv (sigs1, sigs2)); @@ -190,15 +193,15 @@ then raw_history else filtered_history; in ((false, (snd o hd) history), history) end; val functions = Symtab.join (K merge_functions) (functions1, functions2); - val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2); + val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2); val cases = (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2)); - in make_spec (false, ((signatures, functions), (datatypes, cases))) end; + in make_spec (false, ((signatures, functions), (types, cases))) end; fun history_concluded (Spec { history_concluded, ... }) = history_concluded; fun the_signatures (Spec { signatures, ... }) = signatures; fun the_functions (Spec { functions, ... }) = functions; -fun the_datatypes (Spec { datatypes, ... }) = datatypes; +fun the_types (Spec { types, ... }) = types; fun the_cases (Spec { cases, ... }) = cases; val map_history_concluded = map_spec o apfst; val map_signatures = map_spec o apsnd o apfst o apfst; @@ -423,11 +426,11 @@ $ Free ("x", ty_abs)), Free ("x", ty_abs)); in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end; -fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco) +fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco) of (_, entry) :: _ => SOME entry | _ => NONE; -fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco +fun get_type_spec thy tyco = case get_type_entry thy tyco of SOME (vs, spec) => apfst (pair vs) (constructors_of spec) | NONE => arity_number thy tyco |> Name.invents Name.context Name.aT @@ -435,23 +438,23 @@ |> rpair [] |> rpair false; -fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco +fun get_abstype_spec thy tyco = case get_type_entry thy tyco of SOME (vs, Abstractor spec) => (vs, spec) | NONE => error ("Not an abstract type: " ^ tyco); -fun get_datatype thy = fst o get_datatype_spec thy; +fun get_type thy = fst o get_type_spec thy; -fun get_datatype_of_constr_or_abstr thy c = +fun get_type_of_constr_or_abstr thy c = case (snd o strip_type o const_typ thy) c - of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco + of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end | _ => NONE; -fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c +fun is_constr thy c = case get_type_of_constr_or_abstr thy c of SOME (_, false) => true | _ => false; -fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c +fun is_abstr thy c = case get_type_of_constr_or_abstr thy c of SOME (_, true) => true | _ => false; @@ -952,7 +955,7 @@ |> Symtab.dest |> (map o apsnd) (snd o fst) |> sort (string_ord o pairself fst); - val datatypes = the_datatypes exec + val datatypes = the_types exec |> Symtab.dest |> map (fn (tyco, (_, (vs, spec)) :: _) => ((tyco, vs), constructors_of spec)) @@ -1088,15 +1091,12 @@ (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy; -(* datatypes *) +(* types *) -structure Type_Interpretation = - Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); - -fun register_datatype (tyco, vs_spec) thy = +fun register_type (tyco, vs_spec) thy = let val (old_constrs, some_old_proj) = - case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco) + case these (Symtab.lookup ((the_types o the_exec) thy) tyco) of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE) | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co) | [] => ([], NONE) @@ -1116,13 +1116,15 @@ |> map_exec_purge ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec)) #> (map_cases o apfst) drop_outdated_cases) - |> Type_Interpretation.data (tyco, serial ()) end; -fun type_interpretation f = Type_Interpretation.interpretation - (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy); +fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty); -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty); +structure Datatype_Interpretation = + Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); + +fun datatype_interpretation f = Datatype_Interpretation.interpretation + (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy); fun add_datatype proto_constrs thy = let @@ -1131,20 +1133,28 @@ in thy |> fold (del_eqns o fst) constrs - |> register_datatype (tyco, (vs, Constructors cos)) + |> register_type (tyco, (vs, Constructors cos)) + |> Datatype_Interpretation.data (tyco, serial ()) end; fun add_datatype_cmd raw_constrs thy = add_datatype (map (read_bare_const thy) raw_constrs) thy; +structure Abstype_Interpretation = + Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); + +fun abstype_interpretation f = Abstype_Interpretation.interpretation + (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy); + fun add_abstype proto_abs proto_rep thy = let val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep); val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep); fun after_qed [[cert]] = ProofContext.theory - (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) + (register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) #> change_fun_spec false rep ((K o Proj) - (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))); + (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)) + #> Abstype_Interpretation.data (tyco, serial ())); in thy |> ProofContext.init @@ -1188,7 +1198,7 @@ (mk_attribute o code_target_attr)) || Scan.succeed (mk_attribute add_warning_eqn); in - Type_Interpretation.init + Datatype_Interpretation.init #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser) "declare theorems for code generation" end)); diff -r 4f6760122b2a -r 4f4d5bf4ea08 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Mon Feb 22 10:28:49 2010 +0100 +++ b/src/Tools/Code/code_eval.ML Mon Feb 22 11:10:20 2010 +0100 @@ -130,7 +130,7 @@ val thy = ProofContext.theory_of background; val tyco = Sign.intern_type thy raw_tyco; val constrs = map (Code.check_const thy) raw_constrs; - val constrs' = (map fst o snd o Code.get_datatype thy) tyco; + val constrs' = (map fst o snd o Code.get_type thy) tyco; val _ = if eq_set (op =) (constrs, constrs') then () else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors") val is_first = is_first_occ background; diff -r 4f6760122b2a -r 4f4d5bf4ea08 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Feb 22 10:28:49 2010 +0100 +++ b/src/Tools/Code/code_thingol.ML Mon Feb 22 11:10:20 2010 +0100 @@ -256,7 +256,7 @@ | thyname :: _ => thyname; fun thyname_of_const thy c = case AxClass.class_of_param thy c of SOME class => thyname_of_class thy class - | NONE => (case Code.get_datatype_of_constr_or_abstr thy c + | NONE => (case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => Codegen.thyname_of_type thy tyco | NONE => Codegen.thyname_of_const thy c); fun purify_base "==>" = "follows" @@ -543,7 +543,7 @@ let val stmt_datatype = let - val (vs, cos) = Code.get_datatype thy tyco; + val (vs, cos) = Code.get_type thy tyco; in fold_map (translate_tyvar_sort thy algbr eqngr) vs ##>> fold_map (fn (c, tys) => @@ -569,7 +569,7 @@ ##>> fold_map (translate_eqn thy algbr eqngr) eqns #>> (fn info => Fun (c, info)) end; - val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c + val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco | NONE => (case AxClass.class_of_param thy c of SOME class => stmt_classparam class