1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
module T11195 where
import TyCoRep
import Coercion
import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
import TcType ( exactTyCoVarsOfType )
import CoAxiom
import VarSet
import VarEnv
import Pair
import InstEnv
type NormalCo = Coercion
type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
type SymFlag = Bool
type ReprFlag = Bool
chooseRole :: ReprFlag -> Role -> Role
chooseRole = undefined
wrapRole :: ReprFlag -> Role -> Coercion -> Coercion
wrapRole = undefined
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym = undefined
optForAllCoBndr :: LiftingContext -> Bool
-> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
optForAllCoBndr = undefined
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans = undefined
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
-> Type -> Type -> Coercion
opt_univ = undefined
opt_co3 :: LiftingContext -> SymFlag -> Maybe Role
-> Role -> Coercion -> NormalCo
opt_co3 = undefined
opt_co2 :: LiftingContext -> SymFlag -> Role -> Coercion -> NormalCo
opt_co2 = undefined
compatible_co :: Coercion -> Coercion -> Bool
compatible_co = undefined
etaTyConAppCo_maybe = undefined
etaAppCo_maybe = undefined
etaForAllCo_maybe = undefined
matchAxiom = undefined
checkAxInstCo = undefined
isAxiom_maybe = undefined
isCohLeft_maybe = undefined
isCohRight_maybe = undefined
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
| d1 == d2
, co1 `compatible_co` co2 = undefined
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
| d1 == d2
, co1 `compatible_co` co2 = undefined
-- Push transitivity inside instantiation
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
| ty1 `eqCoercion` ty2
, co1 `compatible_co` co2 = undefined
opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
in_co2@(UnivCo p2 r2 _tyl2 tyr2)
| Just prov' <- opt_trans_prov p1 p2 = undefined
where
-- if the provenances are different, opt'ing will be very confusing
opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv
= Just UnsafeCoerceProv
opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
= Just $ PhantomProv $ opt_trans is kco1 kco2
opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
= Just $ ProofIrrelProv $ opt_trans is kco1 kco2
opt_trans_prov (PluginProv str1) (PluginProv str2)
| str1 == str2 = Just p1
opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1)
in_co2@(TyConAppCo r2 tc2 cos2)
| tc1 == tc2 = undefined
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
= undefined
-- Eta rules
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
| Just cos2 <- etaTyConAppCo_maybe tc co2 = undefined
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
| Just cos1 <- etaTyConAppCo_maybe tc co1 = undefined
opt_trans_rule is co1@(AppCo co1a co1b) co2
| Just (co2a,co2b) <- etaAppCo_maybe co2 = undefined
opt_trans_rule is co1 co2@(AppCo co2a co2b)
| Just (co1a,co1b) <- etaAppCo_maybe co1 = undefined
-- Push transitivity inside forall
opt_trans_rule is co1 co2
| ForAllCo tv1 eta1 r1 <- co1
, Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
| ForAllCo tv2 eta2 r2 <- co2
, Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined
where
push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
-- Push transitivity inside axioms
opt_trans_rule is co1 co2
| Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
, True <- sym
, Just cos2 <- matchAxiom sym con ind co2
, let newAxInst = AxiomInstCo con ind
(opt_transList is (map mkSymCo cos2) cos1)
, Nothing <- checkAxInstCo newAxInst
= undefined
-- TrPushAxR
| Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
, False <- sym
, Just cos2 <- matchAxiom sym con ind co2
, let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
, Nothing <- checkAxInstCo newAxInst
= undefined
-- TrPushSymAxL
| Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
, True <- sym
, Just cos1 <- matchAxiom (not sym) con ind co1
, let newAxInst = AxiomInstCo con ind
(opt_transList is cos2 (map mkSymCo cos1))
, Nothing <- checkAxInstCo newAxInst
= undefined
-- TrPushAxL
| Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
, False <- sym
, Just cos1 <- matchAxiom (not sym) con ind co1
, let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
, Nothing <- checkAxInstCo newAxInst
= undefined
-- TrPushAxSym/TrPushSymAx
| Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
, Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
, con1 == con2
, ind1 == ind2
, sym1 == not sym2
, let branch = coAxiomNthBranch con1 ind1
qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
lhs = coAxNthLHS con1 ind1
rhs = coAxBranchRHS branch
pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
, all (`elemVarSet` pivot_tvs) qtvs
= undefined
where
co1_is_axiom_maybe = isAxiom_maybe co1
co2_is_axiom_maybe = isAxiom_maybe co2
role = coercionRole co1 -- should be the same as coercionRole co2!
opt_trans_rule is co1 co2
| Just (lco, lh) <- isCohRight_maybe co1
, Just (rco, rh) <- isCohLeft_maybe co2
, (coercionType lh) `eqType` (coercionType rh)
= undefined
opt_trans_rule _ co1 co2 -- Identity rule
| (Pair ty1 _, r) <- coercionKindRole co1
, Pair _ ty2 <- coercionKind co2
, ty1 `eqType` ty2
= undefined
opt_trans_rule _ _ _ = Nothing
|
