Skip to content

Commit c2fccd7

Browse files
buzdenbuzden
committed
[ fix ] Fix ability of derivation of ungeneratable stuff
1 parent 6bbb814 commit c2fccd7

48 files changed

Lines changed: 957 additions & 34 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/Deriving/DepTyCheck/Gen/ForOneTypeConRhs/Impl.idr‎

Lines changed: 21 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -49,37 +49,39 @@ record TypeApp (0 con : Con) where
4949
{auto 0 argHeadTypeGood : AllTyArgsNamed argHeadType}
5050
argApps : Vect argHeadType.args.length .| Either (Fin con.args.length) TTImp
5151

52-
getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length (TypeApp con, Determination con)
52+
getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length (Either (FC, String) $ TypeApp con, Determination con)
5353
getTypeApps con = do
5454
let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName' arg, idx)
5555

5656
-- Analyse that we can do subgeneration for each constructor argument
5757
-- Fails using `Elaboration` if the given expression is not an application to a type constructor
58-
let analyseTypeApp : TTImp -> m (TypeApp con, Determination con)
58+
let analyseTypeApp : TTImp -> m (Either (FC, String) $ TypeApp con, Determination con)
5959
analyseTypeApp expr = do
6060
let (lhs, args) = unAppAny expr
61+
let as = args.asVect <&> \arg => case getExpr arg of
62+
expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
63+
expr => Right expr
6164
ty <- case lhs of
6265
IVar _ lhsName => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
63-
| Just found => pure found
66+
| Just found => pure $ pure found
6467
-- we haven't found, failing, there are at least two reasons
65-
failAt (getFC lhs) $ if isNamespaced lhsName
66-
then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
67-
else "Unsupported applications to a non-concrete type `\{lhsName}` in \{show con.name}"
68-
IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
69-
IType _ => pure typeInfoForTypeOfTypes
70-
lhs@(IPi {}) => failAt (getFC lhs) "Fields with function types are not supported in constructors, like in \{show con.name}"
71-
lhs => failAt (getFC lhs) "Unsupported type of a constructor's \{show con.name} field: \{show lhs}"
72-
let Yes lengthCorrect = decEq ty.args.length args.length
73-
| No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
74-
_ <- ensureTyArgsNamed ty
75-
let as = rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
76-
expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
77-
expr => Right expr
68+
if isNamespaced lhsName
69+
then failAt (getFC lhs) "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
70+
else pure $ Left (getFC lhs, "Unsupported applications to a non-concrete type `\{lhsName}` in \{show con.name}")
71+
IPrimVal _ (PrT t) => pure $ pure $ typeInfoForPrimType t
72+
IType _ => pure $ pure typeInfoForTypeOfTypes
73+
lhs@(IPi {}) => pure $ Left (getFC lhs, "Fields with function types are not supported in constructors, like in \{show con.name}")
74+
lhs => pure $ Left (getFC lhs, "Unsupported type of a constructor's \{show con.name} field: \{show lhs}")
75+
ta <- Prelude.for ty $ \ty : TypeInfo => do
76+
let Yes lengthCorrect = decEq ty.args.length args.length
77+
| No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
78+
_ <- ensureTyArgsNamed ty
79+
pure $ MkTypeApp ty $ rewrite lengthCorrect in as
7880
let strongDetermination = rights as.asList <&> mapMaybe (lookup' conArgIdxs) . allVarNames
7981
let strongDeterminationWeight = concatMap @{Additive} (max 1 . length) strongDetermination -- we add 1 for constant givens
8082
let stronglyDeterminedBy = fromList $ join strongDetermination
8183
let argsDependsOn = fromList (lefts as.asList) `difference` stronglyDeterminedBy
82-
pure (MkTypeApp ty as, MkDetermination stronglyDeterminedBy argsDependsOn $ argsDependsOn.size + strongDeterminationWeight)
84+
pure (ta, MkDetermination stronglyDeterminedBy argsDependsOn $ argsDependsOn.size + strongDeterminationWeight)
8385

8486
for con.args.asVect $ analyseTypeApp . type
8587

@@ -251,7 +253,8 @@ export
251253
genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do
252254

253255
-- Get info for the `genedArg`
254-
let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ TypeApp con) argsTypeApps
256+
let Right $ MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ Either _ $ TypeApp con) argsTypeApps
257+
| Left (fc, str) => failAt fc str
255258

