[ perf ] Use specialised type for set of fins

deptycheck.ipkg

@@ -11,7 +11,8 @@ builddir = ".build"
 
 version = 0.0.240909
 
-modules = Deriving.DepTyCheck
+modules = Data.Fin.Set
+        , Deriving.DepTyCheck
         , Deriving.DepTyCheck.Gen
         , Deriving.DepTyCheck.Gen.Derive
         , Deriving.DepTyCheck.Gen.Entry

src/Data/Fin/Set.idr

@@ -0,0 +1,140 @@
+-- This should be a replacement for `SortedSet (Fin n)` working better at least in elaborator scripts.
+module Data.Fin.Set
+
+import Data.List
+import Data.SortedMap
+import Data.String
+import Data.Vect
+import Data.Vect.Extra
+
+%default total
+
+export
+data FinSet : Nat -> Type where
+  MkFS : Vect n Bool -> FinSet n
+
+%inline
+unFS : FinSet n -> Vect n Bool
+unFS (MkFS bs) = bs
+
+export %inline
+empty : {n : _} -> FinSet n
+empty = MkFS $ replicate _ False
+
+export %inline
+full : {n : _} -> FinSet n
+full = MkFS $ replicate _ True
+
+export %inline
+complement : FinSet n -> FinSet n
+complement = MkFS . map not . unFS
+
+export %inline
+insert : Fin n -> FinSet n -> FinSet n
+insert n = MkFS . replaceAt n True . unFS
+
+export %inline
+insert' : FinSet n -> Fin n -> FinSet n
+insert' = flip insert
+
+export %inline
+delete : Fin n -> FinSet n -> FinSet n
+delete n = MkFS . replaceAt n False . unFS
+
+export %inline
+delete' : FinSet n -> Fin n -> FinSet n
+delete' = flip delete
+
+export %inline
+contains : Fin n -> FinSet n -> Bool
+contains i = index i . unFS
+
+export %inline
+contains' : FinSet n -> Fin n -> Bool
+contains' = flip contains
+
+-- much more effective implementation exists if we know that this foldable to sorted
+export %inline
+fromFoldable : Foldable f => {n : _} -> f (Fin n) -> FinSet n
+fromFoldable = foldl insert' empty
+
+export %inline
+fromList : {n : _} -> List (Fin n) -> FinSet n
+fromList = fromFoldable
+
+export %inline
+toList : FinSet n -> List (Fin n)
+toList = map snd . toListI . unFS
+
+public export %inline
+(.asList) : FinSet n -> List (Fin n)
+(.asList) = toList
+
+public export %inline
+size : FinSet n -> Nat
+size = length . toList -- this implementation is to make `asVect` work seamlessly
+--size = foldl (\n, b => if b then S n else n) 0 . unFS
+
+public export %inline
+(.size) : FinSet n -> Nat
+(.size) = size
+
+public export %inline
+(.asVect) : (fs : FinSet n) -> Vect fs.size (Fin n)
+(.asVect) fs = fromList $ toList fs
+
+export %inline
+union : FinSet n -> FinSet n -> FinSet n
+union = MkFS .: zipWith (\x, y => x || y) `on` unFS
+
+export %inline
+difference : FinSet n -> FinSet n -> FinSet n
+difference = MkFS .: zipWith (\l, r => l && not r) `on` unFS
+
+export %inline
+symDifference : FinSet n -> FinSet n -> FinSet n
+symDifference = MkFS .: zipWith (\l, r => l /= r) `on` unFS
+
+export %inline
+insersection : FinSet n -> FinSet n -> FinSet n
+insersection = MkFS .: zipWith (\x, y => x && y) `on` unFS
+
+export %inline
+leftMost : FinSet n -> Maybe $ Fin n
+leftMost = findIndex id . unFS
+
+export %inline
+rightMost : FinSet n -> Maybe $ Fin n
+rightMost = last' . findIndices id . unFS
+
+export
+Semigroup (FinSet n) where
+  (<+>) = union
+
+export
+{n : _} -> Monoid (FinSet n) where
+  neutral = empty
+
+export
+Interpolation (FinSet n) where
+  interpolate = ("{" ++) . (++ "}") . joinBy ", " . map show . Fin.Set.toList
+
+export
+null : FinSet n -> Bool
+null = all not . unFS
+
+export
+keySet : {n : _} -> SortedMap (Fin n) v -> FinSet n
+keySet = fromFoldable . map fst . SortedMap.toList
+-- we can employ the fact that given list is sorted
+
+export
+keySetSize : (m : SortedMap (Fin n) v) -> (keySet m).size = length (SortedMap.toList m)
+keySetSize _ = believe_me $ Refl {x=Z}
+
+export
+singleton : {n : _} -> Fin n -> FinSet n
+singleton = MkFS . go where
+  go : {n : _} -> Fin n -> Vect n Bool
+  go FZ     = True  :: replicate _ False
+  go (FS i) = False :: go i

src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr

@@ -21,7 +21,7 @@ import public Deriving.DepTyCheck.Gen.Derive
 
 public export
 interface ConstructorDerivator where
