--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 29 09:57:10 2010 +0200
@@ -521,11 +521,10 @@
val is_bind = is_const @{const_name bind};
val is_return = is_const @{const_name return};
val dummy_name = "";
- val dummy_type = ITyVar dummy_name;
val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
- val unitt = case lookup_const naming @{const_name Unity}
- of SOME unit' => IConst (unit', (([], []), []))
+ val (unitt, unitT) = case lookup_const naming @{const_name Unity}
+ of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
@@ -546,7 +545,7 @@
then tr_bind' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
- fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
+ fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
[(unitt, tr_bind' ts)]), dummy_case_term)
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Thu Jul 29 09:57:10 2010 +0200
@@ -14,6 +14,6 @@
Array.upd, Array.map_entry, Array.swap, Array.freeze,
ref, Ref.lookup, Ref.update, Ref.change)"
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jul 29 09:57:10 2010 +0200
@@ -655,6 +655,6 @@
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 09:57:10 2010 +0200
@@ -110,6 +110,8 @@
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
(drule sym[of "List.length (Array.get h a)"], simp)
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
+
+export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
end
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 09:57:10 2010 +0200
@@ -1014,6 +1014,6 @@
ML {* @{code test_2} () *}
ML {* @{code test_3} () *}
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
end
--- a/src/Tools/Code/code_scala.ML Thu Jul 29 08:16:49 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jul 29 09:57:10 2010 +0200
@@ -79,24 +79,24 @@
val arg_typs' = if is_pat orelse
(is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
val (l, print') = case syntax_const c
- of NONE => (args_num c, fn ts => applify "(" ")"
+ of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
NOBR ((str o deresolve) c) arg_typs') ts)
- | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
+ | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
NOBR (str s) arg_typs') ts)
| SOME (Complex_const_syntax (k, print)) =>
- (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
+ (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
(ts ~~ take k function_typs))
- in if k = l then print' ts
+ in if k = l then print' fxy ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
else let
val (ts1, ts23) = chop l ts;
in
- Pretty.block (print' ts1 :: map (fn t => Pretty.block
+ Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
[str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
end end
and print_bind tyvars some_thm fxy p =
@@ -104,17 +104,19 @@
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
- fun print_match ((pat, ty), t) vars =
- vars
- |> print_bind tyvars some_thm BR pat
- |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
- str "=", print_term tyvars false some_thm vars NOBR t])
- val (all_ps, vars') = fold_map print_match binds vars;
- val (ps, p) = split_last all_ps;
- in brackify_block fxy
- (str "{")
- (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
- (str "}")
+ fun print_match ((IVar NONE, _), t) vars =
+ ((true, print_term tyvars false some_thm vars NOBR t), vars)
+ | print_match ((pat, ty), t) vars =
+ vars
+ |> print_bind tyvars some_thm BR pat
+ |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
+ str "=", print_term tyvars false some_thm vars NOBR t]))
+ val (seps_ps, vars') = fold_map print_match binds vars;
+ val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
+ fun insert_seps [(_, p)] = [p]
+ | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
+ (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
+ in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}")
end
| print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
let