RyanGlScott

{-# 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(..))

RyanGlScott

diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index f55e3884..428b6ac3 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -799,6 +799,8 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
   (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2
   (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2
   (CE.Index _, xe1, xe2) -> translateIndex xe1 xe2
+  (CE.UpdateField atp _ftp extractor, structXe, fieldXe) ->
+    translateUpdateField atp extractor structXe fieldXe

RyanGlScott

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

import Language.Copilot
import Copilot.Compile.C99

data SoA = SoA
  { arr :: Field "arr" (Array 2 Word32)
  }

RyanGlScott

module FloatingPoint where

import Float

type FloatingPoint e m =
  { sign : Bit
  , exp : [e]
  , sfd : [m]
  }

RyanGlScott

allow-newer:
  aeson:containers,
  aeson:template-haskell,
  -- Ugh.
  aeson:th-abstraction,
  assoc:base,
  async:base,
  -- TODO
  bifunctors:template-haskell,
  binary-orphans:base,

RyanGlScott

constraints:
  containers == 0.7.*

allow-newer:
  aeson:containers,
  Cabal-syntax:containers,
  cabal-install-parsers:containers,
  cassava:containers,
  foldable1-classes-compat:containers,
  hashable:containers,

RyanGlScott

crux-mir
  crux concrete
    
      refs
        promoted_imm:            OK (0.15s)
          Compiling and running oracle program (0.15s)
          Oracle output: 0
          Crux output: 0
        mut_raw:                 OK (0.15s)
          Compiling and running oracle program (0.15s)

RyanGlScott

module Blah where

RyanGlScott

allow-newer:
  aeson:deepseq,
  aeson:ghc-prim,
  aeson:template-haskell,
  aeson:th-abstraction,
  assoc:base,
  async:base,
  attoparsec:ghc-prim,
  binary-orphans:base,
  boring:base,

RyanGlScott

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.