Skip to content

Commit 109f06d

Browse files
committed
feat(kore): add IEEE float builtin support
1 parent 00479fb commit 109f06d

File tree

18 files changed

+1393
-0
lines changed

18 files changed

+1393
-0
lines changed

kore/kore.cabal

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -268,6 +268,8 @@ library
268268
Kore.Builtin.Endianness.Endianness
269269
Kore.Builtin.EqTerm
270270
Kore.Builtin.Error
271+
Kore.Builtin.Float
272+
Kore.Builtin.Float.Float
271273
Kore.Builtin.Inj
272274
Kore.Builtin.Int
273275
Kore.Builtin.Int.Int
@@ -316,6 +318,7 @@ library
316318
Kore.Internal.Inj
317319
Kore.Internal.InternalBool
318320
Kore.Internal.InternalBytes
321+
Kore.Internal.InternalFloat
319322
Kore.Internal.InternalInt
320323
Kore.Internal.InternalList
321324
Kore.Internal.InternalMap
@@ -473,6 +476,7 @@ library
473476
Kore.Simplify.InjSimplifier
474477
Kore.Simplify.InternalBool
475478
Kore.Simplify.InternalBytes
479+
Kore.Simplify.InternalFloat
476480
Kore.Simplify.InternalInt
477481
Kore.Simplify.InternalList
478482
Kore.Simplify.InternalMap
@@ -697,6 +701,7 @@ test-suite kore-test
697701
Test.Kore.Builtin.Encoding
698702
Test.Kore.Builtin.Endianness
699703
Test.Kore.Builtin.External
704+
Test.Kore.Builtin.Float
700705
Test.Kore.Builtin.Inj
701706
Test.Kore.Builtin.Int
702707
Test.Kore.Builtin.InternalBytes

kore/src/Kore/Builtin.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ import Kore.Attribute.Symbol qualified as Attribute
3838
import Kore.Builtin.Bool qualified as Bool
3939
import Kore.Builtin.Builtin qualified as Builtin
4040
import Kore.Builtin.Endianness qualified as Endianness
41+
import Kore.Builtin.Float qualified as Float
4142
import Kore.Builtin.IO qualified as IO
4243
import Kore.Builtin.Inj qualified as Inj
4344
import Kore.Builtin.Int qualified as Int
@@ -68,6 +69,7 @@ koreVerifiers =
6869
mempty
6970
<> Bool.verifiers
7071
<> Endianness.verifiers
72+
<> Float.verifiers
7173
<> Inj.verifiers
7274
<> Int.verifiers
7375
<> InternalBytes.verifiers
@@ -92,6 +94,7 @@ koreEvaluators :: Text -> Maybe BuiltinAndAxiomSimplifier
9294
koreEvaluators key =
9395
asum
9496
[ Bool.builtinFunctions key
97+
, Float.builtinFunctions key
9598
, Int.builtinFunctions key
9699
, IO.builtinFunctions key
97100
, KEqual.builtinFunctions key

0 commit comments

Comments
 (0)