author | paulson |
Tue, 04 Mar 1997 10:58:29 +0100 | |
changeset 2719 | 27167b432e7a |
parent 2446 | c2a9bf6c0948 |
child 3176 | a3db6c177885 |
permissions | -rw-r--r-- |
2276 | 1 |
(* Title: HOLCF/domain/library.ML |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
2 |
ID: $Id$ |
2276 | 3 |
Author : David von Oheimb |
4 |
Copyright 1995, 1996 TU Muenchen |
|
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
5 |
|
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
6 |
library for domain section |
1274 | 7 |
*) |
8 |
||
2446
c2a9bf6c0948
The previous log message was wrong. The correct one is:
oheimb
parents:
2445
diff
changeset
|
9 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
10 |
(* ----- general support ---------------------------------------------------- *) |
1274 | 11 |
|
12 |
fun Id x = x; |
|
13 |
||
14 |
fun mapn f n [] = [] |
|
15 |
| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; |
|
16 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
17 |
fun foldr'' f (l,f2) = let fun itr [] = raise LIST "foldr''" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
18 |
| itr [a] = f2 a |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
19 |
| itr (a::l) = f(a, itr l) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
20 |
in itr l end; |
1274 | 21 |
fun foldr' f l = foldr'' f (l,Id); |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
22 |
fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
23 |
(y::ys,res2)) (xs,([],start)); |
1274 | 24 |
|
25 |
||
26 |
fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; |
|
27 |
fun upd_first f (x,y,z) = (f x, y, z); |
|
28 |
fun upd_second f (x,y,z) = ( x, f y, z); |
|
29 |
fun upd_third f (x,y,z) = ( x, y, f z); |
|
30 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
31 |
fun atomize thm = let val r_inst = read_instantiate; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
32 |
fun at thm = case concl_of thm of |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
33 |
_$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
34 |
| _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
35 |
| _ => [thm]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
36 |
in map zero_var_indexes (at thm) end; |
1274 | 37 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
38 |
(* ----- specific support for domain ---------------------------------------- *) |
1274 | 39 |
|
40 |
structure Domain_Library = struct |
|
41 |
||
42 |
exception Impossible of string; |
|
43 |
fun Imposs msg = raise Impossible ("Domain:"^msg); |
|
44 |
||
45 |
(* ----- name handling ----- *) |
|
46 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
47 |
val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
48 |
| strip ["'"] = [] |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
49 |
| strip (c :: cs) = c :: strip cs |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
50 |
| strip [] = []; |
1274 | 51 |
in implode o strip o explode end; |
52 |
||
53 |
fun extern_name con = case explode con of |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
54 |
("o"::"p"::" "::rest) => implode rest |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
55 |
| _ => con; |
1274 | 56 |
fun dis_name con = "is_"^ (extern_name con); |
57 |
fun dis_name_ con = "is_"^ (strip_esc con); |
|
58 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
59 |
(* make distinct names out of the type list, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
60 |
forbidding "o", "x..","f..","P.." as names *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
61 |
(* a number string is added if necessary *) |
1274 | 62 |
fun mk_var_names types : string list = let |
63 |
fun typid (Type (id,_) ) = hd (explode id) |
|
64 |
| typid (TFree (id,_) ) = hd (tl (explode id)) |
|
65 |
| typid (TVar ((id,_),_)) = hd (tl (explode id)); |
|
66 |
fun nonreserved id = let val cs = explode id in |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
67 |
if not(hd cs mem ["x","f","P"]) then id |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
68 |
else implode(chr(1+ord (hd cs))::tl cs) end; |
1819
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
69 |
fun index_vnames(vn::vns,occupied) = |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
70 |
(case assoc(occupied,vn) of |
1274 | 71 |
None => if vn mem vns |
1819
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
72 |
then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
73 |
else vn :: index_vnames(vns, occupied) |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
74 |
| Some(i) => (vn^(string_of_int (i+1))) |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
75 |
:: index_vnames(vns,(vn,i+1)::occupied)) |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
76 |
| index_vnames([],occupied) = []; |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
77 |
in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end; |
1274 | 78 |
|
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
79 |
fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type"; |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
80 |
fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree"; |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
81 |
val tsig_of = #tsig o Sign.rep_sg o sign_of; |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
82 |
fun pcpo_type thy t = Type.typ_instance(tsig_of thy,t,TVar(("'a",0),["pcpo"])); |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
83 |
fun string_of_typ thy = Sign.string_of_typ (sign_of thy); |
1274 | 84 |
|
85 |
(* ----- constructor list handling ----- *) |
|
86 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
87 |
type cons = (string * (* operator name of constr *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
88 |
((bool*int)* (* (lazy,recursive element or ~1) *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
89 |
string* (* selector name *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
90 |
string) (* argument name *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
91 |
list); (* argument list *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
92 |
type eq = (string * (* name of abstracted type *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
93 |
typ list) * (* arguments of abstracted type *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
94 |
cons list; (* represented type, as a constructor list *) |
1274 | 95 |
|
2238
c72a23bbe762
Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents:
1834
diff
changeset
|
96 |
fun rec_of arg = snd (first arg); |
c72a23bbe762
Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents:
1834
diff
changeset
|
97 |
fun is_lazy arg = fst (first arg); |
1274 | 98 |
val sel_of = second; |
99 |
val vname = third; |
|
100 |
val upd_vname = upd_third; |
|
101 |
fun is_rec arg = rec_of arg >=0; |
|
102 |
fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
103 |
fun nonlazy args = map vname (filter_out is_lazy args); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
104 |
fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
105 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
106 |
(* ----- support for type and mixfix expressions ----- *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
107 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
108 |
fun mk_tvar s = TFree("'"^s,["pcpo"]); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
109 |
fun mk_typ t (S,T) = Type(t,[S,T]); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
110 |
infixr 5 -->; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
111 |
infixr 6 ~>; val op ~> = mk_typ "->"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
112 |
val NoSyn' = ThyOps.Mixfix NoSyn; |
1274 | 113 |
|
114 |
(* ----- support for term expressions ----- *) |
|
115 |
||
116 |
fun % s = Free(s,dummyT); |
|
117 |
fun %# arg = %(vname arg); |
|
118 |
fun %% s = Const(s,dummyT); |
|
119 |
||
120 |
local open HOLogic in |
|
121 |
val mk_trp = mk_Trueprop; |
|
122 |
fun mk_conj (S,T) = conj $ S $ T; |
|
123 |
fun mk_disj (S,T) = disj $ S $ T; |
|
124 |
fun mk_imp (S,T) = imp $ S $ T; |
|
125 |
fun mk_lam (x,T) = Abs(x,dummyT,T); |
|
126 |
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); |
|
127 |
local |
|
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
128 |
fun sg [s] = %s |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
129 |
| sg (s::ss) = %%"_classes" $ %s $ sg ss |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
130 |
| sg _ = Imposs "library:sg"; |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
131 |
fun sf [] = %%"_emptysort" |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
132 |
| sf s = %%"_sort" $ sg s |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
133 |
fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
134 |
| tf (TFree(s,sort)) = %%"_ofsort" $ %s $ sf sort |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
2276
diff
changeset
|
135 |
| tf _ = Imposs "library:tf"; |
1274 | 136 |
in |
137 |
fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ; |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
138 |
fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ); |
1274 | 139 |
end; |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
140 |
|
1274 | 141 |
fun mk_ex (x,P) = mk_exists (x,dummyT,P); |
2719 | 142 |
fun mk_not P = Const("Not" ,boolT --> boolT) $ P; |
1274 | 143 |
end; |
144 |
||
145 |
fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *) |
|
146 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
147 |
infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T; |
1274 | 148 |
infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T; |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
149 |
infix 0 ==; fun S == T = %%"==" $ S $ T; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
150 |
infix 1 ===; fun S === T = %%"op =" $ S $ T; |
1274 | 151 |
infix 1 ~=; fun S ~= T = mk_not (S === T); |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
152 |
infix 1 <<; fun S << T = %%"op <<" $ S $ T; |
1274 | 153 |
infix 1 ~<<; fun S ~<< T = mk_not (S << T); |
154 |
||
155 |
infix 9 ` ; fun f` x = %%"fapp" $ f $ x; |
|
156 |
infix 9 `% ; fun f`% s = f` % s; |
|
157 |
infix 9 `%%; fun f`%%s = f` %%s; |
|
158 |
fun mk_cfapp (F,As) = foldl (op `) (F,As); |
|
159 |
fun con_app2 con f args = mk_cfapp(%%con,map f args); |
|
160 |
fun con_app con = con_app2 con %#; |
|
161 |
fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; |
|
162 |
fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg); |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
163 |
fun prj _ _ y 1 _ = y |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
164 |
| prj f1 _ y _ 0 = f1 y |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
165 |
| prj f1 f2 y i j = prj f1 f2 (f2 y) (i-1) (j-1); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
166 |
val cproj = prj (fn S => %%"cfst"`S) (fn S => %%"csnd"`S); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
167 |
val proj = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S); |
1274 | 168 |
fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); |
169 |
||
170 |
fun /\ v T = %%"fabs" $ mk_lam(v,T); |
|
171 |
fun /\# (arg,T) = /\ (vname arg) T; |
|
172 |
infixr 9 oo; fun S oo T = %%"cfcomp"`S`T; |
|
173 |
val UU = %%"UU"; |
|
174 |
fun strict f = f`UU === UU; |
|
175 |
fun defined t = t ~= UU; |
|
176 |
fun cpair (S,T) = %%"cpair"`S`T; |
|
177 |
fun lift_defined f = lift (fn x => defined (f x)); |
|
178 |
fun bound_arg vns v = Bound(length vns-find(v,vns)-1); |
|
179 |
||
180 |
fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = |
|
181 |
(case cont_eta_contract body of |
|
182 |
body' as (Const("fapp",Ta) $ f $ Bound 0) => |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
183 |
if not (0 mem loose_bnos f) then incr_boundvars ~1 f |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
184 |
else Const("fabs",TT) $ Abs(a,T,body') |
1274 | 185 |
| body' => Const("fabs",TT) $ Abs(a,T,body')) |
186 |
| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t |
|
187 |
| cont_eta_contract t = t; |
|
188 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
189 |
fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); |
1834 | 190 |
fun when_funs cons = if length cons = 1 then ["f"] |
191 |
else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
|
1274 | 192 |
fun when_body cons funarg = let |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
193 |
fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
194 |
| one_fun n (_,args) = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
195 |
val l2 = length args; |
2276 | 196 |
fun idxs m arg = (if is_lazy arg then fn x=> %%"fup"`%%"ID"`x |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
197 |
else Id) (Bound(l2-m)); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
198 |
in cont_eta_contract (foldr'' |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
199 |
(fn (a,t) => %%"ssplit"`(/\# (a,t))) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
200 |
(args, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
201 |
fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args)))) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
202 |
) end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
203 |
in (if length cons = 1 andalso length(snd(hd cons)) <= 1 |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
204 |
then fn t => %%"strictify"`t else Id) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
205 |
(foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons)) end; |
1274 | 206 |
end; (* struct *) |