forked from antalsz/hs-to-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathedits
149 lines (122 loc) · 5.59 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
skip module GHC.Arr
skip module GHC.Generics
skip module GHC.Types
skip module GHC.CString
skip module GHC.Classes
skip module GHC.Magic
skip module GHC.IO
skip module GHC.Integer
skip module GHC.Unicode
skip module GHC.Show
skip module Data.Data
## Not yet translated or manually implemented
skip module GHC.Int
skip module GHC.Word
skip module GHC.Integer.Type
rename type GHC.IO.FilePath = GHC.Base.String
# Work around the fact that build is higher rank, so the generator
# expects a non-implicit type argument.
rewrite forall g, (GHC.Base.build g) = GHC.Base.build' (fun _ => g)
# Much prettier
rewrite forall f x, (f GHC.Base.$ x) = f x
rewrite forall f x, (f GHC.Base.$! x) = f x
rename type GHC.Tuple.() = unit
rename value GHC.Tuple.() = tt
rename type GHC.Tuple.(,) = GHC.Tuple.pair_type
rename type GHC.Tuple.(,,) = GHC.Tuple.triple_type
rename type GHC.Tuple.(,,,) = GHC.Tuple.quad_type
rename type GHC.Tuple.(,,,,) = GHC.Tuple.quint_type
rename type GHC.Tuple.(,,,,,) = GHC.Tuple.sext_type
rename type GHC.Tuple.(,,,,,,) = GHC.Tuple.sept_type
rename value GHC.Tuple.(,) = GHC.Tuple.pair2
rename value GHC.Tuple.(,,) = GHC.Tuple.pair3
rename value GHC.Tuple.(,,,) = GHC.Tuple.pair4
rename value GHC.Tuple.(,,,,) = GHC.Tuple.pair5
rename value GHC.Tuple.(,,,,,) = GHC.Tuple.pair6
rename value GHC.Tuple.(,,,,,,) = GHC.Tuple.pair7
rename type GHC.Types.[] = list
rename value GHC.Types.[] = nil
rename value GHC.Types.: = cons
rename value GHC.Base.++ = Coq.Init.Datatypes.app
rename value GHC.List.concatMap = Coq.Lists.List.flat_map
rename value GHC.List.foldl = GHC.Base.foldl
rename value GHC.List.foldl' = GHC.Base.foldl'
# rename value GHC.Magic.oneShot = GHC.Base.oneShot
rewrite forall x, GHC.Magic.lazy x = x
rewrite forall x, GHC.Magic.oneShot x = x
rename type GHC.Types.Ordering = comparison
rename value GHC.Types.EQ = Eq
rename value GHC.Types.LT = Lt
rename value GHC.Types.GT = Gt
rename type GHC.Types.* = Type
rename type GHC.Types.Word = GHC.Num.Word
rename type GHC.Types.Int = GHC.Num.Int
rename type GHC.Types.Char = GHC.Char.Char
rename type GHC.Types.Coercible = GHC.Prim.Coercible
rename type GHC.Classes.Eq = GHC.Base.Eq_
rename value GHC.Classes.== = GHC.Base.op_zeze__
rename value GHC.Classes./= = GHC.Base.op_zsze__
rename type GHC.Classes.Ord = GHC.Base.Ord
rename value GHC.Classes.< = GHC.Base.<
rename value GHC.Classes.<= = GHC.Base.<=
rename value GHC.Classes.> = GHC.Base.>
rename value GHC.Classes.>= = GHC.Base.>=
rename value GHC.Classes.max = GHC.Base.max
rename value GHC.Classes.min = GHC.Base.min
rename value GHC.Classes.compare = GHC.Base.compare
rename type GHC.Types.Bool = bool
rename value GHC.Types.True = true
rename value GHC.Types.False = false
rename value GHC.Classes.not = negb
rename value GHC.Classes.|| = orb
rename value GHC.Classes.&& = andb
rename type GHC.Base.Maybe = option
rename value GHC.Base.Just = Some
rename value GHC.Base.Nothing = None
# rename value GHC.Err.errorWithoutStackTrace = GHC.Base.errorWithoutStackTrace
skip method GHC.Base.Monad fail
skip method GHC.Enum.Enum enumFromThen
skip method GHC.Enum.Enum enumFromThenTo
skip method Data.Semigroup.Semigroup stimes
skip method Data.Semigroup.Semigroup sconcat
# deprecated
skip method Data.Bits.Bits bitSize
# default definition cannot be used
skip method GHC.Base.Applicative op_zlzt__
# partial methods
skip method Data.Foldable.Foldable foldl1
skip method Data.Foldable.Foldable foldr1
skip method Data.Foldable.Foldable maximum
skip method Data.Foldable.Foldable minimum
# We do not create notation for constructors yet
# (but it would not be hard)
rename value Data.List.NonEmpty.:| = Data.List.NonEmpty.NEcons
# Punned constructors
rename value Control.Arrow.ArrowMonad = Control.Arrow.Mk_ArrowMonad
rename value Control.Arrow.Kleisli = Control.Arrow.Mk_Kleisli
rename value Data.Foldable.Max = Data.Foldable.Mk_Max
rename value Data.Foldable.Min = Data.Foldable.Mk_Min
rename value Data.Functor.Const.Const = Data.Functor.Const.Mk_Const
rename value Data.Functor.Identity.Identity = Data.Functor.Identity.Mk_Identity
rename value Data.Monoid.All = Data.Monoid.Mk_All
rename value Data.Monoid.Alt = Data.Monoid.Mk_Alt
rename value Data.Monoid.Any = Data.Monoid.Mk_Any
rename value Data.Monoid.Dual = Data.Monoid.Mk_Dual
rename value Data.Monoid.Endo = Data.Monoid.Mk_Endo
rename value Data.Monoid.First = Data.Monoid.Mk_First
rename value Data.Monoid.Last = Data.Monoid.Mk_Last
rename value Data.Monoid.Product = Data.Monoid.Mk_Product
rename value Data.Monoid.Sum = Data.Monoid.Mk_Sum
rename value Data.OldList.SnocBuilder = Data.OldList.Mk_SnocBuilder
rename value Data.Ord.Down = Data.Ord.Mk_Down
rename value Data.Proxy.KProxy = Data.Proxy.Mk_KProxy
rename value Data.Proxy.Proxy = Data.Proxy.Mk_Proxy
rename value Data.Semigroup.Arg = Data.Semigroup.Mk_Arg
rename value Data.Semigroup.First = Data.Semigroup.Mk_First
rename value Data.Semigroup.Last = Data.Semigroup.Mk_Last
rename value Data.Semigroup.Max = Data.Semigroup.Mk_Max
rename value Data.Semigroup.Min = Data.Semigroup.Mk_Min
rename value Data.Semigroup.Option = Data.Semigroup.Mk_Option
rename value Data.Traversable.Id = Data.Traversable.Mk_Id
rename value Data.Traversable.StateL = Data.Traversable.Mk_StateL
rename value Data.Traversable.StateR = Data.Traversable.Mk_StateR