1.1 --- a/src/HOL/Tools/list_code.ML Tue Jun 01 12:16:40 2010 +0200
1.2 +++ b/src/HOL/Tools/list_code.ML Tue Jun 01 13:59:13 2010 +0200
1.3 @@ -31,11 +31,11 @@
1.4 end;
1.5
1.6 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
1.7 - Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
1.8 + Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
1.9 pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
1.10 Code_Printer.str target_cons,
1.11 pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
1.12 - ];
1.13 + );
1.14
1.15 fun add_literal_list target =
1.16 let
2.1 --- a/src/Tools/Code/code_haskell.ML Tue Jun 01 12:16:40 2010 +0200
2.2 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 01 13:59:13 2010 +0200
2.3 @@ -447,7 +447,7 @@
2.4 (ps @| print_term vars' NOBR t'')
2.5 end
2.6 | NONE => brackify_infix (1, L) fxy
2.7 - [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2]
2.8 + (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
2.9 in (2, ([c_bind], pretty)) end;
2.10
2.11 fun add_monad target' raw_c_bind thy =
2.12 @@ -477,11 +477,11 @@
2.13 val setup =
2.14 Code_Target.add_target (target, (isar_seri_haskell, literals))
2.15 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
2.16 - brackify_infix (1, R) fxy [
2.17 + brackify_infix (1, R) fxy (
2.18 print_typ (INFX (1, X)) ty1,
2.19 str "->",
2.20 print_typ (INFX (1, R)) ty2
2.21 - ]))
2.22 + )))
2.23 #> fold (Code_Target.add_reserved target) [
2.24 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
2.25 "import", "default", "forall", "let", "in", "class", "qualified", "data",
3.1 --- a/src/Tools/Code/code_ml.ML Tue Jun 01 12:16:40 2010 +0200
3.2 +++ b/src/Tools/Code/code_ml.ML Tue Jun 01 13:59:13 2010 +0200
3.3 @@ -963,17 +963,17 @@
3.4 Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
3.5 #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
3.6 #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
3.7 - brackify_infix (1, R) fxy [
3.8 + brackify_infix (1, R) fxy (
3.9 print_typ (INFX (1, X)) ty1,
3.10 str "->",
3.11 print_typ (INFX (1, R)) ty2
3.12 - ]))
3.13 + )))
3.14 #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
3.15 - brackify_infix (1, R) fxy [
3.16 + brackify_infix (1, R) fxy (
3.17 print_typ (INFX (1, X)) ty1,
3.18 str "->",
3.19 print_typ (INFX (1, R)) ty2
3.20 - ]))
3.21 + )))
3.22 #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
3.23 #> fold (Code_Target.add_reserved target_SML)
3.24 ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
4.1 --- a/src/Tools/Code/code_printer.ML Tue Jun 01 12:16:40 2010 +0200
4.2 +++ b/src/Tools/Code/code_printer.ML Tue Jun 01 13:59:13 2010 +0200
4.3 @@ -61,7 +61,7 @@
4.4 val INFX: int * lrx -> fixity
4.5 val APP: fixity
4.6 val brackify: fixity -> Pretty.T list -> Pretty.T
4.7 - val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
4.8 + val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
4.9 val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
4.10 val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
4.11
4.12 @@ -219,8 +219,9 @@
4.13 fun brackify fxy_ctxt =
4.14 gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
4.15
4.16 -fun brackify_infix infx fxy_ctxt =
4.17 - gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
4.18 +fun brackify_infix infx fxy_ctxt (l, m, r) =
4.19 + (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
4.20 + ([l, str " ", m, Pretty.brk 1, r]);
4.21
4.22 fun brackify_block fxy_ctxt p1 ps p2 =
4.23 let val p = Pretty.block_enclose (p1, p2) ps
4.24 @@ -304,7 +305,7 @@
4.25 val r = case x of R => INFX (i, R) | _ => INFX (i, X);
4.26 in
4.27 mk_mixfix prep_arg (INFX (i, x),
4.28 - [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
4.29 + [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
4.30 end;
4.31
4.32 fun parse_mixfix prep_arg s =
5.1 --- a/src/Tools/Code/code_scala.ML Tue Jun 01 12:16:40 2010 +0200
5.2 +++ b/src/Tools/Code/code_scala.ML Tue Jun 01 13:59:13 2010 +0200
5.3 @@ -25,11 +25,12 @@
5.4 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
5.5 let
5.6 val deresolve_base = Long_Name.base_name o deresolve;
5.7 + val lookup_tyvar = first_upper oo lookup_var;
5.8 fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
5.9 of NONE => applify "[" "]" fxy
5.10 ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
5.11 | SOME (i, print) => print (print_typ tyvars) fxy tys)
5.12 - | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
5.13 + | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
5.14 fun print_typed tyvars p ty =
5.15 Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
5.16 fun print_var vars NONE = str "_"
5.17 @@ -114,19 +115,20 @@
5.18 fun implicit_arguments tyvars vs vars =
5.19 let
5.20 val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
5.21 - [(str o deresolve) class, str "[", (str o lookup_var tyvars) v, str "]"]) sort) vs;
5.22 - val implicit_names = Name.invents (snd vars) "a" (length implicit_typ_ps);
5.23 + [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
5.24 + val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
5.25 + lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
5.26 val vars' = intro_vars implicit_names vars;
5.27 val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
5.28 implicit_names implicit_typ_ps;
5.29 in ((implicit_names, implicit_ps), vars') end;
5.30 fun print_defhead tyvars vars p vs params tys implicits ty =
5.31 - concat [str "def", print_typed tyvars (applify "(implicit " ")" NOBR
5.32 + Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
5.33 (applify "(" ")" NOBR
5.34 - (applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs))
5.35 + (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
5.36 (map2 (fn param => fn ty => print_typed tyvars
5.37 ((str o lookup_var vars) param) ty)
5.38 - params tys)) implicits) ty, str "="]
5.39 + params tys)) implicits) ty, str " ="]
5.40 fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
5.41 of [] =>
5.42 let
5.43 @@ -193,7 +195,7 @@
5.44 val fields = Name.names (snd reserved) "a" tys;
5.45 val vars = intro_vars (map fst fields) reserved;
5.46 fun add_typargs p = applify "[" "]" NOBR p
5.47 - (map (str o lookup_var tyvars o fst) vs);
5.48 + (map (str o lookup_tyvar tyvars o fst) vs);
5.49 in
5.50 concat [
5.51 applify "(" ")" NOBR
5.52 @@ -206,7 +208,7 @@
5.53 in
5.54 Pretty.chunks (
5.55 applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
5.56 - (map (str o prefix "+" o lookup_var tyvars o fst) vs)
5.57 + (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
5.58 :: map print_co cos
5.59 )
5.60 end
5.61 @@ -214,7 +216,7 @@
5.62 let
5.63 val tyvars = intro_vars [v] reserved;
5.64 val vs = [(v, [name])];
5.65 - fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_var tyvars) v];
5.66 + fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
5.67 fun print_superclasses [] = NONE
5.68 | print_superclasses classes = SOME (concat (str "extends"
5.69 :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
5.70 @@ -255,7 +257,7 @@
5.71 val tyvars = intro_vars (map fst vs) reserved;
5.72 val insttyp = tyco `%% map (ITyVar o fst) vs;
5.73 val p_inst_typ = print_typ tyvars NOBR insttyp;
5.74 - fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs);
5.75 + fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
5.76 fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
5.77 val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
5.78 fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
5.79 @@ -282,10 +284,10 @@
5.80 @ map print_classparam_inst classparam_insts),
5.81 concat [str "implicit", str (if null vs then "val" else "def"),
5.82 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
5.83 - ((str o deresolve_base) name) (map (str o lookup_var tyvars o fst) vs))
5.84 + ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
5.85 implicit_ps,
5.86 str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
5.87 - (map (str o lookup_var tyvars o fst) vs),
5.88 + (map (str o lookup_tyvar tyvars o fst) vs),
5.89 Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
5.90 implicit_names)]
5.91 ]
5.92 @@ -431,17 +433,17 @@
5.93 val setup =
5.94 Code_Target.add_target (target, (isar_seri_scala, literals))
5.95 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
5.96 - brackify_infix (1, R) fxy [
5.97 + brackify_infix (1, R) fxy (
5.98 print_typ BR ty1 (*product type vs. tupled arguments!*),
5.99 str "=>",
5.100 print_typ (INFX (1, R)) ty2
5.101 - ]))
5.102 + )))
5.103 #> fold (Code_Target.add_reserved target) [
5.104 "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
5.105 "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
5.106 "match", "new", "null", "object", "override", "package", "private", "protected",
5.107 "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
5.108 - "true", "type", "val", "var", "while", "with"
5.109 + "true", "type", "val", "var", "while", "with", "yield"
5.110 ]
5.111 #> fold (Code_Target.add_reserved target) [
5.112 "error", "apply", "List", "Nil", "BigInt"
6.1 --- a/src/Tools/Code/lib/Tools/codegen Tue Jun 01 12:16:40 2010 +0200
6.2 +++ b/src/Tools/Code/lib/Tools/codegen Tue Jun 01 13:59:13 2010 +0200
6.3 @@ -58,7 +58,7 @@
6.4 QND_CMD="reset"
6.5 fi
6.6
6.7 -CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
6.8 +CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
6.9
6.10 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
6.11