Skip to content

Commit f1eed9c

Browse files
UARTmanUARTman
committed
[refactor, new] Add first test for specialiseIfNeeded
1 parent ff22fcb commit f1eed9c

19 files changed

Lines changed: 334 additions & 122 deletions

File tree

‎elab-util-extra/src/Deriving/SpecialiseData.idr‎

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,33 @@
11
module Deriving.SpecialiseData
22

33
import Control.Monad.Either
4-
import Control.Monad.Error.Either
5-
import Control.Monad.Error.Interface
6-
import Control.Monad.Reader.Tuple
74
import Control.Monad.Trans
8-
import Data.SnocList
95
import Data.DPair
10-
import Data.List1
11-
import Data.Vect
12-
import Data.Vect.Quantifiers
6+
import Data.Either
7+
import Data.Fin.Set
138
import Data.List
9+
import public Data.List.Map -- workaround for compiler bug
1410
import Data.List.Quantifiers
15-
import Data.Either
11+
import Data.List1
12+
import Data.Maybe
13+
import Data.SnocList
1614
import Data.SortedMap
17-
import Data.SortedSet
1815
import Data.SortedMap.Dependent
19-
import Decidable.Equality
16+
import Data.SortedSet
17+
import Data.Vect
18+
import Data.Vect.Quantifiers
19+
import public Decidable.Decidable
20+
import public Decidable.Equality
2021
import Deriving.Show
2122
import public Language.Mk
2223
import Language.Reflection.Compat
2324
import Language.Reflection.Compat.Constr
24-
import Language.Reflection.Compat.TypeInfo
25+
import public Language.Reflection.Compat.TypeInfo -- workaround for compiler bug
2526
import Language.Reflection.Expr
27+
import Language.Reflection.Syntax
2628
import Language.Reflection.Logging
27-
import Language.Reflection.Unify
28-
import Language.Reflection.VarSubst
29+
import public Language.Reflection.Unify.Interface
30+
import public Language.Reflection.VarSubst -- workaround for compiler bug
2931
import Syntax.IHateParens
3032

3133
%language ElabReflection
@@ -331,7 +333,7 @@ getTask resultName resultKind resultContent = do
331333
, ttArgs
332334
, ttArgsNamed
333335
, currentNs
334-
, resultName
336+
, resultName = snd $ unNS resultName
335337
, fullInvocation = tqRet --- TODO: intelligent full invocation
336338
, polyTy
337339
, polyTyNamed

‎elab-util-extra/src/Language/Reflection/Compat.idr‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ import public Data.List1
1010
import public Data.String
1111
import public Data.Vect
1212

13+
import public Deriving.Show
14+
1315
import public Language.Reflection
1416
import Language.Reflection.Expr
1517
import Language.Reflection.Logging
@@ -18,6 +20,8 @@ import public Language.Reflection.Syntax.Ops
1820

1921
%default total
2022

23+
%language ElabReflection
24+
2125
--------------------------------------------------------------------------------
2226
-- General Types
2327
--------------------------------------------------------------------------------
@@ -30,6 +34,34 @@ record Con where
3034
args : List Arg
3135
type : TTImp
3236

37+
countShow : Show Count
38+
countShow = %runElab derive
39+
40+
export
41+
Show Count where
42+
show = show @{countShow}
43+
44+
piInfoShow : Show a => Show (PiInfo a)
45+
piInfoShow = %runElab derive
46+
47+
export
48+
Show a => Show (PiInfo a) where
49+
show = show @{piInfoShow}
50+
51+
argShow : Show Arg
52+
argShow = %runElab derive
53+
54+
export
55+
Show Arg where
56+
show = show @{argShow}
57+
58+
conShow : Show Con
59+
conShow = %runElab derive
60+
61+
export
62+
Show Con where
63+
show = show @{conShow}
64+
3365
||| Tries to lookup a constructor by name.
3466
export
3567
getCon : Elaboration m => Name -> m Con
@@ -62,6 +94,13 @@ export
6294
LogPosition TypeInfo where
6395
logPosition = show . name
6496

97+
tiShow : Show TypeInfo
98+
tiShow = %runElab derive
99+
100+
export
101+
Show TypeInfo where
102+
show = show @{tiShow}
103+
65104
||| Tries to get information about the data type specified
66105
||| by name. The name need not be fully qualified, but
67106
||| needs to be unambiguous.

‎elab-util-extra/src/Language/Reflection/Compat/TypeInfo.idr‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,7 @@ export
134134
[TypeInfoOrdByName] Ord TypeInfo using TypeInfoEqByName where
135135
compare = comparing name
136136