-  consGenExpr : CanonicGen m => GenSignature -> (con : Con) -> (given : SortedSet $ Fin con.args.length) -> (fuel : TTImp) -> m TTImp
+  consGenExpr : CanonicGen m => GenSignature -> (con : Con) -> (given : FinSet con.args.length) -> (fuel : TTImp) -> m TTImp
 
   ||| Workarond of inability to put an arbitrary name under `IBindVar`
   bindNameRenamer : Name -> String
@@ -33,11 +33,11 @@ interface ConstructorDerivator where
 record Determination (0 con : Con) where
   constructor MkDetermination
   ||| Args which cannot be determined by this arg, e.g. because it is used in a non-trivial expression.
-  stronglyDeterminingArgs : SortedSet $ Fin con.args.length
+  stronglyDeterminingArgs : FinSet con.args.length
   ||| Args which this args depends on, which are not strongly determining.
-  determinableArgs : SortedSet $ Fin con.args.length
+  determinableArgs : FinSet con.args.length
 
-mapDetermination : {0 con : Con} -> (SortedSet (Fin con.args.length) -> SortedSet (Fin con.args.length)) -> Determination con -> Determination con
+mapDetermination : {0 con : Con} -> (FinSet con.args.length -> FinSet con.args.length) -> Determination con -> Determination con
 mapDetermination f $ MkDetermination sda da = MkDetermination .| f sda .| f da
 
 -- If given foldable is sorted, this can be done linearly
@@ -87,7 +87,7 @@ searchOrder left' = do
   let curr = fst curr
 
   -- remove information about all currently chosen args
-  let next = removeDeeply .| Id curr .| removeDeeply determined left'
+  let next = removeDeeply .| Id curr .| removeDeeply (toList determined) left'
 
   -- `next` is smaller than `left` because `curr` must be not empty
   curr :: searchOrder (assert_smaller left' next)
@@ -227,7 +227,7 @@ namespace NonObligatoryExts
       logPoint {level=15} "least-effort" [sig, con] "- determ: \{determ}"
       logPoint {level=15} "least-effort" [sig, con] "- givs: \{givs}"
 
-      let theOrder = searchOrder $ removeDeeply givs determ
+      let theOrder = searchOrder $ removeDeeply (toList givs) determ
 
       logPoint {level=10} "least-effort" [sig, con] "- used final order: \{theOrder}"
 
@@ -259,14 +259,14 @@ namespace NonObligatoryExts
           MkTypeApp :
             (type : TypeInfo) ->
             (0 _ : AllTyArgsNamed type) =>
-            (determinedBy : SortedSet $ Fin con.args.length) ->
+            (determinedBy : FinSet con.args.length) ->
             (argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) ->
             TypeApp
 
-        argsDeterminedBy : TypeApp -> SortedSet $ Fin con.args.length
+        argsDeterminedBy : TypeApp -> FinSet con.args.length
         argsDeterminedBy $ MkTypeApp {determinedBy, _} = determinedBy
 
-        argsCanDetermine : TypeApp -> SortedSet $ Fin con.args.length
+        argsCanDetermine : TypeApp -> FinSet con.args.length
         argsCanDetermine $ MkTypeApp {argTypes, determinedBy, _} = fromList (lefts argTypes.asList) `difference` determinedBy
 
   ||| Best effort non-obligatory tactic tries to use as much external generators as possible

src/Deriving/DepTyCheck/Gen/Derive.idr

@@ -3,9 +3,10 @@ module Deriving.DepTyCheck.Gen.Derive
 
 import public Control.Monad.Error.Interface
 
+import public Data.Fin.Set
+
 import public Data.SortedMap
 import public Data.SortedMap.Dependent
-import public Data.SortedSet
 
 import public Deriving.DepTyCheck.Util.Reflection
 
@@ -20,17 +21,17 @@ record GenSignature where
   constructor MkGenSignature
   targetType : TypeInfo
   {auto 0 targetTypeCorrect : AllTyArgsNamed targetType}
-  givenParams : SortedSet $ Fin targetType.args.length
+  givenParams : FinSet targetType.args.length
 
 namespace GenSignature
 
   export
   characteristics : GenSignature -> (String, List Nat)
-  characteristics $ MkGenSignature ty giv = (show ty.name, toNatList giv)
+  characteristics $ MkGenSignature ty giv = (show ty.name, map finToNat $ toList giv)
 
 public export %inline
-(.generatedParams) : (sig : GenSignature) -> SortedSet $ Fin sig.targetType.args.length
-sig.generatedParams = fromList (allFins sig.targetType.args.length) `difference` sig.givenParams
+(.generatedParams) : (sig : GenSignature) -> FinSet sig.targetType.args.length
+sig.generatedParams = complement sig.givenParams
 
 export
 SingleLogPosition GenSignature where
@@ -60,7 +61,7 @@ CanonicGen m => MonadTrans t => Monad (t m) => CanonicGen (t m) where
 
 export
 canonicSig : GenSignature -> TTImp
-canonicSig sig = piAll returnTy $ MkArg MW ExplicitArg Nothing `(Data.Fuel.Fuel) :: (arg <$> SortedSet.toList sig.givenParams) where
+canonicSig sig = piAll returnTy $ MkArg MW ExplicitArg Nothing `(Data.Fuel.Fuel) :: (arg <$> toList sig.givenParams) where
   -- TODO Check that the resulting `TTImp` reifies to a `Type`? During this check, however, all types must be present in the caller's context.
 
   arg : Fin sig.targetType.args.length -> Arg