--- a/src/Tools/Code/code_ml.ML Mon Dec 13 10:15:27 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Dec 13 22:54:47 2010 +0100
@@ -80,16 +80,18 @@
| print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
| print_classrels fxy classrels ps =
brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
- fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
- print_classrels fxy classrels ((str o deresolve) inst ::
+ fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
+ print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
+ and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
+ ((str o deresolve) inst ::
(if is_pseudo_fun inst then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
- | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
- print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
+ | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
+ [str (if k = 1 then first_upper v ^ "_"
else first_upper v ^ string_of_int (i+1) ^ "_")]
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_Var ([], (v, (i, length sort)))) sort));
+ (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, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -219,7 +221,7 @@
concat [
(str o Long_Name.base_name o deresolve) classrel,
str "=",
- print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
];
fun print_classparam_instance ((classparam, const), (thm, _)) =
concat [
@@ -380,18 +382,19 @@
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
val print_classrels =
fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
- fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
+ fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
+ print_plain_dict is_pseudo_fun fxy x
+ |> print_classrels classrels
+ and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
brackify BR ((str o deresolve) inst ::
(if is_pseudo_fun inst then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
- |> print_classrels classrels
- | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
+ | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
str (if k = 1 then "_" ^ first_upper v
else "_" ^ first_upper v ^ string_of_int (i+1))
- |> print_classrels classrels
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_Var ([], (v, (i, length sort)))) sort));
+ (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, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -556,7 +559,7 @@
concat [
(str o deresolve) classrel,
str "=",
- print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
];
fun print_classparam_instance ((classparam, const), (thm, _)) =
concat [
--- a/src/Tools/Code/code_thingol.ML Mon Dec 13 10:15:27 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Dec 13 22:54:47 2010 +0100
@@ -15,8 +15,10 @@
sig
type vname = string;
datatype dict =
- Dict_Const of string list * (string * dict list list)
- | Dict_Var of string list * (vname * (int * int));
+ Dict of (string list * plain_dict)
+ and plain_dict =
+ Dict_Const of string * dict list list
+ | Dict_Var of vname * (int * int)
datatype itype =
`%% of string * itype list
| ITyVar of vname;
@@ -132,8 +134,10 @@
type vname = string;
datatype dict =
- Dict_Const of string list * (string * dict list list)
- | Dict_Var of string list * (vname * (int * int));
+ Dict of (string list * plain_dict)
+and plain_dict =
+ Dict_Const of string * dict list list
+ | Dict_Var of vname * (int * int)
datatype itype =
`%% of string * itype list
@@ -244,8 +248,9 @@
fun contains_dict_var t =
let
- fun cont_dict (Dict_Const (_, (_, dss))) = (exists o exists) cont_dict dss
- | cont_dict (Dict_Var _) = true;
+ 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
| cont_term (IVar _) = false
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
@@ -641,7 +646,7 @@
ensure_class thy algbr eqngr permissive super_class
##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
- #>> (fn ((super_class, classrel), [Dict_Const ([], (inst, dss))]) =>
+ #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
(super_class, (classrel, (inst, dss))));
fun translate_classparam_instance (c, ty) =
let
@@ -802,33 +807,33 @@
and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
let
datatype typarg_witness =
- Global of (class * class) list * ((class * string) * typarg_witness list list)
- | Local of (class * class) list * (string * (int * sort));
- fun add_classrel classrel (Global (classrels, x)) =
- Global (classrel :: classrels, x)
- | add_classrel classrel (Local (classrels, x)) =
- Local (classrel :: classrels, x)
- fun class_relation (d, sub_class) super_class =
- add_classrel (sub_class, super_class) d;
+ Weakening of (class * class) list * plain_typarg_witness
+ and plain_typarg_witness =
+ Global of (class * string) * typarg_witness list list
+ | Local of string * (int * sort);
+ fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
+ Weakening ((sub_class, super_class) :: classrels, x);
fun type_constructor (tyco, _) dss class =
- Global ([], ((class, tyco), (map o map) fst dss));
+ Weakening ([], Global ((class, tyco), (map o map) fst dss));
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
- in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+ in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
val typarg_witnesses = Sorts.of_sort_derivation algebra
{class_relation = K (Sorts.classrel_derivation algebra class_relation),
type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
- fun mk_dict (Global (classrels, (inst, dss))) =
+ fun mk_dict (Weakening (classrels, x)) =
fold_map (ensure_classrel thy algbr eqngr permissive) classrels
- ##>> ensure_inst thy algbr eqngr permissive inst
+ ##>> mk_plain_dict x
+ #>> Dict
+ and mk_plain_dict (Global (inst, dss)) =
+ ensure_inst thy algbr eqngr permissive inst
##>> (fold_map o fold_map) mk_dict dss
- #>> (fn ((classrels, inst), dss) => Dict_Const (classrels, (inst, dss)))
- | mk_dict (Local (classrels, (v, (n, sort)))) =
- fold_map (ensure_classrel thy algbr eqngr permissive) classrels
- #>> (fn classrels => Dict_Var (classrels, (unprefix "'" v, (n, length sort))))
+ #>> (fn (inst, dss) => Dict_Const (inst, dss))
+ | mk_plain_dict (Local (v, (n, sort))) =
+ pair (Dict_Var (unprefix "'" v, (n, length sort)))
in fold_map mk_dict typarg_witnesses end;
--- a/src/Tools/nbe.ML Mon Dec 13 10:15:27 2010 +0100
+++ b/src/Tools/nbe.ML Mon Dec 13 22:54:47 2010 +0100
@@ -287,7 +287,7 @@
fun assemble_constapp c dss ts =
let
- val ts' = (maps o map) assemble_idict dss @ ts;
+ val ts' = (maps o map) assemble_dict dss @ ts;
in case AList.lookup (op =) eqnss' c
of SOME (num_args, _) => if num_args <= length ts'
then let val (ts1, ts2) = chop num_args ts'
@@ -299,10 +299,12 @@
end
and assemble_classrels classrels =
fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
- and assemble_idict (Dict_Const (classrels, (inst, dss))) =
- assemble_classrels classrels (assemble_constapp inst dss [])
- | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
- assemble_classrels classrels (nbe_dict v n);
+ and assemble_dict (Dict (classrels, x)) =
+ assemble_classrels classrels (assemble_plain_dict x)
+ and assemble_plain_dict (Dict_Const (inst, dss)) =
+ assemble_constapp inst dss []
+ | assemble_plain_dict (Dict_Var (v, (n, _))) =
+ nbe_dict v n
fun assemble_iterm constapp =
let