finish-interpreter.diff

commit 25d3e99f8e05ca9b5af21859965e2d072f7855c0
Author: Ryan Scott <rscott@galois.com>
Date:   Fri Jul 5 18:47:29 2024 -0400

    WIP: finish interpret

diff --git a/copilot-core/src/Copilot/Core/Operators.hs b/copilot-core/src/Copilot/Core/Operators.hs
index 94624508..0009e568 100644
--- a/copilot-core/src/Copilot/Core/Operators.hs
+++ b/copilot-core/src/Copilot/Core/Operators.hs
@@ -98,7 +98,7 @@ data Op2 a b c where
               -- ^ Array access/projection of an array element.
 
   -- Struct operator.
-  UpdateField :: (Typeable b, KnownSymbol s)
+  UpdateField :: (Typeable b, KnownSymbol s, Show b)
               => Type a -> Type b -> (a -> Field s b) -> Op2 a b a
               -- ^ Projection of a struct field.
 
diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index 9074049f..38973f5e 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -60,7 +60,7 @@ class Struct a where
   -- | Transforms all the struct's fields into a list of values.
   toValues :: a -> [Value a]
 
-  updateField :: Typeable t => a -> Value t -> a
+  updateField :: a -> Value a -> a
   updateField = error "Field updates not supported for this type."
 
 -- | The field of a struct, together with a representation of its type.
diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 8207e280..4da73f84 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
@@ -244,9 +244,10 @@ evalOp2 op = case op of
   BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )
   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
   Index    _   -> \xs n -> (arrayElems xs) !! (fromIntegral n)
-  UpdateField (Struct _) ty (f :: a -> Field s b) -> \str v -> let fv :: Field s b
-                                                                   fv = Field v
-                                                               in updateField str (Value ty fv)
+  UpdateField (Struct _) ty (f :: a -> Field s b) -> \str v ->
+      let fv :: Field s b
+          fv = Field v
+      in updateField str (Value ty fv)
     where
       -- Extract value from field
       unfield (Field v) = v

StructOfArrays.hs

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

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

import Data.Proxy (Proxy(..))
import GHC.TypeLits (sameSymbol)

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
  }

instance Struct SoC where
  typeName _ = "soc"
  toValues soc = [Value typeOf (arr3 soc)]
  updateField s (Value ty (f :: Field s b)) =
    case sameSymbol (Proxy @s) (Proxy @"arr3") of
      Just DE.Refl -> case testEquality ty Int32 of
                  Just DE.Refl -> s { arr3 = f }
                  _ -> error "what do you think you are doing"
      _ -> error "you done goofed"

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

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

v1 = SoA $ Field $ SoB $ Field $ array [0, 1, 2]
                   --       , SoB $ Field $ array [3, 4, 5]
                   --       ]

b1 = SoB $ Field $ array [10, 20, 30]
b2 = SoB $ Field $ array [40, 50, 60]

spec :: Spec
spec = do
  let soa :: Stream SoA
      soa = constant v1
      soa1 = soa ## arr =: recursiveArray
      soa2 = soa ## arr =: constant b1
      soarr = soa ## arr =: soa # arr
      soc = constant (SoC $ Field 5)

  -- trigger "arrays" (soa1 # arr # arr2 .!! 1 /= 60) [arg soa, arg soa1, arg soa2]
  trigger "arrays2" true [arg (soc ## arr3 =$ (+1))]

main :: IO ()
main = do
  spec' <- reify spec
  compile "structs_of_arrays" spec'
  interpret 5 spec