diff --git a/src/Deriving/DepTyCheck/Gen/Checked.idr b/src/Deriving/DepTyCheck/Gen/Checked.idr index f80f2fc43..577e4ee06 100644 --- a/src/Deriving/DepTyCheck/Gen/Checked.idr +++ b/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,10 +156,11 @@ 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 --- @@ -169,5 +168,5 @@ namespace ClojuringCanonicImpl 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)