Merge branch 'develop-update-arrays'. Close #36.

**Description**

Copilot currently supports reading values from streams of arrays, but
not changing them.

We'd like to be able to modify an array by adjusting the value at a
specific position.

**Type**

- Feature: new extension to the language.

**Additional context**

None.

**Requester**

- Ivan Perez

**Method to check presence of bug**

No applicable (not a bug).

**Expected result**

Copilot provides a mechanism to update elements in an array. The
following Dockerfile installs copilot and runs a file with struct update
operations, which it then links and compares against its expected
output, printing the message "Success" if the output matches the
expectation:

```
--- Dockerfile
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc g++ make libgmp3-dev
RUN apt-get install --yes pkg-config

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.4.8
RUN cabal update

ADD Arrays.hs /tmp/Arrays.hs
ADD main.c /tmp/main.c
ADD expected /tmp/expected

CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cabal v1-sandbox init \
    && cabal v1-install alex happy \
    && cabal v1-install copilot**/ \
    && cabal v1-exec -- runhaskell /tmp/Arrays.hs \
    && mv /tmp/main.c . \
    && gcc main.c arrays.c -o main \
    && ./main > actual \
    && diff actual /tmp/expected \
    && echo Success

--- Arrays.hs
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Copilot.Compile.C99
import Data.Type.Equality  as DE
import Language.Copilot

-- Sample values

arr :: Stream (Array 2 Float)
arr = [ array [1.0, 2.5]
      , array [2.5, 1.0]
      ]
   ++ arr

arr1 = (arr !! 1 =$ (+1)) !! 0 =$ (+100)

arr2 = arr1 !! 1 =$ ([0.0] ++)

spec :: Spec
spec = do
  trigger "arrays" true [arg arr2]

main :: IO ()
main = do
  spec' <- reify spec
  compile "arrays" spec'

--- main.c
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include "arrays.h"
#include "arrays_types.h"

void arrays( float* arrays_arg0
           ) {
  printf("%f %f\n"
        , arrays_arg0[0]
        , arrays_arg0[1]);
}

int main() {
  step();
  step();
  step();
  step();
}

--- expected
101.000000 0.000000
102.500000 3.500000
101.000000 2.000000
102.500000 3.500000
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-36
```

**Solution implemented**

Extend `copilot-language` to provide operations to modify values of
arrays in streams, with a syntax that is uniform for structs and arrays.

Extend `copilot-core`, `copilot-c99`, `copilot-theorem`,
`copilot-interpreter` and `copilot-prettyprinter` as needed.

Provide examples that demonstrate the new features.

Provide (!) alternative to (.!!) to make syntax uniform. Adjust examples
to use (!).

Hide (!!) in copilot-libraries, and provide an alternative (!!!).

**Further notes**

None.

copilot-c99/CHANGELOG

