Skip to content

Commit 9c0f3c2

Browse files
buzdenbuzden
committed
[ derive ] Don't stop analysing cons when error occur
1 parent 9b33209 commit 9c0f3c2

18 files changed

Lines changed: 196 additions & 54 deletions

File tree

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

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -50,23 +50,24 @@ canonicConsBody sig name con = do
5050
-- - (maybe, deeply) constructor call (need to match)
5151
-- - function call on a free param (need to use "inverted function" filtering trick)
5252
-- - something else (cannot manage yet, unless it is fully determined by other given arguments)
53-
let deepConsApps : Vect _ $ Either (String, TTImp, List Name) _ := sig.givenParams.asVect <&> \idx => do
53+
let deepConsApps : Vect _ (DeepConsAnalysisRes True, Maybe String, TTImp) := sig.givenParams.asVect <&> \idx => do
5454
let argExpr = conRetTypeArg idx
55-
let (ei, fns) = runWriter $ runEitherT {e=String} {m=Writer _} $ analyseDeepConsApp True conArgNames argExpr
56-
flip mapFst ei $ \err =>
57-
("Argument #\{show idx} of \{show con.name} with given type arguments [\{showGivens sig}] is not supported, " ++
58-
"argument expression: \{show argExpr}, reason: \{err}", argExpr, fns)
59-
let allAppliedFreeNames = foldMap (SortedSet.fromList . either (snd . snd) (map fst . fst)) deepConsApps
55+
let (fns, errs) = runWriter {w=List String} $ analyseDeepConsApp True conArgNames argExpr
56+
let err = if null errs then Nothing else Just $
57+
"Argument #\{show idx} of \{show con.name} with given type arguments [\{showGivens sig}] is not supported, " ++
58+
"argument expression: \{show argExpr}, reason(s): \{joinBy "; " errs}"
59+
(fns, err, argExpr)
60+
let allAppliedFreeNames = foldMap (SortedSet.fromList . map fst . fst . fst) deepConsApps
6061
let bindAppliedFreeNames : TTImp -> TTImp
6162
bindAppliedFreeNames orig@(IVar _ n) = if contains n allAppliedFreeNames then bindVar n else orig
6263
-- /---------------------------------------------^^^^^^^
6364
-- `bindVar` instead of `var` here is because this expression can be earlier than the real binding, thus undeclared,
6465
-- and the compiler turns unnecessary `IBindVar`s into `IVar`s by itself
6566
bindAppliedFreeNames x = x
6667
deepConsApps <- for deepConsApps $ \case
67-
Right x => pure x
68-
Left (err, argExpr, fns) => if null $ (allVarNames' argExpr `intersection` conArgNames) `difference` allAppliedFreeNames
69-
then pure (filter (contains' conArgNames) fns <&> (, neutral) ** const $ mapTTImp bindAppliedFreeNames argExpr)
68+
(x, Nothing, _) => pure x
69+
(x, Just err, argExpr) => if null $ (allVarNames' argExpr `intersection` conArgNames) `difference` allAppliedFreeNames
70+
then pure x
7071
else failAt conFC err
7172

7273
-- Acquire LHS bind expressions for the given parameters

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

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -61,13 +61,12 @@ MaybeConsDetermInfo False = Unit
6161
||| It returns correct bind expression only when all given bind names are different.
6262
export
6363
analyseDeepConsApp : NamesInfoInTypes =>
64-
MonadError String m =>
65-
MonadWriter (List Name) m => -- a redundant thing, allowing, however, returning this list even on errors
64+
MonadWriter (List String) m =>
6665
(collectConsDetermInfo : Bool) ->
6766
(freeNames : SortedSet Name) ->
6867
(analysedExpr : TTImp) ->
6968
m $ DeepConsAnalysisRes collectConsDetermInfo
70-
analyseDeepConsApp ccdi freeNames = isD where
69+
analyseDeepConsApp ccdi freeNames = pass . map (, nub) . isD where
7170

7271
isD : TTImp -> m $ DeepConsAnalysisRes ccdi
7372
isD e = do
@@ -76,24 +75,24 @@ analyseDeepConsApp ccdi freeNames = isD where
7675
let (IVar _ lhsName, args) = unAppAny e
7776
| (IType {} , _) => pure $ noFree e
7877
| (IPrimVal {}, _) => pure $ noFree e
79-
| _ => throwError "not an application to a variable"
78+
| _ => bad "not an application to a variable"
8079

8180
-- Check if this is a free name
8281
let False = contains lhsName freeNames
8382
| True => if null args
84-
then do tell [lhsName]; pure $ if ccdi then ([(lhsName, neutral)] ** \f => f FZ) else [lhsName]
85-
else throwError "applying free name to some arguments"
83+
then pure $ if ccdi then ([(lhsName, neutral)] ** \f => f FZ) else [lhsName]
84+
else bad "applying free name to some arguments"
8685

8786
-- Check that this is an application to a constructor's name
8887
let Just con = lookupCon lhsName
89-
| Nothing => if ccdi then throwError "name `\{lhsName}` is not a constructor" else pure $ noFree implicitTrue
88+
| Nothing => bad "name `\{lhsName}` is not a constructor"
9089

9190
-- Acquire type-determination info, if needed
9291
typeDetermInfo <- if ccdi then assert_total {- `ccdi` is `True` here when `False` inside -} $ typeDeterminedArgs con else pure neutral
9392
let _ : Vect con.args.length (MaybeConsDetermInfo ccdi) := typeDetermInfo
9493

9594
let Just typeDetermInfo = reorder typeDetermInfo
96-
| Nothing => throwError "INTERNAL ERROR: cannot reorder formal determ info along with a call to a constructor"
95+
| Nothing => bad "INTERNAL ERROR: cannot reorder formal determ info along with a call to a constructor"
9796

9897
-- Analyze deeply all the arguments
9998
deepArgs <- for (args.asVect `zip` typeDetermInfo) $
@@ -109,6 +108,11 @@ analyseDeepConsApp ccdi freeNames = isD where
109108
noFree : TTImp -> DeepConsAnalysisRes ccdi
110109
noFree e = if ccdi then ([] ** const e) else []
111110

111+
bad : String -> m $ DeepConsAnalysisRes ccdi
112+
bad msg = tell [msg] $> noFree implicitTrue
113+
-- well, returning `implicitTrue` may be too kinda lazy, maybe, we should return `e` itself, maybe dotted;
114+
-- but we need to work with variables determination correctly -- they mustn't be deceqed further down
115+
112116
mergeApp : (ccdi : _) -> DeepConsAnalysisRes ccdi -> (AnyApp, DeepConsAnalysisRes ccdi) -> DeepConsAnalysisRes ccdi
113117
mergeApp False namesL (_, namesR) = namesL ++ namesR
114118
mergeApp True (namesL ** bindL) (anyApp, (namesR ** bindR)) = MkDPair (namesL ++ namesR) $ \bindNames => do

‎tests/derivation/core/non-cons given match 001-neg/expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
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: Argument #0 of DerivedGen.X2 with given type arguments [0] is not supported, argument expression: DerivedGen.boolToNat x, reason: name `DerivedGen.boolToNat` is not a constructor
3+
Error: While processing right hand side of checkedGen. Error during reflection: Argument #0 of DerivedGen.X2 with given type arguments [0] is not supported, argument expression: DerivedGen.boolToNat x, reason(s): name `DerivedGen.boolToNat` is not a constructor
44

55
DerivedGen:1
66
12 |

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

Lines changed: 2 additions & 4 deletions
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" .$ bindVar "a" .$ bindVar "b")
76+
.$ implicitTrue
7777
.$ (var "Prelude.Types.S" .$ bindVar "{x:1}")
7878
.$ (var "DerivedGen.A1" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")
7979
.= var "Test.DepTyCheck.Gen.label"
@@ -88,9 +88,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1(x), 2] B2 - used fina
8888
"<<DerivedGen.B2>>"
8989
[ var "<<DerivedGen.B2>>"
9090
.$ bindVar "^cons_fuel^"
91-
.$ ( var "Prelude.Types.plus"
92-
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
93-
.$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))
91+
.$ implicitTrue
9492
.$ (var "Prelude.Types.S" .$ bindVar "{x:2}")
9593
.$ (var "DerivedGen.A2" .! ("x", implicitTrue) .$ bindVar "a" .$ bindVar "b")
9694
.= var "Test.DepTyCheck.Gen.label"

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,7 @@ LOG deptycheck.derive.least-effort:7: Data.Fin.Fin[0(n)] FS - used final order:
175175
[ var "<<DerivedGen.MHere>>"
176176
.$ bindVar "^cons_fuel^"
177177
.$ (var "DerivedGen.B.(::)" .$ bindVar "p" .$ bindVar "ps")
178-
.$ (var "Data.Fin.FZ" .! ("k", var "DerivedGen.B..length" .$ bindVar "ps"))
178+
.$ (var "Data.Fin.FZ" .! ("k", implicitTrue))
179179
.= var "Test.DepTyCheck.Gen.label"
180180
.$ (var "fromString" .$ primVal (Str "DerivedGen.MHere (orders)"))
181181
.$ ( var "Prelude.pure"

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

Lines changed: 1 addition & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -58,22 +58,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.NT[0(ar), 1(cfg), 2] NTF - used
5858
"<<DerivedGen.NTF>>"
5959
[ var "<<DerivedGen.NTF>>"
6060
.$ bindVar "^cons_fuel^"
61-
.$ ( var "DerivedGen.MkNA"
62-
.$ ( var "DerivedGen.case block in "f""
63-
.$ bindVar "{cfg:1}"
64-
.$ bindVar "nz"
65-
.$ bindVar "{k:1}"
66-
.$ (var "Data.Nat.modNatNZ" .$ bindVar "{k:1}" .$ bindVar "{cfg:1}" .$ bindVar "nz"))
67-
.! ( "curTotLTE"
68-
, var "Data.Nat.reflexive"
69-
.! ( "x"
70-
, var "DerivedGen.case block in "f""
71-
.$ bindVar "{cfg:1}"
72-
.$ bindVar "nz"
73-
.$ bindVar "{k:1}"
74-
.$ (var "Data.Nat.modNatNZ" .$ bindVar "{k:1}" .$ bindVar "{cfg:1}" .$ bindVar "nz")
75-
)
76-
))
61+
.$ (var "DerivedGen.MkNA" .$ implicitTrue .! ("curTotLTE", implicitTrue))
7762
.$ bindVar "{cfg:1}"
7863
.$ (var "DerivedGen.F" .! ("c", implicitTrue) .! ("nz", bindVar "nz") .! ("k", bindVar "{k:1}"))
7964
.= var "Test.DepTyCheck.Gen.label"

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

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ LOG deptycheck.derive.least-effort:7: Prelude.Types.Nat[] S - used final order:
234234
[ var "<<DerivedGen.CPEmpty>>"
235235
.$ bindVar "^cons_fuel^"
236236
.$ bindVar "ms"
237-
.$ (var "DerivedGen.FinsList.Nil" .! ("n", var "DerivedGen.ModuleSig..length" .$ bindVar "ms"))
237+
.$ (var "DerivedGen.FinsList.Nil" .! ("n", implicitTrue))
238238
.$ (var "DerivedGen.FinsList.Nil" .! ("n", var "Prelude.Types.Z"))
239239
.= var "Test.DepTyCheck.Gen.label"
240240
.$ (var "fromString" .$ primVal (Str "DerivedGen.CPEmpty (orders)"))
@@ -250,14 +250,7 @@ LOG deptycheck.derive.least-effort:7: Prelude.Types.Nat[] S - used final order:
250250
.$ bindVar "^cons_fuel^"
251251
.$ bindVar "ms"
252252
.$ bindVar "subMs"
253-
.$ ( var "DerivedGen.FinsList.(::)"
254-
.! ( "n"
255-
, var "DerivedGen.FinsList..length"
256-
.! ("n", var "DerivedGen.ModuleSig..length" .$ bindVar "ms")
257-
.$ bindVar "subMs"
258-
)
259-
.$ bindVar "subMF"
260-
.$ bindVar "restFins")
253+
.$ (var "DerivedGen.FinsList.(::)" .! ("n", implicitTrue) .$ bindVar "subMF" .$ bindVar "restFins")
261254
.= var "Test.DepTyCheck.Gen.label"
262255
.$ (var "fromString" .$ primVal (Str "DerivedGen.CPCons (orders)"))
263256
.$ ( var ">>="

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

Lines changed: 2 additions & 4 deletions
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" .$ bindVar "a" .$ bindVar "b")
72+
.$ implicitTrue
7373
.$ (var "DerivedGen.A1" .$ bindVar "a" .$ bindVar "b")
7474
.= var "Test.DepTyCheck.Gen.label"
7575
.$ (var "fromString" .$ primVal (Str "DerivedGen.B1 (orders)"))
@@ -83,9 +83,7 @@ LOG deptycheck.derive.least-effort:7: DerivedGen.B[0(n), 1] B2 - used final orde
8383
"<<DerivedGen.B2>>"
8484
[ var "<<DerivedGen.B2>>"
8585
.$ bindVar "^cons_fuel^"
86-
.$ ( var "Prelude.Types.plus"
87-
.$ (var "Prelude.Types.plus" .$ bindVar "a" .$ bindVar "b")
88-
.$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))
86+
.$ implicitTrue
8987
.$ (var "DerivedGen.A2" .$ bindVar "a" .$ bindVar "b")
9088
.= var "Test.DepTyCheck.Gen.label"
9189
.$ (var "fromString" .$ primVal (Str "DerivedGen.B2 (orders)"))

‎tests/derivation/least-effort/print/regression/undefined-tobedeceqed/DerivedGen.idr‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
module DerivedGen
2+
3+
import Deriving.DepTyCheck.Gen
4+
5+
import Data.Vect
6+
7+
%language ElabReflection
8+
9+
record C where
10+
constructor Mk
11+
len : Nat
12+
13+
data Each : {arity : _} -> (m : C) -> (vals : Vect arity (Fin m.len)) -> Type where
14+
Next : {m : C} -> {0 vals : Vect n _} -> {0 val : _} -> Each m (val :: vals)
15+
16+
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
17+
Fuel -> {arity : _} -> (m : C) -> (vals : Vect arity (Fin m.len)) -> Gen MaybeEmpty (Each m vals)

‎tests/derivation/least-effort/print/regression/undefined-tobedeceqed/derive.ipkg‎

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

0 commit comments

Comments
 (0)