forked from plclub/hs-to-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathedits
223 lines (201 loc) · 10.5 KB
/
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
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
####################################################
# Replace IntMap with Map
####################################################
rename type Data.IntMap.Internal.IntMap = IntMap.IntMap
rename value Data.IntMap.Internal.empty = IntMap.empty
rename value Data.IntMap.Internal.singleton = IntMap.singleton
rename value Data.IntMap.Internal.null = IntMap.null
rename value Data.IntMap.Internal.keys = IntMap.keys
rename value Data.IntMap.Internal.keysSet = IntMap.keysSet
rename value Data.IntMap.Internal.elems = IntMap.elems
rename value Data.IntMap.Internal.member = IntMap.member
rename value Data.IntMap.Internal.size = IntMap.size
rename value Data.IntMap.Internal.insert = IntMap.insert
rename value Data.IntMap.Internal.insertWith = IntMap.insertWith
rename value Data.IntMap.Internal.delete = IntMap.delete
rename value Data.IntMap.Internal.alter = IntMap.alter
rename value Data.IntMap.Internal.adjust = IntMap.adjust
rename value Data.IntMap.Internal.map = IntMap.map
rename value Data.IntMap.Internal.mapWithKey = IntMap.mapWithKey
rename value Data.IntMap.Internal.mergeWithKey = IntMap.mergeWithKey
rename value Data.IntMap.Internal.filter = IntMap.filter
rename value Data.IntMap.Internal.filterWithKey = IntMap.filterWithKey
rename value Data.IntMap.Internal.union = IntMap.union
rename value Data.IntMap.Internal.unionWith = IntMap.unionWith
rename value Data.IntMap.Internal.intersection = IntMap.intersection
rename value Data.IntMap.Internal.intersectionWith = IntMap.intersectionWith
rename value Data.IntMap.Internal.difference = IntMap.difference
rename value Data.IntMap.Internal.partition = IntMap.partition
rename value Data.IntMap.Internal.toList = IntMap.toList
rename value Data.IntMap.Internal.foldr = IntMap.foldr
rename value Data.IntMap.Internal.foldrWithKey = IntMap.foldrWithKey
rename value Data.IntMap.Internal.findWithDefault = IntMap.findWithDefault
rename value Data.IntMap.Internal.lookup = IntMap.lookup
####################################################
### DVarSet => VarSet, DVarEnv => VarEnv
##
## We do this translation by implementing DVarSets using
## the same implementation as VarSets. (Both are definitions
## in Coq.)
rename type UniqDSet.UniqDSet = UniqSet.UniqSet
rename value UniqDSet.unitUniqDSet = UniqSet.unitUniqSet
rename value UniqDSet.unionManyUniqDSets = UniqSet.unionManyUniqSets
rename value UniqDSet.unionUniqDSets = UniqSet.unionUniqSets
rename value UniqDSet.sizeUniqDSet = UniqSet.sizeUniqSet
rename value UniqDSet.partitionUniqDSet = UniqSet.partitionUniqSet
rename value UniqDSet.mkUniqDSet = UniqSet.mkUniqSet
rename value UniqDSet.minusUniqDSet = UniqSet.minusUniqSet
rename value UniqDSet.isEmptyUniqDSet = UniqSet.isEmptyUniqSet
rename value UniqDSet.intersectUniqDSets = UniqSet.intersectUniqSets
rename value UniqDSet.foldUniqDSet = UniqSet.nonDetFoldUniqSet
rename value UniqDSet.filterUniqDSet = UniqSet.filterUniqSet
rename value UniqDSet.addOneToUniqDSet = UniqSet.addOneToUniqSet
rename value UniqDSet.addListToUniqDSet = UniqSet.addListToUniqSet
rename value UniqDSet.emptyUniqDSet = UniqSet.emptyUniqSet
rename value UniqDSet.delOneFromUniqDSet = UniqSet.delOneFromUniqSet
rename value UniqDSet.delListFromUniqDSet = UniqSet.delListFromUniqSet
rename value UniqDSet.elementOfUniqDSet = UniqSet.elementOfUniqSet
rename value UniqDSet.uniqDSetMinusUniqSet = UniqSet.minusUniqSet
rename value UniqDSet.uniqDSetIntersectUniqSet = UniqSet.intersectUniqSets
rename value UniqDSet.uniqDSetToList = UniqSet.nonDetEltsUniqSet
rename value UniqDSet.foldDVarSet = Core.nonDetFoldUniqSet
redefine Definition Core.disjointDVarSet := Core.disjointVarSet.
redefine Definition Core.anyDVarSet := Core.anyVarSet.
redefine Definition Core.allDVarSet := Core.allVarSet.
redefine Definition Core.dVarSetToVarSet : DVarSet -> VarSet := fun x => x.
redefine Definition FV.fvDVarSet : FV.FV -> Core.DVarSet := FV.fvVarSet.
rename type UniqDFM.UniqDFM = UniqFM.UniqFM
rename value UniqDFM.unitUDFM = UniqFM.unitUFM
rename value UniqDFM.addListToUDFM = UniqFM.addListToUFM
rename value UniqDFM.addToUDFM = UniqFM.addToUFM
rename value UniqDFM.addToUDFM_C = UniqFM.addToUFM_C
rename value UniqDFM.allUDFM = UniqFM.allUFM
rename value UniqDFM.alterUDFM = UniqFM.alterUFM
rename value UniqDFM.anyUDFM = UniqFM.anyUFM
rename value UniqDFM.delFromUDFM = UniqFM.delFromUFM
rename value UniqDFM.delListFromUDFM = UniqFM.delListFromUFM
rename value UniqDFM.disjointUDFM = UniqFM.disjointUFM
rename value UniqDFM.elemUDFM = UniqFM.elemUFM
rename value UniqDFM.eltsUDFM = UniqFM.eltsUFM
rename value UniqDFM.emptyUDFM = UniqFM.emptyUFM
rename value UniqDFM.filterUDFM = UniqFM.filterUFM
rename value UniqDFM.foldUDFM = UniqFM.nonDetFoldUFM
rename value UniqDFM.isNullUDFM = UniqFM.isNullUFM
rename value UniqDFM.listToUDFM = UniqFM.listToUFM
rename value UniqDFM.lookupUDFM = UniqFM.lookupUFM
rename value UniqDFM.mapUDFM = UniqFM.mapUFM
rename value UniqDFM.minusUDFM = UniqFM.minusUFM
rename value UniqDFM.partitionUDFM = UniqFM.partitionUFM
rename value UniqDFM.plusUDFM = UniqFM.plusUFM
rename value UniqDFM.plusUDFM_C = UniqFM.plusUFM_C
rewrite forall x, UniqDFM.udfmToUfm x = x
rename value UniqDFM.unitUFM = UniqDFM.unitUFM
####################################################
# Edits related to base
####################################################
# specialize generic method to (->) constructor
# to make type inference easier
rename value Control.Arrow.first = Control.Arrow.arrow_first
rename value Control.Arrow.second = Control.Arrow.arrow_second
####################################################
# Now we are serious
####################################################
# Should skip these everywhere
skip module Outputable
skip module GHC.Show
skip module Deriving
# TODO: better treatment of primitive values
skip module GHC.Int
skip module GHC.Word
# packages we don't yet support 'bytestring'
rename type Data.ByteString.Internal.ByteString = GHC.Base.String
# packages we don't yet support 'integer-simple' and 'integer-gmp'
skip module GHC.Integer.Type
rename type GHC.Integer.Type.Integer = GHC.Num.Integer
# partial functions
rename value GHC.List.head = GHC.Err.head
# we're not debugging
# rewrite forall x, andb Util.debugIsOn x = false
# don't try to format the error messages
rename type Outputable.SDoc = GHC.Base.String
rename value Outputable.pprPanic = Panic.panicStr
rename value Outputable.<+> = GHC.Base.mappend
rename value Outputable.<> = GHC.Base.mappend
rename value Outputable.text = Datatypes.id
rename value Outputable.empty = Panic.someSDoc
rename value Outputable.comma = Panic.someSDoc
rewrite forall x, Outputable.ppr x = Panic.someSDoc
rewrite forall x, Outputable.ptext x = Panic.someSDoc
rewrite forall x, Outputable.int x = Panic.someSDoc
rewrite forall x, Outputable.char x = Panic.someSDoc
rewrite forall x, Outputable.ftext x = Panic.someSDoc
rewrite forall x, Outputable.fsep x = Panic.someSDoc
rewrite forall x, Outputable.vcat x = Panic.someSDoc
rename value Outputable.vbar = Panic.someSDoc
rename value Outputable.warnPprTrace = Panic.warnPprTrace
rewrite forall x, Outputable.parens x = x
rewrite forall x, Outputable.brackets x = x
rewrite forall x, Outputable.doubleQuotes x = x
rewrite forall x y, Outputable.punctuate x y = Panic.someSDoc
rewrite forall x str msg, Outputable.pprTraceDebug str msg x = x
rewrite forall x y, x Outputable.$$ y = Panic.someSDoc
rewrite forall v str num msg, Outputable.warnPprTrace b str num msg v = v
rewrite forall s n d, Outputable.assertPprPanic s n d = GHC.Err.error d
rewrite forall x y, x Outputable.$$ y = x
# Skip serialization-related classes…
skip class Outputable.Outputable
skip class Outputable.OutputableBndr
skip class Json.ToJson
skip class Binary.Binary
# …and other non-interesting classes
skip class GHC.PackageDb.BinaryStringRep
skip class GHC.PackageDb.DbUnitIdModuleRep
# Punned
rename value BasicTypes.EP = BasicTypes.Mk_EP
rename value BasicTypes.Fixity = BasicTypes.Mk_Fixity
rename value BasicTypes.InlinePragma = BasicTypes.Mk_InlinePragma
rename value BasicTypes.OverlapFlag = BasicTypes.Mk_OverlapFlag
rename value BasicTypes.StringLiteral = BasicTypes.Mk_StringLiteral
rename value BasicTypes.SourceText = BasicTypes.Mk_SourceText
rename value BasicTypes.WarningTxt = BasicTypes.Mk_WarningTxt
rename value CmmType.CmmType = CmmType.Mk_CmmType
rename value Pair.Pair = Pair.Mk_Pair
rename value SourceLoc.L = SourceLoc.Mk_L
rename value DynFlags.PackageArg = DynFlags.Mk_PackageArg
rename value DynFlags.Option = DynFlags.Mk_Option
rename value DynFlags.ModRenaming = DynFlags.Mk_ModRenaming
rename value DynFlags.FlushOut = DynFlags.Mk_FlushOut
rename value DynFlags.LlvmTarget = DynFlags.Mk_LlvmTarget
rename value DynFlags.FilesToClean = DynFlags.Mk_FilesToClean
rename value Module.Module = Module.Mk_Module
rename value Module.ModuleName = Module.Mk_ModuleName
rename value Module.NDModule = Module.Mk_NDModule
rename value Module.ModLocation = Module.Mk_ModLocation
rename value Module.ModuleEnv = Module.Mk_ModuleEnv
rename value Module.ComponentId = Module.Mk_ComponentId
rename value Module.IndefUnitId = Module.Mk_IndefUnitId
rename value Module.IndefModule = Module.Mk_IndefModule
rename value OccName.OccName = OccName.Mk_OccName
rename value Name.Name = Name.Mk_Name
rename value Name.BuiltInSyntax = Name.Mk_BuiltInSyntax
rename value FieldLabel.FieldLabel = FieldLabel.Mk_FieldLabel
rename value UniqDFM.TaggedVal = UniqDFM.Mk_TaggedVal
rename value UniqDFM.UniqDFM = UniqDFM.Mk_UniqDFM
rename value UniqSet.UniqSet = UniqSet.Mk_UniqSet
rename value EnumSet.EnumSet = EnumSet.Mk_EnumSet
rename value Module.InstalledUnitId = Module.Mk_InstalledUnitId
rename value Module.InstalledModule = Module.Mk_InstalledModule
rename value Module.InstalledModuleEnv = Module.Mk_InstalledModuleEnv
rename value Module.DefUnitId = Module.Mk_DefUnitId
rename value BooleanFormula.Clause = BooleanFormula.Mk_Clause
rename value CoreType.CoAxiomRule = CoreType.Mk_CoAxiomRule
rename value CoreType.CoAxBranch = CoreType.Mk_CoAxBranch
rename value CoreType.BuiltInSynFamily = CoreType.Mk_BuiltInSynFamily
rename value CoreType.Branched = CoreType.Mk_Branched
rename value CoreType.Unbranched = CoreType.Mk_Unbranched
rename value State.State = State.Mk_State
# These constructor are named after their argument, not their return type,
# so use a different, non-confusing convention here
rename value SrcLoc.RealSrcLoc = SrcLoc.ARealSrcLoc
rename value SrcLoc.RealSrcSpan = SrcLoc.ARealSrcSpan
rename value SrcLoc.SrcLoc = SrcLoc.ASrcLoc