156 fun prj _ _ x ( _::[]) _ = x |
156 fun prj _ _ x ( _::[]) _ = x |
157 | prj f1 _ x (_::y::ys) 0 = f1 x y |
157 | prj f1 _ x (_::y::ys) 0 = f1 x y |
158 | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); |
158 | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); |
159 fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to |
159 fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to |
160 avoid type varaibles *) |
160 avoid type varaibles *) |
161 val proj = prj (fn S => K(%%"fst" $S)) (fn S => K(%%"snd" $S)); |
161 fun proj x = prj (fn S => K(%%"fst" $S)) (fn S => K(%%"snd" $S)) x; |
162 val cproj = prj (fn S => K(%%"cfst"`S)) (fn S => K(%%"csnd"`S)); |
162 fun cproj x = prj (fn S => K(%%"cfst"`S)) (fn S => K(%%"csnd"`S)) x; |
163 fun cproj' T eqs = prj |
163 fun cproj' T eqs = prj |
164 (fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S) |
164 (fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S) |
165 (fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S) |
165 (fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S) |
166 T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs); |
166 T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs); |
167 fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); |
167 fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); |