src/HOLCF/Tools/domain/domain_library.ML
changeset 31162 6dc708ca4a8f
parent 31076 99fe356cbbc2
child 31228 bcacfd816d28
equal deleted inserted replaced
31161:a27d4254ff4c 31162:6dc708ca4a8f
    50 (* ----- specific support for domain ---------------------------------------- *)
    50 (* ----- specific support for domain ---------------------------------------- *)
    51 
    51 
    52 signature DOMAIN_LIBRARY =
    52 signature DOMAIN_LIBRARY =
    53 sig
    53 sig
    54   val Imposs : string -> 'a;
    54   val Imposs : string -> 'a;
       
    55   val cpo_type : theory -> typ -> bool;
    55   val pcpo_type : theory -> typ -> bool;
    56   val pcpo_type : theory -> typ -> bool;
    56   val string_of_typ : theory -> typ -> string;
    57   val string_of_typ : theory -> typ -> string;
    57 
    58 
    58   (* Creating HOLCF types *)
    59   (* Creating HOLCF types *)
    59   val mk_cfunT : typ * typ -> typ;
    60   val mk_cfunT : typ * typ -> typ;
   188            | SOME(i) => (vn^(string_of_int (i+1)))
   189            | SOME(i) => (vn^(string_of_int (i+1)))
   189 				   :: index_vnames(vns,(vn,i+1)::occupied))
   190 				   :: index_vnames(vns,(vn,i+1)::occupied))
   190       | index_vnames([],occupied) = [];
   191       | index_vnames([],occupied) = [];
   191 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
   192 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
   192 
   193 
       
   194 fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
   193 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
   195 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
   194 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   196 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   195 
   197 
   196 (* ----- constructor list handling ----- *)
   198 (* ----- constructor list handling ----- *)
   197 
   199