copilot-core 3.20 → 4.0

raw patch · 4 files changed

+29/−2 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• copilot-core.cabal +1/−1
• src/Copilot/Core/Operators.hs +3/−0
• src/Copilot/Core/Type/Array.hs +21/−1

@@ -1,3 +1,7 @@+2024-09-07+        * Version bump (4.0). (#532)+        * Update Op3, Array to support array updates. (#36)+ 2024-07-07         * Version bump (3.20). (#522)         * Update Op2, Struct to support struct field updates. (#520)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.20+version:             4.0 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.

@@ -106,3 +106,6 @@ data Op3 a b c d where   -- Conditional operator.   Mux :: Type a -> Op3 Bool a a a+  -- Array operator.+  UpdateArray :: Type (Array n t) -> Op3 (Array n t) Word32 t (Array n t)+           -- ^ Update an element of an array.

@@ -3,6 +3,7 @@ {-# LANGUAGE Safe                #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeOperators       #-}  -- | -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -14,12 +15,13 @@     ( Array     , array     , arrayElems+    , arrayUpdate     )   where  -- External imports import Data.Proxy   (Proxy (..))-import GHC.TypeLits (KnownNat, Nat, natVal)+import GHC.TypeLits (KnownNat, Nat, natVal, type(-))  -- | Implementation of an array that uses type literals to store length. data Array (n :: Nat) t where@@ -42,3 +44,21 @@ -- | Return the elements of an array. arrayElems :: Array n a -> [a] arrayElems (Array xs) = xs++-- | Update element of array to given element.+--+-- PRE: the second argument denotes a valid index in the array.+arrayUpdate :: Array n a -> Int -> a -> Array n a+arrayUpdate (Array []) _ _ = error errMsg+  where+    errMsg = "copilot-core: arrayUpdate: Attempt to update empty array"++arrayUpdate (Array (x:xs)) 0 y = Array (y:xs)++arrayUpdate (Array (x:xs)) n y =+    arrayAppend x (arrayUpdate (Array xs) (n - 1) y)+  where+    -- | Append to an array while preserving length information at the type+    -- level.+    arrayAppend :: a -> Array (n - 1) a -> Array n a+    arrayAppend x (Array xs) = Array (x:xs)