--- 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
--- 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
--- 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);
--- 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",
--- 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"]
--- 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 =
--- 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"
--- 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"