1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jun 04 12:55:54 2012 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:05:56 2012 +0200
1.3 @@ -633,8 +633,12 @@
1.4 (*assumption: dummy values are not relevant for serialization*)
1.5 val (unitt, unitT) = case lookup_const naming @{const_name Unity}
1.6 of SOME unit' =>
1.7 - let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
1.8 - in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
1.9 + let
1.10 + val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
1.11 + in
1.12 + (IConst { name = unit', typargs = [], dicts = [], dom = [],
1.13 + range = unitT, annotate = false }, unitT)
1.14 + end
1.15 | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
1.16 fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
1.17 | dest_abs (t, ty) =
1.18 @@ -643,21 +647,21 @@
1.19 val v = singleton (Name.variant_list vs) "x";
1.20 val ty' = (hd o fst o unfold_fun) ty;
1.21 in ((SOME v, ty'), t `$ IVar (SOME v)) end;
1.22 - fun force (t as IConst (c, _) `$ t') = if is_return c
1.23 + fun force (t as IConst { name = c, ... } `$ t') = if is_return c
1.24 then t' else t `$ unitt
1.25 | force t = t `$ unitt;
1.26 fun tr_bind'' [(t1, _), (t2, ty2)] =
1.27 let
1.28 val ((v, ty), t) = dest_abs (t2, ty2);
1.29 - in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
1.30 + in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
1.31 and tr_bind' t = case unfold_app t
1.32 - of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
1.33 + of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
1.34 then tr_bind'' [(x1, ty1), (x2, ty2)]
1.35 else force t
1.36 | _ => force t;
1.37 - fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
1.38 - [(unitt, tr_bind'' ts)]), dummy_case_term)
1.39 - fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
1.40 + fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
1.41 + ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
1.42 + fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
1.43 of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
1.44 | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
1.45 | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
1.46 @@ -668,10 +672,9 @@
1.47 of (IConst const, ts) => imp_monad_bind' const ts
1.48 | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
1.49 | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
1.50 - | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
1.51 - (((imp_monad_bind t, ty),
1.52 - (map o pairself) imp_monad_bind pats),
1.53 - imp_monad_bind t0);
1.54 + | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
1.55 + ICase { term = imp_monad_bind t, typ = ty,
1.56 + clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
1.57
1.58 in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
1.59
1.60 @@ -688,3 +691,4 @@
1.61 hide_const (open) Heap heap guard raise' fold_map
1.62
1.63 end
1.64 +
2.1 --- a/src/HOL/Tools/list_code.ML Mon Jun 04 12:55:54 2012 +0200
2.2 +++ b/src/HOL/Tools/list_code.ML Tue Jun 05 07:05:56 2012 +0200
2.3 @@ -20,14 +20,14 @@
2.4
2.5 fun implode_list nil' cons' t =
2.6 let
2.7 - fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
2.8 + fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
2.9 if c = cons'
2.10 then SOME (t1, t2)
2.11 else NONE
2.12 | dest_cons _ = NONE;
2.13 val (ts, t') = Code_Thingol.unfoldr dest_cons t;
2.14 in case t'
2.15 - of IConst (c, _) => if c = nil' then SOME ts else NONE
2.16 + of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
2.17 | _ => NONE
2.18 end;
2.19
3.1 --- a/src/HOL/Tools/numeral.ML Mon Jun 04 12:55:54 2012 +0200
3.2 +++ b/src/HOL/Tools/numeral.ML Tue Jun 05 07:05:56 2012 +0200
3.3 @@ -69,11 +69,11 @@
3.4 let
3.5 fun dest_numeral one' bit0' bit1' thm t =
3.6 let
3.7 - fun dest_bit (IConst (c, _)) = if c = bit0' then 0
3.8 + fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
3.9 else if c = bit1' then 1
3.10 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
3.11 | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
3.12 - fun dest_num (IConst (c, _)) = if c = one' then 1
3.13 + fun dest_num (IConst { name = c, ... }) = if c = one' then 1
3.14 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
3.15 | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
3.16 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
4.1 --- a/src/HOL/Tools/string_code.ML Mon Jun 04 12:55:54 2012 +0200
4.2 +++ b/src/HOL/Tools/string_code.ML Tue Jun 05 07:05:56 2012 +0200
4.3 @@ -23,13 +23,13 @@
4.4 | decode _ ~1 = NONE
4.5 | decode n m = SOME (chr (n * 16 + m));
4.6 in case tt
4.7 - of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
4.8 + of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
4.9 | _ => NONE
4.10 end;
4.11
4.12 fun implode_string char' nibbles' mk_char mk_string ts =
4.13 let
4.14 - fun implode_char (IConst (c, _) `$ t1 `$ t2) =
4.15 + fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
4.16 if c = char' then decode_char nibbles' (t1, t2) else NONE
4.17 | implode_char _ = NONE;
4.18 val ts' = map_filter implode_char ts;
5.1 --- a/src/Tools/Code/code_haskell.ML Mon Jun 04 12:55:54 2012 +0200
5.2 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 05 07:05:56 2012 +0200
5.3 @@ -60,8 +60,8 @@
5.4 print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
5.5 fun print_typscheme tyvars (vs, ty) =
5.6 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
5.7 - fun print_term tyvars some_thm vars fxy (IConst c) =
5.8 - print_app tyvars some_thm vars fxy (c, [])
5.9 + fun print_term tyvars some_thm vars fxy (IConst const) =
5.10 + print_app tyvars some_thm vars fxy (const, [])
5.11 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
5.12 (case Code_Thingol.unfold_const_app t
5.13 of SOME app => print_app tyvars some_thm vars fxy app
5.14 @@ -79,15 +79,15 @@
5.15 val (binds, t') = Code_Thingol.unfold_pat_abs t;
5.16 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
5.17 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
5.18 - | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
5.19 - (case Code_Thingol.unfold_const_app t0
5.20 - of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
5.21 - then print_case tyvars some_thm vars fxy cases
5.22 - else print_app tyvars some_thm vars fxy c_ts
5.23 - | NONE => print_case tyvars some_thm vars fxy cases)
5.24 - and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
5.25 + | print_term tyvars some_thm vars fxy (ICase case_expr) =
5.26 + (case Code_Thingol.unfold_const_app (#primitive case_expr)
5.27 + of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
5.28 + then print_case tyvars some_thm vars fxy case_expr
5.29 + else print_app tyvars some_thm vars fxy app
5.30 + | NONE => print_case tyvars some_thm vars fxy case_expr)
5.31 + and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
5.32 let
5.33 - val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
5.34 + val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
5.35 val printed_const =
5.36 if annotate then
5.37 brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
5.38 @@ -98,9 +98,11 @@
5.39 end
5.40 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
5.41 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
5.42 - and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
5.43 + and print_case tyvars some_thm vars fxy { clauses = [], ... } =
5.44 + (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
5.45 + | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
5.46 let
5.47 - val (binds, body) = Code_Thingol.unfold_let (ICase cases);
5.48 + val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
5.49 fun print_match ((pat, _), t) vars =
5.50 vars
5.51 |> print_bind tyvars some_thm BR pat
5.52 @@ -110,7 +112,7 @@
5.53 ps
5.54 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
5.55 end
5.56 - | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
5.57 + | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
5.58 let
5.59 fun print_select (pat, body) =
5.60 let
5.61 @@ -119,9 +121,7 @@
5.62 in Pretty.block_enclose
5.63 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
5.64 (map print_select clauses)
5.65 - end
5.66 - | print_case tyvars some_thm vars fxy ((_, []), _) =
5.67 - (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
5.68 + end;
5.69 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
5.70 let
5.71 val tyvars = intro_vars (map fst vs) reserved;
5.72 @@ -221,7 +221,7 @@
5.73 str "};"
5.74 ) (map print_classparam classparams)
5.75 end
5.76 - | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
5.77 + | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
5.78 let
5.79 val tyvars = intro_vars (map fst vs) reserved;
5.80 fun requires_args classparam = case const_syntax classparam
5.81 @@ -237,14 +237,15 @@
5.82 ]
5.83 | SOME k =>
5.84 let
5.85 - val (c, ((_, tys), _)) = const;
5.86 + val { name = c, dom, range, ... } = const;
5.87 val (vs, rhs) = (apfst o map) fst
5.88 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
5.89 val s = if (is_some o const_syntax) c
5.90 then NONE else (SOME o Long_Name.base_name o deresolve) c;
5.91 val vars = reserved
5.92 |> intro_vars (map_filter I (s :: vs));
5.93 - val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
5.94 + val lhs = IConst { name = classparam, typargs = [],
5.95 + dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
5.96 (*dictionaries are not relevant at this late stage,
5.97 and these consts never need type annotations for disambiguation *)
5.98 in
5.99 @@ -264,7 +265,7 @@
5.100 str " where {"
5.101 ],
5.102 str "};"
5.103 - ) (map print_classparam_instance classparam_instances)
5.104 + ) (map print_classparam_instance inst_params)
5.105 end;
5.106 in print_stmt end;
5.107
5.108 @@ -407,7 +408,7 @@
5.109 of SOME ((pat, ty), t') =>
5.110 SOME ((SOME ((pat, ty), true), t1), t')
5.111 | NONE => NONE;
5.112 - fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
5.113 + fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
5.114 if c = c_bind_name then dest_bind t1 t2
5.115 else NONE
5.116 | dest_monad _ t = case Code_Thingol.split_let t
6.1 --- a/src/Tools/Code/code_ml.ML Mon Jun 04 12:55:54 2012 +0200
6.2 +++ b/src/Tools/Code/code_ml.ML Tue Jun 05 07:05:56 2012 +0200
6.3 @@ -28,9 +28,10 @@
6.4
6.5 datatype ml_binding =
6.6 ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
6.7 - | ML_Instance of string * ((class * (string * (vname * sort) list))
6.8 - * ((class * (string * (string * dict list list))) list
6.9 - * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
6.10 + | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
6.11 + superinsts: (class * (string * (string * dict list list))) list,
6.12 + inst_params: ((string * const) * (thm * bool)) list,
6.13 + superinst_params: ((string * const) * (thm * bool)) list };
6.14
6.15 datatype ml_stmt =
6.16 ML_Exc of string * (typscheme * int)
6.17 @@ -83,15 +84,15 @@
6.18 and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
6.19 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
6.20 (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
6.21 - fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
6.22 - print_app is_pseudo_fun some_thm vars fxy (c, [])
6.23 + fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
6.24 + print_app is_pseudo_fun some_thm vars fxy (const, [])
6.25 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
6.26 str "_"
6.27 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
6.28 str (lookup_var vars v)
6.29 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
6.30 (case Code_Thingol.unfold_const_app t
6.31 - of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
6.32 + of SOME app => print_app is_pseudo_fun some_thm vars fxy app
6.33 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
6.34 print_term is_pseudo_fun some_thm vars BR t2])
6.35 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
6.36 @@ -102,15 +103,15 @@
6.37 #>> (fn p => concat [str "fn", p, str "=>"]);
6.38 val (ps, vars') = fold_map print_abs binds vars;
6.39 in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
6.40 - | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
6.41 - (case Code_Thingol.unfold_const_app t0
6.42 - of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
6.43 - then print_case is_pseudo_fun some_thm vars fxy cases
6.44 - else print_app is_pseudo_fun some_thm vars fxy c_ts
6.45 - | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
6.46 - and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
6.47 + | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
6.48 + (case Code_Thingol.unfold_const_app (#primitive case_expr)
6.49 + of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
6.50 + then print_case is_pseudo_fun some_thm vars fxy case_expr
6.51 + else print_app is_pseudo_fun some_thm vars fxy app
6.52 + | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
6.53 + and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
6.54 if is_cons c then
6.55 - let val k = length arg_tys in
6.56 + let val k = length dom in
6.57 if k < 2 orelse length ts = k
6.58 then (str o deresolve) c
6.59 :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
6.60 @@ -118,14 +119,16 @@
6.61 end
6.62 else if is_pseudo_fun c
6.63 then (str o deresolve) c @@ str "()"
6.64 - else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
6.65 + else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
6.66 @ map (print_term is_pseudo_fun some_thm vars BR) ts
6.67 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
6.68 (print_term is_pseudo_fun) const_syntax some_thm vars
6.69 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
6.70 - and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
6.71 + and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
6.72 + (concat o map str) ["raise", "Fail", "\"empty case\""]
6.73 + | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
6.74 let
6.75 - val (binds, body) = Code_Thingol.unfold_let (ICase cases);
6.76 + val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
6.77 fun print_match ((pat, _), t) vars =
6.78 vars
6.79 |> print_bind is_pseudo_fun some_thm NOBR pat
6.80 @@ -139,7 +142,7 @@
6.81 str "end"
6.82 ]
6.83 end
6.84 - | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
6.85 + | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
6.86 let
6.87 fun print_select delim (pat, body) =
6.88 let
6.89 @@ -154,9 +157,7 @@
6.90 :: print_select "of" clause
6.91 :: map (print_select "|") clauses
6.92 )
6.93 - end
6.94 - | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
6.95 - (concat o map str) ["raise", "Fail", "\"empty case\""];
6.96 + end;
6.97 fun print_val_decl print_typscheme (name, typscheme) = concat
6.98 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
6.99 fun print_datatype_decl definer (tyco, (vs, cos)) =
6.100 @@ -206,7 +207,7 @@
6.101 ))
6.102 end
6.103 | print_def is_pseudo_fun _ definer
6.104 - (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
6.105 + (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
6.106 let
6.107 fun print_super_instance (_, (classrel, x)) =
6.108 concat [
6.109 @@ -230,8 +231,8 @@
6.110 else print_dict_args vs)
6.111 @ str "="
6.112 :: enum "," "{" "}"
6.113 - (map print_super_instance super_instances
6.114 - @ map print_classparam_instance classparam_instances)
6.115 + (map print_super_instance superinsts
6.116 + @ map print_classparam_instance inst_params)
6.117 :: str ":"
6.118 @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
6.119 ))
6.120 @@ -386,15 +387,15 @@
6.121 and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
6.122 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
6.123 (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
6.124 - fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
6.125 - print_app is_pseudo_fun some_thm vars fxy (c, [])
6.126 + fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
6.127 + print_app is_pseudo_fun some_thm vars fxy (const, [])
6.128 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
6.129 str "_"
6.130 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
6.131 str (lookup_var vars v)
6.132 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
6.133 (case Code_Thingol.unfold_const_app t
6.134 - of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
6.135 + of SOME app => print_app is_pseudo_fun some_thm vars fxy app
6.136 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
6.137 print_term is_pseudo_fun some_thm vars BR t2])
6.138 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
6.139 @@ -402,15 +403,15 @@
6.140 val (binds, t') = Code_Thingol.unfold_pat_abs t;
6.141 val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
6.142 in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
6.143 - | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
6.144 - (case Code_Thingol.unfold_const_app t0
6.145 - of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
6.146 - then print_case is_pseudo_fun some_thm vars fxy cases
6.147 - else print_app is_pseudo_fun some_thm vars fxy c_ts
6.148 - | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
6.149 - and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
6.150 + | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
6.151 + (case Code_Thingol.unfold_const_app (#primitive case_expr)
6.152 + of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
6.153 + then print_case is_pseudo_fun some_thm vars fxy case_expr
6.154 + else print_app is_pseudo_fun some_thm vars fxy app
6.155 + | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
6.156 + and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
6.157 if is_cons c then
6.158 - let val k = length tys in
6.159 + let val k = length dom in
6.160 if length ts = k
6.161 then (str o deresolve) c
6.162 :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
6.163 @@ -418,14 +419,16 @@
6.164 end
6.165 else if is_pseudo_fun c
6.166 then (str o deresolve) c @@ str "()"
6.167 - else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
6.168 + else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
6.169 @ map (print_term is_pseudo_fun some_thm vars BR) ts
6.170 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
6.171 (print_term is_pseudo_fun) const_syntax some_thm vars
6.172 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
6.173 - and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
6.174 + and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
6.175 + (concat o map str) ["failwith", "\"empty case\""]
6.176 + | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
6.177 let
6.178 - val (binds, body) = Code_Thingol.unfold_let (ICase cases);
6.179 + val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
6.180 fun print_let ((pat, _), t) vars =
6.181 vars
6.182 |> print_bind is_pseudo_fun some_thm NOBR pat
6.183 @@ -436,7 +439,7 @@
6.184 brackify_block fxy (Pretty.chunks ps) []
6.185 (print_term is_pseudo_fun some_thm vars' NOBR body)
6.186 end
6.187 - | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
6.188 + | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
6.189 let
6.190 fun print_select delim (pat, body) =
6.191 let
6.192 @@ -449,9 +452,7 @@
6.193 :: print_select "with" clause
6.194 :: map (print_select "|") clauses
6.195 )
6.196 - end
6.197 - | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
6.198 - (concat o map str) ["failwith", "\"empty case\""];
6.199 + end;
6.200 fun print_val_decl print_typscheme (name, typscheme) = concat
6.201 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
6.202 fun print_datatype_decl definer (tyco, (vs, cos)) =
6.203 @@ -546,7 +547,7 @@
6.204 ))
6.205 end
6.206 | print_def is_pseudo_fun _ definer
6.207 - (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
6.208 + (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
6.209 let
6.210 fun print_super_instance (_, (classrel, x)) =
6.211 concat [
6.212 @@ -570,8 +571,8 @@
6.213 else print_dict_args vs)
6.214 @ str "="
6.215 @@ brackets [
6.216 - enum_default "()" ";" "{" "}" (map print_super_instance super_instances
6.217 - @ map print_classparam_instance classparam_instances),
6.218 + enum_default "()" ";" "{" "}" (map print_super_instance superinsts
6.219 + @ map print_classparam_instance inst_params),
6.220 str ":",
6.221 print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
6.222 ]
6.223 @@ -731,7 +732,7 @@
6.224 | _ => (eqs, NONE)
6.225 else (eqs, NONE)
6.226 in (ML_Function (name, (tysm, eqs')), some_value_name) end
6.227 - | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
6.228 + | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
6.229 (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
6.230 | ml_binding_of_stmt (name, _) =
6.231 error ("Binding block containing illegal statement: " ^ labelled_name name)
7.1 --- a/src/Tools/Code/code_printer.ML Mon Jun 04 12:55:54 2012 +0200
7.2 +++ b/src/Tools/Code/code_printer.ML Tue Jun 05 07:05:56 2012 +0200
7.3 @@ -315,7 +315,7 @@
7.4 |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
7.5
7.6 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
7.7 - (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
7.8 + (app as ({ name = c, dom, ... }, ts)) =
7.9 case const_syntax c of
7.10 NONE => brackify fxy (print_app_expr some_thm vars app)
7.11 | SOME (Plain_const_syntax (_, s)) =>
7.12 @@ -323,7 +323,7 @@
7.13 | SOME (Complex_const_syntax (k, print)) =>
7.14 let
7.15 fun print' fxy ts =
7.16 - print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
7.17 + print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
7.18 in
7.19 if k = length ts
7.20 then print' fxy ts
8.1 --- a/src/Tools/Code/code_scala.ML Mon Jun 04 12:55:54 2012 +0200
8.2 +++ b/src/Tools/Code/code_scala.ML Tue Jun 05 07:05:56 2012 +0200
8.3 @@ -46,8 +46,8 @@
8.4 fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
8.5 fun print_var vars NONE = str "_"
8.6 | print_var vars (SOME v) = (str o lookup_var vars) v
8.7 - fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
8.8 - print_app tyvars is_pat some_thm vars fxy (c, [])
8.9 + fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
8.10 + print_app tyvars is_pat some_thm vars fxy (const, [])
8.11 | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
8.12 (case Code_Thingol.unfold_const_app t
8.13 of SOME app => print_app tyvars is_pat some_thm vars fxy app
8.14 @@ -65,30 +65,30 @@
8.15 print_term tyvars false some_thm vars' NOBR t
8.16 ]
8.17 end
8.18 - | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
8.19 - (case Code_Thingol.unfold_const_app t0
8.20 - of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
8.21 - then print_case tyvars some_thm vars fxy cases
8.22 - else print_app tyvars is_pat some_thm vars fxy c_ts
8.23 - | NONE => print_case tyvars some_thm vars fxy cases)
8.24 + | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
8.25 + (case Code_Thingol.unfold_const_app (#primitive case_expr)
8.26 + of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
8.27 + then print_case tyvars some_thm vars fxy case_expr
8.28 + else print_app tyvars is_pat some_thm vars fxy app
8.29 + | NONE => print_case tyvars some_thm vars fxy case_expr)
8.30 and print_app tyvars is_pat some_thm vars fxy
8.31 - (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
8.32 + (app as ({ name = c, typargs, dom, ... }, ts)) =
8.33 let
8.34 val k = length ts;
8.35 - val tys' = if is_pat orelse
8.36 - (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
8.37 + val typargs' = if is_pat orelse
8.38 + (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
8.39 val (l, print') = case const_syntax c
8.40 of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
8.41 (print_term tyvars is_pat some_thm vars NOBR) fxy
8.42 (applify "[" "]" (print_typ tyvars NOBR)
8.43 - NOBR ((str o deresolve) c) tys') ts)
8.44 + NOBR ((str o deresolve) c) typargs') ts)
8.45 | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
8.46 (print_term tyvars is_pat some_thm vars NOBR) fxy
8.47 (applify "[" "]" (print_typ tyvars NOBR)
8.48 - NOBR (str s) tys') ts)
8.49 + NOBR (str s) typargs') ts)
8.50 | SOME (Complex_const_syntax (k, print)) =>
8.51 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
8.52 - (ts ~~ take k arg_tys))
8.53 + (ts ~~ take k dom))
8.54 in if k = l then print' fxy ts
8.55 else if k < l then
8.56 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
8.57 @@ -100,9 +100,11 @@
8.58 end end
8.59 and print_bind tyvars some_thm fxy p =
8.60 gen_print_bind (print_term tyvars true) some_thm fxy p
8.61 - and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
8.62 + and print_case tyvars some_thm vars fxy { clauses = [], ... } =
8.63 + (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
8.64 + | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
8.65 let
8.66 - val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
8.67 + val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
8.68 fun print_match_val ((pat, ty), t) vars =
8.69 vars
8.70 |> print_bind tyvars some_thm BR pat
8.71 @@ -123,7 +125,7 @@
8.72 | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
8.73 (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
8.74 in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
8.75 - | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
8.76 + | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
8.77 let
8.78 fun print_select (pat, body) =
8.79 let
8.80 @@ -135,9 +137,7 @@
8.81 |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
8.82 |> single
8.83 |> enclose "(" ")"
8.84 - end
8.85 - | print_case tyvars some_thm vars fxy ((_, []), _) =
8.86 - (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
8.87 + end;
8.88 fun print_context tyvars vs name = applify "[" "]"
8.89 (fn (v, sort) => (Pretty.block o map str)
8.90 (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
8.91 @@ -261,19 +261,19 @@
8.92 :: map print_classparam_def classparams
8.93 )
8.94 end
8.95 - | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
8.96 - (super_instances, (classparam_instances, further_classparam_instances)))) =
8.97 + | print_stmt (name, Code_Thingol.Classinst
8.98 + { class, tyco, vs, inst_params, superinst_params, ... }) =
8.99 let
8.100 val tyvars = intro_tyvars vs reserved;
8.101 val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
8.102 - fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
8.103 + fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
8.104 let
8.105 - val aux_tys = Name.invent_names (snd reserved) "a" tys;
8.106 - val auxs = map fst aux_tys;
8.107 + val aux_dom = Name.invent_names (snd reserved) "a" dom;
8.108 + val auxs = map fst aux_dom;
8.109 val vars = intro_vars auxs reserved;
8.110 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
8.111 (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
8.112 - (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
8.113 + (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
8.114 in
8.115 concat ([str "val", print_method classparam, str "="]
8.116 @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
8.117 @@ -283,7 +283,7 @@
8.118 Pretty.block_enclose (concat [str "implicit def",
8.119 constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
8.120 str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
8.121 - (map print_classparam_instance (classparam_instances @ further_classparam_instances))
8.122 + (map print_classparam_instance (inst_params @ superinst_params))
8.123 end;
8.124 in print_stmt end;
8.125
9.1 --- a/src/Tools/Code/code_simp.ML Mon Jun 04 12:55:54 2012 +0200
9.2 +++ b/src/Tools/Code/code_simp.ML Tue Jun 05 07:05:56 2012 +0200
9.3 @@ -38,8 +38,8 @@
9.4 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
9.5 ss addsimps (map_filter (fst o snd)) eqs
9.6 |> fold Simplifier.add_cong (the_list some_cong)
9.7 - | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
9.8 - ss addsimps (map (fst o snd) classparam_instances)
9.9 + | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
9.10 + ss addsimps (map (fst o snd) inst_params)
9.11 | add_stmt _ ss = ss;
9.12
9.13 val add_program = Graph.fold (add_stmt o fst o snd);
10.1 --- a/src/Tools/Code/code_thingol.ML Mon Jun 04 12:55:54 2012 +0200
10.2 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 05 07:05:56 2012 +0200
10.3 @@ -18,19 +18,18 @@
10.4 Dict of string list * plain_dict
10.5 and plain_dict =
10.6 Dict_Const of string * dict list list
10.7 - | Dict_Var of vname * (int * int)
10.8 + | Dict_Var of vname * (int * int);
10.9 datatype itype =
10.10 `%% of string * itype list
10.11 | ITyVar of vname;
10.12 - type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
10.13 - (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
10.14 + type const = { name: string, typargs: itype list, dicts: dict list list,
10.15 + dom: itype list, range: itype, annotate: bool };
10.16 datatype iterm =
10.17 IConst of const
10.18 | IVar of vname option
10.19 | `$ of iterm * iterm
10.20 | `|=> of (vname option * itype) * iterm
10.21 - | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
10.22 - (*((term, type), [(selector pattern, body term )]), primitive term)*)
10.23 + | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
10.24 val `$$ : iterm * iterm list -> iterm;
10.25 val `|==> : (vname option * itype) list * iterm -> iterm;
10.26 type typscheme = (vname * sort) list * itype;
10.27 @@ -77,10 +76,10 @@
10.28 | Class of class * (vname * ((class * string) list * (string * itype) list))
10.29 | Classrel of class * class
10.30 | Classparam of string * class
10.31 - | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
10.32 - * ((class * (string * (string * dict list list))) list (*super instances*)
10.33 - * (((string * const) * (thm * bool)) list (*class parameter instances*)
10.34 - * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
10.35 + | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
10.36 + superinsts: (class * (string * (string * dict list list))) list,
10.37 + inst_params: ((string * const) * (thm * bool)) list,
10.38 + superinst_params: ((string * const) * (thm * bool)) list };
10.39 type program = stmt Graph.T
10.40 val empty_funs: program -> string list
10.41 val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
10.42 @@ -126,7 +125,7 @@
10.43 case dest x
10.44 of NONE => ([], x)
10.45 | SOME (x1, x2) =>
10.46 - let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
10.47 + let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
10.48
10.49
10.50 (** language core - types, terms **)
10.51 @@ -137,21 +136,21 @@
10.52 Dict of string list * plain_dict
10.53 and plain_dict =
10.54 Dict_Const of string * dict list list
10.55 - | Dict_Var of vname * (int * int)
10.56 + | Dict_Var of vname * (int * int);
10.57
10.58 datatype itype =
10.59 `%% of string * itype list
10.60 | ITyVar of vname;
10.61
10.62 -type const = string * (((itype list * dict list list) *
10.63 - (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
10.64 +type const = { name: string, typargs: itype list, dicts: dict list list,
10.65 + dom: itype list, range: itype, annotate: bool };
10.66
10.67 datatype iterm =
10.68 IConst of const
10.69 | IVar of vname option
10.70 | `$ of iterm * iterm
10.71 | `|=> of (vname option * itype) * iterm
10.72 - | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
10.73 + | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
10.74 (*see also signature*)
10.75
10.76 fun is_IVar (IVar _) = true
10.77 @@ -172,7 +171,7 @@
10.78 | _ => NONE);
10.79
10.80 val split_let =
10.81 - (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
10.82 + (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
10.83 | _ => NONE);
10.84
10.85 val unfold_let = unfoldr split_let;
10.86 @@ -188,16 +187,16 @@
10.87 | fold' (IVar _) = I
10.88 | fold' (t1 `$ t2) = fold' t1 #> fold' t2
10.89 | fold' (_ `|=> t) = fold' t
10.90 - | fold' (ICase (((t, _), ds), _)) = fold' t
10.91 - #> fold (fn (pat, body) => fold' pat #> fold' body) ds
10.92 + | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
10.93 + #> fold (fn (p, body) => fold' p #> fold' body) clauses
10.94 in fold' end;
10.95
10.96 -val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
10.97 +val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
10.98
10.99 fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
10.100 | add_tycos (ITyVar _) = I;
10.101
10.102 -val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
10.103 +val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
10.104
10.105 fun fold_varnames f =
10.106 let
10.107 @@ -209,7 +208,7 @@
10.108 | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
10.109 | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
10.110 | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
10.111 - | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
10.112 + | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
10.113 and fold_case vs (p, t) = fold_term (add p vs) t;
10.114 in fold_term [] end;
10.115 fun add t = fold_aux add (insert (op =)) t;
10.116 @@ -219,9 +218,9 @@
10.117
10.118 fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
10.119 | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
10.120 - of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
10.121 - if v = w andalso (exists_var p v orelse not (exists_var t' v))
10.122 - then ((p, ty), t')
10.123 + of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
10.124 + if v = w andalso (exists_var p v orelse not (exists_var body v))
10.125 + then ((p, ty), body)
10.126 else ((IVar (SOME v), ty), t)
10.127 | _ => ((IVar (SOME v), ty), t))
10.128 | split_pat_abs _ = NONE;
10.129 @@ -239,27 +238,27 @@
10.130 val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
10.131 in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
10.132
10.133 -fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
10.134 +fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
10.135 let
10.136 val j = length ts;
10.137 val l = k - j;
10.138 val _ = if l > length tys
10.139 - then error ("Impossible eta-expansion for constant " ^ quote name) else ();
10.140 + then error ("Impossible eta-expansion for constant " ^ quote c) else ();
10.141 val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
10.142 val vs_tys = (map o apfst) SOME
10.143 (Name.invent_names ctxt "a" ((take l o drop j) tys));
10.144 - in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
10.145 + in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
10.146
10.147 fun contains_dict_var t =
10.148 let
10.149 fun cont_dict (Dict (_, d)) = cont_plain_dict d
10.150 and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
10.151 | cont_plain_dict (Dict_Var _) = true;
10.152 - fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
10.153 + fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
10.154 | cont_term (IVar _) = false
10.155 | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
10.156 | cont_term (_ `|=> t) = cont_term t
10.157 - | cont_term (ICase (_, t)) = cont_term t;
10.158 + | cont_term (ICase { primitive = t, ... }) = cont_term t;
10.159 in cont_term t end;
10.160
10.161
10.162 @@ -427,11 +426,10 @@
10.163 | Class of class * (vname * ((class * string) list * (string * itype) list))
10.164 | Classrel of class * class
10.165 | Classparam of string * class
10.166 - | Classinst of (class * (string * (vname * sort) list))
10.167 - * ((class * (string * (string * dict list list))) list
10.168 - * (((string * const) * (thm * bool)) list
10.169 - * ((string * const) * (thm * bool)) list))
10.170 - (*see also signature*);
10.171 + | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
10.172 + superinsts: (class * (string * (string * dict list list))) list,
10.173 + inst_params: ((string * const) * (thm * bool)) list,
10.174 + superinst_params: ((string * const) * (thm * bool)) list };
10.175
10.176 type program = stmt Graph.T;
10.177
10.178 @@ -444,9 +442,10 @@
10.179 (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
10.180 | map_terms_bottom_up f ((v, ty) `|=> t) = f
10.181 ((v, ty) `|=> map_terms_bottom_up f t)
10.182 - | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
10.183 - (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
10.184 - (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
10.185 + | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
10.186 + (ICase { term = map_terms_bottom_up f t, typ = ty,
10.187 + clauses = (map o pairself) (map_terms_bottom_up f) clauses,
10.188 + primitive = map_terms_bottom_up f t0 });
10.189
10.190 fun map_classparam_instances_as_term f =
10.191 (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
10.192 @@ -459,8 +458,11 @@
10.193 | map_terms_stmt f (stmt as Class _) = stmt
10.194 | map_terms_stmt f (stmt as Classrel _) = stmt
10.195 | map_terms_stmt f (stmt as Classparam _) = stmt
10.196 - | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
10.197 - Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
10.198 + | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
10.199 + inst_params, superinst_params }) =
10.200 + Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
10.201 + inst_params = map_classparam_instances_as_term f inst_params,
10.202 + superinst_params = map_classparam_instances_as_term f superinst_params };
10.203
10.204 fun is_cons program name = case Graph.get_node program name
10.205 of Datatypecons _ => true
10.206 @@ -484,7 +486,7 @@
10.207 quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
10.208 end
10.209 | Classparam (c, _) => quote (Code.string_of_const thy c)
10.210 - | Classinst ((class, (tyco, _)), _) =>
10.211 + | Classinst { class, tyco, ... } =>
10.212 let
10.213 val Class (class, _) = Graph.get_node program class;
10.214 val Datatype (tyco, _) = Graph.get_node program tyco;
10.215 @@ -678,9 +680,9 @@
10.216 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
10.217 let
10.218 val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
10.219 - val these_classparams = these o try (#params o AxClass.get_info thy);
10.220 - val classparams = these_classparams class;
10.221 - val further_classparams = maps these_classparams
10.222 + val these_class_params = these o try (#params o AxClass.get_info thy);
10.223 + val class_params = these_class_params class;
10.224 + val superclass_params = maps these_class_params
10.225 ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
10.226 val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
10.227 val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
10.228 @@ -710,12 +712,11 @@
10.229 ##>> ensure_tyco thy algbr eqngr permissive tyco
10.230 ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
10.231 ##>> fold_map translate_super_instance super_classes
10.232 - ##>> fold_map translate_classparam_instance classparams
10.233 - ##>> fold_map translate_classparam_instance further_classparams
10.234 - #>> (fn (((((class, tyco), arity_args), super_instances),
10.235 - classparam_instances), further_classparam_instances) =>
10.236 - Classinst ((class, (tyco, arity_args)), (super_instances,
10.237 - (classparam_instances, further_classparam_instances))));
10.238 + ##>> fold_map translate_classparam_instance class_params
10.239 + ##>> fold_map translate_classparam_instance superclass_params
10.240 + #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
10.241 + Classinst { class = class, tyco = tyco, vs = vs,
10.242 + superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
10.243 in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
10.244 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
10.245 pair (ITyVar (unprefix "'" v))
10.246 @@ -759,17 +760,18 @@
10.247 then translation_error thy permissive some_thm
10.248 "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
10.249 else ()
10.250 - val (annotate, ty') = dest_tagged_type ty
10.251 - val arg_typs = Sign.const_typargs thy (c, ty');
10.252 + val (annotate, ty') = dest_tagged_type ty;
10.253 + val typargs = Sign.const_typargs thy (c, ty');
10.254 val sorts = Code_Preproc.sortargs eqngr c;
10.255 - val (function_typs, body_typ) = Term.strip_type ty';
10.256 + val (dom, range) = Term.strip_type ty';
10.257 in
10.258 ensure_const thy algbr eqngr permissive c
10.259 - ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
10.260 - ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
10.261 - ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
10.262 - #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
10.263 - IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
10.264 + ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
10.265 + ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
10.266 + ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
10.267 + #>> (fn (((c, typargs), dss), range :: dom) =>
10.268 + IConst { name = c, typargs = typargs, dicts = dss,
10.269 + dom = dom, range = range, annotate = annotate })
10.270 end
10.271 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
10.272 translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
10.273 @@ -788,22 +790,22 @@
10.274 val constrs =
10.275 if null case_pats then []
10.276 else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
10.277 - fun casify naming constrs ty ts =
10.278 + fun casify naming constrs ty t_app ts =
10.279 let
10.280 val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
10.281 fun collapse_clause vs_map ts body =
10.282 let
10.283 in case body
10.284 - of IConst (c, _) => if member (op =) undefineds c
10.285 + of IConst { name = c, ... } => if member (op =) undefineds c
10.286 then []
10.287 else [(ts, body)]
10.288 - | ICase (((IVar (SOME v), _), subclauses), _) =>
10.289 + | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
10.290 if forall (fn (pat', body') => exists_var pat' v
10.291 - orelse not (exists_var body' v)) subclauses
10.292 + orelse not (exists_var body' v)) clauses
10.293 then case AList.lookup (op =) vs_map v
10.294 of SOME i => maps (fn (pat', body') =>
10.295 collapse_clause (AList.delete (op =) v vs_map)
10.296 - (nth_map i (K pat') ts) body') subclauses
10.297 + (nth_map i (K pat') ts) body') clauses
10.298 | NONE => [(ts, body)]
10.299 else [(ts, body)]
10.300 | _ => [(ts, body)]
10.301 @@ -818,11 +820,11 @@
10.302 val ts_clause = nth_drop t_pos ts;
10.303 val clauses = if null case_pats
10.304 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
10.305 - else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
10.306 + else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
10.307 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
10.308 (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
10.309 (case_pats ~~ ts_clause)));
10.310 - in ((t, ty), clauses) end;
10.311 + in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
10.312 in
10.313 translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
10.314 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
10.315 @@ -830,7 +832,7 @@
10.316 ##>> translate_typ thy algbr eqngr permissive ty
10.317 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
10.318 #-> (fn (((t, constrs), ty), ts) =>
10.319 - `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
10.320 + `(fn (_, (naming, _)) => casify naming constrs ty t ts))
10.321 end
10.322 and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
10.323 if length ts < num_args then
11.1 --- a/src/Tools/nbe.ML Mon Jun 04 12:55:54 2012 +0200
11.2 +++ b/src/Tools/nbe.ML Tue Jun 05 07:05:56 2012 +0200
11.3 @@ -314,13 +314,13 @@
11.4 let
11.5 val (t', ts) = Code_Thingol.unfold_app t
11.6 in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
11.7 - and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
11.8 + and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
11.9 | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
11.10 | of_iapp match_cont ((v, _) `|=> t) ts =
11.11 nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
11.12 - | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
11.13 + | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
11.14 nbe_apps (ml_cases (of_iterm NONE t)
11.15 - (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
11.16 + (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
11.17 @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
11.18 in of_iterm end;
11.19
11.20 @@ -345,7 +345,7 @@
11.21 |> subst_vars t1
11.22 ||>> subst_vars t2
11.23 |>> (op `$)
11.24 - | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
11.25 + | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
11.26 val (args', _) = fold_map subst_vars args samepairs;
11.27 in (samepairs, args') end;
11.28
11.29 @@ -410,6 +410,10 @@
11.30
11.31 (* extract equations from statements *)
11.32
11.33 +fun dummy_const c dss =
11.34 + IConst { name = c, typargs = [], dicts = dss,
11.35 + dom = [], range = ITyVar "", annotate = false };
11.36 +
11.37 fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
11.38 []
11.39 | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
11.40 @@ -424,17 +428,17 @@
11.41 val params = Name.invent Name.context "d" (length names);
11.42 fun mk (k, name) =
11.43 (name, ([(v, [])],
11.44 - [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
11.45 + [([dummy_const class [] `$$ map (IVar o SOME) params],
11.46 IVar (SOME (nth params k)))]));
11.47 in map_index mk names end
11.48 | eqns_of_stmt (_, Code_Thingol.Classrel _) =
11.49 []
11.50 | eqns_of_stmt (_, Code_Thingol.Classparam _) =
11.51 []
11.52 - | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
11.53 - [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
11.54 - map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
11.55 - @ map (IConst o snd o fst) classparam_instances)]))];
11.56 + | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
11.57 + [(inst, (vs, [([], dummy_const class [] `$$
11.58 + map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
11.59 + @ map (IConst o snd o fst) inst_params)]))];
11.60
11.61
11.62 (* compile whole programs *)