src/HOLCF/Tools/domain/domain_syntax.ML
changeset 30364 577edc39b501
parent 30341 78d08e2d01b9
child 30912 4022298c1a86
equal deleted inserted replaced
30363:9b8d9b6ef803 30364:577edc39b501
    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;