137+
export
137138
Semigroup NamesInfoInTypes where
138139
Names ts cs nit <+> Names ts' cs' nit' = Names (ts `mergeLeft` ts') (cs `mergeLeft` cs') (nit <+> nit')
139140

‎elab-util-extra/src/Language/Reflection/Unify/Interface.idr‎

Lines changed: 76 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,11 @@ import Data.Either
55
import Data.Fin.Set
66
import Data.SortedMap
77
import Data.Vect
8+
import Data.Vect.Quantifiers
89
import Decidable.Equality
9-
import Derive.Prelude
10+
import Deriving.Show
1011
import Language.Reflection
1112
import Language.Reflection.Expr
12-
import Language.Reflection.TTImp
13-
import Language.Reflection.TT
1413
import Language.Reflection.Syntax
1514

1615
%language ElabReflection
@@ -38,9 +37,24 @@ record UnificationTask where
3837

3938
%name UnificationTask task
4039

41-
%runElab derive "Count" [Show]
42-
%runElab derive "PiInfo" [Show]
43-
%runElab derive "Syntax.Arg" [Show]
40+
sCount : Show Count
41+
sCount = %runElab derive
42+
43+
Show Count where
44+
show = show @{sCount}
45+
46+
sPiInfo : Show a => Show (PiInfo a)
47+
sPiInfo = %runElab derive
48+
49+
Show a => Show (PiInfo a) where
50+
show = show @{sPiInfo}
51+
52+
sArg : Show Arg
53+
sArg = %runElab derive
54+
55+
Show Arg where
56+
show = show @{sArg}
57+
4458

4559
export
4660
Show UnificationTask where
@@ -74,7 +88,17 @@ record FVData where
7488

7589
%name FVData fv, fvData
7690

77-
%runElab derive "FVData" [Show, Eq]
91+
sFVData : Show FVData
92+
sFVData = %runElab derive
93+
94+
export
95+
Show FVData where
96+
show = show @{sFVData}
97+
98+
export
99+
Eq FVData where
100+
(MkFVData name holeName rig piInfo type value) == (MkFVData name' holeName' rig' piInfo' type' value') =
101+
name == name' && holeName == holeName' && rig == rig' && piInfo == piInfo' && type == type' && value == value'
78102

79103
export
80104
Interpolation FVData where
@@ -137,7 +161,18 @@ record DependencyGraph where
137161

138162
%name DependencyGraph dg, depGraph
139163

140-
%runElab derive "DependencyGraph" [Show]
164+
export
165+
Show DependencyGraph where
166+
showPrec p t =
167+
showCon p "MkDG" $
168+
joinBy "" $
169+
[ showArg t.freeVars
170+
, showArg t.fvData
171+
, showArg t.fvDeps
172+
, showArg t.empties
173+
, showArg t.nameToId
174+
, showArg t.holeToId
175+
]
141176

142177
export
143178
Eq DependencyGraph where
@@ -164,7 +199,18 @@ record UnificationResult where
164199
||| (specialised constructor arguments)
165200
order : List $ Fin uniDg.freeVars
166201

167-
%runElab derive "UnificationResult" [Show]
202+
export
203+
Show UnificationResult where
204+
showPrec p t =
205+
showCon p "MkUR" $
206+
joinBy "" $
207+
[ showArg t.task
208+
, showArg t.uniDg
209+
, showArg t.lhsResult
210+
, showArg t.rhsResult
211+
, showArg t.fullResult
212+
, showArg t.order
213+
]
168214

169215
public export
170216
data UnificationError : Type where
@@ -174,15 +220,34 @@ data UnificationError : Type where
174220
ExtractionError : TTImp -> UnificationError
175221
NoUnificationError : UnificationError
176222

177-
%runElab derive "UnificationError" [Show, Eq]
223+
sUE : Show UnificationError
224+
sUE = %runElab derive
225+
226+
export
227+
Show UnificationError where
228+
show = show @{sUE}
229+
230+
export
231+
Eq UnificationError where
232+
CatastrophicError == CatastrophicError = True
233+
InternalError s == InternalError s' = s == s'
234+
TargetTypeError t == TargetTypeError t' = t == t'
235+
ExtractionError t == ExtractionError t' = t == t'
236+
NoUnificationError == NoUnificationError = True
237+
_ == _ = False
178238

179239
public export
180240
data UnificationVerdict : Type where
181241
Success : UnificationResult -> UnificationVerdict
182242
Undecided : UnificationVerdict
183243
Fail : UnificationError -> UnificationVerdict
184244

185-
%runElab derive "UnificationVerdict" [Show]
245+
sUV : Show UnificationVerdict
246+
sUV = %runElab derive
247+
248+
export
249+
Show UnificationVerdict where
250+
show = show @{sUV}
186251

