forked from plclub/hs-to-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathaxiomatize-types.edits
337 lines (275 loc) · 13.7 KB
/
axiomatize-types.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
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
# This version of the core edit files axiomatizes types
#
skip module Unify
skip module TcType
skip module RepType
skip module ForeignCall
skip module PprCore
skip module Data.ByteString
skip module ErrUtils
skip module CostCentre
skip module Platform
####################################################
## Most of the time, we are counting
rename type GHC.Num.Int = nat
rewrite forall, Data.Foldable.length = Coq.Lists.List.length
rewrite forall x y, GHC.List.replicate x y = Coq.Lists.List.repeat y x
rewrite forall x, GHC.List.take x = Coq.Lists.List.firstn x
rewrite forall x, GHC.List.drop x = Coq.Lists.List.skipn x
####################################################
#
# Here are some edits to redefine the VarSet to use invariants.
# However, making this change will require many modifications to our
# proofs.
# redefine Definition Core.VarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.DVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.CoVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.TyVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.DTyVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.TyCoVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.DTyCoVarSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.IdSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition Core.DIdSet := (UniqSetInv.UniqSet Core.Var).
# redefine Definition NameSet.NameSet := (UniqSetInv.UniqSet Name.Name).
# add type Core Instance Core.Uniquable__Var2 : (Unique.Uniquable Core.Var) :=
# fun _ k__ => k__ (Unique.Uniquable__Dict_Build _
# (fun v => (Unique.mkUniqueGrimily (match v with
# | Core.Mk_Id _ x _ _ _ _ => x end)))).
# order Core.Uniquable__Var2 Core.VarSet Core.DVarSet Core.CoVarSet Core.TyVarSet Core.DTyVarSEt Core.TyCOVarSet Core.DTyCoVarSet Core.IdSet Core.DIdSet
# rename value UniqSet.unitUniqSet = UniqSetInv.unitUniqSet
# rename value UniqSet.unionManyUniqSets = UniqSetInv.unionManyUniqSets
# rename value UniqSet.unionUniqSets = UniqSetInv.unionUniqSets
# rename value UniqSet.sizeUniqSet = UniqSetInv.sizeUniqSet
# rename value UniqSet.mkUniqSet = UniqSetInv.mkUniqSet
# rename value UniqSet.minusUniqSet = UniqSetInv.minusUniqSet
# rename value UniqSet.lookupUniqSet = UniqSetInv.lookupUniqSet
# rename value UniqSet.lookupUniqSet_Directly = UniqSetInv.lookupUniqSet_Directly
# rename value UniqSet.isEmptyUniqSet = UniqSetInv.isEmptyUniqSet
# rename value UniqSet.intersectUniqSets = UniqSetInv.intersectUniqSets
# rename value UniqSet.partitionUniqSet = UniqSetInv.partitionUniqSet
# rename value UniqSet.nonDetFoldUniqSet = UniqSetInv.nonDetFoldUniqSet
# rename value UniqSet.filterUniqSet = UniqSetInv.filterUniqSet
# rename value UniqSet.addOneToUniqSet = UniqSetInv.addOneToUniqSet
# rename value UniqSet.addListToUniqSet = UniqSetInv.addListToUniqSet
# rename value UniqSet.emptyUniqSet = UniqSetInv.emptyUniqSet
# rename value UniqSet.elemUniqSet_Directly = UniqSetInv.elemUniqSet_Directly
# rename value UniqSet.delOneFromUniqSet = UniqSetInv.delOneFromUniqSet
# rename value UniqSet.delOneFromUniqSet_Directly = UniqSetInv.delOneFromUniqSet_Directly
# rename value UniqSet.delListFromUniqSet = UniqSetInv.delListFromUniqSet
# rename value UniqSet.elementOfUniqSet = UniqSetInv.elementOfUniqSet
# rename value UniqSet.getUniqSet = UniqSetInv.getUniqSet
# rename value UniqSet.nonDetEltsUniqSet = UniqSetInv.nonDetEltsUniqSet
# rename value UniqSet.uniqSetAny = UniqSetInv.uniqSetAny
# rename value UniqSet.uniqSetAll = UniqSetInv.uniqSetAll
# rename value UniqSet.restrictUniqSetToUFM = UniqSetInv.restrictUniqSetToUFM
# rename value UniqSet.nonDetKeysUniqSet = UniqSetInv.nonDetKeysUniqSet
# preserve abstraction
# redefine Core.disjointVarSet : Core.VarSet -> Core.VarSet -> bool := UniqSetInv.disjointUniqSet
####################################################
## Glueing together the Core
####################################################
#
# This must stay in sync with the Makefile
#
rename module Var Core
rename module IdInfo Core
rename module VarSet Core
rename module VarEnv Core
rename module CoreSyn Core
rename module Class Core
axiomatize original module name Class
rename module TyCon Core
axiomatize original module name TyCon
rename module DataCon Core
axiomatize original module name DataCon
rename module PatSyn Core
axiomatize original module name PatSyn
rename module Demand Core
axiomatize original module name Demand
rename module Type Core
axiomatize original module name Type
rename module TyCoRep Core
axiomatize original module name TyCoRep
rename module Coercion Core
axiomatize original module name Coercion
#
# Punned constructor values (in Core)
#
rename value DataCon.HsSrcBang = Core.Mk_HsSrcBang
rename value DataCon.EqSpec = Core.Mk_EqSpec
rename value Class.Class = Core.Mk_Class
rename value Var.Id = Core.Mk_Id
# rename value Var.TyVar = Core.Mk_TyVar
# rename value Var.TcTyVar = Core.Mk_TcTyVar
rename value IdInfo.IdInfo = Core.Mk_IdInfo
rename value IdInfo.DFunId = Core.Mk_DFunId
rename value IdInfo.JoinId = Core.Mk_JoinId
rename value CoreSyn.Var = Core.Mk_Var
rename value CoreSyn.IsOrphan = Core.Mk_IsOrphan
rename value CoreSyn.RuleEnv = Core.Mk_RuleEnv
rename value Demand.ExnStr = Core.Mk_ExnStr
rename value Demand.Str = Core.Mk_Str
rename value Demand.Use = Core.Mk_Use
rename value Demand.DmdType = Core.Mk_DmdType
rename value Demand.StrictSig = Core.Mk_StrictSig
rename value Demand.KillFlags = Core.Mk_KillFlags
rename value TyCoRep.TCvSubst = Core.Mk_TCvSubst
rename value CoreSyn.Type_ = Core.Mk_Type
rename value CoreSyn.Coercion = Core.Mk_Coercion
## Other punning
rename value CoreFVs.FVAnn = CoreFVs.Mk_FVAnn
rename value CoreSubst.Subst = CoreSubst.Mk_Subst
###############################################################################
# General edits related to translating Core
###############################################################################
## Outputtable
rewrite forall x, Core.pprIdDetails x = Panic.someSDoc
rename type GHC.Stack.Types.HasCallStack = Util.HasDebugCallStack
###############################################################################
# Pruning the AST, general
###############################################################################
#
# we never use any operations on these types, so perfectly sound to forget
# they exist. Could also axiomatize, but then would need to add Default/Eq
# instances for them too.
#
rename type PrimOp.PrimOp = AxiomatizedTypes.PrimOp
rename type ForeignCall.ForeignCall = AxiomatizedTypes.ForeignCall
rename type ForeignCall.CType = AxiomatizedTypes.CType
rename type CostCentre.CostCentre = AxiomatizedTypes.CostCentre
# used in DataCon
rename type MkId.DataConBoxer = AxiomatizedTypes.DataConBoxer
###############################################################################
# Skipping constructors
###############################################################################
#
# data Unfolding
# = NoUnfolding -- ^ We have no information about the unfolding.
#
skip constructor Core.BootUnfolding
skip constructor Core.OtherCon
skip constructor Core.DFunUnfolding
skip constructor Core.CoreUnfolding
#
# eliminating parts of the 'Expr' and 'AnnExpr' type
#
skip constructor Core.Tick
skip constructor Core.AnnTick
#
# eliminating TcTy variables and Type variables from 'Var'
#
skip constructor Core.TcTyVar
skip constructor Core.TyVar
# eliminating coercion variables from 'IdDetails'
# (there are other unimportant IdDetails, but this one controls
# the operations 'isCoVar` and `isNonCoVarId`)
skip constructor Core.CoVarId
###############################################################################
# axiomatize type & coercion information
# - define types in a new (manual) module called AxiomatizedTypes
# it helps to be able to refer to these types *before* Core is defined
# - rewrite refererences to these types to new module
###############################################################################
#
# axiomatized types
#
rename type TyCoRep.Coercion = AxiomatizedTypes.Coercion
rename type TyCoRep.Type_ = AxiomatizedTypes.Type_
rename type TyCoRep.ThetaType = AxiomatizedTypes.ThetaType
rename type TyCoRep.TyBinder = AxiomatizedTypes.TyBinder
rename type TyCoRep.TyThing = AxiomatizedTypes.TyThing
rename type TyCoRep.Kind = AxiomatizedTypes.Kind
rename type TyCoRep.PredType = AxiomatizedTypes.PredType
rename type CoAxiom.CoAxiom = AxiomatizedTypes.CoAxiom
rename type CoAxiom.BranchFlag = AxiomatizedTypes.BranchFlag
rename type CoAxiom.Branched = AxiomatizedTypes.Branched
rename type CoAxiom.Unbranched = AxiomatizedTypes.Unbranched
rename type CoAxiom.BuiltInSynFamily = AxiomatizedTypes.BuiltInSynFamily
rename type CoAxiom.Role = AxiomatizedTypes.Role
rename type CoAxiom.BranchIndex = AxiomatizedTypes.BranchIndex
rename type CoAxiom.CoAxiomRule = AxiomatizedTypes.CoAxiomRule
rename type CoAxiom.CoAxBranch = AxiomatizedTypes.CoAxBranch
rename value CoAxiom.Representational = AxiomatizedTypes.Representational
rename value CoAxiom.Nominal = AxiomatizedTypes.Nominal
rename value CoAxiom.Phantom = AxiomatizedTypes.Phantom
#
# not translating TcType or TysWiredIn yet
#
# these can be added as Axioms to Core, but
# for some reason, adding these as Axioms double adds them.
# add Core Axiom Core.TcTyVarDetails : Type.
rename type TcType.TcTyVarDetails = AxiomatizedTypes.TcTyVarDetails
# add Core Axiom Core.liftedTypeKind : AxiomatizedTypes.Kind.
rename value TysWiredIn.liftedTypeKind = AxiomatizedTypes.liftedTypeKind
# add Core Axiom Core.constraintKind : AxiomatizedTypes.Kind.
rename value TysWiredIn.constraintKind = AxiomatizedTypes.constraintKind
###############################################################################
# rewrites for type/corecion related operations defined in skipped modules
##############################################################################
# DataCon
# This relies on Unify.typesCantMatch as well as several operations from Type
axiomatize definition Core.dataConCannotMatch
############################################################################
# rewrites for type/corecion related operations defined in translated modules
############################################################################
#
# (these operations were in TyCoRep)
#
rewrite forall co, Core.tyCoFVsOfCo co = FV.emptyFV
rewrite forall ty, Core.tyCoFVsOfType ty = FV.emptyFV
rewrite forall ty, Core.tyCoVarsOfTypeDSet ty = Core.emptyDVarSet
rewrite forall co, Core.tyCoVarsOfCoDSet co = Core.emptyDVarSet
in CoreSubst.substBndr rewrite forall x, Core.noFreeVarsOfType x = true
in CoreSubst.substIdBndr rewrite forall x, Core.noFreeVarsOfType x = true
# don't need substCoVarBndr and substTyVarBndr
in CoreSubst.substBndr rewrite forall bndr, Core.isTyVar bndr = false
in CoreSubst.substBndr rewrite forall bndr, Core.isCoVar bndr = false
#
# We need to avoid creating new Coercions and Types with mkTyVarTy and mkCoVarCo
#
in Core.varToCoreExpr rewrite forall v, Core.isCoVar v = false
in Core.varToCoreExpr rewrite forall v, Core.isTyVar v = false
in Core.varToCoreExpr rewrite forall bndr, Core.isId v = true
in CoreSubst.extendSubstWithVar rewrite forall v2, andb Util.debugIsOn (negb (Core.isTyVar v2)) = false
in CoreSubst.extendSubstWithVar rewrite forall v1, (Core.isTyVar v1) = false
in CoreSubst.extendSubstWithVar rewrite forall v2, andb Util.debugIsOn (negb (Core.isCoVar v2)) = false
in CoreSubst.extendSubstWithVar rewrite forall v1, (Core.isCoVar v1) = false
in CoreSubst.clone_id rewrite forall old_id, Core.isCoVar old_id = false
#######
# we cannot verify these assertions as we aren't tracking whether types are
# coercion types are not. But they are debug assertions!
#
in Id.mkSysLocal rewrite forall ty, (Core.isCoercionType ty) = false
in Id.mkUserLocal rewrite forall ty, (Core.isCoercionType ty) = false
# these two use the type information to determine whether to make a type
# or a coercion variable
#
in Id.mkLocalIdOrCoVarWithInfo rewrite forall ty, (Core.isCoercionType ty) = false
in Id.mkLocalIdOrCoVar rewrite forall ty, Core.isCoercionType ty = false
############################################################################
# pruning ticks
############################################################################
in CoreFVs.expr_fvs rewrite forall t, CoreFVs.tickish_fvs t = FV.emptyFV
# remove reasoning about ticks
#
rewrite forall xs e, CoreUtils.stripTicksE xs e = e
rewrite forall xs e, CoreUtils.stripTicksT xs e = e
rewrite forall ts e, CoreUtils.mkTicks ts e = e
############################################################################
# pruning Rules
############################################################################
# Redefine RuleInfo so that it is always empty. This is *safe*
# these redefines are for definitions in IdInfo
redefine Inductive Core.RuleInfo : Type := Core.EmptyRuleInfo.
redefine Definition Core.emptyRuleInfo := Core.EmptyRuleInfo.
redefine Definition Core.isEmptyRuleInfo : Core.RuleInfo -> bool
:= fun x => true.
redefine Definition Core.ruleInfoFreeVars : Core.RuleInfo -> Core.DVarSet
:= fun x => Core.emptyDVarSet.
redefine Definition Core.ruleInfoRules : Core.RuleInfo -> list Core.CoreRule
:= fun x => nil.
redefine Definition Core.setRuleInfoHead : Name.Name -> (Core.RuleInfo -> Core.RuleInfo)
:= fun x y => Core.EmptyRuleInfo.
redefine Definition CoreFVs.idRuleFVs : Core.Id -> FV.FV := fun id => FV.emptyFV.
redefine Definition Id.idCoreRules : Core.Id -> list (Core.CoreRule)
:= fun x => nil.