18 | itr [a] = f2 a |
18 | itr [a] = f2 a |
19 | itr (a::l) = f(a, itr l) |
19 | itr (a::l) = f(a, itr l) |
20 in itr l end; |
20 in itr l end; |
21 fun foldr' f l = foldr'' f (l,Id); |
21 fun foldr' f l = foldr'' f (l,Id); |
22 fun map_cumulr f start xs = foldr (fn (x,(ys,res)) => case f(x,res) of (y,res2) => |
22 fun map_cumulr f start xs = foldr (fn (x,(ys,res)) => case f(x,res) of (y,res2) => |
23 (y::ys,res2)) (xs,([],start)); |
23 (y::ys,res2)) (xs,([],start)); |
24 |
24 |
25 |
25 |
26 fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; |
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); |
27 fun upd_first f (x,y,z) = (f x, y, z); |
28 fun upd_second f (x,y,z) = ( x, f y, z); |
28 fun upd_second f (x,y,z) = ( x, f y, z); |
35 | bb y i j = if i=2 then (f2 y) else bb (f2 y) (i-1) (j-1) |
35 | bb y i j = if i=2 then (f2 y) else bb (f2 y) (i-1) (j-1) |
36 in bb y (length is) j end; |
36 in bb y (length is) j end; |
37 |
37 |
38 fun atomize thm = case concl_of thm of |
38 fun atomize thm = case concl_of thm of |
39 _ $ (Const("op &",_) $ _ $ _) => atomize (thm RS conjunct1) @ |
39 _ $ (Const("op &",_) $ _ $ _) => atomize (thm RS conjunct1) @ |
40 atomize (thm RS conjunct2) |
40 atomize (thm RS conjunct2) |
41 | _ $ (Const("All" ,_) $ Abs (s,_,_)) => atomize (thm RS |
41 | _ $ (Const("All" ,_) $ Abs (s,_,_)) => atomize (thm RS |
42 (read_instantiate [("x","?"^s)] spec)) |
42 (read_instantiate [("x","?"^s)] spec)) |
43 | _ => [thm]; |
43 | _ => [thm]; |
44 |
44 |
45 (* ----- specific support for domain ---------------------------------------------- *) |
45 (* ----- specific support for domain ---------------------------------------------- *) |
46 |
46 |
47 structure Domain_Library = struct |
47 structure Domain_Library = struct |
48 |
48 |
57 | strip (c :: cs) = c :: strip cs |
57 | strip (c :: cs) = c :: strip cs |
58 | strip [] = []; |
58 | strip [] = []; |
59 in implode o strip o explode end; |
59 in implode o strip o explode end; |
60 |
60 |
61 fun extern_name con = case explode con of |
61 fun extern_name con = case explode con of |
62 ("o"::"p"::" "::rest) => implode rest |
62 ("o"::"p"::" "::rest) => implode rest |
63 | _ => con; |
63 | _ => con; |
64 fun dis_name con = "is_"^ (extern_name con); |
64 fun dis_name con = "is_"^ (extern_name con); |
65 fun dis_name_ con = "is_"^ (strip_esc con); |
65 fun dis_name_ con = "is_"^ (strip_esc con); |
66 |
66 |
67 (*make distinct names out of the type list, |
67 (*make distinct names out of the type list, |
68 forbidding "o", "x..","f..","P.." as names *) |
68 forbidding "o", "x..","f..","P.." as names *) |
70 fun mk_var_names types : string list = let |
70 fun mk_var_names types : string list = let |
71 fun typid (Type (id,_) ) = hd (explode id) |
71 fun typid (Type (id,_) ) = hd (explode id) |
72 | typid (TFree (id,_) ) = hd (tl (explode id)) |
72 | typid (TFree (id,_) ) = hd (tl (explode id)) |
73 | typid (TVar ((id,_),_)) = hd (tl (explode id)); |
73 | typid (TVar ((id,_),_)) = hd (tl (explode id)); |
74 fun nonreserved id = let val cs = explode id in |
74 fun nonreserved id = let val cs = explode id in |
75 if not(hd cs mem ["x","f","P"]) then id |
75 if not(hd cs mem ["x","f","P"]) then id |
76 else implode(chr(1+ord (hd cs))::tl cs) end; |
76 else implode(chr(1+ord (hd cs))::tl cs) end; |
77 fun index_vnames(vn::vns,tab) = |
77 fun index_vnames(vn::vns,tab) = |
78 (case assoc(tab,vn) of |
78 (case assoc(tab,vn) of |
79 None => if vn mem vns |
79 None => if vn mem vns |
80 then (vn^"1") :: index_vnames(vns,(vn,2)::tab) |
80 then (vn^"1") :: index_vnames(vns,(vn,2)::tab) |
81 else vn :: index_vnames(vns, tab) |
81 else vn :: index_vnames(vns, tab) |
94 infixr 6 ~>; val op ~> = mk_typ "->"; |
94 infixr 6 ~>; val op ~> = mk_typ "->"; |
95 val NoSyn' = ThyOps.Mixfix NoSyn; |
95 val NoSyn' = ThyOps.Mixfix NoSyn; |
96 |
96 |
97 (* ----- constructor list handling ----- *) |
97 (* ----- constructor list handling ----- *) |
98 |
98 |
99 type cons = (string * (* operator name of constr *) |
99 type cons = (string * (* operator name of constr *) |
100 ((bool*int)* (* (lazy,recursive element or ~1) *) |
100 ((bool*int)* (* (lazy,recursive element or ~1) *) |
101 string* (* selector name *) |
101 string* (* selector name *) |
102 string) (* argument name *) |
102 string) (* argument name *) |
103 list); (* argument list *) |
103 list); (* argument list *) |
104 type eq = (string * (* name of abstracted type *) |
104 type eq = (string * (* name of abstracted type *) |
105 typ list) * (* arguments of abstracted type *) |
105 typ list) * (* arguments of abstracted type *) |
106 cons list; (* represented type, as a constructor list *) |
106 cons list; (* represented type, as a constructor list *) |
107 |
107 |
108 val rec_of = snd o first; |
108 val rec_of = snd o first; |
109 val is_lazy = fst o first; |
109 val is_lazy = fst o first; |
110 val sel_of = second; |
110 val sel_of = second; |
111 val vname = third; |
111 val vname = third; |
112 val upd_vname = upd_third; |
112 val upd_vname = upd_third; |
113 fun is_rec arg = rec_of arg >=0; |
113 fun is_rec arg = rec_of arg >=0; |
114 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
114 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
115 fun nonlazy args = map vname (filter_out is_lazy args); |
115 fun nonlazy args = map vname (filter_out is_lazy args); |
116 fun is_one_con_one_arg p cons = length cons = 1 andalso let val args = snd(hd cons) in |
116 fun is_one_con_one_arg p cons = length cons = 1 andalso let val args = snd(hd cons) in |
117 length args = 1 andalso p (hd args) end; |
117 length args = 1 andalso p (hd args) end; |
118 |
118 |
119 (* ----- support for term expressions ----- *) |
119 (* ----- support for term expressions ----- *) |
120 |
120 |
121 fun % s = Free(s,dummyT); |
121 fun % s = Free(s,dummyT); |
122 fun %# arg = %(vname arg); |
122 fun %# arg = %(vname arg); |
128 fun mk_disj (S,T) = disj $ S $ T; |
128 fun mk_disj (S,T) = disj $ S $ T; |
129 fun mk_imp (S,T) = imp $ S $ T; |
129 fun mk_imp (S,T) = imp $ S $ T; |
130 fun mk_lam (x,T) = Abs(x,dummyT,T); |
130 fun mk_lam (x,T) = Abs(x,dummyT,T); |
131 fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); |
131 fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); |
132 local |
132 local |
133 fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) |
133 fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) |
134 | tf (TFree(s,_ )) = %s |
134 | tf (TFree(s,_ )) = %s |
135 | tf _ = Imposs "mk_constrainall"; |
135 | tf _ = Imposs "mk_constrainall"; |
136 in |
136 in |
137 fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ; |
137 fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ; |
138 fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs"$Abs(x,dummyT,P)$tf typ); |
138 fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs"$Abs(x,dummyT,P)$tf typ); |
139 end; |
139 end; |
140 |
140 |
141 fun mk_ex (x,P) = mk_exists (x,dummyT,P); |
141 fun mk_ex (x,P) = mk_exists (x,dummyT,P); |
142 fun mk_not P = Const("not" ,boolT --> boolT) $ P; |
142 fun mk_not P = Const("not" ,boolT --> boolT) $ P; |
143 end; |
143 end; |
144 |
144 |
145 fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *) |
145 fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *) |
175 fun bound_arg vns v = Bound(length vns-find(v,vns)-1); |
175 fun bound_arg vns v = Bound(length vns-find(v,vns)-1); |
176 |
176 |
177 fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = |
177 fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = |
178 (case cont_eta_contract body of |
178 (case cont_eta_contract body of |
179 body' as (Const("fapp",Ta) $ f $ Bound 0) => |
179 body' as (Const("fapp",Ta) $ f $ Bound 0) => |
180 if not (0 mem loose_bnos f) then incr_boundvars ~1 f |
180 if not (0 mem loose_bnos f) then incr_boundvars ~1 f |
181 else Const("fabs",TT) $ Abs(a,T,body') |
181 else Const("fabs",TT) $ Abs(a,T,body') |
182 | body' => Const("fabs",TT) $ Abs(a,T,body')) |
182 | body' => Const("fabs",TT) $ Abs(a,T,body')) |
183 | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t |
183 | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t |
184 | cont_eta_contract t = t; |
184 | cont_eta_contract t = t; |
185 |
185 |
186 fun idx_name dnames s n = s ^ (if length dnames = 1 then "" else string_of_int n); |
186 fun idx_name dnames s n = s ^ (if length dnames = 1 then "" else string_of_int n); |
187 fun when_funs cons = if length cons = 1 then ["f"] |
187 fun when_funs cons = if length cons = 1 then ["f"] |
188 else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
188 else mapn (fn n => K("f"^(string_of_int n))) 1 cons; |
189 fun when_body cons funarg = let |
189 fun when_body cons funarg = let |
190 fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) |
190 fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) |
191 | one_fun n (_,args) = let |
191 | one_fun n (_,args) = let |
192 val l2 = length args; |
192 val l2 = length args; |
193 fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x |
193 fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x |
194 else Id) (Bound(l2-m)); |
194 else Id) (Bound(l2-m)); |
195 in cont_eta_contract (foldr'' |
195 in cont_eta_contract (foldr'' |
196 (fn (a,t) => %%"ssplit"`(/\# (a,t))) |
196 (fn (a,t) => %%"ssplit"`(/\# (a,t))) |
197 (args, |
197 (args, |
198 fn a => /\# (a,(mk_cfapp(funarg (l2,n),mapn idxs 1 args)))) |
198 fn a => /\# (a,(mk_cfapp(funarg (l2,n),mapn idxs 1 args)))) |
199 ) end; |
199 ) end; |
200 in foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons) end; |
200 in foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons) end; |
201 |
201 |
202 end; (* struct *) |
202 end; (* struct *) |