chore(*): remove support for Lua
This commit is contained in:
Leonardo de Moura
parent
3de4ec1a6c
commit
f67181baf3
310 changed files with 42 additions and 12093 deletions
739
doc/lua/lua.md
739
doc/lua/lua.md
|
|
@ -1,739 +0,0 @@
|
|||
# Lua API documentation
|
||||
|
||||
We the [Lua](http://www.lua.org) script language to customize and
|
||||
extend [Lean](http://leanprover.net). This
|
||||
[link](http://www.lua.org/docs.html) is a good starting point for
|
||||
learning Lua. In this document, we focus on the Lean specific APIs.
|
||||
Most of Lean components are exposed in the Lua API.
|
||||
|
||||
**Remark:** the script [md2lua.sh](md2lua.sh) extracts the Lua code
|
||||
examples from the `*.md` documentation files in this directory.
|
||||
|
||||
## Hierarchical names
|
||||
|
||||
In Lean, we use _hierarchical names_ for identifying configuration
|
||||
options, constants, and kernel objects. A hierarchical name is
|
||||
essentially a list of strings and integers.
|
||||
The following example demonstrates how to create and manipulate
|
||||
hierarchical names using the Lua API.
|
||||
|
||||
```lua
|
||||
local x = name("x") -- create a simple hierarchical name
|
||||
local y = name("y")
|
||||
-- In Lua, 'assert(p)' succeeds if 'p' does not evaluate to false (or nil)
|
||||
assert(x == name("x")) -- test if 'x' is equal to 'name("x")'
|
||||
assert(x ~= y) -- '~=' is the not equal operator in Lua
|
||||
assert(x ~= "x")
|
||||
|
||||
assert(is_name(x)) -- test whether argument is a hierarchical name or not.
|
||||
assert(not is_name("x"))
|
||||
|
||||
local x1 = name(x, 1) -- x1 is a name composed of the string "x" and number 1
|
||||
assert(tostring(x1) == "x.1")
|
||||
assert(x1 ~= name("x.1")) -- x1 is not equal to the string x.1
|
||||
assert(x1 == name("x", 1))
|
||||
|
||||
local o = name("lean", "pp", "colors")
|
||||
-- The previous construct is syntax sugar for the following expression
|
||||
assert(o == name(name(name("lean"), "pp"), "colors"))
|
||||
|
||||
assert(x < y) -- '<' is a total order on hierarchical names
|
||||
|
||||
local h = x:hash() -- retrieve the hash code for 'x'
|
||||
assert(h ~= y:hash())
|
||||
```
|
||||
|
||||
## Lua tables
|
||||
|
||||
Tables are the only mutable, non-atomic type of data in Lua. Tables
|
||||
are used to implement mappings, arrays, lists, objects, etc. Here is a
|
||||
small examples demonstrating how to use Lua tables:
|
||||
|
||||
```lua
|
||||
local t = {} -- create an empty table
|
||||
t["x"] = 10 -- insert the entry "x" -> 10
|
||||
t.x = 20 -- syntax-sugar for t["x"] = 20
|
||||
t["y"] = 30 -- insert the entry "y" -> 30
|
||||
assert(t["x"] == 20)
|
||||
local p = { x = 10, y = 20 } -- create a table with two entries
|
||||
assert(p.x == 10)
|
||||
assert(p["x"] == 10)
|
||||
assert(p.y == 20)
|
||||
assert(p["y"] == 20)
|
||||
```
|
||||
|
||||
Arrays are implemented by indexing tables with integers.
|
||||
The arrays don't have a fixed size and grow dynamically.
|
||||
The arrays in Lua usually start at index 1. The Lua libraries
|
||||
use this convention. The following example initializes
|
||||
an array with 100 elements.
|
||||
|
||||
```lua
|
||||
local a = {} -- new array
|
||||
for i=1, 100 do
|
||||
a[i] = 0
|
||||
end
|
||||
local b = {2, 4, 6, 8, 10} -- create an array with 5 elements
|
||||
assert(#b == 5) -- array has 5 elements
|
||||
assert(b[1] == 2)
|
||||
assert(b[2] == 4)
|
||||
```
|
||||
In Lua, we cannot provide custom hash and equality functions to tables.
|
||||
So, we cannot effectively use Lua tables to implement mappings where
|
||||
the keys are Lean hierarchical names, expressions, etc.
|
||||
The following example demonstrates the issue.
|
||||
|
||||
```lua
|
||||
local m = {} -- create empty table
|
||||
local a = name("a")
|
||||
m[a] = 10 -- map the hierarchical name 'a' to 10
|
||||
assert(m[a] == 10)
|
||||
local a1 = name("a")
|
||||
assert(a == a1) -- 'a' and 'a1' are the same hierarchical name
|
||||
assert(m[a1] == nil) -- 'a1' is not a key in the mapping 'm'
|
||||
assert(m[a] == 10)
|
||||
-- 'a' and 'a1' are two instances of the same object
|
||||
-- Lua tables assume that different instances are not equal
|
||||
```
|
||||
|
||||
## Red-black tree maps
|
||||
|
||||
In Lean, we provide red-black tree maps for implementing mappings where the keys are
|
||||
Lean objects such as hierarchical names. The maps are implemented on
|
||||
top of [red-black tree data structure](http://en.wikipedia.org/wiki/Red%E2%80%93black_tree).
|
||||
We can also use Lua atomic data types as keys in these maps.
|
||||
However, we should not mix different types in the same map.
|
||||
The Lean map assumes that `<` is a total order on the
|
||||
keys inserted in the map.
|
||||
|
||||
```lua
|
||||
local m = rb_map() -- create an empty red-black tree map
|
||||
assert(is_rb_map(m))
|
||||
assert(#m == 0)
|
||||
local a = name("a", 1)
|
||||
local a1 = name("a", 1)
|
||||
m:insert(a, 10) -- add the entry 'a.1' -> 10
|
||||
assert(m:find(a1) == 10)
|
||||
m:insert(name("b"), 20)
|
||||
assert(#m == 2)
|
||||
m:erase(a) -- remove entry with key 'a.1'
|
||||
assert(m:find(a) == nil)
|
||||
assert(not m:contains(a))
|
||||
assert(#m == 1)
|
||||
m:insert(name("c"), 30)
|
||||
m:for_each( -- traverse the entries in the map
|
||||
function(k, v) -- executing the given function
|
||||
print(k, v)
|
||||
end
|
||||
)
|
||||
local m2 = m:copy() -- the maps are copied in constant time
|
||||
assert(#m2 == #m)
|
||||
m2:insert(name("b", 2), 40)
|
||||
assert(#m2 == #m + 1)
|
||||
```
|
||||
|
||||
## Multiple precision numerals
|
||||
|
||||
We expose [GMP](http://gmplib.org/) (GNU Multiple precision arithmetic
|
||||
library) in Lua. Internally, Lean uses multiple precision numerals for
|
||||
representing expressing containing numerals.
|
||||
In Lua, we can create multiple precision integers (_mpz_) and multiple
|
||||
precision rationals (_mpq_). The following example demonstrates how to
|
||||
use `mpz` and `mpq` numerals.
|
||||
|
||||
```lua
|
||||
local ten = mpz(10) -- create the mpz numeral 10.
|
||||
assert(is_mpz(ten)) -- test whether 'ten' is a mpz numeral or not
|
||||
assert(not is_mpz(10))
|
||||
local big = mpz("100000000000000000000000") -- create a mpz numeral from a string
|
||||
-- The operators +, -, *, /, ^, <, <=, >, >=, ==, ~=
|
||||
-- The operators +, -, *, /, ^ accept mixed mpz and Lua native types
|
||||
assert(ten + 1 == mpz(11))
|
||||
-- In Lua, objects of different types are always different
|
||||
-- So, the mpz number 10 is different from the native Lua numeral 10
|
||||
assert(mpz(10) ~= 10)
|
||||
assert(mpz(3) / 2 == mpz(1))
|
||||
-- The second argument of ^ must be a non-negative Lua numeral
|
||||
assert(mpz(10) ^ 100 > mpz("1000000000000000000000000"))
|
||||
assert(mpz(3) * mpz("1000000000000000000000") == mpz("3000000000000000000000"))
|
||||
assert(mpz(4) + "10" == mpz(14))
|
||||
local q1 = mpq(10) -- create the mpq numeral 10
|
||||
local q2 = q1 / 3 -- create the mpq numeral 10/3
|
||||
assert(q2 == mpq("10/3"))
|
||||
local q3 = mpq(0.25) -- create the mpq numeral 1/4
|
||||
assert(q3 == mpq(1)/4)
|
||||
assert(is_mpq(q3)) -- test whether 'q3' is a mpq numeral or not
|
||||
assert(not is_mpq(mpz(10))) -- mpz numerals are not mpq
|
||||
assert(ten == mpz(10))
|
||||
local q4 = mpq(ten) -- convert the mpz numeral 'ten' into a mpq numeral
|
||||
assert(is_mpq(q4))
|
||||
assert(mpq(1)/3 + mpq(2)/3 == mpq(1))
|
||||
assert(mpq(0.5)^5 == mpq("1/32"))
|
||||
assert(mpq(1)/2 > mpq("1/3"))
|
||||
```
|
||||
|
||||
## S-expressions
|
||||
|
||||
In Lean, we use Lisp-like non-mutable S-expressions as a basis for
|
||||
building configuration options, statistics, formatting objects, and
|
||||
other structured objects. S-expressions can be atomic values (nil, strings,
|
||||
hierarchical names, integers, doubles, Booleans, and multiple precision
|
||||
integers and rationals), or pairs (aka _cons-cell_).
|
||||
The following example demonstrates how to create S-expressions using Lua.
|
||||
|
||||
```lua
|
||||
local s = sexpr(1, 2) -- Create a pair containing the atomic values 1 and 2
|
||||
assert(is_sexpr(s)) -- 's' is a pair
|
||||
assert(s:is_cons()) -- 's' is a cons-cell/pair
|
||||
assert(s:head():is_atom()) -- the 'head' is an atomic S-expression
|
||||
assert(s:head() == sexpr(1)) -- the 'head' of 's' is the atomic S-expression 1
|
||||
assert(s:tail() == sexpr(2)) -- the 'head' of 's' is the atomic S-expression 2
|
||||
s = sexpr(1, 2, 3, nil) -- Create a 'list' containing 1, 2 and 3
|
||||
assert(s:length() == 3)
|
||||
assert(s:head() == sexpr(1))
|
||||
assert(s:tail() == sexpr(2, 3, nil))
|
||||
assert(s:head():is_int()) -- the 'head' is an integer
|
||||
assert(s:head():to_int() == 1) -- return the integer stored in the 'head' of 's'
|
||||
local h, t = s:fields() -- return the 'head' and 'tail' of s
|
||||
assert(h == sexpr(1))
|
||||
```
|
||||
|
||||
The following example demonstrates how to test the kind of and extract
|
||||
the value stored in atomic S-expressions.
|
||||
|
||||
```lua
|
||||
assert(sexpr(1):is_int())
|
||||
assert(sexpr(1):to_int() == 1)
|
||||
assert(sexpr(true):is_bool())
|
||||
assert(sexpr(false):to_bool() == false)
|
||||
assert(sexpr("hello"):is_string())
|
||||
assert(sexpr("hello"):to_string() == "hello")
|
||||
assert(sexpr(name("n", 1)):is_name())
|
||||
assert(sexpr(name("n", 1)):to_name() == name("n", 1))
|
||||
assert(sexpr(mpz(10)):is_mpz())
|
||||
assert(sexpr(mpz(10)):to_mpz() == mpz(10))
|
||||
assert(sexpr(mpq(3)/2):is_mpq())
|
||||
assert(sexpr(mpq(3)/2):to_mpq() == mpq(6)/4)
|
||||
```
|
||||
We can also use the method `fields` to extract the value stored
|
||||
in atomic S-expressions. It is more convenient than using
|
||||
the `to_*` methods.
|
||||
|
||||
```lua
|
||||
assert(sexpr(10):fields() == 10)
|
||||
assert(sexpr("hello"):fields() == "hello")
|
||||
```
|
||||
|
||||
The `to_*` methods raise an error is the argument does not match
|
||||
the expected type. Remark: in Lua, we catch errors using
|
||||
the builtin function [`pcall`](http://pgl.yoyo.org/luai/i/pcall) (aka _protected call_).
|
||||
|
||||
```lua
|
||||
local s = sexpr(10)
|
||||
local ok, ex = pcall(function() s:to_string() end)
|
||||
assert(not ok)
|
||||
-- 'ex' is a Lean exception
|
||||
assert(is_exception(ex))
|
||||
```
|
||||
|
||||
We say an S-expression `s` is a _list_ iff `s` is a pair, and the
|
||||
`tail` is nil or a list. So, every _list_ is a pair, but not every
|
||||
pair is a list.
|
||||
|
||||
```lua
|
||||
assert(sexpr(1, 2):is_cons()) -- The S-expression is a pair
|
||||
assert(not sexpr(1, 2):is_list()) -- This pair is not a list
|
||||
assert(sexpr(1, nil):is_list()) -- List with one element
|
||||
assert(sexpr(1, 2, nil):is_list()) -- List with two elements
|
||||
-- The expression sexpr(1, 2, nil) is syntax-sugar
|
||||
-- for sexpr(1, sexpr(2, nil))
|
||||
assert(sexpr(1, 2, nil) == sexpr(1, sexpr(2, nil)))
|
||||
-- The methond 'length' returns the length of the list
|
||||
assert(sexpr(1, 2, nil):length() == 2)
|
||||
```
|
||||
|
||||
We can encode trees using S-expressions. The following example
|
||||
demonstrates how to write a simple recursive function that
|
||||
collects all leaves (aka atomic values) stored in a S-expression
|
||||
tree.
|
||||
|
||||
```lua
|
||||
function collect(S)
|
||||
-- We store the result in a Lua table
|
||||
local result = {}
|
||||
function loop(S)
|
||||
if S:is_cons() then
|
||||
loop(S:head())
|
||||
loop(S:tail())
|
||||
elseif not S:is_nil() then
|
||||
result[#result + 1] = S:fields()
|
||||
end
|
||||
end
|
||||
loop(S)
|
||||
return result
|
||||
end
|
||||
-- Create a simple tree
|
||||
local tree = sexpr(sexpr(1, 5), sexpr(sexpr(4, 3), 5))
|
||||
local leaves = collect(tree) -- store the leaves in a Lua table
|
||||
assert(#leaves == 5)
|
||||
assert(leaves[1] == 1)
|
||||
assert(leaves[2] == 5)
|
||||
assert(leaves[3] == 4)
|
||||
```
|
||||
|
||||
## Options
|
||||
|
||||
Lean components can be configured used _options_ objects. The options
|
||||
can be explicitly provided or read from a global variable. An options
|
||||
object is a non-mutable value based on S-expressions.
|
||||
An options object is essentially a list of pairs, where each pair
|
||||
is a hierarchical name and a value. The following example demonstrates
|
||||
how to create options objects using Lua.
|
||||
|
||||
```lua
|
||||
-- Create an options set containing the entries
|
||||
-- pp.colors -> false,
|
||||
-- pp.unicode -> false
|
||||
local o1 = options(name("pp", "colors"), false, name("pp", "unicode"), false)
|
||||
assert(is_options(o1))
|
||||
print(o1)
|
||||
-- The same example using syntax-sugar for hierarchical names.
|
||||
-- The Lean-Lua API will automatically convert Lua arrays into hierarchical names.
|
||||
local o2 = options({"pp", "colors"}, false, {"pp", "unicode"}, false)
|
||||
print(o2)
|
||||
-- An error is raised if the option is not known.
|
||||
local ok, ex = pcall(function() options({"pp", "foo"}, true) end)
|
||||
assert(not ok)
|
||||
assert(ex:what():find("unknown option 'pp.foo'"))
|
||||
```
|
||||
|
||||
Options objects are non-mutable values. The method `update` returns a new
|
||||
updates options object.
|
||||
|
||||
```lua
|
||||
local o1 = options() -- create the empty options
|
||||
assert(o1:empty())
|
||||
local o2 = o1:update({'pp', 'colors'}, true)
|
||||
assert(o1:empty())
|
||||
assert(not o2:empty())
|
||||
assert(o2:size() == 1)
|
||||
assert(o2:get({'pp', 'colors'}) == true)
|
||||
assert(o2:get{'pp', 'colors'} == true)
|
||||
assert(o2:contains{'pp', 'colors'})
|
||||
assert(not o2:contains{'pp', 'unicode'})
|
||||
-- We can provide a default value for 'get'.
|
||||
-- The default value is used if the options object does
|
||||
-- not contain the key.
|
||||
assert(o2:get({'pp', 'width'}) == 0)
|
||||
assert(o2:get({'pp', 'width'}, 10) == 10)
|
||||
assert(o2:get({'pp', 'width'}, 20) == 20)
|
||||
local o3 = o2:update({'pp', 'width'}, 100)
|
||||
assert(o3:get({'pp', 'width'}) == 100)
|
||||
assert(o3:get({'pp', 'width'}, 1) == 100)
|
||||
assert(o3:get({'pp', 'width'}, 20) == 100)
|
||||
```
|
||||
|
||||
The functions `get_options` and `set_options` get/set the global
|
||||
options object. For example, the global options object is used
|
||||
by the `print` method.
|
||||
|
||||
```lua
|
||||
local o = options({'pp', 'unicode'}, false)
|
||||
set_options(o)
|
||||
assert(get_options():contains{'pp', 'unicode'})
|
||||
```
|
||||
|
||||
# Universe levels
|
||||
|
||||
Lean supports universe polymorphism. That is, declaration in Lean can
|
||||
be parametrized by one or more universe level parameters.
|
||||
The declarations can then be instantiated with universe level
|
||||
expressions. In the standard Lean front-end, universe levels can be
|
||||
omitted, and the Lean elaborator (tries) to infer them automatically
|
||||
for users. In this section, we describe the API for creating and using
|
||||
universe level expressions.
|
||||
|
||||
In Lean, we have a hierarchy of universes: `Type.{0}` : `Type.{1}` :
|
||||
`Type.{2}`, ...
|
||||
We do not assume our universes are cumulative (like Coq).
|
||||
In Lean, when we create an empty environment, we can specify whether
|
||||
`Type.{0}` is impredicative or not. The idea is to be able to use
|
||||
`Type.{0}` to represent the universe of Propositions.
|
||||
|
||||
In Lean, we have the following kinds of universe level expression:
|
||||
- `Zero` : the universe level expression for representing `Type.{0}`.
|
||||
- `Succ(l)` : the successor of universe level `l`.
|
||||
- `Max(l1, l2)` : the maximum of levels `l1` and `l2`.
|
||||
- `IMax(l1, l2)` : the "impredicative" maximum. It is defined as
|
||||
`IMax(x, y) = Zero` if `y` is `Zero`, and `Max(x, y)` otherwise.
|
||||
- `Param(n)` : a universe level parameter named `n`.
|
||||
- `Global(n)` : a global universe level named `n`.
|
||||
- `Meta(n)` : a meta universe level named `n`. Meta universe
|
||||
levels are used to identify placeholders that must be automatically
|
||||
constructed by Lean.
|
||||
|
||||
The following example demonstrates how to create universe level
|
||||
expressions using Lua.
|
||||
|
||||
```lua
|
||||
local zero = level() -- Create level Zero
|
||||
assert(is_level(zero)) -- zero is a level expression
|
||||
assert(zero:is_zero())
|
||||
local one = zero + 1 -- Create level One
|
||||
assert(one ~= 1) -- level one is not the constant 1
|
||||
-- We can also use the API mk_level_succ instead of +1
|
||||
local two = mk_level_succ(one) -- Create level Two
|
||||
assert(two == one+1)
|
||||
assert(two:is_succ()) -- two is of the kind: successor
|
||||
assert(two:succ_of() == one) -- it is the successor of one
|
||||
local u = mk_global_univ("u") -- u is a reference to global universe level "u"
|
||||
assert(u:is_global())
|
||||
assert(u:id() == name("u")) -- Retrieve u's name
|
||||
local l = mk_param_univ("l") -- l is a reference to a universe level parameter
|
||||
assert(l:is_param())
|
||||
assert(l:id() == name("l"))
|
||||
assert(l:id() ~= "l") -- The names are not strings, but hierarchical names
|
||||
assert(l:kind() == level_kind.Param)
|
||||
local m = mk_meta_univ("m") -- Create a meta universe level named "m"
|
||||
assert(m:is_meta())
|
||||
assert(m:id() == name("m"))
|
||||
print(max_univ(l, u)) -- Create level expression Max(l, u)
|
||||
assert(max_univ(l, u):is_max())
|
||||
-- The max_univ API applies basic coercions automatically
|
||||
assert(max_univ("l", 1) == max_univ(l, one))
|
||||
assert(max_univ("l", 1, u) == max_univ(l, max_univ(one, u)))
|
||||
-- The max_univ API applies basic simplifications automatically
|
||||
assert(max_univ(l, l) == l)
|
||||
assert(max_univ(l, zero) == l)
|
||||
assert(max_univ(one, zero) == one)
|
||||
print(imax_univ(l, u)) -- Create level expression IMax(l, u)
|
||||
assert(imax_univ(l, u):is_imax())
|
||||
-- The imax_univ API also applies basic coercions automatically
|
||||
assert(imax_univ(1, "l") == imax_univ(one, l))
|
||||
-- The imax_univ API applies basic simplifications automatically
|
||||
assert(imax_univ(l, l) == l)
|
||||
assert(imax_univ(l, zero) == zero)
|
||||
-- It "knows" that u+1 can never be zero
|
||||
assert(imax_univ(l, u+1) == max_univ(l, u+1))
|
||||
assert(imax_univ(zero, one) == one)
|
||||
assert(imax_univ(one, zero) == zero)
|
||||
-- The methods lhs and rhs deconstruct max and imax expressions
|
||||
assert(max_univ(l, u):lhs() == l)
|
||||
assert(imax_univ(l, u):rhs() == u)
|
||||
-- The method is_not_zero if there if for all assignments
|
||||
-- of the parameters, globals and meta levels, the resultant
|
||||
-- level expression is different from zero.
|
||||
assert((l+1):is_not_zero())
|
||||
assert(not l:is_not_zero())
|
||||
assert(max_univ(l+1, u):is_not_zero())
|
||||
-- The method instantiate replaces parameters with level expressions
|
||||
assert(max_univ(l, u):instantiate({"l"}, {two}) == max_univ(two, u))
|
||||
local l1 = mk_param_univ("l1")
|
||||
assert(max_univ(l, l1):instantiate({"l", "l1"}, {two, u+1}) == max_univ(two, u+1))
|
||||
-- The method has_meta returns true, if the given level expression
|
||||
-- contains meta levels
|
||||
assert(max_univ(m, l):has_meta())
|
||||
assert(not max_univ(u, l):has_meta())
|
||||
-- The is_eqp method checks for pointer equality
|
||||
local e1 = max_univ(l, u)
|
||||
local e2 = max_univ(l, u)
|
||||
assert(e1 == e2)
|
||||
local e3 = e1
|
||||
-- e1 and e3 are references to the same level expression.
|
||||
assert(e1:is_eqp(e3))
|
||||
```
|
||||
|
||||
In the previous example, we learned that functions such as `max_univ`
|
||||
apply basic simplifications automatically. However, they do not put
|
||||
the level expressions in any normal form. We can use the method
|
||||
`normalize` for that. The normalization procedure is also use to
|
||||
implement the method `is_equivalent` that returns true when two level
|
||||
expressions are equivalent. The Lua API also contains the method
|
||||
`is_geq` that can be used to check whether a level expression
|
||||
represents a universe bigger than or equal another one.
|
||||
|
||||
```lua
|
||||
local zero = level()
|
||||
local l = mk_param_univ("l")
|
||||
local u = mk_global_univ("u")
|
||||
assert(max_univ(l, 1, u+1):is_equivalent(max_univ(u+1, 1, l)))
|
||||
local e1 = max_univ(l, u+1)+1
|
||||
assert(e1:normalize() == max_univ(l+1, u+2))
|
||||
-- norm is syntax sugar for normalize
|
||||
assert(e1:norm() == max_univ(l+1, u+2))
|
||||
assert(e1:is_geq(l))
|
||||
assert(e1:is_geq(e1))
|
||||
assert(e1:is_geq(zero))
|
||||
assert(e1:is_geq(u+2))
|
||||
assert(e1:is_geq(max_univ(l, u)))
|
||||
```
|
||||
|
||||
We say a universe level is _explicit_ iff it is of the form
|
||||
`succ^k(zero)`
|
||||
|
||||
```lua
|
||||
local zero = level()
|
||||
assert(zero:is_explicit())
|
||||
local two = zero+2
|
||||
assert(two:is_explicit())
|
||||
local l = mk_param_univ("l")
|
||||
assert(not l:is_explicit())
|
||||
```
|
||||
|
||||
The Lua dictionary `level_kind` contains the id for all universe level
|
||||
kinds.
|
||||
|
||||
```lua
|
||||
local zero = level()
|
||||
local one = zero+1
|
||||
local l = mk_param_univ("l")
|
||||
local u = mk_global_univ("u")
|
||||
local m = mk_meta_univ("m")
|
||||
local e1 = max_univ(l, u)
|
||||
local e2 = imax_univ(m, l)
|
||||
assert(zero:kind() == level_kind.Zero)
|
||||
assert(one:kind() == level_kind.Succ)
|
||||
assert(l:kind() == level_kind.Param)
|
||||
assert(u:kind() == level_kind.Global)
|
||||
assert(m:kind() == level_kind.Meta)
|
||||
assert(e1:kind() == level_kind.Max)
|
||||
assert(e2:kind() == level_kind.IMax)
|
||||
```
|
||||
|
||||
# Expressions
|
||||
|
||||
In Lean, we have the following kind of expressions: constants,
|
||||
function applications, variables, lambdas, dependent function spaces
|
||||
(aka Pis), let expressions, and sorts (aka Type).
|
||||
There are three additional kinds of auxiliary
|
||||
expressions: local constants, metavariables, and macros.
|
||||
|
||||
## Constants
|
||||
|
||||
Constants are essentially references to declarations in the
|
||||
environment. We can create a variable using
|
||||
|
||||
```lua
|
||||
local f = mk_constant("f")
|
||||
local a = Const("a") -- Const is an alias for mk_constant
|
||||
assert(is_expr(f)) -- f is an expression
|
||||
assert(f:is_constant()) -- f is a constant
|
||||
```
|
||||
Lean supports universe polymorphism. When we define a constant,
|
||||
theorem or axiom, we can use universe level parameters.
|
||||
Thus, if a declaration `g` has two universe level parameters,
|
||||
we instantiate them when we create a reference to `g`.
|
||||
|
||||
```lua
|
||||
local zero = level()
|
||||
local one = zero+1
|
||||
local g01 = mk_constant("g", {zero, one})
|
||||
```
|
||||
|
||||
The command `mk_constant` automatically applies coercions to level
|
||||
expressions. A numeral `n` is automatically converted into
|
||||
`level()+n`, and a string `s` into `mk_param_univ(s)`.
|
||||
|
||||
```lua
|
||||
local g1l = mk_constant("g", {1, "l"})
|
||||
```
|
||||
|
||||
The method `data()` retrieves the name and universe levels of a
|
||||
constant.
|
||||
|
||||
```lua
|
||||
local gl1 = mk_constant("g", {"l", 1})
|
||||
assert(gl1:is_constant())
|
||||
local n, ls = gl1:data()
|
||||
assert(n == name("g"))
|
||||
assert(#ls == 2)
|
||||
assert(ls:head() == mk_param_univ("l"))
|
||||
assert(ls:tail():head() == level()+1)
|
||||
```
|
||||
|
||||
## Function applications
|
||||
|
||||
In Lean, the expression `f t` is a function application, where `f` is
|
||||
a function that is applied to `t`.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local t = Const("t")
|
||||
local a = f(t) -- Creates the term `f t`
|
||||
assert(is_expr(a))
|
||||
assert(a:is_app())
|
||||
```
|
||||
|
||||
The method `data()` retrieves the function and argument of an
|
||||
application. The methods `fn()` and `arg()` retrieve the function
|
||||
and argument respectively.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local t = Const("t")
|
||||
local a = f(t)
|
||||
assert(a:fn() == f)
|
||||
assert(a:arg() == t)
|
||||
local g, b = a:data()
|
||||
assert(g == f)
|
||||
assert(b == t)
|
||||
```
|
||||
As usual, we write `f t s` to denote the expression
|
||||
`((f t) s)`. The Lua API provides a similar convenience.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local t = Const("t")
|
||||
local s = Const("s")
|
||||
local a = f(t, s)
|
||||
assert(a:fn() == f(t))
|
||||
assert(a:fn():fn() == f)
|
||||
assert(a:fn():arg() == t)
|
||||
assert(a:arg() == s)
|
||||
```
|
||||
|
||||
## Variables
|
||||
|
||||
Variables are references to local declarations in lambda and Pi
|
||||
expressions. The variables are represented using
|
||||
[de Bruijn indices](http://en.wikipedia.org/wiki/De_Bruijn_index).
|
||||
|
||||
```lua
|
||||
local x = mk_var(0)
|
||||
local y = Var(1) -- Var is an alias for mk_var
|
||||
assert(is_expr(x))
|
||||
assert(x:is_var())
|
||||
assert(x:data() == 0)
|
||||
assert(y:data() == 1)
|
||||
```
|
||||
|
||||
## Lambda abstractions
|
||||
|
||||
Lambda abstraction is a converse operation to function
|
||||
application. Given a variable `x`, a type `A`, and a term `t` that may or
|
||||
may not contain `x`, one can construct the so-called lambda abstraction
|
||||
`fun x : A, t`, or using unicode notation `λ x : A, t`.
|
||||
There are many APIs for creating lambda abstractions in the Lua API.
|
||||
The most basic one is `mk_lambda(x, A, t)`, where `x` is a string or
|
||||
hierarchical name, and `A` and `t` are expressions.
|
||||
|
||||
```lua
|
||||
local x = Var(0)
|
||||
local A = Const("A")
|
||||
local id = mk_lambda("x", A, x) -- create the identity function
|
||||
assert(is_expr(id))
|
||||
assert(id:is_lambda())
|
||||
```
|
||||
|
||||
As usual, the method `data()` retrieves the "fields" of a lambda
|
||||
abstraction.
|
||||
|
||||
```lua
|
||||
-- id is the identity function defined above.
|
||||
local y, B, v = id:data()
|
||||
assert(y == name("x"))
|
||||
assert(B == A)
|
||||
assert(v == Var(0))
|
||||
```
|
||||
|
||||
We say a variable is _free_ if it is not bound by any lambda (or Pi)
|
||||
abstraction. We say an expression is _closed_ if it does not contain
|
||||
free variables. The method `closed()` return `true` iff the expression
|
||||
is closed.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local N = Const("N")
|
||||
assert(not f(Var(0)):closed())
|
||||
local l1 = mk_lambda("x", N, f(Var(0)))
|
||||
assert(l1:closed())
|
||||
local l2 = mk_lambda("x", N, f(Var(1)))
|
||||
assert(not l2:closed())
|
||||
```
|
||||
|
||||
The method `has_free_var(i)` return `true` if the expression contains
|
||||
the free variable `i`.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local N = Const("N")
|
||||
assert(f(Var(0)):has_free_var(0))
|
||||
assert(not f(Var(0)):has_free_var(1))
|
||||
local l1 = mk_lambda("x", N, f(Var(0)))
|
||||
assert(not l1:has_free_var(0))
|
||||
local l2 = mk_lambda("x", N, f(Var(1)))
|
||||
assert(l2:has_free_var(0))
|
||||
assert(not l2:has_free_var(1))
|
||||
```
|
||||
|
||||
The de Bruijn indices can be lifted and lowered using the methods
|
||||
`lift_free_vars` and `lower_free_vars`.
|
||||
|
||||
```lua
|
||||
local f = Const("f")
|
||||
local N = Const("N")
|
||||
assert(f(Var(0)):lift_free_vars(1) == f(Var(1)))
|
||||
assert(f(Var(0)):lift_free_vars(2) == f(Var(2)))
|
||||
-- lift the free variables >= 2 by 3
|
||||
assert(f(Var(0), Var(2)):lift_free_vars(2, 3) == f(Var(0), Var(5)))
|
||||
|
||||
assert(f(Var(1)):lower_free_vars(1) == f(Var(0)))
|
||||
assert(f(Var(2)):lower_free_vars(1) == f(Var(1)))
|
||||
-- lower the free variables >= 2 by 1
|
||||
assert(f(Var(0), Var(2)):lower_free_vars(2, 1) ==
|
||||
f(Var(0), Var(1)))
|
||||
```
|
||||
|
||||
It is not convenient to create complicated lambda abstractions using
|
||||
de Bruijn indices. It is usually a very error-prone task.
|
||||
To simplify the creation of lambda abstractions, Lean provides local constants.
|
||||
A local constant is essentially a pair name and expression, where the
|
||||
expression represents the type of the local constant.
|
||||
The API `Fun(c, b)` automatically replace the local constant `c` in `b` with
|
||||
the variable 0. It does all necessary adjustments when `b` contains nested
|
||||
lambda abstractions. The API also provides `Fun(c_1, ..., c_n, b)` as
|
||||
syntax-sugar for `Fun(c_1, ..., Fun(c_n, b)...)`.
|
||||
|
||||
```lua
|
||||
local N = Const("N")
|
||||
local f = Const("f")
|
||||
local c_1 = Local("c_1", N)
|
||||
local c_2 = Local("c_2", N)
|
||||
local c_3 = Local("c_3", N)
|
||||
assert(Fun(c_1, f(c_1)) == mk_lambda("c_1", N, f(Var(0))))
|
||||
assert(Fun(c_1, c_2, f(c_1, c_2)) ==
|
||||
mk_lambda("c_1", N, mk_lambda("c_2", N, f(Var(1), Var(0)))))
|
||||
assert(Fun(c_1, c_2, f(c_1, Fun(c_3, f(c_2, c_3)))) ==
|
||||
mk_lambda("c_1", N, mk_lambda("c_2", N,
|
||||
f(Var(1), mk_lambda("c_3", N, f(Var(1), Var(0)))))))
|
||||
````
|
||||
|
||||
Local constants can be annotated with `hints` for the Lean _elaborator_.
|
||||
For example, we can say a binder is an _implicit argument_, and
|
||||
must be inferred automatically by the elaborator.
|
||||
These annotations are irrelevant from the kernel's point of view,
|
||||
and they are just "propagated" by the Lean type checker.
|
||||
The other annotations are explained later in the Section describing
|
||||
the elaboration engine.
|
||||
|
||||
```lua
|
||||
local b = binder_info(true)
|
||||
assert(is_binder_info(b))
|
||||
assert(b:is_implicit())
|
||||
local N = Const("N")
|
||||
local f = Const("f")
|
||||
local c1 = Local("c1", N, b)
|
||||
local c2 = Local("c2", N)
|
||||
-- Create the expression
|
||||
-- fun {c1 : N} (c2 : N), (f c1 c2)
|
||||
-- In Lean, curly braces are used to denote
|
||||
-- implicit arguments
|
||||
local l = Fun(c1, c2, f(c1, c2))
|
||||
local x, T, B, bi = l:data()
|
||||
assert(x == name("c1"))
|
||||
assert(T == N)
|
||||
assert(B == Fun(c2, f(Var(1), c2)))
|
||||
assert(bi:is_implicit())
|
||||
local y, T, C, bi2 = B:data()
|
||||
assert(not bi2:is_implicit())
|
||||
```
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
#!/usr/bin/awk -f
|
||||
BEGIN{ in_block = 0 }
|
||||
!/```/{ if (in_block == 1) print $0; else print "" }
|
||||
/```/{ in_block = 0; print "" }
|
||||
/```lua/{ in_block = 1; print "" }
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Test is all examples in the .md files are working
|
||||
if [ $# -ne 1 ]; then
|
||||
echo "Usage: test.sh [lean-executable-path]"
|
||||
exit 1
|
||||
fi
|
||||
ulimit -s unlimited
|
||||
LEAN=$1
|
||||
NUM_ERRORS=0
|
||||
for f in `ls *.md`; do
|
||||
echo "-- testing $f"
|
||||
awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' "$f" > "$f.lua"
|
||||
if "$LEAN" "$f.lua" > "$f.produced.out"; then
|
||||
echo "-- worked"
|
||||
else
|
||||
echo "ERROR executing $f.lua, produced output is at $f.produced.out"
|
||||
NUM_ERRORS=$(($NUM_ERRORS+1))
|
||||
fi
|
||||
done
|
||||
if [ $NUM_ERRORS -gt 0 ]; then
|
||||
echo "-- Number of errors: $NUM_ERRORS"
|
||||
exit 1
|
||||
else
|
||||
echo "-- Passed"
|
||||
exit 0
|
||||
fi
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Test is all examples in the .md files are working
|
||||
if [ $# -ne 2 ]; then
|
||||
echo "Usage: test.sh [lean-executable-path] [file]"
|
||||
exit 1
|
||||
fi
|
||||
ulimit -s unlimited
|
||||
LEAN=$1
|
||||
f=$2
|
||||
echo "-- testing $f"
|
||||
awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' "$f" > "$f.lua"
|
||||
if "$LEAN" "$f.lua" > "$f.produced.out"; then
|
||||
echo "-- worked"
|
||||
exit 0
|
||||
else
|
||||
echo "ERROR executing $f.lua, produced output:"
|
||||
cat "$f.produced.out"
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -1,125 +0,0 @@
|
|||
-- Given a term t that does not contain global universe levels,
|
||||
-- This procedure produces a new environment based on env, but
|
||||
-- without using universe polymorphism. The optional argument
|
||||
-- def_level is used to instantiate global universe levels used
|
||||
-- in the definitions t depends on.
|
||||
function elim_univ_poly(env, t, def_level)
|
||||
if not def_level then
|
||||
-- If def_level is not provided, set it to universe 1.
|
||||
def_level = level()+1
|
||||
end
|
||||
|
||||
-- Create the new environment
|
||||
local new_env = environment()
|
||||
-- Already processed definitions
|
||||
local map = rb_map()
|
||||
|
||||
-- TODO(Leo): convert inductive datatypes.
|
||||
|
||||
-- Return a new (based on n) that is not used in new_env
|
||||
function mk_name(n)
|
||||
local i = 1
|
||||
local r = n
|
||||
while new_env:find(r) do
|
||||
r = name(n, i)
|
||||
i = i + 1
|
||||
end
|
||||
return r
|
||||
end
|
||||
|
||||
-- Instantiate the declaration decl from env using the levels ls,
|
||||
-- and add it to new_env. Return the name of this instance in new_env.
|
||||
function process_declaration(decl, ls)
|
||||
local new_name = mk_name(decl:name())
|
||||
local ps = decl:univ_params()
|
||||
local new_type = process_expr(decl:type(), ps, ls)
|
||||
local new_decl
|
||||
if decl:is_axiom() then
|
||||
new_decl = mk_axiom(new_name, new_type)
|
||||
elseif decl:is_var_decl() then
|
||||
new_decl = mk_var_decl(new_name, new_type)
|
||||
else
|
||||
local new_value = process_expr(decl:type(), ps, ls)
|
||||
if decl:is_theorem() then
|
||||
new_decl = mk_theorem(new_name, new_type, new_value)
|
||||
else
|
||||
-- TODO(Leo): expose update_declaration functions in the
|
||||
-- Lua API.
|
||||
local attrs = {opaque=decl:opaque(),
|
||||
weight=decl:weight(),
|
||||
module_idx=decl:module_idx(),
|
||||
use_conv_opt=decl:use_conv_opt()}
|
||||
new_decl = mk_definition(new_name, new_type, new_value, attrs)
|
||||
end
|
||||
end
|
||||
new_env = add_decl(new_env, new_decl)
|
||||
return new_name
|
||||
end
|
||||
|
||||
-- Convert a constant from env into a constant for new_env
|
||||
function process_constant(e)
|
||||
if e:is_constant() then
|
||||
local n, ls = e:data()
|
||||
local new_e = map:find(e)
|
||||
if new_e then
|
||||
-- constant was already mapped to new_env
|
||||
return new_e
|
||||
else
|
||||
local decl = env:find(n)
|
||||
if not decl then
|
||||
error("undefined constant '" .. n .. "'")
|
||||
end
|
||||
local new_name = process_declaration(decl, ls)
|
||||
local new_e = mk_constant(new_name)
|
||||
map:insert(e, new_e)
|
||||
return new_e
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
-- Convert the expression e from env to new_env.
|
||||
-- The universe level parameters ps are instantiated with
|
||||
-- the explicit universe levels ls
|
||||
function process_expr(e, ps, ls)
|
||||
local new_e = e:instantiate_levels(ps, ls)
|
||||
-- replace all constants occurring in new_env with the
|
||||
-- corresponding ones from env
|
||||
return new_e:replace(process_constant)
|
||||
end
|
||||
|
||||
-- Convert all constants occurring in t, and return the new environment.
|
||||
local new_t = process_expr(t, {}, {})
|
||||
return new_env, new_t
|
||||
end
|
||||
|
||||
function display_env(env)
|
||||
env:for_each(function(d)
|
||||
print(tostring(d:name()) .. " : " .. tostring(d:type()))
|
||||
end)
|
||||
end
|
||||
|
||||
function example1()
|
||||
local env = environment()
|
||||
local l = mk_param_univ("l")
|
||||
local v = mk_param_univ("v")
|
||||
local A = Local("A", mk_sort(l))
|
||||
local a = Local("a", A)
|
||||
env = add_decl(env, mk_var_decl("eq", {l}, Pi(A, mk_arrow(A, A, Bool))))
|
||||
env = add_decl(env, mk_var_decl("group", {l}, mk_sort(l+1)))
|
||||
env = add_decl(env, mk_var_decl("prod", {l, v}, mk_arrow(mk_sort(l), mk_sort(v), mk_sort(max_univ(l, v)))))
|
||||
local eq2 = Const("eq", {2})
|
||||
local group1 = Const("group", {1})
|
||||
local group2 = Const("group", {2})
|
||||
local prod1 = Const("prod", {2, 3})(group1, group2)
|
||||
env:type_check(prod1) -- Type check prod1
|
||||
local prod2 = Const("prod", {3, 0})(prod1, eq2(Type, Bool, Bool))
|
||||
env:type_check(prod2) -- Type check prod1
|
||||
|
||||
local new_env, new_prod2 = elim_univ_poly(env, prod2)
|
||||
print("converted term: " .. tostring(new_prod2))
|
||||
print("converted environment: ")
|
||||
display_env(new_env)
|
||||
new_env:type_check(new_prod2)
|
||||
end
|
||||
|
||||
example1()
|
||||
|
|
@ -269,27 +269,6 @@ if(NOT "${EMSCRIPTEN}" AND NOT "${TCMALLOC_FOUND}" AND NOT "${JEMALLOC_FOUND}" A
|
|||
endif()
|
||||
endif()
|
||||
|
||||
# Lua
|
||||
find_package(Lua REQUIRED)
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} ${LUA_LIBRARIES})
|
||||
if(NOT "${EMSCRIPTEN}" AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux")
|
||||
# Lua static library for linux depends on dl.so
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} -ldl)
|
||||
endif()
|
||||
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${LUA_INCLUDE_DIR}")
|
||||
if (HAS_LUA_NEWSTATE)
|
||||
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_NEWSTATE")
|
||||
endif()
|
||||
|
||||
IF(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" AND ${LUA_FOUND} AND
|
||||
"${LUA_INCLUDE_DIR}" MATCHES "jit")
|
||||
# http://luajit.org/install.html
|
||||
# If you're building a 64 bit application on OSX which links
|
||||
# directly or indirectly against LuaJIT, you need to link your main
|
||||
# executable with these flags:
|
||||
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -pagezero_size 10000 -image_base 100000000")
|
||||
ENDIF()
|
||||
|
||||
# Python
|
||||
find_package(PythonInterp REQUIRED)
|
||||
|
||||
|
|
@ -375,8 +354,6 @@ add_subdirectory(compiler)
|
|||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
|
||||
add_subdirectory(frontends/lean)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lean_frontend>)
|
||||
add_subdirectory(frontends/lua)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:leanlua>)
|
||||
add_subdirectory(init)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:init>)
|
||||
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
|
||||
|
|
@ -556,7 +533,7 @@ endif()
|
|||
if(STATIC)
|
||||
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "python")
|
||||
else()
|
||||
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libmpfr-dev,liblua5.2-dev,python")
|
||||
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libmpfr-dev,python")
|
||||
endif()
|
||||
SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover")
|
||||
SET(CPACK_DEBIAN_PACKAGE_SECTION "devel")
|
||||
|
|
|
|||
|
|
@ -1,20 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <iostream>
|
||||
#include <memory>
|
||||
#include <cstdlib>
|
||||
#include <lua.hpp>
|
||||
|
||||
static void * lua_realloc(void *, void * q, size_t, size_t sz) { return realloc(q, sz); }
|
||||
|
||||
// Little program for checking whether lua_newstate is available
|
||||
int main() {
|
||||
lua_State * L;
|
||||
L = lua_newstate(lua_realloc, 0);
|
||||
lua_close(L);
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1,137 +0,0 @@
|
|||
# Locate Lua library
|
||||
# This module defines
|
||||
# LUA_EXECUTABLE, if found
|
||||
# LUA_FOUND, if false, do not try to link to Lua
|
||||
# LUA_LIBRARIES
|
||||
# LUA_INCLUDE_DIR, where to find lua.h
|
||||
# LUA_VERSION_STRING, the version of Lua found (since CMake 2.8.8)
|
||||
#
|
||||
# Note that the expected include convention is
|
||||
# #include "lua.h"
|
||||
# and not
|
||||
# #include <lua/lua.h>
|
||||
# This is because, the lua location is not standardized and may exist
|
||||
# in locations other than lua/
|
||||
|
||||
#=============================================================================
|
||||
# Copyright 2007-2009 Kitware, Inc.
|
||||
# Modified to support Lua 5.2 by LuaDist 2012
|
||||
#
|
||||
# Distributed under the OSI-approved BSD License (the "License");
|
||||
# see accompanying file Copyright.txt for details.
|
||||
#
|
||||
# This software is distributed WITHOUT ANY WARRANTY; without even the
|
||||
# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
|
||||
# See the License for more information.
|
||||
#=============================================================================
|
||||
# (To distribute this file outside of CMake, substitute the full
|
||||
# License text for the above reference.)
|
||||
#
|
||||
# The required version of Lua can be specified using the
|
||||
# standard syntax, e.g. FIND_PACKAGE(Lua 5.1)
|
||||
# Otherwise the module will search for any available Lua implementation
|
||||
|
||||
# Always search for non-versioned lua first (recommended)
|
||||
SET(_POSSIBLE_LUA_INCLUDE include include/lua)
|
||||
SET(_POSSIBLE_LUA_EXECUTABLE lua)
|
||||
SET(_POSSIBLE_LUA_LIBRARY lua)
|
||||
|
||||
# Determine possible naming suffixes (there is no standard for this)
|
||||
IF(Lua_FIND_VERSION_MAJOR AND Lua_FIND_VERSION_MINOR)
|
||||
SET(_POSSIBLE_SUFFIXES "${Lua_FIND_VERSION_MAJOR}${Lua_FIND_VERSION_MINOR}" "${Lua_FIND_VERSION_MAJOR}.${Lua_FIND_VERSION_MINOR}" "-${Lua_FIND_VERSION_MAJOR}.${Lua_FIND_VERSION_MINOR}")
|
||||
ELSE(Lua_FIND_VERSION_MAJOR AND Lua_FIND_VERSION_MINOR)
|
||||
SET(_POSSIBLE_SUFFIXES "52" "5.2" "-5.2" "51" "5.1" "-5.1" "jit-2.0" "jit-5.1")
|
||||
ENDIF(Lua_FIND_VERSION_MAJOR AND Lua_FIND_VERSION_MINOR)
|
||||
|
||||
# Set up possible search names and locations
|
||||
FOREACH(_SUFFIX ${_POSSIBLE_SUFFIXES})
|
||||
LIST(APPEND _POSSIBLE_LUA_INCLUDE "include/lua${_SUFFIX}")
|
||||
LIST(APPEND _POSSIBLE_LUA_EXECUTABLE "lua${_SUFFIX}")
|
||||
LIST(APPEND _POSSIBLE_LUA_LIBRARY "lua${_SUFFIX}")
|
||||
ENDFOREACH(_SUFFIX)
|
||||
|
||||
# Find the lua executable
|
||||
FIND_PROGRAM(LUA_EXECUTABLE
|
||||
NAMES ${_POSSIBLE_LUA_EXECUTABLE}
|
||||
)
|
||||
|
||||
# Find the lua header
|
||||
FIND_PATH(LUA_INCLUDE_DIR lua.h
|
||||
HINTS
|
||||
$ENV{LUA_DIR}
|
||||
PATH_SUFFIXES ${_POSSIBLE_LUA_INCLUDE}
|
||||
PATHS
|
||||
~/Library/Frameworks
|
||||
/Library/Frameworks
|
||||
/usr/local
|
||||
/usr
|
||||
/sw # Fink
|
||||
/opt/local # DarwinPorts
|
||||
/opt/csw # Blastwave
|
||||
/opt
|
||||
)
|
||||
|
||||
# Find the lua library
|
||||
FIND_LIBRARY(LUA_LIBRARY
|
||||
NAMES ${_POSSIBLE_LUA_LIBRARY}
|
||||
HINTS
|
||||
$ENV{LUA_DIR}
|
||||
PATH_SUFFIXES lib64 lib
|
||||
PATHS
|
||||
~/Library/Frameworks
|
||||
/Library/Frameworks
|
||||
/usr/local
|
||||
/usr
|
||||
/sw
|
||||
/opt/local
|
||||
/opt/csw
|
||||
/opt
|
||||
)
|
||||
|
||||
IF(LUA_LIBRARY)
|
||||
# include the math library for Unix
|
||||
IF(UNIX AND NOT APPLE)
|
||||
FIND_LIBRARY(LUA_MATH_LIBRARY m)
|
||||
SET( LUA_LIBRARIES "${LUA_LIBRARY};${LUA_MATH_LIBRARY}" CACHE STRING "Lua Libraries")
|
||||
# For Windows and Mac, don't need to explicitly include the math library
|
||||
ELSE(UNIX AND NOT APPLE)
|
||||
SET( LUA_LIBRARIES "${LUA_LIBRARY}" CACHE STRING "Lua Libraries")
|
||||
ENDIF(UNIX AND NOT APPLE)
|
||||
ENDIF(LUA_LIBRARY)
|
||||
|
||||
# Determine Lua version
|
||||
IF(LUA_INCLUDE_DIR AND EXISTS "${LUA_INCLUDE_DIR}/lua.h")
|
||||
FILE(STRINGS "${LUA_INCLUDE_DIR}/lua.h" lua_version_str REGEX "^#define[ \t]+LUA_RELEASE[ \t]+\"Lua .+\"")
|
||||
|
||||
STRING(REGEX REPLACE "^#define[ \t]+LUA_RELEASE[ \t]+\"Lua ([^\"]+)\".*" "\\1" LUA_VERSION_STRING "${lua_version_str}")
|
||||
UNSET(lua_version_str)
|
||||
ENDIF()
|
||||
|
||||
INCLUDE(FindPackageHandleStandardArgs)
|
||||
# handle the QUIETLY and REQUIRED arguments and set LUA_FOUND to TRUE if
|
||||
# all listed variables are TRUE
|
||||
FIND_PACKAGE_HANDLE_STANDARD_ARGS(Lua
|
||||
REQUIRED_VARS LUA_LIBRARIES LUA_INCLUDE_DIR
|
||||
VERSION_VAR LUA_VERSION_STRING)
|
||||
|
||||
MARK_AS_ADVANCED(LUA_INCLUDE_DIR LUA_LIBRARIES LUA_LIBRARY LUA_MATH_LIBRARY LUA_EXECUTABLE)
|
||||
|
||||
# Print out version number
|
||||
if (LUA_FOUND)
|
||||
if (CMAKE_CROSSCOMPILING)
|
||||
message(STATUS "Cross-compiling: can't find whether lua_objlen or lua_newstate is available.")
|
||||
else()
|
||||
try_run(LUA_CHECK LUA_CHECK_BUILD
|
||||
${LEAN_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp
|
||||
${LEAN_SOURCE_DIR}/cmake/Modules/CheckLuaNewstate.cc
|
||||
CMAKE_FLAGS -DINCLUDE_DIRECTORIES=${LUA_INCLUDE_DIR}
|
||||
-DLINK_LIBRARIES=${LUA_LIBRARIES}
|
||||
RUN_OUTPUT_VARIABLE LUA_TRY_OUT)
|
||||
if ("${LUA_CHECK}" MATCHES "0" AND "${LUA_CHECK_BUILD}$" MATCHES "TRUE")
|
||||
message(STATUS "lua_newstate works")
|
||||
set(HAS_LUA_NEWSTATE TRUE)
|
||||
else()
|
||||
message(STATUS "lua_newstate is not supported by your Lua engine, Lean will not be able to track memory consumed by the Lua engine")
|
||||
endif()
|
||||
endif()
|
||||
endif ()
|
||||
|
|
@ -1,8 +1,8 @@
|
|||
add_library(lean_frontend OBJECT tokens.cpp register_module.cpp
|
||||
add_library(lean_frontend OBJECT tokens.cpp
|
||||
token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
|
||||
parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
|
||||
server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
|
||||
inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
|
||||
inductive_cmd.cpp elaborator.cpp dependencies.cpp
|
||||
begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
|
||||
structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
|
||||
coercion_elaborator.cpp info_tactic.cpp
|
||||
|
|
|
|||
|
|
@ -87,7 +87,6 @@ using notation::mk_binders_action;
|
|||
using notation::mk_exprs_action;
|
||||
using notation::mk_scoped_expr_action;
|
||||
using notation::mk_skip_action;
|
||||
using notation::mk_ext_lua_action;
|
||||
using notation::transition;
|
||||
using notation::action;
|
||||
|
||||
|
|
@ -354,10 +353,6 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
|
|||
} else if (p.curr_is_token_or_id(get_prev_tk())) {
|
||||
p.next();
|
||||
return mk_expr_action(get_precedence(p.env(), new_tokens, prev_token));
|
||||
} else if (p.curr_is_string()) {
|
||||
std::string fn = p.get_str_val();
|
||||
p.next();
|
||||
return mk_ext_lua_action(fn.c_str());
|
||||
} else if (p.curr_is_token_or_id(get_scoped_tk())) {
|
||||
p.next();
|
||||
return mk_scoped_expr_action(mk_var(0));
|
||||
|
|
@ -401,11 +396,6 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
|
|||
}
|
||||
p.check_token_next(get_rparen_tk(), "invalid scoped notation argument, ')' expected");
|
||||
return mk_scoped_expr_action(rec, prec ? *prec : 0);
|
||||
} else if (p.curr_is_token_or_id(get_call_tk())) {
|
||||
p.next();
|
||||
name fn = p.check_id_next("invalid call notation argument, identifier expected");
|
||||
p.check_token_next(get_rparen_tk(), "invalid call notation argument, ')' expected");
|
||||
return mk_ext_lua_action(fn.to_string().c_str());
|
||||
} else {
|
||||
throw parser_error("invalid notation declaration, 'foldl', 'foldr' or 'scoped' expected", p.pos());
|
||||
}
|
||||
|
|
@ -568,7 +558,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
|
|||
ts.push_back(transition(tk, a, pp_tk));
|
||||
break;
|
||||
case notation::action_kind::Expr: case notation::action_kind::Exprs: case notation::action_kind::ScopedExpr:
|
||||
case notation::action_kind::Ext: case notation::action_kind::LuaExt: {
|
||||
case notation::action_kind::Ext: {
|
||||
if (g_allow_local && !p.curr_is_identifier()) {
|
||||
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp, pp_tk));
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include "util/sstream.h"
|
||||
#include "kernel/free_vars.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/tactic/expr_to_tactic.h"
|
||||
#include "frontends/lean/parse_table.h"
|
||||
|
|
@ -119,12 +118,6 @@ struct ext_action_cell : public action_cell {
|
|||
action_cell(action_kind::Ext), m_parse_fn(fn) {}
|
||||
};
|
||||
|
||||
struct ext_lua_action_cell : public action_cell {
|
||||
std::string m_lua_fn;
|
||||
ext_lua_action_cell(char const * fn):
|
||||
action_cell(action_kind::LuaExt), m_lua_fn(fn) {}
|
||||
};
|
||||
|
||||
action::action(action_cell * ptr):m_ptr(ptr) { lean_assert(ptr); }
|
||||
action::action():action(mk_skip_action()) {}
|
||||
action::action(action const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
|
|
@ -150,10 +143,6 @@ ext_action_cell * to_ext_action(action_cell * c) {
|
|||
lean_assert(c->m_kind == action_kind::Ext);
|
||||
return static_cast<ext_action_cell*>(c);
|
||||
}
|
||||
ext_lua_action_cell * to_ext_lua_action(action_cell * c) {
|
||||
lean_assert(c->m_kind == action_kind::LuaExt);
|
||||
return static_cast<ext_lua_action_cell*>(c);
|
||||
}
|
||||
unsigned action::rbp() const { return to_expr_action(m_ptr)->m_rbp; }
|
||||
name const & action::get_sep() const { return to_exprs_action(m_ptr)->m_token_sep; }
|
||||
optional<name> const & action::get_terminator() const { return to_exprs_action(m_ptr)->m_terminator; }
|
||||
|
|
@ -167,7 +156,6 @@ bool action::use_lambda_abstraction() const { return to_scoped_expr_action(m_ptr
|
|||
optional<expr> const & action::get_initial() const { return to_exprs_action(m_ptr)->m_ini; }
|
||||
bool action::is_fold_right() const { return to_exprs_action(m_ptr)->m_fold_right; }
|
||||
parse_fn const & action::get_parse_fn() const { return to_ext_action(m_ptr)->m_parse_fn; }
|
||||
std::string const & action::get_lua_fn() const { return to_ext_lua_action(m_ptr)->m_lua_fn; }
|
||||
bool action::is_equal(action const & a) const {
|
||||
if (kind() != a.kind())
|
||||
return false;
|
||||
|
|
@ -178,8 +166,6 @@ bool action::is_equal(action const & a) const {
|
|||
return rbp() == a.rbp();
|
||||
case action_kind::Ext:
|
||||
return m_ptr == a.m_ptr;
|
||||
case action_kind::LuaExt:
|
||||
return get_lua_fn() == a.get_lua_fn();
|
||||
case action_kind::Exprs:
|
||||
return
|
||||
rbp() == a.rbp() &&
|
||||
|
|
@ -241,7 +227,6 @@ void action::display(io_state_stream & out) const {
|
|||
out << "binders";
|
||||
break;
|
||||
case action_kind::Ext: out << "builtin"; break;
|
||||
case action_kind::LuaExt: out << "luaext"; break;
|
||||
case action_kind::Expr: out << rbp(); break;
|
||||
case action_kind::Exprs:
|
||||
out << "(fold" << (is_fold_right() ? "r" : "l");
|
||||
|
|
@ -257,8 +242,9 @@ void action::display(io_state_stream & out) const {
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
bool action::is_simple() const {
|
||||
return kind() != action_kind::Ext && kind() != action_kind::LuaExt;
|
||||
return kind() != action_kind::Ext;
|
||||
}
|
||||
|
||||
void action_cell::dealloc() {
|
||||
|
|
@ -269,7 +255,6 @@ void action_cell::dealloc() {
|
|||
case action_kind::Exprs: delete(to_exprs_action(this)); break;
|
||||
case action_kind::ScopedExpr: delete(to_scoped_expr_action(this)); break;
|
||||
case action_kind::Ext: delete(to_ext_action(this)); break;
|
||||
case action_kind::LuaExt: delete(to_ext_lua_action(this)); break;
|
||||
default: delete this; break;
|
||||
}
|
||||
}
|
||||
|
|
@ -310,12 +295,10 @@ action mk_ext_action(parse_fn const & fn) {
|
|||
return action(new ext_action_cell(new_fn));
|
||||
}
|
||||
|
||||
action mk_ext_lua_action(char const * fn) { return action(new ext_lua_action_cell(fn)); }
|
||||
|
||||
action replace(action const & a, std::function<expr(expr const &)> const & f) {
|
||||
switch (a.kind()) {
|
||||
case action_kind::Skip: case action_kind::Binder: case action_kind::Binders:
|
||||
case action_kind::Ext: case action_kind::LuaExt: case action_kind::Expr:
|
||||
case action_kind::Ext: case action_kind::Expr:
|
||||
return a;
|
||||
case action_kind::Exprs:
|
||||
return mk_exprs_action(a.get_sep(), f(a.get_rec()), a.get_initial() ? some_expr(f(*a.get_initial())) : none_expr(), a.get_terminator(),
|
||||
|
|
@ -371,7 +354,7 @@ static void validate_transitions(bool nud, unsigned num, transition const * ts,
|
|||
case action_kind::Binder: case action_kind::Binders:
|
||||
found_binder = true;
|
||||
break;
|
||||
case action_kind::Expr: case action_kind::Exprs: case action_kind::Ext: case action_kind::LuaExt:
|
||||
case action_kind::Expr: case action_kind::Exprs: case action_kind::Ext:
|
||||
nargs++;
|
||||
break;
|
||||
case action_kind::ScopedExpr:
|
||||
|
|
@ -478,7 +461,7 @@ static expr expand_pp_pattern(unsigned num, transition const * ts, expr const &
|
|||
switch (act.kind()) {
|
||||
case action_kind::Binder: case action_kind::Binders: case action_kind::Skip:
|
||||
break;
|
||||
case action_kind::Ext: case action_kind::LuaExt:
|
||||
case action_kind::Ext:
|
||||
lean_unreachable();
|
||||
case action_kind::Expr:
|
||||
if (vidx == 0) return none_expr();
|
||||
|
|
@ -602,214 +585,4 @@ void parse_table::display(io_state_stream & out, optional<token_table> const & t
|
|||
::lean::notation::display(out, num, ts, es, is_nud(), tt);
|
||||
});
|
||||
}
|
||||
|
||||
typedef action notation_action;
|
||||
DECL_UDATA(notation_action)
|
||||
|
||||
static int mk_skip_action(lua_State * L) { return push_notation_action(L, mk_skip_action()); }
|
||||
static int mk_binder_action(lua_State * L) { return push_notation_action(L, mk_binder_action()); }
|
||||
static int mk_binders_action(lua_State * L) { return push_notation_action(L, mk_binders_action()); }
|
||||
static int mk_expr_action(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unsigned rbp = nargs == 0 ? 0 : lua_tonumber(L, 1);
|
||||
return push_notation_action(L, mk_expr_action(rbp));
|
||||
}
|
||||
static int mk_exprs_action(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unsigned rbp = nargs <= 5 ? 0 : lua_tonumber(L, 6);
|
||||
optional<name> terminator;
|
||||
if (nargs >= 4) terminator = to_optional_name(L, 4);
|
||||
return push_notation_action(L, mk_exprs_action(to_name_ext(L, 1),
|
||||
to_expr(L, 2),
|
||||
lua_isnil(L, 3) ? none_expr() : some_expr(to_expr(L, 3)),
|
||||
terminator,
|
||||
lua_toboolean(L, 5),
|
||||
rbp));
|
||||
}
|
||||
static int mk_scoped_expr_action(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unsigned rbp = nargs <= 1 ? 0 : lua_tonumber(L, 2);
|
||||
bool lambda = (nargs <= 2) || lua_toboolean(L, 3);
|
||||
return push_notation_action(L, mk_scoped_expr_action(to_expr(L, 1), rbp, lambda));
|
||||
}
|
||||
static int mk_ext_lua_action(lua_State * L) {
|
||||
char const * fn = lua_tostring(L, 1);
|
||||
lua_getglobal(L, fn);
|
||||
if (lua_isnil(L, -1))
|
||||
throw exception("arg #1 is a unknown function name");
|
||||
lua_pop(L, 1);
|
||||
return push_notation_action(L, mk_ext_lua_action(fn));
|
||||
}
|
||||
static int is_equal(lua_State * L) {
|
||||
return push_boolean(L, to_notation_action(L, 1).is_equal(to_notation_action(L, 2)));
|
||||
}
|
||||
static void check_action(lua_State * L, int idx, std::initializer_list<action_kind> const & ks) {
|
||||
action_kind k = to_notation_action(L, idx).kind();
|
||||
if (std::find(ks.begin(), ks.end(), k) == ks.end())
|
||||
throw exception(sstream() << "arg #" << idx << " is a notation action, but it has an unexpected kind");
|
||||
}
|
||||
static int kind(lua_State * L) { return push_integer(L, static_cast<unsigned>(to_notation_action(L, 1).kind())); }
|
||||
static int rbp(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::Expr, action_kind::Exprs, action_kind::ScopedExpr });
|
||||
return push_integer(L, to_notation_action(L, 1).rbp());
|
||||
}
|
||||
static int sep(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::Exprs });
|
||||
return push_name(L, to_notation_action(L, 1).get_sep());
|
||||
}
|
||||
static int rec(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::Exprs, action_kind::ScopedExpr });
|
||||
return push_expr(L, to_notation_action(L, 1).get_rec());
|
||||
}
|
||||
static int initial(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::Exprs });
|
||||
return push_optional_expr(L, to_notation_action(L, 1).get_initial());
|
||||
}
|
||||
static int is_fold_right(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::Exprs });
|
||||
return push_boolean(L, to_notation_action(L, 1).is_fold_right());
|
||||
}
|
||||
static int use_lambda_abstraction(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::ScopedExpr });
|
||||
return push_boolean(L, to_notation_action(L, 1).use_lambda_abstraction());
|
||||
}
|
||||
static int fn(lua_State * L) {
|
||||
check_action(L, 1, { action_kind::LuaExt });
|
||||
return push_string(L, to_notation_action(L, 1).get_lua_fn().c_str());
|
||||
}
|
||||
|
||||
static const struct luaL_Reg notation_action_m[] = {
|
||||
{"__gc", notation_action_gc},
|
||||
{"is_equal", safe_function<is_equal>},
|
||||
{"kind", safe_function<kind>},
|
||||
{"rbp", safe_function<rbp>},
|
||||
{"sep", safe_function<sep>},
|
||||
{"separator", safe_function<sep>},
|
||||
{"rec", safe_function<rec>},
|
||||
{"initial", safe_function<initial>},
|
||||
{"is_fold_right", safe_function<is_fold_right>},
|
||||
{"use_lambda_abstraction", safe_function<use_lambda_abstraction>},
|
||||
{"fn", safe_function<fn>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static void open_notation_action(lua_State * L) {
|
||||
luaL_newmetatable(L, notation_action_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, notation_action_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(notation_action_pred, "is_notation_action");
|
||||
SET_GLOBAL_FUN(mk_skip_action, "skip_notation_action");
|
||||
SET_GLOBAL_FUN(mk_binder_action, "binder_notation_action");
|
||||
SET_GLOBAL_FUN(mk_binders_action, "binders_notation_action");
|
||||
SET_GLOBAL_FUN(mk_expr_action, "expr_notation_action");
|
||||
SET_GLOBAL_FUN(mk_exprs_action, "exprs_notation_action");
|
||||
SET_GLOBAL_FUN(mk_scoped_expr_action, "scoped_expr_notation_action");
|
||||
SET_GLOBAL_FUN(mk_ext_lua_action, "ext_action");
|
||||
|
||||
push_notation_action(L, mk_skip_action());
|
||||
lua_setglobal(L, "Skip");
|
||||
push_notation_action(L, mk_binder_action());
|
||||
lua_setglobal(L, "Binder");
|
||||
push_notation_action(L, mk_binders_action());
|
||||
lua_setglobal(L, "Binders");
|
||||
|
||||
lua_newtable(L);
|
||||
SET_ENUM("Skip", action_kind::Skip);
|
||||
SET_ENUM("Expr", action_kind::Expr);
|
||||
SET_ENUM("Exprs", action_kind::Exprs);
|
||||
SET_ENUM("Binder", action_kind::Binder);
|
||||
SET_ENUM("Binders", action_kind::Binders);
|
||||
SET_ENUM("ScopedExpr", action_kind::ScopedExpr);
|
||||
SET_ENUM("Ext", action_kind::Ext);
|
||||
SET_ENUM("LuaExt", action_kind::LuaExt);
|
||||
lua_setglobal(L, "notation_action_kind");
|
||||
}
|
||||
|
||||
static notation_action to_notation_action_ext(lua_State * L, int idx) {
|
||||
if (is_notation_action(L, idx)) {
|
||||
return to_notation_action(L, idx);
|
||||
} else if (lua_isnumber(L, idx)) {
|
||||
return mk_expr_action(lua_tonumber(L, idx));
|
||||
} else {
|
||||
throw exception("notation_action expected");
|
||||
}
|
||||
}
|
||||
|
||||
DECL_UDATA(parse_table)
|
||||
static int mk_parse_table(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
bool nud = nargs == 0 || lua_toboolean(L, 1);
|
||||
return push_parse_table(L, parse_table(nud));
|
||||
}
|
||||
static int add(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
buffer<transition> ts;
|
||||
luaL_checktype(L, 2, LUA_TTABLE);
|
||||
int sz = objlen(L, 2);
|
||||
for (int i = 1; i <= sz; i++) {
|
||||
lua_rawgeti(L, 2, i);
|
||||
if (lua_isstring(L, -1) || is_name(L, -1)) {
|
||||
ts.push_back(transition(to_name_ext(L, -1), mk_expr_action()));
|
||||
lua_pop(L, 1);
|
||||
} else {
|
||||
luaL_checktype(L, -1, LUA_TTABLE);
|
||||
lua_rawgeti(L, -1, 1);
|
||||
lua_rawgeti(L, -2, 2);
|
||||
ts.push_back(transition(to_name_ext(L, -2), to_notation_action_ext(L, -1)));
|
||||
lua_pop(L, 3);
|
||||
}
|
||||
}
|
||||
bool overload = (nargs <= 3) || lua_toboolean(L, 4);
|
||||
return push_parse_table(L, to_parse_table(L, 1).add(ts.size(), ts.data(), to_expr(L, 3), LEAN_DEFAULT_NOTATION_PRIORITY,
|
||||
overload));
|
||||
}
|
||||
|
||||
static int merge(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
bool overload = (nargs >= 2) && lua_toboolean(L, 2);
|
||||
return push_parse_table(L, to_parse_table(L, 1).merge(to_parse_table(L, 2), overload));
|
||||
}
|
||||
|
||||
static int find(lua_State * L) {
|
||||
list<pair<transition, parse_table>> it = to_parse_table(L, 1).find(to_name_ext(L, 2));
|
||||
if (it) {
|
||||
// TODO(Leo): support multiple actions
|
||||
auto p = head(it);
|
||||
push_notation_action(L, p.first.get_action());
|
||||
push_parse_table(L, p.second);
|
||||
return 2;
|
||||
} else {
|
||||
return push_nil(L);
|
||||
}
|
||||
}
|
||||
|
||||
static int is_nud(lua_State * L) {
|
||||
return push_boolean(L, to_parse_table(L, 1).is_nud());
|
||||
}
|
||||
|
||||
static const struct luaL_Reg parse_table_m[] = {
|
||||
{"__gc", parse_table_gc},
|
||||
{"add", safe_function<add>},
|
||||
{"merge", safe_function<merge>},
|
||||
{"find", safe_function<find>},
|
||||
{"is_nud", safe_function<is_nud>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static void open_parse_table(lua_State * L) {
|
||||
luaL_newmetatable(L, parse_table_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, parse_table_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(parse_table_pred, "is_parse_table");
|
||||
SET_GLOBAL_FUN(mk_parse_table, "parse_table");
|
||||
}
|
||||
}
|
||||
void open_parse_table(lua_State * L) {
|
||||
notation::open_notation_action(L);
|
||||
notation::open_parse_table(L);
|
||||
}
|
||||
}
|
||||
}}
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include <utility>
|
||||
#include "util/buffer.h"
|
||||
#include "util/lua.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "library/head_map.h"
|
||||
#include "frontends/lean/token_table.h"
|
||||
|
|
@ -24,7 +23,7 @@ class io_state_stream;
|
|||
namespace notation {
|
||||
typedef std::function<expr(parser &, unsigned, expr const *, pos_info const &)> parse_fn;
|
||||
|
||||
enum class action_kind { Skip, Expr, Exprs, Binder, Binders, ScopedExpr, Ext, LuaExt };
|
||||
enum class action_kind { Skip, Expr, Exprs, Binder, Binders, ScopedExpr, Ext };
|
||||
struct action_cell;
|
||||
|
||||
/**
|
||||
|
|
@ -72,7 +71,6 @@ public:
|
|||
friend action mk_scoped_expr_action(expr const & rec, unsigned rbp, bool lambda);
|
||||
friend action mk_ext_action_core(parse_fn const & fn);
|
||||
friend action mk_ext_action(parse_fn const & fn);
|
||||
friend action mk_ext_lua_action(char const * lua_fn);
|
||||
|
||||
action_kind kind() const;
|
||||
unsigned rbp() const;
|
||||
|
|
@ -83,7 +81,6 @@ public:
|
|||
bool is_fold_right() const;
|
||||
bool use_lambda_abstraction() const;
|
||||
parse_fn const & get_parse_fn() const;
|
||||
std::string const & get_lua_fn() const;
|
||||
|
||||
bool is_equal(action const & a) const;
|
||||
bool is_equivalent(action const & a) const;
|
||||
|
|
@ -92,7 +89,7 @@ public:
|
|||
|
||||
void display(io_state_stream & out) const;
|
||||
|
||||
/** \brief Return true iff the action is not Ext or LuaExt */
|
||||
/** \brief Return true iff the action is not Ext */
|
||||
bool is_simple() const;
|
||||
};
|
||||
inline bool operator==(action const & a1, action const & a2) { return a1.is_equal(a2); }
|
||||
|
|
@ -107,7 +104,6 @@ action mk_binders_action(unsigned rbp = 0);
|
|||
action mk_scoped_expr_action(expr const & rec, unsigned rbp = 0, bool lambda = true);
|
||||
action mk_ext_action_core(parse_fn const & fn);
|
||||
action mk_ext_action(parse_fn const & fn);
|
||||
action mk_ext_lua_action(char const * lua_fn);
|
||||
|
||||
/** \brief Apply \c f to expressions embedded in the given action */
|
||||
action replace(action const & a, std::function<expr(expr const &)> const & f);
|
||||
|
|
@ -185,7 +181,7 @@ public:
|
|||
/** \brief Given a notation definition, return the "head symbol" of
|
||||
every instance of the given notation.
|
||||
|
||||
\remark The result is none if the notation uses actions implemented in C++ or Lua.
|
||||
\remark The result is none if the notation uses actions implemented in C++.
|
||||
The result is none if the denotation is a variable.
|
||||
*/
|
||||
optional<head_index> get_head_index(unsigned num, transition const * ts, expr const & a);
|
||||
|
|
@ -194,7 +190,6 @@ void initialize_parse_table();
|
|||
void finalize_parse_table();
|
||||
}
|
||||
typedef notation::parse_table parse_table;
|
||||
void open_parse_table(lua_State * L);
|
||||
inline void initialize_parse_table() { notation::initialize_parse_table(); }
|
||||
inline void finalize_parse_table() { notation::finalize_parse_table(); }
|
||||
}
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include <vector>
|
||||
#include <util/utf8.h>
|
||||
#include "util/interrupt.h"
|
||||
#include "util/script_exception.h"
|
||||
#include "util/sstream.h"
|
||||
#include "util/flet.h"
|
||||
#include "util/lean_path.h"
|
||||
|
|
@ -47,7 +46,6 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/tokens.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/parser_bindings.h"
|
||||
#include "frontends/lean/notation_cmd.h"
|
||||
#include "frontends/lean/elaborator.h"
|
||||
#include "frontends/lean/info_annotation.h"
|
||||
|
|
@ -351,11 +349,6 @@ void parser::display_error(throwable const & ex) {
|
|||
::lean::display_error(regular_stream(), &pos_provider, ex);
|
||||
}
|
||||
|
||||
void parser::display_error(script_exception const & ex) {
|
||||
parser_pos_provider pos_provider(m_pos_table, get_stream_name(), m_last_script_pos);
|
||||
::lean::display_error(regular_stream(), &pos_provider, ex);
|
||||
}
|
||||
|
||||
void parser::throw_parser_exception(char const * msg, pos_info p) {
|
||||
throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
|
||||
}
|
||||
|
|
@ -394,9 +387,6 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
|
|||
sync();
|
||||
if (m_use_exceptions || m_info_manager)
|
||||
throw;
|
||||
} catch (script_exception & ex) {
|
||||
reset_interrupt();
|
||||
CATCH(display_error(ex), throw_nested_exception(ex, m_last_script_pos));
|
||||
} catch (throwable & ex) {
|
||||
reset_interrupt();
|
||||
CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
|
||||
|
|
@ -1406,28 +1396,6 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
|
|||
scoped_info.push_back(mk_pair(ps.size(), binder_pos));
|
||||
break;
|
||||
}
|
||||
case notation::action_kind::LuaExt:
|
||||
m_last_script_pos = p;
|
||||
using_script([&](lua_State * L) {
|
||||
scoped_set_parser scope(L, *this);
|
||||
lua_getglobal(L, a.get_lua_fn().c_str());
|
||||
if (!lua_isfunction(L, -1))
|
||||
throw parser_error(sstream() << "failed to use notation implemented in Lua, "
|
||||
<< "Lua state does not contain function '"
|
||||
<< a.get_lua_fn() << "'", p);
|
||||
lua_pushinteger(L, p.first);
|
||||
lua_pushinteger(L, p.second);
|
||||
for (unsigned i = 0; i < args.size(); i++)
|
||||
push_expr(L, args[i]);
|
||||
pcall(L, args.size() + 2, 1, 0);
|
||||
if (!is_expr(L, -1))
|
||||
throw parser_error(sstream() << "failed to use notation implemented in Lua, value returned by function '"
|
||||
<< a.get_lua_fn() << "' is not an expression", p);
|
||||
args.push_back(rec_save_pos(to_expr(L, -1), p));
|
||||
kinds.push_back(a.kind());
|
||||
lua_pop(L, 1);
|
||||
});
|
||||
break;
|
||||
case notation::action_kind::Ext:
|
||||
args.push_back(a.get_parse_fn()(*this, args.size(), args.data(), p));
|
||||
kinds.push_back(a.kind());
|
||||
|
|
@ -2091,25 +2059,6 @@ void parser::parse_command() {
|
|||
}
|
||||
}
|
||||
|
||||
void parser::parse_script(bool as_expr) {
|
||||
m_last_script_pos = pos();
|
||||
std::string script_code = m_scanner.get_str_val();
|
||||
if (as_expr)
|
||||
script_code = "return " + script_code;
|
||||
next();
|
||||
using_script([&](lua_State * L) {
|
||||
dostring(L, script_code.c_str());
|
||||
});
|
||||
}
|
||||
|
||||
static optional<std::string> try_file(name const & f, char const * ext) {
|
||||
try {
|
||||
return optional<std::string>(find_file(f, {ext}));
|
||||
} catch (...) {
|
||||
return optional<std::string>();
|
||||
}
|
||||
}
|
||||
|
||||
static optional<std::string> try_file(std::string const & base, optional<unsigned> const & k, name const & f, char const * ext) {
|
||||
try {
|
||||
return optional<std::string>(find_file(base, k, f, ext));
|
||||
|
|
@ -2118,22 +2067,8 @@ static optional<std::string> try_file(std::string const & base, optional<unsigne
|
|||
}
|
||||
}
|
||||
|
||||
static std::string * g_lua_module_key = nullptr;
|
||||
static void lua_module_reader(deserializer & d, shared_environment &,
|
||||
std::function<void(asynch_update_fn const &)> &,
|
||||
std::function<void(delayed_update_fn const &)> & add_delayed_update) {
|
||||
name fname;
|
||||
d >> fname;
|
||||
add_delayed_update([=](environment const & env, io_state const &) -> environment {
|
||||
std::string rname = find_file(fname, {".lua"});
|
||||
system_import(rname.c_str());
|
||||
return env;
|
||||
});
|
||||
}
|
||||
|
||||
void parser::parse_imports() {
|
||||
buffer<module_name> olean_files;
|
||||
buffer<name> lua_files;
|
||||
bool prelude = false;
|
||||
std::string base = m_base_dir ? *m_base_dir : dirname(get_stream_name().c_str());
|
||||
bool imported = false;
|
||||
|
|
@ -2188,14 +2123,7 @@ void parser::parse_imports() {
|
|||
fingerprint = hash(fingerprint, f.hash());
|
||||
if (k)
|
||||
fingerprint = hash(fingerprint, *k);
|
||||
if (auto it = try_file(f, ".lua")) {
|
||||
if (k)
|
||||
throw parser_error(sstream() << "invalid import, failed to import '" << f
|
||||
<< "', relative paths are not supported for .lua files", pos());
|
||||
lua_files.push_back(f);
|
||||
} else {
|
||||
import_olean(k, f);
|
||||
}
|
||||
import_olean(k, f);
|
||||
next();
|
||||
}
|
||||
}
|
||||
|
|
@ -2206,13 +2134,6 @@ void parser::parse_imports() {
|
|||
m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads,
|
||||
keep_imported_thms, m_ios);
|
||||
m_env = update_fingerprint(m_env, fingerprint);
|
||||
for (auto const & f : lua_files) {
|
||||
std::string rname = find_file(f, {".lua"});
|
||||
system_import(rname.c_str());
|
||||
m_env = module::add(m_env, *g_lua_module_key, [=](environment const &, serializer & s) {
|
||||
s << f;
|
||||
});
|
||||
}
|
||||
if (imported)
|
||||
commit_info(1, 0);
|
||||
}
|
||||
|
|
@ -2258,10 +2179,6 @@ bool parser::parse_commands() {
|
|||
parse_command();
|
||||
commit_info();
|
||||
break;
|
||||
case scanner::token_kind::ScriptBlock:
|
||||
parse_script();
|
||||
save_snapshot();
|
||||
break;
|
||||
case scanner::token_kind::Eof:
|
||||
done = true;
|
||||
break;
|
||||
|
|
@ -2463,14 +2380,11 @@ void initialize_parser() {
|
|||
register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
|
||||
"(lean parser) import modules in parallel");
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
g_lua_module_key = new std::string("lua_module");
|
||||
register_module_object_reader(*g_lua_module_key, lua_module_reader);
|
||||
g_anonymous_inst_name_prefix = new name("_inst");
|
||||
}
|
||||
|
||||
void finalize_parser() {
|
||||
delete g_anonymous_inst_name_prefix;
|
||||
delete g_lua_module_key;
|
||||
delete g_tmp_prefix;
|
||||
delete g_parser_show_errors;
|
||||
delete g_parser_parallel_import;
|
||||
|
|
|
|||
|
|
@ -9,17 +9,13 @@ Author: Leonardo de Moura
|
|||
#include <utility>
|
||||
#include <vector>
|
||||
#include "util/flet.h"
|
||||
#include "util/script_state.h"
|
||||
#include "util/name_map.h"
|
||||
#include "util/exception.h"
|
||||
#include "util/thread_script_state.h"
|
||||
#include "util/script_exception.h"
|
||||
#include "util/name_generator.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/expr_maps.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/definition_cache.h"
|
||||
#include "library/declaration_index.h"
|
||||
#include "frontends/lean/scanner.h"
|
||||
|
|
@ -110,7 +106,6 @@ class parser {
|
|||
name_set m_include_vars; // subset of m_local_decls that is marked as include
|
||||
parser_scope_stack m_parser_scope_stack;
|
||||
pos_info m_last_cmd_pos;
|
||||
pos_info m_last_script_pos;
|
||||
unsigned m_next_tag_idx;
|
||||
unsigned m_next_inst_idx;
|
||||
bool m_found_errors;
|
||||
|
|
@ -166,23 +161,11 @@ class parser {
|
|||
void display_error_pos(pos_info p);
|
||||
void display_error(char const * msg, unsigned line, unsigned pos);
|
||||
void display_error(char const * msg, pos_info p);
|
||||
void display_error(script_exception const & ex);
|
||||
void throw_parser_exception(char const * msg, pos_info p);
|
||||
void throw_nested_exception(throwable const & ex, pos_info p);
|
||||
|
||||
void sync_command();
|
||||
void protected_call(std::function<void()> && f, std::function<void()> && sync);
|
||||
template<typename F>
|
||||
typename std::result_of<F(lua_State * L)>::type using_script(F && f) {
|
||||
try {
|
||||
script_state S = get_thread_script_state();
|
||||
set_io_state set1(S, m_ios);
|
||||
set_environment set2(S, m_env);
|
||||
return f(S.get_state());
|
||||
} catch (script_nested_exception & ex) {
|
||||
ex.get_exception().rethrow();
|
||||
}
|
||||
}
|
||||
|
||||
tag get_tag(expr e);
|
||||
expr copy_with_new_pos(expr const & e, pos_info p);
|
||||
|
|
@ -200,7 +183,6 @@ class parser {
|
|||
|
||||
void parse_imports();
|
||||
void parse_command();
|
||||
void parse_script(bool as_expr = false);
|
||||
bool parse_commands();
|
||||
unsigned curr_lbp_core(bool as_tactic) const;
|
||||
void process_postponed(buffer<expr> const & args, bool is_left, buffer<notation::action_kind> const & kinds,
|
||||
|
|
@ -364,8 +346,6 @@ public:
|
|||
bool curr_is_keyword() const { return curr() == scanner::token_kind::Keyword; }
|
||||
/** \brief Return true iff the current token is a keyword */
|
||||
bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; }
|
||||
/** \brief Return true iff the current token is a Lua script block */
|
||||
bool curr_is_script_block() const { return curr() == scanner::token_kind::ScriptBlock; }
|
||||
/** \brief Return true iff the current token is EOF */
|
||||
bool curr_is_eof() const { return curr() == scanner::token_kind::Eof; }
|
||||
/** \brief Return true iff the current token is a keyword */
|
||||
|
|
|
|||
|
|
@ -1,185 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <utility>
|
||||
#include <vector>
|
||||
#include "kernel/abstract.h"
|
||||
#include "frontends/lean/parser_bindings.h"
|
||||
|
||||
namespace lean {
|
||||
static char g_parser_key;
|
||||
void set_global_parser(lua_State * L, parser * p) {
|
||||
lua_pushlightuserdata(L, static_cast<void *>(&g_parser_key));
|
||||
lua_pushlightuserdata(L, static_cast<void *>(p));
|
||||
lua_settable(L, LUA_REGISTRYINDEX);
|
||||
}
|
||||
|
||||
parser * get_global_parser_ptr(lua_State * L) {
|
||||
lua_pushlightuserdata(L, static_cast<void *>(&g_parser_key));
|
||||
lua_gettable(L, LUA_REGISTRYINDEX);
|
||||
if (!lua_islightuserdata(L, -1))
|
||||
return nullptr;
|
||||
parser * p = static_cast<parser*>(const_cast<void*>(lua_topointer(L, -1)));
|
||||
lua_pop(L, 1);
|
||||
return p;
|
||||
}
|
||||
|
||||
parser & get_global_parser(lua_State * L) {
|
||||
parser * p = get_global_parser_ptr(L);
|
||||
if (p == nullptr)
|
||||
throw exception("there is no Lean parser on the Lua stack");
|
||||
return *p;
|
||||
}
|
||||
|
||||
scoped_set_parser::scoped_set_parser(lua_State * L, parser & p):m_state(L) {
|
||||
m_old = get_global_parser_ptr(L);
|
||||
set_global_parser(L, &p);
|
||||
}
|
||||
scoped_set_parser::~scoped_set_parser() {
|
||||
set_global_parser(m_state, m_old);
|
||||
}
|
||||
|
||||
static unsigned to_rbp(lua_State * L, int idx) {
|
||||
int nargs = lua_gettop(L);
|
||||
return idx < nargs ? 0 : lua_tointeger(L, idx);
|
||||
}
|
||||
|
||||
typedef pair<local_environment, std::vector<expr>> local_scope_cell;
|
||||
typedef std::shared_ptr<local_scope_cell> local_scope;
|
||||
DECL_UDATA(local_scope);
|
||||
static const struct luaL_Reg local_scope_m[] = {
|
||||
{"__gc", local_scope_gc},
|
||||
{0, 0}
|
||||
};
|
||||
int push_local_scope_ext(lua_State * L, local_environment const & lenv, buffer<expr> const & ps) {
|
||||
local_scope r = std::make_shared<local_scope_cell>();
|
||||
r->first = lenv;
|
||||
for (auto const & p : ps)
|
||||
r->second.push_back(p);
|
||||
return push_local_scope(L, r);
|
||||
}
|
||||
|
||||
static void open_local_scope(lua_State * L) {
|
||||
luaL_newmetatable(L, local_scope_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, local_scope_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(local_scope_pred, "is_local_scope");
|
||||
}
|
||||
|
||||
#define gparser get_global_parser(L)
|
||||
|
||||
static int parse_level(lua_State * L) { return push_level(L, gparser.parse_level(to_rbp(L, 1))); }
|
||||
static int parse_expr(lua_State * L) { return push_expr(L, gparser.parse_expr(to_rbp(L, 1))); }
|
||||
static int parse_led(lua_State * L) { return push_expr(L, gparser.parse_led(to_expr(L, 1))); }
|
||||
static int parse_binders(lua_State * L) {
|
||||
buffer<expr> ps;
|
||||
unsigned rbp = 0;
|
||||
auto lenv = gparser.parse_binders(ps, rbp);
|
||||
return push_local_scope_ext(L, lenv, ps);
|
||||
}
|
||||
static int parse_binder(lua_State * L) {
|
||||
buffer<expr> ps;
|
||||
unsigned rbp = 0;
|
||||
ps.push_back(gparser.parse_binder(rbp));
|
||||
return push_local_scope_ext(L, gparser.env(), ps);
|
||||
}
|
||||
static int parse_scoped_expr(lua_State * L) {
|
||||
local_scope const & s = to_local_scope(L, 1);
|
||||
unsigned rbp = to_rbp(L, 2);
|
||||
return push_expr(L, gparser.parse_scoped_expr(s->second.size(), s->second.data(), s->first, rbp));
|
||||
}
|
||||
static int lambda_abstract(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
local_scope const & s = to_local_scope(L, 1);
|
||||
expr const & e = to_expr(L, 2);
|
||||
expr r;
|
||||
bool using_cache = false;
|
||||
if (nargs == 2)
|
||||
r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e, using_cache), gparser.pos_of(e));
|
||||
else
|
||||
r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e, using_cache), pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4)));
|
||||
return push_expr(L, r);
|
||||
}
|
||||
static int next(lua_State * L) { gparser.next(); return 0; }
|
||||
static int curr(lua_State * L) { return push_integer(L, static_cast<unsigned>(gparser.curr())); }
|
||||
static int curr_is_token(lua_State * L) { return push_boolean(L, gparser.curr_is_token(to_name_ext(L, 1))); }
|
||||
static int curr_is_token_or_id(lua_State * L) { return push_boolean(L, gparser.curr_is_token_or_id(to_name_ext(L, 1))); }
|
||||
static int curr_is_identifier(lua_State * L) { return push_boolean(L, gparser.curr_is_identifier()); }
|
||||
static int curr_is_numeral(lua_State * L) { return push_boolean(L, gparser.curr_is_numeral()); }
|
||||
static int curr_is_string(lua_State * L) { return push_boolean(L, gparser.curr_is_string()); }
|
||||
static int curr_is_keyword(lua_State * L) { return push_boolean(L, gparser.curr_is_keyword()); }
|
||||
static int curr_is_command(lua_State * L) { return push_boolean(L, gparser.curr_is_command()); }
|
||||
static int curr_is_quoted_symbol(lua_State * L) { return push_boolean(L, gparser.curr_is_quoted_symbol()); }
|
||||
static int check_token_next(lua_State * L) { gparser.check_token_next(to_name_ext(L, 1), lua_tostring(L, 2)); return 0; }
|
||||
static int check_id_next(lua_State * L) { return push_name(L, gparser.check_id_next(lua_tostring(L, 1))); }
|
||||
static int pos(lua_State * L) {
|
||||
auto pos = gparser.pos();
|
||||
push_integer(L, pos.first);
|
||||
push_integer(L, pos.second);
|
||||
return 2;
|
||||
}
|
||||
static int save_pos(lua_State * L) {
|
||||
return push_expr(L, gparser.save_pos(to_expr(L, 1), pos_info(lua_tointeger(L, 2), lua_tointeger(L, 3))));
|
||||
}
|
||||
static int pos_of(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
pos_info pos;
|
||||
if (nargs == 1)
|
||||
pos = gparser.pos_of(to_expr(L, 1));
|
||||
else
|
||||
pos = gparser.pos_of(to_expr(L, 1), pos_info(lua_tointeger(L, 2), lua_tointeger(L, 3)));
|
||||
push_integer(L, pos.first);
|
||||
push_integer(L, pos.second);
|
||||
return 2;
|
||||
}
|
||||
static int env(lua_State * L) { return push_environment(L, gparser.env()); }
|
||||
static int ios(lua_State * L) { return push_io_state(L, gparser.ios()); }
|
||||
|
||||
void open_parser(lua_State * L) {
|
||||
open_local_scope(L);
|
||||
|
||||
lua_newtable(L);
|
||||
SET_FUN(parse_expr, "parse_expr");
|
||||
SET_FUN(parse_level, "parse_level");
|
||||
SET_FUN(parse_led, "parse_led");
|
||||
SET_FUN(parse_binders, "parse_binders");
|
||||
SET_FUN(parse_binder, "parse_binder");
|
||||
SET_FUN(parse_scoped_expr, "parse_scoped_expr");
|
||||
SET_FUN(lambda_abstract, "lambda_abstract");
|
||||
SET_FUN(lambda_abstract, "abstract");
|
||||
SET_FUN(next, "next");
|
||||
SET_FUN(curr, "curr");
|
||||
SET_FUN(curr_is_token, "curr_is_token");
|
||||
SET_FUN(curr_is_token_or_id, "curr_is_token_or_id");
|
||||
SET_FUN(curr_is_identifier, "curr_is_identifier");
|
||||
SET_FUN(curr_is_numeral, "curr_is_numeral");
|
||||
SET_FUN(curr_is_string, "curr_is_string");
|
||||
SET_FUN(curr_is_keyword, "curr_is_keyword");
|
||||
SET_FUN(curr_is_command, "curr_is_command");
|
||||
SET_FUN(curr_is_quoted_symbol, "curr_is_quoted_symbol");
|
||||
SET_FUN(check_token_next, "check_token_next");
|
||||
SET_FUN(check_id_next, "check_id_next");
|
||||
SET_FUN(pos, "pos");
|
||||
SET_FUN(save_pos, "save_pos");
|
||||
SET_FUN(pos_of, "pos_of");
|
||||
SET_FUN(env, "env");
|
||||
SET_FUN(ios, "ios");
|
||||
lua_setglobal(L, "parser");
|
||||
|
||||
lua_newtable(L);
|
||||
SET_ENUM("Keyword", scanner::token_kind::Keyword);
|
||||
SET_ENUM("CommandKeyword", scanner::token_kind::CommandKeyword);
|
||||
SET_ENUM("ScriptBlock", scanner::token_kind::ScriptBlock);
|
||||
SET_ENUM("Identifier", scanner::token_kind::Identifier);
|
||||
SET_ENUM("Numeral", scanner::token_kind::Numeral);
|
||||
SET_ENUM("Decimal", scanner::token_kind::Decimal);
|
||||
SET_ENUM("String", scanner::token_kind::String);
|
||||
SET_ENUM("QuotedSymbol", scanner::token_kind::QuotedSymbol);
|
||||
lua_setglobal(L, "token_kind");
|
||||
}
|
||||
}
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
namespace lean {
|
||||
struct scoped_set_parser {
|
||||
lua_State * m_state;
|
||||
parser * m_old;
|
||||
scoped_set_parser(lua_State * L, parser & p);
|
||||
~scoped_set_parser();
|
||||
};
|
||||
void open_parser(lua_State * L);
|
||||
}
|
||||
|
|
@ -154,9 +154,6 @@ serializer & operator<<(serializer & s, action const & a) {
|
|||
case action_kind::ScopedExpr:
|
||||
s << a.get_rec() << a.rbp() << a.use_lambda_abstraction();
|
||||
break;
|
||||
case action_kind::LuaExt:
|
||||
s << a.get_lua_fn();
|
||||
break;
|
||||
case action_kind::Ext:
|
||||
lean_unreachable();
|
||||
}
|
||||
|
|
@ -195,8 +192,6 @@ action read_action(deserializer & d) {
|
|||
d >> rec >> rbp >> use_lambda_abstraction;
|
||||
return notation::mk_scoped_expr_action(rec, rbp, use_lambda_abstraction);
|
||||
}
|
||||
case action_kind::LuaExt:
|
||||
return notation::mk_ext_lua_action(d.read_string().c_str());
|
||||
case action_kind::Ext:
|
||||
break;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -879,7 +879,6 @@ static unsigned get_num_parameters(notation_entry const & entry) {
|
|||
case notation::action_kind::Exprs:
|
||||
case notation::action_kind::ScopedExpr:
|
||||
case notation::action_kind::Ext:
|
||||
case notation::action_kind::LuaExt:
|
||||
r++;
|
||||
}
|
||||
}
|
||||
|
|
@ -1166,7 +1165,6 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
|
|||
break;
|
||||
}
|
||||
case notation::action_kind::Ext:
|
||||
case notation::action_kind::LuaExt:
|
||||
return optional<result>();
|
||||
}
|
||||
token_lbp = get_some_precedence(m_token_table, tk);
|
||||
|
|
|
|||
|
|
@ -1,24 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <sstream>
|
||||
#include "util/lua.h"
|
||||
#include "util/script_state.h"
|
||||
#include "frontends/lean/token_table.h"
|
||||
#include "frontends/lean/parse_table.h"
|
||||
#include "frontends/lean/parser_bindings.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
void open_frontend_lean(lua_State * L) {
|
||||
open_token_table(L);
|
||||
open_parse_table(L);
|
||||
open_parser(L);
|
||||
}
|
||||
void register_frontend_lean_module() {
|
||||
script_state::register_module(open_frontend_lean);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <lua.hpp>
|
||||
namespace lean {
|
||||
void open_frontend_lean(lua_State * L);
|
||||
void register_frontend_lean_module();
|
||||
}
|
||||
|
|
@ -179,88 +179,4 @@ void finalize_token_table() {
|
|||
}
|
||||
|
||||
token_table mk_token_table() { return token_table(); }
|
||||
|
||||
DECL_UDATA(token_table)
|
||||
static int mk_token_table(lua_State * L) { return push_token_table(L, mk_token_table()); }
|
||||
static int mk_default_token_table(lua_State * L) { return push_token_table(L, mk_default_token_table()); }
|
||||
static int add_command_token(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2)
|
||||
return push_token_table(L, add_command_token(to_token_table(L, 1), lua_tostring(L, 2)));
|
||||
else
|
||||
return push_token_table(L, add_command_token(to_token_table(L, 1), lua_tostring(L, 2), lua_tostring(L, 3)));
|
||||
}
|
||||
static int add_token(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 3)
|
||||
return push_token_table(L, add_token(to_token_table(L, 1), lua_tostring(L, 2), lua_tonumber(L, 3)));
|
||||
else
|
||||
return push_token_table(L, add_token(to_token_table(L, 1), lua_tostring(L, 2), lua_tostring(L, 3), lua_tonumber(L, 4)));
|
||||
}
|
||||
static int merge(lua_State * L) {
|
||||
return push_token_table(L, merge(to_token_table(L, 1), to_token_table(L, 2)));
|
||||
}
|
||||
static int find(lua_State * L) {
|
||||
char k;
|
||||
if (lua_isnumber(L, 2)) {
|
||||
k = lua_tonumber(L, 2);
|
||||
} else {
|
||||
char const * str = lua_tostring(L, 2);
|
||||
if (strlen(str) != 1)
|
||||
throw exception("arg #2 must be a string of length 1");
|
||||
k = str[0];
|
||||
}
|
||||
auto it = to_token_table(L, 1).find(k);
|
||||
if (it)
|
||||
return push_token_table(L, *it);
|
||||
else
|
||||
return push_nil(L);
|
||||
}
|
||||
static int value_of(lua_State * L) {
|
||||
auto it = value_of(to_token_table(L, 1));
|
||||
if (it) {
|
||||
push_boolean(L, it->is_command());
|
||||
push_name(L, it->value());
|
||||
push_integer(L, it->expr_precedence());
|
||||
return 3;
|
||||
} else {
|
||||
push_nil(L);
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static int for_each(lua_State * L) {
|
||||
token_table const & t = to_token_table(L, 1);
|
||||
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
|
||||
for_each(t, [&](char const * k, token_info const & info) {
|
||||
lua_pushvalue(L, 2);
|
||||
lua_pushstring(L, k);
|
||||
lua_pushboolean(L, info.is_command());
|
||||
push_name(L, info.value());
|
||||
lua_pushinteger(L, info.expr_precedence());
|
||||
pcall(L, 4, 0, 0);
|
||||
});
|
||||
return 0;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg token_table_m[] = {
|
||||
{"__gc", token_table_gc},
|
||||
{"add_command_token", safe_function<add_command_token>},
|
||||
{"add_token", safe_function<add_token>},
|
||||
{"merge", safe_function<merge>},
|
||||
{"find", safe_function<find>},
|
||||
{"value_of", safe_function<value_of>},
|
||||
{"for_each", safe_function<for_each>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_token_table(lua_State * L) {
|
||||
luaL_newmetatable(L, token_table_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, token_table_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(token_table_pred, "is_token_table");
|
||||
SET_GLOBAL_FUN(mk_default_token_table, "default_token_table");
|
||||
SET_GLOBAL_FUN(mk_token_table, "token_table");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include "util/trie.h"
|
||||
#include "util/name.h"
|
||||
#include "util/lua.h"
|
||||
|
||||
#ifndef LEAN_DEFAULT_PRECEDENCE
|
||||
#define LEAN_DEFAULT_PRECEDENCE 1
|
||||
|
|
@ -67,7 +66,6 @@ optional<unsigned> get_expr_precedence(token_table const & s, char const * token
|
|||
optional<unsigned> get_tactic_precedence(token_table const & s, char const * token);
|
||||
bool is_token(token_table const & s, char const * token);
|
||||
token_info const * value_of(token_table const & s);
|
||||
void open_token_table(lua_State * L);
|
||||
void initialize_token_table();
|
||||
void finalize_token_table();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -136,7 +136,6 @@ tactic_infixr tactic_infixr
|
|||
tactic_postfix tactic_postfix
|
||||
tactic_prefix tactic_prefix
|
||||
tactic_notation tactic_notation
|
||||
call call
|
||||
calc calc
|
||||
obtain obtain
|
||||
root _root_
|
||||
|
|
|
|||
|
|
@ -40,17 +40,15 @@ void consume_until_end(parser & p) {
|
|||
}
|
||||
|
||||
void check_command_period_or_eof(parser const & p) {
|
||||
if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()) &&
|
||||
!p.curr_is_script_block())
|
||||
throw parser_error("unexpected token, '.', command, Lua script, or end-of-file expected", p.pos());
|
||||
if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()))
|
||||
throw parser_error("unexpected token, '.', command, or end-of-file expected", p.pos());
|
||||
}
|
||||
|
||||
void check_command_period_open_binder_or_eof(parser const & p) {
|
||||
if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()) &&
|
||||
!p.curr_is_script_block() &&
|
||||
!p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lbracket_tk()) &&
|
||||
!p.curr_is_token(get_lcurly_tk()) && !p.curr_is_token(get_ldcurly_tk()))
|
||||
throw parser_error("unexpected token, '(', '{', '[', '⦃', '.', command, Lua script, or end-of-file expected", p.pos());
|
||||
throw parser_error("unexpected token, '(', '{', '[', '⦃', '.', command, or end-of-file expected", p.pos());
|
||||
}
|
||||
|
||||
void check_atomic(name const & n) {
|
||||
|
|
|
|||
|
|
@ -1 +0,0 @@
|
|||
add_library(leanlua OBJECT register_modules.cpp)
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/script_state.h"
|
||||
#include "util/numerics/register_module.h"
|
||||
#include "util/sexpr/register_module.h"
|
||||
#include "library/register_module.h"
|
||||
#include "library/tactic/register_module.h"
|
||||
#include "frontends/lean/register_module.h"
|
||||
|
||||
namespace lean {
|
||||
void register_modules() {
|
||||
register_numerics_module();
|
||||
register_sexpr_module();
|
||||
register_core_module();
|
||||
register_tactic_module();
|
||||
register_frontend_lean_module();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Register all modules at \c script_state.
|
||||
*/
|
||||
void register_modules();
|
||||
}
|
||||
|
|
@ -20,7 +20,6 @@ Author: Leonardo de Moura
|
|||
#include "library/print.h"
|
||||
#include "compiler/init_module.h"
|
||||
#include "frontends/lean/init_module.h"
|
||||
#include "frontends/lua/register_modules.h"
|
||||
#include "init/init.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -40,7 +39,6 @@ void initialize() {
|
|||
initialize_definitional_module();
|
||||
initialize_compiler_module();
|
||||
initialize_frontend_lean_module();
|
||||
register_modules();
|
||||
}
|
||||
void finalize() {
|
||||
run_thread_finalizers();
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ Author: Leonardo de Moura
|
|||
#include <tuple>
|
||||
#include <string>
|
||||
#include "util/thread.h"
|
||||
#include "util/lua.h"
|
||||
#include "util/rc.h"
|
||||
#include "util/name.h"
|
||||
#include "util/hash.h"
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
|
||||
occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
|
||||
occurs.cpp io_state_stream.cpp bin_app.cpp
|
||||
constants.cpp resolve_macro.cpp kernel_serializer.cpp
|
||||
max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp
|
||||
coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/abstract.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "library/expr_lt.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/aliases.h"
|
||||
#include "library/placeholder.h"
|
||||
#include "library/scoped_ext.h"
|
||||
|
|
@ -212,57 +211,6 @@ void for_each_expr_alias(environment const & env, std::function<void(name const
|
|||
ext.for_each_expr_alias(fn);
|
||||
}
|
||||
|
||||
static int add_expr_alias(lua_State * L) {
|
||||
return push_environment(L, add_expr_alias(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
|
||||
}
|
||||
static int add_level_alias(lua_State * L) {
|
||||
return push_environment(L, add_level_alias(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
|
||||
}
|
||||
|
||||
static int is_expr_aliased(lua_State * L) {
|
||||
return push_optional_name(L, is_expr_aliased(to_environment(L, 1), to_name_ext(L, 2)));
|
||||
}
|
||||
static int is_level_aliased(lua_State * L) {
|
||||
return push_optional_name(L, is_level_aliased(to_environment(L, 1), to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int get_expr_aliases(lua_State * L) {
|
||||
return push_list_name(L, get_expr_aliases(to_environment(L, 1), to_name_ext(L, 2)));
|
||||
}
|
||||
static int get_level_alias(lua_State * L) {
|
||||
return push_optional_name(L, get_level_alias(to_environment(L, 1), to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int add_aliases(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2) {
|
||||
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), name()));
|
||||
} else if (nargs == 3) {
|
||||
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
|
||||
} else {
|
||||
buffer<name> exs;
|
||||
luaL_checktype(L, 4, LUA_TTABLE);
|
||||
int n = objlen(L, 4);
|
||||
for (int i = 1; i <= n; i++) {
|
||||
lua_rawgeti(L, 4, i);
|
||||
exs.push_back(to_name_ext(L, -1));
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3),
|
||||
exs.size(), exs.data()));
|
||||
}
|
||||
}
|
||||
|
||||
void open_aliases(lua_State * L) {
|
||||
SET_GLOBAL_FUN(add_expr_alias, "add_expr_alias");
|
||||
SET_GLOBAL_FUN(add_level_alias, "add_level_alias");
|
||||
SET_GLOBAL_FUN(is_expr_aliased, "is_expr_aliased");
|
||||
SET_GLOBAL_FUN(is_level_aliased, "is_level_aliased");
|
||||
SET_GLOBAL_FUN(get_expr_aliases, "get_expr_aliases");
|
||||
SET_GLOBAL_FUN(get_level_alias, "get_level_alias");
|
||||
SET_GLOBAL_FUN(add_aliases, "add_aliases");
|
||||
}
|
||||
|
||||
void initialize_aliases() {
|
||||
g_aliases = new name("alias");
|
||||
g_ext = new aliases_ext_reg();
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/lua.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -57,7 +56,6 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
|
|||
|
||||
void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
|
||||
|
||||
void open_aliases(lua_State * L);
|
||||
void initialize_aliases();
|
||||
void finalize_aliases();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ Author: Leonardo de Moura
|
|||
#include "library/match.h"
|
||||
#include "library/constants.h"
|
||||
#include "library/app_builder.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/tmp_type_context.h"
|
||||
#include "library/relation_manager.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
|||
#include "util/sstream.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
#include "library/choice.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/kernel_serializer.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -112,40 +111,4 @@ expr const & get_choice(expr const & e, unsigned i) {
|
|||
lean_assert(is_choice(e));
|
||||
return macro_arg(e, i);
|
||||
}
|
||||
|
||||
static int mk_choice(lua_State * L) {
|
||||
check_atleast_num_args(L, 1);
|
||||
int nargs = lua_gettop(L);
|
||||
buffer<expr> args;
|
||||
for (int i = 1; i <= nargs; i++)
|
||||
args.push_back(to_expr(L, i));
|
||||
return push_expr(L, mk_choice(args.size(), args.data()));
|
||||
}
|
||||
|
||||
static int is_choice(lua_State * L) {
|
||||
return push_boolean(L, is_choice(to_expr(L, 1)));
|
||||
}
|
||||
static void check_choice(lua_State * L, int idx) {
|
||||
if (!is_choice(to_expr(L, idx)))
|
||||
throw exception(sstream() << "arg #" << idx << " is not a choice-expression");
|
||||
}
|
||||
static int get_num_choices(lua_State * L) {
|
||||
check_choice(L, 1);
|
||||
return push_integer(L, get_num_choices(to_expr(L, 1)));
|
||||
}
|
||||
static int get_choice(lua_State * L) {
|
||||
check_choice(L, 1);
|
||||
expr const & c = to_expr(L, 1);
|
||||
int i = lua_tointeger(L, 2);
|
||||
if (i < 0 || static_cast<unsigned>(i) >= get_num_choices(c))
|
||||
throw exception("arg #2 is an invalid choice index");
|
||||
return push_expr(L, get_choice(c, i));
|
||||
}
|
||||
|
||||
void open_choice(lua_State * L) {
|
||||
SET_GLOBAL_FUN(mk_choice, "mk_choice");
|
||||
SET_GLOBAL_FUN(is_choice, "is_choice");
|
||||
SET_GLOBAL_FUN(get_num_choices, "get_num_choices");
|
||||
SET_GLOBAL_FUN(get_choice, "get_choice");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -45,7 +44,6 @@ list<list<name>> collect_choice_symbols(expr const & e);
|
|||
/** \brief Format the result produced by collect_choice_symbols. */
|
||||
format pp_choice_symbols(expr const & e);
|
||||
|
||||
void open_choice(lua_State * L);
|
||||
void initialize_choice();
|
||||
void finalize_choice();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/lua.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "library/expr_pair.h"
|
||||
#include "library/io_state.h"
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include <utility>
|
||||
#include <string>
|
||||
#include "util/script_exception.h"
|
||||
#include "util/name_set.h"
|
||||
#include "kernel/ext_exception.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
|
|
@ -91,64 +90,12 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
|
|||
ios << " " << mk_pair(j.pp(fmt, p, ex.get_substitution()), opts) << endl;
|
||||
}
|
||||
|
||||
static void display_error(io_state_stream const & ios, pos_info_provider const * p, script_exception const & ex) {
|
||||
if (p) {
|
||||
char const * msg = ex.get_msg();
|
||||
char const * space = msg && *msg == ' ' ? "" : " ";
|
||||
switch (ex.get_source()) {
|
||||
case script_exception::source::String:
|
||||
display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1));
|
||||
ios << " executing script," << space << msg << endl;
|
||||
break;
|
||||
case script_exception::source::File:
|
||||
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
|
||||
ios << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")," << space << msg << endl;
|
||||
break;
|
||||
case script_exception::source::Unknown:
|
||||
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
|
||||
ios << " executing script, exact error position is not available, " << ex.what() << endl;
|
||||
break;
|
||||
}
|
||||
} else {
|
||||
ios << ex.what() << endl;
|
||||
}
|
||||
}
|
||||
|
||||
static void display_error(io_state_stream const & ios, pos_info_provider const * p, script_nested_exception const & ex) {
|
||||
switch (ex.get_source()) {
|
||||
case script_exception::source::String:
|
||||
if (p) {
|
||||
display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1));
|
||||
ios << " executing script" << endl;
|
||||
}
|
||||
display_error(ios, nullptr, ex.get_exception());
|
||||
break;
|
||||
case script_exception::source::File:
|
||||
if (p) {
|
||||
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
|
||||
ios << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")" << endl;
|
||||
} else {
|
||||
display_error_pos(ios, ex.get_file_name(), ex.get_line(), -1);
|
||||
ios << " executing script" << endl;
|
||||
}
|
||||
display_error(ios, nullptr, ex.get_exception());
|
||||
break;
|
||||
case script_exception::source::Unknown:
|
||||
display_error(ios, nullptr, ex.get_exception());
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
|
||||
flycheck_error err(ios);
|
||||
if (auto k_ex = dynamic_cast<ext_exception const *>(&ex)) {
|
||||
display_error(ios, p, *k_ex);
|
||||
} else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
|
||||
display_error(ios, p, *e_ex);
|
||||
} else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {
|
||||
display_error(ios, p, *ls_ex);
|
||||
} else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) {
|
||||
display_error(ios, p, *s_ex);
|
||||
} else if (p) {
|
||||
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
|
||||
ios << " " << ex.what() << endl;
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#include "util/sstream.h"
|
||||
#include "library/annotation.h"
|
||||
#include "library/explicit.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
|
||||
namespace lean {
|
||||
static name * g_explicit_name = nullptr;
|
||||
|
|
@ -62,36 +61,4 @@ void finalize_explicit() {
|
|||
delete g_explicit_name;
|
||||
delete g_consume_args_name;
|
||||
}
|
||||
|
||||
static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); }
|
||||
static int is_explicit(lua_State * L) { return push_boolean(L, is_explicit(to_expr(L, 1))); }
|
||||
static void check_explicit(lua_State * L, int idx) {
|
||||
if (!is_explicit(to_expr(L, idx)))
|
||||
throw exception(sstream() << "arg #" << idx << " is not a '@'-expression");
|
||||
}
|
||||
static int get_explicit_arg(lua_State * L) {
|
||||
check_explicit(L, 1);
|
||||
return push_expr(L, get_explicit_arg(to_expr(L, 1)));
|
||||
}
|
||||
|
||||
static int mk_partial_explicit(lua_State * L) { return push_expr(L, mk_partial_explicit(to_expr(L, 1))); }
|
||||
static int is_partial_explicit(lua_State * L) { return push_boolean(L, is_partial_explicit(to_expr(L, 1))); }
|
||||
static void check_partial_explicit(lua_State * L, int idx) {
|
||||
if (!is_partial_explicit(to_expr(L, idx)))
|
||||
throw exception(sstream() << "arg #" << idx << " is not a '@'-expression");
|
||||
}
|
||||
static int get_partial_explicit_arg(lua_State * L) {
|
||||
check_partial_explicit(L, 1);
|
||||
return push_expr(L, get_partial_explicit_arg(to_expr(L, 1)));
|
||||
}
|
||||
|
||||
void open_explicit(lua_State * L) {
|
||||
SET_GLOBAL_FUN(mk_explicit, "mk_explicit");
|
||||
SET_GLOBAL_FUN(is_explicit, "is_explicit");
|
||||
SET_GLOBAL_FUN(get_explicit_arg, "get_explicit_arg");
|
||||
|
||||
SET_GLOBAL_FUN(mk_partial_explicit, "mk_partial_explicit");
|
||||
SET_GLOBAL_FUN(is_partial_explicit, "is_partial_explicit");
|
||||
SET_GLOBAL_FUN(get_partial_explicit_arg, "get_partial_explicit_arg");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -70,7 +69,6 @@ expr mk_consume_args(expr const & e);
|
|||
bool is_consume_args(expr const & e);
|
||||
expr const & get_consume_args_arg(expr const & e);
|
||||
|
||||
void open_explicit(lua_State * L);
|
||||
void initialize_explicit();
|
||||
void finalize_explicit();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@ Author: Leonardo de Moura
|
|||
#include "library/coercion.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/idx_metavar.h"
|
||||
#include "library/sorry.h"
|
||||
#include "library/placeholder.h"
|
||||
|
|
@ -58,7 +57,6 @@ void initialize_library_module() {
|
|||
initialize_print();
|
||||
initialize_placeholder();
|
||||
initialize_idx_metavar();
|
||||
initialize_kernel_bindings();
|
||||
initialize_io_state();
|
||||
initialize_unifier();
|
||||
initialize_kernel_serializer();
|
||||
|
|
@ -134,7 +132,6 @@ void finalize_library_module() {
|
|||
finalize_kernel_serializer();
|
||||
finalize_unifier();
|
||||
finalize_io_state();
|
||||
finalize_kernel_bindings();
|
||||
finalize_idx_metavar();
|
||||
finalize_placeholder();
|
||||
finalize_print();
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -1,98 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/script_state.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/type_checker.h"
|
||||
|
||||
namespace lean {
|
||||
void open_kernel_module(lua_State * L);
|
||||
UDATA_DEFS(level)
|
||||
UDATA_DEFS(expr)
|
||||
UDATA_DEFS(formatter)
|
||||
UDATA_DEFS(definition)
|
||||
UDATA_DEFS(macro_definition)
|
||||
UDATA_DEFS(environment)
|
||||
UDATA_DEFS(substitution)
|
||||
UDATA_DEFS(justification)
|
||||
UDATA_DEFS(constraint)
|
||||
UDATA_DEFS_CORE(constraint_seq)
|
||||
UDATA_DEFS(substitution)
|
||||
UDATA_DEFS(io_state)
|
||||
UDATA_DEFS_CORE(type_checker_ref)
|
||||
|
||||
int push_optional_level(lua_State * L, optional<level> const & e);
|
||||
int push_optional_expr(lua_State * L, optional<expr> const & e);
|
||||
int push_optional_justification(lua_State * L, optional<justification> const & j);
|
||||
int push_optional_declaration(lua_State * L, optional<declaration> const & e);
|
||||
int push_optional_constraint(lua_State * L, optional<constraint> const & c);
|
||||
int push_list_expr(lua_State * L, list<expr> const & l);
|
||||
/**
|
||||
\brief Return the formatter factory object associated with the given Lua State.
|
||||
This procedure checks for options at:
|
||||
1- Lean state object associated with \c L
|
||||
2- Lua Registry associated with \c L
|
||||
*/
|
||||
optional<formatter_factory> get_global_formatter_factory_core(lua_State * L);
|
||||
/**
|
||||
\brief Similar to \c get_global_formatter_factory_core, but returns
|
||||
the simple_formatter if a formatter can't be found.
|
||||
*/
|
||||
formatter_factory get_global_formatter_factory(lua_State * L);
|
||||
/**
|
||||
\brief Update the formatter object associated with the given Lua State.
|
||||
If \c L is associated with a Lean state object \c S, then we update the formatter of \c S.
|
||||
Otherwise, we update the registry of \c L.
|
||||
*/
|
||||
void set_global_formatter_factory(lua_State * L, formatter_factory const & fmtf);
|
||||
|
||||
/** \brief Make a fresh formatter object using the global formatter factory associated with L, and the global environment */
|
||||
formatter mk_formatter(lua_State * L);
|
||||
|
||||
/** \brief Set the Lua registry of a Lua state with an environment object. */
|
||||
void set_global_environment(lua_State * L, environment const & env);
|
||||
environment get_global_environment(lua_State * L);
|
||||
/**
|
||||
\brief Auxiliary class for temporarily setting the Lua registry of a Lua state
|
||||
with an environment object.
|
||||
*/
|
||||
class set_environment {
|
||||
lua_State * m_state;
|
||||
environment * m_old_env;
|
||||
public:
|
||||
set_environment(lua_State * L, environment & env);
|
||||
set_environment(script_state & S, environment & env):set_environment(S.get_state(), env) {}
|
||||
~set_environment();
|
||||
};
|
||||
|
||||
/** \brief Set the Lua registry of a Lua state with an io_state object. */
|
||||
void set_global_io_state(lua_State * L, io_state & ios);
|
||||
/**
|
||||
\brief Auxiliary class for temporarily setting the Lua registry of a Lua state
|
||||
with a Lean io_state object.
|
||||
*/
|
||||
class set_io_state {
|
||||
lua_State * m_state;
|
||||
io_state * m_prev;
|
||||
options m_prev_options;
|
||||
public:
|
||||
set_io_state(lua_State * L, io_state & ios);
|
||||
set_io_state(script_state & S, io_state & ios):set_io_state(S.get_state(), ios) {}
|
||||
~set_io_state();
|
||||
};
|
||||
/**
|
||||
\brief Return the Lean state object associated with the given Lua state.
|
||||
Return nullptr is there is none.
|
||||
*/
|
||||
io_state * get_io_state_ptr(lua_State * L);
|
||||
io_state get_io_state(lua_State * L);
|
||||
io_state to_io_state_ext(lua_State * L, int idx);
|
||||
void open_io_state(lua_State * L);
|
||||
|
||||
void initialize_kernel_bindings();
|
||||
void finalize_kernel_bindings();
|
||||
}
|
||||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/instantiate.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/match.h"
|
||||
#include "library/idx_metavar.h"
|
||||
|
|
@ -436,89 +435,4 @@ static pair<unsigned, unsigned> get_idx_meta_univ_ranges(expr const & e) {
|
|||
});
|
||||
return mk_pair(rlvl, rexp);
|
||||
}
|
||||
|
||||
typedef std::shared_ptr<match_plugin> match_plugin_ref;
|
||||
DECL_UDATA(match_plugin_ref)
|
||||
|
||||
static const struct luaL_Reg match_plugin_ref_m[] = {
|
||||
{"__gc", match_plugin_ref_gc},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
// version of whnf_match_plugin for Lua
|
||||
class whnf_match_plugin2 : public whnf_match_plugin {
|
||||
std::shared_ptr<type_checker> m_tc_ref;
|
||||
public:
|
||||
whnf_match_plugin2(std::shared_ptr<type_checker> & tc):
|
||||
whnf_match_plugin(*tc), m_tc_ref(tc) {}
|
||||
};
|
||||
|
||||
static int mk_whnf_match_plugin(lua_State * L) {
|
||||
return push_match_plugin_ref(L, match_plugin_ref(new whnf_match_plugin2(to_type_checker_ref(L, 1))));
|
||||
}
|
||||
|
||||
static int match(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
expr p = to_expr(L, 1);
|
||||
expr t = to_expr(L, 2);
|
||||
match_plugin * plugin = nullptr;
|
||||
if (nargs >= 3)
|
||||
plugin = to_match_plugin_ref(L, 3).get();
|
||||
if (!closed(t))
|
||||
throw exception("higher-order pattern matching failure, input term must not contain free variables");
|
||||
unsigned r1, r2;
|
||||
auto r1_r2 = get_idx_meta_univ_ranges(p);
|
||||
r1 = r1_r2.first;
|
||||
r2 = r1_r2.second;
|
||||
buffer<optional<level>> lsubst;
|
||||
buffer<optional<expr>> esubst;
|
||||
lsubst.resize(r1); esubst.resize(r2);
|
||||
if (match(p, t, lsubst, esubst, nullptr, nullptr, plugin)) {
|
||||
lua_newtable(L);
|
||||
int i = 1;
|
||||
for (auto s : esubst) {
|
||||
if (s)
|
||||
push_expr(L, *s);
|
||||
else
|
||||
lua_pushboolean(L, false);
|
||||
lua_rawseti(L, -2, i);
|
||||
i = i + 1;
|
||||
}
|
||||
lua_newtable(L);
|
||||
i = 1;
|
||||
for (auto s : lsubst) {
|
||||
if (s)
|
||||
push_level(L, *s);
|
||||
else
|
||||
lua_pushboolean(L, false);
|
||||
lua_rawseti(L, -2, i);
|
||||
i = i + 1;
|
||||
}
|
||||
} else {
|
||||
lua_pushnil(L);
|
||||
lua_pushnil(L);
|
||||
}
|
||||
return 2;
|
||||
}
|
||||
|
||||
static int mk_idx_metauniv(lua_State * L) {
|
||||
return push_level(L, mk_idx_metauniv(luaL_checkinteger(L, 1)));
|
||||
}
|
||||
|
||||
static int mk_idx_metavar(lua_State * L) {
|
||||
return push_expr(L, mk_idx_metavar(luaL_checkinteger(L, 1), to_expr(L, 2)));
|
||||
}
|
||||
|
||||
void open_match(lua_State * L) {
|
||||
luaL_newmetatable(L, match_plugin_ref_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, match_plugin_ref_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_whnf_match_plugin, "whnf_match_plugin");
|
||||
SET_GLOBAL_FUN(match_plugin_ref_pred, "is_match_plugin");
|
||||
SET_GLOBAL_FUN(mk_idx_metauniv, "mk_idx_metauniv");
|
||||
SET_GLOBAL_FUN(mk_idx_metavar, "mk_idx_metavar");
|
||||
SET_GLOBAL_FUN(match, "match");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <functional>
|
||||
#include "util/lua.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/buffer.h"
|
||||
|
|
@ -110,7 +109,6 @@ bool match(expr const & p, expr const & t,
|
|||
name const * prefix = nullptr, name_map<name> * name_subst = nullptr,
|
||||
match_plugin const * plugin = nullptr, bool * assigned = nullptr);
|
||||
|
||||
void open_match(lua_State * L);
|
||||
void initialize_match();
|
||||
void finalize_match();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#include "util/thread.h"
|
||||
#include "kernel/find_fn.h"
|
||||
#include "library/placeholder.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
|
||||
namespace lean {
|
||||
static name * g_implicit_placeholder_name = nullptr;
|
||||
|
|
@ -101,34 +100,4 @@ bool has_placeholder(expr const & e) {
|
|||
return false;
|
||||
});
|
||||
}
|
||||
|
||||
static int mk_level_placeholder(lua_State * L) { return push_level(L, mk_level_placeholder()); }
|
||||
static int mk_expr_placeholder(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 0)
|
||||
return push_expr(L, mk_expr_placeholder());
|
||||
else
|
||||
return push_expr(L, mk_expr_placeholder(some_expr(to_expr(L, 1))));
|
||||
}
|
||||
static int is_placeholder(lua_State * L) {
|
||||
if (is_expr(L, 1))
|
||||
return push_boolean(L, is_placeholder(to_expr(L, 1)));
|
||||
else
|
||||
return push_boolean(L, is_placeholder(to_level(L, 1)));
|
||||
}
|
||||
static int has_placeholder(lua_State * L) {
|
||||
if (is_expr(L, 1))
|
||||
return push_boolean(L, has_placeholder(to_expr(L, 1)));
|
||||
else
|
||||
return push_boolean(L, has_placeholder(to_level(L, 1)));
|
||||
}
|
||||
static int placeholder_type(lua_State * L) { return push_optional_expr(L, placeholder_type(to_expr(L, 1))); }
|
||||
|
||||
void open_placeholder(lua_State * L) {
|
||||
SET_GLOBAL_FUN(mk_level_placeholder, "mk_level_placeholder");
|
||||
SET_GLOBAL_FUN(mk_expr_placeholder, "mk_expr_placeholder");
|
||||
SET_GLOBAL_FUN(is_placeholder, "is_placeholder");
|
||||
SET_GLOBAL_FUN(placeholder_type, "placeholder_type");
|
||||
SET_GLOBAL_FUN(has_placeholder, "has_placeholder");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
// Placeholders are used to mark locations where additional
|
||||
|
|
@ -42,7 +41,6 @@ optional<expr> placeholder_type(expr const & e);
|
|||
/** \brief Return true iff the given expression contains placeholders. */
|
||||
bool has_placeholder(expr const & e);
|
||||
|
||||
void open_placeholder(lua_State * L);
|
||||
void initialize_placeholder();
|
||||
void finalize_placeholder();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include "util/hash.h"
|
||||
#include "library/private.h"
|
||||
#include "library/module.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/fingerprint.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -80,26 +79,6 @@ bool is_private(environment const & env, name const & n) {
|
|||
return static_cast<bool>(hidden_to_user_name(env, n));
|
||||
}
|
||||
|
||||
static int add_private_name(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
optional<unsigned> h;
|
||||
if (nargs > 2)
|
||||
h = lua_tonumber(L, 3);
|
||||
auto p = add_private_name(to_environment(L, 1), to_name_ext(L, 2), h);
|
||||
push_environment(L, p.first);
|
||||
push_name(L, p.second);
|
||||
return 2;
|
||||
}
|
||||
|
||||
static int hidden_to_user_name(lua_State * L) {
|
||||
return push_optional_name(L, hidden_to_user_name(to_environment(L, 1), to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
void open_private(lua_State * L) {
|
||||
SET_GLOBAL_FUN(add_private_name, "add_private_name");
|
||||
SET_GLOBAL_FUN(hidden_to_user_name, "hidden_to_user_name");
|
||||
}
|
||||
|
||||
void initialize_private() {
|
||||
g_ext = new private_ext_reg();
|
||||
g_private = new name("private");
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/optional.h"
|
||||
#include "util/lua.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -33,7 +32,6 @@ optional<name> hidden_to_user_name(environment const & env, name const & n);
|
|||
|
||||
bool is_private(environment const & env, name const & n);
|
||||
|
||||
void open_private(lua_State * L);
|
||||
void initialize_private();
|
||||
void finalize_private();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,7 +11,6 @@ Author: Leonardo de Moura
|
|||
#include "library/kernel_serializer.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/attribute_manager.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -177,67 +176,4 @@ type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb)
|
|||
type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen) {
|
||||
return mk_type_checker(env, std::move(ngen), [](name const &) { return true; });
|
||||
}
|
||||
|
||||
static int mk_opaque_type_checker(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 0) {
|
||||
type_checker_ref r(mk_opaque_type_checker(get_global_environment(L), name_generator()));
|
||||
return push_type_checker_ref(L, r);
|
||||
} else if (nargs == 1) {
|
||||
type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), name_generator()));
|
||||
return push_type_checker_ref(L, r);
|
||||
} else {
|
||||
type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child()));
|
||||
return push_type_checker_ref(L, r);
|
||||
}
|
||||
}
|
||||
|
||||
static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 0) {
|
||||
type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), rb));
|
||||
return push_type_checker_ref(L, r);
|
||||
} else if (nargs == 1) {
|
||||
type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb));
|
||||
return push_type_checker_ref(L, r);
|
||||
} else {
|
||||
type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child(), rb));
|
||||
return push_type_checker_ref(L, r);
|
||||
}
|
||||
}
|
||||
|
||||
static int mk_reducible_type_checker(lua_State * L) {
|
||||
return mk_reducible_checker_core(L, UnfoldReducible);
|
||||
}
|
||||
|
||||
static int mk_non_irreducible_type_checker(lua_State * L) {
|
||||
return mk_reducible_checker_core(L, UnfoldSemireducible);
|
||||
}
|
||||
|
||||
static int set_reducible(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
environment const & env = to_environment(L, 1);
|
||||
if (nargs == 3) {
|
||||
return push_environment(L, set_reducible(env, to_name_ext(L, 2),
|
||||
static_cast<reducible_status>(lua_tonumber(L, 3)),
|
||||
get_namespace(env), true));
|
||||
} else {
|
||||
return push_environment(L, set_reducible(env, to_name_ext(L, 2),
|
||||
static_cast<reducible_status>(lua_tonumber(L, 3)),
|
||||
get_namespace(env), lua_toboolean(L, 4)));
|
||||
}
|
||||
}
|
||||
|
||||
void open_reducible(lua_State * L) {
|
||||
lua_newtable(L);
|
||||
SET_ENUM("Reducible", reducible_status::Reducible);
|
||||
SET_ENUM("QuasiReducible", reducible_status::Quasireducible);
|
||||
SET_ENUM("SemiReducible", reducible_status::Semireducible);
|
||||
SET_ENUM("Irreducible", reducible_status::Irreducible);
|
||||
lua_setglobal(L, "reducible_status");
|
||||
SET_GLOBAL_FUN(set_reducible, "set_reducible");
|
||||
SET_GLOBAL_FUN(mk_opaque_type_checker, "opaque_type_checker");
|
||||
SET_GLOBAL_FUN(mk_non_irreducible_type_checker, "non_irreducible_type_checker");
|
||||
SET_GLOBAL_FUN(mk_reducible_type_checker, "reducible_type_checker");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -49,5 +49,4 @@ type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator
|
|||
|
||||
void initialize_reducible();
|
||||
void finalize_reducible();
|
||||
void open_reducible(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/justification.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "kernel/free_vars.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/kernel_serializer.h"
|
||||
#include "library/bin_app.h"
|
||||
#include "library/constants.h"
|
||||
|
|
@ -348,7 +347,4 @@ void finalize_resolve_macro() {
|
|||
delete g_resolve_opcode;
|
||||
delete g_resolve_macro_name;
|
||||
}
|
||||
|
||||
static int mk_resolve_macro(lua_State * L) { return push_expr(L, mk_resolve_macro(to_expr(L, 1), to_expr(L, 2), to_expr(L, 3))); }
|
||||
void open_resolve_macro(lua_State * L) { SET_GLOBAL_FUN(mk_resolve_macro, "resolve_macro"); }
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,12 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
expr mk_resolve_macro(expr const & l, expr const & H1, expr const & H2);
|
||||
void open_resolve_macro(lua_State * L);
|
||||
void initialize_resolve_macro();
|
||||
void finalize_resolve_macro();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include "util/sstream.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
|
||||
namespace lean {
|
||||
typedef std::tuple<name, using_namespace_fn, export_namespace_fn, push_scope_fn, pop_scope_fn> entry;
|
||||
|
|
@ -216,50 +215,6 @@ bool has_open_scopes(environment const & env) {
|
|||
return !is_nil(ext.m_namespaces);
|
||||
}
|
||||
|
||||
static int using_namespace_objects(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
environment const & env = to_environment(L, 1);
|
||||
name n = to_name_ext(L, 2);
|
||||
if (nargs == 2)
|
||||
return push_environment(L, using_namespace(env, get_io_state(L), n));
|
||||
else if (nargs == 3)
|
||||
return push_environment(L, using_namespace(env, get_io_state(L), n, to_name_ext(L, 3)));
|
||||
else
|
||||
return push_environment(L, using_namespace(env, to_io_state(L, 4), n, to_name_ext(L, 3)));
|
||||
}
|
||||
|
||||
static int push_scope(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 1)
|
||||
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Section));
|
||||
else if (nargs == 2)
|
||||
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Namespace, to_name_ext(L, 2)));
|
||||
scope_kind k = static_cast<scope_kind>(lua_tonumber(L, 3));
|
||||
if (nargs == 3)
|
||||
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), k, to_name_ext(L, 2)));
|
||||
else
|
||||
return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 4), k, to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int pop_scope(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 1)
|
||||
return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L)));
|
||||
else
|
||||
return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L), to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
void open_scoped_ext(lua_State * L) {
|
||||
SET_GLOBAL_FUN(using_namespace_objects, "using_namespace_objects");
|
||||
SET_GLOBAL_FUN(push_scope, "push_scope");
|
||||
SET_GLOBAL_FUN(pop_scope, "pop_scope");
|
||||
|
||||
lua_newtable(L);
|
||||
SET_ENUM("Namespace", scope_kind::Namespace);
|
||||
SET_ENUM("Section", scope_kind::Section);
|
||||
lua_setglobal(L, "scope_kind");
|
||||
}
|
||||
|
||||
void initialize_scoped_ext() {
|
||||
g_exts = new scoped_exts();
|
||||
g_ext = new scope_mng_ext_reg();
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include "util/list.h"
|
||||
#include "util/rb_map.h"
|
||||
#include "util/name.h"
|
||||
#include "util/lua.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/module.h"
|
||||
|
|
@ -81,8 +80,6 @@ environment mark_namespace_as_open(environment const & env, name const & n);
|
|||
/** \brief Return the set of namespaces marked as "open" using \c mark_namespace_as_open. */
|
||||
name_set get_opened_namespaces(environment const & env);
|
||||
|
||||
void open_scoped_ext(lua_State * L);
|
||||
|
||||
/** \brief Auxilary template used to simplify the creation of environment extensions that support
|
||||
the scope */
|
||||
template<typename Config>
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/error_msgs.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/occurs.h"
|
||||
#include "library/constants.h"
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "library/tactic/elaborate.h"
|
||||
namespace lean {
|
||||
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
|
||||
|
|
|
|||
|
|
@ -15,7 +15,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/type_checker.h"
|
||||
#include "kernel/metavar.h"
|
||||
#include "library/util.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/tactic/goal.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -179,60 +178,4 @@ io_state_stream const & operator<<(io_state_stream const & out, goal const & g)
|
|||
out.get_stream() << mk_pair(g.pp(out.get_formatter()), opts);
|
||||
return out;
|
||||
}
|
||||
|
||||
DECL_UDATA(goal)
|
||||
|
||||
static int mk_goal(lua_State * L) { return push_goal(L, goal(to_expr(L, 1), to_expr(L, 2))); }
|
||||
static int goal_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).get_meta()); }
|
||||
static int goal_type(lua_State * L) { return push_expr(L, to_goal(L, 1).get_type()); }
|
||||
static int goal_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
goal & g = to_goal(L, 1);
|
||||
formatter fmt = mk_formatter(L);
|
||||
options opts = get_global_options(L);
|
||||
out << mk_pair(g.pp(fmt), opts);
|
||||
lua_pushstring(L, out.str().c_str());
|
||||
return 1;
|
||||
}
|
||||
static int goal_mk_meta(lua_State * L) {
|
||||
return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3)));
|
||||
}
|
||||
|
||||
static int goal_pp(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
goal & g = to_goal(L, 1);
|
||||
if (nargs == 1) {
|
||||
return push_format(L, g.pp(mk_formatter(L)));
|
||||
} else {
|
||||
return push_format(L, g.pp(to_formatter(L, 2)));
|
||||
}
|
||||
}
|
||||
static int goal_validate_locals(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate_locals()); }
|
||||
static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate(to_environment(L, 2))); }
|
||||
static int goal_abstract(lua_State * L) { return push_expr(L, to_goal(L, 1).abstract(to_expr(L, 2))); }
|
||||
static int goal_name(lua_State * L) { return push_name(L, to_goal(L, 1).get_name()); }
|
||||
|
||||
static const struct luaL_Reg goal_m[] = {
|
||||
{"__gc", goal_gc}, // never throws
|
||||
{"__tostring", safe_function<goal_tostring>},
|
||||
{"abstract", safe_function<goal_abstract>},
|
||||
{"mk_meta", safe_function<goal_mk_meta>},
|
||||
{"pp", safe_function<goal_pp>},
|
||||
{"validate", safe_function<goal_validate>},
|
||||
{"validate_locals", safe_function<goal_validate_locals>},
|
||||
{"meta", safe_function<goal_meta>},
|
||||
{"type", safe_function<goal_type>},
|
||||
{"name", safe_function<goal_name>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_goal(lua_State * L) {
|
||||
luaL_newmetatable(L, goal_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, goal_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(goal_pred, "is_goal");
|
||||
SET_GLOBAL_FUN(mk_goal, "goal");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/lua.h"
|
||||
#include "util/list.h"
|
||||
#include "util/name.h"
|
||||
#include "kernel/formatter.h"
|
||||
|
|
@ -111,7 +110,4 @@ name get_unused_name(name const & prefix, unsigned & idx, expr const & meta);
|
|||
name get_unused_name(name const & prefix, expr const & meta);
|
||||
|
||||
io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
|
||||
|
||||
UDATA_DEFS(goal)
|
||||
void open_goal(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/instantiate.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/tactic/proof_state.h"
|
||||
|
||||
#ifndef LEAN_PROOF_STATE_GOAL_NAMES
|
||||
|
|
@ -99,163 +98,13 @@ proof_state apply_substitution(proof_state const & s) {
|
|||
return proof_state(s, goals(new_g, gs), subst);
|
||||
}
|
||||
|
||||
DECL_UDATA(goals)
|
||||
|
||||
static int mk_goals(lua_State * L) {
|
||||
int i = lua_gettop(L);
|
||||
goals r;
|
||||
if (i > 0 && is_goals(L, i)) {
|
||||
r = to_goals(L, i);
|
||||
i--;
|
||||
}
|
||||
while (i > 0) {
|
||||
r = goals(to_goal(L, i), r);
|
||||
i--;
|
||||
}
|
||||
return push_goals(L, r);
|
||||
}
|
||||
|
||||
static int goals_is_nil(lua_State * L) {
|
||||
lua_pushboolean(L, !to_goals(L, 1));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int goals_head(lua_State * L) {
|
||||
goals const & hs = to_goals(L, 1);
|
||||
if (!hs)
|
||||
throw exception("head method expects a non-empty goal list");
|
||||
return push_goal(L, head(hs));
|
||||
}
|
||||
|
||||
static int goals_tail(lua_State * L) {
|
||||
goals const & hs = to_goals(L, 1);
|
||||
if (!hs)
|
||||
throw exception("tail method expects a non-empty goal list");
|
||||
push_goals(L, tail(hs));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int goals_next(lua_State * L) {
|
||||
goals & hs = to_goals(L, lua_upvalueindex(1));
|
||||
if (hs) {
|
||||
push_goals(L, tail(hs));
|
||||
lua_replace(L, lua_upvalueindex(1));
|
||||
return push_goal(L, head(hs));
|
||||
} else {
|
||||
lua_pushnil(L);
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
static int goals_items(lua_State * L) {
|
||||
goals & hs = to_goals(L, 1);
|
||||
push_goals(L, hs); // upvalue(1): goals
|
||||
lua_pushcclosure(L, &safe_function<goals_next>, 1); // create closure with 1 upvalue
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int goals_len(lua_State * L) {
|
||||
return push_integer(L, length(to_goals(L, 1)));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg goals_m[] = {
|
||||
{"__gc", goals_gc}, // never throws
|
||||
{"__len", safe_function<goals_len>},
|
||||
{"size", safe_function<goals_len>},
|
||||
{"pairs", safe_function<goals_items>},
|
||||
{"is_nil", safe_function<goals_is_nil>},
|
||||
{"empty", safe_function<goals_is_nil>},
|
||||
{"head", safe_function<goals_head>},
|
||||
{"tail", safe_function<goals_tail>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
DECL_UDATA(proof_state)
|
||||
|
||||
static int mk_proof_state(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2) {
|
||||
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2)));
|
||||
} else if (nargs == 3 && is_proof_state(L, 1)) {
|
||||
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
|
||||
} else if (nargs == 3) {
|
||||
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3),
|
||||
constraints()));
|
||||
} else {
|
||||
throw exception("proof_state invalid number of arguments");
|
||||
}
|
||||
}
|
||||
|
||||
static name * g_tmp_prefix = nullptr;
|
||||
static int to_proof_state(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2)
|
||||
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix)));
|
||||
else
|
||||
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3)));
|
||||
}
|
||||
|
||||
static int proof_state_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
proof_state & s = to_proof_state(L, 1);
|
||||
options opts = get_global_options(L);
|
||||
out << mk_pair(s.pp(get_global_environment(L), get_io_state(L)), opts);
|
||||
lua_pushstring(L, out.str().c_str());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int proof_state_get_goals(lua_State * L) { return push_goals(L, to_proof_state(L, 1).get_goals()); }
|
||||
static int proof_state_get_ngen(lua_State * L) { return push_name_generator(L, to_proof_state(L, 1).get_ngen()); }
|
||||
static int proof_state_get_subst(lua_State * L) { return push_substitution(L, to_proof_state(L, 1).get_subst()); }
|
||||
static int proof_state_is_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_final_state()); }
|
||||
static int proof_state_pp(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
proof_state & s = to_proof_state(L, 1);
|
||||
if (nargs == 1)
|
||||
return push_format(L, s.pp(get_global_environment(L), get_io_state(L)));
|
||||
else
|
||||
return push_format(L, s.pp(to_environment(L, 1), to_io_state(L, 2)));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg proof_state_m[] = {
|
||||
{"__gc", proof_state_gc}, // never throws
|
||||
{"__tostring", safe_function<proof_state_tostring>},
|
||||
{"pp", safe_function<proof_state_pp>},
|
||||
{"goals", safe_function<proof_state_get_goals>},
|
||||
{"subst", safe_function<proof_state_get_subst>},
|
||||
{"ngen", safe_function<proof_state_get_ngen>},
|
||||
{"is_final_state", safe_function<proof_state_is_final_state>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_proof_state(lua_State * L) {
|
||||
luaL_newmetatable(L, goals_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, goals_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(goals_pred, "is_goals");
|
||||
SET_GLOBAL_FUN(mk_goals, "goals");
|
||||
|
||||
luaL_newmetatable(L, proof_state_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, proof_state_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(proof_state_pred, "is_proof_state");
|
||||
SET_GLOBAL_FUN(mk_proof_state, "proof_state");
|
||||
SET_GLOBAL_FUN(to_proof_state, "to_proof_state");
|
||||
}
|
||||
|
||||
void initialize_proof_state() {
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
g_proof_state_goal_names = new name{"tactic", "goal_names"};
|
||||
register_bool_option(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES,
|
||||
"(tactic) display goal names when pretty printing proof state");
|
||||
}
|
||||
|
||||
void finalize_proof_state() {
|
||||
delete g_tmp_prefix;
|
||||
delete g_proof_state_goal_names;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
|||
#include <utility>
|
||||
#include <algorithm>
|
||||
#include <functional>
|
||||
#include "util/lua.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/name_set.h"
|
||||
#include "kernel/metavar.h"
|
||||
|
|
@ -84,10 +83,6 @@ proof_state to_proof_state(expr const & meta, expr const & type, name_generator
|
|||
|
||||
goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
|
||||
|
||||
UDATA_DEFS_CORE(goals)
|
||||
UDATA_DEFS(proof_state)
|
||||
void open_proof_state(lua_State * L);
|
||||
|
||||
void initialize_proof_state();
|
||||
void finalize_proof_state();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#include <utility>
|
||||
#include <chrono>
|
||||
#include <string>
|
||||
#include "util/luaref.h"
|
||||
#include "util/sstream.h"
|
||||
#include "util/interrupt.h"
|
||||
#include "util/lazy_list_fn.h"
|
||||
|
|
@ -18,7 +17,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/replace_fn.h"
|
||||
#include "library/normalize.h"
|
||||
#include "library/util.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/tactic/tactic.h"
|
||||
#include "library/io_state_stream.h"
|
||||
|
||||
|
|
@ -291,182 +289,4 @@ tactic all_goals(tactic const & t) {
|
|||
return r(env, ios, s);
|
||||
});
|
||||
}
|
||||
|
||||
DECL_UDATA(proof_state_seq)
|
||||
static const struct luaL_Reg proof_state_seq_m[] = {
|
||||
{"__gc", proof_state_seq_gc}, // never throws
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static int proof_state_seq_next(lua_State * L) {
|
||||
proof_state_seq seq = to_proof_state_seq(L, lua_upvalueindex(1));
|
||||
auto p = seq.pull();
|
||||
if (p) {
|
||||
push_proof_state_seq(L, p->second);
|
||||
lua_replace(L, lua_upvalueindex(1));
|
||||
push_proof_state(L, p->first);
|
||||
} else {
|
||||
lua_pushnil(L);
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int push_proof_state_seq_it(lua_State * L, proof_state_seq const & seq) {
|
||||
push_proof_state_seq(L, seq);
|
||||
lua_pushcclosure(L, &safe_function<proof_state_seq_next>, 1); // create closure with 1 upvalue
|
||||
return 1;
|
||||
}
|
||||
|
||||
DECL_UDATA(tactic)
|
||||
|
||||
[[ noreturn ]] void throw_tactic_expected(int i) {
|
||||
throw exception(sstream() << "arg #" << i << " must be a tactic or a function that returns a tactic");
|
||||
}
|
||||
|
||||
static int tactic_call_core(lua_State * L, tactic t, environment env, io_state ios, proof_state s) {
|
||||
return push_proof_state_seq_it(L, t(env, ios, s));
|
||||
}
|
||||
|
||||
static int tactic_call(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
tactic t = to_tactic(L, 1);
|
||||
environment env = to_environment(L, 2);
|
||||
if (nargs == 3)
|
||||
return tactic_call_core(L, t, env, get_io_state(L), to_proof_state(L, 3));
|
||||
else
|
||||
return tactic_call_core(L, t, env, to_io_state(L, 3), to_proof_state(L, 4));
|
||||
}
|
||||
|
||||
typedef tactic (*binary_tactic_fn)(tactic const &, tactic const &);
|
||||
|
||||
template<binary_tactic_fn F>
|
||||
static int nary_tactic(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs < 2)
|
||||
throw exception("tactical expects at least two arguments");
|
||||
tactic r = F(to_tactic(L, 1), to_tactic(L, 2));
|
||||
for (int i = 3; i <= nargs; i++)
|
||||
r = F(r, to_tactic(L, i));
|
||||
return push_tactic(L, r);
|
||||
}
|
||||
|
||||
static int tactic_then(lua_State * L) { return push_tactic(L, then(to_tactic(L, 1), to_tactic(L, 2))); }
|
||||
static int tactic_orelse(lua_State * L) { return push_tactic(L, orelse(to_tactic(L, 1), to_tactic(L, 2))); }
|
||||
static int tactic_append(lua_State * L) { return push_tactic(L, append(to_tactic(L, 1), to_tactic(L, 2))); }
|
||||
static int tactic_interleave(lua_State * L) { return push_tactic(L, interleave(to_tactic(L, 1), to_tactic(L, 2))); }
|
||||
static int tactic_par(lua_State * L) { return push_tactic(L, par(to_tactic(L, 1), to_tactic(L, 2))); }
|
||||
static int tactic_repeat(lua_State * L) { return push_tactic(L, repeat(to_tactic(L, 1))); }
|
||||
static int tactic_repeat_at_most(lua_State * L) { return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
|
||||
static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
|
||||
static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
|
||||
static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
|
||||
static int tactic_focus(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 1)
|
||||
return push_tactic(L, focus(to_tactic(L, 1)));
|
||||
else
|
||||
return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2)));
|
||||
}
|
||||
static int mk_lua_tactic01(lua_State * L) {
|
||||
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
|
||||
luaref ref(L, 1);
|
||||
tactic t = tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
|
||||
ref.push(); // push user-fun on the stack
|
||||
push_environment(L, env); // push args...
|
||||
push_io_state(L, ios);
|
||||
push_proof_state(L, s);
|
||||
pcall(L, 3, 1, 0);
|
||||
optional<proof_state> r;
|
||||
if (is_proof_state(L, -1))
|
||||
r = to_proof_state(L, -1);
|
||||
lua_pop(L, 1);
|
||||
return r;
|
||||
});
|
||||
return push_tactic(L, t);
|
||||
}
|
||||
|
||||
static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) {
|
||||
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
|
||||
luaref ref(L, 1);
|
||||
tactic t = tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
|
||||
return mk_proof_state_seq([=]() {
|
||||
ref.push(); // push user-fun on the stack
|
||||
push_environment(L, env); // push args...
|
||||
push_io_state(L, ios);
|
||||
push_proof_state(L, s);
|
||||
pcall(L, 3, 1, 0);
|
||||
bool cond = lua_toboolean(L, -1);
|
||||
lua_pop(L, 1);
|
||||
if (cond) {
|
||||
return t1(env, ios, s).pull();
|
||||
} else {
|
||||
return t2(env, ios, s).pull();
|
||||
}
|
||||
});
|
||||
});
|
||||
return push_tactic(L, t);
|
||||
}
|
||||
|
||||
static int mk_lua_cond_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_tactic(L, 2), to_tactic(L, 3)); }
|
||||
static int mk_lua_when_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_tactic(L, 2), id_tactic()); }
|
||||
static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tactic()); }
|
||||
static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tactic()); }
|
||||
static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); }
|
||||
static int mk_beta_tactic(lua_State * L) { return push_tactic(L, beta_tactic()); }
|
||||
static const struct luaL_Reg tactic_m[] = {
|
||||
{"__gc", tactic_gc}, // never throws
|
||||
{"__call", safe_function<tactic_call>},
|
||||
{"__concat", safe_function<tactic_then>},
|
||||
{"__pow", safe_function<tactic_orelse>},
|
||||
{"__add", safe_function<tactic_append>},
|
||||
{"then", safe_function<tactic_then>},
|
||||
{"orelse", safe_function<tactic_orelse>},
|
||||
{"append", safe_function<tactic_append>},
|
||||
{"interleave", safe_function<tactic_interleave>},
|
||||
{"par", safe_function<tactic_par>},
|
||||
{"repeat", safe_function<tactic_repeat>},
|
||||
{"repeat_at_most", safe_function<tactic_repeat_at_most>},
|
||||
{"take", safe_function<tactic_take>},
|
||||
{"try_for", safe_function<tactic_try_for>},
|
||||
{"using_params", safe_function<tactic_using_params>},
|
||||
{"using", safe_function<tactic_using_params>},
|
||||
{"focus", safe_function<tactic_focus>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_tactic(lua_State * L) {
|
||||
luaL_newmetatable(L, proof_state_seq_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, proof_state_seq_m, 0);
|
||||
SET_GLOBAL_FUN(proof_state_seq_pred, "is_proof_state_seq");
|
||||
|
||||
luaL_newmetatable(L, tactic_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, tactic_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(tactic_pred, "is_tactic");
|
||||
SET_GLOBAL_FUN(mk_id_tactic, "id_tac");
|
||||
SET_GLOBAL_FUN(mk_now_tactic, "now_tac");
|
||||
SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac");
|
||||
SET_GLOBAL_FUN(mk_beta_tactic, "beta_tac");
|
||||
SET_GLOBAL_FUN(mk_lua_tactic01, "tactic01");
|
||||
|
||||
// HOL-like tactic names
|
||||
SET_GLOBAL_FUN(nary_tactic<then>, "Then");
|
||||
SET_GLOBAL_FUN(nary_tactic<orelse>, "OrElse");
|
||||
SET_GLOBAL_FUN(nary_tactic<interleave>, "Interleave");
|
||||
SET_GLOBAL_FUN(nary_tactic<append>, "Append");
|
||||
SET_GLOBAL_FUN(nary_tactic<par>, "Par");
|
||||
SET_GLOBAL_FUN(tactic_repeat, "Repeat");
|
||||
SET_GLOBAL_FUN(tactic_repeat_at_most, "RepeatAtMost");
|
||||
SET_GLOBAL_FUN(mk_lua_cond_tactic, "Cond");
|
||||
SET_GLOBAL_FUN(mk_lua_when_tactic, "When");
|
||||
SET_GLOBAL_FUN(tactic_try_for, "TryFor");
|
||||
SET_GLOBAL_FUN(tactic_take, "Take");
|
||||
SET_GLOBAL_FUN(tactic_using_params, "Using");
|
||||
SET_GLOBAL_FUN(tactic_using_params, "UsingParams");
|
||||
SET_GLOBAL_FUN(tactic_focus, "Focus");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -150,8 +150,4 @@ inline tactic focus(tactic const & t) { return focus(t, 0); }
|
|||
tactic beta_tactic();
|
||||
/** \brief Apply \c t to all goals in the proof state */
|
||||
tactic all_goals(tactic const & t);
|
||||
|
||||
UDATA_DEFS_CORE(proof_state_seq)
|
||||
UDATA_DEFS_CORE(tactic);
|
||||
void open_tactic(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include <limits>
|
||||
#include <algorithm>
|
||||
#include "util/interrupt.h"
|
||||
#include "util/luaref.h"
|
||||
#include "util/lazy_list_fn.h"
|
||||
#include "util/sstream.h"
|
||||
#include "util/lbool.h"
|
||||
|
|
@ -30,7 +29,6 @@ Author: Leonardo de Moura
|
|||
#include "library/unifier.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/print.h"
|
||||
#include "library/expr_lt.h"
|
||||
#include "library/projection.h"
|
||||
|
|
@ -2845,163 +2843,6 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r
|
|||
}
|
||||
}
|
||||
|
||||
static int unify_simple(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unify_status r;
|
||||
if (nargs == 2)
|
||||
r = unify_simple(to_substitution(L, 1), to_constraint(L, 2));
|
||||
else if (nargs == 3 && is_expr(L, 2))
|
||||
r = unify_simple(to_substitution(L, 1), to_expr(L, 2), to_expr(L, 3), justification());
|
||||
else if (nargs == 3 && is_level(L, 2))
|
||||
r = unify_simple(to_substitution(L, 1), to_level(L, 2), to_level(L, 3), justification());
|
||||
else if (is_expr(L, 2))
|
||||
r = unify_simple(to_substitution(L, 1), to_expr(L, 2), to_expr(L, 3), to_justification(L, 4));
|
||||
else
|
||||
r = unify_simple(to_substitution(L, 1), to_level(L, 2), to_level(L, 3), to_justification(L, 4));
|
||||
return push_integer(L, static_cast<unsigned>(r));
|
||||
}
|
||||
|
||||
DECL_UDATA(unify_result_seq)
|
||||
|
||||
static const struct luaL_Reg unify_result_seq_m[] = {
|
||||
{"__gc", unify_result_seq_gc},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static int unify_result_seq_next(lua_State * L) {
|
||||
unify_result_seq seq = to_unify_result_seq(L, lua_upvalueindex(1));
|
||||
unify_result_seq::maybe_pair p;
|
||||
p = seq.pull();
|
||||
if (p) {
|
||||
push_unify_result_seq(L, p->second);
|
||||
lua_replace(L, lua_upvalueindex(1));
|
||||
push_substitution(L, p->first.first);
|
||||
// TODO(Leo): return postponed constraints
|
||||
} else {
|
||||
lua_pushnil(L);
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int push_unify_result_seq_it(lua_State * L, unify_result_seq const & seq) {
|
||||
push_unify_result_seq(L, seq);
|
||||
lua_pushcclosure(L, &safe_function<unify_result_seq_next>, 1); // create closure with 1 upvalue
|
||||
return 1;
|
||||
}
|
||||
|
||||
static void to_constraint_buffer(lua_State * L, int idx, buffer<constraint> & cs) {
|
||||
luaL_checktype(L, idx, LUA_TTABLE);
|
||||
lua_pushvalue(L, idx); // put table on top of the stack
|
||||
int n = objlen(L, idx);
|
||||
for (int i = 1; i <= n; i++) {
|
||||
lua_rawgeti(L, -1, i);
|
||||
cs.push_back(to_constraint(L, -1));
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
|
||||
#if 0
|
||||
static constraints to_constraints(lua_State * L, int idx) {
|
||||
buffer<constraint> cs;
|
||||
to_constraint_buffer(L, idx, cs);
|
||||
return to_list(cs.begin(), cs.end());
|
||||
}
|
||||
|
||||
static unifier_plugin to_unifier_plugin(lua_State * L, int idx) {
|
||||
luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
|
||||
luaref f(L, idx);
|
||||
return unifier_plugin([=](constraint const & c, name_generator && ngen) {
|
||||
lua_State * L = f.get_state();
|
||||
f.push();
|
||||
push_constraint(L, c);
|
||||
push_name_generator(L, ngen);
|
||||
pcall(L, 2, 1, 0);
|
||||
lazy_list<constraints> r;
|
||||
if (is_constraint(L, -1)) {
|
||||
// single constraint
|
||||
r = lazy_list<constraints>(constraints(to_constraint(L, -1)));
|
||||
} else if (lua_istable(L, -1)) {
|
||||
int num = objlen(L, -1);
|
||||
if (num == 0) {
|
||||
// empty table
|
||||
r = lazy_list<constraints>();
|
||||
} else {
|
||||
lua_rawgeti(L, -1, 1);
|
||||
if (is_constraint(L, -1)) {
|
||||
// array of constraints case
|
||||
lua_pop(L, 1);
|
||||
r = lazy_list<constraints>(to_constraints(L, -1));
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
buffer<constraints> css;
|
||||
// array of array of constraints
|
||||
for (int i = 1; i <= num; i++) {
|
||||
lua_rawgeti(L, -1, i);
|
||||
css.push_back(to_constraints(L, -1));
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
r = to_lazy(to_list(css.begin(), css.end()));
|
||||
}
|
||||
}
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
// nil case
|
||||
r = lazy_list<constraints>();
|
||||
} else {
|
||||
throw exception("invalid unifier plugin, the result value must be a constrant, "
|
||||
"nil, an array of constraints, or an array of arrays of constraints");
|
||||
}
|
||||
lua_pop(L, 1);
|
||||
return r;
|
||||
});
|
||||
}
|
||||
#endif
|
||||
|
||||
static name * g_tmp_prefix = nullptr;
|
||||
|
||||
static int unify(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unify_result_seq r;
|
||||
environment const & env = to_environment(L, 1);
|
||||
if (is_expr(L, 2)) {
|
||||
if (nargs == 6)
|
||||
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5),
|
||||
unifier_config(to_options(L, 6)));
|
||||
else if (nargs == 5)
|
||||
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5));
|
||||
else
|
||||
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child());
|
||||
} else {
|
||||
buffer<constraint> cs;
|
||||
to_constraint_buffer(L, 2, cs);
|
||||
if (nargs == 5)
|
||||
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4),
|
||||
unifier_config(to_options(L, 5)));
|
||||
else if (nargs == 4)
|
||||
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4));
|
||||
else
|
||||
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child());
|
||||
}
|
||||
return push_unify_result_seq_it(L, r);
|
||||
}
|
||||
|
||||
void open_unifier(lua_State * L) {
|
||||
luaL_newmetatable(L, unify_result_seq_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, unify_result_seq_m, 0);
|
||||
SET_GLOBAL_FUN(unify_result_seq_pred, "is_unify_result_seq");
|
||||
|
||||
SET_GLOBAL_FUN(unify_simple, "unify_simple");
|
||||
SET_GLOBAL_FUN(unify, "unify");
|
||||
|
||||
lua_newtable(L);
|
||||
SET_ENUM("Solved", unify_status::Solved);
|
||||
SET_ENUM("Failed", unify_status::Failed);
|
||||
SET_ENUM("Unsupported", unify_status::Unsupported);
|
||||
lua_setglobal(L, "unify_status");
|
||||
}
|
||||
|
||||
void initialize_unifier() {
|
||||
register_trace_class(name{"unifier"});
|
||||
g_unifier_max_steps = new name{"unifier", "max_steps"};
|
||||
|
|
@ -3020,11 +2861,9 @@ void initialize_unifier() {
|
|||
"(unifier) enable/disable nonchronological backtracking in the unifier (this option is only available for debugging and benchmarking purposes, and running experiments)");
|
||||
|
||||
g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification()));
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
}
|
||||
|
||||
void finalize_unifier() {
|
||||
delete g_tmp_prefix;
|
||||
delete g_dont_care_cnstr;
|
||||
delete g_unifier_max_steps;
|
||||
delete g_unifier_normalizer_max_steps;
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <utility>
|
||||
#include <functional>
|
||||
#include "util/lua.h"
|
||||
#include "util/lazy_list.h"
|
||||
#include "util/name_generator.h"
|
||||
#include "util/sexpr/options.h"
|
||||
|
|
@ -123,8 +122,6 @@ public:
|
|||
substitution const & get_substitution() const { return m_subst; }
|
||||
};
|
||||
|
||||
void open_unifier(lua_State * L);
|
||||
|
||||
void initialize_unifier();
|
||||
void finalize_unifier();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,13 +27,8 @@ add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
|
|||
add_test(lean_path1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -p)
|
||||
add_test(lean_path2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --path)
|
||||
add_test(export_all "${LEAN_SOURCE_DIR}/../bin/lean" --export-all=all.out "${LEAN_SOURCE_DIR}/../library/standard.lean")
|
||||
add_test(lean_luahook1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
|
||||
add_test(lean_luahook2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -k 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
|
||||
# add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")
|
||||
# add_test(lean_lua2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-u" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")
|
||||
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
|
||||
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
|
||||
add_test(lean_unknown_file2 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua")
|
||||
add_test(lean_server_trace "${CMAKE_CURRENT_BINARY_DIR}/lean" --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/consume_args.input")
|
||||
add_test(lean_server_trace "${CMAKE_CURRENT_BINARY_DIR}/lean" --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/options_cmd.trace")
|
||||
add_test(lean_server_trace "${CMAKE_CURRENT_BINARY_DIR}/lean" --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/commands.trace")
|
||||
|
|
@ -138,25 +133,6 @@ FOREACH(T ${LEANSLOWTESTS})
|
|||
set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
|
||||
ENDFOREACH(T)
|
||||
|
||||
# LEAN LUA TESTS
|
||||
file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
|
||||
FOREACH(T ${LEANLUATESTS})
|
||||
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
|
||||
add_test(NAME "leanluatest_${T_NAME}"
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
|
||||
COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
|
||||
ENDFOREACH(T)
|
||||
|
||||
# LEAN LUA SLOW TESTS
|
||||
file(GLOB LEANLUASLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lua/slow/*.lua")
|
||||
FOREACH(T ${LEANLUASLOWTESTS})
|
||||
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
|
||||
add_test(NAME "leanluaslowtest_${T_NAME}"
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/slow"
|
||||
COMMAND bash "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
|
||||
set_tests_properties("leanluaslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
|
||||
ENDFOREACH(T)
|
||||
|
||||
# LEAN DOCS
|
||||
file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
|
||||
FOREACH(T ${LEANDOCS})
|
||||
|
|
@ -166,15 +142,6 @@ FOREACH(T ${LEANDOCS})
|
|||
COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
|
||||
ENDFOREACH(T)
|
||||
|
||||
# LEAN LUA DOCS
|
||||
file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md")
|
||||
FOREACH(T ${LEANLUADOCS})
|
||||
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
|
||||
add_test(NAME "leanluadoc_${T_NAME}"
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua"
|
||||
COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
|
||||
ENDFOREACH(T)
|
||||
|
||||
# # Create the script lean.sh
|
||||
# # This is used to create a soft dependency on the Lean executable
|
||||
# # Some rules can only be applied if the lean executable exists,
|
||||
|
|
|
|||
|
|
@ -5,11 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "util/script_state.h"
|
||||
#include "util/thread_script_state.h"
|
||||
#include "library/module.h"
|
||||
#include "library/standard_kernel.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/error_handling.h"
|
||||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
|
|
@ -24,14 +21,10 @@ private:
|
|||
options opts;
|
||||
environment env;
|
||||
io_state ios;
|
||||
script_state S;
|
||||
set_environment set1;
|
||||
set_io_state set2;
|
||||
|
||||
public:
|
||||
emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1), opts("flycheck", true),
|
||||
env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()),
|
||||
S(lean::get_thread_script_state()), set1(S, env), set2(S, ios) {
|
||||
env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()) {
|
||||
}
|
||||
|
||||
int import_module(std::string mname) {
|
||||
|
|
|
|||
|
|
@ -16,9 +16,7 @@ Author: Leonardo de Moura
|
|||
#include "util/sstream.h"
|
||||
#include "util/interrupt.h"
|
||||
#include "util/memory.h"
|
||||
#include "util/script_state.h"
|
||||
#include "util/thread.h"
|
||||
#include "util/thread_script_state.h"
|
||||
#include "util/lean_path.h"
|
||||
#include "util/file_lock.h"
|
||||
#include "util/sexpr/options.h"
|
||||
|
|
@ -46,7 +44,6 @@ Author: Leonardo de Moura
|
|||
#include "version.h"
|
||||
#include "githash.h" // NOLINT
|
||||
|
||||
using lean::script_state;
|
||||
using lean::unreachable_reached;
|
||||
using lean::environment;
|
||||
using lean::io_state;
|
||||
|
|
@ -54,8 +51,6 @@ using lean::io_state_stream;
|
|||
using lean::regular;
|
||||
using lean::mk_environment;
|
||||
using lean::mk_hott_environment;
|
||||
using lean::set_environment;
|
||||
using lean::set_io_state;
|
||||
using lean::definition_cache;
|
||||
using lean::pos_info;
|
||||
using lean::pos_info_provider;
|
||||
|
|
@ -69,7 +64,7 @@ using lean::simple_pos_info_provider;
|
|||
using lean::shared_file_lock;
|
||||
using lean::exclusive_file_lock;
|
||||
|
||||
enum class input_kind { Unspecified, Lean, HLean, Lua, Trace };
|
||||
enum class input_kind { Unspecified, Lean, HLean, Trace };
|
||||
|
||||
static void on_ctrl_c(int ) {
|
||||
lean::request_interrupt();
|
||||
|
|
@ -95,7 +90,6 @@ static void display_help(std::ostream & out) {
|
|||
std::cout << " with unknown extension (default)\n";
|
||||
std::cout << " --hlean use parser for Lean default input format \n";
|
||||
std::cout << " and use HoTT compatible kernel for files, with unknown extension\n";
|
||||
std::cout << " --lua use Lua parser for files with unknown extension\n";
|
||||
std::cout << " --server-trace use lean server trace parser for files with unknown extension\n";
|
||||
std::cout << "Miscellaneous:\n";
|
||||
std::cout << " --help -h display this message\n";
|
||||
|
|
@ -103,9 +97,6 @@ static void display_help(std::ostream & out) {
|
|||
std::cout << " --githash display the git commit hash number used to build this binary\n";
|
||||
std::cout << " --path display the path used for finding Lean libraries and extensions\n";
|
||||
std::cout << " --output=file -o save the final environment in binary format in the given file\n";
|
||||
std::cout << " --luahook=num -k how often the Lua interpreter checks the interrupted flag,\n";
|
||||
std::cout << " it is useful for interrupting non-terminating user scripts,\n";
|
||||
std::cout << " 0 means 'do not check'.\n";
|
||||
std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n"
|
||||
<< " and type check all imported modules\n";
|
||||
std::cout << " --discard -r discard the proof of imported theorems after checking\n";
|
||||
|
|
@ -163,10 +154,8 @@ static struct option g_long_options[] = {
|
|||
{"help", no_argument, 0, 'h'},
|
||||
{"lean", no_argument, 0, 'l'},
|
||||
{"hlean", no_argument, 0, 'H'},
|
||||
{"lua", no_argument, 0, 'u'},
|
||||
{"server-trace", no_argument, 0, 'R'},
|
||||
{"path", no_argument, 0, 'p'},
|
||||
{"luahook", required_argument, 0, 'k'},
|
||||
{"githash", no_argument, 0, 'g'},
|
||||
{"output", required_argument, 0, 'o'},
|
||||
{"export", required_argument, 0, 'E'},
|
||||
|
|
@ -310,15 +299,9 @@ int main(int argc, char ** argv) {
|
|||
case 'H':
|
||||
default_k = input_kind::HLean;
|
||||
break;
|
||||
case 'u':
|
||||
default_k = input_kind::Lua;
|
||||
break;
|
||||
case 'R':
|
||||
default_k = input_kind::Trace;
|
||||
break;
|
||||
case 'k':
|
||||
script_state::set_check_interrupt_freq(atoi(optarg));
|
||||
break;
|
||||
case 'p':
|
||||
if (default_k == input_kind::HLean)
|
||||
lean::initialize_lean_path(true);
|
||||
|
|
@ -458,9 +441,6 @@ int main(int argc, char ** argv) {
|
|||
|
||||
environment env = has_hlean ? mk_hott_environment(trust_lvl) : mk_environment(trust_lvl);
|
||||
io_state ios(opts, lean::mk_pretty_formatter_factory());
|
||||
script_state S = lean::get_thread_script_state();
|
||||
set_environment set1(S, env);
|
||||
set_io_state set2(S, ios);
|
||||
definition_cache cache;
|
||||
definition_cache * cache_ptr = nullptr;
|
||||
if (read_cache) {
|
||||
|
|
@ -500,8 +480,6 @@ int main(int argc, char ** argv) {
|
|||
k = input_kind::Lean;
|
||||
} else if (strcmp(ext, "hlean") == 0) {
|
||||
k = input_kind::HLean;
|
||||
} else if (strcmp(ext, "lua") == 0) {
|
||||
k = input_kind::Lua;
|
||||
}
|
||||
}
|
||||
switch (k) {
|
||||
|
|
@ -515,9 +493,6 @@ int main(int argc, char ** argv) {
|
|||
ok = false;
|
||||
}
|
||||
break;
|
||||
case input_kind::Lua:
|
||||
lean::system_import(argv[i]);
|
||||
break;
|
||||
case input_kind::Trace:
|
||||
ok = lean::parse_server_trace(env, ios, argv[i], base_dir);
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#include <limits>
|
||||
#include <dirent.h>
|
||||
#include <algorithm>
|
||||
#include <string>
|
||||
|
|
@ -1365,7 +1366,7 @@ void random_test_on_i(unsigned i) {
|
|||
}
|
||||
|
||||
void random_test() {
|
||||
for (unsigned i = 0; i < UINT_MAX; i++) {
|
||||
for (unsigned i = 0; i < std::numeric_limits<unsigned>::max(); i++) {
|
||||
try {
|
||||
random_test_on_i(i);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,7 +11,6 @@ Author: Leonardo de Moura
|
|||
#include "util/debug.h"
|
||||
#include "util/shared_mutex.h"
|
||||
#include "util/interrupt.h"
|
||||
#include "util/thread_script_state.h"
|
||||
#include "util/init_module.h"
|
||||
using namespace lean;
|
||||
|
||||
|
|
@ -184,52 +183,6 @@ static void tst6() {
|
|||
t1.join();
|
||||
}
|
||||
|
||||
static __thread script_state * g_state = nullptr;
|
||||
|
||||
static void tst7() {
|
||||
std::cout << "start\n";
|
||||
system_import("import_test.lua");
|
||||
system_dostring("print('hello'); x = 10;");
|
||||
interruptible_thread t1([]() {
|
||||
g_state = new script_state();
|
||||
g_state->dostring("x = 1");
|
||||
script_state S = get_thread_script_state();
|
||||
S.dostring("print(x)\n"
|
||||
"for i = 1, 100000 do\n"
|
||||
" x = x + 1\n"
|
||||
"end\n"
|
||||
"print(x)\n");
|
||||
delete g_state;
|
||||
});
|
||||
interruptible_thread t2([]() {
|
||||
g_state = new script_state();
|
||||
g_state->dostring("x = 0");
|
||||
script_state S = get_thread_script_state();
|
||||
S.dostring("print(x)\n"
|
||||
"for i = 1, 20000 do\n"
|
||||
" x = x + 1\n"
|
||||
"end\n"
|
||||
"print(x)\n");
|
||||
delete g_state;
|
||||
});
|
||||
t1.join(); t2.join();
|
||||
std::cout << "done\n";
|
||||
}
|
||||
|
||||
static void tst8() {
|
||||
std::cout << "starting tst8\n";
|
||||
interruptible_thread t1([]() {
|
||||
script_state S = get_thread_script_state();
|
||||
S.dostring("print(x)\n"
|
||||
"for i = 1, 10000 do\n"
|
||||
" x = x + 1\n"
|
||||
"end\n"
|
||||
"print(x)\n"
|
||||
"print(fact(10))\n");
|
||||
});
|
||||
t1.join();
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
initialize_util_module();
|
||||
|
|
@ -239,8 +192,6 @@ int main() {
|
|||
tst4();
|
||||
tst5();
|
||||
tst6();
|
||||
tst7();
|
||||
tst8();
|
||||
run_thread_finalizers();
|
||||
finalize_util_module();
|
||||
run_post_thread_finalizers();
|
||||
|
|
|
|||
|
|
@ -1,8 +1,6 @@
|
|||
add_library(util OBJECT debug.cpp name.cpp name_set.cpp
|
||||
name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp
|
||||
bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp
|
||||
realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
|
||||
lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp
|
||||
serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp
|
||||
realpath.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp bitap_fuzzy_search.cpp
|
||||
init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp
|
||||
null_ostream.cpp file_lock.cpp)
|
||||
|
|
|
|||
|
|
@ -53,56 +53,4 @@ char const * memory_exception::what() const noexcept {
|
|||
buffer = s.str();
|
||||
return buffer.c_str();
|
||||
}
|
||||
|
||||
constexpr char const * exception_mt = "exception_mt";
|
||||
throwable const & to_exception(lua_State * L, int i) {
|
||||
return *(*static_cast<throwable**>(luaL_checkudata(L, i, exception_mt)));
|
||||
}
|
||||
|
||||
int push_exception(lua_State * L, throwable const & e) {
|
||||
throwable ** mem = static_cast<throwable**>(lua_newuserdata(L, sizeof(throwable*))); // NOLINT
|
||||
*mem = e.clone();
|
||||
luaL_getmetatable(L, exception_mt);
|
||||
lua_setmetatable(L, -2);
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int exception_gc(lua_State * L) {
|
||||
throwable ** mem = static_cast<throwable**>(lua_touserdata(L, 1));
|
||||
delete (*mem);
|
||||
return 0;
|
||||
}
|
||||
|
||||
bool is_exception(lua_State * L, int i) {
|
||||
return testudata(L, i, exception_mt);
|
||||
}
|
||||
|
||||
static int exception_what(lua_State * L) {
|
||||
return push_string(L, to_exception(L, 1).what());
|
||||
}
|
||||
|
||||
static int exception_rethrow(lua_State * L) {
|
||||
lua_pushvalue(L, 1);
|
||||
return lua_error(L);
|
||||
}
|
||||
|
||||
static int exception_pred(lua_State * L) {
|
||||
return push_boolean(L, is_exception(L, 1));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg exception_m[] = {
|
||||
{"__gc", exception_gc}, // never throws
|
||||
{"what", safe_function<exception_what>},
|
||||
{"rethrow", exception_rethrow}, // generates a lua_error
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_exception(lua_State * L) {
|
||||
luaL_newmetatable(L, exception_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, exception_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(exception_pred, "is_exception");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include <exception>
|
||||
#include <string>
|
||||
#include <memory>
|
||||
|
|
@ -87,9 +86,4 @@ public:
|
|||
virtual throwable * clone() const { return new memory_exception(m_component_name.c_str()); }
|
||||
virtual void rethrow() const { throw *this; }
|
||||
};
|
||||
|
||||
int push_exception(lua_State * L, throwable const & e);
|
||||
throwable const & to_exception(lua_State * L, int i);
|
||||
bool is_exception(lua_State * L, int i);
|
||||
void open_exception(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,8 +7,6 @@ Author: Leonardo de Moura
|
|||
#include "util/ascii.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/serializer.h"
|
||||
#include "util/thread_script_state.h"
|
||||
#include "util/script_state.h"
|
||||
#include "util/name.h"
|
||||
#include "util/name_generator.h"
|
||||
#include "util/lean_path.h"
|
||||
|
|
@ -21,8 +19,6 @@ void initialize_util_module() {
|
|||
initialize_serializer();
|
||||
initialize_thread();
|
||||
initialize_ascii();
|
||||
initialize_thread_script_state();
|
||||
initialize_script_state();
|
||||
initialize_name();
|
||||
initialize_name_generator();
|
||||
initialize_lean_path();
|
||||
|
|
@ -31,8 +27,6 @@ void finalize_util_module() {
|
|||
finalize_lean_path();
|
||||
finalize_name_generator();
|
||||
finalize_name();
|
||||
finalize_script_state();
|
||||
finalize_thread_script_state();
|
||||
finalize_ascii();
|
||||
finalize_thread();
|
||||
finalize_serializer();
|
||||
|
|
|
|||
|
|
@ -196,12 +196,8 @@ bool is_olean_file(std::string const & fname) {
|
|||
return has_file_ext(fname, ".olean");
|
||||
}
|
||||
|
||||
bool is_lua_file(std::string const & fname) {
|
||||
return has_file_ext(fname, ".lua");
|
||||
}
|
||||
|
||||
bool is_known_file_ext(std::string const & fname) {
|
||||
return is_lean_file(fname) || is_hlean_file(fname) || is_olean_file(fname) || is_lua_file(fname);
|
||||
return is_lean_file(fname) || is_hlean_file(fname) || is_olean_file(fname);
|
||||
}
|
||||
|
||||
optional<std::string> check_file_core(std::string file, char const * ext) {
|
||||
|
|
@ -271,7 +267,7 @@ std::string find_file(std::string const & base, optional<unsigned> const & k, na
|
|||
}
|
||||
|
||||
std::string find_file(std::string fname) {
|
||||
return find_file(fname, {".olean", ".lean", ".lua"});
|
||||
return find_file(fname, {".olean", ".lean"});
|
||||
}
|
||||
|
||||
std::string find_file(name const & fname) {
|
||||
|
|
|
|||
|
|
@ -40,8 +40,6 @@ std::string find_file(std::string const & base, optional<unsigned> const & k, na
|
|||
bool is_lean_file(std::string const & fname);
|
||||
/** \brief Return true iff fname ends with ".olean" */
|
||||
bool is_olean_file(std::string const & fname);
|
||||
/** \brief Return true iff fname ends with ".lua" */
|
||||
bool is_lua_file(std::string const & fname);
|
||||
|
||||
/** \brief Return a string that replaces hierachical name separator '::' with a path separator. */
|
||||
std::string name_to_file(name const & fname);
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#include <limits>
|
||||
#include <string>
|
||||
#include <algorithm>
|
||||
#include "util/lp/lp_core_solver_base.h"
|
||||
|
|
|
|||
|
|
@ -4,8 +4,8 @@
|
|||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
|
||||
#pragma once
|
||||
#include <limits>
|
||||
#include <string>
|
||||
#include <algorithm>
|
||||
#include <vector>
|
||||
|
|
@ -43,7 +43,7 @@ class core_solver_pretty_printer {
|
|||
|
||||
unsigned ncols() { return m_core_solver.m_A.column_count(); }
|
||||
unsigned nrows() { return m_core_solver.m_A.row_count(); }
|
||||
unsigned m_artificial_start = UINT_MAX;
|
||||
unsigned m_artificial_start = std::numeric_limits<unsigned>::max();
|
||||
T * m_w_buff;
|
||||
T * m_ed_buff;
|
||||
vector<T> m_exact_column_norms;
|
||||
|
|
|
|||
|
|
@ -7,21 +7,21 @@
|
|||
|
||||
#pragma once
|
||||
#include <list>
|
||||
#include "util/numerics/double.h"
|
||||
#include "util/lp/lu.h"
|
||||
#include "util/lp/lp_solver.h"
|
||||
#include <sstream>
|
||||
|
||||
#include <limits>
|
||||
#include <unordered_map>
|
||||
#include "util/lp/static_matrix.h"
|
||||
#include "util/lp/core_solver_pretty_printer.h"
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
#include <vector>
|
||||
#include <set>
|
||||
#include <math.h>
|
||||
#include <cstdlib>
|
||||
#include <algorithm>
|
||||
#include "util/numerics/double.h"
|
||||
#include "util/lp/lu.h"
|
||||
#include "util/lp/lp_solver.h"
|
||||
#include "util/lp/static_matrix.h"
|
||||
#include "util/lp/core_solver_pretty_printer.h"
|
||||
#include "util/lp/lp_core_solver_base.h"
|
||||
#include <math.h>
|
||||
#include "util/lp/breakpoint.h"
|
||||
#include "util/lp/binary_heap_priority_queue.h"
|
||||
namespace lean {
|
||||
|
|
@ -55,7 +55,7 @@ public:
|
|||
int find_leaving_and_t_precisely(unsigned entering, X & t);
|
||||
|
||||
static X positive_infinity() {
|
||||
return convert_struct<X, double>::convert(UINT_MAX);
|
||||
return convert_struct<X, double>::convert(std::numeric_limits<unsigned>::max());
|
||||
}
|
||||
|
||||
X get_harris_theta();
|
||||
|
|
|
|||
208
src/util/lua.cpp
208
src/util/lua.cpp
|
|
@ -1,208 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
#include <sstream>
|
||||
#include <vector>
|
||||
#include <memory>
|
||||
#include <cstring>
|
||||
#include <limits>
|
||||
#include "util/lua.h"
|
||||
#include "util/script_exception.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/sstream.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief luaL_setfuncs replacement. The function luaL_setfuncs is only available in Lua 5.2.
|
||||
*/
|
||||
void setfuncs(lua_State * L, luaL_Reg const * l, int nup) {
|
||||
luaL_checkstack(L, nup, "too many upvalues");
|
||||
for (; l->name != NULL; l++) {
|
||||
// fill the table with given functions
|
||||
for (int i = 0; i < nup; i++) // copy upvalues to the top
|
||||
lua_pushvalue(L, -nup);
|
||||
lua_pushcclosure(L, l->func, nup); // closure with those upvalues
|
||||
lua_setfield(L, -(nup + 2), l->name);
|
||||
}
|
||||
lua_pop(L, nup); // remove upvalues
|
||||
}
|
||||
|
||||
/**
|
||||
\brief luaL_testudata replacement.
|
||||
*/
|
||||
bool testudata(lua_State * L, int ud, char const * tname) {
|
||||
void * p = lua_touserdata(L, ud);
|
||||
if (p != nullptr) {
|
||||
if (lua_getmetatable(L, ud)) {
|
||||
luaL_getmetatable(L, tname);
|
||||
if (!lua_rawequal(L, -1, -2))
|
||||
p = nullptr;
|
||||
lua_pop(L, 2);
|
||||
return p != nullptr;
|
||||
}
|
||||
}
|
||||
return false; // value is not a userdata with a metatable
|
||||
}
|
||||
|
||||
int load(lua_State * L, lua_Reader reader, void * data, char const * source) {
|
||||
#if LUA_VERSION_NUM < 502
|
||||
return lua_load(L, reader, data, source);
|
||||
#else
|
||||
return lua_load(L, reader, data, source, nullptr);
|
||||
#endif
|
||||
}
|
||||
|
||||
size_t objlen(lua_State * L, int idx) {
|
||||
#if LUA_VERSION_NUM < 502
|
||||
return lua_objlen(L, idx);
|
||||
#else
|
||||
return lua_rawlen(L, idx);
|
||||
#endif
|
||||
}
|
||||
|
||||
int lessthan(lua_State * L, int idx1, int idx2) {
|
||||
#if LUA_VERSION_NUM < 502
|
||||
return lua_lessthan(L, idx1, idx2);
|
||||
#else
|
||||
return lua_compare(L, idx1, idx2, LUA_OPLT);
|
||||
#endif
|
||||
}
|
||||
|
||||
int equal(lua_State * L, int idx1, int idx2) {
|
||||
#if LUA_VERSION_NUM < 502
|
||||
return lua_equal(L, idx1, idx2);
|
||||
#else
|
||||
return lua_compare(L, idx1, idx2, LUA_OPEQ);
|
||||
#endif
|
||||
}
|
||||
|
||||
char const * tostring(lua_State * L, int idx) {
|
||||
if (!luaL_callmeta(L, idx, "__tostring")) { /* no metafield? */
|
||||
switch (lua_type(L, idx)) {
|
||||
case LUA_TNUMBER:
|
||||
case LUA_TSTRING:
|
||||
lua_pushvalue(L, idx);
|
||||
break;
|
||||
case LUA_TBOOLEAN:
|
||||
lua_pushstring(L, (lua_toboolean(L, idx) ? "true" : "false"));
|
||||
break;
|
||||
case LUA_TNIL:
|
||||
lua_pushliteral(L, "nil");
|
||||
break;
|
||||
default: {
|
||||
std::ostringstream strm;
|
||||
strm << lua_typename(L, idx) << ": " << lua_topointer(L, idx);
|
||||
lua_pushstring(L, strm.str().c_str());
|
||||
break;
|
||||
}}
|
||||
}
|
||||
return lua_tostring(L, -1);
|
||||
}
|
||||
|
||||
int get_nonnil_top(lua_State * L) {
|
||||
int top = lua_gettop(L);
|
||||
while (top > 0 && lua_isnil(L, top))
|
||||
top--;
|
||||
return top;
|
||||
}
|
||||
|
||||
static void exec(lua_State * L) {
|
||||
pcall(L, 0, LUA_MULTRET, 0);
|
||||
}
|
||||
|
||||
void check_result(lua_State * L, int result) {
|
||||
if (result) {
|
||||
if (is_exception(L, -1)) {
|
||||
to_exception(L, -1).rethrow();
|
||||
} else {
|
||||
throw script_exception(lua_tostring(L, -1));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void dofile(lua_State * L, char const * fname) {
|
||||
int result = luaL_loadfile(L, fname);
|
||||
check_result(L, result);
|
||||
exec(L);
|
||||
}
|
||||
|
||||
void dostring(lua_State * L, char const * str) {
|
||||
int result = luaL_loadstring(L, str);
|
||||
check_result(L, result);
|
||||
exec(L);
|
||||
}
|
||||
|
||||
void pcall(lua_State * L, int nargs, int nresults, int errorfun) {
|
||||
int result = lua_pcall(L, nargs, nresults, errorfun);
|
||||
check_result(L, result);
|
||||
}
|
||||
|
||||
bool resume(lua_State * L, int nargs) {
|
||||
#if LUA_VERSION_NUM < 502
|
||||
int result = lua_resume(L, nargs);
|
||||
#else
|
||||
int result = lua_resume(L, nullptr, nargs);
|
||||
#endif
|
||||
if (result == LUA_YIELD)
|
||||
return false;
|
||||
if (result == 0)
|
||||
return true;
|
||||
check_result(L, result);
|
||||
lean_unreachable();
|
||||
return true;
|
||||
}
|
||||
|
||||
void throw_bad_arg_error(lua_State * L, int i, char const * expected_type) {
|
||||
lua_Debug ar;
|
||||
if (!lua_getstack(L, 0, &ar)) /* no stack frame? */
|
||||
throw exception(sstream() << "bad argument #" << i << " (" << expected_type << " expected)");
|
||||
lua_getinfo(L, "n", &ar);
|
||||
if (strcmp(ar.namewhat, "method") == 0 || ar.name == nullptr)
|
||||
throw exception(sstream() << "bad argument #" << i << " (" << expected_type << " expected)");
|
||||
throw exception(sstream() << "bad argument #" << i << " to '" << ar.name << "' (" << expected_type << " expected)");
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Wrapper for "customers" that are only using a subset
|
||||
of Lean libraries.
|
||||
*/
|
||||
int safe_function_wrapper(lua_State * L, lua_CFunction f) {
|
||||
try {
|
||||
return f(L);
|
||||
} catch (throwable & e) {
|
||||
lua_Debug ar;
|
||||
lua_getstack(L, 1, &ar);
|
||||
lua_getinfo(L, "Sl", &ar);
|
||||
if (ar.source && *(ar.source) == '@')
|
||||
push_exception(L, script_nested_exception(true, ar.source+1, ar.currentline,
|
||||
std::shared_ptr<throwable>(e.clone())));
|
||||
else if (ar.source)
|
||||
push_exception(L, script_nested_exception(false, ar.source, ar.currentline,
|
||||
std::shared_ptr<throwable>(e.clone())));
|
||||
else
|
||||
push_exception(L, e);
|
||||
} catch (std::bad_alloc &) {
|
||||
lua_pushstring(L, "out of memory");
|
||||
} catch (std::exception & e) {
|
||||
lua_pushstring(L, e.what());
|
||||
} catch(...) {
|
||||
lua_pushstring(L, "unknown error");
|
||||
}
|
||||
return lua_error(L);
|
||||
}
|
||||
|
||||
void check_num_args(lua_State * L, int num) {
|
||||
if (lua_gettop(L) != num) throw exception("incorrect number of arguments to function");
|
||||
}
|
||||
void check_atmost_num_args(lua_State * L, int high) {
|
||||
if (lua_gettop(L) > high) throw exception("too many arguments to function");
|
||||
}
|
||||
void check_atleast_num_args(lua_State * L, int low) {
|
||||
if (lua_gettop(L) < low) throw exception("too few arguments to function");
|
||||
}
|
||||
}
|
||||
136
src/util/lua.h
136
src/util/lua.h
|
|
@ -1,136 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <lua.hpp>
|
||||
|
||||
namespace lean {
|
||||
// =======================================
|
||||
// Lua 5.1 and 5.2 compatibility
|
||||
//
|
||||
// The following helper functions make sure
|
||||
// we can compile using Lua 5.1 or 5.2
|
||||
void setfuncs(lua_State * L, luaL_Reg const * l, int nup);
|
||||
bool testudata(lua_State * L, int idx, char const * mt);
|
||||
int load(lua_State * L, lua_Reader reader, void * data, char const * source);
|
||||
size_t objlen(lua_State * L, int idx);
|
||||
void dofile(lua_State * L, char const * fname);
|
||||
void dostring(lua_State * L, char const * str);
|
||||
void pcall(lua_State * L, int nargs, int nresults, int errorfun);
|
||||
char const * tostring (lua_State * L, int idx);
|
||||
/**
|
||||
\brief Return true iff coroutine is done, false if it has yielded,
|
||||
and throws an exception if error.
|
||||
*/
|
||||
bool resume(lua_State * L, int nargs);
|
||||
int lessthan(lua_State * L, int idx1, int idx2);
|
||||
int equal(lua_State * L, int idx1, int idx2);
|
||||
int get_nonnil_top(lua_State * L);
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Goodies/Macros for automating Lua binding
|
||||
// generation.
|
||||
/**
|
||||
\brief Wrapper for invoking function f, and catching Lean exceptions.
|
||||
*/
|
||||
int safe_function_wrapper(lua_State * L, lua_CFunction f);
|
||||
template<lua_CFunction F> int safe_function(lua_State * L) {
|
||||
return safe_function_wrapper(L, F);
|
||||
}
|
||||
template<lua_CFunction F> void set_global_function(lua_State * L, char const * name) {
|
||||
lua_pushcfunction(L, safe_function<F>);
|
||||
lua_setglobal(L, name);
|
||||
}
|
||||
#define SET_GLOBAL_FUN(F, N) set_global_function<F>(L, N)
|
||||
#define SET_FUN(F, N) lua_pushstring(L, N); lua_pushcfunction(L, safe_function<F>); lua_settable(L, -3)
|
||||
|
||||
// Auxiliary macro for creating a Lua table that stores enumeration values
|
||||
#define SET_ENUM(N, V) lua_pushstring(L, N); lua_pushinteger(L, static_cast<int>(V)); lua_settable(L, -3)
|
||||
|
||||
#define DECL_PUSH_CORE(NAME, T, TREF) \
|
||||
int push_ ## NAME(lua_State * L, TREF val) { \
|
||||
void * mem = lua_newuserdata(L, sizeof(T)); \
|
||||
new (mem) T(val); \
|
||||
luaL_getmetatable(L, NAME ## _mt); \
|
||||
lua_setmetatable(L, -2); \
|
||||
return 1; \
|
||||
}
|
||||
|
||||
#define DECL_PUSH(T) \
|
||||
DECL_PUSH_CORE(T, T, T const &) \
|
||||
DECL_PUSH_CORE(T, T, T &&)
|
||||
|
||||
#define DECL_GC(T) static int T ## _gc(lua_State * L) { static_cast<T*>(lua_touserdata(L, 1))->~T(); return 0; }
|
||||
|
||||
#define DECL_PRED(T) \
|
||||
bool is_ ## T(lua_State * L, int idx) { return testudata(L, idx, T ## _mt); } \
|
||||
static int T ## _pred(lua_State * L) { check_num_args(L, 1); return push_boolean(L, is_ ## T(L, 1)); }
|
||||
|
||||
void throw_bad_arg_error(lua_State * L, int i, char const * expected_type);
|
||||
|
||||
/**
|
||||
\brief Create basic declarations for adding a new kind of userdata in Lua
|
||||
T is a Lean object type.
|
||||
For example, if T == expr, it produces an implementation for the
|
||||
following declarations
|
||||
|
||||
constexpr char const * expr_mt = "expr";
|
||||
expr & to_expr(lua_State * L, int i);
|
||||
bool is_expr(lua_State * L, int i);
|
||||
static int expr_pred(lua_State * L);
|
||||
static int expr_gc(lua_State * L);
|
||||
int push_expr(lua_State * L, expr const & e);
|
||||
int push_expr(lua_State * L, expr && e);
|
||||
*/
|
||||
#define DECL_UDATA(T) \
|
||||
constexpr char const * T ## _mt = #T; \
|
||||
DECL_PRED(T) \
|
||||
T & to_ ## T(lua_State * L, int i) { if (!is_ ## T(L, i)) throw_bad_arg_error(L, i, T ## _mt); return *static_cast<T*>(luaL_checkudata(L, i, T ## _mt)); } \
|
||||
DECL_GC(T) \
|
||||
DECL_PUSH(T)
|
||||
|
||||
/**
|
||||
\brief Similar to DECL_UDATA, but it only declares the functions.
|
||||
|
||||
For example, if T == expr, it produces the following declarations:
|
||||
|
||||
class expr;
|
||||
expr & to_expr(lua_State * L, int i);
|
||||
bool is_expr(lua_State * L, int i);
|
||||
int push_expr(lua_State * L, expr const & e);
|
||||
int push_expr(lua_State * L, expr && e);
|
||||
*/
|
||||
#define UDATA_DEFS_CORE(T) \
|
||||
T & to_ ## T(lua_State * L, int i); \
|
||||
bool is_ ## T(lua_State * L, int i); \
|
||||
int push_ ## T(lua_State * L, T const & e); \
|
||||
int push_ ## T(lua_State * L, T && e);
|
||||
#define UDATA_DEFS(T) \
|
||||
class T; \
|
||||
UDATA_DEFS_CORE(T)
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Useful macros
|
||||
inline int push_boolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }
|
||||
inline int push_string(lua_State * L, char const * s) { lua_pushstring(L, s); return 1; }
|
||||
inline int push_integer(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); return 1; }
|
||||
inline int push_number(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
|
||||
inline int push_nil(lua_State * L) { lua_pushnil(L); return 1; }
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Extra validation functions
|
||||
|
||||
/** \brief Throw an exception if lua_gettop(L) != num */
|
||||
void check_num_args(lua_State * L, int num);
|
||||
/** \brief Throw an exception if lua_gettop(L) > high */
|
||||
void check_atmost_num_args(lua_State * L, int high);
|
||||
/** \brief Throw an exception if lua_gettop(L) < low */
|
||||
void check_atleast_num_args(lua_State * L, int low);
|
||||
// =======================================
|
||||
}
|
||||
|
|
@ -1,80 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/list.h"
|
||||
#include "util/sstream.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Convert a Lua table into a list<T> */
|
||||
template<typename T, typename Proc>
|
||||
list<T> table_to_list(lua_State * L, int idx, Proc const & to_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
int n = objlen(L, idx);
|
||||
list<T> r;
|
||||
for (int i = n; i >= 1; i--) {
|
||||
lua_rawgeti(L, idx, i);
|
||||
r = cons(to_value(L, -1), r);
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
return r;
|
||||
} else {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a lua table");
|
||||
}
|
||||
}
|
||||
|
||||
#define DEFINE_LUA_LIST(T, PushVal, ToVal) \
|
||||
typedef list<T> list_ ## T; \
|
||||
DECL_UDATA(list_ ## T) \
|
||||
static int list_ ## T ## _cons(lua_State * L) { return push_list_ ## T(L, list<T>(ToVal(L, 1), to_list_ ## T(L, 2))); } \
|
||||
static int list_ ## T ## _nil(lua_State * L) { return push_list_ ## T(L, list<T>()); } \
|
||||
static int list_ ## T ## _mk(lua_State * L) { \
|
||||
int nargs = lua_gettop(L); \
|
||||
return (nargs == 0) ? list_ ## T ## _nil(L) : list_ ## T ## _cons(L); \
|
||||
} \
|
||||
static int list_ ## T ## _is_nil(lua_State * L) { return push_boolean(L, is_nil(to_list_ ## T(L, 1))); } \
|
||||
static int list_ ## T ## _car(lua_State * L) { \
|
||||
list<T> & l = to_list_ ## T(L, 1); \
|
||||
if (is_nil(l)) throw exception("arg #1 must be a cons cell"); \
|
||||
return PushVal(L, car(l)); \
|
||||
} \
|
||||
static int list_ ## T ## _cdr(lua_State * L) { \
|
||||
list<T> & l = to_list_ ## T(L, 1); \
|
||||
if (is_nil(l)) throw exception("arg #1 must be a cons cell"); \
|
||||
return push_list_ ## T(L, cdr(l)); \
|
||||
} \
|
||||
static int list_ ## T ## _eq(lua_State * L) { return push_boolean(L, to_list_ ## T(L, 1) == to_list_ ## T(L, 2)); } \
|
||||
static int list_ ## T ## _is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_list_ ## T(L, 1), to_list_ ## T(L, 2))); } \
|
||||
static int list_ ## T ## _len(lua_State * L) { return push_integer(L, length(to_list_ ## T(L, 1))); } \
|
||||
static const struct luaL_Reg list_ ## T ## _m[] = { \
|
||||
{"__gc", list_ ## T ## _gc}, \
|
||||
{"__eq", safe_function<list_ ## T ## _eq>}, \
|
||||
{"__len", safe_function<list_ ## T ## _len>}, \
|
||||
{"is_nil", safe_function<list_ ## T ## _is_nil>}, \
|
||||
{"empty", safe_function<list_ ## T ## _is_nil>}, \
|
||||
{"car", safe_function<list_ ## T ## _car>}, \
|
||||
{"cdr", safe_function<list_ ## T ## _cdr>}, \
|
||||
{"head", safe_function<list_ ## T ## _car>}, \
|
||||
{"tail", safe_function<list_ ## T ## _cdr>}, \
|
||||
{"is_eqp", safe_function<list_ ## T ## _is_eqp>}, \
|
||||
{0, 0} \
|
||||
}; \
|
||||
list<T> to_list_ ## T ## _ext(lua_State * L, int idx) { \
|
||||
if (is_list_ ## T(L, idx)) \
|
||||
return to_list_ ## T(L, idx); \
|
||||
else \
|
||||
return table_to_list<T>(L, idx, ToVal); \
|
||||
} \
|
||||
static void open_list_ ## T(lua_State * L) { \
|
||||
luaL_newmetatable(L, list_ ## T ## _mt); \
|
||||
lua_pushvalue(L, -1); \
|
||||
lua_setfield(L, -2, "__index"); \
|
||||
setfuncs(L, list_ ## T ## _m, 0); \
|
||||
\
|
||||
set_global_function<list_ ## T ## _mk>(L, "list_" #T); \
|
||||
set_global_function<list_ ## T ## _pred>(L, "is_list_" #T); \
|
||||
}
|
||||
}
|
||||
|
|
@ -1,151 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <limits>
|
||||
#include "util/lua_named_param.h"
|
||||
#include "util/sstream.h"
|
||||
#include "util/int64.h"
|
||||
|
||||
namespace lean {
|
||||
bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
bool result = def_value;
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (lua_isboolean(L, -1)) {
|
||||
result = lua_toboolean(L, -1);
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a Boolean in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
|
||||
int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
int result = def_value;
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (lua_isnumber(L, -1)) {
|
||||
result = lua_tointeger(L, -1);
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
|
||||
unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (lua_isnumber(L, -1)) {
|
||||
int64 result = lua_tointeger(L, -1);
|
||||
lua_pop(L, 1);
|
||||
if (result < 0 || result > static_cast<int64>(std::numeric_limits<unsigned>::max()))
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
|
||||
return static_cast<unsigned>(result);
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return def_value;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
|
||||
optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name, optional<unsigned> const & def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (lua_isnumber(L, -1)) {
|
||||
int64 result = lua_tointeger(L, -1);
|
||||
lua_pop(L, 1);
|
||||
if (result < 0 || result > static_cast<int64>(std::numeric_limits<unsigned>::max()))
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
|
||||
return optional<unsigned>(static_cast<unsigned>(result));
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return def_value;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
|
||||
name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (is_name_set(L, -1)) {
|
||||
name_set result = to_name_set(L, -1);
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return def_value;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a name_set in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
|
||||
list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value) {
|
||||
if (lua_istable(L, idx)) {
|
||||
push_string(L, opt_name);
|
||||
lua_gettable(L, idx);
|
||||
if (is_list_name(L, -1) || lua_istable(L, -1)) {
|
||||
list<name> result = to_list_name_ext(L, -1);
|
||||
lua_pop(L, 1);
|
||||
return result;
|
||||
} else if (lua_isnil(L, -1)) {
|
||||
lua_pop(L, 1);
|
||||
return def_value;
|
||||
} else {
|
||||
lua_pop(L, 1);
|
||||
throw exception(sstream() << "field '" << opt_name << "' must be a list of names in table at arg #" << idx);
|
||||
}
|
||||
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table");
|
||||
} else {
|
||||
return def_value;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/name_set.h"
|
||||
|
||||
namespace lean {
|
||||
// =======================================
|
||||
// Utilities for simulating Python-like named parameters using Lua tables.
|
||||
// In the following function \c idx is the position of the Lua table on the Lua stack.
|
||||
bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value);
|
||||
int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value);
|
||||
unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value);
|
||||
optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name,
|
||||
optional<unsigned> const & def_value = optional<unsigned>());
|
||||
name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value = name_set());
|
||||
list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value);
|
||||
}
|
||||
|
|
@ -1,59 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/sstream.h"
|
||||
|
||||
namespace lean {
|
||||
#define DEFINE_LUA_PAIR_CORE(T1, PushVal1, ToVal1, T2, PushVal2, ToVal2, MK_Name, IS_Name) \
|
||||
typedef pair<T1, T2> pair_ ## T1 ## _ ## T2; \
|
||||
DECL_UDATA(pair_ ## T1 ## _ ## T2) \
|
||||
pair<T1, T2> to_pair_ ## T1 ## _ ## T2 ## _ext(lua_State * L, int idx) { \
|
||||
if (is_pair_ ## T1 ## _ ## T2(L, idx)) { \
|
||||
return to_pair_ ## T1 ## _ ## T2(L, idx); \
|
||||
} else if (lua_istable(L, idx)) { \
|
||||
lua_pushvalue(L, idx); \
|
||||
int n = objlen(L, -1); \
|
||||
if (n != 2) \
|
||||
throw exception(sstream() << "arg #" << idx << " must be a table of size 2"); \
|
||||
lua_rawgeti(L, -1, 1); \
|
||||
lua_rawgeti(L, -2, 2); \
|
||||
pair<T1, T2> r(ToVal1(L, -2), ToVal2(L, -1)); \
|
||||
lua_pop(L, 3); \
|
||||
return r; \
|
||||
} else { \
|
||||
throw exception(sstream() << "arg #" << idx << " must be a pair or a Lua table"); \
|
||||
} \
|
||||
} \
|
||||
static int pair_ ## T1 ## _ ## T2 ## _mk(lua_State * L) { return push_pair_ ## T1 ## _ ## T2(L, pair<T1, T2>(ToVal1(L, 1), ToVal2(L, 2))); } \
|
||||
static int pair_ ## T1 ## _ ## T2 ## _first(lua_State * L) { return PushVal1(L, to_pair_ ## T1 ## _ ## T2(L, 1).first); } \
|
||||
static int pair_ ## T1 ## _ ## T2 ## _second(lua_State * L) { return PushVal2(L, to_pair_ ## T1 ## _ ## T2(L, 1).second); } \
|
||||
static const struct luaL_Reg pair_ ## T1 ## _ ## T2 ## _m[] = { \
|
||||
{"__gc", pair_ ## T1 ## _ ## T2 ## _gc}, \
|
||||
{"first", safe_function<pair_ ## T1 ## _ ## T2 ## _first>}, \
|
||||
{"second", safe_function<pair_ ## T1 ## _ ## T2 ## _second>}, \
|
||||
{0, 0} \
|
||||
}; \
|
||||
static void open_pair_ ## T1 ## _ ## T2 (lua_State * L) { \
|
||||
luaL_newmetatable(L, pair_ ## T1 ## _ ## T2 ## _mt); \
|
||||
lua_pushvalue(L, -1); \
|
||||
lua_setfield(L, -2, "__index"); \
|
||||
setfuncs(L, pair_ ## T1 ## _ ## T2 ## _m, 0); \
|
||||
\
|
||||
set_global_function<pair_ ## T1 ## _ ## T2 ## _mk>(L, MK_Name); \
|
||||
set_global_function<pair_ ## T1 ## _ ## T2 ## _pred>(L, IS_Name); \
|
||||
}
|
||||
|
||||
#define DEFINE_LUA_PAIR(T1, PushVal1, ToVal1, T2, PushVal2, ToVal2) DEFINE_LUA_PAIR_CORE(T1, PushVal1, ToVal1, T2, PushVal2, ToVal2, "pair_" #T1 "_" #T2, "is_pair_" #T1 "_" #T2)
|
||||
|
||||
// A Pair (T, T)
|
||||
#define DEFINE_LUA_HOMO_PAIR(T, PushVal, ToVal) DEFINE_LUA_PAIR_CORE(T, PushVal, ToVal, T, PushVal, ToVal, "pair_" #T, "is_pair_" #T) \
|
||||
static void open_pair_ ## T(lua_State * L) { open_pair_ ## T ## _ ## T(L); } \
|
||||
pair<T, T> & to_pair_ ## T(lua_State * L, int idx) { return to_pair_ ## T ## _ ## T(L, idx); } \
|
||||
pair<T, T> to_pair_ ## T ## _ext(lua_State * L, int idx) { return to_pair_ ## T ## _ ## T ## _ext(L, idx); } \
|
||||
int push_pair_ ## T(lua_State * L, pair<T, T> const & p) { return push_pair_ ## T ## _ ## T(L, p); }
|
||||
}
|
||||
|
|
@ -1,80 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/luaref.h"
|
||||
#include "util/debug.h"
|
||||
|
||||
namespace lean {
|
||||
luaref::luaref(lua_State * L, int i) {
|
||||
lean_assert(L);
|
||||
m_state = L;
|
||||
lua_pushvalue(m_state, i);
|
||||
m_ref = luaL_ref(m_state, LUA_REGISTRYINDEX);
|
||||
}
|
||||
|
||||
luaref::luaref(luaref const & r) {
|
||||
m_state = r.m_state;
|
||||
if (m_state) {
|
||||
r.push();
|
||||
m_ref = luaL_ref(m_state, LUA_REGISTRYINDEX);
|
||||
}
|
||||
}
|
||||
|
||||
luaref::luaref(luaref && r) {
|
||||
m_state = r.m_state;
|
||||
m_ref = r.m_ref;
|
||||
r.m_state = nullptr;
|
||||
}
|
||||
|
||||
luaref::~luaref() {
|
||||
if (m_state)
|
||||
luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
|
||||
}
|
||||
|
||||
void luaref::release() {
|
||||
if (m_state) {
|
||||
luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
|
||||
m_state = nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
luaref & luaref::operator=(luaref const & r) {
|
||||
if (m_state != nullptr && r.m_state != nullptr && m_ref == r.m_ref)
|
||||
return *this;
|
||||
if (m_state)
|
||||
luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
|
||||
m_state = r.m_state;
|
||||
if (m_state) {
|
||||
r.push();
|
||||
m_ref = luaL_ref(m_state, LUA_REGISTRYINDEX);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
void luaref::push() const {
|
||||
lean_assert(m_state);
|
||||
lua_rawgeti(m_state, LUA_REGISTRYINDEX, m_ref);
|
||||
}
|
||||
|
||||
int luaref_lt_proc::operator()(luaref const & r1, luaref const & r2) const {
|
||||
lean_assert(r1.get_state() == r2.get_state());
|
||||
lua_State * L = r1.get_state();
|
||||
r1.push();
|
||||
r2.push();
|
||||
int r;
|
||||
if (lessthan(L, -2, -1)) {
|
||||
r = -1;
|
||||
} else if (lessthan(L, -1, -2)) {
|
||||
r = 1;
|
||||
} else if (equal(L, -2, -1)) {
|
||||
r = 0;
|
||||
} else {
|
||||
throw exception("'<' is not a total order for the elements inserted on the table");
|
||||
}
|
||||
lua_pop(L, 2);
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/lua.h"
|
||||
#pragma once
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Reference to Lua object.
|
||||
*/
|
||||
class luaref {
|
||||
lua_State * m_state;
|
||||
int m_ref;
|
||||
public:
|
||||
luaref():m_state(nullptr), m_ref(0) {}
|
||||
/**
|
||||
\brief Create a reference to the Lua object at position \c i on \c L stack.
|
||||
*/
|
||||
luaref(lua_State * L, int i);
|
||||
luaref(luaref const & r);
|
||||
luaref(luaref && r);
|
||||
~luaref();
|
||||
void release();
|
||||
luaref & operator=(luaref const & r);
|
||||
void push() const;
|
||||
lua_State * get_state() const { return m_state; }
|
||||
};
|
||||
|
||||
/**
|
||||
\brief '<' functor for luaref.
|
||||
*/
|
||||
struct luaref_lt_proc {
|
||||
int operator()(luaref const & r1, luaref const & r2) const;
|
||||
};
|
||||
}
|
||||
|
|
@ -19,7 +19,6 @@ Author: Leonardo de Moura
|
|||
#include "util/ascii.h"
|
||||
#include "util/utf8.h"
|
||||
#include "util/object_serializer.h"
|
||||
#include "util/lua_list.h"
|
||||
|
||||
namespace lean {
|
||||
constexpr char const * anonymous_str = "[anonymous]";
|
||||
|
|
@ -457,133 +456,6 @@ name read_name(deserializer & d) {
|
|||
return d.get_extension<name_deserializer>(g_name_sd->m_deserializer_extid).read();
|
||||
}
|
||||
|
||||
DECL_UDATA(name)
|
||||
|
||||
static int mk_name(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
name r;
|
||||
for (int i = 1; i <= nargs; i++) {
|
||||
switch (lua_type(L, i)) {
|
||||
case LUA_TNIL: break; // skip
|
||||
case LUA_TNUMBER: r = name(r, lua_tointeger(L, i)); break;
|
||||
case LUA_TSTRING: r = name(r, lua_tostring(L, i)); break;
|
||||
case LUA_TUSERDATA: r = r + to_name(L, i); break;
|
||||
default: throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer");
|
||||
}
|
||||
}
|
||||
return push_name(L, r);
|
||||
}
|
||||
|
||||
name to_name_ext(lua_State * L, int idx) {
|
||||
if (lua_isstring(L, idx)) {
|
||||
return luaL_checkstring(L, idx);
|
||||
} else if (lua_isnil(L, idx)) {
|
||||
return name();
|
||||
} else if (lua_istable(L, idx)) {
|
||||
name r;
|
||||
int n = objlen(L, idx);
|
||||
for (int i = 1; i <= n; i++) {
|
||||
lua_rawgeti(L, idx, i);
|
||||
switch (lua_type(L, -1)) {
|
||||
case LUA_TNIL: break; // skip
|
||||
case LUA_TNUMBER: r = name(r, lua_tointeger(L, -1)); break;
|
||||
case LUA_TSTRING: r = name(r, lua_tostring(L, -1)); break;
|
||||
case LUA_TUSERDATA: r = r + to_name(L, -1); break;
|
||||
default: throw exception("invalid array arguments, elements must be a hierarchical name, string, or integer");
|
||||
}
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
return r;
|
||||
} else {
|
||||
return to_name(L, idx);
|
||||
}
|
||||
}
|
||||
|
||||
optional<name> to_optional_name(lua_State * L, int idx) {
|
||||
if (lua_isnil(L, idx))
|
||||
return optional<name>();
|
||||
else
|
||||
return optional<name>(to_name_ext(L, idx));
|
||||
}
|
||||
|
||||
int push_optional_name(lua_State * L, optional<name> const & n) {
|
||||
if (n)
|
||||
return push_name(L, *n);
|
||||
else
|
||||
return push_nil(L);
|
||||
}
|
||||
|
||||
static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); }
|
||||
static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); }
|
||||
static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); }
|
||||
static int name_hash(lua_State * L) { return push_integer(L, to_name(L, 1).hash()); }
|
||||
#define NAME_PRED(P) static int name_ ## P(lua_State * L) { check_num_args(L, 1); return push_boolean(L, to_name(L, 1).P()); }
|
||||
NAME_PRED(is_atomic)
|
||||
NAME_PRED(is_anonymous)
|
||||
NAME_PRED(is_string)
|
||||
NAME_PRED(is_numeral)
|
||||
|
||||
static int name_get_prefix(lua_State * L) {
|
||||
if (to_name(L, 1).is_atomic())
|
||||
throw exception("invalid get_prefix, non-atomic name expected");
|
||||
return push_name(L, to_name(L, 1).get_prefix());
|
||||
}
|
||||
|
||||
static int name_get_numeral(lua_State * L) {
|
||||
if (!to_name(L, 1).is_numeral())
|
||||
throw exception("invalid get_numeral, hierarchical name with numeric head expected");
|
||||
return push_integer(L, to_name(L, 1).get_numeral());
|
||||
}
|
||||
|
||||
static int name_get_string(lua_State * L) {
|
||||
if (!to_name(L, 1).is_string())
|
||||
throw exception("invalid get_string, hierarchical name with string head expected");
|
||||
return push_string(L, to_name(L, 1).get_string());
|
||||
}
|
||||
|
||||
static int name_append_before(lua_State * L) { return push_name(L, to_name(L, 1).append_before(lua_tostring(L, 2))); }
|
||||
static int name_append_after(lua_State * L) {
|
||||
if (lua_isnumber(L, 2))
|
||||
return push_name(L, to_name(L, 1).append_after(lua_tonumber(L, 2)));
|
||||
else
|
||||
return push_name(L, to_name(L, 1).append_after(lua_tostring(L, 2)));
|
||||
}
|
||||
|
||||
static int name_replace_prefix(lua_State * L) { return push_name(L, to_name(L, 1).replace_prefix(to_name_ext(L, 2), to_name_ext(L, 3))); }
|
||||
|
||||
static const struct luaL_Reg name_m[] = {
|
||||
{"__gc", name_gc}, // never throws
|
||||
{"__tostring", safe_function<name_tostring>},
|
||||
{"__eq", safe_function<name_eq>},
|
||||
{"__lt", safe_function<name_lt>},
|
||||
{"is_atomic", safe_function<name_is_atomic>},
|
||||
{"is_anonymous", safe_function<name_is_anonymous>},
|
||||
{"is_numeral", safe_function<name_is_numeral>},
|
||||
{"is_string", safe_function<name_is_string>},
|
||||
{"get_prefix", safe_function<name_get_prefix>},
|
||||
{"get_numeral", safe_function<name_get_numeral>},
|
||||
{"get_string", safe_function<name_get_string>},
|
||||
{"hash", safe_function<name_hash>},
|
||||
{"append_before", safe_function<name_append_before>},
|
||||
{"append_after", safe_function<name_append_after>},
|
||||
{"replace_prefix", safe_function<name_replace_prefix>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
DEFINE_LUA_LIST(name, push_name, to_name_ext)
|
||||
|
||||
void open_name(lua_State * L) {
|
||||
luaL_newmetatable(L, name_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, name_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_name, "name");
|
||||
SET_GLOBAL_FUN(name_pred, "is_name");
|
||||
|
||||
open_list_name(L);
|
||||
}
|
||||
|
||||
void initialize_name() {
|
||||
g_anonymous = new name();
|
||||
g_name_sd = new name_sd();
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ Author: Leonardo de Moura
|
|||
#include <utility>
|
||||
#include "util/rc.h"
|
||||
#include "util/pair.h"
|
||||
#include "util/lua.h"
|
||||
#include "util/serializer.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/list.h"
|
||||
|
|
@ -224,15 +223,6 @@ serializer & operator<<(serializer & s, name const & n);
|
|||
name read_name(deserializer & d);
|
||||
inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }
|
||||
|
||||
UDATA_DEFS(name)
|
||||
name to_name_ext(lua_State * L, int idx);
|
||||
optional<name> to_optional_name(lua_State * L, int idx);
|
||||
int push_optional_name(lua_State * L, optional<name> const & n);
|
||||
bool is_list_name(lua_State * L, int idx);
|
||||
list<name> & to_list_name(lua_State * L, int idx);
|
||||
list<name> to_list_name_ext(lua_State * L, int idx);
|
||||
int push_list_name(lua_State * L, list<name> const & l);
|
||||
void open_name(lua_State * L);
|
||||
void initialize_name();
|
||||
void finalize_name();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -28,34 +28,6 @@ void swap(name_generator & a, name_generator & b) {
|
|||
std::swap(a.m_next_idx, b.m_next_idx);
|
||||
}
|
||||
|
||||
DECL_UDATA(name_generator)
|
||||
static int mk_name_generator(lua_State * L) {
|
||||
if (lua_gettop(L) == 0)
|
||||
return push_name_generator(L, name_generator(*g_tmp_prefix));
|
||||
else
|
||||
return push_name_generator(L, name_generator(to_name_ext(L, 1)));
|
||||
}
|
||||
static int name_generator_next(lua_State * L) { return push_name(L, to_name_generator(L, 1).next()); }
|
||||
static int name_generator_prefix(lua_State * L) { return push_name(L, to_name_generator(L, 1).prefix()); }
|
||||
static int name_generator_mk_child(lua_State * L) { return push_name_generator(L, to_name_generator(L, 1).mk_child()); }
|
||||
static const struct luaL_Reg name_generator_m[] = {
|
||||
{"__gc", name_generator_gc}, // never throws
|
||||
{"next", safe_function<name_generator_next>},
|
||||
{"prefix", safe_function<name_generator_prefix>},
|
||||
{"mk_child", safe_function<name_generator_mk_child>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_name_generator(lua_State * L) {
|
||||
luaL_newmetatable(L, name_generator_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, name_generator_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_name_generator, "name_generator");
|
||||
SET_GLOBAL_FUN(name_generator_pred, "is_name_generator");
|
||||
}
|
||||
|
||||
void initialize_name_generator() {
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -38,8 +38,6 @@ public:
|
|||
};
|
||||
void swap(name_generator & a, name_generator & b);
|
||||
|
||||
UDATA_DEFS(name_generator)
|
||||
void open_name_generator(lua_State * L);
|
||||
void initialize_name_generator();
|
||||
void finalize_name_generator();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,34 +17,4 @@ name mk_unique(name_set const & s, name const & suggestion) {
|
|||
i++;
|
||||
}
|
||||
}
|
||||
|
||||
DECL_UDATA(name_set)
|
||||
static int mk_name_set(lua_State * L) {
|
||||
name_set r;
|
||||
int nargs = lua_gettop(L);
|
||||
for (int i = 1; i <= nargs; i++)
|
||||
r.insert(to_name_ext(L, i));
|
||||
return push_name_set(L, r);
|
||||
}
|
||||
static int name_set_insert(lua_State * L) { return push_name_set(L, insert(to_name_set(L, 1), to_name_ext(L, 2))); }
|
||||
static int name_set_contains(lua_State * L) { return push_boolean(L, to_name_set(L, 1).contains(to_name_ext(L, 2))); }
|
||||
static int name_set_erase(lua_State * L) { return push_name_set(L, erase(to_name_set(L, 1), to_name_ext(L, 2))); }
|
||||
|
||||
static const struct luaL_Reg name_set_m[] = {
|
||||
{"__gc", name_set_gc}, // never throws
|
||||
{"insert", safe_function<name_set_insert>},
|
||||
{"contains", safe_function<name_set_contains>},
|
||||
{"erase", safe_function<name_set_erase>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_name_set(lua_State * L) {
|
||||
luaL_newmetatable(L, name_set_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, name_set_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_name_set, "name_set");
|
||||
SET_GLOBAL_FUN(name_set_pred, "is_name_set");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include "util/rb_tree.h"
|
||||
#include "util/name.h"
|
||||
#include "util/lua.h"
|
||||
namespace lean {
|
||||
typedef rb_tree<name, name_quick_cmp> name_set;
|
||||
/** \brief Make a name that does not occur in \c s, based on the given suggestion. */
|
||||
|
|
@ -20,7 +19,4 @@ name_set to_name_set(C const & ns) {
|
|||
r.insert(n);
|
||||
return r;
|
||||
}
|
||||
|
||||
UDATA_DEFS_CORE(name_set)
|
||||
void open_name_set(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -164,94 +164,6 @@ void finalize_mpq() {
|
|||
mpq read_mpq(deserializer & d) {
|
||||
return mpq(d.read_string().c_str());
|
||||
}
|
||||
|
||||
DECL_UDATA(mpq)
|
||||
|
||||
mpq to_mpq_ext(lua_State * L, int idx) {
|
||||
switch (lua_type(L, idx)) {
|
||||
case LUA_TNUMBER: return mpq(lua_tonumber(L, idx));
|
||||
case LUA_TSTRING: return mpq(lua_tostring(L, idx));
|
||||
case LUA_TUSERDATA:
|
||||
if (is_mpz(L, idx)) {
|
||||
return mpq(to_mpz(L, idx));
|
||||
} else {
|
||||
return *static_cast<mpq*>(luaL_checkudata(L, idx, mpq_mt));
|
||||
}
|
||||
default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq");
|
||||
}
|
||||
}
|
||||
|
||||
static int mpq_tostring(lua_State * L) {
|
||||
mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
|
||||
std::ostringstream out;
|
||||
out << *n;
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int mpq_eq(lua_State * L) {
|
||||
return push_boolean(L, to_mpq_ext(L, 1) == to_mpq_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpq_lt(lua_State * L) {
|
||||
return push_boolean(L, to_mpq_ext(L, 1) < to_mpq_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpq_add(lua_State * L) {
|
||||
return push_mpq(L, to_mpq_ext(L, 1) + to_mpq_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpq_sub(lua_State * L) {
|
||||
return push_mpq(L, to_mpq_ext(L, 1) - to_mpq_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpq_mul(lua_State * L) {
|
||||
return push_mpq(L, to_mpq_ext(L, 1) * to_mpq_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpq_div(lua_State * L) {
|
||||
mpq arg2 = to_mpq_ext(L, 2);
|
||||
if (arg2 == 0) throw exception("division by zero");
|
||||
return push_mpq(L, to_mpq_ext(L, 1) / arg2);
|
||||
}
|
||||
|
||||
static int mpq_umn(lua_State * L) {
|
||||
return push_mpq(L, 0 - to_mpq_ext(L, 1));
|
||||
}
|
||||
|
||||
static int mpq_power(lua_State * L) {
|
||||
int k = luaL_checkinteger(L, 2);
|
||||
if (k < 0) throw exception("argument #2 must be positive");
|
||||
return push_mpq(L, pow(to_mpq_ext(L, 1), k));
|
||||
}
|
||||
|
||||
static int mk_mpq(lua_State * L) {
|
||||
mpq arg = to_mpq_ext(L, 1);
|
||||
return push_mpq(L, arg);
|
||||
}
|
||||
|
||||
static const struct luaL_Reg mpq_m[] = {
|
||||
{"__gc", mpq_gc}, // never throws
|
||||
{"__tostring", safe_function<mpq_tostring>},
|
||||
{"__eq", safe_function<mpq_eq>},
|
||||
{"__lt", safe_function<mpq_lt>},
|
||||
{"__add", safe_function<mpq_add>},
|
||||
{"__sub", safe_function<mpq_sub>},
|
||||
{"__mul", safe_function<mpq_mul>},
|
||||
{"__div", safe_function<mpq_div>},
|
||||
{"__pow", safe_function<mpq_power>},
|
||||
{"__unm", safe_function<mpq_umn>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_mpq(lua_State * L) {
|
||||
luaL_newmetatable(L, mpq_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, mpq_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_mpq, "mpq");
|
||||
SET_GLOBAL_FUN(mpq_pred, "is_mpq");
|
||||
}
|
||||
}
|
||||
|
||||
void print(lean::mpq const & v) { std::cout << v << std::endl; }
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lua.h"
|
||||
#include "util/numerics/mpz.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -286,10 +285,6 @@ serializer & operator<<(serializer & s, mpq const & n);
|
|||
mpq read_mpq(deserializer & d);
|
||||
inline deserializer & operator>>(deserializer & d, mpq & n) { n = read_mpq(d); return d; }
|
||||
|
||||
UDATA_DEFS(mpq)
|
||||
mpq to_mpq_ext(lua_State * L, int idx);
|
||||
void open_mpq(lua_State * L);
|
||||
|
||||
void initialize_mpq();
|
||||
void finalize_mpq();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -102,88 +102,6 @@ serializer & operator<<(serializer & s, mpz const & n) {
|
|||
mpz read_mpz(deserializer & d) {
|
||||
return mpz(d.read_string().c_str());
|
||||
}
|
||||
|
||||
DECL_UDATA(mpz)
|
||||
mpz to_mpz_ext(lua_State * L, int idx) {
|
||||
switch (lua_type(L, idx)) {
|
||||
case LUA_TNUMBER: return mpz(static_cast<long>(lua_tointeger(L, idx)));
|
||||
case LUA_TSTRING: return mpz(lua_tostring(L, idx));
|
||||
case LUA_TUSERDATA: return *static_cast<mpz*>(luaL_checkudata(L, idx, mpz_mt));
|
||||
default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz");
|
||||
}
|
||||
}
|
||||
|
||||
static int mpz_tostring(lua_State * L) {
|
||||
mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
|
||||
std::ostringstream out;
|
||||
out << *n;
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int mpz_eq(lua_State * L) {
|
||||
return push_boolean(L, to_mpz_ext(L, 1) == to_mpz_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpz_lt(lua_State * L) {
|
||||
return push_boolean(L, to_mpz_ext(L, 1) < to_mpz_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpz_add(lua_State * L) {
|
||||
return push_mpz(L, to_mpz_ext(L, 1) + to_mpz_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpz_sub(lua_State * L) {
|
||||
return push_mpz(L, to_mpz_ext(L, 1) - to_mpz_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpz_mul(lua_State * L) {
|
||||
return push_mpz(L, to_mpz_ext(L, 1) * to_mpz_ext(L, 2));
|
||||
}
|
||||
|
||||
static int mpz_div(lua_State * L) {
|
||||
mpz arg2 = to_mpz_ext(L, 2);
|
||||
if (arg2 == 0) throw exception("division by zero");
|
||||
return push_mpz(L, to_mpz_ext(L, 1) / arg2);
|
||||
}
|
||||
|
||||
static int mpz_umn(lua_State * L) {
|
||||
return push_mpz(L, 0 - to_mpz_ext(L, 1));
|
||||
}
|
||||
|
||||
static int mpz_power(lua_State * L) {
|
||||
int k = luaL_checkinteger(L, 2);
|
||||
if (k < 0) throw exception("argument #2 must be positive");
|
||||
return push_mpz(L, pow(to_mpz_ext(L, 1), k));
|
||||
}
|
||||
|
||||
static int mk_mpz(lua_State * L) {
|
||||
mpz arg = to_mpz_ext(L, 1);
|
||||
return push_mpz(L, arg);
|
||||
}
|
||||
|
||||
static const struct luaL_Reg mpz_m[] = {
|
||||
{"__gc", mpz_gc}, // never throws
|
||||
{"__tostring", safe_function<mpz_tostring>},
|
||||
{"__eq", safe_function<mpz_eq>},
|
||||
{"__lt", safe_function<mpz_lt>},
|
||||
{"__add", safe_function<mpz_add>},
|
||||
{"__sub", safe_function<mpz_sub>},
|
||||
{"__mul", safe_function<mpz_mul>},
|
||||
{"__div", safe_function<mpz_div>},
|
||||
{"__pow", safe_function<mpz_power>},
|
||||
{"__unm", safe_function<mpz_umn>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_mpz(lua_State * L) {
|
||||
luaL_newmetatable(L, mpz_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, mpz_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_mpz, "mpz");
|
||||
SET_GLOBAL_FUN(mpz_pred, "is_mpz");
|
||||
}
|
||||
}
|
||||
|
||||
void print(lean::mpz const & n) { std::cout << n << std::endl; }
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include <gmp.h>
|
||||
#include <iostream>
|
||||
#include "util/debug.h"
|
||||
#include "util/lua.h"
|
||||
#include "util/serializer.h"
|
||||
#include "util/numerics/numeric_traits.h"
|
||||
|
||||
|
|
@ -246,10 +245,6 @@ serializer & operator<<(serializer & s, mpz const & n);
|
|||
mpz read_mpz(deserializer & d);
|
||||
inline deserializer & operator>>(deserializer & d, mpz & n) { n = read_mpz(d); return d; }
|
||||
|
||||
UDATA_DEFS(mpz)
|
||||
mpz to_mpz_ext(lua_State * L, int idx);
|
||||
void open_mpz(lua_State * L);
|
||||
|
||||
void initialize_mpz();
|
||||
void finalize_mpz();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,97 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/lua.h"
|
||||
#include "util/luaref.h"
|
||||
#include "util/rb_map.h"
|
||||
|
||||
namespace lean {
|
||||
typedef rb_map<luaref, luaref, luaref_lt_proc> lua_rb_map;
|
||||
DECL_UDATA(lua_rb_map)
|
||||
|
||||
static int mk_lua_rb_map(lua_State * L) {
|
||||
lua_rb_map r;
|
||||
return push_lua_rb_map(L, r);
|
||||
}
|
||||
|
||||
static int lua_rb_map_size(lua_State * L) {
|
||||
return push_integer(L, to_lua_rb_map(L, 1).size());
|
||||
}
|
||||
|
||||
static int lua_rb_map_contains(lua_State * L) {
|
||||
return push_boolean(L, to_lua_rb_map(L, 1).contains(luaref(L, 2)));
|
||||
}
|
||||
|
||||
static int lua_rb_map_empty(lua_State * L) {
|
||||
return push_boolean(L, to_lua_rb_map(L, 1).empty());
|
||||
}
|
||||
|
||||
static int lua_rb_map_insert(lua_State * L) {
|
||||
to_lua_rb_map(L, 1).insert(luaref(L, 2), luaref(L, 3));
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int lua_rb_map_erase(lua_State * L) {
|
||||
to_lua_rb_map(L, 1).erase(luaref(L, 2));
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int lua_rb_map_find(lua_State * L) {
|
||||
lua_rb_map & m = to_lua_rb_map(L, 1);
|
||||
luaref const * val = m.find(luaref(L, 2));
|
||||
if (val) {
|
||||
lean_assert(val->get_state() == L);
|
||||
val->push();
|
||||
} else {
|
||||
lua_pushnil(L);
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int lua_rb_map_copy(lua_State * L) {
|
||||
return push_lua_rb_map(L, to_lua_rb_map(L, 1));
|
||||
}
|
||||
|
||||
static int lua_rb_map_for_each(lua_State * L) {
|
||||
// Remark: we take a copy of the map to make sure
|
||||
// for_each will not crash if the map is updated while being
|
||||
// traversed.
|
||||
// The copy operation is very cheap O(1).
|
||||
lua_rb_map m(to_lua_rb_map(L, 1)); // map
|
||||
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
|
||||
m.for_each([&](luaref const & k, luaref const & v) {
|
||||
lua_pushvalue(L, 2); // push user-fun
|
||||
k.push();
|
||||
v.push();
|
||||
pcall(L, 2, 0, 0);
|
||||
});
|
||||
return 0;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg lua_rb_map_m[] = {
|
||||
{"__gc", lua_rb_map_gc}, // never throws
|
||||
{"__len", safe_function<lua_rb_map_size> },
|
||||
{"contains", safe_function<lua_rb_map_contains>},
|
||||
{"size", safe_function<lua_rb_map_size>},
|
||||
{"empty", safe_function<lua_rb_map_empty>},
|
||||
{"insert", safe_function<lua_rb_map_insert>},
|
||||
{"erase", safe_function<lua_rb_map_erase>},
|
||||
{"find", safe_function<lua_rb_map_find>},
|
||||
{"copy", safe_function<lua_rb_map_copy>},
|
||||
{"for_each", safe_function<lua_rb_map_for_each>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_rb_map(lua_State * L) {
|
||||
luaL_newmetatable(L, lua_rb_map_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, lua_rb_map_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_lua_rb_map, "rb_map");
|
||||
SET_GLOBAL_FUN(lua_rb_map_pred, "is_rb_map");
|
||||
}
|
||||
}
|
||||
|
|
@ -6,7 +6,6 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/lua.h"
|
||||
#include "util/pair.h"
|
||||
#include "util/rb_tree.h"
|
||||
|
||||
|
|
@ -100,5 +99,4 @@ template<typename K, typename T, typename CMP, typename F>
|
|||
void for_each(rb_map<K, T, CMP> const & m, F && f) {
|
||||
return m.for_each(f);
|
||||
}
|
||||
void open_rb_map(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,110 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
#include <cstdlib>
|
||||
#include "util/thread.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/script_exception.h"
|
||||
|
||||
namespace lean {
|
||||
script_exception::script_exception(char const * lua_error) {
|
||||
lean_assert(lua_error);
|
||||
std::string fname;
|
||||
std::string line;
|
||||
std::string msg;
|
||||
int state = 0;
|
||||
char const * it = lua_error;
|
||||
while (*it) {
|
||||
if (state == 0) {
|
||||
if (*it == ':') {
|
||||
state = 1;
|
||||
} else {
|
||||
fname += *it;
|
||||
}
|
||||
} else if (state == 1) {
|
||||
if (*it == ':') {
|
||||
state = 2;
|
||||
} else {
|
||||
line += *it;
|
||||
}
|
||||
} else {
|
||||
msg += *it;
|
||||
}
|
||||
it++;
|
||||
}
|
||||
if (state != 2) {
|
||||
// failed to decode Lua error message
|
||||
m_source = source::Unknown;
|
||||
m_msg = lua_error;
|
||||
} else {
|
||||
if (fname == "[string \"...\"]") {
|
||||
m_source = source::String;
|
||||
} else {
|
||||
m_source = source::File;
|
||||
m_file = fname;
|
||||
}
|
||||
m_line = atoi(line.c_str());
|
||||
m_msg = msg;
|
||||
}
|
||||
}
|
||||
|
||||
script_exception::~script_exception() {
|
||||
}
|
||||
|
||||
char const * script_exception::get_file_name() const {
|
||||
lean_assert(get_source() == source::File);
|
||||
return m_file.c_str();
|
||||
}
|
||||
|
||||
unsigned script_exception::get_line() const {
|
||||
lean_assert(get_source() != source::Unknown);
|
||||
return m_line;
|
||||
}
|
||||
|
||||
char const * script_exception::get_msg() const noexcept {
|
||||
return exception::what();
|
||||
}
|
||||
|
||||
MK_THREAD_LOCAL_GET_DEF(std::string, get_g_buffer)
|
||||
|
||||
char const * script_exception::what() const noexcept {
|
||||
std::string & buffer = get_g_buffer();
|
||||
std::ostringstream strm;
|
||||
char const * msg = get_msg();
|
||||
char const * space = msg && *msg == ' ' ? "" : " ";
|
||||
switch (get_source()) {
|
||||
case source::String: strm << "[string]:" << get_line() << ":" << space << get_msg(); break;
|
||||
case source::File: strm << get_file_name() << ":" << get_line() << ":" << space << get_msg(); break;
|
||||
case source::Unknown: return get_msg();
|
||||
}
|
||||
buffer = strm.str();
|
||||
return buffer.c_str();
|
||||
}
|
||||
|
||||
script_nested_exception::script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<throwable> const & ex):
|
||||
script_exception(s, f, l, "Lean exception"),
|
||||
m_exception(ex) {
|
||||
lean_assert(ex);
|
||||
}
|
||||
|
||||
script_nested_exception::~script_nested_exception() {}
|
||||
|
||||
char const * script_nested_exception::what() const noexcept {
|
||||
std::string super_what = script_exception::what();
|
||||
std::string nested_what = get_exception().what();
|
||||
{
|
||||
std::string buffer;
|
||||
std::ostringstream strm;
|
||||
strm << super_what << "\n" << nested_what;
|
||||
buffer = strm.str();
|
||||
std::string & r_buffer = get_g_buffer();
|
||||
r_buffer = buffer;
|
||||
return r_buffer.c_str();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <string>
|
||||
#include <memory>
|
||||
#include "util/exception.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Exception for wrapping errors produced by the Lua engine.
|
||||
*/
|
||||
class script_exception : public exception {
|
||||
public:
|
||||
enum class source { String, File, Unknown };
|
||||
protected:
|
||||
source m_source;
|
||||
std::string m_file; // if source == File, then this field contains the filename that triggered the error.
|
||||
unsigned m_line; // line number
|
||||
script_exception(source s, std::string f, unsigned l, std::string const & msg):exception(msg), m_source(s), m_file(f), m_line(l) {}
|
||||
public:
|
||||
script_exception(char const * lua_error);
|
||||
virtual ~script_exception();
|
||||
virtual char const * what() const noexcept;
|
||||
virtual source get_source() const { return m_source; }
|
||||
virtual char const * get_file_name() const;
|
||||
virtual unsigned get_line() const;
|
||||
/** \brief Return error message without position information */
|
||||
virtual char const * get_msg() const noexcept;
|
||||
virtual throwable * clone() const { return new script_exception(m_source, m_file, m_line, m_msg); }
|
||||
virtual void rethrow() const { throw *this; }
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Lean exception occurred inside of a script
|
||||
*/
|
||||
class script_nested_exception : public script_exception {
|
||||
std::shared_ptr<throwable> m_exception;
|
||||
script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<throwable> const & ex);
|
||||
public:
|
||||
script_nested_exception(bool file, std::string f, unsigned l, std::shared_ptr<throwable> const & ex):script_nested_exception(file ? source::File : source::String, f, l, ex) {}
|
||||
virtual ~script_nested_exception();
|
||||
virtual char const * what() const noexcept;
|
||||
virtual throwable * clone() const { return new script_nested_exception(m_source, m_file, m_line, m_exception); }
|
||||
virtual void rethrow() const { throw *this; }
|
||||
throwable const & get_exception() const { return *(m_exception.get()); }
|
||||
};
|
||||
}
|
||||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Reference in a new issue