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});