Skip to content

Commit e53397f

Browse files
UARTmanUARTman
committed
[ fix ] Allow detection of existing specialised types in local context
1 parent 3f3129c commit e53397f

13 files changed

Lines changed: 81 additions & 28 deletions

File tree

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

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

117-
export
117+
-- export
118118
-- %defaulthint
119-
CurrentNS : Elaboration m => NamespaceProvider m
120-
CurrentNS = MkNSProvider $ do
121-
NS nsn _ <- inCurrentNS ""
122-
| _ => fail "Internal error: inCurrentNS did not return NS"
123-
pure nsn
119+
-- CurrentNS : Elaboration m => NamespaceProvider m
120+
-- CurrentNS = MkNSProvider $ do
121+
-- NS nsn _ <- inCurrentNS ""
122+
-- | _ => fail "Internal error: inCurrentNS did not return NS"
123+
-- pure nsn
124124

125125
export
126126
Monad m => MonadTrans t => NamespaceProvider m => NamespaceProvider (t m) where

‎pack.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ whitelist = [ "deptycheck-docs", "pil-fun", "pil-dyn" ]
88
[custom.all.hashable-derive]
99
type = "github"
1010
url = "https://github.com//uartman/hashable-derive"
11-
commit = "9c1788178848f5718cc1ddd3135bed463cb121d8"
11+
commit = "37a80fec1c72b7cbdb5a6e182f84899f34bcd1bd"
1212
ipkg = "hashable-derive.ipkg"
1313

1414
#######################

‎src/Deriving/DepTyCheck/Util/Specialisation.idr‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ specTaskToName' t = do
157157
(IVar _ n) => show $ snd $ unNS n
158158
x => show x
159159
hash <- pure $ show $ hash t
160-
pure $ fromString "\{vname}^\{hash}"
160+
pure $ fromString "\{vname}^\{hash}.\{vname}^\{hash}"
161161

162162
export %tcinline
163163
specialiseIfNeeded :
@@ -187,9 +187,12 @@ specialiseIfNeeded sig fuel givenParamValues = do
187187
logPoint DetailedDebug "deptycheck.util.specialisation" [sig] "Specialised type not found, deriving..."
188188
Right (specTy, specDecls) <- runEitherT {m} {e=SpecialisationError} $ specialiseDataRaw specName lambdaTy lambdaBody
189189
| Left err => fail "INTERNAL ERROR: Specialisation \{show lambdaBody} failed with error \{show err}."
190+
logPoint DetailedDebug "deptycheck.util.specialisation" [sig] "Derived \{show specTy.name}"
190191
pure (specTy, specDecls)
191-
Just specTy => pure (specTy, [])
192-
logPoint DetailedDebug "deptycheck.util.specialisation" [sig] "Found or derived \{show specTy.name}"
192+
Just specTy => do
193+
logPoint DetailedDebug "deptycheck.util.specialisation" [sig] "Found \{show specTy.name}"
194+
pure (specTy, [])
195+
-- logPoint DetailedDebug "deptycheck.util.specialisation" [sig] "Found or derived \{show specTy.name}"
193196
let Yes stNamed = areAllTyArgsNamed specTy
194197
| No _ => fail "INTERNAL ERROR: Specialised type \{show specTy.name} does not have fully named arguments and constructors."
195198
let (newGP ** newGVals) = genGivens $ mapMaybe (\(a,b) => map (,b) a) $ zip givenSubst $ withIndex specTy.args

‎tests/derivation/utils/specialise-if-needed/_common/Shared.idr‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ export
8383
runSIN' :
8484
Elaboration m =>
8585
MonadWriter (Maybe CallGen) m =>
86-
Maybe NamesInfoInTypes -> Bool -> TTImp -> m $ Maybe TTImp
86+
Maybe NamesInfoInTypes -> Bool -> TTImp -> m $ Maybe (TTImp, TypeInfo)
8787
runSIN' namesInfo declareSpec e = do
8888
e <- expandNames e
8989
logPoint Warning "deptycheck.test.utils.specialise" [] "Expanded e: \{show e}"
@@ -113,12 +113,12 @@ runSIN' namesInfo declareSpec e = do
113113
Nothing => pure Nothing
114114
Just (sdecls, stype, retExpr) => do
115115
when declareSpec $ declare sdecls
116-
pure $ Just retExpr
116+
pure $ Just (retExpr, stype)
117117

118118

