Merge branch 'develop-update-structs'. Close #520.

**Description**

Copilot currently supports reading values from fields of structs, but
not changing them.

We'd like to be able to modify a struct by adjusting the values of
specific fields.

**Type**

- Feature: new extension to the language.

**Additional context**

None.

**Requester**

- Ivan Perez

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Copilot provides a mechanism to update the field of a struct. 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 Structs.hs /tmp/Structs.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/Structs.hs \
    && mv /tmp/main.c . \
    && gcc main.c structs.c -o main \
    && ./main > actual \
    && diff actual /tmp/expected \
    && echo Success

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

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

-- * Struct type definitions

data SoA = SoA
  { arr :: Field "arr" SoB
  }

instance Struct SoA where
  typeName _ = "soa"
  toValues soa = [Value typeOf (arr soa)]

instance Typed SoA where
  typeOf = Struct $ SoA $ Field undefined

data SoB = SoB
  { arr2 :: Field "arr2" (Array 3 Float)
  }

instance Struct SoB where
  typeName _ = "sob"
  toValues sob = [Value typeOf (arr2 sob)]

instance Typed SoB where
  typeOf = Struct $ SoB $ Field undefined

data SoC = SoC
  { arr3 :: Field "arr3" Int32
  }

-- | Struct with a custom value for updates
instance Struct SoC where
  typeName _ = "soc"
  toValues soc = [Value typeOf (arr3 soc)]
  updateField s (Value ty f@(Field v)) =
    case fieldName f of
      "arr3" -> case testEquality ty Int32 of
                  Just DE.Refl -> s { arr3 = Field v }
                  _            -> error "The value provided for arr3 does not have type Int32"
      _      -> error "The field name provided does not exist in SoC"

instance Typed SoC where
  typeOf = Struct $ SoC $ Field undefined

-- Sample values

-- We purposefully leave some type signatures out to check that GHC can infer
-- them.

-- SoAs
a1 = SoA $ Field $ SoB $ Field $ array [0, 1, 2]
b1 = SoB $ Field $ array [10, 20, 30]
b2 = SoB $ Field $ array [40, 50, 60]
c1 = SoC $ Field 5

soa :: Stream SoA
soa = constant a1

soa1  = soa ## arr =: recursiveArray
soa2  = soa ## arr =: constant b1
soarr = soa ## arr =: soa # arr
soc1   = constant c1 ## arr3 =: counter
soc2   = constant c1 ## arr3 =$ (+5)

recursiveArray :: Stream SoB
recursiveArray = [b1, b2] ++ recursiveArray

counter :: Stream Int32
counter = [55] ++ (counter + 1)

