Skip to content

Commit cad8509

Browse files
buzdenbuzden
committed
[ fix ] Rename bound implicits in a determined non-cons expressions
1 parent e586fc5 commit cad8509

File tree

13 files changed

+207
-6
lines changed

13 files changed

+207
-6
lines changed

‎src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr

+7-1
Original file line numberDiff line numberDiff line change
@@ -52,10 +52,16 @@ canonicConsBody sig name con = do
5252
"argument expression: \{show argExpr}, reason: \{err}", argExpr)) $
5353
analyseDeepConsApp True conArgNames argExpr
5454
let allAppliedFreeNames = foldMap (either .| const empty .| SortedSet.fromList . map fst . fst) deepConsApps
55+
let bindAppliedFreeNames : TTImp -> TTImp
56+
bindAppliedFreeNames orig@(IVar _ n) = if contains n allAppliedFreeNames then bindVar $ bindNameRenamer n else orig
57+
-- /---------------------------------------------^^^^^^^
58+
-- `bindVar` instead of `var` here is because this expression can be earlier than the real binding, thus undeclared,
59+
-- and the compiler turns unnecessary `IBindVar`s into `IVar`s by itself
60+
bindAppliedFreeNames x = x
5561
deepConsApps <- for deepConsApps $ \case
5662
Right x => pure x
5763
Left (err, argExpr) => if null $ (allVarNames' argExpr `intersection` conArgNames) `difference` allAppliedFreeNames
58-
then pure ([] ** const argExpr)
64+
then pure ([] ** const $ mapTTImp bindAppliedFreeNames argExpr)
5965
else failAt conFC err
6066

6167
-- Acquire LHS bind expressions for the given parameters

‎tests/derivation/least-effort/print/regression/determined-noncons-given-add/expected

+2-2
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1(x), 2] B2 - used fina
7373
"<<DerivedGen.B1>>"
7474
[ var "<<DerivedGen.B1>>"
7575
.$ bindVar "^cons_fuel^"
76-
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
76+
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
7777
.$ (var "Prelude.Types.S" .$ bindVar "^bnd^{x:1}")
7878
.$ (var "DerivedGen.A1" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")
7979
.= var "Test.DepTyCheck.Gen.label"
@@ -89,7 +89,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1(x), 2] B2 - used fina
8989
[ var "<<DerivedGen.B2>>"
9090
.$ bindVar "^cons_fuel^"
9191
.$ ( var "Prelude.Types.plus"
92-
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
92+
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
9393
.$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))
9494
.$ (var "Prelude.Types.S" .$ bindVar "^bnd^{x:2}")
9595
.$ (var "DerivedGen.A2" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")

‎tests/derivation/least-effort/print/regression/determined-noncons-given-complex/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ LOG deptycheck.derive.least-effort:7: Data.Fin.Fin[0(n)] FS - used final order:
160160
[ var "<<DerivedGen.MHere>>"
161161
.$ bindVar "^cons_fuel^"
162162
.$ (var "DerivedGen.B.(::)" .$ bindVar "p" .$ bindVar "ps")
163-
.$ (var "Data.Fin.FZ" .! ("k", var "DerivedGen.B..length" .$ var "ps"))
163+
.$ (var "Data.Fin.FZ" .! ("k", var "DerivedGen.B..length" .$ bindVar "ps"))
164164
.= var "Test.DepTyCheck.Gen.label"
165165
.$ (var "fromString" .$ primVal (Str "DerivedGen.MHere (orders)"))
166166
.$ ( var "Prelude.pure"

‎tests/derivation/least-effort/print/regression/determined-noncons-given-impl/DerivedGen.idr

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
module DerivedGen
2+
3+
import Data.Nat
4+
5+
import Deriving.DepTyCheck.Gen
6+
7+
%default total
8+
9+
f : Nat -> (y : Nat) -> (0 _ : IsSucc y) => Nat
10+
f x y = case (modNatNZ x y %search) of
11+
Z => divNatNZ x y %search
12+
S _ => S (divNatNZ x y %search)
13+
14+
record NA where
15+
constructor MkNA
16+
curS : Nat
17+
{auto 0 curTotLTE : LTE curS curS}
18+
19+
data N : Nat -> NA -> Type where
20+
F : (0 nz : IsSucc c) =>
21+
{k : Nat} ->
22+
N c (MkNA (f k c) @{Relation.reflexive})
23+
24+
data NT : N cfg ar -> Type where
25+
NTF : NT $ F @{nz}
26+
27+
%language ElabReflection
28+
29+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> (cfg : Nat) -> (ar : NA) -> (node : N cfg ar) -> Gen MaybeEmpty $ NT node

‎tests/derivation/least-effort/print/regression/determined-noncons-given-impl/derive.ipkg

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/derive.ipkg

‎tests/derivation/least-effort/print/regression/determined-noncons-given-impl/expected

+99
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
1/1: Building DerivedGen (DerivedGen.idr)
2+
LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (cfg : Nat) -> (ar : NA) -> (node : N cfg ar) -> Gen MaybeEmpty (NT node)
3+
LOG deptycheck.derive.least-effort:7: DerivedGen.NT[0(ar), 1(cfg), 2] NTF - used final order: []
4+
MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
5+
.=> MkArg MW ExplicitArg (Just "outer^<cfg>") implicitTrue
6+
.=> MkArg MW ExplicitArg (Just "outer^<ar>") implicitTrue
7+
.=> MkArg MW ExplicitArg (Just "outer^<node>") implicitTrue
8+
.=> local
9+
{ decls =
10+
[ IClaim
11+
(MkIClaimData
12+
{ rig = MW
13+
, vis = Export
14+
, opts = []
15+
, type =
16+
mkTy
17+
{ name = "<DerivedGen.NT>[0, 1, 2]"
18+
, type =
19+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
20+
.-> MkArg MW ExplicitArg (Just "ar") (var "DerivedGen.NA")
21+
.-> MkArg MW ExplicitArg (Just "cfg") (var "Prelude.Types.Nat")
22+
.-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.N" .$ var "cfg" .$ var "ar")
23+
.-> var "Test.DepTyCheck.Gen.Gen"
24+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
25+
.$ (var "DerivedGen.NT" .! ("ar", var "ar") .! ("cfg", var "cfg") .$ var "{arg:1}")
26+
}
27+
})
28+
, IDef
29+
emptyFC
30+
"<DerivedGen.NT>[0, 1, 2]"
31+
[ var "<DerivedGen.NT>[0, 1, 2]"
32+
.$ bindVar "^fuel_arg^"
33+
.$ bindVar "inter^<ar>"
34+
.$ bindVar "inter^<cfg>"
35+
.$ bindVar "inter^<{arg:1}>"
36+
.= local
37+
{ decls =
38+
[ IClaim
39+
(MkIClaimData
40+
{ rig = MW
41+
, vis = Export
42+
, opts = []
43+
, type =
44+
mkTy
45+
{ name = "<<DerivedGen.NTF>>"
46+
, type =
47+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
48+
.-> MkArg MW ExplicitArg (Just "ar") (var "DerivedGen.NA")
49+
.-> MkArg MW ExplicitArg (Just "cfg") (var "Prelude.Types.Nat")
50+
.-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.N" .$ var "cfg" .$ var "ar")
51+
.-> var "Test.DepTyCheck.Gen.Gen"
52+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
53+
.$ (var "DerivedGen.NT" .! ("ar", var "ar") .! ("cfg", var "cfg") .$ var "{arg:1}")
54+
}
55+
})
56+
, IDef
57+
emptyFC
58+
"<<DerivedGen.NTF>>"
59+
[ var "<<DerivedGen.NTF>>"
60+
.$ bindVar "^cons_fuel^"
61+
.$ ( var "DerivedGen.MkNA"
62+
.$ ( var "DerivedGen.case block in "f""
63+
.$ bindVar "^bnd^{cfg:1}"
64+
.$ bindVar "nz"
65+
.$ bindVar "^bnd^{k:1}"
66+
.$ (var "Data.Nat.modNatNZ" .$ bindVar "^bnd^{k:1}" .$ bindVar "^bnd^{cfg:1}" .$ bindVar "nz"))
67+
.! ( "curTotLTE"
68+
, var "Data.Nat.reflexive"
69+
.! ( "x"
70+
, var "DerivedGen.case block in "f""
71+
.$ bindVar "^bnd^{cfg:1}"
72+
.$ bindVar "nz"
73+
.$ bindVar "^bnd^{k:1}"
74+
.$ (var "Data.Nat.modNatNZ" .$ bindVar "^bnd^{k:1}" .$ bindVar "^bnd^{cfg:1}" .$ bindVar "nz")
75+
)
76+
))
77+
.$ bindVar "^bnd^{cfg:1}"
78+
.$ (var "DerivedGen.F" .! ("c", implicitTrue) .! ("nz", bindVar "nz") .! ("k", bindVar "^bnd^{k:1}"))
79+
.= var "Test.DepTyCheck.Gen.label"
80+
.$ (var "fromString" .$ primVal (Str "DerivedGen.NTF (orders)"))
81+
.$ ( var "Prelude.pure"
82+
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
83+
.$ ( var "DerivedGen.NTF"
84+
.! ("{cfg:1}", implicitTrue)
85+
.! ("{k:1}", var "^bnd^{k:1}")
86+
.! ("nz", var "nz")))
87+
, var "<<DerivedGen.NTF>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
88+
]
89+
]
90+
, scope =
91+
var "Test.DepTyCheck.Gen.label"
92+
.$ (var "fromString" .$ primVal (Str "DerivedGen.NT[0(ar), 1(cfg), 2] (non-spending)"))
93+
.$ (var "<<DerivedGen.NTF>>" .$ var "^fuel_arg^" .$ var "inter^<ar>" .$ var "inter^<cfg>" .$ var "inter^<{arg:1}>")
94+
}
95+
]
96+
]
97+
, scope = var "<DerivedGen.NT>[0, 1, 2]" .$ var "^outmost-fuel^" .$ var "outer^<ar>" .$ var "outer^<cfg>" .$ var "outer^<node>"
98+
}
99+

‎tests/derivation/least-effort/print/regression/determined-noncons-given-impl/run

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/run

‎tests/derivation/least-effort/print/regression/determined-noncons-given-simple/expected

+2-2
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1] B2 - used final orde
6969
"<<DerivedGen.B1>>"
7070
[ var "<<DerivedGen.B1>>"
7171
.$ bindVar "^cons_fuel^"
72-
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
72+
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
7373
.$ (var "DerivedGen.A1" .$ bindVar "a" .$ bindVar "b")
7474
.= var "Test.DepTyCheck.Gen.label"
7575
.$ (var "fromString" .$ primVal (Str "DerivedGen.B1 (orders)"))
@@ -84,7 +84,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1] B2 - used final orde
8484
[ var "<<DerivedGen.B2>>"
8585
.$ bindVar "^cons_fuel^"
8686
.$ ( var "Prelude.Types.plus"
87-
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
87+
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
8888
.$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))
8989
.$ (var "DerivedGen.A2" .$ bindVar "a" .$ bindVar "b")
9090
.= var "Test.DepTyCheck.Gen.label"

‎tests/derivation/least-effort/run/regression/determined-noncons-given-impl/DerivedGen.idr

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
module DerivedGen
2+
3+
import RunDerivedGen
4+
5+
import Data.Fin
6+
7+
%default total
8+
9+
f : Nat -> (y : Nat) -> (0 _ : IsSucc y) => Nat
10+
f x y = case (modNatNZ x y %search) of
11+
Z => divNatNZ x y %search
12+
S _ => S (divNatNZ x y %search)
13+
14+
record NA where
15+
constructor MkNA
16+
curS : Nat
17+
{auto 0 curTotLTE : LTE curS curS}
18+
19+
data N : Nat -> NA -> Type where
20+
F : (0 nz : IsSucc c) =>
21+
{k : Nat} ->
22+
N c $ MkNA (f k c) @{Relation.reflexive}
23+
24+
data NT : N cfg ar -> Type where
25+
NTF : NT $ F @{nz}
26+
27+
checkedGen : Fuel -> (cfg : Nat) -> (ar : NA) -> (node : N cfg ar) -> Gen MaybeEmpty $ NT node
28+
checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
29+
30+
Show (NT n) where
31+
show NTF = "NTF"
32+
33+
main : IO ()
34+
main = runGs
35+
[ G $ \fl => checkedGen fl 1 (MkNA 2) $ F {k=2}
36+
]

‎tests/derivation/least-effort/run/regression/determined-noncons-given-impl/RunDerivedGen.idr

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/RunDerivedGen.idr

‎tests/derivation/least-effort/run/regression/determined-noncons-given-impl/derive.ipkg

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/derive.ipkg

‎tests/derivation/least-effort/run/regression/determined-noncons-given-impl/expected

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
1/2: Building RunDerivedGen (RunDerivedGen.idr)
2+
2/2: Building DerivedGen (DerivedGen.idr)
3+
Warning: Unreachable clause: (<<DerivedGen.NTF>>) (^outmost-fuel^) outer^<cfg> outer^<ar> outer^<node> inter^<cfg> inter^<ar> inter^<{arg:1}> (^fuel_arg^) _ _ _ _
4+
5+
Generated values:
6+
-----
7+
-----
8+
NTF
9+
-----
10+
NTF
11+
-----
12+
NTF
13+
-----
14+
NTF
15+
-----
16+
NTF
17+
-----
18+
NTF
19+
-----
20+
NTF
21+
-----
22+
NTF
23+
-----
24+
NTF
25+
-----
26+
NTF

‎tests/derivation/least-effort/run/regression/determined-noncons-given-impl/run

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../_common/run

0 commit comments

Comments
 (0)