Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

copilot-language: Support modifying values in arrays #36

Closed
ghost opened this issue Jul 8, 2019 · 13 comments
Closed

copilot-language: Support modifying values in arrays #36

ghost opened this issue Jul 8, 2019 · 13 comments
Assignees
Labels
CR:Status:Closed Admin only: Change request that has been completed CR:Type:Feature Admin only: Change request pertaining to new features requested
Milestone

Comments

@ghost
Copy link

ghost commented Jul 8, 2019

If I have 2 streams carrying doubles, such as:

x :: Stream Double
x = extern "x" Nothing

y :: Stream Double
y = extern "y" Nothing

Is it possible to define, with some function (or maybe an Op2):

xy :: Stream (Array 2 Double)
xy = ??? x y
@fdedden
Copy link
Member

fdedden commented Jul 9, 2019

Currently there is no way to construct an array from stream carrying scalars. Having a feature like this (and a similar one for structs) would indeed help a lot, and is worth looking into.

@ivanperez-keera
Copy link
Member

I wouldn't know how to go about it. I'm thinking about kinds and arities, but I'm not sure we could make it work.

@fdedden fdedden added the enhancement New feature or request label Jul 27, 2019
@fdedden fdedden added the feature request Request or advice for a feature label Mar 30, 2020
@ivanperez-keera
Copy link
Member

Update: Someone is working on a feature atm that would allow us to implement this.

@ivanperez-keera
Copy link
Member

ivanperez-keera commented Aug 6, 2023

Update: @InnovativeInventor has implemented 'set' or 'update' for arrays, which allows us to implement this. We'll be discussing integrating this into Copilot in the upcoming future.

@ivanperez-keera
Copy link
Member

Update: similar requests have come up recently related to structs. We are looking into porting the solution that @InnovativeInventor prepared to work for structs and adding both to Copilot. Stay tuned.

@ivanperez-keera
Copy link
Member

For awareness, we have an open issue #520 that we intend to merge today on updating fields of structs.

@ivanperez-keera
Copy link
Member

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

Not applicable (not a bug).

Expected result

Copilot provides a mechanism to update specific values in arrays in an stream of arrays.

Desired result

Copilot provides a mechanism to update specific values in arrays in an stream of arrays.

Proposed solution

Extend copilot-language to provide operations to modify values of arrays in streams.

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

Further notes

None.

@ivanperez-keera ivanperez-keera added CR:Type:Feature Admin only: Change request pertaining to new features requested CR:Status:Initiated Admin only: Change request that has been initiated and removed enhancement New feature or request feature request Request or advice for a feature labels Jul 8, 2024
@ivanperez-keera ivanperez-keera changed the title Defining Stream (Array 2 Double) from 2 Stream Double copilot-language: Support modifying values in arrays Jul 8, 2024
@ivanperez-keera
Copy link
Member

Change Manager: Confirmed that the issue exists.

@ivanperez-keera ivanperez-keera added CR:Status:Confirmed Admin only: Change request that has been acknowledged by the change manager and removed CR:Status:Initiated Admin only: Change request that has been initiated labels Jul 8, 2024
@ivanperez-keera
Copy link
Member

Technical Lead: Confirmed that the issue should be addressed.

@ivanperez-keera ivanperez-keera added CR:Status:Accepted Admin only: Change request accepted by technical lead and removed CR:Status:Confirmed Admin only: Change request that has been acknowledged by the change manager labels Jul 8, 2024
@ivanperez-keera
Copy link
Member

Technical Lead: Issue scheduled for Copilot 4.

Fix assigned to: @ivanperez-keera.

@ivanperez-keera ivanperez-keera added CR:Status:Scheduled Admin only: Change requested scheduled and removed CR:Status:Accepted Admin only: Change request accepted by technical lead labels Aug 10, 2024
@ivanperez-keera ivanperez-keera added this to the Copilot 4 milestone Aug 10, 2024
@ivanperez-keera ivanperez-keera self-assigned this Aug 10, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
… !. Refs Copilot-Language#36.

A prior commit has introduced a new symbol (!) as the preferred way to
project an element of an array for the purposes of reading it.

This commit modifies the pretty printer so that it uses the same
notation when printing an expression that projects a value of an array.
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…e#36.

A prior commit has introduced a new symbol (!) as the preferred way to
project an element of an array for the purposes of reading it.

This commit modifies all examples involving arrays to use the new
notation.
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…Language#36.

