Skip to content

Commit 4c30a1d

Browse files
buzdenbuzden
committed
[ fix ] Don't check already fully determined arguments
1 parent 143a3dd commit 4c30a1d

File tree

30 files changed

+833
-7
lines changed

30 files changed

+833
-7
lines changed

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

+9-4
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,16 @@ canonicConsBody sig name con = do
4646
-- - (maybe, deeply) constructor call (need to match)
4747
-- - function call on a free param (need to use "inverted function" filtering trick)
4848
-- - something else (cannot manage yet)
49-
deepConsApps <- for sig.givenParams.asVect $ \idx => do
49+
let deepConsApps = sig.givenParams.asVect <&> \idx => do
5050
let argExpr = conRetTypeArg idx
51-
let Right analysed = analyseDeepConsApp True conArgNames argExpr
52-
| Left err => failAt conFC "Argument #\{show idx} is not supported yet, argument expression: \{show argExpr}, reason: \{err}"
53-
pure analysed
51+
mapFst (\err => ("Argument #\{show idx} is not supported yet, argument expression: \{show argExpr}, reason: \{err}", argExpr)) $
52+
analyseDeepConsApp True conArgNames argExpr
53+
let allAppliedFreeNames = foldMap (either .| const empty .| SortedSet.fromList . map fst . fst) deepConsApps
54+
deepConsApps <- for deepConsApps $ \case
55+
Right x => pure x
56+
Left (err, argExpr) => if null $ (allVarNames' argExpr `intersection` conArgNames) `difference` allAppliedFreeNames
57+
then pure ([] ** const argExpr)
58+
else failAt conFC err
5459

5560
-- Acquire LHS bind expressions for the given parameters
5661
-- Determine pairs of names which should be `decEq`'ed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ analyseDeepConsApp ccdi freeNames = isD where
8585

8686
-- Check that this is an application to a constructor's name
8787
let Just con = lookupCon lhsName
88-
| Nothing => Left "name `\{lhsName}` is not a constructor"
88+
| Nothing => if ccdi then Left "name `\{lhsName}` is not a constructor" else pure ([] ** const implicitTrue)
8989

9090
-- Acquire type-determination info, if needed
9191
typeDetermInfo <- if ccdi then assert_total {- `ccdi` is `True` here when `False` inside -} $ typeDeterminedArgs con else pure neutral

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

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module DerivedGen
2+
3+
import Deriving.DepTyCheck.Gen
4+
5+
import Data.Fin
6+
7+
%default total
8+
9+
data A : Nat -> Nat -> Type where
10+
A1 : (0 a : Nat) -> (0 b : Nat) -> A (S x) (a + b)
11+
A2 : (0 a : Nat) -> (0 b : Nat) -> A (S x) (a + b + 2)
12+
13+
data B : A x n -> Type where
14+
B1 : B $ A1 a b
15+
B2 : B $ A2 a b
16+
17+
%language ElabReflection
18+
19+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> (n : Nat) -> (x : Nat) -> (sub : A x n) -> Gen MaybeEmpty (B sub)

‎tests/derivation/least-effort/print/regression/determined-noncons-given-add/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-add/expected

+123
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
1/1: Building DerivedGen (DerivedGen.idr)
2+
LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (x : Nat) -> (sub : A x n) -> Gen MaybeEmpty (B sub)
3+
LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1(x), 2] B1 - used final order: []
4+
LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1(x), 2] B2 - used final order: []
5+
MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
6+
.=> MkArg MW ExplicitArg (Just "outer^<n>") implicitTrue
7+
.=> MkArg MW ExplicitArg (Just "outer^<x>") implicitTrue
8+
.=> MkArg MW ExplicitArg (Just "outer^<sub>") implicitTrue
9+
.=> local
10+
{ decls =
11+
[ IClaim
12+
(MkIClaimData
13+
{ rig = MW
14+
, vis = Export
15+
, opts = []
16+
, type =
17+
mkTy
18+
{ name = "<DerivedGen.B>[0, 1, 2]"
19+
, type =
20+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
21+
.-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat")
22+
.-> MkArg MW ExplicitArg (Just "x") (var "Prelude.Types.Nat")
23+
.-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.A" .$ var "x" .$ var "n")
24+
.-> var "Test.DepTyCheck.Gen.Gen"
25+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
26+
.$ (var "DerivedGen.B" .! ("n", var "n") .! ("x", var "x") .$ var "{arg:1}")
27+
}
28+
})
29+
, IDef
30+
emptyFC
31+
"<DerivedGen.B>[0, 1, 2]"
32+
[ var "<DerivedGen.B>[0, 1, 2]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<n>" .$ bindVar "inter^<x>" .$ bindVar "inter^<{arg:1}>"
33+
.= local
34+
{ decls =
35+
[ IClaim
36+
(MkIClaimData
37+
{ rig = MW
38+
, vis = Export
39+
, opts = []
40+
, type =
41+
mkTy
42+
{ name = "<<DerivedGen.B1>>"
43+
, type =
44+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
45+
.-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat")
46+
.-> MkArg MW ExplicitArg (Just "x") (var "Prelude.Types.Nat")
47+
.-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.A" .$ var "x" .$ var "n")
48+
.-> var "Test.DepTyCheck.Gen.Gen"
49+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
50+
.$ (var "DerivedGen.B" .! ("n", var "n") .! ("x", var "x") .$ var "{arg:1}")
51+
}
52+
})
53+
, IClaim
54+
(MkIClaimData
55+
{ rig = MW
56+
, vis = Export
57+
, opts = []
58+
, type =
59+
mkTy
60+
{ name = "<<DerivedGen.B2>>"
61+
, type =
62+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
63+
.-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat")
64+
.-> MkArg MW ExplicitArg (Just "x") (var "Prelude.Types.Nat")
65+
.-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.A" .$ var "x" .$ var "n")
66+
.-> var "Test.DepTyCheck.Gen.Gen"
67+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
68+
.$ (var "DerivedGen.B" .! ("n", var "n") .! ("x", var "x") .$ var "{arg:1}")
69+
}
70+
})
71+
, IDef
72+
emptyFC
73+
"<<DerivedGen.B1>>"
74+
[ var "<<DerivedGen.B1>>"
75+
.$ bindVar "^cons_fuel^"
76+
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
77+
.$ (var "Prelude.Types.S" .$ bindVar "^bnd^{x:1}")
78+
.$ (var "DerivedGen.A1" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")
79+
.= var "Test.DepTyCheck.Gen.label"
80+
.$ (var "fromString" .$ primVal (Str "DerivedGen.B1 (orders)"))
81+
.$ ( var "Prelude.pure"
82+
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
83+
.$ (var "DerivedGen.B1" .! ("{x:1}", var "^bnd^{x:1}") .! ("b", var "b") .! ("a", var "a")))
84+
, var "<<DerivedGen.B1>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
85+
]
86+
, IDef
87+
emptyFC
88+
"<<DerivedGen.B2>>"
89+
[ var "<<DerivedGen.B2>>"
90+
.$ bindVar "^cons_fuel^"
91+
.$ ( var "Prelude.Types.plus"
92+
.$ (var "Prelude.Types.plus" .$ var "a" .$ var "b")
93+
.$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))
94+
.$ (var "Prelude.Types.S" .$ bindVar "^bnd^{x:2}")
95+
.$ (var "DerivedGen.A2" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")
96+
.= var "Test.DepTyCheck.Gen.label"
97+
.$ (var "fromString" .$ primVal (Str "DerivedGen.B2 (orders)"))
98+
.$ ( var "Prelude.pure"
99+
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
100+
.$ (var "DerivedGen.B2" .! ("{x:2}", var "^bnd^{x:2}") .! ("b", var "b") .! ("a", var "a")))
101+
, var "<<DerivedGen.B2>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
102+
]
103+
]
104+
, scope =
105+
var "Test.DepTyCheck.Gen.label"
106+
.$ (var "fromString" .$ primVal (Str "DerivedGen.B[0(n), 1(x), 2] (non-spending)"))
107+
.$ ( var "Test.DepTyCheck.Gen.oneOf"
108+
.! ("em", var "MaybeEmpty")
109+
.$ ( var "::"
110+
.$ (var "<<DerivedGen.B1>>" .$ var "^fuel_arg^" .$ var "inter^<n>" .$ var "inter^<x>" .$ var "inter^<{arg:1}>")
111+
.$ ( var "::"
112+
.$ ( var "<<DerivedGen.B2>>"
113+
.$ var "^fuel_arg^"
114+
.$ var "inter^<n>"
115+
.$ var "inter^<x>"
116+
.$ var "inter^<{arg:1}>")
117+
.$ var "Nil")))
118+
}
119+
]
120+
]
121+
, scope = var "<DerivedGen.B>[0, 1, 2]" .$ var "^outmost-fuel^" .$ var "outer^<n>" .$ var "outer^<x>" .$ var "outer^<sub>"
122+
}
123+

‎tests/derivation/least-effort/print/regression/determined-noncons-given-add/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-complex/DerivedGen.idr

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
module DerivedGen
2+
3+
import Deriving.DepTyCheck.Gen
4+
5+
import Data.Fin
6+
7+
%default total
8+
9+
namespace A
10+
11+
public export
12+
data FinsList : Nat -> Type where
13+
Nil : FinsList n
14+
(::) : Fin n -> FinsList n -> FinsList n
15+
16+
public export
17+
(.length) : FinsList n -> Nat
18+
(.length) [] = 0
19+
(.length) (x::xs) = S xs.length
20+
21+
public export
22+
fst : (fs : FinsList s) -> Fin fs.length -> Fin s
23+
fst (f::_ ) _ = f
24+
25+
namespace B
26+
27+
public export
28+
data NatsList = Nil | (::) Nat NatsList
29+
30+
public export
31+
(.length) : NatsList -> Nat
32+
(.length) [] = Z
33+
(.length) (_::ms) = S ms.length
34+
35+
data FindNat : (nats: NatsList) -> Fin (nats.length) -> Type where
36+
MHere : FindNat (p::ps) FZ
37+
38+
data Test : (nats: NatsList) -> FinsList (nats.length) -> Type where
39+
MkT : FindNat nats (fst fins f) -> Test nats fins
40+
41+
%language ElabReflection
42+
43+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
44+
Fuel -> (nats: NatsList) -> (fins: FinsList $ nats.length) -> Gen MaybeEmpty $ Test nats fins

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

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

0 commit comments

Comments
 (0)