[ performance ] Change the order of derivation, derive one strictly a…

…fter another

src/Deriving/DepTyCheck/Gen/Checked.idr

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

tests/derivation/infra/ext print 004/expected

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