109 end; |
109 end; |
110 |
110 |
111 (* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) |
111 (* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) |
112 (*####*) |
112 (*####*) |
113 fun op_to_fun true sign (Type("->" ,[larg,t]))= |
113 fun op_to_fun true sign (Type("->" ,[larg,t]))= |
114 Type("fun",[larg,op_to_fun true sign t]) |
114 Type("fun",[larg,op_to_fun true sign t]) |
115 | op_to_fun false sign (Type("->",[args,res])) = let |
115 | op_to_fun false sign (Type("->",[args,res])) = let |
116 fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs]) |
116 fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs]) |
117 | otf t = Type("fun",[t,res]); |
117 | otf t = Type("fun",[t,res]); |
118 in otf args end |
118 in otf args end |
119 | op_to_fun _ sign t = t(*error("Wrong type for cinfix/cmixfix : "^ |
119 | op_to_fun _ sign t = t(*error("Wrong type for cinfix/cmixfix : "^ |
120 (Sign.string_of_typ sign t))*); |
120 (Sign.string_of_typ sign t))*); |
121 (*####*) |
121 (*####*) |
122 |
122 |
123 (* oldstyle is called by add_ext_axioms(_i) *) |
123 (* oldstyle is called by add_ext_axioms(_i) *) |
165 (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [ |
165 (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [ |
166 Constant (mk_internal_name name),Variable "A"]),Variable "B"])) |
166 Constant (mk_internal_name name),Variable "A"]),Variable "B"])) |
167 ::xrules_of true tail |
167 ::xrules_of true tail |
168 (*####*) |
168 (*####*) |
169 | xrules_of true ((name,typ,CMixfix(_))::tail) = let |
169 | xrules_of true ((name,typ,CMixfix(_))::tail) = let |
170 fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t |
170 fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t |
171 | argnames _ _ = []; |
171 | argnames _ _ = []; |
172 val names = argnames (ord"A") typ; |
172 val names = argnames (ord"A") typ; |
173 in if names = [] then [] else [mk_appl (Constant name) (map Variable names)<-> |
173 in if names = [] then [] else [mk_appl (Constant name) (map Variable names)<-> |
174 foldl (fn (t,arg) => (mk_appl (Constant "@fapp") [t,Variable arg])) |
174 foldl (fn (t,arg) => (mk_appl (Constant "@fapp") [t,Variable arg])) |
175 (Constant name,names)] end |
175 (Constant name,names)] end |
176 @xrules_of true tail |
176 @xrules_of true tail |
177 (*####*) |
177 (*####*) |
178 | xrules_of false ((name,typ,CInfixl(i))::tail) = |
178 | xrules_of false ((name,typ,CInfixl(i))::tail) = |
179 ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <-> |
179 ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <-> |
180 (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
180 (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
185 (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
185 (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
186 (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])) |
186 (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])) |
187 ::xrules_of false tail |
187 ::xrules_of false tail |
188 (*####*) |
188 (*####*) |
189 | xrules_of false ((name,typ,CMixfix(_))::tail) = let |
189 | xrules_of false ((name,typ,CMixfix(_))::tail) = let |
190 fun foldr' f l = |
190 fun foldr' f l = |
191 let fun itr [] = raise LIST "foldr'" |
191 let fun itr [] = raise LIST "foldr'" |
192 | itr [a] = a |
192 | itr [a] = a |
193 | itr (a::l) = f(a, itr l) |
193 | itr (a::l) = f(a, itr l) |
194 in itr l end; |
194 in itr l end; |
195 fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t |
195 fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t |
196 | argnames n _ = [chr n]; |
196 | argnames n _ = [chr n]; |
197 val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t |
197 val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t |
198 | _ => []); |
198 | _ => []); |
199 in if vars = [] then [] else [mk_appl (Constant name) vars <-> |
199 in if vars = [] then [] else [mk_appl (Constant name) vars <-> |
200 (mk_appl (Constant "@fapp") [Constant name, case vars of [v] => v |
200 (mk_appl (Constant "@fapp") [Constant name, case vars of [v] => v |
201 | args => mk_appl (Constant "@ctuple") [hd args,foldr' (fn (t,arg) => |
201 | args => mk_appl (Constant "@ctuple") [hd args,foldr' (fn (t,arg) => |
202 mk_appl (Constant "_args") [t,arg]) (tl args)]])] |
202 mk_appl (Constant "_args") [t,arg]) (tl args)]])] |
203 end |
203 end |
204 @xrules_of false tail |
204 @xrules_of false tail |
205 (*####*) |
205 (*####*) |
206 | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail |
206 | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail |
207 | xrules_of _ [] = []; |
207 | xrules_of _ [] = []; |
208 end; |
208 end; |