This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
allow-newer: | |
assoc:base, | |
async:base, | |
binary-orphans:base, | |
-- TODO | |
blank-canvas:base, | |
-- TODO | |
blank-canvas-examples:base, | |
boring:base, | |
-- TODO |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE Haskell2010 #-} | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE ImplicitParams #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE PatternSynonyms #-} | |
{-# LANGUAGE PolyKinds #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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(..)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE NoImplicitPrelude #-} | |
module Main (main) where | |
import Language.Copilot | |
import Copilot.Compile.C99 | |
data SoA = SoA | |
{ arr :: Field "arr" (Array 2 Word32) | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module FloatingPoint where | |
import Float | |
type FloatingPoint e m = | |
{ sign : Bit | |
, exp : [e] | |
, sfd : [m] | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
allow-newer: | |
aeson:containers, | |
aeson:template-haskell, | |
-- Ugh. | |
aeson:th-abstraction, | |
assoc:base, | |
async:base, | |
-- TODO | |
bifunctors:template-haskell, | |
binary-orphans:base, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
constraints: | |
containers == 0.7.* | |
allow-newer: | |
aeson:containers, | |
Cabal-syntax:containers, | |
cabal-install-parsers:containers, | |
cassava:containers, | |
foldable1-classes-compat:containers, | |
hashable:containers, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Blah where |
NewerOlder