Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ derive ] Do not pass values of arguments on which someone else depends #199

Merged
merged 1 commit into from
Sep 17, 2024
Merged

[ derive ] Do not pass values of arguments on which someone else depends #199

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 21 additions & 15 deletions examples/covering-seq/tests/gens/print/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.$ ( MkArg MW ExplicitArg (Just "^bnd^{conArg:1}") implicitFalse
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "Data.List.Covering.End" .! ("n", var "n") .! ("bs", var "bs") .@ var "^bnd^{conArg:1}")))
.$ ( var "Data.List.Covering.End"
.! ("n", implicitTrue)
.! ("bs", implicitTrue)
.@ var "^bnd^{conArg:1}")))
]
, IDef
emptyFC
Expand All @@ -159,8 +162,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ ( var "Data.List.Covering.Miss"
.! ("n", var "n")
.! ("bs", var "bs")
.! ("n", implicitTrue)
.! ("bs", implicitTrue)
.$ var "^bnd^{arg:7}"
.$ var "^bnd^{arg:8}"))))
]
Expand Down Expand Up @@ -194,9 +197,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ ( var "Data.List.Covering.Hit"
.! ("n", var "n")
.! ("bs", var "bs")
.$ var "i"
.! ("n", implicitTrue)
.! ("bs", implicitTrue)
.$ implicitTrue
.@ var "^bnd^{conArg:2}"
.$ var "^bnd^{arg:9}")))))
]
Expand Down Expand Up @@ -320,7 +323,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.Here (orders)"))
.$ ( var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "Data.List.Covering.BitMask.Index.Here" .! ("n", var "n") .! ("bs", var "bs") .! ("b", var "b")))
.$ ( var "Data.List.Covering.BitMask.Index.Here"
.! ("n", implicitTrue)
.! ("bs", var "bs")
.! ("b", var "b")))
, var "<<Data.List.Covering.BitMask.Index.Here>>"
.$ bindVar "^cons_fuel^"
.$ (var "Prelude.Types.S" .$ bindVar "n")
Expand Down Expand Up @@ -362,10 +368,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ ( var "Data.List.Covering.BitMask.Index.There"
.! ("b", var "b")
.! ("v", var "v")
.! ("n", var "n")
.! ("bs", var "bs")
.! ("i", var "i")
.! ("v", implicitTrue)
.! ("n", implicitTrue)
.! ("bs", implicitTrue)
.! ("i", implicitTrue)
.$ var "^bnd^{arg:10}")))
, var "<<Data.List.Covering.BitMask.Index.There>>"
.$ implicitTrue
Expand Down Expand Up @@ -473,7 +479,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:11}") implicitFalse
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:11}")))
.$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:11}")))
, var "<<Data.Fin.FS>>" .$ implicitTrue .$ implicitTrue .= var "empty"
]
]
Expand Down Expand Up @@ -668,9 +674,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ ( var "Data.List.Covering.BitMask.Index.Continue"
.! ("n", var "n")
.! ("bs", var "bs")
.! ("b", var "b")
.! ("n", implicitTrue)
.! ("bs", implicitTrue)
.! ("b", implicitTrue)
.$ var "^bnd^{arg:13}")))
, var "<<Data.List.Covering.BitMask.Index.Continue>>"
.$ bindVar "^cons_fuel^"
Expand Down
18 changes: 9 additions & 9 deletions examples/sorted-list/tests/gens/print/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
.$ (var "Builtin.DPair.MkDPair" .$ bindVar "xs" .$ bindVar "^bnd^{conArg:1}")
.= var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "Data.List.Sorted.(::)" .$ var "x" .$ var "xs" .@ var "^bnd^{conArg:1}")
.$ (var "Data.List.Sorted.(::)" .$ implicitTrue .$ implicitTrue .@ var "^bnd^{conArg:1}")
]
}))
]
Expand Down Expand Up @@ -255,10 +255,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
.$ ( var "Builtin.DPair.MkDPair"
.$ implicitTrue
.$ ( var "Data.List.Sorted.NE"
.! ("xs", var "xs")
.! ("x", var "x")
.! ("xs", implicitTrue)
.! ("x", implicitTrue)
.! ("prf", var "prf")
.! ("n", var "n")
.! ("n", implicitTrue)
.$ var "^bnd^{arg:3}")))
]
})
Expand Down Expand Up @@ -367,10 +367,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
.$ ( var "Builtin.DPair.MkDPair"
.$ implicitTrue
.$ ( var "Data.List.Sorted.NE"
.! ("xs", var "xs")
.! ("x", var "x")
.! ("xs", implicitTrue)
.! ("x", implicitTrue)
.! ("prf", var "prf")
.! ("n", var "n")
.! ("n", implicitTrue)
.$ var "^bnd^{arg:3}"))
]
})
Expand Down Expand Up @@ -477,8 +477,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
.$ ( var "Builtin.DPair.MkDPair"
.$ implicitTrue
.$ ( var "Data.Nat.LTESucc"
.! ("right", var "right")
.! ("left", var "left")
.! ("right", implicitTrue)
.! ("left", implicitTrue)
.$ var "^bnd^{arg:4}"))
]
}))
Expand Down
21 changes: 11 additions & 10 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,12 +84,17 @@ namespace NonObligatoryExts
-- Compute left-to-right need of generation when there are non-trivial types at the left
argsTypeApps <- for con.args.asVect $ analyseTypeApp . type

