copilot-language: Support modifying fields of structs

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.

Desired result

Copilot provides a mechanism to update the field of a struct.

Proposed solution

Extend copilot-language to provide operations to modify fields of structs.

Extend copilot-core, copilot-c99 and other libraries accordingly.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 3.20.

Fix assigned to: @ivanperez-keera.

copilot-c99: Expand expression translation environment to include sta…

copilot-c99: Handle new struct update operator. Refs Copilot-Language…

copilot-language: High-level array update operator. Refs Copilot-Lang…

copilot-core: Document changes in CHANGELOG. Refs Copilot-Language#520.

copilot-interpreter: Document changes in CHANGELOG. Refs Copilot-Lang…

copilot-c99: Document changes in CHANGELOG. Refs Copilot-Language#520.

copilot-language: Document changes in CHANGELOG. Refs Copilot-Languag…

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/271307963

The solution proposed produces the expected result. Details:
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/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=5fb6d605b4e25714f54a7ebfac1c6afaeb2e7519" -it copilot-verify-520

Implementation is documented. Details:
New operations are documented.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed.
Required version bumps are evaluated. Details:
Bump needed (the definitions of both Op2 and Struct have changed).

Change Manager: Implementation ready to be merged.

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

Merge branch 'develop-copilot-theorem-UpdateField'. Close #524.

Merge branch 'develop-copilot-prettyprinter-UpdateField'. Close #526.

Navigation Menu

Repository navigation

`copilot-language`: Support modifying fields of structs #520

60 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-language: Support modifying fields of structs #520

Description

Activity

ivanperez-keera commented on Jul 7, 2024

ivanperez-keera commented on Jul 7, 2024

ivanperez-keera commented on Jul 7, 2024

60 remaining items

ivanperez-keera commented on Jul 8, 2024

ivanperez-keera commented on Jul 8, 2024

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-language`: Support modifying fields of structs #520