forked from runtimeverification/python-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpython-semantics-floats.k
More file actions
19 lines (14 loc) · 2.26 KB
/
Copy pathpython-semantics-floats.k
File metadata and controls
19 lines (14 loc) · 2.26 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
require "python-semantics-boolean-ops.k"
module PYTHON-SEMANTICS-FLOATS
imports PYTHON-SEMANTICS-BOOLEAN-OPS
rule invokeBuiltin(obj("float.__lt__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) <Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) <Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__gt__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) >Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) >Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__le__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) <=Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) <=Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__ge__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) >=Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) >=Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__eq__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) ==Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) ==Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__ne__",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("int")), binaryOp(O, O2, "float", "int", bool(floatvalue(O) =/=Float Int2Float(intvalue(O2)))), binaryOp(O, O2, "float", "float", bool(floatvalue(O) =/=Float floatvalue(O2))))
rule invokeBuiltin(obj("float.__int__",_), ListItem(O), .) => unaryOp(O, "float", Float2Int(floatvalue(O)))
rule invokeBuiltin(obj("float.__new__",_), ListItem(O:Object), .) => newHelper(O, ref("float"), .) ~> immutable(0.0, O)
rule invokeBuiltin(obj("float.__new__",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("float"), .) ~> immutable(floatvalue(getmember(O2, "__float__", true, false, true) (.Arguments)), O)
context immutable(floatvalue(HOLE), _)
endmodule