[ wip ] Manage all present derivation demands at once

src/Deriving/DepTyCheck/Gen/Checked.idr

@@ -10,8 +10,6 @@ import public Control.Monad.RWS
 
 import public Data.DPair
 import public Data.Vect.Extra
-import public Data.Seq.Internal
-import public Data.Seq.Unsized as SU
 import public Data.SortedMap as M
 import public Data.SortedSet as S
 
@@ -95,7 +93,7 @@ namespace ClojuringCanonicImpl
   ClojuringContext m =
     ( MonadReader (SortedMap GenSignature (ExternalGenSignature, Name)) m -- external gens
     , MonadState  (SortedMap GenSignature Name) m -- gens already asked to be derived
-    , MonadState  (Seq (GenSignature, Name)) m -- queue of gens to be derived
+    , MonadState  (List (GenSignature, Name)) m -- queue of gens to be derived
     , MonadWriter (List Decl, List Decl) m -- function declarations and bodies
     )
 
@@ -115,7 +113,7 @@ namespace ClojuringCanonicImpl
     callGen sig fuel values = do
 
       -- check if we are the first, then we need to start the loop
-      let startLoop = null !(get {stateType=Seq _})
+      let startLoop = null !(get {stateType=List _})
 
       -- look for external gens, and call it if exists
       let Nothing = lookupLengthChecked sig !ask
@@ -135,7 +133,7 @@ namespace ClojuringCanonicImpl
         modify $ insert sig name
 
         -- remember the task to derive
-        modify $ SU.cons (sig, name)
+        modify $ (::) (sig, name)
 
         -- return the name of the newly derived generator
         pure name
@@ -158,16 +156,17 @@ namespace ClojuringCanonicImpl
           tell ([genFunClaim], [genFunBody])
 
         deriveAll : m ()
-        deriveAll = whenJust !(gets viewr) $ \(rest, curr) => do
-          deriveOne curr
-          put rest
-          assert_total deriveAll
+        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, empty) calc {s=(SortedMap GenSignature Name, Seq (GenSignature, Name))} {w=(_, _)}
+    (x, defs, bodies) <- evalRWST exts (empty, empty) calc {s=(SortedMap GenSignature Name, List (GenSignature, Name))} {w=(_, _)}
     pure (x, defs ++ bodies)