src/HOLCF/Tools/domain/domain_library.ML
changeset 31006 644d18da3c77
parent 30910 a7cc0ef93269
child 31023 d027411c9a38
     1.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 22 07:20:13 2009 -0700
     1.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 22 11:00:25 2009 -0700
     1.3 @@ -30,9 +30,129 @@
     1.4      | _				    => [thm];
     1.5  in map zero_var_indexes (at thm) end;
     1.6  
     1.7 +(* infix syntax *)
     1.8 +
     1.9 +infixr 5 -->;
    1.10 +infixr 6 ->>;
    1.11 +infixr 0 ===>;
    1.12 +infixr 0 ==>;
    1.13 +infix 0 ==;
    1.14 +infix 1 ===;
    1.15 +infix 1 ~=;
    1.16 +infix 1 <<;
    1.17 +infix 1 ~<<;
    1.18 +
    1.19 +infix 9 `  ;
    1.20 +infix 9 `% ;
    1.21 +infix 9 `%%;
    1.22 +
    1.23 +
    1.24  (* ----- specific support for domain ---------------------------------------- *)
    1.25  
    1.26 -structure Domain_Library = struct
    1.27 +signature DOMAIN_LIBRARY =
    1.28 +sig
    1.29 +  val Imposs : string -> 'a;
    1.30 +  val pcpo_type : theory -> typ -> bool;
    1.31 +  val string_of_typ : theory -> typ -> string;
    1.32 +
    1.33 +  (* Creating HOLCF types *)
    1.34 +  val mk_cfunT : typ * typ -> typ;
    1.35 +  val ->> : typ * typ -> typ;
    1.36 +  val mk_ssumT : typ * typ -> typ;
    1.37 +  val mk_sprodT : typ * typ -> typ;
    1.38 +  val mk_uT : typ -> typ;
    1.39 +  val oneT : typ;
    1.40 +  val trT : typ;
    1.41 +  val mk_maybeT : typ -> typ;
    1.42 +  val mk_ctupleT : typ list -> typ;
    1.43 +  val mk_TFree : string -> typ;
    1.44 +  val pcpoS : sort;
    1.45 +
    1.46 +  (* Creating HOLCF terms *)
    1.47 +  val %: : string -> term;
    1.48 +  val %%: : string -> term;
    1.49 +  val ` : term * term -> term;
    1.50 +  val `% : term * string -> term;
    1.51 +  val /\ : string -> term -> term;
    1.52 +  val UU : term;
    1.53 +  val TT : term;
    1.54 +  val FF : term;
    1.55 +  val mk_up : term -> term;
    1.56 +  val mk_sinl : term -> term;
    1.57 +  val mk_sinr : term -> term;
    1.58 +  val mk_stuple : term list -> term;
    1.59 +  val mk_ctuple : term list -> term;
    1.60 +  val mk_fix : term -> term;
    1.61 +  val mk_iterate : term * term * term -> term;
    1.62 +  val mk_fail : term;
    1.63 +  val mk_return : term -> term;
    1.64 +  val cproj : term -> 'a list -> int -> term;
    1.65 +  val list_ccomb : term * term list -> term;
    1.66 +  val con_app : string -> ('a * 'b * string) list -> term;
    1.67 +  val con_app2 : string -> ('a -> term) -> 'a list -> term;
    1.68 +  val proj : term -> 'a list -> int -> term;
    1.69 +  val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
    1.70 +  val mk_ctuple_pat : term list -> term;
    1.71 +  val mk_branch : term -> term;
    1.72 +
    1.73 +  (* Creating propositions *)
    1.74 +  val mk_conj : term * term -> term;
    1.75 +  val mk_disj : term * term -> term;
    1.76 +  val mk_imp : term * term -> term;
    1.77 +  val mk_lam : string * term -> term;
    1.78 +  val mk_all : string * term -> term;
    1.79 +  val mk_ex : string * term -> term;
    1.80 +  val mk_constrain : typ * term -> term;
    1.81 +  val mk_constrainall : string * typ * term -> term;
    1.82 +  val === : term * term -> term;
    1.83 +  val << : term * term -> term;
    1.84 +  val ~<< : term * term -> term;
    1.85 +  val strict : term -> term;
    1.86 +  val defined : term -> term;
    1.87 +  val mk_adm : term -> term;
    1.88 +  val mk_compact : term -> term;
    1.89 +  val lift : ('a -> term) -> 'a list * term -> term;
    1.90 +  val lift_defined : ('a -> term) -> 'a list * term -> term;
    1.91 +
    1.92 +  (* Creating meta-propositions *)
    1.93 +  val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
    1.94 +  val == : term * term -> term;
    1.95 +  val ===> : term * term -> term;
    1.96 +  val ==> : term * term -> term;
    1.97 +  val mk_All : string * term -> term;
    1.98 +
    1.99 +  (* Domain specifications *)
   1.100 +  type arg = (bool * int * DatatypeAux.dtyp) * string option * string;
   1.101 +  type cons = string * arg list;
   1.102 +  type eq = (string * typ list) * cons list;
   1.103 +  val is_lazy : arg -> bool;
   1.104 +  val rec_of : arg -> int;
   1.105 +  val sel_of : arg -> string option;
   1.106 +  val vname : arg -> string;
   1.107 +  val upd_vname : (string -> string) -> arg -> arg;
   1.108 +  val is_rec : arg -> bool;
   1.109 +  val is_nonlazy_rec : arg -> bool;
   1.110 +  val nonlazy : arg list -> string list;
   1.111 +  val nonlazy_rec : arg list -> string list;
   1.112 +  val %# : arg -> term;
   1.113 +  val /\# : arg * term -> term;
   1.114 +  val when_body : cons list -> (int * int -> term) -> term;
   1.115 +  val when_funs : 'a list -> string list;
   1.116 +  val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
   1.117 +  val idx_name : 'a list -> string -> int -> string;
   1.118 +  val app_rec_arg : (int -> term) -> arg -> term;
   1.119 +
   1.120 +  (* Name mangling *)
   1.121 +  val strip_esc : string -> string;
   1.122 +  val extern_name : string -> string;
   1.123 +  val dis_name : string -> string;
   1.124 +  val mat_name : string -> string;
   1.125 +  val pat_name : string -> string;
   1.126 +  val mk_var_names : string list -> string list;
   1.127 +end;
   1.128 +
   1.129 +structure Domain_Library : DOMAIN_LIBRARY =
   1.130 +struct
   1.131  
   1.132  exception Impossible of string;
   1.133  fun Imposs msg = raise Impossible ("Domain:"^msg);
   1.134 @@ -75,14 +195,19 @@
   1.135  
   1.136  (* ----- constructor list handling ----- *)
   1.137  
   1.138 -type cons = (string *				(* operator name of constr *)
   1.139 -	    ((bool*int*DatatypeAux.dtyp)*	(*  (lazy,recursive element or ~1) *)
   1.140 -	      string option*			(*   selector name    *)
   1.141 -	      string)				(*   argument name    *)
   1.142 -	    list);				(* argument list      *)
   1.143 -type eq = (string *		(* name      of abstracted type *)
   1.144 -	   typ list) *		(* arguments of abstracted type *)
   1.145 -	  cons list;		(* represented type, as a constructor list *)
   1.146 +type arg =
   1.147 +  (bool * int * DatatypeAux.dtyp) *	(*  (lazy,recursive element or ~1) *)
   1.148 +  string option *			(*   selector name    *)
   1.149 +  string;				(*   argument name    *)
   1.150 +
   1.151 +type cons =
   1.152 +  string *				(* operator name of constr *)
   1.153 +  arg list;				(* argument list      *)
   1.154 +
   1.155 +type eq =
   1.156 +  (string *		(* name      of abstracted type *)
   1.157 +   typ list) *		(* arguments of abstracted type *)
   1.158 +  cons list;		(* represented type, as a constructor list *)
   1.159  
   1.160  fun rec_of arg  = second (first arg);
   1.161  fun is_lazy arg = first (first arg);
   1.162 @@ -96,7 +221,6 @@
   1.163  
   1.164  (* ----- support for type and mixfix expressions ----- *)
   1.165  
   1.166 -infixr 5 -->;
   1.167  fun mk_uT T = Type(@{type_name "u"}, [T]);
   1.168  fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
   1.169  fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
   1.170 @@ -104,7 +228,6 @@
   1.171  val oneT = @{typ one};
   1.172  val trT = @{typ tr};
   1.173  
   1.174 -infixr 6 ->>;
   1.175  val op ->> = mk_cfunT;
   1.176  
   1.177  fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});