256259
-- Acquire the set of arguments that are already present
257260
presentArguments <- get

‎tests/derivation/core/norec t-pi--.. noext 003/expected‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,7 @@
11
1/2: Building RunDerivedGen (RunDerivedGen.idr)
22
2/2: Building DerivedGen (DerivedGen.idr)
3-
Error: While processing right hand side of checkedGen. Error during reflection: Unsupported applications to a non-concrete type `a` in Builtin.Refl
3+
Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3]. While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3],<<Builtin.Refl>>. Can't find an implementation for DecEq Type.
44

5-
DerivedGen:1
6-
13 | Show (X b1 b2) where
7-
14 | show (MkX b1 b2 _) = "MkX \{show b1} \{show b2} Refl"
8-
15 |
9-
16 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
10-
17 | checkedGen = deriveGen
11-
^^^^^^^^^
5+
Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl:1
6+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
127

‎tests/derivation/core/norec t-pi--.. noext 004/expected‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,7 @@
11
1/2: Building RunDerivedGen (RunDerivedGen.idr)
22
2/2: Building DerivedGen (DerivedGen.idr)
3-
Error: While processing right hand side of checkedGen. Error during reflection: Unsupported applications to a non-concrete type `a` in Builtin.Refl
3+
Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3]. While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3],<<Builtin.Refl>>. Can't find an implementation for DecEq Type.
44

5-
DerivedGen:1
6-
15 | show (X0 b1 b2 _) = "X0 \{show b1} \{show b2} Refl"
7-
16 | show X1 = "X1"
8-
17 |
9-
18 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
10-
19 | checkedGen = deriveGen
11-
^^^^^^^^^
5+
Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl:1
6+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
127

‎tests/derivation/least-effort/print/adt/025 given-list-gen/DerivedGen.idr‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module DerivedGen
2+
3+
import Deriving.DepTyCheck.Gen
4+
5+
%default total
6+
7+
%language ElabReflection
8+
9+
data X : Type -> Type where
10+
MkX : Nat -> List a -> X a
11+
12+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> (Fuel -> Gen MaybeEmpty (t ** List t)) => Gen MaybeEmpty (t ** X t)

‎tests/derivation/least-effort/print/adt/025 given-list-gen/derive.ipkg‎

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

