Merge branch 'main' into Issue-3424

CHANGELOG_NEXT.md

@@ -95,6 +95,12 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Typst files can be compiled as Literate Idris
 
+* `min` was renamed to `leftMost` in `Libraries.Data.Sorted{Map|Set}` in order
+  to be defined as in `base`.
+
+* Reflected trees now make use of WithFC to replicate the new location tracking
+  in the compiler.
+
 ### Backend changes
 
 #### RefC Backend
@@ -240,6 +246,14 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added `Data.IORef.atomically` for the chez backend.
 
+* `Data.Nat.NonZero` was made to be an alias for `Data.Nat.IsSucc`.
+  `SIsNonZero` was made to be an alias for `ItIsSucc`, was marked as deprecated,
+  and won't work on LHS anymore.
+
+* Deprecated `toList` function in favor of `Prelude.toList` in `Data.SortedSet`.
+
+* Several functions like `pop`, `differenceMap` and `toSortedMap` were added to `Data.Sorted{Map|Set}`
+
 * Added `System.Concurrency.channelGetNonBlocking` for the chez backend.
 
 * Added `System.Concurrency.channelGetWithTimeout` for the chez backend.

libs/base/Data/Nat.idr

@@ -32,6 +32,9 @@ isSucc : Nat -> Bool
 isSucc Z     = False
 isSucc (S n) = True
 
+||| A definition of non-zero with a better behaviour than `Not (x = Z)`
+||| This is amenable to proof search and `NonZero Z` is more readily
+||| detected as impossible by Idris
 public export
 data IsSucc : (n : Nat) -> Type where
   ItIsSucc : IsSucc (S n)
@@ -45,6 +48,18 @@ isItSucc : (n : Nat) -> Dec (IsSucc n)
 isItSucc Z = No absurd
 isItSucc (S n) = Yes ItIsSucc
 
+||| A hystorical synonym for `IsSucc`
+public export
+0 NonZero : Nat -> Type
+NonZero = IsSucc
+
+-- Remove as soon as 0.8.0 (or greater) is released
+||| Use `ItIsSucc` instead
+public export %inline
+%deprecate
+SIsNonZero : NonZero (S n)
+SIsNonZero = ItIsSucc
+
 public export
 power : Nat -> Nat -> Nat
 power base Z       = S Z
@@ -319,15 +334,6 @@ export
 Injective S where
   injective Refl = Refl
 
-||| A definition of non-zero with a better behaviour than `Not (x = Z)`
-||| This is amenable to proof search and `NonZero Z` is more readily
-||| detected as impossible by Idris
-public export
-data NonZero : Nat -> Type where
-  SIsNonZero : NonZero (S x)
-
-export Uninhabited (NonZero Z) where uninhabited SIsNonZero impossible
-
 export
 SIsNotZ : Not (S x = Z)
 SIsNotZ = absurd
@@ -351,7 +357,7 @@ modNatNZ left (S right) _ = mod' left left right
 
 export partial
 modNat : Nat -> Nat -> Nat
-modNat left (S right) = modNatNZ left (S right) SIsNonZero
+modNat left (S right) = modNatNZ left (S right) ItIsSucc
 
 ||| Auxiliary function:
 ||| div' fuel a b = a `div` (S b)
@@ -372,7 +378,7 @@ divNatNZ left (S right) _ = div' left left right
 
 export partial
 divNat : Nat -> Nat -> Nat
-divNat left (S right) = divNatNZ left (S right) SIsNonZero
+divNat left (S right) = divNatNZ left (S right) ItIsSucc
 
 export
 covering
@@ -383,7 +389,7 @@ divCeilNZ x y p = case (modNatNZ x y p) of
 
 export partial
 divCeil : Nat -> Nat -> Nat
-divCeil x (S y) = divCeilNZ x (S y) SIsNonZero
+divCeil x (S y) = divCeilNZ x (S y) ItIsSucc
 
 
 public export
@@ -411,7 +417,7 @@ covering
 gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
 gcd a Z     = a
 gcd Z b     = b
-gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNonZero)
+gcd a (S b) = gcd (S b) (modNatNZ a (S b) ItIsSucc)
 
 export partial
 lcm : Nat -> Nat -> Nat

libs/base/Data/SortedMap.idr

@@ -189,6 +189,11 @@ rightMost : SortedMap key val -> Maybe (key,val)
 rightMost = map unDPair . rightMost . unM
 
 
+||| Pops the leftmost key and corresponding value from the map
+export
+pop : SortedMap k v -> Maybe ((k, v), SortedMap k v)
+pop = map (bimap unDPair M) . pop . unM
+
 export
 (Show k, Show v) => Show (SortedMap k v) where
    show m = "fromList " ++ (show $ toList m)

libs/base/Data/SortedMap/Dependent.idr

@@ -451,6 +451,13 @@ rightMost : SortedDMap k v -> Maybe (x : k ** v x)
 rightMost Empty = Nothing
 rightMost (M _ t) = Just $ treeRightMost t
 
+||| Pops the leftmost key and corresponding value from the map
+export
+pop : SortedDMap k v -> Maybe ((x : k ** v x), SortedDMap k v)
+pop m = do
+  kv@(k ** _) <- leftMost m
+  pure (kv, delete k m)
+
 export
 (Show k, {x : k} -> Show (v x)) => Show (SortedDMap k v) where
    show m = "fromList " ++ (show $ toList m)

libs/base/Data/SortedSet.idr

@@ -4,8 +4,6 @@ import Data.Maybe
 import Data.SortedMap
 import Data.SortedMap.Dependent
 