-- Get dependencies of constructor's arguments
let rawDeps' = argDeps con.args
let rawDeps : Vect _ $ SortedSet $ Fin con.args.length := downmap (mapIn weakenToSuper) rawDeps'
let dependees = concat rawDeps -- arguments which any other argument depends on

-- Decide how constructor arguments would be named during generation
let bindNames = fromList con.args <&> bindNameRenamer . argName
let bindNames = withIndex (fromList con.args) <&> map (bindNameRenamer . argName)

-- Form the expression of calling the current constructor
let callCons = do
let constructorCall = callCon con $ bindNames <&> varStr
let constructorCall = callCon con $ bindNames <&> \(idx, n) => if contains idx dependees then implicitTrue else varStr n
let wrapImpls : Nat -> TTImp
wrapImpls Z = constructorCall
wrapImpls (S n) = var `{Builtin.DPair.MkDPair} .$ implicitTrue .$ wrapImpls n
Expand Down Expand Up @@ -140,7 +145,7 @@ namespace NonObligatoryExts
subgenCall <- callGen subsig subfuel $ snd <$> subgivens

-- Form an expression of binding the result of subgen
let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames
let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . snd . flip Vect.index bindNames
let bindSubgenResult = foldr (\l, r => var `{Builtin.DPair.MkDPair} .$ l .$ r) genedArg subgeneratedArgs

-- Form an expression of the RHS of a bind; simplify lambda if subgeneration result type does not require pattern matching
Expand All @@ -151,10 +156,6 @@ namespace NonObligatoryExts
-- Chain the subgen call with a given continuation
pure $ \cont => `(~subgenCall >>= ~(bindRHS cont))

-- Get dependencies of constructor's arguments
let rawDeps = argDeps con.args
let deps = downmap ((`difference` givs) . mapIn weakenToSuper) rawDeps

-------------------------------------------------
-- Left-to-right generation phase (2nd phase) ---
-------------------------------------------------
Expand All @@ -173,21 +174,21 @@ namespace NonObligatoryExts
-- Find rightmost arguments among `preLTR`
let depsLTR = SortedSet.fromList $
mapMaybe (\(ds, idx) => whenT .| contains idx preLTR && null ds .| idx) $
toListI $ deps <&> intersection preLTR
toListI $ rawDeps <&> intersection preLTR . (`difference` givs)

---------------------------------------------------------------------------------
-- Main right-to-left generation phase (3rd phase aka 2nd right-to-left phase) --
---------------------------------------------------------------------------------

-- Arguments that no other argument depends on
let rightmostArgs = fromFoldable {f=Vect _} range `difference` (givs `union` concat deps)
let rightmostArgs = fromFoldable {f=Vect _} range `difference` (givs `union` dependees)

---------------------------------------------------------------
-- Manage different possible variants of generation ordering --
---------------------------------------------------------------

-- Prepare info about which arguments are independent and thus can be ordered arbitrarily
let disjDeps = disjointDepSets rawDeps givs
let disjDeps = disjointDepSets rawDeps' givs

-- Acquire order(s) in what we will generate arguments
let allOrders = do
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/adt/007 right-to-left simple/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y
[ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:2}"
.= var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}")
.$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}")
]
}))
]
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/adt/008 right-to-left simple/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y
[ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:2}"
.= var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}")
.$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}")
]
}))
]
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/adt/009 left-to-right/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y
.$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}"))))
.$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}"))))
]
]
, scope =
Expand Down
5 changes: 4 additions & 1 deletion tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y
.$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}")
.= var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkY" .! ("m", var "m") .! ("n", var "n") .$ var "^bnd^{arg:3}")
.$ ( var "DerivedGen.MkY"
.! ("m", implicitTrue)
.! ("n", implicitTrue)
.$ var "^bnd^{arg:3}")
]
}))
]
Expand Down
5 changes: 4 additions & 1 deletion tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y
.$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}")
.= var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkY" .! ("m", var "m") .! ("n", var "n") .$ var "^bnd^{arg:3}")
.$ ( var "DerivedGen.MkY"
.! ("m", implicitTrue)
.! ("n", implicitTrue)
.$ var "^bnd^{arg:3}")
]
}))
]
Expand Down
Loading