--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Jun 18 14:14:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Jun 18 14:14:42 2010 +0200
@@ -864,9 +864,10 @@
Internally, the evaluation is performed by registered evaluators,
which are invoked sequentially until a result is returned.
Alternatively a specific evaluator can be selected using square
- brackets; available evaluators include @{text nbe} for
- \emph{normalization by evaluation} and \emph{code} for code
- generation in SML.
+ brackets; typical evaluators use the current set of code equations
+ to normalize and include @{text simp} for fully symbolic evaluation
+ using the simplifier, @{text nbe} for \emph{normalization by evaluation}
+ and \emph{code} for code generation in SML.
\item @{command (HOL) "quickcheck"} tests the current goal for
counter examples using a series of arbitrary assignments for its
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Jun 18 14:14:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Jun 18 14:14:42 2010 +0200
@@ -882,9 +882,10 @@
Internally, the evaluation is performed by registered evaluators,
which are invoked sequentially until a result is returned.
Alternatively a specific evaluator can be selected using square
- brackets; available evaluators include \isa{nbe} for
- \emph{normalization by evaluation} and \emph{code} for code
- generation in SML.
+ brackets; typical evaluators use the current set of code equations
+ to normalize and include \isa{simp} for fully symbolic evaluation
+ using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
+ and \emph{code} for code generation in SML.
\item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
counter examples using a series of arbitrary assignments for its
--- a/src/HOL/List.thy Fri Jun 18 14:14:29 2010 +0200
+++ b/src/HOL/List.thy Fri Jun 18 14:14:42 2010 +0200
@@ -4964,7 +4964,7 @@
(Haskell "concat")
code_const rev
- (Haskell "rev")
+ (Haskell "reverse")
code_const zip
(Haskell "zip")
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jun 18 14:14:29 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jun 18 14:14:42 2010 +0200
@@ -5266,7 +5266,7 @@
(* class constraint due to continuous_on_inverse *)
shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
\<Longrightarrow> s homeomorphic t"
- unfolding homeomorphic_def by(metis homeomorphism_compact)
+ unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
text{* Preservation of topological properties. *}
--- a/src/Pure/Isar/code.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Pure/Isar/code.ML Fri Jun 18 14:14:42 2010 +0200
@@ -66,7 +66,7 @@
val del_eqns: string -> theory -> theory
val add_case: thm -> theory -> theory
val add_undefined: string -> theory -> theory
- val get_type: theory -> string -> ((string * sort) list * (string * typ list) list)
+ val get_type: theory -> string -> ((string * sort) list * ((string * string list) * typ list) list)
val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
val is_constr: theory -> string -> bool
val is_abstr: theory -> string -> bool
@@ -429,7 +429,13 @@
of SOME (vs, Abstractor spec) => (vs, spec)
| _ => error ("Not an abstract type: " ^ tyco);
-fun get_type thy = fst o get_type_spec thy;
+fun get_type thy tyco =
+ let
+ val ((vs, cos), _) = get_type_spec thy tyco;
+ fun args_of c tys = map (fst o dest_TFree)
+ (Sign.const_typargs thy (c, tys ---> Type (tyco, map TFree vs)));
+ fun add_typargs (c, tys) = ((c, args_of c tys), tys);
+ in (vs, map add_typargs cos) end;
fun get_type_of_constr_or_abstr thy c =
case (snd o strip_type o const_typ thy) c
@@ -1115,7 +1121,7 @@
val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
- val T = Logic.unvarifyT_global (const_typ thy case_const);
+ val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
val Ts = (fst o strip_type) T;
val T_cong = nth Ts pos;
fun mk_prem z = Free (z, T_cong);
@@ -1177,7 +1183,7 @@
Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
fun datatype_interpretation f = Datatype_Interpretation.interpretation
- (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy);
+ (fn (tyco, _) => fn thy => f (tyco, fst (get_type_spec thy tyco)) thy);
fun add_datatype proto_constrs thy =
let
--- a/src/Tools/Code/code_eval.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Fri Jun 18 14:14:42 2010 +0200
@@ -122,7 +122,7 @@
fun check_datatype thy tyco consts =
let
- val constrs = (map fst o snd o Code.get_type thy) tyco;
+ val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
val missing_constrs = subtract (op =) consts constrs;
val _ = if null missing_constrs then []
else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
--- a/src/Tools/Code/code_haskell.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Fri Jun 18 14:14:42 2010 +0200
@@ -75,7 +75,7 @@
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
- and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+ and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
| fingerprint => let
val ts_fingerprint = ts ~~ take (length ts) fingerprint;
@@ -86,7 +86,7 @@
brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
in
if needs_annotation then
- (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
+ (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
@@ -163,7 +163,7 @@
print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
]
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
+ | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
let
val tyvars = intro_vars (map fst vs) reserved;
in
@@ -179,7 +179,7 @@
| print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_co (co, tys) =
+ fun print_co ((co, _), tys) =
concat (
(str o deresolve_base) co
:: map (print_typ tyvars BR) tys
@@ -214,7 +214,7 @@
str "};"
) (map print_classparam classparams)
end
- | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
+ | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
--- a/src/Tools/Code/code_ml.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Fri Jun 18 14:14:42 2010 +0200
@@ -32,14 +32,14 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * ((class * (string * (vname * sort) list))
- * (((class * (string * (string * dict list list))) list * (class * class) list list)
- * ((string * const) * (thm * bool)) list));
+ * ((class * (string * (string * dict list list))) list
+ * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
| ML_Funs of ml_binding list * string list
- | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
+ | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
| ML_Class of string * (vname * ((class * string) list * (string * itype) list));
fun stmt_name_of_binding (ML_Function (name, _)) = name
@@ -121,9 +121,9 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
if is_cons c then
- let val k = length tys in
+ let val k = length function_typs in
if k < 2 orelse length ts = k
then (str o deresolve) c
:: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -174,8 +174,8 @@
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co (co, []) = str (deresolve co)
- | print_co (co, tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve co)
+ | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
@@ -219,7 +219,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [
@@ -466,8 +466,8 @@
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co (co, []) = str (deresolve co)
- | print_co (co, tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve co)
+ | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
@@ -554,7 +554,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [
--- a/src/Tools/Code/code_printer.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Jun 18 14:14:42 2010 +0200
@@ -256,12 +256,12 @@
fold_map (Code_Thingol.ensure_declared_const thy) cs naming
|-> (fn cs' => pair (n, f literals cs'));
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
case syntax_const c
of NONE => brackify fxy (print_app_expr thm vars app)
| SOME (k, print) =>
let
- fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys);
+ fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
in if k = length ts
then print' fxy ts
else if k < length ts
--- a/src/Tools/Code/code_scala.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Jun 18 14:14:42 2010 +0200
@@ -61,18 +61,18 @@
then print_case tyvars some_thm vars fxy cases
else print_app tyvars is_pat some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
- and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
+ and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) =
let
val k = length ts;
val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
- val tys' = if is_pat orelse
- (is_none (syntax_const c) andalso is_singleton c) then [] else tys;
+ val arg_typs' = if is_pat orelse
+ (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
val (no_syntax, print') = case syntax_const c
of NONE => (true, fn ts => applify "(" ")" fxy
- (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
+ (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs'))
(map (print_term tyvars is_pat some_thm vars NOBR) ts))
| SOME (_, print) => (false, fn ts =>
- print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
+ print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs));
in if k = l then print' ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -122,10 +122,11 @@
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 =
+ fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
(applify "(" ")" NOBR
- (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
+ (applify "[" "]" NOBR p (map (fn (v, sort) =>
+ (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
(map2 (fn param => fn ty => print_typed tyvars
((str o lookup_var vars) param) ty)
params tys)) implicits) ty, str " ="]
@@ -156,7 +157,7 @@
val vars1 = reserved
|> intro_base_names
(is_none o syntax_const) deresolve consts
- val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1;
+ val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*)
val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
else aux_params vars2 (map (fst o fst) eqs);
val vars3 = intro_vars params vars2;
@@ -174,7 +175,7 @@
concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
- val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
+ val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2;
in if simple then
concat [head, print_rhs vars3 (hd eqs)]
else
@@ -186,23 +187,25 @@
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_co (co, []) =
+ fun print_co ((co, _), []) =
concat [str "final", str "case", str "object", (str o deresolve_base) co,
str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
(replicate (length vs) (str "Nothing"))]
- | print_co (co, tys) =
+ | print_co ((co, vs_args), tys) =
let
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_tyvar tyvars o fst) vs);
+ fun add_typargs1 p = applify "[" "]" NOBR p
+ (map (str o lookup_tyvar tyvars o fst) vs); (*FIXME*)
+ fun add_typargs2 p = applify "[" "]" NOBR p
+ (map (str o lookup_tyvar tyvars) vs_args); (*FIXME*)
in
concat [
applify "(" ")" NOBR
- (add_typargs ((concat o map str) ["final", "case", "class", deresolve_base co]))
+ (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co]))
(map (uncurry (print_typed tyvars) o apfst str) fields),
str "extends",
- add_typargs ((str o deresolve_base) name)
+ add_typargs1 ((str o deresolve_base) name)
]
end
in
@@ -230,13 +233,24 @@
fun print_classparam_val (classparam, ty) =
concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
(print_tupled_typ o Code_Thingol.unfold_fun) ty]
+ fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
+ let
+ val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
+ [(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_classparam_def (classparam, ty) =
let
val (tys, ty) = Code_Thingol.unfold_fun ty;
val params = Name.invents (snd reserved) "a" (length tys);
val vars = intro_vars params reserved;
val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
- val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
+ val head = print_defhead tyvars vars' ((str o deresolve) classparam)
+ ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
in
concat [head, applify "(" ")" NOBR
(Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
@@ -252,14 +266,22 @@
)
end
| print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
- ((super_instances, _), classparam_instances))) =
+ (super_instances, (classparam_instances, further_classparam_instances)))) =
let
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_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;
+ val classtyp = (class, (tyco, map fst vs));
+ fun print_classtyp' (class, (tyco, vs)) = (*FIXME already exists?*)
+ applify "[" "]" NOBR(*? FIXME*) ((str o deresolve) class)
+ [print_typ tyvars NOBR (tyco `%% map ITyVar vs)]; (*FIXME a mess...*)
+ fun print_typed' tyvars p classtyp = (*FIXME unify with existing print_typed*)
+ Pretty.block [p, str ":", Pretty.brk 1, print_classtyp' classtyp];
+ fun print_defhead' tyvars vars p vs params tys classtyp = (*FIXME unify with existing def_head*)
+ Pretty.block [str "def ", print_typed' tyvars
+ (applify "(" ")" NOBR
+ (applify "[" "]" NOBR p (map (fn (v, sort) =>
+ (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
+ (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty)
+ params tys)) classtyp, str " ="];
fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
let
val auxs = Name.invents (snd reserved) "a" (length tys);
@@ -271,27 +293,10 @@
concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
end;
- in
- Pretty.chunks [
- Pretty.block_enclose
- (concat ([str "trait",
- add_typ_params ((str o deresolve_base) name),
- str "extends",
- Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
- @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance)))
- super_instances @| str "{"), str "}")
- (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
- @ map print_classparam_instance classparam_instances),
- 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_tyvar tyvars o fst) vs))
- implicit_ps,
- str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
- (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)]
- ]
- end;
+ val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
+ val body = [str "new", print_classtyp' classtyp,
+ Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
+ in concat (str "implicit" :: head :: body) end;
in print_stmt end;
fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
@@ -356,14 +361,14 @@
| Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
| Code_Thingol.Datatypecons (_, tyco) =>
let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
- in (length o the o AList.lookup (op =) constrs) c end
+ in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
| Code_Thingol.Classparam (_, class) =>
let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
fun is_singleton c = case Graph.get_node program c
of Code_Thingol.Datatypecons (_, tyco) =>
let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
- in (null o the o AList.lookup (op =) constrs) c end
+ in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
reserved args_num is_singleton deresolver;
--- a/src/Tools/Code/code_simp.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Fri Jun 18 14:14:42 2010 +0200
@@ -10,6 +10,7 @@
val map_ss: (simpset -> simpset) -> theory -> theory
val current_conv: theory -> conv
val current_tac: theory -> int -> tactic
+ val current_value: theory -> term -> term
val make_conv: theory -> simpset option -> string list -> conv
val make_tac: theory -> simpset option -> string list -> int -> tactic
val setup: theory -> theory
@@ -50,8 +51,8 @@
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
- | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
- ss addsimps (map (fst o snd) classparam_insts)
+ | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
+ ss addsimps (map (fst o snd) classparam_instances)
| add_stmt _ ss = ss;
val add_program = Graph.fold (add_stmt o fst o snd)
@@ -68,9 +69,12 @@
fun current_tac thy = CONVERSION (current_conv thy);
+fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy
+
val setup = Method.setup (Binding.name "code_simp")
(Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
"simplification with code equations"
+ #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
(* evaluation with freezed code context *)
--- a/src/Tools/Code/code_thingol.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Jun 18 14:14:42 2010 +0200
@@ -67,15 +67,16 @@
datatype stmt =
NoStmt
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * ((vname * sort) list * (string * itype list) list)
+ | Datatype of string * ((vname * sort) list *
+ ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
| Classparam of string * class
- | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
- * (((class * (string * (string * dict list list))) list (*super instances*)
- * (class * class) list list (*type argument weakening mapping*))
- * ((string * const) * (thm * bool)) list (*class parameter instances*))
+ | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
+ * ((class * (string * (string * dict list list))) list (*super instances*)
+ * (((string * const) * (thm * bool)) list (*class parameter instances*)
+ * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
type program = stmt Graph.T
val empty_funs: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -404,15 +405,16 @@
datatype stmt =
NoStmt
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * ((vname * sort) list * (string * itype list) list)
+ | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
| Classparam of string * class
| Classinst of (class * (string * (vname * sort) list))
- * (((class * (string * (string * dict list list))) list
- * (class * class) list list)
- * ((string * const) * (thm * bool)) list) (*see also signature*);
+ * ((class * (string * (string * dict list list))) list
+ * (((string * const) * (thm * bool)) list
+ * ((string * const) * (thm * bool)) list))
+ (*see also signature*);
type program = stmt Graph.T;
@@ -430,6 +432,9 @@
(ICase (((map_terms_bottom_up f t, ty), (map o pairself)
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
+fun map_classparam_instances_as_term f =
+ (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
+
fun map_terms_stmt f NoStmt = NoStmt
| map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
(fn (ts, t) => (map f ts, f t)) eqs), case_cong))
@@ -438,9 +443,8 @@
| map_terms_stmt f (stmt as Class _) = stmt
| map_terms_stmt f (stmt as Classrel _) = stmt
| map_terms_stmt f (stmt as Classparam _) = stmt
- | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
- Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
- case f (IConst const) of IConst const' => const') classparams));
+ | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
+ Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
fun is_cons program name = case Graph.get_node program name
of Datatypecons _ => true
@@ -559,8 +563,9 @@
val (vs, cos) = Code.get_type thy tyco;
val stmt_datatype =
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
- ##>> fold_map (fn (c, tys) =>
+ ##>> fold_map (fn ((c, vs), tys) =>
ensure_const thy algbr eqngr permissive c
+ ##>> pair (map (unprefix "'") vs)
##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
#>> (fn info => Datatype (tyco, info));
in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
@@ -609,7 +614,10 @@
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
- val classparams = these (try (#params o AxClass.get_info thy) class);
+ val these_classparams = these o try (#params o AxClass.get_info thy);
+ val classparams = these_classparams class;
+ val further_classparams = maps these_classparams
+ ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
@@ -639,8 +647,11 @@
##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> fold_map translate_super_instance super_classes
##>> fold_map translate_classparam_instance classparams
- #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
- Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
+ ##>> fold_map translate_classparam_instance further_classparams
+ #>> (fn (((((class, tyco), arity_args), super_instances),
+ classparam_instances), further_classparam_instances) =>
+ Classinst ((class, (tyco, arity_args)), (super_instances,
+ (classparam_instances, further_classparam_instances))));
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
@@ -684,15 +695,15 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val tys = Sign.const_typargs thy (c, ty);
+ val arg_typs = Sign.const_typargs thy (c, ty);
val sorts = Code_Preproc.sortargs eqngr c;
- val tys_args = (fst o Term.strip_type) ty;
+ val function_typs = (fst o Term.strip_type) ty;
in
ensure_const thy algbr eqngr permissive c
- ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
- ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (tys ~~ sorts)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) tys_args
- #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
+ ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
+ #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
--- a/src/Tools/nbe.ML Fri Jun 18 14:14:29 2010 +0200
+++ b/src/Tools/nbe.ML Fri Jun 18 14:14:42 2010 +0200
@@ -417,7 +417,7 @@
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), ((super_instances, _), classparam_instances))) =
+ | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
[(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];