# HG changeset patch # User wenzelm # Date 1275406613 -7200 # Node ID 8e1e27a3b3613df4ebed6daec5b8f3f65b314e03 # Parent b3ff14122645ece1c195c7cd587896359fc6cf79# Parent 04d2521e79b0d44c3790b360636b9a1745e0c8e7 merged diff -r 04d2521e79b0 -r 8e1e27a3b361 src/HOL/Tools/list_code.ML --- a/src/HOL/Tools/list_code.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/HOL/Tools/list_code.ML Tue Jun 01 17:36:53 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 04d2521e79b0 -r 8e1e27a3b361 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Pure/Isar/class_target.ML Tue Jun 01 17:36:53 2010 +0200 @@ -243,7 +243,7 @@ | NONE => I in thy - |> AxClass.add_classrel true classrel + |> AxClass.add_classrel classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) |> add_dependency @@ -366,7 +366,7 @@ fun gen_classrel mk_prop classrel thy = let fun after_qed results = - ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results); + ProofContext.theory ((fold o fold) AxClass.add_classrel results); in thy |> ProofContext.init_global @@ -450,7 +450,7 @@ (* target *) -val sanatize_name = (*FIXME*) +val sanitize_name = (*FIXME*) let fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'" orelse s = "_"; @@ -467,7 +467,7 @@ fun type_name "*" = "prod" | type_name "+" = "sum" - | type_name s = sanatize_name (Long_Name.base_name s); + | type_name s = sanitize_name (Long_Name.base_name s); fun resort_terms pp algebra consts constraints ts = let @@ -531,7 +531,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results) + Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) #> after_qed; in lthy @@ -591,7 +591,7 @@ val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed results = ProofContext.theory - ((fold o fold) (AxClass.add_arity true) results); + ((fold o fold) AxClass.add_arity results); in thy |> ProofContext.init_global diff -r 04d2521e79b0 -r 8e1e27a3b361 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Pure/axclass.ML Tue Jun 01 17:36:53 2010 +0200 @@ -24,8 +24,8 @@ val read_classrel: theory -> xstring * xstring -> class * class val declare_overloaded: string * typ -> theory -> term * theory val define_overloaded: binding -> string * term -> theory -> thm * theory - val add_classrel: bool -> thm -> theory -> theory - val add_arity: bool -> thm -> theory -> theory + val add_classrel: thm -> theory -> theory + val add_arity: thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory val prove_arity: string * sort list * sort -> tactic -> theory -> theory val define_class: binding * class list -> string list -> @@ -412,7 +412,7 @@ (* primitive rules *) -fun add_classrel store raw_th thy = +fun gen_add_classrel store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; @@ -433,7 +433,7 @@ |> perhaps complete_arities end; -fun add_arity store raw_th thy = +fun gen_add_arity store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; @@ -463,6 +463,9 @@ |> put_arity ((t, Ss, c), th'') end; +val add_classrel = gen_add_classrel true; +val add_arity = gen_add_arity true; + (* tactical proofs *) @@ -477,7 +480,7 @@ thy |> PureThy.add_thms [((Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] - |-> (fn [th'] => add_classrel false th') + |-> (fn [th'] => gen_add_classrel false th') end; fun prove_arity raw_arity tac thy = @@ -493,7 +496,7 @@ in thy |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) - |-> fold (add_arity false) + |-> fold (gen_add_arity false) end; @@ -627,11 +630,11 @@ fun ax_classrel prep = axiomatize (map o prep) (map Logic.mk_classrel) - (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false); + (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false); fun ax_arity prep = axiomatize (prep o ProofContext.init_global) Logic.mk_arities - (map (prefix arity_prefix) o Logic.name_arities) (add_arity false); + (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false); fun class_const c = (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); diff -r 04d2521e79b0 -r 8e1e27a3b361 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 01 17:36:53 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 04d2521e79b0 -r 8e1e27a3b361 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jun 01 17:36:53 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 04d2521e79b0 -r 8e1e27a3b361 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Tue Jun 01 17:36:53 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 04d2521e79b0 -r 8e1e27a3b361 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Tue Jun 01 17:36:53 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 04d2521e79b0 -r 8e1e27a3b361 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Tue Jun 01 17:27:38 2010 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Tue Jun 01 17:36:53 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"