119119
export
120120
runSIN'' :
121121
Elaboration m =>
122-
Maybe NamesInfoInTypes -> Bool -> TTImp -> m (Maybe TTImp, Maybe CallGen)
122+
Maybe NamesInfoInTypes -> Bool -> TTImp -> m (Maybe (TTImp, TypeInfo), Maybe CallGen)
123123
runSIN'' namesInfo declareSpec e =
124124
runWriterT {w=Maybe CallGen} {m} $ runSIN' namesInfo declareSpec e

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ LOG deptycheck.test.utils.specialise:0: Expanded e: Data.Vect.Vect _ Prelude.Ty
44
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Task before normalisation: \ lam^0 => Data.Vect.Vect lam^0 Prelude.Types.Nat
55
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] NormaliseTask returned: lambdaTy = (lam^0 : Prelude.Types.Nat) -> Type;
66
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] lambdaBody = \ lam^0 => Data.Vect.Vect lam^0 Prelude.Types.Nat;
7-
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Specialised type name: Vect^17613086623960416996
7+
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Specialised type name: Vect^9686363643684445030.Vect^9686363643684445030
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 Vect^17613086623960416996.Vect^17613086623960416996
10-
LOG deptycheck.test.utils.specialise:0: Vect^17613086623960416996.Vect^17613086623960416996[] CallGen params: []
9+
LOG deptycheck.util.specialisation:20: Data.Vect.Vect[1(elem)] Derived Vect^9686363643684445030.Vect^9686363643684445030
10+
LOG deptycheck.test.utils.specialise:0: Vect^9686363643684445030.Vect^9686363643684445030[] CallGen params: []

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ LOG deptycheck.test.utils.specialise:0: Expanded e: Test.X Prelude.Types.Nat Pr
44
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Task before normalisation: \ lam^0 => Test.X Prelude.Types.Nat lam^0
55
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] NormaliseTask returned: lambdaTy = (lam^0 : ({arg:1} : Prelude.Types.Nat) -> Prelude.Types.Nat) -> Type;
66
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] lambdaBody = \ lam^0 => Test.X Prelude.Types.Nat lam^0;
7-
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^15319567236415762791
7+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^17949373096448478648.X^17949373096448478648
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 X^15319567236415762791.X^15319567236415762791
10-
LOG deptycheck.test.utils.specialise:0: X^15319567236415762791.X^15319567236415762791[0(fv^lam^0)] CallGen params: [Prelude.Types.S]
9+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Derived X^17949373096448478648.X^17949373096448478648
10+
LOG deptycheck.test.utils.specialise:0: X^17949373096448478648.X^17949373096448478648[0(fv^lam^0)] CallGen params: [Prelude.Types.S]

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ LOG deptycheck.test.utils.specialise:0: Expanded e: Test.X Prelude.Types.Nat Da
44
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Task before normalisation: Test.X Prelude.Types.Nat Data.Fin.Fin
55
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] NormaliseTask returned: lambdaTy = Type;
66
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] lambdaBody = Test.X Prelude.Types.Nat Data.Fin.Fin;
7-
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^16134534282501286198
7+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Specialised type name: X^8135581006587252120.X^8135581006587252120
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 X^16134534282501286198.X^16134534282501286198
10-
LOG deptycheck.test.utils.specialise:0: X^16134534282501286198.X^16134534282501286198[] CallGen params: []
9+
LOG deptycheck.util.specialisation:20: Test.X[0(t), 1] Derived X^8135581006587252120.X^8135581006587252120
10+
LOG deptycheck.test.utils.specialise:0: X^8135581006587252120.X^8135581006587252120[] CallGen params: []

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,15 @@ LOG deptycheck.test.utils.specialise:0: Expanded e: Test.Y {a = Prelude.Types.N
44
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Task before normalisation: \ lam^0 => \ lam^1 => \ lam^2 => \ lam^3 => Test.Y {a = Prelude.Types.Nat} lam^0 (Test.X lam^1 lam^2 lam^3)
55
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 : ({arg:2} : Prelude.Types.Nat) -> Type) -> (lam^2 : Prelude.Types.Nat) -> (lam^3 : ({arg:3} : lam^1 lam^2) -> Prelude.Types.Nat) -> Type;
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);
7-
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^16724760417298030003
7+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^14421981371219706324.Y^14421981371219706324
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 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]
9+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Derived Y^14421981371219706324.Y^14421981371219706324
10+
LOG deptycheck.test.utils.specialise:0: Y^14421981371219706324.Y^14421981371219706324[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);
15-
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^10917347264591893612
15+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Specialised type name: Y^17936145782101774282.Y^17936145782101774282
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 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']
17+
LOG deptycheck.util.specialisation:20: Test.Y[0(a), 1, 2] Derived Y^17936145782101774282.Y^17936145782101774282
18+
LOG deptycheck.test.utils.specialise:0: Y^17936145782101774282.Y^17936145782101774282[0(fv^lam^0), 1(fv^lam^1), 2(fv^lam^2)] CallGen params: [Test.Nn', fromInteger 5, Test.Nn']

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-005/Shared.idr‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/Shared.idr

‎tests/derivation/utils/specialise-if-needed/spec-if-needed-005/Test.idr‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
module Test
2+
3+
import Data.Fin
4+
import Shared
5+
6+
%language ElabReflection
7+
8+
%logging "deptycheck.util.specialisation" 20
9+
10+
11+
%runElab do
12+
(Just (_, ti), _) <- runSIN'' Nothing False `(List Nat)
13+
| _ => fail "Didn't generate a specialised type!"
14+
logMsg "" 0 $ show ti.name
15+
specNIIT <- getNamesInfoInTypes ti
16+
logMsg "" 0 $ show $ keys $ knownTypes
17+
runSIN (Just specNIIT) False `(List Nat)
18+
19+
-- specRes : Maybe (TTImp, TypeInfo)
20+
-- specRes = %runElab runSIN' Nothing True `(List Nat)
21+
--
22+
23+
-- specNIIT : NamesInfoInTypes
24+
-- specNIIT = %runElab do
25+
-- let Just (_, ti) = specRes
26+
-- | _ => fail "Didn't find specialised type!"
27+
-- getNamesInfoInTypes ti
28+
--
29+
-- %runElab runSIN (Just specNIIT) False `(List Nat)

0 commit comments

Comments
 (0)