src/HOLCF/Tools/domain/domain_library.ML
changeset 31229 8a890890d143
parent 31228 bcacfd816d28
child 31231 9434cd5ef24a
equal deleted inserted replaced
31228:bcacfd816d28 31229:8a890890d143
   126 
   126 
   127   (* Domain specifications *)
   127   (* Domain specifications *)
   128   eqtype arg;
   128   eqtype arg;
   129   type cons = string * arg list;
   129   type cons = string * arg list;
   130   type eq = (string * typ list) * cons list;
   130   type eq = (string * typ list) * cons list;
   131   val mk_arg : (bool * int * DatatypeAux.dtyp) * string option * string -> arg;
   131   val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
   132   val is_lazy : arg -> bool;
   132   val is_lazy : arg -> bool;
   133   val rec_of : arg -> int;
   133   val rec_of : arg -> int;
   134   val sel_of : arg -> string option;
   134   val sel_of : arg -> string option;
   135   val vname : arg -> string;
   135   val vname : arg -> string;
   136   val upd_vname : (string -> string) -> arg -> arg;
   136   val upd_vname : (string -> string) -> arg -> arg;
   201 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   201 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   202 
   202 
   203 (* ----- constructor list handling ----- *)
   203 (* ----- constructor list handling ----- *)
   204 
   204 
   205 type arg =
   205 type arg =
   206   (bool * int * DatatypeAux.dtyp) *	(*  (lazy,recursive element or ~1) *)
   206   (bool * DatatypeAux.dtyp) *           (*  (lazy, recursive element) *)
   207   string option *			(*   selector name    *)
   207   string option *			(*   selector name    *)
   208   string;				(*   argument name    *)
   208   string;				(*   argument name    *)
   209 
   209 
   210 type cons =
   210 type cons =
   211   string *				(* operator name of constr *)
   211   string *				(* operator name of constr *)
   215   (string *		(* name      of abstracted type *)
   215   (string *		(* name      of abstracted type *)
   216    typ list) *		(* arguments of abstracted type *)
   216    typ list) *		(* arguments of abstracted type *)
   217   cons list;		(* represented type, as a constructor list *)
   217   cons list;		(* represented type, as a constructor list *)
   218 
   218 
   219 val mk_arg = I;
   219 val mk_arg = I;
   220 fun rec_of arg  = second (first arg);
   220 
   221 fun is_lazy arg = first (first arg);
   221 fun rec_of ((_,dtyp),_,_) =
       
   222   case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
       
   223 (* FIXME: what about indirect recursion? *)
       
   224 
       
   225 fun is_lazy arg = fst (first arg);
   222 val sel_of    =       second;
   226 val sel_of    =       second;
   223 val     vname =       third;
   227 val     vname =       third;
   224 val upd_vname =   upd_third;
   228 val upd_vname =   upd_third;
   225 fun is_rec         arg = rec_of arg >=0;
   229 fun is_rec         arg = rec_of arg >=0;
   226 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
   230 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);