-%hide Prelude.toList
-
 export
 data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
 
@@ -41,18 +39,23 @@ export
 fromList : Ord k => List k -> SortedSet k
 fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
 
-export
-toList : SortedSet k -> List k
-toList (SetWrapper m) = keys m
-
 export
 Foldable SortedSet where
-  foldr f z = foldr f z . Data.SortedSet.toList
-  foldl f z = foldl f z . Data.SortedSet.toList
+  foldr f z = foldr f z . toList
+  foldl f z = foldl f z . toList
 
   null (SetWrapper m) = null m
 
-  foldMap f = foldMap f . Data.SortedSet.toList
+  foldMap f = foldMap f . toList
+
+  toList (SetWrapper m) = keys m
+
+-- Remove as soon as 0.8.0 (or greater) is released
+||| Use `Prelude.toList` instead
+%deprecate
+public export %inline
+toList : SortedSet k -> List k
+toList = Prelude.toList
 
 ||| Set union. Inserts all elements of x into y
 export
@@ -98,7 +101,7 @@ Eq k => Eq (SortedSet k) where
 
 export
 Show k => Show (SortedSet k) where
-   show m = "fromList " ++ (show $ toList m)
+   show m = "fromList " ++ show (Prelude.toList m)
 
 export
 keySet : SortedMap k v -> SortedSet k
@@ -110,6 +113,29 @@ namespace Dependent
   keySet : SortedDMap k v -> SortedSet k
   keySet = SetWrapper . cast . map (const ())
 
+||| Removes all given keys from the given map
+export
+differenceMap : SortedMap k v -> SortedSet k -> SortedMap k v
+differenceMap x y = foldr delete x y
+
+||| Leaves only given keys in the given map
+export
+intersectionMap : SortedMap k v -> SortedSet k -> SortedMap k v
+intersectionMap x y = differenceMap x (keySet $ differenceMap x y)
+
 export
 singleton : Ord k => k -> SortedSet k
 singleton = insert' empty
+
+export %inline
+toSortedMap : SortedSet k -> SortedMap k ()
+toSortedMap (SetWrapper m) = m
+
+export %inline
+fromSortedMap : SortedMap k () -> SortedSet k
+fromSortedMap = SetWrapper
+
+||| Pops the leftmost element from the set
+export
+pop : SortedSet k -> Maybe (k, SortedSet k)
+pop (SetWrapper m) = bimap fst fromSortedMap <$> pop m

libs/base/Deriving/Foldable.idr

@@ -371,7 +371,7 @@ namespace Foldable
     let b = un $ freshName paramNames "b"
     let va = IVar fc a
     let vb = IVar fc b
-    let ty = MkTy fc fc foldMapName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC foldMapName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ `(Monoid ~(vb) => (~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(vb))
@@ -381,7 +381,7 @@ namespace Foldable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc foldMapName cls
       ] `(fromFoldMap ~(t) ~(IVar fc foldMapName))
 

libs/base/Deriving/Functor.idr

@@ -382,7 +382,7 @@ namespace Functor
       , "Bifunctors: \{show ns.asBifunctors}"
       , "Parameters: \{show (map (mapFst unArg) params)}"
       ]
-    let ty = MkTy fc fc mapName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC mapName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ `((~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(t) ~(vb))
@@ -392,7 +392,7 @@ namespace Functor
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc mapName cls
       ] `(MkFunctor {f = ~(t)} ~(IVar fc mapName))
 

libs/base/Deriving/Show.idr

@@ -264,15 +264,15 @@ namespace Show
             ])
 
     -- Generate the type of the show function
-    let ty = MkTy fc fc showName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC showName) $ withParams fc (paramConstraints ns) params
            $ `(Prec -> ~(t) -> String)
     logMsg "derive.show.clauses" 1 $
       joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
                       :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc showName cls
       ] `(fromShowPrec ~(IVar fc showName))
 

libs/base/Deriving/Traversable.idr

@@ -395,7 +395,7 @@ namespace Traversable
     let va = IVar fc a
     let vb = IVar fc b
     let vf = IVar fc f
-    let ty = MkTy fc fc traverseName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC traverseName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ IPi fc M0 ImplicitArg (Just f) (IPi fc MW ExplicitArg Nothing (IType fc) (IType fc))
@@ -406,7 +406,7 @@ namespace Traversable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc traverseName cls
       ] `(MkTraversable {t = ~(t)} ~(IVar fc traverseName))
 

libs/base/Language/Reflection/TT.idr

@@ -68,6 +68,41 @@ public export
 emptyFC : FC
 emptyFC = EmptyFC
 
+------------------------------------------------------------------------
+||| A wrapper for a value with a file context.
+public export
+record WithFC (ty : Type) where
+  constructor MkFCVal
+  fc : FC
+  value : ty
+
+||| Smart constructor for WithFC that uses EmptyFC as location
+%inline export
+NoFC : a -> WithFC a
+NoFC = MkFCVal EmptyFC
+
+export
+Functor WithFC where
+  map f = { value $= f}
+
+export
+Foldable WithFC where
+  foldr f i v = f v.value i
+
+export
+Traversable WithFC where
+  traverse f (MkFCVal fc val) = map (MkFCVal fc) (f val)
+
+||| Locations are not taken into account when comparing reflected trees
+export
+Eq a => Eq (WithFC a) where
+  x == y = x.value == y.value
+
+||| Locations are not taken into account when comparing reflected trees
+export
+Ord a => Ord (WithFC a) where
+  compare x y = compare x.value y.value
+
 public export
 data NameType : Type where
      Bound   : NameType