Skip to content

Commit 7e9bfb4

Browse files
abdoo8080abdoo8080
committed
feat: initial work to support QF_FP
1 parent 95ed24d commit 7e9bfb4

3 files changed

Lines changed: 230 additions & 6 deletions

File tree

‎Leanwuzla/Aux.lean‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
1-
module
1+
-- module
22
prelude
3-
public import Init.Data.BitVec.Basic
3+
-- public import Init.Data.BitVec.Basic
4+
-- Temporarily disable module system until Fp supports it
5+
import Init.Data.BitVec.Basic
6+
import Fp
47

58
public section
69

‎Leanwuzla/Parser.lean‎

Lines changed: 220 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
import Leanwuzla.Aux
22
import Leanwuzla.Sexp
3+
import Fp
34

45
open Lean
56

@@ -23,16 +24,44 @@ abbrev ParserM := StateT Parser.State (Except MessageData)
2324
namespace Parser
2425

2526
private def mkBool : Expr :=
26-
.const ``Bool []
27+
toTypeExpr Bool
2728

2829
private def mkBitVec (w : Nat) : Expr :=
29-
.app (.const ``BitVec []) (mkNatLit w)
30+
toTypeExpr (BitVec w)
31+
32+
-- Temporary ToExpr instances for PackedFloat and RoundingMode
33+
deriving instance ToExpr for PackedFloat
34+
deriving instance ToExpr for RoundingMode
35+
36+
private def mkFloat (eb sb : Nat) : Expr :=
37+
toTypeExpr (PackedFloat eb sb)
38+
39+
private def mkRoundingMode : Expr :=
40+
toTypeExpr RoundingMode
41+
42+
private def mkFloat16 : Expr :=
43+
toTypeExpr (PackedFloat 5 (11 - 1))
44+
45+
private def mkFloat32 : Expr :=
46+
toTypeExpr (PackedFloat 8 (24 - 1))
47+
48+
private def mkFloat64 : Expr :=
49+
toTypeExpr (PackedFloat 11 (53 - 1))
50+
51+
private def mkFloat128 : Expr :=
52+
toTypeExpr (PackedFloat 15 (113 - 1))
3053

3154
private def getBitVecWidth (α : Expr) : ParserM Nat := do
3255
match α with
3356
| .app (.const ``BitVec []) w => return w.nat?.get!
3457
| _ => throw m!"Error: expected BitVec type, got {α}"
3558

59+
private def getFloatEbSb (α : Expr) : ParserM (Nat × Nat) := do
60+
match α with
61+
| .app (.app (.const ``PackedFloat []) eb) sb =>
62+
return (eb.nat?.get!, sb.nat?.get!)
63+
| _ => throw m!"Error: expected PackedFloat type, got {α}"
64+
3665
private def mkInstBEqBool : Expr :=
3766
mkApp2 (.const ``instBEqOfDecidableEq [0]) mkBool
3867
(.const ``instDecidableEqBool [])
@@ -41,6 +70,10 @@ private def mkInstBEqBitVec (w : Nat) : Expr :=
4170
mkApp2 (.const ``instBEqOfDecidableEq [0]) (mkBitVec w)
4271
(.app (.const ``instDecidableEqBitVec []) (mkNatLit w))
4372

