forked from plclub/hs-to-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathno-type-edits
233 lines (186 loc) · 8.5 KB
/
no-type-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
skip module TyCoRep
skip module Coercion
skip module CoAxiom
skip module Type
skip module Unify
skip module TcType
#skip module TysWiredIn
skip module RepType
skip module ForeignCall
skip module FamInstEnv
skip module PprCore
skip module Data.ByteString
skip module ErrUtils
skip module OccurAnal
skip module CostCentre
skip module PrimOp
skip module TysPrim
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
####################################################
## Glueing together the Core
####################################################
#
# This must stay in sync with the Makefile
#
rename module Class Core
rename module TyCon Core
rename module DataCon Core
rename module Var Core
rename module IdInfo Core
rename module PatSyn Core
rename module VarSet Core
rename module VarEnv Core
rename module CoreSyn Core
rename module Demand Core
#
# 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
## 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
## CallStack
rewrite forall x, Core.idInfo x = @Core.idInfo tt x
###############################################################################
# Pruning the AST, general
###############################################################################
rename type PrimOp.PrimOp = unit
rename type ForeignCall.ForeignCall = unit
rename type ForeignCall.CType = unit
rename type CostCentre.CostCentre = unit
# used in DataCon
rename type MkId.DataConBoxer = unit
###############################################################################
# brutaly skip all type info
###############################################################################
rename type TcType.TcTyVarDetails = unit
rename type TyCoRep.Coercion = unit
rename type TyCoRep.Type_ = unit
rename type TyCoRep.ThetaType = unit
rename type TyCoRep.TyBinder = unit
rename type TyCoRep.TyThing = unit
rename type TyCoRep.Kind = unit
rename type TyCoRep.PredType = unit
rename type TyCoRep.TvSubstEnv = unit
rename type TyCoRep.CvSubstEnv = unit
rename type TyCoRep.TCvSubst = unit
rename type CoAxiom.CoAxiom = list
rename type CoAxiom.Branched = unit
rename type CoAxiom.Unbranched = unit
rename type CoAxiom.BuiltInSynFamily = unit
rename type CoAxiom.Role = unit
rename value CoAxiom.Representational = tt
rename value CoAxiom.Nominal = tt
rename value TysWiredIn.liftedTypeKind = tt
rename value TysWiredIn.constraintKind = tt
###############################################################################
# rewrites for type/corecion related operations defined in skipped modules
##############################################################################
# maybe some of these should be axioms instead of rewrites so that we have
# to consider each case.
rewrite forall v, Coercion.mkCoVarCo v = tt
rewrite forall co, Coercion.coercionType co = tt
rewrite forall x, TyCoRep.mkTyVarTy x = tt
rewrite forall env x, TyCoRep.tidyType env x = tt
rewrite forall env co, TyCoRep.tidyCo env co = tt
rewrite forall co, TyCoRep.tyCoFVsOfCo co = FV.emptyFV
rewrite forall ty, TyCoRep.tyCoFVsOfType ty = FV.emptyFV
rewrite forall b_ty, TyCoRep.tyCoVarsOfTypeDSet b_ty = Core.emptyDVarSet
rewrite forall co, TyCoRep.tyCoVarsOfCoDSet co = Core.emptyDVarSet
rewrite forall s knd, TyCoRep.substTyUnchecked s knd = tt
rewrite forall s t n, TyCoRep.extendTvSubstWithClone s t n = s
rewrite forall s ty, TyCoRep.substTy s ty = tt
rewrite forall x, TyCoRep.noFreeVarsOfType x = true
rewrite forall x y, TyCoRep.zipTvSubst x y = tt
rewrite forall x, Type.caseBinder x = x
rewrite forall ty, Type.typeKind ty = tt
rewrite forall x, Type.mkInvForAllTys x y = tt
rewrite forall x, Type.getRuntimeRep x = tt
rewrite forall x y, Type.piResultTy x y = tt
rewrite forall x, Type.splitFunTy x = (pair tt tt)
rewrite forall ids, Type.toposortTyVars ids = ids
rewrite forall f, (f GHC.Base.∘ Type.getRuntimeRep) = f
# axiomatize functions that return bool or option
#
# these functions are not defined in any of the modules that we are translating
# but we need them so we move them to Core as we axiomatize their results.
#
rename value TyCoRep.isCoercionType = Core.isCoercionType
add Core Axiom Core.isCoercionType : unit -> bool.
rename value Type.isFunTy = Core.isFunTy
add Core Axiom Core.isFunTy : unit -> bool.
rename value Type.isUnliftedType = Core.isUnliftedType
add Core Axiom Core.isUnliftedType : unit -> bool.
rename value Type.isTypeLevPoly = Core.isTypeLevPoly
add Core Axiom Core.isTypeLevPoly : unit -> bool.
rename value Type.resultIsLevPoly = Core.resultIsLevPoly
add Core Axiom Core.resultIsLevPoly : unit -> bool.
rename value Type.splitPiTy_maybe = Core.splitPiTy_maybe
add Core Axiom Core.splitPiTy_maybe : unit -> option (unit * unit).
rename value Type.isCoercionTy_maybe = Core.isCoercionTy_maybe
add Core Axiom Core.isCoercionTy_maybe : unit -> option unit.
rename value Coercion.eqCoercionX = Core.eqCoercionX
add Core Axiom Core.eqCoercionX : RnEnv2 -> (unit -> (unit -> bool)).
rename value Type.eqTypeX = Core.eqTypeX
add Core Axiom Core.eqTypeX : RnEnv2 -> (unit -> (unit -> bool)).
rename value Type.eqType = Core.eqType
add Core Axiom Core.eqType : (unit -> (unit -> bool)).
rename value TyCoRep.tidyTyCoVarBndr = Core.tidyTyCoVarBndr
add Core Axiom Core.tidyTyCoVarBndr : TidyEnv -> (TyCoVar -> (TidyEnv * TyCoVar)).
# Var
axiomatize definition Core.isTyCoVar
# DataCon
axiomatize definition Core.dataConCannotMatch
############################################################################
# rewrites for type/corecion related operations defined in translated modules
############################################################################
# TODO: translate PrelNames
rewrite forall id, (Unique.hasKey id PrelNames.absentErrorIdKey) = false
rewrite forall x, Core.sel_tycon x = tt
rewrite forall x y, Core.mkTyConKind x y = tt
rewrite forall e t1 t2, Core.rnBndrs2 e t1 t2 = env
rewrite forall rhs, CoreUtils.exprType rhs = tt
rewrite forall con, DataCon.dataConRepStrictness con = nil
rewrite forall con, DataCon.dataConRepArgTys con = nil
rewrite forall con, DataCon.dataConExTyVars con = @nil unit
rewrite forall x, Literal.literalType x = tt
rewrite forall x, Id.idType x = tt
rewrite forall x t, Id.setIdType x t = x
rewrite forall ty, CoreFVs.orphNamesOfType ty = NameSet.emptyNameSet
rewrite forall co, CoreFVs.orphNamesOfCo co = NameSet.emptyNameSet
rewrite forall id, CoreFVs.bndrRuleAndUnfoldingFVs id = FV.emptyFV
redefine Definition CoreFVs.idRuleFVs : Core.Id -> FV.FV := fun id => FV.emptyFV.
redefine Definition CoreFVs.varTypeTyCoFVs : Core.Var -> FV.FV := fun var => FV.emptyFV.
redefine Definition CoreFVs.idUnfoldingFVs : Core.Id -> FV.FV := fun id => FV.emptyFV.
rewrite forall x y, TyCon.mkTyConKind x y = tt
# could make this unit too
axiomatize definition TyCon.RuntimeRepInfo