--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:05:56 2012 +0200
@@ -633,8 +633,12 @@
(*assumption: dummy values are not relevant for serialization*)
val (unitt, unitT) = case lookup_const naming @{const_name Unity}
of SOME unit' =>
- let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
- in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
+ let
+ val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
+ in
+ (IConst { name = unit', typargs = [], dicts = [], dom = [],
+ range = unitT, annotate = false }, unitT)
+ end
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
@@ -643,21 +647,21 @@
val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
- fun force (t as IConst (c, _) `$ t') = if is_return c
+ fun force (t as IConst { name = c, ... } `$ t') = if is_return c
then t' else t `$ unitt
| force t = t `$ unitt;
fun tr_bind'' [(t1, _), (t2, ty2)] =
let
val ((v, ty), t) = dest_abs (t2, ty2);
- in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
+ in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
and tr_bind' t = case unfold_app t
- of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
+ of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
- fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
- [(unitt, tr_bind'' ts)]), dummy_case_term)
- fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
+ fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
+ ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
+ fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
@@ -668,10 +672,9 @@
of (IConst const, ts) => imp_monad_bind' const ts
| (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
| imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
- | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
- (((imp_monad_bind t, ty),
- (map o pairself) imp_monad_bind pats),
- imp_monad_bind t0);
+ | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
+ ICase { term = imp_monad_bind t, typ = ty,
+ clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
@@ -688,3 +691,4 @@
hide_const (open) Heap heap guard raise' fold_map
end
+
--- a/src/HOL/Tools/list_code.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/list_code.ML Tue Jun 05 07:05:56 2012 +0200
@@ -20,14 +20,14 @@
fun implode_list nil' cons' t =
let
- fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
+ fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
if c = cons'
then SOME (t1, t2)
else NONE
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst (c, _) => if c = nil' then SOME ts else NONE
+ of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
| _ => NONE
end;
--- a/src/HOL/Tools/numeral.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Jun 05 07:05:56 2012 +0200
@@ -69,11 +69,11 @@
let
fun dest_numeral one' bit0' bit1' thm t =
let
- fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+ fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
else if c = bit1' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
| dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
- fun dest_num (IConst (c, _)) = if c = one' then 1
+ fun dest_num (IConst { name = c, ... }) = if c = one' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
--- a/src/HOL/Tools/string_code.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/string_code.ML Tue Jun 05 07:05:56 2012 +0200
@@ -23,13 +23,13 @@
| decode _ ~1 = NONE
| decode n m = SOME (chr (n * 16 + m));
in case tt
- of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
+ of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
| _ => NONE
end;
fun implode_string char' nibbles' mk_char mk_string ts =
let
- fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+ fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
if c = char' then decode_char nibbles' (t1, t2) else NONE
| implode_char _ = NONE;
val ts' = map_filter implode_char ts;
--- a/src/Tools/Code/code_haskell.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 05 07:05:56 2012 +0200
@@ -60,8 +60,8 @@
print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
fun print_typscheme tyvars (vs, ty) =
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
- fun print_term tyvars some_thm vars fxy (IConst c) =
- print_app tyvars some_thm vars fxy (c, [])
+ fun print_term tyvars some_thm vars fxy (IConst const) =
+ print_app tyvars some_thm vars fxy (const, [])
| print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app tyvars some_thm vars fxy app
@@ -79,15 +79,15 @@
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
- | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- 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, ((_, (arg_tys, result_ty)), annotate)), ts) =
+ | print_term tyvars some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case tyvars some_thm vars fxy case_expr
+ else print_app tyvars some_thm vars fxy app
+ | NONE => print_case tyvars some_thm vars fxy case_expr)
+ and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
let
- val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+ val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
val printed_const =
if annotate then
brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
@@ -98,9 +98,11 @@
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
- and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+ (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
+ | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match ((pat, _), t) vars =
vars
|> print_bind tyvars some_thm BR pat
@@ -110,7 +112,7 @@
ps
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
end
- | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
@@ -119,9 +121,7 @@
in Pretty.block_enclose
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
- end
- | print_case tyvars some_thm vars fxy ((_, []), _) =
- (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
+ end;
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
let
val tyvars = intro_vars (map fst vs) reserved;
@@ -221,7 +221,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, inst_params, ... }) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun requires_args classparam = case const_syntax classparam
@@ -237,14 +237,15 @@
]
| SOME k =>
let
- val (c, ((_, tys), _)) = const;
+ val { name = c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+ val lhs = IConst { name = classparam, typargs = [],
+ dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
(*dictionaries are not relevant at this late stage,
and these consts never need type annotations for disambiguation *)
in
@@ -264,7 +265,7 @@
str " where {"
],
str "};"
- ) (map print_classparam_instance classparam_instances)
+ ) (map print_classparam_instance inst_params)
end;
in print_stmt end;
@@ -407,7 +408,7 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
+ fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t
--- a/src/Tools/Code/code_ml.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 05 07:05:56 2012 +0200
@@ -28,9 +28,10 @@
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
- * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
+ | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
@@ -83,15 +84,15 @@
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
- print_app is_pseudo_fun some_thm vars fxy (c, [])
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+ print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ of SOME app => print_app is_pseudo_fun some_thm vars fxy app
| NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
print_term is_pseudo_fun some_thm vars BR t2])
| print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -102,15 +103,15 @@
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map print_abs binds vars;
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
- | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- 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), (arg_tys, _)), _)), ts)) =
+ | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case is_pseudo_fun some_thm vars fxy case_expr
+ else print_app is_pseudo_fun some_thm vars fxy app
+ | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
if is_cons c then
- let val k = length arg_tys in
+ let val k = length dom in
if k < 2 orelse length ts = k
then (str o deresolve) c
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -118,14 +119,16 @@
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+ else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+ (concat o map str) ["raise", "Fail", "\"empty case\""]
+ | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
@@ -139,7 +142,7 @@
str "end"
]
end
- | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
let
fun print_select delim (pat, body) =
let
@@ -154,9 +157,7 @@
:: print_select "of" clause
:: map (print_select "|") clauses
)
- end
- | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
- (concat o map str) ["raise", "Fail", "\"empty case\""];
+ end;
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -206,7 +207,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+ (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
let
fun print_super_instance (_, (classrel, x)) =
concat [
@@ -230,8 +231,8 @@
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
- (map print_super_instance super_instances
- @ map print_classparam_instance classparam_instances)
+ (map print_super_instance superinsts
+ @ map print_classparam_instance inst_params)
:: str ":"
@@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
))
@@ -386,15 +387,15 @@
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
- print_app is_pseudo_fun some_thm vars fxy (c, [])
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+ print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ of SOME app => print_app is_pseudo_fun some_thm vars fxy app
| NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
print_term is_pseudo_fun some_thm vars BR t2])
| print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -402,15 +403,15 @@
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
- | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- 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)) =
+ | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case is_pseudo_fun some_thm vars fxy case_expr
+ else print_app is_pseudo_fun some_thm vars fxy app
+ | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
if is_cons c then
- let val k = length tys in
+ let val k = length dom in
if length ts = k
then (str o deresolve) c
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -418,14 +419,16 @@
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+ else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+ (concat o map str) ["failwith", "\"empty case\""]
+ | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_let ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
@@ -436,7 +439,7 @@
brackify_block fxy (Pretty.chunks ps) []
(print_term is_pseudo_fun some_thm vars' NOBR body)
end
- | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
let
fun print_select delim (pat, body) =
let
@@ -449,9 +452,7 @@
:: print_select "with" clause
:: map (print_select "|") clauses
)
- end
- | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
- (concat o map str) ["failwith", "\"empty case\""];
+ end;
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -546,7 +547,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+ (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
let
fun print_super_instance (_, (classrel, x)) =
concat [
@@ -570,8 +571,8 @@
else print_dict_args vs)
@ str "="
@@ brackets [
- enum_default "()" ";" "{" "}" (map print_super_instance super_instances
- @ map print_classparam_instance classparam_instances),
+ enum_default "()" ";" "{" "}" (map print_super_instance superinsts
+ @ map print_classparam_instance inst_params),
str ":",
print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
]
@@ -731,7 +732,7 @@
| _ => (eqs, NONE)
else (eqs, NONE)
in (ML_Function (name, (tysm, eqs')), some_value_name) end
- | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
+ | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
(ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
| ml_binding_of_stmt (name, _) =
error ("Binding block containing illegal statement: " ^ labelled_name name)
--- a/src/Tools/Code/code_printer.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 05 07:05:56 2012 +0200
@@ -315,7 +315,7 @@
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
+ (app as ({ name = c, dom, ... }, ts)) =
case const_syntax c of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
| SOME (Complex_const_syntax (k, print)) =>
let
fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
in
if k = length ts
then print' fxy ts
--- a/src/Tools/Code/code_scala.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 05 07:05:56 2012 +0200
@@ -46,8 +46,8 @@
fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
fun print_var vars NONE = str "_"
| print_var vars (SOME v) = (str o lookup_var vars) v
- fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
- print_app tyvars is_pat some_thm vars fxy (c, [])
+ fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
+ print_app tyvars is_pat some_thm vars fxy (const, [])
| print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app tyvars is_pat some_thm vars fxy app
@@ -65,30 +65,30 @@
print_term tyvars false some_thm vars' NOBR t
]
end
- | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- 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)
+ | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case tyvars some_thm vars fxy case_expr
+ else print_app tyvars is_pat some_thm vars fxy app
+ | NONE => print_case tyvars some_thm vars fxy case_expr)
and print_app tyvars is_pat some_thm vars fxy
- (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
+ (app as ({ name = c, typargs, dom, ... }, ts)) =
let
val k = length ts;
- val tys' = if is_pat orelse
- (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
+ val typargs' = if is_pat orelse
+ (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
val (l, print') = case const_syntax c
of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR ((str o deresolve) c) tys') ts)
+ NOBR ((str o deresolve) c) typargs') ts)
| SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR (str s) tys') ts)
+ NOBR (str s) typargs') ts)
| SOME (Complex_const_syntax (k, print)) =>
(k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
- (ts ~~ take k arg_tys))
+ (ts ~~ take k dom))
in if k = l then print' fxy ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -100,9 +100,11 @@
end end
and print_bind tyvars some_thm fxy p =
gen_print_bind (print_term tyvars true) some_thm fxy p
- and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+ (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
+ | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match_val ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
@@ -123,7 +125,7 @@
| insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
(if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
- | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
@@ -135,9 +137,7 @@
|> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
|> single
|> enclose "(" ")"
- end
- | print_case tyvars some_thm vars fxy ((_, []), _) =
- (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
+ end;
fun print_context tyvars vs name = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
@@ -261,19 +261,19 @@
:: map print_classparam_def classparams
)
end
- | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
- (super_instances, (classparam_instances, further_classparam_instances)))) =
+ | print_stmt (name, Code_Thingol.Classinst
+ { class, tyco, vs, inst_params, superinst_params, ... }) =
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
- fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
+ fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
let
- val aux_tys = Name.invent_names (snd reserved) "a" tys;
- val auxs = map fst aux_tys;
+ val aux_dom = Name.invent_names (snd reserved) "a" dom;
+ val auxs = map fst aux_dom;
val vars = intro_vars auxs reserved;
val aux_abstr = if null auxs then [] else [enum "," "(" ")"
(map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
+ (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
in
concat ([str "val", print_method classparam, str "="]
@ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
@@ -283,7 +283,7 @@
Pretty.block_enclose (concat [str "implicit def",
constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
- (map print_classparam_instance (classparam_instances @ further_classparam_instances))
+ (map print_classparam_instance (inst_params @ superinst_params))
end;
in print_stmt end;
--- a/src/Tools/Code/code_simp.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_simp.ML Tue Jun 05 07:05:56 2012 +0200
@@ -38,8 +38,8 @@
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
ss addsimps (map_filter (fst o snd)) eqs
|> fold Simplifier.add_cong (the_list some_cong)
- | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
- ss addsimps (map (fst o snd) classparam_instances)
+ | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
+ ss addsimps (map (fst o snd) inst_params)
| add_stmt _ ss = ss;
val add_program = Graph.fold (add_stmt o fst o snd);
--- a/src/Tools/Code/code_thingol.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 05 07:05:56 2012 +0200
@@ -18,19 +18,18 @@
Dict of string list * plain_dict
and plain_dict =
Dict_Const of string * dict list list
- | Dict_Var of vname * (int * int)
+ | Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
- (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
+ type const = { name: string, typargs: itype list, dicts: dict list list,
+ dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
- | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
- (*((term, type), [(selector pattern, body term )]), primitive term)*)
+ | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
val `$$ : iterm * iterm list -> iterm;
val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
@@ -77,10 +76,10 @@
| 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*)
- * (((string * const) * (thm * bool)) list (*class parameter instances*)
- * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
+ | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
type program = stmt Graph.T
val empty_funs: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -126,7 +125,7 @@
case dest x
of NONE => ([], x)
| SOME (x1, x2) =>
- let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
+ let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
(** language core - types, terms **)
@@ -137,21 +136,21 @@
Dict of string list * plain_dict
and plain_dict =
Dict_Const of string * dict list list
- | Dict_Var of vname * (int * int)
+ | Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
-type const = string * (((itype list * dict list list) *
- (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
+type const = { name: string, typargs: itype list, dicts: dict list list,
+ dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
- | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+ | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
(*see also signature*)
fun is_IVar (IVar _) = true
@@ -172,7 +171,7 @@
| _ => NONE);
val split_let =
- (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
+ (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
| _ => NONE);
val unfold_let = unfoldr split_let;
@@ -188,16 +187,16 @@
| fold' (IVar _) = I
| fold' (t1 `$ t2) = fold' t1 #> fold' t2
| fold' (_ `|=> t) = fold' t
- | fold' (ICase (((t, _), ds), _)) = fold' t
- #> fold (fn (pat, body) => fold' pat #> fold' body) ds
+ | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
+ #> fold (fn (p, body) => fold' p #> fold' body) clauses
in fold' end;
-val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
+val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
-val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
fun fold_varnames f =
let
@@ -209,7 +208,7 @@
| fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
| fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
| fold_term vs ((NONE, _) `|=> t) = fold_term vs t
- | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
+ | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
and fold_case vs (p, t) = fold_term (add p vs) t;
in fold_term [] end;
fun add t = fold_aux add (insert (op =)) t;
@@ -219,9 +218,9 @@
fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
| split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
- of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
- if v = w andalso (exists_var p v orelse not (exists_var t' v))
- then ((p, ty), t')
+ of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
+ if v = w andalso (exists_var p v orelse not (exists_var body v))
+ then ((p, ty), body)
else ((IVar (SOME v), ty), t)
| _ => ((IVar (SOME v), ty), t))
| split_pat_abs _ = NONE;
@@ -239,27 +238,27 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
+fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
let
val j = length ts;
val l = k - j;
val _ = if l > length tys
- then error ("Impossible eta-expansion for constant " ^ quote name) else ();
+ then error ("Impossible eta-expansion for constant " ^ quote c) else ();
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
(Name.invent_names ctxt "a" ((take l o drop j) tys));
- in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
+ in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
let
fun cont_dict (Dict (_, d)) = cont_plain_dict d
and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
| cont_plain_dict (Dict_Var _) = true;
- fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
+ fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
| cont_term (IVar _) = false
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
| cont_term (_ `|=> t) = cont_term t
- | cont_term (ICase (_, t)) = cont_term t;
+ | cont_term (ICase { primitive = t, ... }) = cont_term t;
in cont_term t end;
@@ -427,11 +426,10 @@
| 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
- * (((string * const) * (thm * bool)) list
- * ((string * const) * (thm * bool)) list))
- (*see also signature*);
+ | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
type program = stmt Graph.T;
@@ -444,9 +442,10 @@
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
| map_terms_bottom_up f ((v, ty) `|=> t) = f
((v, ty) `|=> map_terms_bottom_up f t)
- | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
- (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
- (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
+ | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
+ (ICase { term = map_terms_bottom_up f t, typ = ty,
+ clauses = (map o pairself) (map_terms_bottom_up f) clauses,
+ primitive = 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')
@@ -459,8 +458,11 @@
| 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, classparam_instances))) =
- Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
+ | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
+ inst_params, superinst_params }) =
+ Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
+ inst_params = map_classparam_instances_as_term f inst_params,
+ superinst_params = map_classparam_instances_as_term f superinst_params };
fun is_cons program name = case Graph.get_node program name
of Datatypecons _ => true
@@ -484,7 +486,7 @@
quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
end
| Classparam (c, _) => quote (Code.string_of_const thy c)
- | Classinst ((class, (tyco, _)), _) =>
+ | Classinst { class, tyco, ... } =>
let
val Class (class, _) = Graph.get_node program class;
val Datatype (tyco, _) = Graph.get_node program tyco;
@@ -678,9 +680,9 @@
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 these_classparams = these o try (#params o AxClass.get_info thy);
- val classparams = these_classparams class;
- val further_classparams = maps these_classparams
+ val these_class_params = these o try (#params o AxClass.get_info thy);
+ val class_params = these_class_params class;
+ val superclass_params = maps these_class_params
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -710,12 +712,11 @@
##>> ensure_tyco thy algbr eqngr permissive tyco
##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> fold_map translate_super_instance super_classes
- ##>> fold_map translate_classparam_instance classparams
- ##>> 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))));
+ ##>> fold_map translate_classparam_instance class_params
+ ##>> fold_map translate_classparam_instance superclass_params
+ #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
+ Classinst { class = class, tyco = tyco, vs = vs,
+ superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
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))
@@ -759,17 +760,18 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val (annotate, ty') = dest_tagged_type ty
- val arg_typs = Sign.const_typargs thy (c, ty');
+ val (annotate, ty') = dest_tagged_type ty;
+ val typargs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
- val (function_typs, body_typ) = Term.strip_type ty';
+ val (dom, range) = Term.strip_type ty';
in
ensure_const thy algbr eqngr permissive c
- ##>> 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) (body_typ :: function_typs)
- #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
- IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
+ ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
+ #>> (fn (((c, typargs), dss), range :: dom) =>
+ IConst { name = c, typargs = typargs, dicts = dss,
+ dom = dom, range = range, annotate = annotate })
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)
@@ -788,22 +790,22 @@
val constrs =
if null case_pats then []
else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
- fun casify naming constrs ty ts =
+ fun casify naming constrs ty t_app ts =
let
val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
fun collapse_clause vs_map ts body =
let
in case body
- of IConst (c, _) => if member (op =) undefineds c
+ of IConst { name = c, ... } => if member (op =) undefineds c
then []
else [(ts, body)]
- | ICase (((IVar (SOME v), _), subclauses), _) =>
+ | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
if forall (fn (pat', body') => exists_var pat' v
- orelse not (exists_var body' v)) subclauses
+ orelse not (exists_var body' v)) clauses
then case AList.lookup (op =) vs_map v
of SOME i => maps (fn (pat', body') =>
collapse_clause (AList.delete (op =) v vs_map)
- (nth_map i (K pat') ts) body') subclauses
+ (nth_map i (K pat') ts) body') clauses
| NONE => [(ts, body)]
else [(ts, body)]
| _ => [(ts, body)]
@@ -818,11 +820,11 @@
val ts_clause = nth_drop t_pos ts;
val clauses = if null case_pats
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
- else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
+ else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
(constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
(case_pats ~~ ts_clause)));
- in ((t, ty), clauses) end;
+ in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
in
translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
@@ -830,7 +832,7 @@
##>> translate_typ thy algbr eqngr permissive ty
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
#-> (fn (((t, constrs), ty), ts) =>
- `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
+ `(fn (_, (naming, _)) => casify naming constrs ty t ts))
end
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
--- a/src/Tools/nbe.ML Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/nbe.ML Tue Jun 05 07:05:56 2012 +0200
@@ -314,13 +314,13 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
+ and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
- | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
+ | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
nbe_apps (ml_cases (of_iterm NONE t)
- (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
+ (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
@ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
in of_iterm end;
@@ -345,7 +345,7 @@
|> subst_vars t1
||>> subst_vars t2
|>> (op `$)
- | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
+ | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
val (args', _) = fold_map subst_vars args samepairs;
in (samepairs, args') end;
@@ -410,6 +410,10 @@
(* extract equations from statements *)
+fun dummy_const c dss =
+ IConst { name = c, typargs = [], dicts = dss,
+ dom = [], range = ITyVar "", annotate = false };
+
fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
| eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
@@ -424,17 +428,17 @@
val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
+ [([dummy_const class [] `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
- [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
- map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
- @ map (IConst o snd o fst) classparam_instances)]))];
+ | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
+ [(inst, (vs, [([], dummy_const class [] `$$
+ map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
+ @ map (IConst o snd o fst) inst_params)]))];
(* compile whole programs *)