-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathcore-edits
197 lines (158 loc) · 7.62 KB
/
core-edits
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
191
192
193
194
195
196
197
## These are the edits directly related to the Core syntax
## Not all files need to see these edits
# rename module TyCoRep CoreType
# rename module Type CoreType
# rename module Coercion CoreType
# rename module Var CoreType
# rename module CoAxiom CoreType
# rename module TyCon CoreType
# rename module VarEnv CoreType
# rename module VarSet CoreType
# rename module FV CoreType
# skip MkId
# type used in DataCon
rename type MkId.DataConBoxer = unit
### get rid of some information in the AST
rename type TcType.TcTyVarDetails = Core.TcTyVarDetails
rename type PrimOp.PrimOp = unit
rename type ForeignCall.ForeignCall = unit
## Punning
rename value Var.Id = Var.Mk_Id
rename value Var.TyVar = Var.Mk_TyVar
rename value Var.TcTyVar = Var.Mk_TcTyVar
rename value CoreSyn.IsOrphan = CoreSyn.Mk_IsOrphan
rename value CoreSyn.RuleEnv = CoreSyn.Mk_RuleEnv
rename value DataCon.HsSrcBang = DataCon.Mk_HsSrcBang
rename value DataCon.EqSpec = DataCon.Mk_EqSpec
rename value Class.Class = Class.Mk_Class
rename value IdInfo.RuleInfo = IdInfo.Mk_RuleInfo
rename value CoAxiom = Core.Mk_CoAxiom
rename value TyCoRep.TCvSubst = TyCoRep.Mk_TCvSubst
rename value CoreFVs.FVAnn = CoreFVs.Mk_FVAnn
rename value CoreSubst.Subst = CoreSubst.Mk_Subst
# Note [Strict positivity]
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# These types all contain actual non-strictly-positive function members
# that e.g. take `Type`s or `Pair`s of `Type`s or lists of `Type`s as arguments.
redefine Inductive TyCon.RuntimeRepInfo : Type := TyCon.Mk_RuntimeRepInfo_Dummy.
# notations in Core (must import Core)
rename type TyCoRep.KindOrType = KindOrType
rename type TyCoRep.CoercionN = CoercionN
rename type TyCoRep.KindCoercion = KindCoercion
rename type TyCoRep.Kind = Kind
rename type TyCoRep.PredType = PredType
rename type TyCoRep.ThetaType = ThetaType
## don't use notation that is same as some module name
#rename type Var.Id = Id
rename type Var.TyVar = TyVar
rename type Var.CoVar = CoVar
# Definitions moved to Core
rename type Var.Var = Core.Var
rename type TyCoRep.Type_ = Core.Type_
rename type TyCoRep.Coercion = Core.Coercion
# rename type TyCoRep.TCvSubst = Core.TCvSubst
rename type TyCoRep.TyBinder = Core.TyBinder
rename type CoAxiom.CoAxiom = Core.CoAxiom
rename type CoAxiom.Role = Core.Role
rename value CoAxiom.Nominal = Core.Nominal
rename value CoAxiom.Representational = Core.Representational
rename value CoAxiom.Phantom = Core.Phantom
rename type CoAxiom.CoAxiomRule = Core.CoAxiomRule
rename type CoAxiom.BuiltInSynFamily = Core.BuiltInSynFamily
rename type CoAxiom.BranchIndex = Core.BranchIndex
rename type CoAxiom.BranchFlag = Core.BranchFlag
rename value CoAxiom.Unbranched = Core.Unbranched
rename value CoAxiom.Branched = Core.Branched
## for promotion
rename type CoAxiom.Branched = Core.Branched
rename type CoAxiom.Unbranched = Core.Unbranched
rename type CoAxiom.Branches = Core.Branches
rename value CoAxiom.MkBranches = Core.MkBranches
rename type CoAxiom.CoAxBranch = Core.CoAxBranch
rename value CoAxiom.CoAxBranch = Core.Mk_CoAxBranch
rename type ForeignCall.CType = Core.CType
rename type TyCon.TyConRepName = Core.TyConRepName
rename type TyCon.RuntimeRepInfo = Core.RuntimeRepInfo
rename type TyCon.Injectivity = Core.Injectivity
rename type TyCon.TyCon = Core.TyCon
rename type TyCon.AlgTyConFlav = Core.AlgTyConFlav
rename type TyCoRep.VisibilityFlag = Core.VisibilityFlag
rename type TyCoRep.TyPrec = Core.TyPrec
rename type TyCoRep.TyLit = Core.TyLit
rename type TyCoRep.LeftOrRight = Core.LeftOrRight
rename type TyCoRep.CoercionHold = Core.CoercionHole
rename type TyCoRep.UnivCoProvenance = Core.UnivCoProvenance
rename value TyCoRep.Refl = Core.Refl
rename value TyCoRep.CoVarCo = Core.CoVarCo
rename value TyCoRep.SubCo = Core.SubCo
rename value TyCoRep.TyConAppCo = Core.TyConAppCo
rename value TyCoRep.SymCo = Core.SymCo
rename value TyCoRep.TransCo = Core.TransCo
rename value TyCoRep.AppCo = Core.AppCo
rename value TyCoRep.ForAllCo = Core.ForAllCo
rename value TyCoRep.NthCo = Core.NthCo
rename value TyCoRep.InstCo = Core.InstCo
rename value TyCoRep.CoherenceCo = Core.CoherenceCo
rename value TyCoRep.UnivCo = Core.UnivCo
rename value TyCoRep.AxiomInstCo = Core.AxiomInstCo
rename value TyCoRep.LRCo = Core.LRCo
rename value TyCoRep.AxiomRuleCo = Core.AxiomRuleCo
rename value TyCoRep.KindCo = Core.KindCo
rename value TyCoRep.UnsafeCoerceProv = Core.UnsafeCoerceProv
rename value TyCoRep.PhantomProv = Core.PhantomProv
rename value TyCoRep.ProofIrrelProv = Core.ProofIrrelProv
rename value TyCoRep.PluginProv = Core.PluginProv
rename value TyCoRep.HoleProv = Core.HoleProv
# rename value TyCoRep.mkEmptyTCvSubst = Core.mkEmptyTCvSubst
# rename value TyCoRep.emptyTvSubstEnv = Core.emptyTvSubstEnv
# rename value TyCoRep.emptyCvSubstEnv = Core.emptyCvSubstEnv
rename value TyCoRep.Named = Core.Named
rename value TyCoRep.Anon = Core.Anon
rename value TyCoRep.TyVarTy = Core.TyVarTy
rename value TyCoRep.AppTy = Core.AppTy
rename value TyCoRep.TyConApp = Core.TyConApp
rename value TyCoRep.ForAllTy = Core.ForAllTy
rename value TyCoRep.LitTy = Core.LitTy
rename value TyCoRep.CastTy = Core.CastTy
rename value TyCoRep.CoercionTy = Core.CoercionTy
rename value TysPrim.addrPrimTy = Core.addrPrimTy
rename value TysPrim.charPrimTy = Core.charPrimTy
rename value TysPrim.intPrimTy = Core.intPrimTy
rename value TysPrim.wordPrimTy = Core.wordPrimTy
rename value TysPrim.int64PrimTy = Core.int64PrimTy
rename value TysPrim.word64PrimTy = Core.word64PrimTy
rename value TysPrim.floatPrimTy = Core.floatPrimTy
rename value TysPrim.doublePrimTy = Core.doublePrimTy
rename type Var.ExportFlag = Core.ExportFlag
rename value Var.NotExported = Core.NotExported
rename value Var.Exported = Core.Exported
rename value DataCon.dataConWorkId = Core.dataConWorkId
rename value DataCon.dataConExTyVars = Core.dataConExTyVars
rename value PatSyn.patSynExTyVars = Core.patSynExTyVars
rename value ConLike.conLikeExTyVars = Core.conLikExTyVars
rename value Class.classTyVars = Core.classTyVars
rename value Class.classMethods = Core.classMethods
rename value Class.classAllSelIds = Core.classAllSelIds
rename value Class.classArity = Core.classArity
rename value IdInfo.demandInfo = IdInfo2.demandInfo
rename value IdInfo.strictnessInfo = IdInfo2.strictnessInfo
rename value IdInfo.unfoldingInfo = IdInfo2.unfoldingInfo
rename value IdInfo.setDemandInfo = IdInfo2.setDemandInfo
rename value IdInfo.setStrictnessInfo = IdInfo2.setStrictnessInfo
rename value IdInfo.setUnfoldingInfo = IdInfo2.setUnfoldingInfo
rename value IdInfo.setUnfoldingInfoLazily = IdInfo2.setUnfoldingInfoLazily
rename value IdInfo.ruleInfoFreeVars = IdInfo2.ruleInfoFreeVars
rename value IdInfo.ruleInfoRules = IdInfo2.ruleInfoRules
####
rename value Type.isCoercionTy_maybe = TyCoRep.Type_isCoercionTy_maybe
rename value Type.isCoercionTy = TyCoRep.Type_isCoercionTy
rename value Type.eqType = TyCoRep.eqType
rename value Coercion.coercionKind = TyCoRep.coercionKind
rename value Coercion.mkCoercionType = TyCoRep.mkCoercionType
rename value Coercion.mkSymCo = TyCoRep.mkSymCo
rename value Coercion.mkTransCo = TyCoRep.mkTransCo
rename value Coercion.mkCoVarCo = TyCoRep.mkCoVarCo
rename value Coercion.isReflCo = TyCoRep.isReflCo
rename value Coercion.mkTyConAppCo = TyCoRep.mkTyConAppCo
rename value Coercion.mkAppCo = TyCoRep.mkAppCo
rename value Coercion.mkForAllCo = TyCoRep.mkForAllCo