--- a/src/HOL/Tools/list_code.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Tue Jun 01 13:59:13 2010 +0200
@@ -31,11 +31,11 @@
end;
fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
- Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
+ Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
Code_Printer.str target_cons,
pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
- ];
+ );
fun add_literal_list target =
let
--- a/src/Tools/Code/code_haskell.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 01 13:59:13 2010 +0200
@@ -447,7 +447,7 @@
(ps @| print_term vars' NOBR t'')
end
| NONE => brackify_infix (1, L) fxy
- [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2]
+ (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
in (2, ([c_bind], pretty)) end;
fun add_monad target' raw_c_bind thy =
@@ -477,11 +477,11 @@
val setup =
Code_Target.add_target (target, (isar_seri_haskell, literals))
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target) [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
"import", "default", "forall", "let", "in", "class", "qualified", "data",
--- a/src/Tools/Code/code_ml.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 01 13:59:13 2010 +0200
@@ -963,17 +963,17 @@
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
--- a/src/Tools/Code/code_printer.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 01 13:59:13 2010 +0200
@@ -61,7 +61,7 @@
val INFX: int * lrx -> fixity
val APP: fixity
val brackify: fixity -> Pretty.T list -> Pretty.T
- val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+ val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
@@ -219,8 +219,9 @@
fun brackify fxy_ctxt =
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
-fun brackify_infix infx fxy_ctxt =
- gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
+fun brackify_infix infx fxy_ctxt (l, m, r) =
+ (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
+ ([l, str " ", m, Pretty.brk 1, r]);
fun brackify_block fxy_ctxt p1 ps p2 =
let val p = Pretty.block_enclose (p1, p2) ps
@@ -304,7 +305,7 @@
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
in
mk_mixfix prep_arg (INFX (i, x),
- [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+ [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
end;
fun parse_mixfix prep_arg s =
--- a/src/Tools/Code/code_scala.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 01 13:59:13 2010 +0200
@@ -25,11 +25,12 @@
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
let
val deresolve_base = Long_Name.base_name o deresolve;
+ val lookup_tyvar = first_upper oo lookup_var;
fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => applify "[" "]" fxy
((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
- | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+ | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
fun print_typed tyvars p ty =
Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
fun print_var vars NONE = str "_"
@@ -114,19 +115,20 @@
fun implicit_arguments tyvars vs vars =
let
val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
- [(str o deresolve) class, str "[", (str o lookup_var tyvars) v, str "]"]) sort) vs;
- val implicit_names = Name.invents (snd vars) "a" (length implicit_typ_ps);
+ [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
+ val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
+ lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
val vars' = intro_vars implicit_names vars;
val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
implicit_names implicit_typ_ps;
in ((implicit_names, implicit_ps), vars') end;
fun print_defhead tyvars vars p vs params tys implicits ty =
- concat [str "def", print_typed tyvars (applify "(implicit " ")" NOBR
+ Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
(applify "(" ")" NOBR
- (applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs))
+ (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
(map2 (fn param => fn ty => print_typed tyvars
((str o lookup_var vars) param) ty)
- params tys)) implicits) ty, str "="]
+ params tys)) implicits) ty, str " ="]
fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
of [] =>
let
@@ -193,7 +195,7 @@
val fields = Name.names (snd reserved) "a" tys;
val vars = intro_vars (map fst fields) reserved;
fun add_typargs p = applify "[" "]" NOBR p
- (map (str o lookup_var tyvars o fst) vs);
+ (map (str o lookup_tyvar tyvars o fst) vs);
in
concat [
applify "(" ")" NOBR
@@ -206,7 +208,7 @@
in
Pretty.chunks (
applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
- (map (str o prefix "+" o lookup_var tyvars o fst) vs)
+ (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
:: map print_co cos
)
end
@@ -214,7 +216,7 @@
let
val tyvars = intro_vars [v] reserved;
val vs = [(v, [name])];
- fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_var tyvars) v];
+ fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
fun print_superclasses [] = NONE
| print_superclasses classes = SOME (concat (str "extends"
:: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
@@ -255,7 +257,7 @@
val tyvars = intro_vars (map fst vs) reserved;
val insttyp = tyco `%% map (ITyVar o fst) vs;
val p_inst_typ = print_typ tyvars NOBR insttyp;
- fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs);
+ fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
@@ -282,10 +284,10 @@
@ map print_classparam_inst classparam_insts),
concat [str "implicit", str (if null vs then "val" else "def"),
applify "(implicit " ")" NOBR (applify "[" "]" NOBR
- ((str o deresolve_base) name) (map (str o lookup_var tyvars o fst) vs))
+ ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
implicit_ps,
str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
- (map (str o lookup_var tyvars o fst) vs),
+ (map (str o lookup_tyvar tyvars o fst) vs),
Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
implicit_names)]
]
@@ -431,17 +433,17 @@
val setup =
Code_Target.add_target (target, (isar_seri_scala, literals))
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
str "=>",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target) [
"abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
"final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
"match", "new", "null", "object", "override", "package", "private", "protected",
"requires", "return", "sealed", "super", "this", "throw", "trait", "try",
- "true", "type", "val", "var", "while", "with"
+ "true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
"error", "apply", "List", "Nil", "BigInt"
--- a/src/Tools/Code/lib/Tools/codegen Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Tue Jun 01 13:59:13 2010 +0200
@@ -58,7 +58,7 @@
QND_CMD="reset"
fi
-CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"