73+
private def mkInstBEqFloat (eb sb : Nat) : Expr :=
74+
mkApp2 (.const ``instBEqOfDecidableEq [0]) (mkFloat eb sb)
75+
(mkApp2 (.const ``instDecidableEqPackedFloat []) (mkNatLit eb) (mkNatLit sb))
76+
4477
private def mkBitVecAppend (w v : Nat) : Expr :=
4578
mkApp4 (.const ``HAppend.hAppend [0, 0, 0])
4679
(mkBitVec w) (mkBitVec v) (mkBitVec (w + v))
@@ -125,6 +158,20 @@ def parseSort (s : Sexp) : ParserM (Expr × Expr) := do
125158
| sexp!{(_ BitVec {w})} =>
126159
let w := w.serialize.toNat!
127160
return (mkBitVec w, mkBitVec w)
161+
| sexp!{(_ FloatingPoint {eb} {sb})} =>
162+
let eb := eb.serialize.toNat!
163+
let sb := sb.serialize.toNat!
164+
return (mkFloat eb (sb - 1), mkFloat eb (sb - 1))
165+
| sexp!{Float16} =>
166+
return (mkFloat16, mkFloat16)
167+
| sexp!{Float32} =>
168+
return (mkFloat32, mkFloat32)
169+
| sexp!{Float64} =>
170+
return (mkFloat64, mkFloat64)
171+
| sexp!{Float128} =>
172+
return (mkFloat128, mkFloat128)
173+
| sexp!{RoundingMode} =>
174+
return (mkRoundingMode, mkRoundingMode)
128175
| sexp!{({sc} ⦃as⦄)} =>
129176
let (bsc, sc) ← parseSort sc
130177
let as ← as.mapM parseSort
@@ -159,9 +206,9 @@ where
159206
let e := bindings.foldr (fun (n, t, v) b => .letE n t v b true) b
160207
return (tb, e)
161208
if let sexp!{true} := e then
162-
return (mkBool, .const ``true [])
209+
return (mkBool, toExpr true)
163210
if let sexp!{false} := e then
164-
return (mkBool, .const ``false [])
211+
return (mkBool, toExpr false)
165212
if let sexp!{(not {p})} := e then
166213
let (_, p) ← parseTerm p
167214
return (mkBool, .app (.const ``not []) p)
@@ -180,6 +227,7 @@ where
180227
let (_, y) ← parseTerm y
181228
let hα ← if uα == mkBool then pure mkInstBEqBool
182229
else if uα.isAppOfArity ``BitVec 1 then pure (mkInstBEqBitVec (← getBitVecWidth uα))
230+
else if uα.isAppOfArity ``PackedFloat 2 then let (eb, sb) ← getFloatEbSb uα; pure (mkInstBEqFloat eb sb)
183231
else throw m!"Error: unsupported type for equality: {uα}"
184232
return (mkBool, mkApp4 (.const ``BEq.beq [0]) uα hα x y)
185233
if let sexp!{(distinct ⦃xs⦄)} := e then
@@ -351,6 +399,173 @@ where
351399
let (α, x) ← parseTerm x
352400
let w ← getBitVecWidth α
353401
return (α, mkApp3 (.const ``BitVec.rotateRight []) (mkNatLit w) x (mkNatLit i))
402+
if let sexp!{roundNearestTiesToEven} := e then
403+
return (mkRoundingMode, toExpr RoundingMode.RNE)
404+
if let sexp!{RNE} := e then
405+
return (mkRoundingMode, toExpr RoundingMode.RNE)
406+
if let sexp!{roundNearestTiesToAway} := e then
407+
return (mkRoundingMode, toExpr RoundingMode.RNA)
408+
if let sexp!{RNA} := e then
409+
return (mkRoundingMode, toExpr RoundingMode.RNA)
410+
if let sexp!{roundTowardPositive} := e then
411+
return (mkRoundingMode, toExpr RoundingMode.RTP)
412+
if let sexp!{RTP} := e then
413+
return (mkRoundingMode, toExpr RoundingMode.RTP)
414+
if let sexp!{roundTowardNegative} := e then
415+
return (mkRoundingMode, toExpr RoundingMode.RTN)
416+
if let sexp!{RTN} := e then
417+
return (mkRoundingMode, toExpr RoundingMode.RTN)
418+
if let sexp!{roundTowardZero} := e then
419+
return (mkRoundingMode, toExpr RoundingMode.RTZ)
420+
if let sexp!{RTZ} := e then
421+
return (mkRoundingMode, toExpr RoundingMode.RTZ)
422+
if let sexp!{(fp {sign} {ex} {sig})} := e then
423+
let some ⟨1, sign⟩ := parseBVLiteral? sign | throw m!"Error: expected sign to be a bit-vector literal"
424+
let some ⟨eb, ex⟩ := parseBVLiteral? ex | throw m!"Error: expected exponent to be a bit-vector literal"
425+
let some ⟨sb, sig⟩ := parseBVLiteral? sig | throw m!"Error: expected significand to be a bit-vector literal"
426+
return (mkFloat eb sb, toExpr (PackedFloat.mk sign.msb ex sig))
427+
if let sexp!{(_ +oo {eb} {sb})} := e then
428+
let eb := eb.serialize.toNat!
429+
let sb := sb.serialize.toNat! - 1
430+
return (mkFloat eb sb, toExpr (PackedFloat.getInfinity eb sb false))
431+
if let sexp!{(_ -oo {eb} {sb})} := e then
432+
let eb := eb.serialize.toNat!
433+
let sb := sb.serialize.toNat! - 1
434+
return (mkFloat eb sb, toExpr (PackedFloat.getInfinity eb sb true))
435+
if let sexp!{(_ +zero {eb} {sb})} := e then
436+
let eb := eb.serialize.toNat!
437+
let sb := sb.serialize.toNat! - 1
438+
return (mkFloat eb sb, toExpr (PackedFloat.getZero eb sb false))
439+
if let sexp!{(_ -zero {eb} {sb})} := e then
440+
let eb := eb.serialize.toNat!
441+
let sb := sb.serialize.toNat! - 1
442+
return (mkFloat eb sb, toExpr (PackedFloat.getZero eb sb true))
443+
if let sexp!{(_ NaN {eb} {sb})} := e then
444+
let eb := eb.serialize.toNat!
445+
let sb := sb.serialize.toNat! - 1
446+
return (mkFloat eb sb, toExpr (PackedFloat.getNaN eb sb))
447+
if let sexp!{(fp.abs {x})} := e then
448+
let (α, x) ← parseTerm x
449+
let (eb, sb) ← getFloatEbSb α
450+
return (α, mkApp3 (.const ``abs []) (mkNatLit eb) (mkNatLit sb) x)
451+
if let sexp!{(fp.neg {x})} := e then
452+
let (α, x) ← parseTerm x
453+
let (eb, sb) ← getFloatEbSb α
454+
return (α, mkApp3 (.const ``neg []) (mkNatLit eb) (mkNatLit sb) x)
455+
if let sexp!{(fp.add {rm} {x} {y})} := e then
456+
let (_, rm) ← parseTerm rm
457+
let (α, x) ← parseTerm x
458+
let (_, y) ← parseTerm y
459+
let (eb, sb) ← getFloatEbSb α
460+
return (α, mkApp5 (.const ``add []) (mkNatLit eb) (mkNatLit sb) x y rm)
461+
if let sexp!{(fp.sub {rm} {x} {y})} := e then
462+
let (_, rm) ← parseTerm rm
463+
let (α, x) ← parseTerm x
464+
let (_, y) ← parseTerm y
465+
let (eb, sb) ← getFloatEbSb α
466+
return (α, mkApp5 (.const ``sub []) (mkNatLit eb) (mkNatLit sb) x y rm)
467+
if let sexp!{(fp.mul {rm} {x} {y})} := e then
468+
let (_, rm) ← parseTerm rm
469+
let (α, x) ← parseTerm x
470+
let (_, y) ← parseTerm y
471+
let (eb, sb) ← getFloatEbSb α
472+
return (α, mkApp5 (.const ``mul []) (mkNatLit eb) (mkNatLit sb) x y rm)
473+
if let sexp!{(fp.div {rm} {x} {y})} := e then
474+
let (_, rm) ← parseTerm rm
475+
let (α, x) ← parseTerm x
476+
let (_, y) ← parseTerm y
477+
let (eb, sb) ← getFloatEbSb α
478+
return (α, mkApp5 (.const ``div []) (mkNatLit eb) (mkNatLit sb) x y rm)
479+
if let sexp!{(fp.fma {rm} {x} {y} {z})} := e then
480+
let (_, rm) ← parseTerm rm
481+
let (α, x) ← parseTerm x
482+
let (_, y) ← parseTerm y
483+
let (_, z) ← parseTerm z
484+
let (eb, sb) ← getFloatEbSb α
485+
return (α, mkApp6 (.const ``fma []) (mkNatLit eb) (mkNatLit sb) x y z rm)
486+
if let sexp!{(fp.sqrt {rm} {x})} := e then
487+
let (_, rm) ← parseTerm rm
488+
let (α, x) ← parseTerm x
489+
let (eb, sb) ← getFloatEbSb α
490+
return (α, mkApp4 (.const ``sqrt []) (mkNatLit eb) (mkNatLit sb) x rm)
491+
if let sexp!{(fp.rem {x} {y})} := e then
492+
let (α, x) ← parseTerm x
493+
let (_, y) ← parseTerm y
494+
let (eb, sb) ← getFloatEbSb α
495+
return (α, mkApp4 (.const ``remainder []) (mkNatLit eb) (mkNatLit sb) x y)
496+
if let sexp!{(fp.roundToIntegral {rm} {x})} := e then
497+
let (_, rm) ← parseTerm rm
498+
let (α, x) ← parseTerm x
499+
let (eb, sb) ← getFloatEbSb α
500+
return (α, mkApp4 (.const ``roundToInt []) (mkNatLit eb) (mkNatLit sb) rm x)
501+
if let sexp!{(fp.min {x} {y})} := e then
502+
let (α, x) ← parseTerm x
503+
let (_, y) ← parseTerm y
504+
let (eb, sb) ← getFloatEbSb α
505+
return (α, mkApp4 (.const ``flt_min []) (mkNatLit eb) (mkNatLit sb) x y)
506+
if let sexp!{(fp.max {x} {y})} := e then
507+
let (α, x) ← parseTerm x
508+
let (_, y) ← parseTerm y
509+
let (eb, sb) ← getFloatEbSb α
510+
return (α, mkApp4 (.const ``flt_max []) (mkNatLit eb) (mkNatLit sb) x y)
511+
if let sexp!{(fp.leq {x} {y})} := e then
512+
let (α, x) ← parseTerm x
513+
let (_, y) ← parseTerm y
514+
let (eb, sb) ← getFloatEbSb α
515+
return (mkBool, mkApp4 (.const ``le []) (mkNatLit eb) (mkNatLit sb) x y)
516+
if let sexp!{(fp.lt {x} {y})} := e then
517+
let (α, x) ← parseTerm x
518+
let (_, y) ← parseTerm y
519+
let (eb, sb) ← getFloatEbSb α
520+
return (mkBool, mkApp4 (.const ``lt []) (mkNatLit eb) (mkNatLit sb) x y)
521+
if let sexp!{(fp.geq {x} {y})} := e then
522+
let (α, x) ← parseTerm x
523+
let (_, y) ← parseTerm y
524+
let (eb, sb) ← getFloatEbSb α
525+
return (mkBool, mkApp4 (.const ``ge []) (mkNatLit eb) (mkNatLit sb) x y)
526+
if let sexp!{(fp.gt {x} {y})} := e then
527+
let (α, x) ← parseTerm x
528+
let (_, y) ← parseTerm y
529+
let (eb, sb) ← getFloatEbSb α
530+
return (mkBool, mkApp4 (.const ``gt []) (mkNatLit eb) (mkNatLit sb) x y)
531+
if let sexp!{(fp.eq {x} {y})} := e then
532+
let (α, x) ← parseTerm x
533+
let (_, y) ← parseTerm y
534+
let (eb, sb) ← getFloatEbSb α
535+
return (mkBool, mkApp4 (.const ``eq []) (mkNatLit eb) (mkNatLit sb) x y)
536+
if let sexp!{(fp.isNormal {x})} := e then
537+
let (α, x) ← parseTerm x
538+
let (eb, sb) ← getFloatEbSb α
539+
return (mkBool, mkApp3 (.const ``PackedFloat.isNorm []) (mkNatLit eb) (mkNatLit sb) x)
540+
if let sexp!{(fp.isSubnormal {x})} := e then
541+
let (α, x) ← parseTerm x
542+
let (eb, sb) ← getFloatEbSb α
543+
return (mkBool, mkApp3 (.const ``PackedFloat.isSubnorm []) (mkNatLit eb) (mkNatLit sb) x)
544+
if let sexp!{(fp.isZero {x})} := e then
545+
let (α, x) ← parseTerm x
546+
let (eb, sb) ← getFloatEbSb α
547+
return (mkBool, mkApp3 (.const ``PackedFloat.isZero []) (mkNatLit eb) (mkNatLit sb) x)
548+
if let sexp!{(fp.isInfinite {x})} := e then
549+
let (α, x) ← parseTerm x
550+
let (eb, sb) ← getFloatEbSb α
551+
return (mkBool, mkApp3 (.const ``PackedFloat.isInfinite []) (mkNatLit eb) (mkNatLit sb) x)
552+
if let sexp!{(fp.isNaN {x})} := e then
553+
let (α, x) ← parseTerm x
554+
let (eb, sb) ← getFloatEbSb α
555+
return (mkBool, mkApp3 (.const ``PackedFloat.isNaN []) (mkNatLit eb) (mkNatLit sb) x)
556+
if let sexp!{(fp.isNegative {x})} := e then
557+
let (α, x) ← parseTerm x
558+
let (eb, sb) ← getFloatEbSb α
559+
return (mkBool, mkApp3 (.const ``PackedFloat.isNeg []) (mkNatLit eb) (mkNatLit sb) x)
560+
if let sexp!{(fp.isPositive {x})} := e then
561+
let (α, x) ← parseTerm x
562+
let (eb, sb) ← getFloatEbSb α
563+
return (mkBool, mkApp3 (.const ``PackedFloat.isPos []) (mkNatLit eb) (mkNatLit sb) x)
564+
if let sexp!{((_ to_fp {eb} {sb}) {x})} := e then
565+
let eb := eb.serialize.toNat!
566+
let sb := sb.serialize.toNat! - 1
567+
let (β, x) ← parseTerm x
568+
return (mkFloat eb sb, mkApp3 (.const ``PackedFloat.ofBits []) (mkNatLit eb) (mkNatLit sb) x)
354569
if let some r ← parseVar? e then
355570
return r
356571
if let some ⟨w, x⟩ := parseBVLiteral? s then
@@ -415,6 +630,7 @@ where
415630
let hα ← if α == mkBool
416631
then pure mkInstBEqBool
417632
else if α.isAppOfArity ``BitVec 1 then pure (mkInstBEqBitVec (← getBitVecWidth α))
633+
else if α.isAppOfArity ``PackedFloat 2 then let (eb, sb) ← getFloatEbSb α; pure (mkInstBEqFloat eb sb)
418634
else throw m!"Error: unsupported type for `distinct`: {α}"
419635
let mut acc : Expr := mkApp4 (.const ``bne [0]) α hα as0 as1
420636
for hi : i in [2:as.length] do

‎lakefile.toml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,3 +18,8 @@ supportInterpreter = true
1818
scope = "leanprover"
1919
name = "Cli"
2020
rev = "nightly-testing"
21+
22+
[[require]]
23+
git = "https://github.com/opencompl/fp-lean"
24+
name = "fp-lean"
25+
rev = "main"

0 commit comments

Comments
 (0)