equal
deleted
inserted
replaced
1 (* library.ML |
1 (* Title: HOLCF/domain/library.ML |
2 Author : David von Oheimb |
2 ID: $ $ |
3 Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML |
3 Author : David von Oheimb |
4 Updated: 30-Aug-95 |
4 Copyright 1995, 1996 TU Muenchen |
5 Updated: 20-Oct-95 small improvement for atomize |
|
6 Copyright 1995 TU Muenchen |
|
7 *) |
5 *) |
8 |
6 |
9 (* ----- general support ---------------------------------------------------- *) |
7 (* ----- general support ---------------------------------------------------- *) |
10 |
8 |
11 fun Id x = x; |
9 fun Id x = x; |
182 else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
180 else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
183 fun when_body cons funarg = let |
181 fun when_body cons funarg = let |
184 fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) |
182 fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) |
185 | one_fun n (_,args) = let |
183 | one_fun n (_,args) = let |
186 val l2 = length args; |
184 val l2 = length args; |
187 fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x |
185 fun idxs m arg = (if is_lazy arg then fn x=> %%"fup"`%%"ID"`x |
188 else Id) (Bound(l2-m)); |
186 else Id) (Bound(l2-m)); |
189 in cont_eta_contract (foldr'' |
187 in cont_eta_contract (foldr'' |
190 (fn (a,t) => %%"ssplit"`(/\# (a,t))) |
188 (fn (a,t) => %%"ssplit"`(/\# (a,t))) |
191 (args, |
189 (args, |
192 fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args)))) |
190 fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args)))) |