spec :: Spec
spec = do
  trigger "arrays" (soa1 # arr # arr2 .!! 1 /= 60) [arg soa, arg soa1, arg soa2]
  trigger "arrays2" true [arg soc1]
  trigger "arrays3" true [arg soc2]

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

--- main.c
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include "structs.h"
#include "structs_types.h"

void arrays( struct soa * arrays_arg0
           , struct soa * arrays_arg1
           , struct soa * arrays_arg2
           ) {
  printf("0: %f %f %f\n"
        , arrays_arg0->arr.arr2[0]
        , arrays_arg0->arr.arr2[1]
        , arrays_arg0->arr.arr2[2]);

  printf("1: %f %f %f\n"
        , arrays_arg1->arr.arr2[0]
        , arrays_arg1->arr.arr2[1]
        , arrays_arg1->arr.arr2[2]);

  printf("2: %f %f %f\n"
        , arrays_arg2->arr.arr2[0]
        , arrays_arg2->arr.arr2[1]
        , arrays_arg2->arr.arr2[2]);
}

void arrays2(struct soc * arrays2_arg0) {
  printf("soc1: %d\n", arrays2_arg0->arr3);
}

void arrays3(struct soc * arrays2_arg0) {
  printf("soc2: %d\n", arrays2_arg0->arr3);
}

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

--- expected
0: 0.000000 1.000000 2.000000
1: 10.000000 20.000000 30.000000
2: 10.000000 20.000000 30.000000
soc1: 55
soc2: 10
0: 0.000000 1.000000 2.000000
1: 40.000000 50.000000 60.000000
2: 10.000000 20.000000 30.000000
soc1: 56
soc2: 10
0: 0.000000 1.000000 2.000000
1: 10.000000 20.000000 30.000000
2: 10.000000 20.000000 30.000000
soc1: 57
soc2: 10
0: 0.000000 1.000000 2.000000
1: 40.000000 50.000000 60.000000
2: 10.000000 20.000000 30.000000
soc1: 58
soc2: 10
```

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-520
```

**Solution implemented**

Extend `copilot-language` to provide operations to modify fields of
structs, and adjust `copilot-core`, `copilot-c99` and
`copilot-interpreter` to support such operations.

**Further notes**

We choose to temporarily limit the operation to values of fields that
can be Shown, due to an overlapping instance for Show that it is
difficult to avoid. We will revisit this point in the future.

Author: ivanperez-keera

copilot-c99/CHANGELOG

@@ -1,3 +1,6 @@
+2024-07-07
+        * Add support for struct field updates. (#520)
+
 2024-05-07
         * Version bump (3.19.1). (#512)
 

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

@@ -121,11 +121,13 @@ mkAccessDecln sId ty xs =
 -- | Write a generator function for a stream.
 mkGenFun :: String -> Expr a -> Type a -> C.FunDef
 mkGenFun name expr ty =
-    C.FunDef static cTy name [] cVars [C.Return $ Just cExpr]
+    C.FunDef static cTy name [] cVars stmts
   where
-    static         = Just C.Static
-    cTy            = C.decay $ transType ty
-    (cExpr, cVars) = runState (transExpr expr) mempty
+    static             = Just C.Static
+    cTy                = C.decay $ transType ty
+    (cExpr, state')    = runState (transExpr expr) (0, mempty, mempty)
+    (_, cVars, stmts') = state'
+    stmts              = stmts' ++ [C.Return $ Just cExpr]
 
 -- | Write a generator function for a stream that returns an array.
 mkGenFunArray :: String -> String -> Expr a -> Type a -> C.FunDef
@@ -139,13 +141,20 @@ mkGenFunArray name nameArg expr ty@(Array _) =
     outputParam = C.Param cArrayType nameArg
     cArrayType  = transType ty
 
-    -- Output value, and any variable declarations needed
-    (cExpr, varDecls) = runState (transExpr expr) mempty
+    -- Statements to execute as part of the generator. They include statements
+    -- related to calculating the values of intermediate expressions, and
+    -- statements related to copying the final value to the destination array.
+    stmts = stmts' ++ [ copyStmt ]
 
-    -- Copy expression to output argument
-    stmts = [ C.Expr $ memcpy (C.Ident nameArg) cExpr size ]
-    size  = C.LitInt (fromIntegral $ typeSize ty)
-              C..* C.SizeOfType (C.TypeName $ tyElemName ty)
+    -- Output value, variable declarations needed, and other statements that
+    -- must be executed to calculate intermediate values.
+    (cExpr, state')       = runState (transExpr expr) (0, mempty, mempty)
+    (_, varDecls, stmts') = state'
+
+    -- Copy expression to output argument.
+    copyStmt = C.Expr $ memcpy (C.Ident nameArg) cExpr size
+    size     = C.LitInt (fromIntegral $ typeSize ty)
+                 C..* C.SizeOfType (C.TypeName $ tyElemName ty)
 
 mkGenFunArray _name _nameArg _expr _ty =
   impossible "mkGenFunArray" "copilot-c99"

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

@@ -8,19 +8,20 @@ module Copilot.Compile.C99.Expr
   where
 
 -- External imports
-import           Control.Monad.State ( State, modify )
+import           Control.Monad.State ( State, get, modify )
 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 )
+                      toValues, typeSize )
 
 -- Internal imports
 import Copilot.Compile.C99.Error ( impossible )
 import Copilot.Compile.C99.Name  ( exCpyName, streamAccessorName )
-import Copilot.Compile.C99.Type  ( transLocalVarDeclType, transTypeName )
+import Copilot.Compile.C99.Type  ( transLocalVarDeclType, transType,
+                                   transTypeName )
 
 -- | Translates a Copilot Core expression into a C99 expression.
 transExpr :: Expr a -> State FunEnv C.Expr
@@ -32,7 +33,9 @@ transExpr (Local ty1 _ name e1 e2) = do
       initExpr = Just $ C.InitExpr e1'
 
   -- Add new decl to the tail of the fun env
-  modify (++ [C.VarDecln Nothing cTy1 name initExpr])
+  modify (\(i, x, y)
+             -> (i, x ++ [C.VarDecln Nothing cTy1 name initExpr], y)
+         )
 
   transExpr e2
 
@@ -51,6 +54,48 @@ transExpr (Op1 op e) = do
   e' <- transExpr e
   return $ transOp1 op e'
 
+transExpr (Op2 (UpdateField ty1@(Struct _) ty2 f) e1 e2) = do
+  -- Translating a struct update Op requires initializing a variable to the
+  -- "old" value, updating the field, and returning the new value.
+  e1' <- transExpr e1
+  e2' <- transExpr e2
+
+  -- Variable to hold the updated struct
+  (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     = transLocalVarDeclType ty1
+  modify (\(i, x, y) -> (i, x ++ [initDecl], y))
+
+  -- Initialize the var to the same value as the original struct
+  let initStmt = C.Expr
+               $ C.AssignOp
+                   C.Assign
+                   (C.Ident varName)
+                   e1'
+
+  -- Update field f with given value e2.
+  let updateStmt = case ty2 of
+        Array _ -> C.Expr $ memcpy dest e2' size
+          where
+            dest = C.Dot (C.Ident varName) (accessorName f)
+            size = C.LitInt
+                       (fromIntegral $ typeSize ty2)
+                       C..* C.SizeOfType (C.TypeName (tyElemName ty2))
+
+        _       -> C.Expr
+                 $ C.AssignOp
+                     C.Assign
+                     (C.Dot (C.Ident varName) (accessorName f))
+                     e2'
+
+  modify (\(i, x, y) -> (i, x, y ++ [ initStmt, updateStmt ]))
+
+  return $ C.Ident varName
+
 transExpr (Op2 op e1 e2) = do
   e1' <- transExpr e1
   e2' <- transExpr e2
@@ -100,32 +145,35 @@ transOp1 op e =
 
 -- | Translates a Copilot binary operator and its arguments into a C99
 -- expression.
+--
+-- PRE: op is not a struct update operation (i.e., 'UpdateField').
 transOp2 :: Op2 a b c -> C.Expr -> C.Expr -> C.Expr
 transOp2 op e1 e2 = case op of
-  And          -> e1 C..&& e2
-  Or           -> e1 C..|| e2
-  Add      _   -> e1 C..+  e2
-  Sub      _   -> e1 C..-  e2
-  Mul      _   -> e1 C..*  e2
-  Mod      _   -> e1 C..%  e2
-  Div      _   -> e1 C../  e2
-  Fdiv     _   -> e1 C../  e2
-  Pow      ty  -> funCall (specializeMathFunName ty "pow") [e1, e2]
-  Logb     ty  -> funCall (specializeMathFunName ty "log") [e2] C../
-                  funCall (specializeMathFunName ty "log") [e1]
-  Atan2    ty  -> funCall (specializeMathFunName ty "atan2") [e1, e2]
-  Eq       _   -> e1 C..== e2
-  Ne       _   -> e1 C..!= e2
-  Le       _   -> e1 C..<= e2
-  Ge       _   -> e1 C..>= e2
-  Lt       _   -> e1 C..<  e2
-  Gt       _   -> e1 C..>  e2
-  BwAnd    _   -> e1 C..&  e2
-  BwOr     _   -> e1 C..|  e2
-  BwXor    _   -> e1 C..^  e2
-  BwShiftL _ _ -> e1 C..<< e2
-  BwShiftR _ _ -> e1 C..>> e2
-  Index    _   -> C.Index e1 e2
+  And               -> e1 C..&& e2
+  Or                -> e1 C..|| e2
+  Add         _     -> e1 C..+  e2
+  Sub         _     -> e1 C..-  e2
+  Mul         _     -> e1 C..*  e2
+  Mod         _     -> e1 C..%  e2
+  Div         _     -> e1 C../  e2
+  Fdiv        _     -> e1 C../  e2
+  Pow         ty    -> funCall (specializeMathFunName ty "pow") [e1, e2]
+  Logb        ty    -> funCall (specializeMathFunName ty "log") [e2] C../
+                       funCall (specializeMathFunName ty "log") [e1]
+  Atan2       ty    -> funCall (specializeMathFunName ty "atan2") [e1, e2]
+  Eq          _     -> e1 C..== e2
+  Ne          _     -> e1 C..!= e2
+  Le          _     -> e1 C..<= e2
+  Ge          _     -> e1 C..>= e2
+  Lt          _     -> e1 C..<  e2
+  Gt          _     -> e1 C..>  e2
+  BwAnd       _     -> e1 C..&  e2
+  BwOr        _     -> e1 C..|  e2
+  BwXor       _     -> e1 C..^  e2
+  BwShiftL    _ _   -> e1 C..<< e2
+  BwShiftR    _ _   -> e1 C..>> e2
+  Index       _     -> C.Index e1 e2
+  UpdateField _ _ _ -> impossible "transOp2" "copilot-c99"
 
 -- | Translates a Copilot ternary operator and its arguments into a C99
 -- expression.
@@ -368,10 +416,24 @@ typeIsFloating _      = False
 -- | Auxiliary type used to collect all the declarations of all the variables
 -- used in a function to be generated, since variable declarations are always
 -- listed first at the top of the function body.
-type FunEnv = [C.Decln]
+type FunEnv = (Int, [C.Decln], [C.Stmt])
 
 -- | Define a C expression that calls a function with arguments.
 funCall :: C.Ident   -- ^ Function name
         -> [C.Expr]  -- ^ Arguments
         -> C.Expr
 funCall name = C.Funcall (C.Ident name)
+
+-- Write a call to the memcpy function.
+memcpy :: C.Expr -> C.Expr -> C.Expr -> C.Expr
+memcpy dest src size = C.Funcall (C.Ident "memcpy") [dest, src, size]
+
+-- Translate a Copilot type to a C99 type, handling arrays especially.
+--
+-- If the given type is an array (including multi-dimensional arrays), the
+-- type is that of the elements in the array. Otherwise, it is just the
+-- equivalent representation of the given type in C.
+tyElemName :: Type a -> C.Type
+tyElemName ty = case ty of
+  Array ty' -> tyElemName ty'
+  _         -> transType ty

copilot-core/CHANGELOG

@@ -1,3 +1,6 @@
+2024-07-07
+        * Update Op2, Struct to support struct field updates. (#520)
+
 2024-05-07
         * Version bump (3.19.1). (#512)
 

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

@@ -13,9 +13,10 @@ module Copilot.Core.Operators
   where
 
 -- External imports
-import Data.Bits    (Bits)
-import Data.Word    (Word32)
-import GHC.TypeLits (KnownSymbol)
+import Data.Bits     (Bits)
+import Data.Typeable (Typeable)
+import Data.Word     (Word32)
+import GHC.TypeLits  (KnownSymbol)
 
 -- Internal imports
 import Copilot.Core.Type       (Field (..), Type (..))
@@ -96,6 +97,11 @@ data Op2 a b c where
   Index    :: Type (Array n t) -> Op2 (Array n t) Word32 t
               -- ^ Array access/projection of an array element.
 
+  -- Struct operator.
+  UpdateField :: (Typeable b, KnownSymbol s, Show b)
+              => Type a -> Type b -> (a -> Field s b) -> Op2 a b a
+              -- ^ Update a field of a struct.
+
 -- | Ternary operators.
 data Op3 a b c d where
   -- Conditional operator.

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

@@ -34,6 +34,7 @@ module Copilot.Core.Type
     , Struct
     , fieldName
     , accessorName
+    , updateField
     )
   where
 
@@ -59,6 +60,9 @@ class Struct a where
   -- | Transforms all the struct's fields into a list of values.
   toValues :: a -> [Value a]
 
+  updateField :: a -> Value t -> a
+  updateField = error "Field updates not supported for this type."
+
 -- | The field of a struct, together with a representation of its type.
 data Value a =
   forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)

copilot-interpreter/CHANGELOG

@@ -1,3 +1,6 @@
+2024-07-07
+        * Add support for struct field updates. (#520)
+
 2024-05-07
         * Version bump (3.19.1). (#512)
 

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

@@ -2,10 +2,11 @@
 
 -- | A tagless interpreter for Copilot specifications.
 
-{-# LANGUAGE BangPatterns       #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GADTs              #-}
-{-# LANGUAGE Safe               #-}
+{-# LANGUAGE BangPatterns        #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE Safe                #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Copilot.Interpret.Eval
   ( Env
@@ -17,8 +18,9 @@ module Copilot.Interpret.Eval
 
 import Copilot.Core            (Expr (..), Field (..), Id, Name, Observer (..),
                                 Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
-                                Trigger (..), Type (..), UExpr (..), arrayElems,
-                                specObservers, specStreams, specTriggers)
+                                Trigger (..), Type (..), UExpr (..), Value (..),
+                                arrayElems, specObservers, specStreams,
+                                specTriggers, updateField)
 import Copilot.Interpret.Error (badUsage)
 
 import           Prelude hiding (id)
@@ -244,6 +246,12 @@ evalOp2 op = case op of
   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
   Index    _   -> \xs n -> (arrayElems xs) !! (fromIntegral n)
 
+  UpdateField (Struct _) ty (fieldAccessor :: a -> Field s b) ->
+    \stream fieldValue ->
+      let newField :: Field s b
+          newField = Field fieldValue
+      in updateField stream (Value ty newField)
+
 -- | Apply a function to two numbers, so long as the second one is
 -- not zero.
 --

copilot-language/CHANGELOG

@@ -1,5 +1,6 @@
-2024-07-06
+2024-07-07
         * Remove deprecated function Copilot.Language.Spec.forall. (#518)
+        * Add support for struct field updates. (#520)
 
 2024-05-07
         * Version bump (3.19.1). (#512)