Skip to content

Commit

Permalink
[ derive ] Take into account outgoing determinations in the priority
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden committed Oct 23, 2024
1 parent 72ab9c8 commit eeab7db
Show file tree
Hide file tree
Showing 6 changed files with 83 additions and 81 deletions.
9 changes: 7 additions & 2 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,10 +125,15 @@ Ord PriorityOrigin where

-- compute the priority
-- priority is a count of given arguments, and it propagates back using `max` on strongly determining arguments and on arguments that depend on this
propagatePri' : FinMap con.args.length (Determination con) -> FinMap con.args.length (Determination con, Nat, PriorityOrigin)
-- additionally we take into account the number of outgoing strong determinations and count of dependent arguments
propagatePri' : {con : _} -> FinMap con.args.length (Determination con) -> FinMap con.args.length (Determination con, Nat, PriorityOrigin, Nat, Nat)
propagatePri' dets = do
let invStrongDetPwr = do
let _ : Monoid Nat = Additive
flip concatMap dets $ \det => fromList $ (,1) <$> det.stronglyDeterminingArgs.asList
let origPri = dets <&> \det => (det,) $ det.typeArgs `minus` det.argsDependsOn.size
map snd origPri `zip` propagatePri origPri <&> \(origPri, det, newPri) => (det, newPri, if origPri == newPri then Original else Propagated)
flip mapWithKey (map snd origPri `zip` propagatePri origPri) $ \idx, (origPri, det, newPri) =>
(det, newPri, if origPri == newPri then Original else Propagated, fromMaybe 0 $ Fin.Map.lookup idx invStrongDetPwr, det.argsDependsOn.size)

searchOrder : {con : _} ->
(determinable : SortedSet $ Fin con.args.length) ->
Expand Down
14 changes: 6 additions & 8 deletions tests/derivation/least-effort/print/john-hughes/004 rgen/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,18 +57,16 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel
.$ (var "fromString" .$ primVal (Str "DerivedGen.R (orders)"))
.$ ( var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "c") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "c") implicitFalse
.$ (var "<Data.So.So>[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.equalNat" .$ var "b" .$ var "c"))
.$ ( MkArg MW ExplicitArg (Just "bc") implicitFalse
.=> var ">>="
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ (var "Prelude.Types.equalNat" .$ var "b" .$ var "c"))
.$ ( MkArg MW ExplicitArg (Just "bc") implicitFalse
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "d") implicitFalse
Expand Down
4 changes: 2 additions & 2 deletions tests/derivation/least-effort/print/john-hughes/006 rgen/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,10 +57,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel
.$ (var "fromString" .$ primVal (Str "DerivedGen.R (orders)"))
.$ ( var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.=> var ">>="
.$ (var "<Data.So.So>[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.equalNat" .$ var "a" .$ var "b"))
.$ ( MkArg MW ExplicitArg (Just "ab") implicitFalse
Expand Down
49 changes: 24 additions & 25 deletions tests/derivation/least-effort/print/john-hughes/009 rgen/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,10 +57,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel
.$ (var "fromString" .$ primVal (Str "DerivedGen.R (orders)"))
.$ ( var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "b") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "a") implicitFalse
.=> var ">>="
.$ (var "<Data.So.So>[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.equalNat" .$ var "a" .$ var "b"))
.$ ( MkArg MW ExplicitArg (Just "ab") implicitFalse
Expand All @@ -72,47 +72,46 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel
.$ ( MkArg MW ExplicitArg (Just "bc") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "d") implicitFalse
.$ ( MkArg MW ExplicitArg (Just "f") implicitFalse
.=> var ">>="
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ (var "Prelude.Types.equalNat" .$ var "c" .$ var "d"))
.$ ( MkArg MW ExplicitArg (Just "cd") implicitFalse
.$ (var "Prelude.Types.equalNat" .$ var "a" .$ var "f"))
.$ ( MkArg MW ExplicitArg (Just "af") implicitFalse
.=> var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "e") implicitFalse
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ ( var "Prelude.Types.equalNat"
.$ var "f"
.$ ( var "Prelude.Types.S"
.$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))))
.$ ( MkArg MW ExplicitArg (Just "f2") implicitFalse
.=> var ">>="
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ (var "Prelude.Types.equalNat" .$ var "b" .$ var "e"))
.$ ( MkArg MW ExplicitArg (Just "be") implicitFalse
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "d") implicitFalse
.=> var ">>="
.$ ( var "external^<Prelude.Types.Nat>[]"
.$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "f") implicitFalse
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ (var "Prelude.Types.equalNat" .$ var "c" .$ var "d"))
.$ ( MkArg MW ExplicitArg (Just "cd") implicitFalse
.=> var ">>="
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ ( var "Prelude.Types.equalNat"
.$ var "a"
.$ var "f"))
.$ ( var "external^<Prelude.Types.Nat>[]"
.$ var "^outmost-fuel^")
.$ ( MkArg
MW
ExplicitArg
(Just "af")
(Just "e")
implicitFalse
.=> var ">>="
.$ ( var "<Data.So.So>[0]"
.$ var "^outmost-fuel^"
.$ ( var "Prelude.Types.equalNat"
.$ var "f"
.$ ( var "Prelude.Types.S"
.$ ( var "Prelude.Types.S"
.$ var "Prelude.Types.Z"))))
.$ var "b"
.$ var "e"))
.$ ( MkArg
MW
ExplicitArg
(Just "f2")
(Just "be")
implicitFalse
.=> var "Prelude.pure"
.! ( "f"
Expand Down
Loading

0 comments on commit eeab7db

Please sign in to comment.