author | oheimb |
Fri, 29 Nov 1996 12:16:57 +0100 | |
changeset 2276 | 3eb9a113029e |
parent 2238 | c72a23bbe762 |
child 2445 | 51993fea433f |
permissions | -rw-r--r-- |
2276 | 1 |
(* Title: HOLCF/domain/library.ML |
2 |
ID: $ $ |
|
3 |
Author : David von Oheimb |
|
4 |
Copyright 1995, 1996 TU Muenchen |
|
1274 | 5 |
*) |
6 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
7 |
(* ----- general support ---------------------------------------------------- *) |
1274 | 8 |
|
9 |
fun Id x = x; |
|
10 |
||
11 |
fun mapn f n [] = [] |
|
12 |
| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; |
|
13 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
14 |
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
|
15 |
| itr [a] = f2 a |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
16 |
| 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
|
17 |
in itr l end; |
1274 | 18 |
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
|
19 |
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
|
20 |
(y::ys,res2)) (xs,([],start)); |
1274 | 21 |
|
22 |
||
23 |
fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; |
|
24 |
fun upd_first f (x,y,z) = (f x, y, z); |
|
25 |
fun upd_second f (x,y,z) = ( x, f y, z); |
|
26 |
fun upd_third f (x,y,z) = ( x, y, f z); |
|
27 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
28 |
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
|
29 |
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
|
30 |
_$(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
|
31 |
| _$(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
|
32 |
| _ => [thm]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
33 |
in map zero_var_indexes (at thm) end; |
1274 | 34 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
35 |
(* ----- specific support for domain ---------------------------------------- *) |
1274 | 36 |
|
37 |
structure Domain_Library = struct |
|
38 |
||
39 |
exception Impossible of string; |
|
40 |
fun Imposs msg = raise Impossible ("Domain:"^msg); |
|
41 |
||
42 |
(* ----- name handling ----- *) |
|
43 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
44 |
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
|
45 |
| strip ["'"] = [] |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
46 |
| 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
|
47 |
| strip [] = []; |
1274 | 48 |
in implode o strip o explode end; |
49 |
||
50 |
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
|
51 |
("o"::"p"::" "::rest) => implode rest |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
52 |
| _ => con; |
1274 | 53 |
fun dis_name con = "is_"^ (extern_name con); |
54 |
fun dis_name_ con = "is_"^ (strip_esc con); |
|
55 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
56 |
(* 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
|
57 |
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
|
58 |
(* a number string is added if necessary *) |
1274 | 59 |
fun mk_var_names types : string list = let |
60 |
fun typid (Type (id,_) ) = hd (explode id) |
|
61 |
| typid (TFree (id,_) ) = hd (tl (explode id)) |
|
62 |
| typid (TVar ((id,_),_)) = hd (tl (explode id)); |
|
63 |
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
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
(case assoc(occupied,vn) of |
1274 | 68 |
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
|
69 |
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
|
70 |
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
|
71 |
| 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
|
72 |
:: 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
|
73 |
| index_vnames([],occupied) = []; |
245721624c8d
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
oheimb
parents:
1637
diff
changeset
|
74 |
in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end; |
1274 | 75 |
|
76 |
fun type_name_vars (Type(name,typevars)) = (name,typevars) |
|
77 |
| type_name_vars _ = Imposs "library:type_name_vars"; |
|
78 |
||
79 |
(* ----- constructor list handling ----- *) |
|
80 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
81 |
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
|
82 |
((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
|
83 |
string* (* selector name *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
84 |
string) (* argument name *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
85 |
list); (* argument list *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
cons list; (* represented type, as a constructor list *) |
1274 | 89 |
|
2238
c72a23bbe762
Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents:
1834
diff
changeset
|
90 |
fun rec_of arg = snd (first arg); |
c72a23bbe762
Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents:
1834
diff
changeset
|
91 |
fun is_lazy arg = fst (first arg); |
1274 | 92 |
val sel_of = second; |
93 |
val vname = third; |
|
94 |
val upd_vname = upd_third; |
|
95 |
fun is_rec arg = rec_of arg >=0; |
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
100 |
(* ----- 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
|
101 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
infixr 5 -->; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
105 |
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
|
106 |
val NoSyn' = ThyOps.Mixfix NoSyn; |
1274 | 107 |
|
108 |
(* ----- support for term expressions ----- *) |
|
109 |
||
110 |
fun % s = Free(s,dummyT); |
|
111 |
fun %# arg = %(vname arg); |
|
112 |
fun %% s = Const(s,dummyT); |
|
113 |
||
114 |
local open HOLogic in |
|
115 |
val mk_trp = mk_Trueprop; |
|
116 |
fun mk_conj (S,T) = conj $ S $ T; |
|
117 |
fun mk_disj (S,T) = disj $ S $ T; |
|
118 |
fun mk_imp (S,T) = imp $ S $ T; |
|
119 |
fun mk_lam (x,T) = Abs(x,dummyT,T); |
|
120 |
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); |
|
121 |
local |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
122 |
fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
123 |
| tf (TFree(s,_ )) = %s |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
124 |
| tf _ = Imposs "mk_constrainall"; |
1274 | 125 |
in |
126 |
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
|
127 |
fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ); |
1274 | 128 |
end; |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
129 |
|
1274 | 130 |
fun mk_ex (x,P) = mk_exists (x,dummyT,P); |
131 |
fun mk_not P = Const("not" ,boolT --> boolT) $ P; |
|
132 |
end; |
|
133 |
||
134 |
fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *) |
|
135 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
136 |
infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T; |
1274 | 137 |
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
|
138 |
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
|
139 |
infix 1 ===; fun S === T = %%"op =" $ S $ T; |
1274 | 140 |
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
|
141 |
infix 1 <<; fun S << T = %%"op <<" $ S $ T; |
1274 | 142 |
infix 1 ~<<; fun S ~<< T = mk_not (S << T); |
143 |
||
144 |
infix 9 ` ; fun f` x = %%"fapp" $ f $ x; |
|
145 |
infix 9 `% ; fun f`% s = f` % s; |
|
146 |
infix 9 `%%; fun f`%%s = f` %%s; |
|
147 |
fun mk_cfapp (F,As) = foldl (op `) (F,As); |
|
148 |
fun con_app2 con f args = mk_cfapp(%%con,map f args); |
|
149 |
fun con_app con = con_app2 con %#; |
|
150 |
fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; |
|
151 |
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
|
152 |
fun prj _ _ y 1 _ = y |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
153 |
| 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
|
154 |
| 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
|
155 |
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
|
156 |
val proj = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S); |
1274 | 157 |
fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); |
158 |
||
159 |
fun /\ v T = %%"fabs" $ mk_lam(v,T); |
|
160 |
fun /\# (arg,T) = /\ (vname arg) T; |
|
161 |
infixr 9 oo; fun S oo T = %%"cfcomp"`S`T; |
|
162 |
val UU = %%"UU"; |
|
163 |
fun strict f = f`UU === UU; |
|
164 |
fun defined t = t ~= UU; |
|
165 |
fun cpair (S,T) = %%"cpair"`S`T; |
|
166 |
fun lift_defined f = lift (fn x => defined (f x)); |
|
167 |
fun bound_arg vns v = Bound(length vns-find(v,vns)-1); |
|
168 |
||
169 |
fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = |
|
170 |
(case cont_eta_contract body of |
|
171 |
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
|
172 |
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
|
173 |
else Const("fabs",TT) $ Abs(a,T,body') |
1274 | 174 |
| body' => Const("fabs",TT) $ Abs(a,T,body')) |
175 |
| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t |
|
176 |
| cont_eta_contract t = t; |
|
177 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
178 |
fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); |
1834 | 179 |
fun when_funs cons = if length cons = 1 then ["f"] |
180 |
else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
|
1274 | 181 |
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
|
182 |
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
|
183 |
| one_fun n (_,args) = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
184 |
val l2 = length args; |
2276 | 185 |
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
|
186 |
else Id) (Bound(l2-m)); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
187 |
in cont_eta_contract (foldr'' |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
188 |
(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
|
189 |
(args, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
190 |
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
|
191 |
) end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
(foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons)) end; |
1274 | 195 |
end; (* struct *) |