michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lua): hop_match experiment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-16 00:15:31 -08:00
parent d063828ff9
commit 5453a8f2f1
1 changed files with 36 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
tests/lua/m1.lua Normal file
View file

@ -0,0 +1,36 @@
function body(e)
while (e:is_pi()) do
e = e:abst_body()
end
return e
end
function show_subst(r)
for i = 1, #r do
if r[i] then
print("#" .. tostring(i) .. " <--- " .. tostring(r[i]))
end
end
end
local env = get_environment()
parse_lean_cmds([[
variable f : Nat -> Nat -> Nat
variable g : Nat -> Nat
variable p : Nat -> Bool
variables a b c : Nat
]])
local t = parse_lean([[fun x, (f (g a)) x]])
print(t)
local eta = env:find_object("eta"):get_type()
local eta_lhs = body(eta):arg(2)
print(eta_lhs)
r = hop_match(eta_lhs, t)
print("r: " .. #r)
show_subst(r)
assert(r[3])
print(eta)
local r3_type = env:infer_type(r[3])
print(r3_type)
local eta3_type = eta:abst_body():abst_body():abst_domain()
print(eta3_type)
r2 = hop_match(eta3_type, r3_type)
show_subst(r2)