187252
export %inline
188253
isSuccess : UnificationVerdict -> Bool

‎elab-util-extra/src/Language/Reflection/Unify/WithCompiler.idr‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
module Language.Reflection.Unify.WithCompiler
22

3-
import Control.Monad.Either
4-
import Control.Monad.Writer
5-
import Control.Monad.Identity
3+
import public Control.Monad.Either -- workaround for compiler bug
4+
import public Control.Monad.Writer -- workaround for compiler bug
5+
import public Control.Monad.Identity -- workaround for compiler bug
66
import Data.DPair
77
import Data.Fin.Set
88
import Data.Vect
9-
import Data.Vect.Quantifiers
10-
import Data.SnocVect
9+
import public Data.Vect.Quantifiers -- workaround for compiler bug
10+
import public Data.SnocVect -- workaround for compiler bug
1111
import Data.SortedMap
12-
import Decidable.Equality
12+
import public Decidable.Equality -- workaround for compiler bug
1313
import Language.Reflection
14-
import Language.Reflection.Expr
15-
import Language.Reflection.Logging
14+
import public Language.Reflection.Expr -- workaround for compiler bug
15+
import public Language.Reflection.Logging -- workaround for compiler bug
1616
import Language.Reflection.Syntax
17-
import Language.Reflection.Unify.Interface
17+
import public Language.Reflection.Unify.Interface
1818
import Language.Reflection.VarSubst
1919

2020
%default total

‎elab-util-extra/src/Language/Reflection/VarSubst.idr‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ import Language.Reflection.TTImp
88
import Language.Reflection.TT
99
import Language.Reflection.Util
1010
import Control.Monad.Identity
11-
import Control.Monad.Reader
12-
import Control.Monad.Reader.Tuple
11+
import public Control.Monad.Reader -- workaround for compiler bug
12+
import public Control.Monad.Reader.Tuple -- workaround for compiler bug
1313
import Control.Monad.State
1414

1515
%default total

‎elab-util-extra/tests/specialise-data/_shared/Shared.idr‎

Lines changed: 0 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,7 @@
11
module Shared
22

3-
import public Control.Monad.Either
4-
import public Control.Monad.Error.Either
5-
import public Control.Monad.Error.Interface
6-
import public Control.Monad.Writer
7-
import public Control.Monad.Identity
8-
import public Control.Monad.Trans
9-
import public Control.Monad.Reader.Reader
10-
import public Control.Monad.Reader.Interface
11-
import public Control.Monad.Reader.Tuple
12-
import public Control.Monad.State
13-
import public Data.DPair
14-
import public Data.Either
15-
import public Data.List
16-
import public Data.List.Map
17-
import public Data.List.Quantifiers
18-
import public Data.Maybe
19-
import public Data.SnocVect
20-
import public Data.SortedSet
21-
import public Data.SortedMap.Dependent
22-
import public Data.Vect
23-
import public Data.Vect.Quantifiers
24-
import public Decidable.Decidable
25-
import public Decidable.Equality
26-
import public Derive.Prelude
273
import public Deriving.SpecialiseData
28-
import public Language.Mk
29-
import public Language.Reflection
30-
import public Language.Reflection.Compat
31-
import public Language.Reflection.Compat.Constr
32-
import public Language.Reflection.Compat.TypeInfo
33-
import public Language.Reflection.Derive
34-
import public Language.Reflection.Expr
35-
import public Language.Reflection.Logging
36-
import public Language.Reflection.Syntax
37-
import public Language.Reflection.Syntax.Ops
38-
import public Language.Reflection.TTImp
39-
import public Language.Reflection.TT
40-
import public Language.Reflection.Types
414
import public Language.Reflection.Unify
42-
import public Language.Reflection.VarSubst
435

446
||| Verify that all values in list check to a given type
457
constructExprs : Type -> List TTImp -> Elab ()

‎elab-util-extra/tests/unify-with-compiler/_shared/Shared.idr‎

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,5 @@
11
module Shared
22

3-
import public Control.Monad.Either
4-
import public Control.Monad.Writer
5-
import public Control.Monad.Identity
6-
import public Decidable.Equality
7-
import public Data.DPair
8-
import public Data.Vect
9-
import public Data.SnocVect
10-
import public Data.Vect.Quantifiers
11-
import public Derive.Prelude
12-
import public Language.Reflection
13-
import public Language.Reflection.Derive
14-
import public Language.Reflection.Expr
15-
import public Language.Reflection.Logging
16-
import public Language.Reflection.Syntax
173
import public Language.Reflection.Unify
184

195
public export

0 commit comments

Comments
 (0)