‎tests/derivation/least-effort/print/adt/025 given-list-gen/expected‎

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
1+
1/1: Building DerivedGen (DerivedGen.idr)
2+
LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel) -> Gen MaybeEmpty (t : Type ** List t))} -> Gen MaybeEmpty (t : Type ** X t)
3+
LOG deptycheck.derive.least-effort:7: DerivedGen.X[] MkX - used final order: [#2, #1]
4+
LOG deptycheck.derive.least-effort:7: Prelude.Types.Nat[] Z - used final order: []
5+
LOG deptycheck.derive.least-effort:7: Prelude.Types.Nat[] S - used final order: [#0]
6+
MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
7+
.=> MkArg
8+
MW
9+
AutoImplicit
10+
(Just "external^<Prelude.Basics.List>[]")
11+
( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fuel.Fuel")
12+
.-> var "Test.DepTyCheck.Gen.Gen"
13+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
14+
.$ (var "Builtin.DPair.DPair" .$ type .$ (MkArg MW ExplicitArg (Just "t") type .=> var "Prelude.Basics.List" .$ var "t")))
15+
.=> local
16+
{ decls =
17+
[ IClaim
18+
(MkIClaimData
19+
{ rig = MW
20+
, vis = Export
21+
, opts = []
22+
, type =
23+
mkTy
24+
{ name = "<DerivedGen.X>[]"
25+
, type =
26+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
27+
.-> var "Test.DepTyCheck.Gen.Gen"
28+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
29+
.$ ( var "Builtin.DPair.DPair"
30+
.$ type
31+
.$ (MkArg MW ExplicitArg (Just "{arg:2}") type .=> var "DerivedGen.X" .$ var "{arg:2}"))
32+
}
33+
})
34+
, IClaim
35+
(MkIClaimData
36+
{ rig = MW
37+
, vis = Export
38+
, opts = []
39+
, type =
40+
mkTy
41+
{ name = "<Prelude.Types.Nat>[]"
42+
, type =
43+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
44+
.-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat"
45+
}
46+
})
47+
, IDef
48+
emptyFC
49+
"<DerivedGen.X>[]"
50+
[ var "<DerivedGen.X>[]" .$ bindVar "^fuel_arg^"
51+
.= local
52+
{ decls =
53+
[ IClaim
54+
(MkIClaimData
55+
{ rig = MW
56+
, vis = Export
57+
, opts = []
58+
, type =
59+
mkTy
60+
{ name = "<<DerivedGen.MkX>>"
61+
, type =
62+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
63+
.-> var "Test.DepTyCheck.Gen.Gen"
64+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
65+
.$ ( var "Builtin.DPair.DPair"
66+
.$ type
67+
.$ (MkArg MW ExplicitArg (Just "{arg:2}") type .=> var "DerivedGen.X" .$ var "{arg:2}"))
68+
}
69+
})
70+
, IDef
71+
emptyFC
72+
"<<DerivedGen.MkX>>"
73+
[ var "<<DerivedGen.MkX>>" .$ bindVar "^cons_fuel^"
74+
.= var "Test.DepTyCheck.Gen.label"
75+
.$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)"))
76+
.$ ( var ">>="
77+
.$ (var "external^<Prelude.Basics.List>[]" .$ var "^outmost-fuel^")
78+
.$ ( MkArg MW ExplicitArg (Just "{lamc:1}") implicitFalse
79+
.=> iCase
80+
{ sc = var "{lamc:1}"
81+
, ty = implicitFalse
82+
, clauses =
83+
[ var "Builtin.DPair.MkDPair" .$ bindVar "a" .$ bindVar "{arg:3}"
84+
.= var ">>="
85+
.$ (var "<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
86+
.$ ( MkArg MW ExplicitArg (Just "{arg:4}") implicitFalse
87+
.=> var "Prelude.pure"
88+
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
89+
.$ ( var "Builtin.DPair.MkDPair"
90+
.$ implicitTrue
91+
.$ ( var "DerivedGen.MkX"
92+
.! ("a", implicitTrue)
93+
.$ var "{arg:4}"
94+
.$ var "{arg:3}")))
95+
]
96+
}))
97+
]
98+
]
99+
, scope =
100+
var "Test.DepTyCheck.Gen.label"
101+
.$ (var "fromString" .$ primVal (Str "DerivedGen.X[] (non-spending)"))
102+
.$ (var "<<DerivedGen.MkX>>" .$ var "^fuel_arg^")
103+
}
104+
]
105+
, IDef
106+
emptyFC
107+
"<Prelude.Types.Nat>[]"
108+
[ var "<Prelude.Types.Nat>[]" .$ bindVar "^fuel_arg^"
109+
.= local
110+
{ decls =
111+
[ IClaim
112+
(MkIClaimData
113+
{ rig = MW
114+
, vis = Export
115+
, opts = []
116+
, type =
117+
mkTy
118+
{ name = "<<Prelude.Types.Z>>"
119+
, type =
120+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
121+
.-> var "Test.DepTyCheck.Gen.Gen"
122+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
123+
.$ var "Prelude.Types.Nat"
124+
}
125+
})
126+
, IClaim
127+
(MkIClaimData
128+
{ rig = MW
129+
, vis = Export
130+
, opts = []
131+
, type =
132+
mkTy
133+
{ name = "<<Prelude.Types.S>>"
134+
, type =
135+
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
136+
.-> var "Test.DepTyCheck.Gen.Gen"
137+
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
138+
.$ var "Prelude.Types.Nat"
139+
}
140+
})
141+
, IDef
142+
emptyFC
143+
"<<Prelude.Types.Z>>"
144+
[ var "<<Prelude.Types.Z>>" .$ bindVar "^cons_fuel^"
145+
.= var "Test.DepTyCheck.Gen.label"
146+
.$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)"))
147+
.$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z")
148+
]
149+
, IDef
150+
emptyFC
151+
"<<Prelude.Types.S>>"
152+
[ var "<<Prelude.Types.S>>" .$ bindVar "^cons_fuel^"
153+
.= var "Test.DepTyCheck.Gen.label"
154+
.$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)"))
155+
.$ ( var ">>="
156+
.$ (var "<Prelude.Types.Nat>[]" .$ var "^cons_fuel^")
157+
.$ ( MkArg MW ExplicitArg (Just "{arg:5}") implicitFalse
158+
.=> var "Prelude.pure"
159+
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
160+
.$ (var "Prelude.Types.S" .$ var "{arg:5}")))
161+
]
162+
]
163+
, scope =
164+
iCase
165+
{ sc = var "^fuel_arg^"
166+
, ty = var "Data.Fuel.Fuel"
167+
, clauses =
168+
[ var "Data.Fuel.Dry"
169+
.= var "Test.DepTyCheck.Gen.label"
170+
.$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)"))
171+
.$ (var "<<Prelude.Types.Z>>" .$ var "^fuel_arg^")
172+
, var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^"
173+
.= var "Test.DepTyCheck.Gen.label"
174+
.$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (non-dry fuel)"))
175+
.$ ( var "Test.DepTyCheck.Gen.frequency"
176+
.$ ( var "::"
177+
.$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<<Prelude.Types.Z>>" .$ var "^fuel_arg^"))
178+
.$ ( var "::"
179+
.$ ( var "Builtin.MkPair"
180+
.$ (var "Deriving.DepTyCheck.Gen.ConsRecs.leftDepth" .$ var "^sub^fuel_arg^")
181+
.$ (var "<<Prelude.Types.S>>" .$ var "^sub^fuel_arg^"))
182+
.$ var "Nil")))
183+
]
184+
}
185+
}
186+
]
187+
]
188+
, scope = var "<DerivedGen.X>[]" .$ var "^outmost-fuel^"
189+
}
190+

‎tests/derivation/least-effort/print/adt/025 given-list-gen/run‎

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

‎tests/derivation/least-effort/print/gadt/023 generated-case-arg/DerivedGen.idr‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
module DerivedGen
2+
3+
import Deriving.DepTyCheck.Gen
4+
5+
%default total
6+
7+
%language ElabReflection
8+
9+
data X : (b : Bool) -> (if b then Unit else Nat) -> Type where
10+
XT : X True ()
11+
XF : X False n
12+
13+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> Gen MaybeEmpty (a ** b ** X a b)

‎tests/derivation/least-effort/print/gadt/023 generated-case-arg/derive.ipkg‎

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

‎tests/derivation/least-effort/print/gadt/023 generated-case-arg/expected‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
1/1: Building DerivedGen (DerivedGen.idr)
2+
Error: DerivedGen.case block in $resolved1 is not accessible in this context.
3+
4+
DerivedGen:1
5+
5 | %default total
6+
6 |
7+
7 | %language ElabReflection
8+
8 |
9+
9 | data X : (b : Bool) -> (if b then Unit else Nat) -> Type where
10+
^^^^^^^^^^^^^^^^^^^^^^^
11+

0 commit comments

Comments
 (0)