equal
deleted
inserted
replaced
17 type vname = string; |
17 type vname = string; |
18 datatype dict = |
18 datatype dict = |
19 Dict of (class * class) list * plain_dict |
19 Dict of (class * class) list * plain_dict |
20 and plain_dict = |
20 and plain_dict = |
21 Dict_Const of (string * class) * dict list list |
21 Dict_Const of (string * class) * dict list list |
22 | Dict_Var of vname * (int * int); |
22 | Dict_Var of { var: vname, index: int, length: int }; |
23 datatype itype = |
23 datatype itype = |
24 `%% of string * itype list |
24 `%% of string * itype list |
25 | ITyVar of vname; |
25 | ITyVar of vname; |
26 type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, |
26 type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, |
27 dom: itype list, annotation: itype option }; |
27 dom: itype list, annotation: itype option }; |
130 |
130 |
131 datatype dict = |
131 datatype dict = |
132 Dict of (class * class) list * plain_dict |
132 Dict of (class * class) list * plain_dict |
133 and plain_dict = |
133 and plain_dict = |
134 Dict_Const of (string * class) * dict list list |
134 Dict_Const of (string * class) * dict list list |
135 | Dict_Var of vname * (int * int); |
135 | Dict_Var of { var: vname, index: int, length: int }; |
136 |
136 |
137 datatype itype = |
137 datatype itype = |
138 `%% of string * itype list |
138 `%% of string * itype list |
139 | ITyVar of vname; |
139 | ITyVar of vname; |
140 |
140 |
758 #>> Dict |
758 #>> Dict |
759 and mk_plain_dict (Global (inst, dss)) = |
759 and mk_plain_dict (Global (inst, dss)) = |
760 ensure_inst ctxt algbr eqngr permissive inst |
760 ensure_inst ctxt algbr eqngr permissive inst |
761 ##>> (fold_map o fold_map) mk_dict dss |
761 ##>> (fold_map o fold_map) mk_dict dss |
762 #>> (fn (inst, dss) => Dict_Const (inst, dss)) |
762 #>> (fn (inst, dss) => Dict_Const (inst, dss)) |
763 | mk_plain_dict (Local (v, (n, sort))) = |
763 | mk_plain_dict (Local (v, (index, sort))) = |
764 pair (Dict_Var (unprefix "'" v, (n, length sort))) |
764 pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort }) |
765 in |
765 in |
766 construct_dictionaries ctxt algbr permissive some_thm (ty, sort) |
766 construct_dictionaries ctxt algbr permissive some_thm (ty, sort) |
767 #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) |
767 #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) |
768 end; |
768 end; |
769 |
769 |