Skip to content

Commit 3f3129c

Browse files
UARTmanUARTman
committed
[ fix ] Use local names in derived specialised types
1 parent 96b657c commit 3f3129c

6 files changed

Lines changed: 19 additions & 12 deletions

File tree

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,8 @@ interface NamespaceProvider (0 m : Type -> Type) where
114114
constructor MkNSProvider
115115
provideNS : m Namespace
116116

117-
export %defaulthint
117+
export
118+
-- %defaulthint
118119
CurrentNS : Elaboration m => NamespaceProvider m
119120
CurrentNS = MkNSProvider $ do
120121
NS nsn _ <- inCurrentNS ""
@@ -129,6 +130,11 @@ export
129130
inNS : Monad m => Namespace -> NamespaceProvider m
130131
inNS ns = MkNSProvider $ pure ns
131132

133+
export
134+
%defaulthint
135+
NoNS : Monad m => NamespaceProvider m
136+
NoNS = inNS (MkNS [])
137+
132138
||| Prepend namespace into which everything is generated to name
133139
inGenNS : SpecTask -> Name -> Name
134140
inGenNS task n = do

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,9 @@ typeCon ti = MkCon ti.name ti.args type
2424
export
2525
(.decl) : TypeInfo -> Decl
2626
(.decl) ti =
27-
iData Public ti.name tySig [] conITys
27+
iData Public tyName tySig [] conITys
2828
where
29+
tyName = snd $ unNS ti.name
2930
tySig = piAll type ti.args
3031
conITys = (.iTy) <$> ti.cons
3132

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-001/expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,5 @@ LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] NormaliseTask ret
66
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] lambdaBody = \ lam^0 => Data.Vect.Vect lam^0 Prelude.Types.Nat;
77
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Specialised type name: Vect^17613086623960416996
88
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Specialised type not found, deriving...
9-
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Found or derived Test.Vect^17613086623960416996.Vect^17613086623960416996
10-
LOG deptycheck.test.utils.specialise:0: Test.Vect^17613086623960416996.Vect^17613086623960416996[] CallGen params: []
9+
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Found or derived Vect^17613086623960416996.Vect^17613086623960416996
10+
LOG deptycheck.test.utils.specialise:0: Vect^17613086623960416996.Vect^17613086623960416996[] CallGen params: []

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-002/expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,5 @@ LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] NormaliseTask returned: l
66
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] lambdaBody = \ lam^0 => Test.X Prelude.Types.Nat lam^0;
77
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^15319567236415762791
88
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type not found, deriving...
9-
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Found or derived Test.X^15319567236415762791.X^15319567236415762791
10-
LOG deptycheck.test.utils.specialise:0: Test.X^15319567236415762791.X^15319567236415762791[0(fv^lam^0)] CallGen params: [Prelude.Types.S]
9+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Found or derived X^15319567236415762791.X^15319567236415762791
10+
LOG deptycheck.test.utils.specialise:0: X^15319567236415762791.X^15319567236415762791[0(fv^lam^0)] CallGen params: [Prelude.Types.S]

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-003/expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,5 @@ LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] NormaliseTask returned: l
66
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] lambdaBody = Test.X Prelude.Types.Nat Data.Fin.Fin;
77
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^16134534282501286198
88
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type not found, deriving...
9-
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Found or derived Test.X^16134534282501286198.X^16134534282501286198
10-
LOG deptycheck.test.utils.specialise:0: Test.X^16134534282501286198.X^16134534282501286198[] CallGen params: []
9+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Found or derived X^16134534282501286198.X^16134534282501286198
10+
LOG deptycheck.test.utils.specialise:0: X^16134534282501286198.X^16134534282501286198[] CallGen params: []

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-004/expected‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] NormaliseTask returned
66
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] lambdaBody = \ lam^0 => \ lam^1 => \ lam^2 => \ lam^3 => Test.Y {a = Prelude.Types.Nat} lam^0 (Test.X lam^1 lam^2 lam^3);
77
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^16724760417298030003
88
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type not found, deriving...
9-
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Found or derived Test.Y^16724760417298030003.Y^16724760417298030003
10-
LOG deptycheck.test.utils.specialise:0: Test.Y^16724760417298030003.Y^16724760417298030003[0(fv^lam^0), 1(fv^lam^1), 2(fv^lam^2), 3(fv^lam^3)] CallGen params: [Test.Nn, Test.Nt, fromInteger 5, Test.Nn]
9+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Found or derived Y^16724760417298030003.Y^16724760417298030003
10+
LOG deptycheck.test.utils.specialise:0: Y^16724760417298030003.Y^16724760417298030003[0(fv^lam^0), 1(fv^lam^1), 2(fv^lam^2), 3(fv^lam^3)] CallGen params: [Test.Nn, Test.Nt, fromInteger 5, Test.Nn]
1111
LOG deptycheck.test.utils.specialise:0: Expanded e: Test.Y {a = Prelude.Types.Nat} Test.Nn' (Test.X Data.Fin.Fin (fromInteger 5) Test.Nn')
1212
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Task before normalisation: \ lam^0 => \ lam^1 => \ lam^2 => Test.Y {a = Prelude.Types.Nat} lam^0 (Test.X Data.Fin.Fin lam^1 lam^2)
1313
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] NormaliseTask returned: lambdaTy = (lam^0 : ({arg:1} : Prelude.Types.Nat) -> Prelude.Types.Nat) -> (lam^1 : Prelude.Types.Nat) -> (lam^2 : ({arg:3} : Data.Fin.Fin lam^1) -> Prelude.Types.Nat) -> Type;
1414
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] lambdaBody = \ lam^0 => \ lam^1 => \ lam^2 => Test.Y {a = Prelude.Types.Nat} lam^0 (Test.X Data.Fin.Fin lam^1 lam^2);
1515
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^10917347264591893612
1616
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type not found, deriving...
17-
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Found or derived Test.Y^10917347264591893612.Y^10917347264591893612
18-
LOG deptycheck.test.utils.specialise:0: Test.Y^10917347264591893612.Y^10917347264591893612[0(fv^lam^0), 1(fv^lam^1), 2(fv^lam^2)] CallGen params: [Test.Nn', fromInteger 5, Test.Nn']
17+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Found or derived Y^10917347264591893612.Y^10917347264591893612
18+
LOG deptycheck.test.utils.specialise:0: Y^10917347264591893612.Y^10917347264591893612[0(fv^lam^0), 1(fv^lam^1), 2(fv^lam^2)] CallGen params: [Test.Nn', fromInteger 5, Test.Nn']

0 commit comments

Comments
 (0)