Skip to content

Instantly share code, notes, and snippets.

@thoughtpolice

thoughtpolice/change.diff

Created April 18, 2017 22:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save thoughtpolice/963783bf79b0788976649ab79a24a163 to your computer and use it in GitHub Desktop.
Save thoughtpolice/963783bf79b0788976649ab79a24a163 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
change.diff
diff --git a/Z3/Category.hs b/Z3/Category.hs
index 816d8ca..7147aba 100644
--- a/Z3/Category.hs
+++ b/Z3/Category.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
@@ -25,6 +26,16 @@ import Control.Arrow (Kleisli(..), arr)
import Control.Monad (join)
import Z3.Monad
+#include "MachDeps.h"
+
+#if WORD_SIZE_IN_BITS == 64
+#define ARCH_64bit
+#elif WORD_SIZE_IN_BITS == 32
+#define ARCH_32bit
+#else
+#error expected WORD_SIZE_IN_BITS to be 32 or 64
+#endif
+
-- Typed AST structures ("expressions")
data E :: * -> * where
PrimE :: AST -> E a
@@ -137,8 +148,7 @@ instance CoproductCat Z3Cat where
constPrim :: (z -> Z3 AST) -> z -> Z3Cat a b
constPrim f x = eprim (const (f x))
-instance ConstCat Z3Cat Int where const = constPrim mkIntNum
-instance ConstCat Z3Cat Integer where const = constPrim mkIntNum
+instance ConstCat Z3Cat Integer where const = constPrim mkInteger
instance ConstCat Z3Cat Bool where const = constPrim mkBool
instance ClosedCat Z3Cat where
@@ -157,10 +167,10 @@ class GenE a where genE :: Z3 (E a)
genPrim :: (String -> Z3 AST) -> Z3 (E a)
genPrim mk = PrimE <$> mk "x"
-instance GenE Bool where genE = genPrim mkFreshBoolVar
-instance GenE Int where genE = genPrim mkFreshIntVar
-instance GenE Float where genE = genPrim mkFreshRealVar
-instance GenE Double where genE = genPrim mkFreshRealVar
+instance GenE Bool where genE = genPrim mkFreshBoolVar
+instance GenE Integer where genE = genPrim mkFreshIntVar
+instance GenE Float where genE = genPrim mkFreshRealVar
+instance GenE Double where genE = genPrim mkFreshRealVar
instance (GenE a, GenE b) => GenE (a,b) where genE = liftA2 PairE genE genE
@@ -182,10 +192,10 @@ evalInt' = (fmap.fmap.fmap.fmap) fromInteger evalInt
evalReal' :: Fractional a => EvalAst Z3 a
evalReal' = (fmap.fmap.fmap.fmap) fromRational evalReal
-instance EvalE Bool where evalE = evalPrim evalBool
-instance EvalE Int where evalE = evalPrim evalInt'
-instance EvalE Float where evalE = evalPrim evalReal'
-instance EvalE Double where evalE = evalPrim evalReal'
+instance EvalE Bool where evalE = evalPrim evalBool
+instance EvalE Integer where evalE = evalPrim evalInt'
+instance EvalE Float where evalE = evalPrim evalReal'
+instance EvalE Double where evalE = evalPrim evalReal'
instance (EvalE a, EvalE b) => EvalE (a,b) where
evalE m (PairE a b) = (liftA2.liftA2) (,) (evalE m a) (evalE m b)
diff --git a/test/Main.hs b/test/Main.hs
index d54b5ff..88d99d8 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -24,5 +24,5 @@ main :: IO ()
main = hspec $
describe "Basic tests" $
it "Runs a Haskell function through Z3" $
- runZ3 (ccc (uncurry (equation @Int)))
+ runZ3 (ccc (uncurry (equation @Integer)))
`shouldReturn` Just (-8, 2)
diff --git a/z3cat.cabal b/z3cat.cabal
index ffa09a8..d11a3e8 100644
--- a/z3cat.cabal
+++ b/z3cat.cabal
@@ -33,6 +33,7 @@ test-suite spec
test
build-depends:
base >= 4.9 && < 4.10
+ , base-orphans
, concat >= 0.2.0
, ghc-prim
, z3
Raw
crash.txt
aseipp@ubuntu:~/src/concat/z3cat$ cabal new-build z3cat:spec
In order, the following will be built (use -v for more details):
- z3cat-0.1.0 (test:spec) (file test/Main.hs changed)
Preprocessing test suite 'spec' for z3cat-0.1.0..
Building test suite 'spec' for z3cat-0.1.0..
[1 of 1] Compiling Main ( test/Main.hs, /home/aseipp/src/concat/dist-newstyle/build/x86_64-linux/ghc-8.0.2/z3cat-0.1.0/c/spec/build/spec/spec-tmp/Main.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
ccc post-transfo check. Lint
<no location info>: warning:
[RHS of wild_ahi9 :: Int#]
The type of this binder is primitive: wild_ahi9
Binder's type: Int#
ccc
@ Z3Cat
@ (Integer, Integer)
@ Bool
(\ (eta1_ah9F :: (Integer, Integer)) ->
let {
x_ahag :: Integer
[LclId,
Str=DmdType,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 50 0}]
x_ahag =
exl
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F } in
let {
ds_ahah :: Integer
[LclId,
Str=DmdType,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 50 0}]
ds_ahah =
exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F } in
case ltInteger# x_ahag ds_ahah of wild_ahi9 { __DEFAULT ->
case boxIB wild_ahi9 of _ [Occ=Dead] {
False -> False;
True ->
case ltInteger# ds_ahah 100 of wild_XhkM { __DEFAULT ->
case boxIB wild_XhkM of _ [Occ=Dead] {
False -> False;
True ->
case leInteger#
0 (plusInteger (minusInteger x_ahag 3) (timesInteger 7 ds_ahah))
of wild_ahig { __DEFAULT ->
case boxIB wild_ahig of _ [Occ=Dead] {
False -> False;
True ->
case eqInteger# x_ahag ds_ahah of wild_ahfW { __DEFAULT ->
case boxIB wild_ahfW of _ [Occ=Dead] {
False ->
case eqInteger# (plusInteger ds_ahah 20) (plusInteger x_ahag 30)
of wild_XhiL { __DEFAULT ->
boxIB wild_XhiL
};
True -> True
}
}
}
}
}
}
}
})
-->
ccc
@ Z3Cat
@ (Integer, Integer)
@ Bool
(\ (eta1_ah9F :: (Integer, Integer)) ->
let {
wild_ahi9 :: Int#
[LclId, Str=DmdType]
wild_ahi9 =
ltInteger#
(exl
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
(exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F) } in
case boxIB wild_ahi9 of _ [Occ=Dead] {
False -> False;
True ->
case ltInteger#
(exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
100
of wild_XhkM { __DEFAULT ->
case boxIB wild_XhkM of _ [Occ=Dead] {
False -> False;
True ->
case leInteger#
0
(plusInteger
(minusInteger
(exl
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
3)
(timesInteger
7
(exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)))
of wild_ahig { __DEFAULT ->
case boxIB wild_ahig of _ [Occ=Dead] {
False -> False;
True ->
case eqInteger#
(exl
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
(exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
of wild_ahfW { __DEFAULT ->
case boxIB wild_ahfW of _ [Occ=Dead] {
False ->
case eqInteger#
(plusInteger
(exr
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
20)
(plusInteger
(exl
@ (->)
@ Integer
@ Integer
$fProductCat(->)
(($fYes1ka @ * @ Integer, $fYes1ka @ * @ Integer)
`cast` ((Sym R:Ok(->)[0] <Integer>_N,
Sym R:Ok(->)[0] <Integer>_N)_R
:: ((Yes1 Integer, Yes1 Integer) :: Constraint)
~R#
((Ok (->) Integer, Ok (->) Integer) :: Constraint)))
eta1_ah9F)
30)
of wild_XhiL { __DEFAULT ->
boxIB wild_XhiL
};
True -> True
}
}
}
}
}
}
})
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment