7.1 in the Code Generation Manual *) + +class ccpo_linorder = ccpo + linorder + +lemma [code]: + "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \ bool) \ bool) P = + (\A. Complete_Partial_Order.chain (op \) A \ (\x\A. P x) \ P (Sup A))" +unfolding admissible_def by blast + +lemma [code]: + "(gfp :: ('a :: complete_linorder \ 'a) \ 'a) f = Sup {u. u \ f u}" +unfolding gfp_def by blast + +lemma [code]: + "(lfp :: ('a :: complete_linorder \ 'a) \ 'a) f = Inf {u. f u \ u}" +unfolding lfp_def by blast + +export_code _ checking Scala? + +end diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Codegenerator_Test/Generate_Pretty.thy --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri Feb 15 11:47:33 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ - -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Pervasive test of code generator using pretty literals *} - -theory Generate_Pretty -imports Candidates_Pretty -begin - -lemma [code, code del]: "nat_of_char = nat_of_char" .. -lemma [code, code del]: "char_of_nat = char_of_nat" .. - -subsection {* Check whether generated code compiles *} - -text {* - If any of the checks fails, inspect the code generated - by a corresponding @{text export_code} command. -*} - -export_code _ checking SML OCaml? Haskell? Scala - -end diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy Fri Feb 15 11:47:34 2013 +0100 @@ -0,0 +1,21 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Pervasive test of code generator *} + +theory Generate_Pretty_Char +imports + Candidates + "~~/src/HOL/Library/AList_Mapping" + "~~/src/HOL/Library/Finite_Lattice" + "~~/src/HOL/Library/Code_Char" +begin + +text {* + If any of the checks fails, inspect the code generated + by a corresponding @{text export_code} command. +*} + +export_code _ checking SML OCaml? Haskell? Scala + +end diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Codegenerator_Test/Generate_Target_Nat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Fri Feb 15 11:47:34 2013 +0100 @@ -0,0 +1,21 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Pervasive test of code generator *} + +theory Generate_Target_Nat +imports + Candidates + "~~/src/HOL/Library/AList_Mapping" + "~~/src/HOL/Library/Finite_Lattice" + "~~/src/HOL/Library/Code_Target_Numeral" +begin + +text {* + If any of the checks fails, inspect the code generated + by a corresponding @{text export_code} command. +*} + +export_code _ checking SML OCaml? Haskell? Scala + +end diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Codegenerator_Test/RBT_Set_Test.thy --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Fri Feb 15 11:47:33 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,70 +0,0 @@ -(* Title: HOL/Codegenerator_Test/RBT_Set_Test.thy - Author: Ondrej Kuncar -*) - -header {* Test of the code generator using an implementation of sets by RBT trees *} - -theory RBT_Set_Test -imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set" -begin - -(* - The following code equations have to be deleted because they use - lists to implement sets in the code generetor. -*) - -lemma [code, code del]: - "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" .. - -lemma [code, code del]: - "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. - -lemma [code, code del]: - "pred_of_set = pred_of_set" .. - -lemma [code, code del]: - "acc = acc" .. - -lemma [code, code del]: - "Cardinality.card' = Cardinality.card'" .. - -lemma [code, code del]: - "Cardinality.finite' = Cardinality.finite'" .. - -lemma [code, code del]: - "Cardinality.subset' = Cardinality.subset'" .. - -lemma [code, code del]: - "Cardinality.eq_set = Cardinality.eq_set" .. - -(* - If the code generation ends with an exception with the following message: - '"List.set" is not a constructor, on left hand side of equation: ...', - the code equation in question has to be either deleted (like many others in this file) - or implemented for RBT trees. -*) - -export_code _ checking SML OCaml? Haskell? - -(* Extra setup to make Scala happy *) -(* If the compilation fails with an error "ambiguous implicit values", - read \

7.1 in the Code Generation Manual *) - -class ccpo_linorder = ccpo + linorder - -lemma [code]: - "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \ bool) \ bool) P = - (\A. Complete_Partial_Order.chain (op \) A \ (\x\A. P x) \ P (Sup A))" -unfolding admissible_def by blast - -lemma [code]: - "(gfp :: ('a :: complete_linorder \ 'a) \ 'a) f = Sup {u. u \ f u}" -unfolding gfp_def by blast - -lemma [code]: - "(lfp :: ('a :: complete_linorder \ 'a) \ 'a) f = Inf {u. f u \ u}" -unfolding lfp_def by blast - -export_code _ checking Scala? - -end diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Library/AList_Mapping.thy --- a/src/HOL/Library/AList_Mapping.thy Fri Feb 15 11:47:33 2013 +0100 +++ b/src/HOL/Library/AList_Mapping.thy Fri Feb 15 11:47:34 2013 +0100 @@ -59,7 +59,7 @@ proof - have aux: "\a b xs. (a, b) \ set xs \ a \ fst ` set xs" by (auto simp add: image_def intro!: bexI) - show ?thesis apply transfer + show ?thesis apply transfer by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) qed diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Fri Feb 15 11:47:33 2013 +0100 +++ b/src/HOL/Library/IArray.thy Fri Feb 15 11:47:34 2013 +0100 @@ -46,6 +46,26 @@ code_const IArray (SML "Vector.fromList") +lemma [code]: +"size (as :: 'a iarray) = 0" +by (cases as) simp + +lemma [code]: +"iarray_size f as = Suc (list_size f (IArray.list_of as))" +by (cases as) simp + +lemma [code]: +"iarray_rec f as = f (IArray.list_of as)" +by (cases as) simp + +lemma [code]: +"iarray_case f as = f (IArray.list_of as)" +by (cases as) simp + +lemma [code]: +"HOL.equal as bs \ HOL.equal (IArray.list_of as) (IArray.list_of bs)" +by (cases as, cases bs) (simp add: equal) + primrec tabulate :: "integer \ (integer \ 'a) \ 'a iarray" where "tabulate (n, f) = IArray (map (f \ integer_of_nat) [0.. 'a) \ ('b \ 'd) \ ('a, 'b) mapping \ ('c, 'd) mapping" is "\f g m. (Option.map g \ m \ f)" . + subsection {* Functorial structure *} enriched_type map: map by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+ + subsection {* Derived operations *} definition ordered_keys :: "('a\linorder, 'b) mapping \ 'a list" where @@ -67,6 +69,22 @@ definition map_default :: "'a \ 'b \ ('b \ 'b) \ ('a, 'b) mapping \ ('a, 'b) mapping" where "map_default k v f m = map_entry k f (default k v m)" +instantiation mapping :: (type, type) equal +begin + +definition + "HOL.equal m1 m2 \ (\k. lookup m1 k = lookup m2 k)" + +instance proof +qed (unfold equal_mapping_def, transfer, auto) + +end + +lemma [transfer_rule]: + "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal" + by (unfold equal) transfer_prover + + subsection {* Properties *} lemma lookup_update: "lookup (update k v m) k = Some v" @@ -258,18 +276,8 @@ code_datatype empty update -instantiation mapping :: (type, type) equal -begin - -lift_definition equal_mapping :: "('a, 'b) mapping \ ('a, 'b) mapping \ bool" is "op=" . - -instance proof -qed(transfer, rule) - -end - - hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size replace default map_entry map_default tabulate bulkload map end + diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Feb 15 11:47:33 2013 +0100 +++ b/src/HOL/Library/Multiset.thy Fri Feb 15 11:47:34 2013 +0100 @@ -5,7 +5,7 @@ header {* (Finite) multisets *} theory Multiset -imports Main DAList +imports Main DAList (* FIXME too specific dependency for a generic theory *) begin subsection {* The type of multisets *} diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Library/RBT_Mapping.thy --- a/src/HOL/Library/RBT_Mapping.thy Fri Feb 15 11:47:33 2013 +0100 +++ b/src/HOL/Library/RBT_Mapping.thy Fri Feb 15 11:47:34 2013 +0100 @@ -73,7 +73,7 @@ lemma equal_Mapping [code]: "HOL.equal (Mapping t1) (Mapping t2) \ entries t1 = entries t2" -by (transfer fixing: t1 t2) (simp add: entries_lookup) + by (transfer fixing: t1 t2) (simp add: entries_lookup) lemma [code nbe]: "HOL.equal (x :: (_, _) mapping) x \ True" diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/ROOT --- a/src/HOL/ROOT Fri Feb 15 11:47:33 2013 +0100 +++ b/src/HOL/ROOT Fri Feb 15 11:47:34 2013 +0100 @@ -20,18 +20,25 @@ description {* Classical Higher-order Logic -- batteries included *} theories Library - Sublist + (*conflicting type class instantiations*) List_lexord Sublist_Order - Finite_Lattice - Code_Char Product_Lexorder Product_Order + Finite_Lattice + (*data refinements and dependent applications*) + AList_Mapping + Code_Binary_Nat + Code_Char (* Code_Prolog FIXME cf. 76965c356d2a *) Code_Real_Approx_By_Float Code_Target_Numeral - IArray + DAList + RBT_Mapping + RBT_Set + (*legacy tools*) Refute + Old_Recdef theories [condition = ISABELLE_FULL_TEST] Sum_of_Squares_Remote files "document/root.bib" "document/root.tex" @@ -148,7 +155,7 @@ session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + options [document = false, document_graph = false, browser_info = false] - theories Generate Generate_Pretty RBT_Set_Test + theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char session "HOL-Metis_Examples" in Metis_Examples = HOL + description {*