We want to add support to be able to modify values of elements in
arrays. In order to provide a uniform interface for arrays and structs,
we have decided to unify the syntax for array and struct accessors, so
that one operator symbol indicates read access, and doubling the same
operator symbol indicates modification access. For example, (!) would
indicate accessing an element of an array to consult it, and (!!) would
indicate the same but to update it or modify it. The analogous operators
for structs would be (#) and (##).

At present, the symbol (!!) is being used for an auxiliary function that
indexes a list of streams by a stream of indexes. That function is
expensive, and rarely used in real specifications.

This commit renames such rarely used function, (!!), to avoid a name
clash with our desired name for the function to access elements of
arrays in streams for the purposes of modifying them.
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
Copilot-Language#36.

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

This commit adds a new Op3 that allows array elements to be modified.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…guage#36.

Copilot defines a types for fixed-length arrays, but no way to update
them. In order to implement array updates for values in streams, we need
to have a mechanism to update values in individual arrays.

This commit adds a function to arrays to update a value while preserving the
length.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…n. Refs Copilot-Language#36.

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

This commit adds a new operation to the high-level Copilot language that
allows updating array elements. It relies on a low-level Op3 that
captures the correspnding operation in Copilot Core expressions.

In order to provide a uniform interface for arrays and structs, we have
decided to unify the syntax for array and struct accessors, so that the
operator symbol (=:) is used to set the value of individual elements,
and (=$) is used to apply a function to values of elements (at each
time). To support using the same syntax for both structs and arrays,
this commit moves those operators into a new class, defined in a module
Copilot.Language.Operators.Projection. The module
Copilot.Language.Operators.Struct now uses that module instead of
defining the operators locally, and so does the new module
Copilot.Language.Operators.Array.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
Copilot currently supports reading values from arrays, but not changing them.

This commit adds the translation to C of expressions that update an element of
an array.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…-Language#36.

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

This commit adds the interpretation in Haskell of expressions that update an
element of an array in a stream of arrays.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…pilot-Language#36.

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

This commit add support to pretty-print expressions that update elements
of an array.

Co-authored-by: Max Fan <maxwell.y.fan@nasa.gov>
ivanperez-keera pushed a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…age#36.

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

This commit adds symbolic reasoning support for array update expressions by
translating them to What4. The implementation is largely inspired by the
existing translation for array index expressions. Because the index in an array
update expression can be symbolic, we must build a chain of symbolic
if-then-else expressions that check the value of the possibly-symbolic index
against all possible concrete index values from `0` to `n - 1` (where `n` is
the size of the array).
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…lot-Language#36.

Previous commits have introduced support to modify individual elements
of arrays, either by giving a new stream of values for a position in an
array, or by applying a stream function to an element.

This commit updates an existing example in the examples/ directory to
demonstrate array updates.
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
…t-Language#36.

Previous commits have introduced support to modify individual elements
of arrays, either by giving a new stream of values for a position in an
array, or by applying a stream function to an element.

This commit introduces a new example in the examples/ directory to
demonstrate using copilot-theorem to reason about arrays where
individual elements are being updated.
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
ivanperez-keera added a commit to ivanperez-keera/copilot that referenced this issue Sep 6, 2024
@ivanperez-keera
Copy link
Member

Implementor: Solution implemetned, review requested.

@ivanperez-keera ivanperez-keera added CR:Status:Verification Admin only: Change request that is currently being verified and removed CR:Status:Implementation Admin only: Change request that is currently being implemented labels Sep 6, 2024
@ivanperez-keera
Copy link
Member

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/272213129

    • 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 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/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=191a75f096d5956f25737b354a1279b00a6e2cde" -it copilot-verify-36
      
  • Implementation is documented. Details:
    New operations and modules are documented.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    Examples updated and new examples included.
  • Required version bumps are evaluated. Details:
    Bump needed (the definitions of both Op3 have changed; a function has been hidden, a function has been deprecated, and operations have moved modules).

@ivanperez-keera
Copy link
Member

Change Manager: Implementation ready to be merged.

@ivanperez-keera ivanperez-keera added CR:Status:Closed Admin only: Change request that has been completed and removed CR:Status:Verification Admin only: Change request that is currently being verified labels Sep 6, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
CR:Status:Closed Admin only: Change request that has been completed CR:Type:Feature Admin only: Change request pertaining to new features requested
Development

No branches or pull requests

2 participants