12.6 Program Collection

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}}
*/