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

[ performance ] Change the order of derivation, derive one strictly after another #85

Merged
merged 4 commits into from
Feb 14, 2024
Merged

[ performance ] Change the order of derivation, derive one strictly after another #85

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
ffa2386
[ refactor ] Prepare to queuing
buzden Sep 12, 2023
0079cf3
[ refactor ] Use queue instead of call stack to order the derivation
buzden Sep 12, 2023
58dcb11
[ fix ] Do not start loop too much
buzden Sep 13, 2023
d703c80
[ test ] Fix print golden values
buzden Sep 13, 2023
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
48 changes: 39 additions & 9 deletions src/Deriving/DepTyCheck/Gen/Checked.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ module Deriving.DepTyCheck.Gen.Checked
import public Control.Monad.Either
import public Control.Monad.Reader
import public Control.Monad.State
import public Control.Monad.State.Tuple
import public Control.Monad.Writer
import public Control.Monad.RWS

Expand Down Expand Up @@ -91,8 +92,10 @@ namespace ClojuringCanonicImpl
ClojuringContext : (Type -> Type) -> Type
ClojuringContext m =
( MonadReader (SortedMap GenSignature (ExternalGenSignature, Name)) m -- external gens
, MonadState (SortedMap GenSignature Name) m -- gens already asked to be derived
, MonadWriter (List Decl, List Decl) m -- function declarations and bodies
, MonadState (SortedMap GenSignature Name) m -- gens already asked to be derived
, MonadState (List (GenSignature, Name)) m -- queue of gens to be derived
, MonadState Bool m -- flat that there is a need to start derivation loop
, MonadWriter (List Decl, List Decl) m -- function declarations and bodies
)

nameForGen : GenSignature -> Name
Expand All @@ -110,6 +113,11 @@ namespace ClojuringCanonicImpl
DerivatorCore => ClojuringContext m => Elaboration m => CanonicGen m where
callGen sig fuel values = do

-- check if we are the first, then we need to start the loop
startLoop <- get {stateType=Bool}
-- say that no one needs any more startups, we are in charge
put False

-- look for external gens, and call it if exists
let Nothing = lookupLengthChecked sig !ask
| Just (name, Element extSig lenEq) => pure $ callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values
Expand All @@ -118,7 +126,7 @@ namespace ClojuringCanonicImpl
internalGenName <- do

-- look for existing (already derived) internals, use it if exists
let Nothing = lookup sig !get
let Nothing = SortedMap.lookup sig !get
| Just name => pure name

-- nothing found, then derive! acquire the name
Expand All @@ -127,23 +135,45 @@ namespace ClojuringCanonicImpl
-- remember that we're responsible for this signature derivation
modify $ insert sig name

-- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
(genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name

-- remember the derived stuff
tell ([genFunClaim], [genFunBody])
-- remember the task to derive
modify {stateType=List _} $ (::) (sig, name)

-- return the name of the newly derived generator
pure name

-- if we were first to start the derivation loop, then...
when startLoop $ do
-- start the derivation loop itself
deriveAll
-- we now are not in charge of the derivation loop, so reset the flag
put True

-- call the internal gen
pure $ callCanonic sig internalGenName fuel values

where

deriveOne : (GenSignature, Name) -> m ()
deriveOne (sig, name) = do

-- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
(genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name

-- remember the derived stuff
tell ([genFunClaim], [genFunBody])

deriveAll : m ()
deriveAll = do
toDerive <- get {stateType=List _}
put {stateType=List _} []
for_ toDerive deriveOne
when (not $ null toDerive) $ assert_total $ deriveAll

--- Canonic-dischagring function ---

export
runCanonic : DerivatorCore => SortedMap ExternalGenSignature Name -> (forall m. CanonicGen m => m a) -> Elab (a, List Decl)
runCanonic exts calc = do
let exts = SortedMap.fromList $ exts.asList <&> \namedSig => (fst $ internalise $ fst namedSig, namedSig)
(x, defs, bodies) <- evalRWST exts empty calc {s=SortedMap GenSignature Name} {w=(_, _)}
(x, defs, bodies) <- evalRWST exts (empty, empty, True) calc {s=(SortedMap GenSignature Name, List (GenSignature, Name), _)} {w=(_, _)}
pure (x, defs ++ bodies)
24 changes: 12 additions & 12 deletions tests/derivation/infra/ext print 004/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,34 +15,34 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
IClaim MW
Export
[]
(MkTy <Prelude.Types.Nat>[]
(MkTy <AlternativeCore.X'S>[0]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ IVar Prelude.Types.Nat)))
$ (IApp. IVar AlternativeCore.X'S
$ IVar {arg:5277}))))
IClaim MW
Export
[]
(MkTy <AlternativeCore.X'S>[0]
(MkTy <Prelude.Types.Nat>[]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ (IApp. IVar AlternativeCore.X'S
$ IVar {arg:5277}))))
IDef <Prelude.Types.Nat>[]
[ PatClause (IApp. IVar <Prelude.Types.Nat>[] $ IBindVar fuel)
$ IVar Prelude.Types.Nat)))
IDef <AlternativeCore.X'S>[0]
[ PatClause (IApp. IVar <AlternativeCore.X'S>[0]
$ IBindVar fuel
$ Implicit True)
(IApp. IVar <*>
$ (IApp. IVar <$>
$ IVar MkXSN
$ (IApp. IVar external^<^prim^.String>[]
$ IVar ^outmost-fuel^))
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar fuel)) ]
IDef <AlternativeCore.X'S>[0]
[ PatClause (IApp. IVar <AlternativeCore.X'S>[0]
$ IBindVar fuel
$ Implicit True)
IDef <Prelude.Types.Nat>[]
[ PatClause (IApp. IVar <Prelude.Types.Nat>[] $ IBindVar fuel)
(IApp. IVar <*>
$ (IApp. IVar <$>
$ IVar MkXSN
Expand Down
Loading