# HG changeset patch # User haftmann # Date 1275393553 -7200 # Node ID c1d14288c5c0767e39dff7e4bdeb956e89421695 # Parent d94459cf7ea860258d9a961f3c6aa21036a227b7# Parent a53f296f86d3bf882f03b250e3d18c3fb1af53b4 merged diff -r d94459cf7ea8 -r c1d14288c5c0 src/HOL/Tools/list_code.ML --- 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 diff -r d94459cf7ea8 -r c1d14288c5c0 src/Tools/Code/code_haskell.ML --- 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", diff -r d94459cf7ea8 -r c1d14288c5c0 src/Tools/Code/code_ml.ML --- 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"] diff -r d94459cf7ea8 -r c1d14288c5c0 src/Tools/Code/code_printer.ML --- 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 = diff -r d94459cf7ea8 -r c1d14288c5c0 src/Tools/Code/code_scala.ML --- 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" diff -r d94459cf7ea8 -r c1d14288c5c0 src/Tools/Code/lib/Tools/codegen --- 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"