<< Prev | - Up - |
Here are the program generated from the chunks Test TimeUnif, Checking Unifiability, and Test AVM Unification:
declare
proc{UnifBinTree X N}
if N==0 then X=a
else
Y
in
X = f(Y Y)
{UnifBinTree Y N-1}
end
end
/*
declare X = {UnifBinTree $ 1000000}{Browse done}
*/
/*
declare {Browse {Property.get time}}
*/
fun{Time P}
T1 = {Property.get time}.user
{P}
T2 = {Property.get time}.user
in
T2-T1
end
fun{TimeUnif N}
{Time proc{$} {UnifBinTree _ N} end}
end
/*
{Browse {TimeUnif 10000}}
{Browse {TimeUnif 100000}}
{Browse {TimeUnif 200000}}
{Browse {TimeUnif 400000}}
*/
declare
proc{CoRef X} Y in X=f(Y Y) end
proc{ALeft X} X=f(a _) end
proc{BRight X} X=f(_ b) end
fun{Unify Ts}
{Search.allP
proc{$ X}
{ForAll Ts proc{$ T} {T X} end}
end
1 _}
end
fun{IsUnifiable Ts}
case {Unify Ts}
of nil then false
else true
end
end
/*
{Browse {IsUnifiable [ALeft CoRef]}}
{Browse {IsUnifiable [BRight CoRef]}}
{Browse {IsUnifiable [ALeft BRight CoRef]}}
*/
declare
proc{AVM1 X}
Y in X=a(f:a(f:X g:Y h:Y))
end
proc{AVM2 X}
Y in X=a(f:a(f:X g:a(f:Y) h:Y))
end
proc{AVM3 X}
X=a(f:a(f:X g:nono h:_))
end
fun{Unify Ts}
{Search.allP
proc{$ X}
{ForAll Ts proc{$ T} {T X} end}
end
1 _}
end
fun{IsUnifiable Ts}
case {Unify Ts}
of nil then false
else true
end
end
proc{BrowseAVM AVMs}
{ForAll AVMs Browse}
{Browse done}
end
/*
{BrowseAVM {Unify AVM1 AVM2}}
{BrowseAVM {Unify AVM2 AVM3}}
{BrowseAVM {Unify AVM1 AVM3}}
*/
<< Prev | - Up - |