@@ -1,3 +1,6 @@
+2024-09-03
+        * Add support for array updates. (#36)
+
 2024-07-07
         * Version bump (3.20). (#522)
         * Add support for struct field updates. (#520)

copilot-c99/src/Copilot/Compile/C99/Expr.hs

@@ -13,9 +13,9 @@ import qualified Data.List.NonEmpty  as NonEmpty
 import qualified Language.C99.Simple as C
 
 -- Internal imports: Copilot
-import Copilot.Core ( Expr (..), Field (..), Op1 (..), Op2 (..), Op3 (..),
-                      Type (..), Value (..), accessorName, arrayElems,
-                      toValues, typeSize )
+import Copilot.Core ( Array, Expr (..), Field (..), Op1 (..), Op2 (..),
+                      Op3 (..), Type (..), Value (..), accessorName,
+                      arrayElems, toValues, typeLength, typeSize )
 
 -- Internal imports
 import Copilot.Compile.C99.Error ( impossible )
@@ -101,6 +101,47 @@ transExpr (Op2 op e1 e2) = do
   e2' <- transExpr e2
   return $ transOp2 op e1' e2'
 
+transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
+  e1' <- transExpr e1
+  e2' <- transExpr e2
+  e3' <- transExpr e3
+
+  -- Variable to hold the updated array
+  (i, _, _) <- get
+  let varName = "_v" ++ show i
+  modify (\(i, x, y) -> (i + 1, x, y))
+
+  -- Add new var decl
+  let initDecl = C.VarDecln Nothing cTy1 varName Nothing
+      cTy1     = transType arrTy
+  modify (\(i, x, y) -> (i, x ++ [initDecl], y))
+
+  let size :: Type (Array n t) -> C.Expr
+      size arrTy@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy)
+                         C..* C.SizeOfType (C.TypeName $ transType ty)
+
+  -- Initialize the var to the same value as the original array
+  let initStmt = C.Expr $ memcpy (C.Ident varName) e1' (size arrTy)
+
+  -- Update element of array
+  let updateStmt = case ty2 of
+        Array _ -> C.Expr $ memcpy dest e3' size
+          where
+            dest = C.Index (C.Ident varName) e2'
+            size = C.LitInt
+                       (fromIntegral $ typeSize ty2)
+                       C..* C.SizeOfType (C.TypeName (tyElemName ty2))
+
+        _ -> C.Expr
+           $ C.AssignOp
+                 C.Assign
+                 (C.Index (C.Ident varName) e2')
+                 e3'
+
+  modify (\(i, x, y) -> (i, x, y ++ [ initStmt, updateStmt ]))
+
+  return $ C.Ident varName
+
 transExpr (Op3 op e1 e2 e3) = do
   e1' <- transExpr e1
   e2' <- transExpr e2
@@ -179,7 +220,8 @@ transOp2 op e1 e2 = case op of
 -- expression.
 transOp3 :: Op3 a b c d -> C.Expr -> C.Expr -> C.Expr -> C.Expr
 transOp3 op e1 e2 e3 = case op of
-  Mux _ -> C.Cond e1 e2 e3
+  Mux         _ -> C.Cond e1 e2 e3
+  UpdateArray _ -> impossible "transOp3" "copilot-c99"
 
 -- | Translate @'Abs' e@ in Copilot Core into a C99 expression.
 --

copilot-core/CHANGELOG

@@ -1,3 +1,6 @@
+2024-09-03
+        * 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)

copilot-core/src/Copilot/Core/Operators.hs

@@ -106,3 +106,6 @@ data Op2 a b c where
 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.

copilot-core/src/Copilot/Core/Type/Array.hs

@@ -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 @@ module Copilot.Core.Type.Array
     ( 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 @@ array xs | datalen == typelen = Array xs
 -- | 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)

copilot-interpreter/CHANGELOG

@@ -1,3 +1,6 @@
+2024-09-03
+        * Add support for array updates. (#36)
+
 2024-07-07
         * Version bump (3.20). (#522)
         * Add support for struct field updates. (#520)

copilot-interpreter/src/Copilot/Interpret/Eval.hs

@@ -19,8 +19,8 @@ module Copilot.Interpret.Eval
 import Copilot.Core            (Expr (..), Field (..), Id, Name, Observer (..),
                                 Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
                                 Trigger (..), Type (..), UExpr (..), Value (..),
-                                arrayElems, specObservers, specStreams,
-                                specTriggers, updateField)
+				arrayElems, arrayUpdate, specObservers,
+                                specStreams, specTriggers, updateField)
 import Copilot.Interpret.Error (badUsage)
 
 import           Prelude hiding (id)
@@ -32,6 +32,7 @@ import Data.Dynamic      (Dynamic, fromDynamic, toDyn)
 import Data.List         (transpose)
 import Data.Maybe        (fromJust)
 import Data.Typeable     (Typeable)
+import GHC.TypeLits      (KnownNat, Nat, natVal)
 
 -- | Exceptions that may be thrown during interpretation of a Copilot
 -- specification.
@@ -265,7 +266,8 @@ catchZero f x y = f x y
 -- Haskell function operating on the same types as the
 -- 'Copilot.Core.Operators.Op3'.
 evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
-evalOp3 (Mux _) = \ !v !x !y -> if v then x else y
+evalOp3 (Mux         _)  = \ !v !x !y -> if v then x else y
+evalOp3 (UpdateArray ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x
 
 -- | Turn a stream into a key-value pair that can be added to an 'Env' for
 -- simulation.

copilot-language/CHANGELOG

@@ -1,3 +1,6 @@
+2024-09-03
+        * Add support for array updates. (#36)
+
 2024-07-07
         * Version bump (3.20). (#522)
         * Remove deprecated function Copilot.Language.Spec.forall. (#518)

copilot-language/copilot-language.cabal

@@ -61,6 +61,7 @@ library
                  , Copilot.Language.Operators.Ord
                  , Copilot.Language.Operators.Temporal
                  , Copilot.Language.Operators.Array
+                 , Copilot.Language.Operators.Projection
                  , Copilot.Language.Operators.Struct
                  , Copilot.Language.Prelude
                  , Copilot.Language.Reify

copilot-language/src/Copilot/Language/Operators/Array.hs

@@ -1,29 +1,89 @@
-{-# LANGUAGE Safe         #-}
-
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe                  #-}
+{-# LANGUAGE TypeFamilies          #-}
+-- The following warning is disabled due to a necessary instance of Projectable
+-- defined in this module.
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- | Combinators to deal with streams carrying arrays.
 module Copilot.Language.Operators.Array
   ( (.!!)
+  , (!)
+  , (!!)
+  , (=:)
+  , (=$)
   ) where
 
-import Copilot.Core             ( Typed
-                                , Op2 (Index)
-                                , typeOf
-                                , Array
-                                )
-import Copilot.Language.Stream  (Stream (..))
+import Copilot.Core                          (Array, Op2 (Index),
+                                              Op3 (UpdateArray), Typed, typeOf)
+import Copilot.Language.Operators.Projection (Projectable(..))
+import Copilot.Language.Stream               (Stream (..))
+
+import Data.Word    (Word32)
+import GHC.TypeLits (KnownNat)
+import Prelude      hiding ((!!))
 
-import Data.Word                (Word32)
-import GHC.TypeLits             (KnownNat)
+-- | Create a stream that carries an element of an array in another stream.
+--
+-- This function implements a projection of the element of an array at a given
+-- position, over time. For example, if @s@ is a stream of type @Stream (Array
+-- '5 Word8)@, then @s ! 3@ has type @Stream Word8@ and contains the 3rd
+-- element (starting from zero) of the arrays in @s@ at any point in time.
+(!) :: (KnownNat n, Typed t)
+    => Stream (Array n t) -> Stream Word32 -> Stream t
+arr ! n = Op2 (Index typeOf) arr n
 
 -- | Create a stream that carries an element of an array in another stream.
 --
 -- This function implements a projection of the element of an array at a given
 -- position, over time. For example, if @s@ is a stream of type @Stream (Array
 -- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd
 -- element (starting from zero) of the arrays in @s@ at any point in time.
+{-# DEPRECATED (.!!) "This function is deprecated in Copilot 4. Use (!)." #-}
 (.!!) :: ( KnownNat n
          , Typed t
          ) => Stream (Array n t) -> Stream Word32 -> Stream t
-arr .!! n = Op2 (Index typeOf) arr n
+(.!!) = (!)
+
+-- | Pair a stream with an element accessor, without applying it to obtain the
+-- value of the element.
+--
+-- This function is needed to refer to an element accessor when the goal is to
+-- update the element value, not just to read it.
+(!!) :: Stream (Array n t)
+     -> Stream Word32
+     -> Projection (Array n t) (Stream Word32) t
+(!!) = ProjectionA
+
+-- | Update a stream of arrays.
+
+-- This is an orphan instance; we suppress the warning that GHC would
+-- normally produce with a GHC option at the top.
+instance (KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t where
+
+  -- | A projection of an element of a stream of arrays.
+  data Projection (Array n t) (Stream Word32) t =
+       ProjectionA (Stream (Array n t)) (Stream Word32)
+
+  -- | Create a stream where an element of an array has been updated with
+  -- values from another stream.
+  --
+  -- For example, if an array has two elements of type @Int32@, and @s@ is a
+  -- stream of such array type (@Stream (Array 2 Int32)@), and $v0$ is a stream
+  -- of type @Int32@, then @s !! 0 =: v0@ has type @Stream (Array 2 Int32)@ and
+  -- contains arrays where the value of the first element of each array is that
+  -- of @v0@ at each point in time, and the value of the second element in the
+  -- array is the same it had in @s@.
+  (=:) (ProjectionA s ix) v = Op3 (UpdateArray typeOf) s ix v
+
+  -- | Create a stream where an element of an array has been updated by
+  -- applying a stream function to it.
+  --
+  -- For example, if an array has two elements of type @Int32@, and @s@ is a
+  -- stream of such array type (@Stream (Array 2 Int32)@), and $f$ is function
+  -- of type @Stream Int32 -> Stream Int32@, then @s !! 0 =$ f@ has type
+  -- @Stream (Array 2 Int32)@ and contains arrays where the value of the first
+  -- element of each array is that of @f (s ! 0)@ at each point in time, and
+  -- the value of the second element in the array is the same it had in @s@.
+  (=$) (ProjectionA s ix) op = Op3 (UpdateArray typeOf) s ix (op (s ! ix))

copilot-language/src/Copilot/Language/Operators/Projection.hs

@@ -0,0 +1,38 @@
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies           #-}
+-- | Interface to access portions of a larger data structure.
+--
+-- Default operations to access elements from structs and arrays (e.g., a field
+-- of a struct, an element of an array) allow obtaining the values of those
+-- elements, but not modifying.
+--
+-- This module defines a common interface to manipulate portions of a larger
+-- data structure. We define the interface in a generic way, using a type
+-- class with two operations: one to set the value of the sub-element, and
+-- one to update the value of such element applying a stream function.
+module Copilot.Language.Operators.Projection
+    ( Projectable (..) )
+  where
+
+import Copilot.Language.Stream (Stream)
+
+infixl 8 =:
+infixl 8 =$
+
+-- | Common interface to manipulate portions of a larger data structure.
+--
+-- A projectable d s t means that it is possible to manipulate a sub-element s
+-- of type t carried in a stream of type d..
+class Projectable d s t | d s -> t where
+
+  -- | Unapplied projection or element access on a type.
+  data Projection d s t
+
+  -- | Modify the value of a sub-element of a type in a stream of elements
+  -- of that type.
+  (=:) :: Projection d s t -> Stream t -> Stream d
+
+  -- | Update the value of a sub-element of a type in a stream of elements of
+  -- that type, by applying a function on streams.
+  (=$) :: Projection d s t -> (Stream t -> Stream t) -> Stream d