23 if tvar mem typevars then freetvar ("t"^s) else tvar end; |
23 if tvar mem typevars then freetvar ("t"^s) else tvar end; |
24 fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args); |
24 fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args); |
25 in |
25 in |
26 val dtype = Type(dname,typevars); |
26 val dtype = Type(dname,typevars); |
27 val dtype2 = foldr1 mk_ssumT (map prod cons'); |
27 val dtype2 = foldr1 mk_ssumT (map prod cons'); |
28 val dnam = NameSpace.base_name dname; |
28 val dnam = Long_Name.base_name dname; |
29 val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); |
29 val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); |
30 val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); |
30 val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); |
31 val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
31 val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
32 val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
32 val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
33 end; |
33 end; |