# Theory Code_Target_List

```chapter‹Code Generation›
text‹This chapter details the code generator setup to produce executable Scala code for our
inference technique.›

section‹Lists›
text‹Here we define some equivalent definitions which make for a faster implementation. We also
make use of the \texttt{code\_printing} statement such that native Scala implementations of common
list operations are used instead of redefining them. This allows us to use the \texttt{par}
construct such that the parallel implementations are used, which makes for an even faster
implementation.›

theory Code_Target_List
imports Main
begin

declare List.insert_def [code del]
declare member_rec [code del]

lemma [code]: "List.insert x xs = (if List.member xs x then xs else x#xs)"

declare enumerate_eq_zip [code]
declare foldr_conv_foldl [code]
declare map_filter_map_filter [code_unfold del]

(* Use the native implementations of list functions *)
definition "flatmap l f = List.maps f l"

lemma [code]: "List.maps f l = flatmap l f"

definition "map_code l f = List.map f l"
lemma [code]:"List.map f l = map_code l f"

lemma [code]: "removeAll a l = filter (λx. x ≠ a) l"
by (induct l arbitrary: a) simp_all

definition "filter_code l f = List.filter f l"

lemma [code]: "List.filter l f = filter_code f l"

definition all :: "'a list ⇒ ('a ⇒ bool) ⇒ bool" where
"all l f = list_all f l"

lemma [code]: "list_all f l = all l f"

definition ex :: "'a list ⇒ ('a ⇒ bool) ⇒ bool" where
"ex l f = list_ex f l"

lemma [code]: "list_ex f l = ex l f"

declare foldl_conv_fold[symmetric]

lemma fold_conv_foldl [code]: "fold f xs s = foldl (λx s. f s x) s xs"

lemma code_list_eq [code]:
"HOL.equal xs ys ⟷ length xs = length ys ∧ (∀(x,y) ∈ set (zip xs ys). x = y)"

definition take_map :: "nat ⇒ 'a list ⇒ 'a list" where
"take_map n l = (if length l ≤ n then l else map (λi. l ! i) [0..<n])"

lemma nth_take_map: "i < n ⟹ take_map n xs ! i = xs ! i"

lemma [code]: "take n l = take_map n l"
by (simp add: list_eq_iff_nth_eq min_def take_map_def)

fun upt_tailrec :: "nat ⇒ nat ⇒ nat list ⇒ nat list" where
"upt_tailrec i 0 l = l" |
"upt_tailrec i (Suc j) l = (if i ≤ j then upt_tailrec i j ([j]@l) else l)"

lemma upt_arbitrary_l: "(upt i j)@l = upt_tailrec i j l"
by (induct i j l rule: upt_tailrec.induct, auto)

lemma [code]: "upt i j = upt_tailrec i j []"
by (metis upt_arbitrary_l append_Nil2)

function max_sort :: "('a::linorder) list ⇒ 'a list ⇒ 'a list" where
"max_sort [] l = l" |
"max_sort (h#t) l = (let u = (h#t); m = Max (set u) in max_sort (removeAll m u) (m#l))"
using splice.cases apply blast
by auto
termination
apply (relation "measures [λ(l1, l2). length l1]")
apply simp
by (metis Max_eq_iff List.finite_set case_prod_conv length_removeAll_less list.distinct(1) measures_less set_empty)

lemma remdups_fold [code]:
"remdups l = foldr (λi l. if i ∈ set l then l else i#l) l []"
proof(induct l)
case Nil
then show ?case
by simp
next
case (Cons a l)
then show ?case
apply (simp)
apply standard
apply (metis set_remdups)
using set_remdups by fastforce
qed

code_printing
constant Cons ⇀ (Scala) "_::_"
| constant rev ⇀ (Scala) "_.par.reverse.toList"
| constant List.member ⇀ (Scala) "_.contains((_))"
| constant "List.remdups" ⇀ (Scala) "_.par.distinct.toList"
| constant "List.length" ⇀ (Scala) "Nat.Nata(_.par.length)"
| constant "zip" ⇀ (Scala) "_.par.zip((_)).toList"
| constant "flatmap" ⇀ (Scala) "_.par.flatMap((_)).toList"
| constant "List.null" ⇀ (Scala) "_.isEmpty"
| constant "map_code" ⇀ (Scala) "_.par.map((_)).toList"
| constant "filter_code" ⇀ (Scala) "_.par.filter((_)).toList"
| constant "all" ⇀ (Scala) "_.par.forall((_))"
| constant "ex" ⇀ (Scala) "_.par.exists((_))"
| constant "nth" ⇀ (Scala) "_(Code'_Numeral.integer'_of'_nat((_)).toInt)"
| constant "foldl" ⇀ (Scala) "Dirties.foldl"
| constant "hd" ⇀ (Scala) "_.head"

end
```