--- a/src/HOL/HOL.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/HOL.thy Mon Jul 19 12:17:38 2010 +0200
@@ -1928,7 +1928,7 @@
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
- (Scala "true" and "false" and "'! _"
+ (Scala "true" and "false" and "'!/ _"
and infixl 3 "&&" and infixl 1 "||"
and "!(if ((_))/ (_)/ else (_))")
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 19 12:17:38 2010 +0200
@@ -124,10 +124,10 @@
*}
definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
- crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
+ crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
lemma crelI:
- "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
+ "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
by (simp add: crel_def)
lemma crelE:
@@ -300,9 +300,9 @@
using assms by (auto simp add: crel_def bind_def split: option.split_asm)
lemma execute_bind_eq_SomeI:
- assumes "Heap_Monad.execute f h = Some (x, h')"
- and "Heap_Monad.execute (g x) h' = Some (y, h'')"
- shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
+ assumes "execute f h = Some (x, h')"
+ and "execute (g x) h' = Some (y, h'')"
+ shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
using assms by (simp add: bind_def)
lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
@@ -487,7 +487,7 @@
code_reserved Scala Heap
code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "!Heap.bind((_), (_))")
+code_const bind (Scala "bind")
code_const return (Scala "('_: Unit)/ =>/ _")
code_const Heap_Monad.raise' (Scala "!error((_))")
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Jul 19 12:17:38 2010 +0200
@@ -296,11 +296,11 @@
text {* Scala *}
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
+code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
end
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 19 12:17:38 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?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
end
--- a/src/HOL/Library/Efficient_Nat.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Jul 19 12:17:38 2010 +0200
@@ -337,7 +337,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat.Nat")
+ (Scala "Nat")
code_instance nat :: eq
(Haskell -)
@@ -405,7 +405,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
+ (Scala "!_.as'_BigInt" and "Nat")
text {* Conversion from and to indices. *}
@@ -419,7 +419,7 @@
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "toEnum")
- (Scala "!Nat.Nat((_))")
+ (Scala "Nat")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/List.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/List.thy Mon Jul 19 12:17:38 2010 +0200
@@ -4819,7 +4819,7 @@
(SML "[]")
(OCaml "[]")
(Haskell "[]")
- (Scala "Nil")
+ (Scala "!Nil")
code_instance list :: eq
(Haskell -)
--- a/src/HOL/Option.thy Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Option.thy Mon Jul 19 12:17:38 2010 +0200
@@ -114,7 +114,7 @@
(SML "NONE" and "SOME")
(OCaml "None" and "Some _")
(Haskell "Nothing" and "Just")
- (Scala "None" and "!Some((_))")
+ (Scala "!None" and "Some")
code_instance option :: eq
(Haskell -)
--- a/src/HOL/Tools/list_code.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Mon Jul 19 12:17:38 2010 +0200
@@ -46,8 +46,8 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target
- @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
+ in Code_Target.add_syntax_const target @{const_name Cons}
+ (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
end
end;
--- a/src/HOL/Tools/numeral.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Mon Jul 19 12:17:38 2010 +0200
@@ -77,8 +77,8 @@
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
thy |> Code_Target.add_syntax_const target number_of
- (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
- @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+ (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+ @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
end;
end; (*local*)
--- a/src/HOL/Tools/string_code.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Mon Jul 19 12:17:38 2010 +0200
@@ -60,7 +60,7 @@
| NONE =>
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in Code_Target.add_syntax_const target
- @{const_name Cons} (SOME (2, (cs_summa, pretty)))
+ @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
end;
fun add_literal_char target =
@@ -70,7 +70,7 @@
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
in Code_Target.add_syntax_const target
- @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
+ @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
end;
fun add_literal_string target =
@@ -83,7 +83,7 @@
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
in Code_Target.add_syntax_const target
- @{const_name STR} (SOME (1, (cs_summa, pretty)))
+ @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
end;
end;
--- a/src/Tools/Code/code_haskell.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Jul 19 12:17:38 2010 +0200
@@ -218,30 +218,35 @@
| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
- of NONE => semicolon [
- (str o deresolve_base) classparam,
- str "=",
- print_app tyvars (SOME thm) reserved NOBR (const, [])
- ]
- | SOME (k, pr) =>
- let
- val (c, (_, tys)) = const;
- val (vs, rhs) = (apfst o map) fst
- (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
- val s = if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c;
- val vars = reserved
- |> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
- (*dictionaries are not relevant at this late stage*)
- in
- semicolon [
- print_term tyvars (SOME thm) vars NOBR lhs,
+ fun requires_args classparam = case syntax_const classparam
+ of NONE => 0
+ | SOME (Code_Printer.Plain_const_syntax _) => 0
+ | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
+ fun print_classparam_instance ((classparam, const), (thm, _)) =
+ case requires_args classparam
+ of 0 => semicolon [
+ (str o deresolve_base) classparam,
str "=",
- print_term tyvars (SOME thm) vars NOBR rhs
+ print_app tyvars (SOME thm) reserved NOBR (const, [])
]
- end;
+ | k =>
+ let
+ val (c, (_, tys)) = const;
+ val (vs, rhs) = (apfst o map) fst
+ (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+ val s = if (is_some o syntax_const) c
+ then NONE else (SOME o Long_Name.base_name o deresolve) c;
+ val vars = reserved
+ |> intro_vars (map_filter I (s :: vs));
+ val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+ (*dictionaries are not relevant at this late stage*)
+ in
+ semicolon [
+ print_term tyvars (SOME thm) vars NOBR lhs,
+ str "=",
+ print_term tyvars (SOME thm) vars NOBR rhs
+ ]
+ end;
in
Pretty.block_enclose (
Pretty.block [
@@ -459,7 +464,7 @@
in if target = target' then
thy
|> Code_Target.add_syntax_const target c_bind
- (SOME (pretty_haskell_monad c_bind))
+ (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
else error "Only Haskell target allows for monad syntax" end;
--- a/src/Tools/Code/code_printer.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Mon Jul 19 12:17:38 2010 +0200
@@ -67,20 +67,22 @@
type tyco_syntax
type simple_const_syntax
- type proto_const_syntax
+ type complex_const_syntax
type const_syntax
- val parse_infix: ('a -> 'b) -> lrx * int -> string
- -> int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)
- val parse_syntax: ('a -> 'b) -> Token.T list
- -> (int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)) option * Token.T list
- val simple_const_syntax: simple_const_syntax -> proto_const_syntax
+ type activated_complex_const_syntax
+ datatype activated_const_syntax = Plain_const_syntax of int * string
+ | Complex_const_syntax of activated_complex_const_syntax
+ val requires_args: const_syntax -> int
+ val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
+ val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
+ val plain_const_syntax: string -> const_syntax
+ val simple_const_syntax: simple_const_syntax -> const_syntax
+ val complex_const_syntax: complex_const_syntax -> const_syntax
val activate_const_syntax: theory -> literals
- -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
+ -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> const_syntax option)
+ -> (string -> activated_const_syntax option)
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> fixity
@@ -243,31 +245,45 @@
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T);
-type proto_const_syntax = int * (string list * (literals -> string list
+
+type complex_const_syntax = int * (string list * (literals -> string list
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
+datatype const_syntax = plain_const_syntax of string
+ | complex_const_syntax of complex_const_syntax;
+
+fun requires_args (plain_const_syntax _) = 0
+ | requires_args (complex_const_syntax (k, _)) = k;
fun simple_const_syntax syn =
- apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
+ complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
-fun activate_const_syntax thy literals (n, (cs, f)) naming =
- fold_map (Code_Thingol.ensure_declared_const thy) cs naming
- |-> (fn cs' => pair (n, f literals cs'));
+type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+
+datatype activated_const_syntax = Plain_const_syntax of int * string
+ | Complex_const_syntax of activated_complex_const_syntax;
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
+ (Plain_const_syntax (Code.args_number thy c, s), naming)
+ | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
+ fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+ |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+
+fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
case syntax_const c
- of NONE => brackify fxy (print_app_expr thm vars app)
- | SOME (k, print) =>
+ of NONE => brackify fxy (print_app_expr some_thm vars app)
+ | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+ | SOME (Complex_const_syntax (k, print)) =>
let
- fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
+ fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
in if k = length ts
then print' fxy ts
else if k < length ts
then case chop k ts of (ts1, ts2) =>
- brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
- else print_term thm vars fxy (Code_Thingol.eta_expand k app)
+ brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+ else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
end;
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
@@ -281,7 +297,8 @@
datatype 'a mixfix =
Arg of fixity
- | Pretty of Pretty.T;
+ | String of string
+ | Break;
fun mk_mixfix prep_arg (fixity_this, mfx) =
let
@@ -292,8 +309,10 @@
[]
| fillin print (Arg fxy :: mfx) (a :: args) =
(print fxy o prep_arg) a :: fillin print mfx args
- | fillin print (Pretty p :: mfx) args =
- p :: fillin print mfx args;
+ | fillin print (String s :: mfx) args =
+ str s :: fillin print mfx args
+ | fillin print (Break :: mfx) args =
+ Pretty.brk 1 :: fillin print mfx args;
in
(i, fn print => fn fixity_ctxt => fn args =>
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
@@ -304,42 +323,45 @@
val l = case x of L => INFX (i, L) | _ => INFX (i, X);
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
in
- mk_mixfix prep_arg (INFX (i, x),
- [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+ mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r])
end;
-fun parse_mixfix prep_arg s =
+fun parse_mixfix mk_plain mk_complex prep_arg s =
let
val sym_any = Scan.one Symbol.is_regular;
val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|| ($$ "_" >> K (Arg BR))
- || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
+ || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
|| (Scan.repeat1
( $$ "'" |-- sym_any
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
- sym_any) >> (Pretty o str o implode)));
+ sym_any) >> (String o implode)));
in case Scan.finite Symbol.stopper parse (Symbol.explode s)
- of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
- | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
+ of ((false, [String s]), []) => mk_plain s
+ | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
+ | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
| _ => Scan.!!
(the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
end;
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
-fun parse_syntax prep_arg xs =
- Scan.option ((
+fun parse_syntax mk_plain mk_complex prep_arg =
+ Scan.option (
((Parse.$$$ infixK >> K X)
|| (Parse.$$$ infixlK >> K L)
|| (Parse.$$$ infixrK >> K R))
- -- Parse.nat >> parse_infix prep_arg
- || Scan.succeed (parse_mixfix prep_arg))
- -- Parse.string
- >> (fn (parse, s) => parse s)) xs;
+ -- Parse.nat -- Parse.string
+ >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
+ || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
+val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
+
+val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
+
(** module name spaces **)
--- a/src/Tools/Code/code_scala.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Mon Jul 19 12:17:38 2010 +0200
@@ -76,17 +76,20 @@
(app as ((c, ((arg_typs, _), function_typs)), ts)) =
let
val k = length ts;
- val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
val arg_typs' = if is_pat orelse
(is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
- val (no_syntax, print') = case syntax_const c
- of NONE => (true, fn ts => applify "(" ")"
+ val (l, print') = case syntax_const c
+ of NONE => (args_num c, 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 (_, print) => (false, fn ts =>
- print (print_term tyvars is_pat some_thm) some_thm vars fxy
- (ts ~~ take l function_typs));
+ | SOME (Plain_const_syntax (k, s)) => (k, 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
+ (ts ~~ take k function_typs))
in if k = l then print' ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -355,20 +358,22 @@
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
reserved args_num is_singleton_constr deresolver;
- fun print_module name content =
- (name, Pretty.chunks [
- str ("object " ^ name ^ " {"),
- str "",
+ fun print_module name imports content =
+ (name, Pretty.chunks (
+ str ("object " ^ name ^ " {")
+ :: (if null imports then []
+ else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
+ @ [str "",
content,
str "",
- str "}"
- ]);
+ str "}"]
+ ));
fun serialize_module the_module_name sca_program =
let
val content = Pretty.chunks2 (map_filter
(fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
| (_, (_, NONE)) => NONE) sca_program);
- in print_module the_module_name content end;
+ in print_module the_module_name (map fst includes) content end;
fun check_destination destination =
(File.check destination; destination);
fun write_module destination (modlname, content) =
@@ -385,7 +390,7 @@
(fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
(write_module (check_destination file)))
(rpair [] o cat_lines o map (code_of_pretty o snd))
- (map (uncurry print_module) includes
+ (map (fn (name, content) => print_module name [] content) includes
@| serialize_module the_module_name sca_program)
destination
end;
@@ -405,7 +410,7 @@
literal_char = Library.enclose "'" "'" o char_scala,
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
literal_naive_numeral = fn k => if k >= 0
then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
--- a/src/Tools/Code/code_target.ML Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon Jul 19 12:17:38 2010 +0200
@@ -41,11 +41,11 @@
val allow_abort: string -> theory -> theory
type tyco_syntax = Code_Printer.tyco_syntax
- type proto_const_syntax = Code_Printer.proto_const_syntax
+ type const_syntax = Code_Printer.const_syntax
val add_syntax_class: string -> class -> string option -> theory -> theory
val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
+ val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
end;
@@ -57,7 +57,7 @@
type literals = Code_Printer.literals;
type tyco_syntax = Code_Printer.tyco_syntax;
-type proto_const_syntax = Code_Printer.proto_const_syntax;
+type const_syntax = Code_Printer.const_syntax;
(** basics **)
@@ -83,7 +83,7 @@
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: Code_Printer.tyco_syntax Symtab.table,
- const: Code_Printer.proto_const_syntax Symtab.table
+ const: Code_Printer.const_syntax Symtab.table
};
fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -108,7 +108,7 @@
-> (string -> string option) (*module aliasses*)
-> (string -> string option) (*class syntax*)
-> (string -> Code_Printer.tyco_syntax option)
- -> (string -> Code_Printer.const_syntax option)
+ -> (string -> Code_Printer.activated_const_syntax option)
-> ((Pretty.T -> string) * (Pretty.T -> unit))
-> Code_Thingol.program
-> string list (*selected statements*)
@@ -244,11 +244,11 @@
|>> map_filter I;
fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
- |> fold_map (fn thing_identifier => fn (tab, naming) =>
- case Code_Thingol.lookup_const naming thing_identifier
+ |> fold_map (fn c => fn (tab, naming) =>
+ case Code_Thingol.lookup_const naming c
of SOME name => let
val (syn, naming') = Code_Printer.activate_const_syntax thy
- literals (the (Symtab.lookup src_tab thing_identifier)) naming
+ literals c (the (Symtab.lookup src_tab c)) naming
in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
| NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
|>> map_filter I;
@@ -445,12 +445,12 @@
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn);
-fun gen_add_syntax_const prep_const prep_syn =
+fun gen_add_syntax_const prep_const =
gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
- (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
- if fst syn > Code.args_number thy c
+ (fn thy => fn c => fn syn =>
+ if Code_Printer.requires_args syn > Code.args_number thy c
then error ("Too many arguments in syntax for constant " ^ quote c)
- else syn end);
+ else syn);
fun add_reserved target =
let
@@ -496,22 +496,23 @@
fun zip_list (x::xs) f g =
f
- #-> (fn y =>
+ :|-- (fn y =>
fold_map (fn x => g |-- f >> pair x) xs
- #-> (fn xys => pair ((x, y) :: xys)));
+ :|-- (fn xys => pair ((x, y) :: xys)));
-fun parse_multi_syntax parse_thing parse_syntax =
- Parse.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
- (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
+fun process_multi_syntax parse_thing parse_syntax change =
+ (Parse.and_list1 parse_thing
+ :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+ (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+ >> (Toplevel.theory oo fold)
+ (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
in
val add_syntax_class = gen_add_syntax_class cert_class;
val add_syntax_inst = gen_add_syntax_inst cert_inst;
val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
-val add_syntax_const = gen_add_syntax_const (K I) I;
+val add_syntax_const = gen_add_syntax_const (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
val add_include = add_include;
@@ -519,9 +520,7 @@
val add_syntax_class_cmd = gen_add_syntax_class read_class;
val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
-
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
@@ -550,32 +549,24 @@
val _ =
Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
- parse_multi_syntax Parse.xname (Scan.option Parse.string)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
- );
+ process_multi_syntax Parse.xname (Scan.option Parse.string)
+ add_syntax_class_cmd);
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
- parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+ process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
- );
+ add_syntax_inst_cmd);
val _ =
Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
- parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
- );
+ process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+ add_syntax_tyco_cmd);
val _ =
Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
- parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
- );
+ process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+ add_syntax_const_cmd);
val _ =
Outer_Syntax.command "code_reserved" "declare words as reserved for target language"