--- a/src/HOL/Library/EfficientNat.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Tue Sep 19 15:22:05 2006 +0200
@@ -126,8 +126,8 @@
unfolding nat_less_def by simp
lemma [code func, code inline]: "(m <= n) = nat_less_equal m n"
unfolding nat_less_equal_def by simp
-lemma [code func, code inline]: "(m = n) = nat_eq m n"
- unfolding nat_eq_def by simp
+lemma [code func, code inline]: "OperationalEquality.eq m n = nat_eq m n"
+ unfolding nat_eq_def eq_def by simp
lemma [code func]:
"int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))"
unfolding nat_eq_def nat_minus_def int_aux_def by simp
@@ -273,8 +273,8 @@
setup {*
Codegen.add_preprocessor eqn_suc_preproc
#> Codegen.add_preprocessor clause_suc_preproc
- #> CodegenTheorems.add_preproc (lift_obj_eq eqn_suc_preproc)
- #> CodegenTheorems.add_preproc (lift_obj_eq clause_suc_preproc)
+ #> CodegenData.add_preproc (lift_obj_eq eqn_suc_preproc)
+ #> CodegenData.add_preproc (lift_obj_eq clause_suc_preproc)
*}
(*>*)
--- a/src/HOL/Library/ExecutableRat.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy Tue Sep 19 15:22:05 2006 +0200
@@ -48,8 +48,8 @@
to_rat :: "erat \<Rightarrow> rat"
to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
if a then Fract p q else Fract (uminus p) q)"
- eq_rat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
- "eq_rat r s = (norm r = norm s)"
+ eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
+ "eq_erat r s = (norm r = norm s)"
defs (overloaded)
zero_rat_def: "0 == Rat True 0 1"
@@ -117,7 +117,7 @@
"op * :: erat \<Rightarrow> erat \<Rightarrow> erat"
"inverse :: erat \<Rightarrow> erat"
"op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
- eq_rat
+ eq_erat
(SML) (Haskell)
code_const Fract
@@ -156,8 +156,12 @@
(SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
(Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
-code_const "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
- (SML "{*eq_rat*}")
- (Haskell "{*eq_rat*}")
+instance rat :: eq ..
+
+code_const "OperationalEquality.eq :: rat \<Rightarrow> rat \<Rightarrow> bool"
+ (SML "{*eq_erat*}")
+ (Haskell "{*eq_erat*}")
+
+code_gen (SML -)
end
--- a/src/HOL/Library/ExecutableSet.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy Tue Sep 19 15:22:05 2006 +0200
@@ -9,14 +9,21 @@
imports Main
begin
-section {* Definitional rewrites *}
+section {* Definitional equality rewrites *}
+
+instance set :: (eq) eq ..
lemma [code target: Set]:
"(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
by blast
+lemma [code func]:
+ "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
+ unfolding eq_def by blast
+
declare bex_triv_one_point1 [symmetric, standard, code]
+
section {* HOL definitions *}
subsection {* Basic definitions *}
@@ -24,9 +31,9 @@
definition
flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
"flip f a b = f b a"
- member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ member :: "'a list \<Rightarrow> 'a\<Colon>eq \<Rightarrow> bool"
"member xs x = (x \<in> set xs)"
- insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ insertl :: "'a\<Colon>eq\<Rightarrow> 'a list \<Rightarrow> 'a list"
"insertl x xs = (if member xs x then xs else x#xs)"
lemma
@@ -44,6 +51,7 @@
declare drop_first.simps [code target: List]
declare remove1.simps [code del]
+ML {* reset CodegenData.strict_functyp *}
lemma [code target: List]:
"remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
proof (cases "member xs x")
@@ -53,6 +61,7 @@
have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
with True show ?thesis by simp
qed
+ML {* set CodegenData.strict_functyp *}
lemma member_nil [simp]:
"member [] = (\<lambda>x. False)"
@@ -84,8 +93,7 @@
subsection {* Derived definitions *}
-
-function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function unionl :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"unionl [] ys = ys"
| "unionl xs ys = foldr insertl xs ys"
@@ -94,7 +102,7 @@
lemmas unionl_def = unionl.simps(2)
declare unionl.simps[code]
-function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function intersect :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"intersect [] ys = []"
| "intersect xs [] = []"
@@ -104,7 +112,7 @@
lemmas intersect_def = intersect.simps(3)
declare intersect.simps[code]
-function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function subtract :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"subtract [] ys = ys"
| "subtract xs [] = []"
@@ -114,7 +122,7 @@
lemmas subtract_def = subtract.simps(3)
declare subtract.simps[code]
-function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+function map_distinct :: "('a \<Rightarrow> 'b\<Colon>eq) \<Rightarrow> 'a list \<Rightarrow> 'b list"
where
"map_distinct f [] = []"
| "map_distinct f xs = foldr (insertl o f) xs []"
@@ -123,7 +131,7 @@
lemmas map_distinct_def = map_distinct.simps(2)
declare map_distinct.simps[code]
-function unions :: "'a list list \<Rightarrow> 'a list"
+function unions :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
where
"unions [] = []"
"unions xs = foldr unionl xs []"
@@ -132,14 +140,14 @@
lemmas unions_def = unions.simps(2)
declare unions.simps[code]
-consts intersects :: "'a list list \<Rightarrow> 'a list"
+consts intersects :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
primrec
"intersects (x#xs) = foldr intersect xs x"
definition
- map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
+ map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
"map_union xs f = unions (map f xs)"
- map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
+ map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
"map_inter xs f = intersects (map f xs)"
@@ -266,11 +274,6 @@
"ExecutableSet.insertl" "List.insertl"
"ExecutableSet.drop_first" "List.drop_first"
-code_gen
- insertl unionl intersect flip subtract map_distinct
- unions intersects map_union map_inter Blall Blex
- (SML) (Haskell)
-
code_const "{}"
(SML target_atom "[]")
(Haskell target_atom "[]")
@@ -319,4 +322,6 @@
(SML "{*Blex*}")
(Haskell "{*Blex*}")
+code_gen (SML -) (SML _)
+
end
--- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 19 15:22:05 2006 +0200
@@ -8,9 +8,11 @@
signature DATATYPE_CODEGEN =
sig
val get_eq: theory -> string -> thm list
- val get_datatype_spec_thms: theory -> string
- -> (((string * sort) list * (string * typ list) list) * tactic) option
- val datatype_tac: theory -> string -> tactic
+ val get_eq_datatype: theory -> string -> thm list
+ val get_eq_typecopy: theory -> string -> thm list
+ val get_cert: theory -> bool * string -> thm list
+ val get_cert_datatype: theory -> string -> thm list
+ val get_cert_typecopy: theory -> string -> thm list
val dest_case_expr: theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
val add_datatype_case_const: string -> theory -> theory
@@ -18,6 +20,8 @@
type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
-> theory -> theory
+ val codetype_hook: hook
+ val eq_hook: hook
val codetypes_dependency: theory -> (string * bool) list list
val add_codetypes_hook_bootstrap: hook -> theory -> theory
val the_codetypes_mut_specs: theory -> (string * bool) list
@@ -26,9 +30,10 @@
-> (string * (((string * sort list) * sort) * term list)) list option
val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
-> (theory -> ((string * sort list) * sort) list -> (string * term list) list
- -> ((bstring * attribute list) * term) list) -> theory -> theory
+ -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
val setup: theory -> theory
+ val setup2: theory -> theory
end;
structure DatatypeCodegen : DATATYPE_CODEGEN =
@@ -370,26 +375,20 @@
in map mk_dist (sym_product cos) end;
local
- val not_sym = thm "HOL.not_sym";
+ val bool_eq_implies = thm "iffD1";
+ val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
+ val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-in fun get_eq thy dtco =
+ val not_eq_quodlibet = thm "not_eq_quodlibet";
+in fun get_cert_datatype thy dtco =
let
val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
- fun mk_triv_inject co =
- let
- val ct' = Thm.cterm_of thy
- (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
- val cty' = Thm.ctyp_of_term ct';
- val refl = Thm.prop_of HOL.refl;
- val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
- (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
- refl NONE;
- in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
- val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
- val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
+ val inject = (#inject o DatatypePackage.the_datatype thy) dtco
+ |> map (fn thm => bool_eq_implies OF [thm] )
+ |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
val ctxt = Context.init_proof thy;
val simpset = Simplifier.context ctxt
- (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+ (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
val cos = map (fn (co, tys) =>
(Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
val tac = ALLGOALS (simp_tac simpset)
@@ -397,30 +396,19 @@
val distinct =
mk_distinct cos
|> map (fn t => Goal.prove_global thy [] [] t (K tac))
- |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
- in inject1 @ inject2 @ distinct end;
+ |> map (fn thm => not_eq_quodlibet OF [thm])
+ in inject @ distinct end
+and get_cert_typecopy thy dtco =
+ let
+ val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
+ val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
+ in
+ [thm]
+ end;
end (*local*);
-fun datatype_tac thy dtco =
- let
- val ctxt = Context.init_proof thy;
- val inject = (#inject o DatatypePackage.the_datatype thy) dtco;
- val simpset = Simplifier.context ctxt
- (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
- in
- (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
- THEN (
- (ALLGOALS o match_tac) (eqTrueI :: inject)
- ORELSE (ALLGOALS o simp_tac) simpset
- )
- THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
- end;
-
-fun get_datatype_spec_thms thy dtco =
- case DatatypePackage.get_datatype_spec thy dtco
- of SOME vs_cos =>
- SOME (vs_cos, datatype_tac thy dtco)
- | NONE => NONE;
+fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
+ | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
fun add_datatype_case_const dtco thy =
let
@@ -433,7 +421,7 @@
let
val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
in
- fold CodegenTheorems.add_fun case_rewrites thy
+ fold_rev CodegenData.add_func case_rewrites thy
end;
@@ -536,7 +524,7 @@
) else NONE
end;
-fun prove_codetypes_arities tac tycos sort f thy =
+fun prove_codetypes_arities tac tycos sort f after_qed thy =
case get_codetypes_arities thy tycos sort
of NONE => thy
| SOME insts => let
@@ -548,20 +536,128 @@
then NONE else SOME (arity, (tyco, cs)))) insts;
in
thy
- |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
- arities ("", []) (f thy arities css)
+ |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
+ arities ("", []) (f thy arities css) #> after_qed)
end;
+local
+ val class_eq = "OperationalEquality.eq";
+in fun add_eq_instance specs =
+ prove_codetypes_arities
+ (K (ClassPackage.intro_classes_tac []))
+ (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+ [class_eq] ((K o K o K) [])
+end; (*local*)
+
+local
+ val not_sym = thm "HOL.not_sym";
+ val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+in fun get_eq_datatype thy dtco =
+ let
+ val _ = writeln "01";
+ val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
+ val _ = writeln "02";
+ fun mk_triv_inject co =
+ let
+ val ct' = Thm.cterm_of (Context.check_thy thy)
+ (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
+ val cty' = Thm.ctyp_of_term ct';
+ val refl = Thm.prop_of HOL.refl;
+ val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
+ (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I)
+ refl NONE;
+ in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+ val _ = writeln "03";
+ val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
+ val _ = writeln "04";
+ val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
+ val _ = writeln "05";
+ val ctxt = Context.init_proof (Context.check_thy thy);
+ val _ = writeln "06";
+ val simpset = Simplifier.context ctxt
+ (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+ val _ = writeln "07";
+ val cos = map (fn (co, tys) =>
+ (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
+ val tac = ALLGOALS (simp_tac simpset)
+ THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
+ val _ = writeln "08";
+ val distinct =
+ mk_distinct cos
+ |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
+ |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
+ val _ = writeln "09";
+ in inject1 @ inject2 @ distinct end;
+
+fun get_eq_typecopy thy tyco =
+ case TypecopyPackage.get_typecopy_info thy tyco
+ of SOME { inject, ... } => [inject]
+ | NONE => [];
+
+local
+ val lift_not_thm = thm "HOL.Eq_FalseI";
+ val lift_thm = thm "HOL.eq_reflection";
+ val eq_def_sym = thm "eq_def" |> Thm.symmetric;
+ fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
+ of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
+ | NONE => case TypecopyPackage.get_typecopy_info thy tyco
+ of SOME _ => get_eq_typecopy thy tyco
+ | NONE => [];
+in
+ fun get_eq thy tyco =
+ get_eq_thms (Context.check_thy thy) tyco
+ |> tap (fn _ => writeln "10")
+ |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
+ |> tap (fn _ => writeln "11")
+ |> constrain_op_eq (Context.check_thy thy)
+ |> tap (fn _ => writeln "12")
+ |> map (Tactic.rewrite_rule [eq_def_sym])
+ |> tap (fn _ => writeln "13")
+end;
+
+end;
+
+fun add_eq_thms (dtco, (_, (vs, cs))) thy =
+ let
+ val thy_ref = Theory.self_ref thy;
+ val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
+ val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
+ val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x"));
+ in
+ CodegenData.add_funcl
+ (c, CodegenData.lazy get_thms) thy
+ end;
+
+fun codetype_hook dtcos theory =
+ let
+ fun add (dtco, (flag, spec)) thy =
+ let
+ fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
+ in
+ CodegenData.add_datatype
+ (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
+ end;
+ in
+ theory
+ |> fold add dtcos
+ end;
+
+fun eq_hook dtcos =
+ add_eq_instance dtcos (fold add_eq_thms dtcos);
+
(** theory setup **)
val setup =
- add_codegen "datatype" datatype_codegen #>
- add_tycodegen "datatype" datatype_tycodegen #>
- CodegenTheorems.add_datatype_extr
- get_datatype_spec_thms #>
- DatatypeHooks.add (fold add_datatype_case_const) #>
- DatatypeHooks.add (fold add_datatype_case_defs)
+ add_codegen "datatype" datatype_codegen
+ #> add_tycodegen "datatype" datatype_tycodegen
+ #> DatatypeHooks.add (fold add_datatype_case_const)
+ #> DatatypeHooks.add (fold add_datatype_case_defs)
+
+val setup2 =
+ add_codetypes_hook_bootstrap codetype_hook
+ #> add_codetypes_hook_bootstrap eq_hook
+
end;
--- a/src/HOL/Tools/datatype_package.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Sep 19 15:22:05 2006 +0200
@@ -308,7 +308,7 @@
(snd o PureThy.add_thmss [(("simps", simps), []),
(("", List.concat case_thms @ size_thms @
List.concat distinct @ rec_thms), [Simplifier.simp_add]),
- (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+ (("", size_thms @ rec_thms), [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
(("", List.concat inject), [iff_add]),
(("", map name_notE (List.concat distinct)), [Classical.safe_elim NONE]),
(("", weak_case_congs), [cong_att])]);
@@ -479,9 +479,10 @@
strip_abs (length dts) t, is_dependent (length dts) t))
(constrs ~~ fs);
fun count_cases (cs, (_, _, true)) = cs
- | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
- NONE => (body, [cname]) :: cs
- | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
+ | count_cases (cs, (cname, (_, body), false)) =
+ case AList.lookup (op = : term * term -> bool) cs body
+ of NONE => (body, [cname]) :: cs
+ | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs;
val cases' = sort (int_ord o Library.swap o pairself (length o snd))
(Library.foldl count_cases ([], cases));
fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
@@ -558,33 +559,42 @@
(********************* axiomatic introduction of datatypes ********************)
-fun add_and_get_axioms_atts label tnames attss ts thy =
- foldr (fn (((tname, atts), t), (thy', axs)) =>
- let
- val ([ax], thy'') =
- thy'
- |> Theory.add_path tname
- |> PureThy.add_axioms_i [((label, t), atts)];
- in (Theory.parent_path thy'', ax::axs)
- end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
+fun add_axiom label t atts thy =
+ thy
+ |> PureThy.add_axioms_i [((label, t), atts)];
+
+fun add_axioms label ts atts thy =
+ thy
+ |> PureThy.add_axiomss_i [((label, ts), atts)];
-fun add_and_get_axioms label tnames =
- add_and_get_axioms_atts label tnames (replicate (length tnames) []);
+fun add_and_get_axioms_atts label tnames ts attss =
+ fold_map (fn (tname, (atts, t)) => fn thy =>
+ thy
+ |> Theory.add_path tname
+ |> add_axiom label t atts
+ ||> Theory.parent_path
+ |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
-fun add_and_get_axiomss label tnames tss thy =
- foldr (fn ((tname, ts), (thy', axss)) =>
- let
- val ([axs], thy'') =
- thy'
- |> Theory.add_path tname
- |> PureThy.add_axiomss_i [((label, ts), [])];
- in (Theory.parent_path thy'', axs::axss)
- end) (thy, []) (tnames ~~ tss) |> swap;
+fun add_and_get_axioms label tnames ts =
+ add_and_get_axioms_atts label tnames ts (replicate (length tnames) []);
+
+fun add_and_get_axiomss label tnames tss =
+ fold_map (fn (tname, ts) => fn thy =>
+ thy
+ |> Theory.add_path tname
+ |> add_axioms label ts []
+ ||> Theory.parent_path
+ |-> (fn [ax] => pair ax)) (tnames ~~ tss);
fun specify_consts args thy =
- let val specs =
- args |> map (fn (c, T, mx) => Const (Sign.full_name thy (Syntax.const_name c mx), T));
- in thy |> Theory.add_consts_i args |> Theory.add_finals_i false specs end;
+ let
+ val specs = map (fn (c, T, mx) =>
+ Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
+ in
+ thy
+ |> Sign.add_consts_i args
+ |> Theory.add_finals_i false specs
+ end;
fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
@@ -675,10 +685,9 @@
val ((([induct], [rec_thms]), inject), thy3) =
thy2
|> Theory.add_path (space_implode "_" new_type_names)
- |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
- [case_names_induct])]
- ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
- ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
+ |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
+ ||>> add_axioms "recs" rec_axs []
+ ||> (if no_size then I else add_axioms "size" size_axs [] #> snd)
||> Theory.parent_path
||>> add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
@@ -688,7 +697,7 @@
val exhaust_ts = DatatypeProp.make_casedists descr sorts;
val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
- (map Library.single case_names_exhausts) exhaust_ts thy4;
+ exhaust_ts (map single case_names_exhausts) thy4;
val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
(DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
val (split_ts, split_asm_ts) = ListPair.unzip
@@ -924,11 +933,9 @@
Theory.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
- val sign = Theory.sign_of tmp_thy;
-
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
+ let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx)
in (case duplicates (op =) tvs of
[] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
@@ -943,12 +950,12 @@
let
fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
let
- val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
+ val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_name sign else
- Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
+ in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+ Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg =>
@@ -961,7 +968,7 @@
in
case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
+ (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx),
map DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups => error ("Duplicate constructors " ^ commas dups ^
@@ -969,9 +976,9 @@
end;
val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
- val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
+ val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
val dt_info = get_datatypes thy;
- val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
+ val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
if err then error ("Nonemptiness check failed for datatype " ^ s)
else raise exn;
--- a/src/HOL/Tools/recfun_codegen.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Sep 19 15:22:05 2006 +0200
@@ -17,7 +17,7 @@
open Codegen;
-structure CodegenData = TheoryDataFun
+structure RecCodegenData = TheoryDataFun
(struct
val name = "HOL/recfun_codegen";
type T = (thm * string option) list Symtab.table;
@@ -40,27 +40,27 @@
let
fun add thm =
if Pattern.pattern (lhs_of thm) then
- CodegenData.map
+ RecCodegenData.map
(Symtab.update_list ((fst o const_of o prop_of) thm, (thm, optmod)))
else tap (fn _ => warn thm)
handle TERM _ => tap (fn _ => warn thm);
in
add thm
- #> CodegenTheorems.add_fun thm
+ #> CodegenData.add_func thm
end);
fun del_thm thm thy =
let
- val tab = CodegenData.get thy;
+ val tab = RecCodegenData.get thy;
val (s, _) = const_of (prop_of thm);
in case Symtab.lookup tab s of
NONE => thy
| SOME thms =>
- CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
+ RecCodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
end handle TERM _ => (warn thm; thy);
val del = Thm.declaration_attribute
- (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_fun thm))
+ (fn thm => Context.map_theory (del_thm thm #> CodegenData.del_func thm))
fun del_redundant thy eqs [] = eqs
| del_redundant thy eqs (eq :: eqs') =
@@ -70,7 +70,7 @@
in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
fun get_equations thy defs (s, T) =
- (case Symtab.lookup (CodegenData.get thy) s of
+ (case Symtab.lookup (RecCodegenData.get thy) s of
NONE => ([], "")
| SOME thms =>
let val thms' = del_redundant thy []
@@ -172,10 +172,10 @@
val setup =
- CodegenData.init #>
+ RecCodegenData.init #>
add_codegen "recfun" recfun_codegen #>
add_attribute ""
(Args.del |-- Scan.succeed del
- || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
+ || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> (fn name => setmp CodegenData.strict_functyp false (add name)));
end;
--- a/src/HOL/Tools/typecopy_package.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 19 15:22:05 2006 +0200
@@ -21,9 +21,6 @@
val get_typecopy_info: theory -> string -> info option
type hook = string * info -> theory -> theory;
val add_hook: hook -> theory -> theory;
- val typecopy_fun_extr: theory -> string * typ -> thm list option
- val typecopy_type_extr: theory -> string
- -> (((string * sort) list * (string * typ list) list) * tactic) option
val print: theory -> unit
val setup: theory -> theory
end;
@@ -137,27 +134,13 @@
end; (*local*)
-(* theory setup *)
-
-fun typecopy_type_extr thy tyco =
- case get_typecopy_info thy tyco
- of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]),
- (ALLGOALS o match_tac) [eq_reflection]
- THEN (ALLGOALS o match_tac) [inject])
- | NONE => NONE;
+(* hooks for projection function code *)
-fun typecopy_fun_extr thy (c, ty) =
- case (fst o strip_type) ty
- of Type (tyco, _) :: _ =>
- (case get_typecopy_info thy tyco
- of SOME { proj_def, proj as (c', _), ... } =>
- if c = c' then SOME [proj_def] else NONE
- | NONE => NONE)
- | _ => NONE;
+fun add_project (_ , { proj_def, ...} : info) =
+ CodegenData.add_func proj_def;
val setup =
TypecopyData.init
- #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr)
- #> CodegenTheorems.add_datatype_extr typecopy_type_extr;
+ #> add_hook add_project;
end; (*struct*)
--- a/src/HOL/Tools/typedef_codegen.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML Tue Sep 19 15:22:05 2006 +0200
@@ -7,12 +7,6 @@
signature TYPEDEF_CODEGEN =
sig
- val get_triv_typedef: theory -> string
- -> ((((string * sort) list * (string * typ list) list) * thm) *
- ((string * typ) * thm)) option
- val typedef_fun_extr: theory -> string * typ -> thm list option
- val typedef_type_extr: theory -> string
- -> (((string * sort) list * (string * typ list) list) * tactic) option
val setup: theory -> theory
end;
@@ -106,42 +100,8 @@
end)
| typedef_tycodegen thy defs gr dep module brack _ = NONE;
-fun get_triv_typedef thy tyco =
- case TypedefPackage.get_info thy tyco
- of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep,
- set_def = SOME def, Abs_inject = inject, Abs_inverse = inverse, ... } =>
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []
- |> rewrite_rule [symmetric def];
- in case try (op OF) (inject, [exists_thm, exists_thm])
- of SOME eq_thm =>
- SOME (((Term.add_tfreesT (Type.no_tvars ty_abs) [], [(c_abs, [ty_rep])]), eq_thm),
- ((c_rep, ty_abs --> ty_rep), inverse OF [exists_thm]))
- | NONE => NONE
- end
- | _ => NONE;
-
-fun typedef_type_extr thy tyco =
- case get_triv_typedef thy tyco
- of SOME ((vs_cs, thm), _) => SOME (vs_cs,
- (ALLGOALS o match_tac) [eq_reflection]
- THEN (ALLGOALS o match_tac) [thm])
- | NONE => NONE;
-
-fun typedef_fun_extr thy (c, ty) =
- case (fst o strip_type) ty
- of Type (tyco, _) :: _ =>
- (case get_triv_typedef thy tyco
- of SOME (_, ((c', _), thm)) => if c = c' then SOME [thm] else NONE
- | NONE => NONE)
- | _ => NONE;
-
val setup =
Codegen.add_codegen "typedef" typedef_codegen
#> Codegen.add_tycodegen "typedef" typedef_tycodegen
- #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
- #> CodegenTheorems.add_datatype_extr typedef_type_extr
end;
--- a/src/HOL/ex/Classpackage.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy Tue Sep 19 15:22:05 2006 +0200
@@ -26,7 +26,7 @@
from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
qed
-instance (type) list :: semigroup
+instance list :: (type) semigroup
"xs \<otimes> ys \<equiv> xs @ ys"
proof
fix xs ys zs :: "'a list"
@@ -52,7 +52,7 @@
from monoidl_num_def show "\<one> \<otimes> k = k" by simp
qed
-instance (type) list :: monoidl
+instance list :: (type) monoidl
"\<one> \<equiv> []"
proof
fix xs :: "'a list"
@@ -67,7 +67,7 @@
class monoid = monoidl +
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
-instance monoid_list_def: (type) list :: monoid
+instance monoid_list_def: list :: (type) monoid
proof
fix xs :: "'a list"
show "xs \<otimes> \<one> = xs"
@@ -288,26 +288,26 @@
"\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
using pow_def nat_pow_one inv_one by simp
-instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
+instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
(x1 \<otimes> y1, x2 \<otimes> y2)"
by default (simp_all add: split_paired_all semigroup_prod_def assoc)
-instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
+instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl
one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
by default (simp_all add: split_paired_all monoidl_prod_def neutl)
-instance monoid_prod_def: (monoid, monoid) * :: monoid
+instance monoid_prod_def: * :: (monoid, monoid) monoid
by default (simp_all add: split_paired_all monoid_prod_def neutr)
-instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
+instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm
by default (simp_all add: split_paired_all monoidl_prod_def comm)
-instance group_prod_def: (group, group) * :: group
+instance group_prod_def: * :: (group, group) group
inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
by default (simp_all add: split_paired_all group_prod_def invl)
-instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
+instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm
by default (simp_all add: split_paired_all group_prod_def comm)
definition
--- a/src/HOL/ex/CodeCollections.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/ex/CodeCollections.thy Tue Sep 19 15:22:05 2006 +0200
@@ -5,7 +5,7 @@
header {* Collection classes as examples for code generation *}
theory CodeCollections
-imports CodeOperationalEquality
+imports Main
begin
section {* Collection classes as examples for code generation *}
@@ -119,7 +119,7 @@
termination by (auto_term "{}")
-instance (ordered) option :: ordered
+instance option :: (ordered) ordered
"x <<= y == le_option' x y"
proof (default, unfold ordered_option_def)
fix x
@@ -149,7 +149,7 @@
"le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
termination by (auto_term "{}")
-instance (ordered, ordered) * :: ordered
+instance * :: (ordered, ordered) ordered
"x <<= y == le_pair' x y"
apply (default, unfold "ordered_*_def", unfold split_paired_all)
apply simp_all
@@ -238,11 +238,11 @@
"inf == ()"
by default (simp add: infimum_unit_def)
-instance (ordered) option :: infimum
+instance option :: (ordered) infimum
"inf == None"
by default (simp add: infimum_option_def)
-instance (infimum, infimum) * :: infimum
+instance * :: (infimum, infimum) infimum
"inf == (inf, inf)"
by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
@@ -333,7 +333,7 @@
apply (rule member_enum)+
sorry*)
-instance (enum) option :: enum
+instance option :: (enum) enum
"_4": "enum == None # map Some enum"
proof (default, unfold enum_option_def)
fix x :: "'a::enum option"
@@ -398,13 +398,11 @@
"test1 = sum [None, Some True, None, Some False]"
"test2 = (inf :: nat \<times> unit)"
-code_gen eq
code_gen "op <<="
code_gen "op <<"
code_gen inf
code_gen between
code_gen index
-code_gen sum
code_gen test1
code_gen test2
--- a/src/HOL/ex/CodeEval.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy Tue Sep 19 15:22:05 2006 +0200
@@ -13,7 +13,7 @@
subsection {* The typ_of class *}
class typ_of =
- fixes typ_of :: "'a option \<Rightarrow> typ"
+ fixes typ_of :: "'a itself \<Rightarrow> typ"
ML {*
structure TypOf =
@@ -22,17 +22,15 @@
local
val thy = the_context ();
val const_typ_of = Sign.intern_const thy "typ_of";
- val const_None = Sign.intern_const thy "None";
- fun typ_option ty = Type (Sign.intern_type (the_context ()) "option", [ty]);
- fun term_typ_of ty = Const (const_typ_of, typ_option ty --> Embed.typ_typ);
+ fun term_typ_of ty = Const (const_typ_of, Term.itselfT ty --> Embed.typ_typ);
in
val class_typ_of = Sign.intern_class thy "typ_of";
- fun term_typ_of_None ty =
- term_typ_of ty $ Const (const_None, typ_option ty);
+ fun term_typ_of_type ty =
+ term_typ_of ty $ Logic.mk_type ty;
fun mk_typ_of_def ty =
let
- val lhs = term_typ_of ty $ Free ("x", typ_option ty)
- val rhs = Embed.term_typ (fn v => term_typ_of_None (TFree v)) ty
+ val lhs = term_typ_of ty $ Free ("x", Term.itselfT ty)
+ val rhs = Embed.term_typ (fn v => term_typ_of_type (TFree v)) ty
in Logic.mk_equals (lhs, rhs) end;
end;
@@ -41,14 +39,15 @@
setup {*
let
- fun mk _ arities _ =
+ fun mk thy arities _ =
maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
- (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities;
+ (Type (tyco, map TFree (Name.names Name.context "'a" asorts)))
+ |> tap (writeln o Sign.string_of_term thy))]) arities;
fun tac _ = ClassPackage.intro_classes_tac [];
fun hook specs =
DatatypeCodegen.prove_codetypes_arities tac
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [TypOf.class_typ_of] mk
+ [TypOf.class_typ_of] mk I
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
@@ -56,7 +55,7 @@
subsection {* term_of class *}
class term_of = typ_of +
- constrains typ_of :: "'a option \<Rightarrow> typ"
+ constrains typ_of :: "'a itself \<Rightarrow> typ"
fixes term_of :: "'a \<Rightarrow> term"
ML {*
@@ -77,7 +76,7 @@
val lhs : term = term_term_of dty $ c;
val rhs : term = Embed.term_term
(fn (v, ty) => term_term_of ty $ Free (v, ty))
- (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_None (TFree (v, sort)))) c
+ (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
in
HOLogic.mk_eq (lhs, rhs)
end;
@@ -103,7 +102,7 @@
else
DatatypeCodegen.prove_codetypes_arities tac
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [TermOf.class_term_of] mk
+ [TermOf.class_term_of] mk I
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
@@ -116,10 +115,9 @@
ML {*
signature EVAL =
sig
- val eval_term: term -> theory -> term * theory
- val eval_term' : theory -> term -> term
+ val eval_term: theory -> term -> term
val term: string -> unit
- val eval_ref: term ref
+ val eval_ref: term option ref
val oracle: string * (theory * exn -> term)
val method: Method.src -> Proof.context -> Method.method
end;
@@ -127,30 +125,24 @@
structure Eval : EVAL =
struct
-val eval_ref = ref Logic.protectC;
-
-fun eval_term t =
- CodegenPackage.eval_term
- (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
+val eval_ref = ref NONE;
-fun eval_term' thy t =
- let
- val thy' = Theory.copy thy;
- val (t', _) = eval_term t thy';
- in t' end;
+fun eval_term thy t =
+ CodegenPackage.eval_term
+ thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
fun term t =
let
val thy = the_context ();
- val t' = eval_term' thy (Sign.read_term thy t);
- in () end;
+ val t = eval_term thy (Sign.read_term thy t);
+ in (writeln o Sign.string_of_term thy) t end;
val lift_eq_Trueprop = thm "lift_eq_Trueprop";
exception Eval of term;
val oracle = ("Eval", fn (thy, Eval t) =>
- Logic.mk_equals (t, eval_term' thy t));
+ Logic.mk_equals (t, eval_term thy t));
val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
@@ -194,8 +186,6 @@
and ('a, 'b) cair =
Cair 'a 'b
-code_gen term_of
-
ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
lemma
@@ -207,4 +197,4 @@
lemma
"fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
-end
+end
\ No newline at end of file
--- a/src/HOL/ex/Codegenerator.thy Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy Tue Sep 19 15:22:05 2006 +0200
@@ -27,8 +27,6 @@
definition
swap :: "'a * 'b \<Rightarrow> 'b * 'a"
"swap p = (let (x, y) = p in (y, x))"
- swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
- "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
"appl p = (let (f, x) = p in f x)"
@@ -91,8 +89,14 @@
h "Mymod.A.B.f"
code_gen xor
-code_gen one "0::nat" "1::nat"
-code_gen "0::int" "1::int" n fac
+code_gen one
+code_gen "0::int" "1::int"
+ (SML) (Haskell)
+code_gen n
+ (SML) (Haskell)
+code_gen fac
+ (SML) (Haskell)
+code_gen n
(SML) (Haskell)
code_gen
"op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -101,7 +105,9 @@
"op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
"op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
code_gen
- Pair fst snd Let split swap swapp appl
+ Pair fst snd Let split swap
+code_gen
+ appl
code_gen
k
"op + :: int \<Rightarrow> int \<Rightarrow> int"
@@ -122,43 +128,31 @@
code_gen
mut1 mut2
code_gen
- "op @" filter concat foldl foldr hd tl
- last butlast list_all2
- map
- nth
- list_update
- take
- drop
- takeWhile
- dropWhile
- rev
- zip
- upt
- remdups
remove1
null
- "distinct"
replicate
rotate1
rotate
splice
- (SML) (Haskell)
+code_gen
+ remdups
+ "distinct"
code_gen
foo1 foo3
code_gen
- "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
- "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
- "op = :: int \<Rightarrow> int \<Rightarrow> bool"
- "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
- "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
- "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
- "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- "op = :: point \<Rightarrow> point \<Rightarrow> bool"
- "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
- "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
+ "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
+ "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
+ "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
+ "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+ "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
+ "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
+ "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
+ "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
+ "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
code_gen
f g h
-code_gen (SML -)
+code_gen (SML -) (SML _)
end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Sep 19 15:22:05 2006 +0200
@@ -6,7 +6,6 @@
no_document time_use_thy "Classpackage";
no_document time_use_thy "Codegenerator";
-no_document time_use_thy "CodeOperationalEquality";
no_document time_use_thy "CodeCollections";
no_document time_use_thy "CodeEval";
no_document time_use_thy "CodeRandom";
--- a/src/Pure/IsaMakefile Tue Sep 19 15:22:03 2006 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 19 15:22:05 2006 +0200
@@ -59,9 +59,9 @@
Tools/am_interpreter.ML Tools/am_util.ML \
Tools/codegen_consts.ML \
Tools/codegen_names.ML \
- Tools/class_package.ML \
+ Tools/class_package.ML Tools/codegen_data.ML \
Tools/codegen_package.ML Tools/codegen_serializer.ML \
- Tools/codegen_theorems.ML Tools/codegen_simtype.ML \
+ Tools/codegen_funcgr.ML Tools/codegen_simtype.ML \
Tools/codegen_thingol.ML Tools/compute.ML \
Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \
assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML \