Skip to content

Commit

Permalink
[ derive ] Do not pass values of arguments on which someone else depends
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden committed Sep 17, 2024
1 parent 1673170 commit d30cade
Show file tree
Hide file tree
Showing 68 changed files with 971 additions and 88 deletions.
36 changes: 21 additions & 15 deletions examples/covering-seq/tests/gens/print/expected
View file
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
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
22 changes: 12 additions & 10 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
View file
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 @@ -171,23 +172,24 @@ namespace NonObligatoryExts
let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR

-- Find rightmost arguments among `preLTR`
let depsNoGivs = (`difference` givs) <$> rawDeps
let depsLTR = SortedSet.fromList $
mapMaybe (\(ds, idx) => whenT .| contains idx preLTR && null ds .| idx) $
toListI $ deps <&> intersection preLTR
toListI $ depsNoGivs <&> intersection preLTR

---------------------------------------------------------------------------------
-- 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
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
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
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
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
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

0 comments on commit d30cade

Please sign in to comment.