Skip to content

Commit 431aaea

Browse files
buzdenbuzden
committed
[ relax ] Treat as weightable any type containing direct recursion
1 parent f4813fc commit 431aaea

File tree

4 files changed

+59
-54
lines changed

4 files changed

+59
-54
lines changed

‎deptycheck.ipkg

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ license = "MPL-2.0"
99
sourcedir = "src"
1010
builddir = ".build"
1111

12-
version = 0.0.250313
12+
version = 0.0.250317
1313

1414
modules = Deriving.DepTyCheck
1515
, Deriving.DepTyCheck.Gen

‎examples/sorted-tree-naive/tests/gens/sorted/expected

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,38 +3,38 @@ length: 5
33
as list: [2, 3, 4, 5, 6]
44
sorted: True
55
--------------
6-
length: 10
7-
as list: [0, 1, 2, 3, 5, 9, 10, 15, 22, 29]
6+
length: 8
7+
as list: [1, 2, 3, 5, 9, 10, 16, 18]
88
sorted: True
99
--------------
10-
length: 10
11-
as list: [0, 1, 2, 3, 4, 5, 10, 11, 13, 17]
10+
length: 0
11+
as list: []
1212
sorted: True
1313
--------------
1414
length: 0
1515
as list: []
1616
sorted: True
1717
--------------
18-
length: 9
19-
as list: [1, 2, 3, 4, 5, 9, 10, 11, 12]
18+
length: 8
19+
as list: [0, 1, 2, 3, 7, 9, 10, 17]
2020
sorted: True
2121
--------------
22-
length: 6
23-
as list: [6, 12, 14, 21, 27, 30]
22+
length: 9
23+
as list: [0, 1, 4, 5, 6, 7, 8, 12, 16]
2424
sorted: True
2525
--------------
26-
length: 9
27-
as list: [2, 3, 4, 5, 6, 13, 17, 22, 29]
26+
length: 8
27+
as list: [0, 1, 2, 3, 4, 7, 11, 18]
2828
sorted: True
2929
--------------
30-
length: 9
31-
as list: [0, 4, 5, 6, 7, 10, 11, 18, 24]
30+
length: 6
31+
as list: [0, 1, 2, 5, 6, 13]
3232
sorted: True
3333
--------------
34-
length: 8
35-
as list: [4, 5, 6, 7, 11, 12, 14, 17]
34+
length: 12
35+
as list: [0, 1, 2, 3, 6, 7, 8, 9, 10, 16, 23, 27]
3636
sorted: True
3737
--------------
38-
length: 0
39-
as list: []
38+
length: 8
39+
as list: [0, 1, 2, 5, 8, 9, 10, 16]
4040
sorted: True

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

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,10 @@ public export
242242
liftList : Foldable f => f TTImp -> TTImp
243243
liftList = foldr (\l, r => `(~l :: ~r)) `([])
244244

245+
public export
246+
liftList' : Foldable f => f TTImp -> TTImp
247+
liftList' = foldr (\l, r => `(Prelude.(::) ~l ~r)) `(Prelude.Nil)
248+
245249
export
246250
liftWeight1 : TTImp
247251
liftWeight1 = `(Data.Nat1.one)
@@ -795,27 +799,25 @@ getConsRecs = do
795799
consRecs <- for niit.types $ \targetType => logBounds {level=DetailedTrace} "consRec" [targetType] $ do
796800
crsForTy <- for targetType.cons $ \con => do
797801
tuneImpl <- search $ ProbabilityTuning con.name
798-
w : Either Nat1 (TTImp -> TTImp, Maybe $ SortedSet $ Fin con.args.length) <- case isRecursive {containingType=Just targetType} con of
799-
-- ^^^^^^^^^^^^^^ ^^^^^ ^^^^^^^^^^^^^^^ <- set of directly recursive constructor arguments
800-
-- | \-- `Just` in this `Maybe` means that this constructor only contains direct recursion (not mutual one)
802+
w : Either Nat1 (TTImp -> TTImp, SortedSet $ Fin con.args.length) <- case isRecursive {containingType=Just targetType} con of
803+
-- ^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^ <- set of directly recursive constructor arguments
801804
-- \------ Modifier of the standard weight expression
802805
False => pure $ Left $ maybe one (\impl => tuneWeight @{impl} one) tuneImpl
803806
True => Right <$> do
804807
fuelWeightExpr <- case tuneImpl of
805808
Nothing => pure id
806809
Just impl => quote (tuneWeight @{impl}) <&> \wm, expr => workaroundFromNat $ wm `applySyn` expr
807-
let directlyRec = filter (not . null) $ map (fromList . mapMaybe id) $ for con.args.withIdx $ \(idx, arg) => do
808-
case (== targetType.name) <$> getAppVar arg.type of
809-
Just True => Just $ Just idx
810-
_ => if hasNameInsideDeep targetType.name arg.type then Nothing else Just Nothing
811-
whenJust directlyRec $ \ars =>
812-
logPoint {level=DetailedTrace} "consRec" [targetType, con] "- directly recursive, rec args: \{show $ finToNat <$> ars.asList}"
813-
pure (fuelWeightExpr, directlyRec)
810+
let directlyRecArgs : List $ Fin con.args.length := flip mapMaybe con.args.withIdx $ \idxarg => do
811+
argTy <- getAppVar (snd idxarg).type
812+
whenT .| argTy == targetType.name .| fst idxarg
813+
when (not $ null directlyRecArgs) $
814+
logPoint {level=DetailedTrace} "consRec" [targetType, con] "- directly recursive args: \{show $ finToNat <$> directlyRecArgs}"
815+
pure (fuelWeightExpr, fromList directlyRecArgs)
814816
pure (con ** w)
815817
-- determine if this type is a nat-or-list-like data, i.e. one which we can measure for the probability
816-
let weightable = flip all crsForTy $ \case (_ ** Right (_, Nothing)) => False; _ => True
818+
let weightable = flip any crsForTy $ \case (_ ** Right (_, dra)) => not $ null dra; _ => False
817819
pure (toMaybe weightable targetType, crsForTy)
818-
let 0 _ : SortedMap Name (Maybe TypeInfo, List (con : Con ** Either Nat1 (TTImp -> TTImp, Maybe $ SortedSet $ Fin con.args.length))) := consRecs
820+
let 0 _ : SortedMap Name (Maybe TypeInfo, List (con : Con ** Either Nat1 (TTImp -> TTImp, SortedSet $ Fin con.args.length))) := consRecs
819821

820822
let weightableTyArgs : (ars : List Arg) -> SortedMap Nat (TypeInfo, Name) -- <- a map from Fin ars.length to a weightable type and its argument name
821823
weightableTyArgs ars = fromList $ flip List.mapMaybe ars.withIdx $ \(idx, ar) =>
@@ -853,7 +855,7 @@ getConsRecs = do
853855
let funSig = export' weightFunName $ piAll `(Data.Nat1.Nat1) $ map {piInfo := ImplicitArg} ty.args ++ [inTyArg]
854856

855857
let wClauses = cons <&> \(con ** e) => do
856-
let wArgs = either (const empty) (fromMaybe empty . snd) e
858+
let wArgs = either (const empty) snd e
857859
let lhsArgs : List (_, _) = mapI con.args $ \idx, arg => appArg arg <$> if contains idx wArgs
858860
then let bindName = "arg^\{show idx}" in (Just bindName, bindVar bindName)
859861
else (Nothing, implicitTrue)
@@ -862,7 +864,7 @@ getConsRecs = do
862864
patClause (var weightFunName .$ (reAppAny .| var con.name .| snd <$> lhsArgs)) $ case mapMaybe (map (UN . Basic) . fst) lhsArgs of
863865
[] => liftWeight1
864866
[x] => `(succ ~(callSelfOn x))
865-
xs => `(succ $ foldMap @{%search} @{Maximal} ~(liftList $ xs <&> callSelfOn))
867+
xs => `(succ $ Prelude.concat @{Maximum} ~(liftList' $ xs <&> callSelfOn))
866868

867869
pure (funSig, def weightFunName wClauses)
868870

‎tests/derivation/least-effort/print/regression/unnamed-auto-implicit-shallow/expected

Lines changed: 26 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,13 @@ LOG deptycheck.derive.least-effort:7: Builtin.Unit[] MkUnit - used final order:
88
.=> local
99
{ decls =
1010
[ IClaim
11+
(MkIClaimData
12+
{ rig = MW
13+
, vis = Export
14+
, opts = []
15+
, type = mkTy {name = "weight^DerivedGen.X", type = MkArg MW ExplicitArg Nothing (var "DerivedGen.X") .-> var "Data.Nat1.Nat1"}
16+
})
17+
, IClaim
1118
(MkIClaimData
1219
{ rig = MW
1320
, vis = Export
@@ -39,6 +46,13 @@ LOG deptycheck.derive.least-effort:7: Builtin.Unit[] MkUnit - used final order:
3946
.-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit"
4047
}
4148
})
49+
, IDef
50+
emptyFC
51+
"weight^DerivedGen.X"
52+
[ var "weight^DerivedGen.X" .$ var "DerivedGen.Nil" .= var "Data.Nat1.one"
53+
, var "weight^DerivedGen.X" .$ (var "DerivedGen.(::)" .$ implicitTrue .$ bindVar "arg^1" .@ implicitTrue)
54+
.= var "succ" .$ (var "weight^DerivedGen.X" .$ var "arg^1")
55+
]
4256
, IDef
4357
emptyFC
4458
"<DerivedGen.Y>[1]"
@@ -129,29 +143,18 @@ LOG deptycheck.derive.least-effort:7: Builtin.Unit[] MkUnit - used final order:
129143
]
130144
]
131145
, scope =
132-
iCase
133-
{ sc = var "^fuel_arg^"
134-
, ty = var "Data.Fuel.Fuel"
135-
, clauses =
136-
[ var "Data.Fuel.Dry"
137-
.= var "Test.DepTyCheck.Gen.label"
138-
.$ (var "fromString" .$ primVal (Str "DerivedGen.Y[1] (dry fuel)"))
139-
.$ (var "<<DerivedGen.A>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>")
140-
, var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^"
141-
.= var "Test.DepTyCheck.Gen.label"
142-
.$ (var "fromString" .$ primVal (Str "DerivedGen.Y[1] (non-dry fuel)"))
143-
.$ ( var "Test.DepTyCheck.Gen.frequency"
144-
.$ ( var "::"
145-
.$ ( var "Builtin.MkPair"
146-
.$ var "Data.Nat1.one"
147-
.$ (var "<<DerivedGen.A>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>"))
148-
.$ ( var "::"
149-
.$ ( var "Builtin.MkPair"
150-
.$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^")
151-
.$ (var "<<DerivedGen.B>>" .$ var "^sub^fuel_arg^" .$ var "inter^<{arg:1}>"))
152-
.$ var "Nil")))
153-
]
154-
}
146+
var "Test.DepTyCheck.Gen.label"
147+
.$ (var "fromString" .$ primVal (Str "DerivedGen.Y[1] (non-spending)"))
148+
.$ ( var "Test.DepTyCheck.Gen.frequency"
149+
.$ ( var "::"
150+
.$ ( var "Builtin.MkPair"
151+
.$ var "Data.Nat1.one"
152+
.$ (var "<<DerivedGen.A>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>"))
153+
.$ ( var "::"
154+
.$ ( var "Builtin.MkPair"
155+
.$ (var "weight^DerivedGen.X" .$ var "inter^<{arg:1}>")
156+
.$ (var "<<DerivedGen.B>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>"))
157+
.$ var "Nil")))
155158
}
156159
]
157160
, IDef

0 commit comments

Comments
 (0)