equal
deleted
inserted
replaced
26 datatype iterm = |
26 datatype iterm = |
27 IConst of string * (inst list list * itype) |
27 IConst of string * (inst list list * itype) |
28 | IVar of vname |
28 | IVar of vname |
29 | `$ of iterm * iterm |
29 | `$ of iterm * iterm |
30 | `|-> of (vname * itype) * iterm |
30 | `|-> of (vname * itype) * iterm |
31 | INum of IntInf.int (*non-negative!*) * iterm |
31 | INum of IntInf.int * iterm |
32 | IChar of string (*length one!*) * iterm |
32 | IChar of string (*length one!*) * iterm |
33 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
33 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
34 (*((discriminendum term (td), discriminendum type (ty)), |
34 (*((discriminendum term (td), discriminendum type (ty)), |
35 [(selector pattern (p), body term (t))] (bs)), |
35 [(selector pattern (p), body term (t))] (bs)), |
36 pure term (t0))*) |
36 pure term (t0))*) |
819 *) |
819 *) |
820 |
820 |
821 val add_deps_of_typparms = |
821 val add_deps_of_typparms = |
822 fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort); |
822 fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort); |
823 |
823 |
824 fun add_deps_of_classlookup (Instance (tyco, lss)) = |
824 fun add_deps_of_classlookup (Instance (inst, lss)) = |
825 insert (op =) tyco |
825 insert (op =) inst |
826 #> (fold o fold) add_deps_of_classlookup lss |
826 #> (fold o fold) add_deps_of_classlookup lss |
827 | add_deps_of_classlookup (Context (clss, _)) = |
827 | add_deps_of_classlookup (Context (clss, _)) = |
828 fold (insert (op =)) clss; |
828 fold (insert (op =)) clss; |
829 |
829 |
830 fun add_deps_of_type (tyco `%% tys) = |
830 fun add_deps_of_type (tyco `%% tys) = |