1.1 --- a/src/HOL/Code_Evaluation.thy Mon Feb 22 10:28:49 2010 +0100
1.2 +++ b/src/HOL/Code_Evaluation.thy Mon Feb 22 11:10:20 2010 +0100
1.3 @@ -76,7 +76,8 @@
1.4 andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
1.5 in if need_inst then add_term_of tyco raw_vs thy else thy end;
1.6 in
1.7 - Code.type_interpretation ensure_term_of
1.8 + Code.datatype_interpretation ensure_term_of
1.9 + #> Code.abstype_interpretation ensure_term_of
1.10 end
1.11 *}
1.12
1.13 @@ -114,7 +115,7 @@
1.14 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
1.15 in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
1.16 in
1.17 - Code.type_interpretation ensure_term_of_code
1.18 + Code.datatype_interpretation ensure_term_of_code
1.19 end
1.20 *}
1.21
2.1 --- a/src/HOL/Typerep.thy Mon Feb 22 10:28:49 2010 +0100
2.2 +++ b/src/HOL/Typerep.thy Mon Feb 22 11:10:20 2010 +0100
2.3 @@ -70,7 +70,8 @@
2.4
2.5 add_typerep @{type_name fun}
2.6 #> Typedef.interpretation ensure_typerep
2.7 -#> Code.type_interpretation (ensure_typerep o fst)
2.8 +#> Code.datatype_interpretation (ensure_typerep o fst)
2.9 +#> Code.abstype_interpretation (ensure_typerep o fst)
2.10
2.11 end
2.12 *}
3.1 --- a/src/Pure/Isar/code.ML Mon Feb 22 10:28:49 2010 +0100
3.2 +++ b/src/Pure/Isar/code.ML Mon Feb 22 11:10:20 2010 +0100
3.3 @@ -49,10 +49,13 @@
3.4 val add_signature_cmd: string * string -> theory -> theory
3.5 val add_datatype: (string * typ) list -> theory -> theory
3.6 val add_datatype_cmd: string list -> theory -> theory
3.7 + val datatype_interpretation:
3.8 + (string * ((string * sort) list * (string * typ list) list)
3.9 + -> theory -> theory) -> theory -> theory
3.10 val add_abstype: string * typ -> string * typ -> theory -> Proof.state
3.11 val add_abstype_cmd: string -> string -> theory -> Proof.state
3.12 - val type_interpretation:
3.13 - (string * ((string * sort) list * (string * typ list) list)
3.14 + val abstype_interpretation:
3.15 + (string * ((string * sort) list * ((string * typ) * (string * thm)))
3.16 -> theory -> theory) -> theory -> theory
3.17 val add_eqn: thm -> theory -> theory
3.18 val add_nbe_eqn: thm -> theory -> theory
3.19 @@ -63,8 +66,8 @@
3.20 val del_eqns: string -> theory -> theory
3.21 val add_case: thm -> theory -> theory
3.22 val add_undefined: string -> theory -> theory
3.23 - val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
3.24 - val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option
3.25 + val get_type: theory -> string -> ((string * sort) list * (string * typ list) list)
3.26 + val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
3.27 val is_constr: theory -> string -> bool
3.28 val is_abstr: theory -> string -> bool
3.29 val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
3.30 @@ -163,21 +166,21 @@
3.31 signatures: int Symtab.table * typ Symtab.table,
3.32 functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
3.33 (*with explicit history*),
3.34 - datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
3.35 + types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
3.36 (*with explicit history*),
3.37 cases: (int * (int * string list)) Symtab.table * unit Symtab.table
3.38 };
3.39
3.40 -fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) =
3.41 +fun make_spec (history_concluded, ((signatures, functions), (types, cases))) =
3.42 Spec { history_concluded = history_concluded,
3.43 - signatures = signatures, functions = functions, datatypes = datatypes, cases = cases };
3.44 + signatures = signatures, functions = functions, types = types, cases = cases };
3.45 fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
3.46 - functions = functions, datatypes = datatypes, cases = cases }) =
3.47 - make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases))));
3.48 + functions = functions, types = types, cases = cases }) =
3.49 + make_spec (f (history_concluded, ((signatures, functions), (types, cases))));
3.50 fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1,
3.51 - datatypes = datatypes1, cases = (cases1, undefs1) },
3.52 + types = types1, cases = (cases1, undefs1) },
3.53 Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2,
3.54 - datatypes = datatypes2, cases = (cases2, undefs2) }) =
3.55 + types = types2, cases = (cases2, undefs2) }) =
3.56 let
3.57 val signatures = (Symtab.merge (op =) (tycos1, tycos2),
3.58 Symtab.merge typ_equiv (sigs1, sigs2));
3.59 @@ -190,15 +193,15 @@
3.60 then raw_history else filtered_history;
3.61 in ((false, (snd o hd) history), history) end;
3.62 val functions = Symtab.join (K merge_functions) (functions1, functions2);
3.63 - val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2);
3.64 + val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
3.65 val cases = (Symtab.merge (K true) (cases1, cases2),
3.66 Symtab.merge (K true) (undefs1, undefs2));
3.67 - in make_spec (false, ((signatures, functions), (datatypes, cases))) end;
3.68 + in make_spec (false, ((signatures, functions), (types, cases))) end;
3.69
3.70 fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
3.71 fun the_signatures (Spec { signatures, ... }) = signatures;
3.72 fun the_functions (Spec { functions, ... }) = functions;
3.73 -fun the_datatypes (Spec { datatypes, ... }) = datatypes;
3.74 +fun the_types (Spec { types, ... }) = types;
3.75 fun the_cases (Spec { cases, ... }) = cases;
3.76 val map_history_concluded = map_spec o apfst;
3.77 val map_signatures = map_spec o apsnd o apfst o apfst;
3.78 @@ -423,11 +426,11 @@
3.79 $ Free ("x", ty_abs)), Free ("x", ty_abs));
3.80 in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;
3.81
3.82 -fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
3.83 +fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
3.84 of (_, entry) :: _ => SOME entry
3.85 | _ => NONE;
3.86
3.87 -fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco
3.88 +fun get_type_spec thy tyco = case get_type_entry thy tyco
3.89 of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
3.90 | NONE => arity_number thy tyco
3.91 |> Name.invents Name.context Name.aT
3.92 @@ -435,23 +438,23 @@
3.93 |> rpair []
3.94 |> rpair false;
3.95
3.96 -fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco
3.97 +fun get_abstype_spec thy tyco = case get_type_entry thy tyco
3.98 of SOME (vs, Abstractor spec) => (vs, spec)
3.99 | NONE => error ("Not an abstract type: " ^ tyco);
3.100
3.101 -fun get_datatype thy = fst o get_datatype_spec thy;
3.102 +fun get_type thy = fst o get_type_spec thy;
3.103
3.104 -fun get_datatype_of_constr_or_abstr thy c =
3.105 +fun get_type_of_constr_or_abstr thy c =
3.106 case (snd o strip_type o const_typ thy) c
3.107 - of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco
3.108 + of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
3.109 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
3.110 | _ => NONE;
3.111
3.112 -fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c
3.113 +fun is_constr thy c = case get_type_of_constr_or_abstr thy c
3.114 of SOME (_, false) => true
3.115 | _ => false;
3.116
3.117 -fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c
3.118 +fun is_abstr thy c = case get_type_of_constr_or_abstr thy c
3.119 of SOME (_, true) => true
3.120 | _ => false;
3.121
3.122 @@ -952,7 +955,7 @@
3.123 |> Symtab.dest
3.124 |> (map o apsnd) (snd o fst)
3.125 |> sort (string_ord o pairself fst);
3.126 - val datatypes = the_datatypes exec
3.127 + val datatypes = the_types exec
3.128 |> Symtab.dest
3.129 |> map (fn (tyco, (_, (vs, spec)) :: _) =>
3.130 ((tyco, vs), constructors_of spec))
3.131 @@ -1088,15 +1091,12 @@
3.132 (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
3.133
3.134
3.135 -(* datatypes *)
3.136 +(* types *)
3.137
3.138 -structure Type_Interpretation =
3.139 - Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
3.140 -
3.141 -fun register_datatype (tyco, vs_spec) thy =
3.142 +fun register_type (tyco, vs_spec) thy =
3.143 let
3.144 val (old_constrs, some_old_proj) =
3.145 - case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
3.146 + case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
3.147 of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
3.148 | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
3.149 | [] => ([], NONE)
3.150 @@ -1116,13 +1116,15 @@
3.151 |> map_exec_purge
3.152 ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
3.153 #> (map_cases o apfst) drop_outdated_cases)
3.154 - |> Type_Interpretation.data (tyco, serial ())
3.155 end;
3.156
3.157 -fun type_interpretation f = Type_Interpretation.interpretation
3.158 - (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
3.159 +fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
3.160
3.161 -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
3.162 +structure Datatype_Interpretation =
3.163 + Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
3.164 +
3.165 +fun datatype_interpretation f = Datatype_Interpretation.interpretation
3.166 + (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy);
3.167
3.168 fun add_datatype proto_constrs thy =
3.169 let
3.170 @@ -1131,20 +1133,28 @@
3.171 in
3.172 thy
3.173 |> fold (del_eqns o fst) constrs
3.174 - |> register_datatype (tyco, (vs, Constructors cos))
3.175 + |> register_type (tyco, (vs, Constructors cos))
3.176 + |> Datatype_Interpretation.data (tyco, serial ())
3.177 end;
3.178
3.179 fun add_datatype_cmd raw_constrs thy =
3.180 add_datatype (map (read_bare_const thy) raw_constrs) thy;
3.181
3.182 +structure Abstype_Interpretation =
3.183 + Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
3.184 +
3.185 +fun abstype_interpretation f = Abstype_Interpretation.interpretation
3.186 + (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
3.187 +
3.188 fun add_abstype proto_abs proto_rep thy =
3.189 let
3.190 val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
3.191 val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
3.192 fun after_qed [[cert]] = ProofContext.theory
3.193 - (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
3.194 + (register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
3.195 #> change_fun_spec false rep ((K o Proj)
3.196 - (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)));
3.197 + (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))
3.198 + #> Abstype_Interpretation.data (tyco, serial ()));
3.199 in
3.200 thy
3.201 |> ProofContext.init
3.202 @@ -1188,7 +1198,7 @@
3.203 (mk_attribute o code_target_attr))
3.204 || Scan.succeed (mk_attribute add_warning_eqn);
3.205 in
3.206 - Type_Interpretation.init
3.207 + Datatype_Interpretation.init
3.208 #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
3.209 "declare theorems for code generation"
3.210 end));
4.1 --- a/src/Tools/Code/code_eval.ML Mon Feb 22 10:28:49 2010 +0100
4.2 +++ b/src/Tools/Code/code_eval.ML Mon Feb 22 11:10:20 2010 +0100
4.3 @@ -130,7 +130,7 @@
4.4 val thy = ProofContext.theory_of background;
4.5 val tyco = Sign.intern_type thy raw_tyco;
4.6 val constrs = map (Code.check_const thy) raw_constrs;
4.7 - val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
4.8 + val constrs' = (map fst o snd o Code.get_type thy) tyco;
4.9 val _ = if eq_set (op =) (constrs, constrs') then ()
4.10 else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
4.11 val is_first = is_first_occ background;
5.1 --- a/src/Tools/Code/code_thingol.ML Mon Feb 22 10:28:49 2010 +0100
5.2 +++ b/src/Tools/Code/code_thingol.ML Mon Feb 22 11:10:20 2010 +0100
5.3 @@ -256,7 +256,7 @@
5.4 | thyname :: _ => thyname;
5.5 fun thyname_of_const thy c = case AxClass.class_of_param thy c
5.6 of SOME class => thyname_of_class thy class
5.7 - | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
5.8 + | NONE => (case Code.get_type_of_constr_or_abstr thy c
5.9 of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
5.10 | NONE => Codegen.thyname_of_const thy c);
5.11 fun purify_base "==>" = "follows"
5.12 @@ -543,7 +543,7 @@
5.13 let
5.14 val stmt_datatype =
5.15 let
5.16 - val (vs, cos) = Code.get_datatype thy tyco;
5.17 + val (vs, cos) = Code.get_type thy tyco;
5.18 in
5.19 fold_map (translate_tyvar_sort thy algbr eqngr) vs
5.20 ##>> fold_map (fn (c, tys) =>
5.21 @@ -569,7 +569,7 @@
5.22 ##>> fold_map (translate_eqn thy algbr eqngr) eqns
5.23 #>> (fn info => Fun (c, info))
5.24 end;
5.25 - val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
5.26 + val stmt_const = case Code.get_type_of_constr_or_abstr thy c
5.27 of SOME (tyco, _) => stmt_datatypecons tyco
5.28 | NONE => (case AxClass.class_of_param thy c
5.29 of SOME class => stmt_classparam class