96 @ (if contra then [(T' --> T)] else []); |
96 @ (if contra then [(T' --> T)] else []); |
97 val contras = maps (fn (_, (co, contra)) => |
97 val contras = maps (fn (_, (co, contra)) => |
98 (if co then [false] else []) @ (if contra then [true] else [])) variances; |
98 (if co then [false] else []) @ (if contra then [true] else [])) variances; |
99 val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); |
99 val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); |
100 val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); |
100 val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); |
101 fun invents n k nctxt = |
|
102 let |
|
103 val names = Name.invent nctxt n k; |
|
104 in (names, fold Name.declare names nctxt) end; |
|
105 val ((names21, names32), nctxt) = Variable.names_of ctxt |
101 val ((names21, names32), nctxt) = Variable.names_of ctxt |
106 |> invents "f" (length Ts21) |
102 |> Name.invent' "f" (length Ts21) |
107 ||>> invents "f" (length Ts32); |
103 ||>> Name.invent' "f" (length Ts32); |
108 val T1 = Type (tyco, Ts1); |
104 val T1 = Type (tyco, Ts1); |
109 val T2 = Type (tyco, Ts2); |
105 val T2 = Type (tyco, Ts2); |
110 val T3 = Type (tyco, Ts3); |
106 val T3 = Type (tyco, Ts3); |
111 val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); |
107 val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); |
112 val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => |
108 val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => |