--- a/NEWS Mon May 30 20:58:16 2016 +0200
+++ b/NEWS Mon May 30 20:58:54 2016 +0200
@@ -104,6 +104,13 @@
*** HOL ***
+* Command 'code_reflect' accepts empty constructor lists for datatypes,
+which renders those abstract effectively.
+
+* Command 'export_code' checks given constants for abstraction violations:
+a small guarantee that given constants specify a safe interface for the
+generated code.
+
* Probability/Random_Permutations.thy contains some theory about
choosing a permutation of a set uniformly at random and folding over a
list in random order.
@@ -231,10 +238,11 @@
for polynomials over factorial rings. INCOMPATIBILITY.
* Library/Sublist.thy: added function "prefixes" and renamed
- prefixeq -> prefix
- prefix -> strict_prefix
- suffixeq -> suffix
- suffix -> strict_suffix
+ prefixeq -> prefix
+ prefix -> strict_prefix
+ suffixeq -> suffix
+ suffix -> strict_suffix
+ Added theory of longest common prefixes.
* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
--- a/src/Doc/Codegen/Evaluation.thy Mon May 30 20:58:16 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Mon May 30 20:58:54 2016 +0200
@@ -344,7 +344,7 @@
\<close>
code_reflect %quote Rat
- datatypes rat = Frct
+ datatypes rat
functions Fract
"(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
"(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
--- a/src/HOL/Code_Numeral.thy Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/Code_Numeral.thy Mon May 30 20:58:54 2016 +0200
@@ -893,9 +893,9 @@
"Nat (integer_of_natural n) = n"
by transfer simp
-lemma [code abstract]:
- "integer_of_natural (natural_of_nat n) = of_nat n"
- by simp
+lemma [code]:
+ "natural_of_nat n = natural_of_integer (integer_of_nat n)"
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (natural_of_integer k) = max 0 k"
@@ -969,7 +969,11 @@
lifting_forget natural.lifting
code_reflect Code_Numeral
- datatypes natural = _
- functions integer_of_natural natural_of_integer
+ datatypes natural
+ functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
+ "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
+ "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
+ "Divides.mod :: natural \<Rightarrow> _"
+ integer_of_natural natural_of_integer
end
--- a/src/HOL/Library/Sublist.thy Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/Library/Sublist.thy Mon May 30 20:58:54 2016 +0200
@@ -127,6 +127,10 @@
"prefix (xs\<^sub>1::'a list) ys \<Longrightarrow> prefix xs\<^sub>2 ys \<Longrightarrow> prefix xs\<^sub>1 xs\<^sub>2 \<or> prefix xs\<^sub>2 xs\<^sub>1"
unfolding prefix_def by (force simp: append_eq_append_conv2)
+lemma prefix_length_prefix:
+ "prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs"
+by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if)
+
lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
by (auto simp add: prefix_def)
@@ -226,6 +230,128 @@
by (cases ys rule: rev_cases) auto
+subsection \<open>Longest Common Prefix\<close>
+
+definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
+"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
+
+lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
+ \<exists>ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
+ (is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
+proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
+ case 0
+ have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
+ by auto
+ hence "?P L []" by(auto)
+ thus ?case ..
+next
+ case (Suc n)
+ let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs"
+ obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2)
+ by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv)
+ hence "[] \<notin> L" using Suc.hyps(2) by auto
+ show ?case
+ proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys")
+ case True
+ let ?L = "{ys. x#ys \<in> L}"
+ have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n"
+ using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"]
+ by - (rule Least_equality, fastforce+)
+ have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto
+ from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" ..
+ { fix qs
+ assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps"
+ and "\<forall>xs\<in>L. prefix qs xs"
+ hence "length (tl qs) \<le> length ps"
+ by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix)
+ hence "length qs \<le> Suc (length ps)" by auto
+ }
+ hence "?P L (x#ps)" using True IH by auto
+ thus ?thesis ..
+ next
+ case False
+ then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close>
+ by (auto) (metis list.exhaust)
+ have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close>
+ by auto (metis Cons_prefix_Cons prefix_Cons)
+ hence "?P L []" by auto
+ thus ?thesis ..
+ qed
+qed
+
+lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
+ \<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
+by(rule ex_ex1I[OF Longest_common_prefix_ex];
+ meson equals0I prefix_length_prefix prefix_order.antisym)
+
+lemma Longest_common_prefix_eq:
+ "\<lbrakk> L \<noteq> {}; \<forall>xs \<in> L. prefix ps xs;
+ \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
+ \<Longrightarrow> Longest_common_prefix L = ps"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule some1_equality[OF Longest_common_prefix_unique]) auto
+
+lemma Longest_common_prefix_prefix:
+ "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_longest:
+ "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_max_prefix:
+ "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
+by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
+ prefix_length_prefix ex_in_conv)
+
+lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
+using Longest_common_prefix_prefix prefix_Nil by blast
+
+lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
+ Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L"
+apply(rule Longest_common_prefix_eq)
+ apply(simp)
+ apply (simp add: Longest_common_prefix_prefix)
+apply simp
+by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
+ Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
+
+lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x"
+shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
+proof -
+ have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3)
+ by (auto simp: image_def)(metis hd_Cons_tl)
+ thus ?thesis
+ by (metis Longest_common_prefix_image_Cons image_is_empty assms(1))
+qed
+
+lemma Longest_common_prefix_eq_Nil:
+ "\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
+by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
+
+
+fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"longest_common_prefix (x#xs) (y#ys) =
+ (if x=y then x # longest_common_prefix xs ys else [])" |
+"longest_common_prefix _ _ = []"
+
+lemma longest_common_prefix_prefix1:
+ "prefix (longest_common_prefix xs ys) xs"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_prefix2:
+ "prefix (longest_common_prefix xs ys) ys"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_max_prefix:
+ "\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
+ \<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
+by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
+ (auto simp: prefix_Cons)
+
+
subsection \<open>Parallel lists\<close>
definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)
--- a/src/HOL/List.thy Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/List.thy Mon May 30 20:58:54 2016 +0200
@@ -1002,6 +1002,12 @@
(ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
by(cases ys) auto
+lemma longest_common_prefix:
+ "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys'
+ \<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
+by (induct xs ys rule: list_induct2')
+ (blast, blast, blast,
+ metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
@@ -1961,6 +1967,12 @@
"xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
by fastforce
+corollary longest_common_suffix:
+ "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
+ \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
+using longest_common_prefix[of "rev xs" "rev ys"]
+unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+
subsubsection \<open>@{const take} and @{const drop}\<close>
--- a/src/Tools/Code/code_ml.ML Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_ml.ML Mon May 30 20:58:54 2016 +0200
@@ -772,13 +772,18 @@
fun modify_funs stmts = single (SOME
(Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts =
- map_filter
- (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
- |> split_list
- |> apfst Code_Namespace.join_exports
- |> apsnd ML_Datas
- |> SOME
- |> single;
+ let
+ val datas = map_filter
+ (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
+ in
+ if null datas then [] (*for abstract types wrt. code_reflect*)
+ else datas
+ |> split_list
+ |> apfst Code_Namespace.join_exports
+ |> apsnd ML_Datas
+ |> SOME
+ |> single
+ end;
fun modify_class stmts =
the_single (map_filter
(fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
--- a/src/Tools/Code/code_runtime.ML Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon May 30 20:58:54 2016 +0200
@@ -375,20 +375,21 @@
fun check_datatype thy tyco some_consts =
let
- val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
- val _ = case some_consts
- of SOME consts =>
+ val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
+ val constrs = case some_consts
+ of SOME [] => []
+ | SOME consts =>
let
- val missing_constrs = subtract (op =) consts constrs;
+ val missing_constrs = subtract (op =) consts declared_constrs;
val _ = if null missing_constrs then []
else error ("Missing constructor(s) " ^ commas_quote missing_constrs
^ " for datatype " ^ quote tyco);
- val false_constrs = subtract (op =) constrs consts;
+ val false_constrs = subtract (op =) declared_constrs consts;
val _ = if null false_constrs then []
else error ("Non-constructor(s) " ^ commas_quote false_constrs
^ " for datatype " ^ quote tyco)
- in () end
- | NONE => ();
+ in consts end
+ | NONE => declared_constrs;
in (tyco, constrs) end;
fun add_eval_tyco (tyco, tyco') thy =
@@ -465,16 +466,16 @@
local
val parse_datatype =
- Parse.name --| @{keyword "="} --
+ Parse.name -- Scan.optional (@{keyword "="} |--
(((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
- || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
+ || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
in
val _ =
Outer_Syntax.command @{command_keyword code_reflect}
"enrich runtime environment with generated code"
- (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
+ (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
-- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) []
-- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)
--- a/src/Tools/Code/code_thingol.ML Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon May 30 20:58:54 2016 +0200
@@ -786,11 +786,23 @@
(* program generation *)
+fun check_abstract_constructors thy consts =
+ case filter (Code.is_abstr thy) consts of
+ [] => ()
+ | abstrs => error ("Cannot export abstract constructor(s): "
+ ^ commas (map (Code.string_of_const thy) abstrs));
+
fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
- Code_Preproc.timed "translating program" #ctxt
- (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
- (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
- { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val _ = if permissive then ()
+ else check_abstract_constructors thy consts;
+ in
+ Code_Preproc.timed "translating program" #ctxt
+ (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
+ (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
+ { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }
+ end;
fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
invoke_generation_for_consts ctxt
@@ -914,7 +926,8 @@
val thy = Proof_Context.theory_of ctxt;
fun consts_of thy' =
fold (fn (c, (_, NONE)) => cons c | _ => I)
- (#constants (Consts.dest (Sign.consts_of thy'))) [];
+ (#constants (Consts.dest (Sign.consts_of thy'))) []
+ |> filter_out (Code.is_abstr thy);
fun belongs_here thy' c = forall
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
@@ -934,8 +947,10 @@
let
val (consts, consts_permissive) =
read_const_exprs_internal ctxt const_exprs;
- val consts' = implemented_deps
- (consts_program_permissive ctxt consts_permissive);
+ val consts' =
+ consts_program_permissive ctxt consts_permissive
+ |> implemented_deps
+ |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt));
in union (op =) consts' consts end;