packages feed

liquid-prelude 0.9.2.5 → 0.9.2.8.1

raw patch · 11 files changed

+11/−83 lines, 11 filesdep ~bytestringdep ~containersdep ~liquidhaskell

Dependency ranges changed: bytestring, containers, liquidhaskell

Files

liquid-prelude.cabal view
@@ -1,6 +1,6 @@ cabal-version:      1.24 name:               liquid-prelude-version:            0.9.2.5+version:            0.9.2.8.1 synopsis:           General utility modules for LiquidHaskell description:        General utility modules for LiquidHaskell. license:            BSD3@@ -25,13 +25,10 @@                     Language.Haskell.Liquid.Equational                     Language.Haskell.Liquid.Bag                     Language.Haskell.Liquid.ProofCombinators-                    KMeansHelper   hs-source-dirs:     src   build-depends:      base          < 5                     , ghc-prim                     , bytestring           >= 0.10.12.1 && < 0.12                     , containers           >= 0.6.4.1  && < 0.7-                    , liquidhaskell        >= 0.9.2.5+                    , liquidhaskell        >= 0.9.2.8   default-language:   Haskell2010-  if impl(ghc >= 8.10)-    ghc-options: -fplugin=LiquidHaskell
− src/KMeansHelper.hs 
@@ -1,78 +0,0 @@-module KMeansHelper where--import Prelude hiding (zipWith)-import Data.List (sort, span, minimumBy)-import Data.Function (on)-import Data.Ord (comparing)-import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)----- | Fixed-Length Lists--{-@ type List a N = {v : [a] | (len v) = N} @-}----- | N Dimensional Points--{-@ type Point N = List Double N @-}--{-@ type NonEmptyList a = {v : [a] | (len v) > 0} @-}---- | Clustering --{-@ type Clustering a  = [(NonEmptyList a)] @-}----------------------------------------------------------------------- | Grouping By a Predicate ----------------------------------------------------------------------------------------------------------{-@ groupBy       :: (a -> a -> Bool) -> [a] -> (Clustering a) @-}-groupBy _  []     =  []-groupBy eq (x:xs) =  (x:ys) : groupBy eq zs-  where (ys,zs)   = span (eq x) xs----------------------------------------------------------------------- | Partitioning By a Size -----------------------------------------------------------------------------------------------------------{-@ type PosInt = {v: Int | v > 0 } @-}--{-@ partition           :: size:PosInt -> xs:[a] -> (Clustering a) / [len xs] @-}--partition size []       = []-partition size ys@(_:_) = zs : partition size zs'-  where-    zs                  = take size ys-    zs'                 = drop size ys---------------------------------------------------------------------------- | Safe Zipping -------------------------------------------------------------------------------------------------------------------------------{-@ zipWith :: (a -> b -> c) -> xs:[a] -> (List b (len xs)) -> (List c (len xs)) @-}-zipWith f (a:as) (b:bs) = f a b : zipWith f as bs-zipWith _ [] []         = []---- Other cases only for exposition-zipWith _ (_:_) []      = liquidError "Dead Code"-zipWith _ [] (_:_)      = liquidError "Dead Code"---------------------------------------------------------------------------- | "Matrix" Transposition ---------------------------------------------------------------------------------------------------------------------{-@ type Matrix a Rows Cols  = (List (List a Cols) Rows) @-}--{-@ transpose                :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}--transpose                    :: Int -> Int -> [[a]] -> [[a]]-transpose 0 _ _              = []-transpose c r ((x:xs) : xss) = (x : map head xss) : transpose (c-1) r (xs : map tail xss)---- Or, with comprehensions--- transpose c r ((x:xs):xss) = (x : [ xs' | (x':_) <- xss ]) : transpose (c-1) r (xs : [xs' | (_ : xs') <- xss])---- Not needed, just for exposition-transpose c r ([] : _)       = liquidError "dead code"-transpose c r []             = liquidError "dead code"-
src/Language/Haskell/Liquid/Bag.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} module Language.Haskell.Liquid.Bag where  import qualified Data.Map      as M
src/Language/Haskell/Liquid/Equational.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} module Language.Haskell.Liquid.Equational where   -------------------------------------------------------------------------------
src/Language/Haskell/Liquid/Foreign.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# OPTIONS_GHC -fno-warn-unused-imports #-} {-# LANGUAGE MagicHash #-}
src/Language/Haskell/Liquid/List.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} module Language.Haskell.Liquid.List (transpose) where  {-@ lazy transpose @-}
src/Language/Haskell/Liquid/Prelude.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# LANGUAGE MagicHash      #-}  module Language.Haskell.Liquid.Prelude where
src/Language/Haskell/Liquid/ProofCombinators.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE TypeFamilies          #-}
src/Language/Haskell/Liquid/RTick.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}  -- -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
src/Language/Haskell/Liquid/RTick/Combinators.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}  -- -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
src/Language/Haskell/Liquid/String.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} -- Support for Strings for SMT   {-# LANGUAGE OverloadedStrings   #-}