In [16]:
from boole import *
from boole.elab.prelude import *
from boole.semantics.value import *
from boole.elab.terms import *
In [17]:
x, y, z = Int('x, y, z')
print x + y
(x + y)
In [18]:
M = Model({}, {'x' : Value(5), 'y' : Value(2)})
In [19]:
eval_expr(elab(x + y), M)
---------------------------------------------------------------------------
NameError Traceback (most recent call last)
<ipython-input-19-fe9483333428> in <module>()
----> 1 eval_expr(elab(x + y), M)
/home/avigad/Dropbox/Projects/Boole/git_repository/boole/semantics/value.py in eval_expr(expr, model, strict)
234 """
235 if model is None:
--> 236 m = EmptyMod
237 else:
238 m = model
NameError: global name 'elab' is not defined
In [11]:
eval_expr(elab(x * (y ** 2)), M)
Out[11]:
7
In [12]:
eval_expr(elab(t), M)
Out[12]:
7
In [13]:
local_ctxt.show()
decls:
Div_int : Div(Int, divide_int)
Le : Π([X, pred], Bool)
false : Bool
Minus_real : Minus(Real, minus_real)
divide_int : (Int) → (Int) → Int
Add_int : Add(Int, add_int)
Mul_int : Mul(Int, mul_int)
<= : Π([X, pred, le_ev], (X) → (X) → Bool)
Lt_real : Lt(Real, lt_real)
uminus_real : (Real) → Real
Add : Π([X, op], Bool)
Abs : Π([X, uop], Bool)
lt_int : (Int) → (Int) → Bool
abs_int : (Int) → Int
le_int : (Int) → (Int) → Bool
Mul : Π([X, op], Bool)
uminus_int : (Int) → Int
divide_real : (Real) → (Real) → Real
Abs_real : Abs(Real, abs_real)
Real : Type
minus_int : (Int) → (Int) → Int
% : (Int) → (Int) → Int
le_real : (Real) → (Real) → Bool
+ : Π([X, op, add_ev], (X) → (X) → X)
* : Π([X, op, mul_ev], (X) → (X) → X)
- : Π([X, op, minus_ev], (X) → (X) → X)
int_sub_real : Int ≤ Real
/ : Π([X, op, div_ev], (X) → (X) → X)
Or : (Bool) → (Bool) → Bool
Uminus : Π([X, uop], Bool)
abs : Π([X, uop, abs_ev], (X) → X)
Lt_int : Lt(Int, lt_int)
Abs_int : Abs(Int, abs_int)
Not : (Bool) → Bool
< : Π([X, pred, lt_ev], (X) → (X) → Bool)
Div_real : Div(Real, divide_real)
Minus_int : Minus(Int, minus_int)
Le_real : Le(Real, lt_real)
== : Π(X, (X) → (X) → Bool)
Uminus_int : Uminus(Int, uminus_int)
uminus : Π([X, uop, uminus_ev], (X) → X)
** : (Real) → (Real) → Real
add_real : (Real) → (Real) → Real
X : Type
Div : Π([X, op], Bool)
true : Bool
Minus : Π([X, op], Bool)
And : (Bool) → (Bool) → Bool
Uminus_real : Uminus(Real, uminus_real)
implies : (Bool) → (Bool) → Bool
minus_real : (Real) → (Real) → Real
Int : Type
Lt : Π([X, pred], Bool)
lt_real : (Real) → (Real) → Bool
add_int : (Int) → (Int) → Int
mul_int : (Int) → (Int) → Int
Mul_real : Mul(Real, mul_real)
Add_real : Add(Real, add_real)
Le_int : Le(Int, le_int)
mul_real : (Real) → (Real) → Real
abs_real : (Real) → Real
defs:
Div_int : triv()
Le : λ([X, pred], true)
Minus_real : triv()
Add_int : triv()
<= : λ([X, pred, le_ev], pred)
Lt_real : triv()
Lt : λ([X, pred], true)
Mul_int : triv()
Mul : λ([X, op], true)
Mul_real : triv()
Abs_real : triv()
Uminus_real : triv()
+ : λ([X, op, add_ev], op)
* : λ([X, op, mul_ev], op)
- : λ([X, op, minus_ev], op)
/ : λ([X, op, div_ev], op)
Uminus : λ([X, uop], true)
abs : λ([X, uop, abs_ev], uop)
Lt_int : triv()
Abs_int : triv()
< : λ([X, pred, lt_ev], pred)
Div_real : triv()
Minus_int : triv()
Le_real : triv()
== : λ([X, x, y], And(Sub(x, y), Sub(y, x)))
Uminus_int : triv()
uminus : λ([X, uop, uminus_ev], uop)
Div : λ([X, op], true)
Minus : λ([X, op], true)
implies : λ([p, q], Sub(p, q))
Add : λ([X, op], true)
Abs : λ([X, uop], true)
Add_real : triv()
Le_int : triv()
hyps:
Div_real : Div(Real, divide_real)
Div_int : Div(Int, divide_int)
Minus_int : Minus(Int, minus_int)
Minus_real : Minus(Real, minus_real)
Le_real : Le(Real, lt_real)
Add_int : Add(Int, add_int)
Uminus_int : Uminus(Int, uminus_int)
Lt_real : Lt(Real, lt_real)
Uminus_real : Uminus(Real, uminus_real)
int_sub_real : Int ≤ Real
Lt_int : Lt(Int, lt_int)
Abs_int : Abs(Int, abs_int)
Add_real : Add(Real, add_real)
Le_int : Le(Int, le_int)
Mul_int : Mul(Int, mul_int)
Mul_real : Mul(Real, mul_real)
Abs_real : Abs(Real, abs_real)
In [14]:
local_ctxt.show(['decls'])
decls:
Div_int : Div(Int, divide_int)
Le : Π([X, pred], Bool)
false : Bool
Minus_real : Minus(Real, minus_real)
divide_int : (Int) → (Int) → Int
Add_int : Add(Int, add_int)
Mul_int : Mul(Int, mul_int)
<= : Π([X, pred, le_ev], (X) → (X) → Bool)
Lt_real : Lt(Real, lt_real)
uminus_real : (Real) → Real
Add : Π([X, op], Bool)
Abs : Π([X, uop], Bool)
lt_int : (Int) → (Int) → Bool
abs_int : (Int) → Int
le_int : (Int) → (Int) → Bool
Mul : Π([X, op], Bool)
uminus_int : (Int) → Int
divide_real : (Real) → (Real) → Real
Abs_real : Abs(Real, abs_real)
Real : Type
minus_int : (Int) → (Int) → Int
% : (Int) → (Int) → Int
le_real : (Real) → (Real) → Bool
+ : Π([X, op, add_ev], (X) → (X) → X)
* : Π([X, op, mul_ev], (X) → (X) → X)
- : Π([X, op, minus_ev], (X) → (X) → X)
int_sub_real : Int ≤ Real
/ : Π([X, op, div_ev], (X) → (X) → X)
Or : (Bool) → (Bool) → Bool
Uminus : Π([X, uop], Bool)
abs : Π([X, uop, abs_ev], (X) → X)
Lt_int : Lt(Int, lt_int)
Abs_int : Abs(Int, abs_int)
Not : (Bool) → Bool
< : Π([X, pred, lt_ev], (X) → (X) → Bool)
Div_real : Div(Real, divide_real)
Minus_int : Minus(Int, minus_int)
Le_real : Le(Real, lt_real)
== : Π(X, (X) → (X) → Bool)
Uminus_int : Uminus(Int, uminus_int)
uminus : Π([X, uop, uminus_ev], (X) → X)
** : (Real) → (Real) → Real
add_real : (Real) → (Real) → Real
X : Type
Div : Π([X, op], Bool)
true : Bool
Minus : Π([X, op], Bool)
And : (Bool) → (Bool) → Bool
Uminus_real : Uminus(Real, uminus_real)
implies : (Bool) → (Bool) → Bool
minus_real : (Real) → (Real) → Real
Int : Type
Lt : Π([X, pred], Bool)
lt_real : (Real) → (Real) → Bool
add_int : (Int) → (Int) → Int
mul_int : (Int) → (Int) → Int
Mul_real : Mul(Real, mul_real)
Add_real : Add(Real, add_real)
Le_int : Le(Int, le_int)
mul_real : (Real) → (Real) → Real
abs_real : (Real) → Real
In [ ]:
Content source: avigad/boole
Similar notebooks: