# HG changeset patch
# User huffman
# Date 1240423225 25200
# Node ID 644d18da3c7785a66eb74cce7b78743d632d4256
# Parent  e55eed7d9b5547189c205c7a6112ced1d138d18a
add module signature to domain_library.ML

diff -r e55eed7d9b55 -r 644d18da3c77 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 22 07:20:13 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 22 11:00:25 2009 -0700
@@ -30,9 +30,129 @@
     | _				    => [thm];
 in map zero_var_indexes (at thm) end;
 
+(* infix syntax *)
+
+infixr 5 -->;
+infixr 6 ->>;
+infixr 0 ===>;
+infixr 0 ==>;
+infix 0 ==;
+infix 1 ===;
+infix 1 ~=;
+infix 1 <<;
+infix 1 ~<<;
+
+infix 9 `  ;
+infix 9 `% ;
+infix 9 `%%;
+
+
 (* ----- specific support for domain ---------------------------------------- *)
 
-structure Domain_Library = struct
+signature DOMAIN_LIBRARY =
+sig
+  val Imposs : string -> 'a;
+  val pcpo_type : theory -> typ -> bool;
+  val string_of_typ : theory -> typ -> string;
+
+  (* Creating HOLCF types *)
+  val mk_cfunT : typ * typ -> typ;
+  val ->> : typ * typ -> typ;
+  val mk_ssumT : typ * typ -> typ;
+  val mk_sprodT : typ * typ -> typ;
+  val mk_uT : typ -> typ;
+  val oneT : typ;
+  val trT : typ;
+  val mk_maybeT : typ -> typ;
+  val mk_ctupleT : typ list -> typ;
+  val mk_TFree : string -> typ;
+  val pcpoS : sort;
+
+  (* Creating HOLCF terms *)
+  val %: : string -> term;
+  val %%: : string -> term;
+  val ` : term * term -> term;
+  val `% : term * string -> term;
+  val /\ : string -> term -> term;
+  val UU : term;
+  val TT : term;
+  val FF : term;
+  val mk_up : term -> term;
+  val mk_sinl : term -> term;
+  val mk_sinr : term -> term;
+  val mk_stuple : term list -> term;
+  val mk_ctuple : term list -> term;
+  val mk_fix : term -> term;
+  val mk_iterate : term * term * term -> term;
+  val mk_fail : term;
+  val mk_return : term -> term;
+  val cproj : term -> 'a list -> int -> term;
+  val list_ccomb : term * term list -> term;
+  val con_app : string -> ('a * 'b * string) list -> term;
+  val con_app2 : string -> ('a -> term) -> 'a list -> term;
+  val proj : term -> 'a list -> int -> term;
+  val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
+  val mk_ctuple_pat : term list -> term;
+  val mk_branch : term -> term;
+
+  (* Creating propositions *)
+  val mk_conj : term * term -> term;
+  val mk_disj : term * term -> term;
+  val mk_imp : term * term -> term;
+  val mk_lam : string * term -> term;
+  val mk_all : string * term -> term;
+  val mk_ex : string * term -> term;
+  val mk_constrain : typ * term -> term;
+  val mk_constrainall : string * typ * term -> term;
+  val === : term * term -> term;
+  val << : term * term -> term;
+  val ~<< : term * term -> term;
+  val strict : term -> term;
+  val defined : term -> term;
+  val mk_adm : term -> term;
+  val mk_compact : term -> term;
+  val lift : ('a -> term) -> 'a list * term -> term;
+  val lift_defined : ('a -> term) -> 'a list * term -> term;
+
+  (* Creating meta-propositions *)
+  val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
+  val == : term * term -> term;
+  val ===> : term * term -> term;
+  val ==> : term * term -> term;
+  val mk_All : string * term -> term;
+
+  (* Domain specifications *)
+  type arg = (bool * int * DatatypeAux.dtyp) * string option * string;
+  type cons = string * arg list;
+  type eq = (string * typ list) * cons list;
+  val is_lazy : arg -> bool;
+  val rec_of : arg -> int;
+  val sel_of : arg -> string option;
+  val vname : arg -> string;
+  val upd_vname : (string -> string) -> arg -> arg;
+  val is_rec : arg -> bool;
+  val is_nonlazy_rec : arg -> bool;
+  val nonlazy : arg list -> string list;
+  val nonlazy_rec : arg list -> string list;
+  val %# : arg -> term;
+  val /\# : arg * term -> term;
+  val when_body : cons list -> (int * int -> term) -> term;
+  val when_funs : 'a list -> string list;
+  val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
+  val idx_name : 'a list -> string -> int -> string;
+  val app_rec_arg : (int -> term) -> arg -> term;
+
+  (* Name mangling *)
+  val strip_esc : string -> string;
+  val extern_name : string -> string;
+  val dis_name : string -> string;
+  val mat_name : string -> string;
+  val pat_name : string -> string;
+  val mk_var_names : string list -> string list;
+end;
+
+structure Domain_Library : DOMAIN_LIBRARY =
+struct
 
 exception Impossible of string;
 fun Imposs msg = raise Impossible ("Domain:"^msg);
@@ -75,14 +195,19 @@
 
 (* ----- constructor list handling ----- *)
 
-type cons = (string *				(* operator name of constr *)
-	    ((bool*int*DatatypeAux.dtyp)*	(*  (lazy,recursive element or ~1) *)
-	      string option*			(*   selector name    *)
-	      string)				(*   argument name    *)
-	    list);				(* argument list      *)
-type eq = (string *		(* name      of abstracted type *)
-	   typ list) *		(* arguments of abstracted type *)
-	  cons list;		(* represented type, as a constructor list *)
+type arg =
+  (bool * int * DatatypeAux.dtyp) *	(*  (lazy,recursive element or ~1) *)
+  string option *			(*   selector name    *)
+  string;				(*   argument name    *)
+
+type cons =
+  string *				(* operator name of constr *)
+  arg list;				(* argument list      *)
+
+type eq =
+  (string *		(* name      of abstracted type *)
+   typ list) *		(* arguments of abstracted type *)
+  cons list;		(* represented type, as a constructor list *)
 
 fun rec_of arg  = second (first arg);
 fun is_lazy arg = first (first arg);
@@ -96,7 +221,6 @@
 
 (* ----- support for type and mixfix expressions ----- *)
 
-infixr 5 -->;
 fun mk_uT T = Type(@{type_name "u"}, [T]);
 fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
 fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
@@ -104,7 +228,6 @@
 val oneT = @{typ one};
 val trT = @{typ tr};
 
-infixr 6 ->>;
 val op ->> = mk_cfunT;
 
 fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});