-- ===============
-- Calculus L_need
-- ===============

-- the syntax comprises letrec, variables, abstractions, and applications
-- the LRSX-unification tool automatically detects the abstractions,applications app
-- with the right arity, strictness, and operator arity.

-- We first define the context classes A,T,C
-- Note that the syntax   ctxt1 / ctxt2  means
--   use ctxt1 for unification and ctxt2 for matching,
--   or matching more solutions are found if the 'most' general context is used,
--   this is only the case in our example for the case that the context hole is 
--   in a letrec enviroment: then it is more general to plug the hole into 
--   an EE-chain than plugging it into a single binding, since EE-chain can match other 
--   EE-chains and also single bindings, while single bindings cannot match EE-chains

define A ::= [.] | (app A S) | (seq A S)
define T ::= [.] | (app T S) | (app S T) | (seq T S) | (seq S T) | letrec X=T;E in S / letrec EE^A[X,T];E in S  | letrec E in T where E /= {}
define C ::= [.] | \X.C | (app C S) | (app S C) |  (seq C S) | (seq S C) |  letrec X=C;E in S / letrec EE^A[X,C];E in S  | letrec E in C where E /= {} 


-- Note that EE^A[,] are chain-variables of A-contexts, and
-- VV|,| are chain-variables of the trivial context

-- We now provide the prefix table for contexts
-- prefix (Class1,Class2) = (Class3,Class4)  means that 
--   an equation D1^Class1[s] =?= D2^Class2[t]
--          can (and must) be branched into
--          s =?= D2'^Class4[t]
--          with substitutions 
--          D1^Class1 |-> D1'^Class3
--          D2^Class2 |-> D1'^Class3 D2'^Class4

declare prefix A A = (A,A) 
declare prefix A T = (A,T)
declare prefix A C = (A,C)
declare prefix T A = (A,A)
declare prefix T T = (T,T)
declare prefix T C = (T,C)
declare prefix C A = (A,A)
declare prefix C T=  (T,T)
declare prefix C C = (C,C)

--  We now provide the forking table for contexts
--   where 
--     fork (Class1,Class2) = (Class3,Class4,Class5,d[.1,.2])  means that 
--        an equation D1^Class1[s] =?= D2^Class2[t] 
--        can (and must) be branched into
--           D1^Class1 |->  D3^Class3[d[D4^Class4[.1]][D5^Class5[t]]]
--           D2^Class1 |->  D3^Class3[d[D4^Class4[s]][D5^Class5[.2]]]
--      since there are several possibilities for the d-context
--      there are several lines per definition  

declare fork   A T = (A,A,T,(app [.1] [.2]))
declare fork   A T = (A,A,T,(seq [.1] [.2]))
declare fork   A C = (A,A,C,(app [.1] [.2]))
declare fork   A C = (A,A,C,(seq [.1] [.2]))
declare fork   T T = (T,T,T,(app [.1] [.2]))
declare fork   T T = (T,T,T,(app [.2] [.1]))
declare fork   T T = (T,T,T,(seq [.1] [.2]))
declare fork   T T = (T,T,T,(seq [.2] [.1]))
declare fork   T T = (T,T,T,(letrec X=[.1];E in [.2]))
declare fork   T T = (T,T,T,(letrec X=[.2];E in [.1]))
declare fork   T T = (T,T,T,(letrec X=[.1];Y=[.2];E in S))
declare fork   T C = (T,T,C,(app [.1] [.2]))
declare fork   T C = (T,T,C,(app [.2] [.1]))
declare fork   T C = (T,T,C,(seq [.1] [.2]))
declare fork   T C = (T,T,C,(seq [.2] [.1]))
declare fork   T C = (T,T,C,(letrec X=[.1];E in [.2]))
declare fork   T C = (T,T,C,(letrec X=[.2];E in [.1]))
declare fork   T C = (T,T,C,(letrec X=[.1];Y=[.2];E in S))


declare fork   T A = (A,T,A,(app [.2] [.1]))
declare fork   T A = (A,T,A,(seq [.2] [.1]))


declare fork   C A = (A,C,A,(app [.2] [.1]))
declare fork   C C = (C,C,C,(app [.1] [.2]))
declare fork   C C = (C,C,C,(app [.2] [.1]))
declare fork   C A = (A,C,A,(seq [.2] [.1]))
declare fork   C C = (C,C,C,(seq [.1] [.2]))
declare fork   C C = (C,C,C,(seq [.2] [.1]))
declare fork   C C = (C,C,C,(letrec X=[.1];E in [.2]))
declare fork   C C = (C,C,C,(letrec X=[.2];E in [.1]))
declare fork   C C = (C,C,C,(letrec X=[.1];Y=[.2];E in S))

declare fork   C T = (T,C,T,(app [.2] [.1]))
declare fork   C T = (T,C,T,(app [.1] [.2]))
declare fork   C T = (T,C,T,(seq [.2] [.1]))
declare fork   C T = (T,C,T,(seq [.1] [.2]))
declare fork   C T = (T,C,T,(letrec X=[.2];E in [.1]))
declare fork   C T = (T,C,T,(letrec X=[.1];E in [.2]))
declare fork   C T = (T,C,T,(letrec X=[.2];Y=[.1];E in S))


-- =======================
-- normal order reduction
-- =======================

-- ***********************
-- **
-- three cases for (no,lbeta)-redution, corresponding to the reduction contexts 

{SR,lbeta,1}  A[app (\X.S1) S2]  ==> A[letrec X=S2 in S1]  

where (S2,\X.[.]),(S2,letrec X=[.] in S1)
{SR,lbeta,2}  letrec E in A[app (\X.S1) S2] ==> letrec E in A[letrec X=S2 in S1]
              where E /= {},(S2,\X.[.]),(S2,letrec X=[.] in S1)
{SR,lbeta,3}  letrec E; EE^A[X1,app (\X.S1) S2] in A1[var X1] ==> letrec E; EE^A[X1,letrec X=S2 in S1] in A1[var X1] 
              where (S2,\X.[.]),(S2,letrec X=[.] in S1)
              
{SR,seq,1}  A[seq (\X.S1) S2]  ==> A[S2]  
             
{SR,seq,2}  letrec E in A[seq (\X.S1) S2] ==> letrec E in A[S2]
 where E /= {}
{SR,seq,3}  letrec E; EE^A[X1,seq (\X.S1) S2] in A1[var X1] ==> letrec E; EE^A[X1,S2] in A1[var X1] 


-- **         
-- ***********************
   
-- ***********************
-- **   
-- cases for (no,cp-in)-reduction (without/with variable-to-variable chain)
                        
{SR,cp-in,1}  letrec VV|Xn,\X.S|; E in A[var Xn] ==> letrec VV|Xn,\X.S|; E in A[\X.S] 

-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- cases for (no,cp-e)-reduction (without/with variable-to-variable chain)
                        
{SR,cp-e,1}   letrec VV|Xn,\X.S|; EE^A[Y,A1[var Xn]]; E in A[var Y] ==> letrec  VV|Xn,\X.S|; EE^A[Y,A1[\X.S]]; E in A[var Y] 
              where A1 /= []

-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- (no,llet-in)
    
{SR,llet-in,1} letrec E1 in letrec E2 in R ==> letrec E1;E2 in R 
               where E1 /= {},E2 /= {},[E1,letrec E2 in [.]]
        
-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- two cases for (no,llet-e), without/with EE-chain
                        
{SR,llet-e,1} letrec E1;X=letrec E2 in R in A[var X] ==> letrec E1;E2;X=R in A[var X] 
              where E2 /= {},[E1,letrec E2 in [.]],(A[var X],letrec E2 in [.])
                          
{SR,llet-e,2} letrec E1;X=letrec E2 in R;EE^A[Y,var X] in A[var Y] ==> letrec E1;E2;X=R;EE^A[Y,var X] in A[var Y]     
              where E2 /= {},[E1;EE^A[Y,var X],letrec E2 in [.]],(var X,letrec E1;E2;EE^A[Y,var X] in [.]),(A[var Y],letrec E2 in [.])
         
-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- three cases for (no,lapp) corresponding to reduction contexts

{SR,lapp,1}         A[app (letrec E in R) S] ==> A[letrec E in (app R S)] 
    where  E /={},(S,letrec E in [.])
                    
{SR,lapp,2}         letrec E1 in A[app (letrec E in R) S] 
                    ==> letrec E1 in A[letrec E in (app R S)]
    -- constraints:                    
    where E1 /= {}
         ,E /={} 
         ,(S,letrec E in [.])

{SR,lapp,3}         letrec E1;EE^A[X,app (letrec E in R) S] in A1[var X] 
                    ==> letrec E1;EE^A[X,letrec E in app R S] in A1[var X] 
    -- constraints:
    where E/={}
         ,(S,letrec E in [.])


{SR,lseq,1}         A[seq (letrec E in R) S] ==> A[letrec E in (seq R S)] 
    where  E /={},(S,letrec E in [.])
                    
{SR,lseq,2}         letrec E1 in A[seq (letrec E in R) S] 
                    ==> letrec E1 in A[letrec E in (seq R S)]
    -- constraints:                    
    where E1 /= {}
         ,E /={} 
         ,(S,letrec E in [.])

{SR,lseq,3}         letrec E1;EE^A[X,seq (letrec E in R) S] in A1[var X] 
                    ==> letrec E1;EE^A[X,letrec E in seq R S] in A1[var X] 
    -- constraints:
    where E/={}
         ,(S,letrec E in [.])

-- transitive closures of lapp, only used for closing ucp
{SR,lll,+,1}         A[letrec E in R]
                    ==> letrec E in A[R]
    -- constraints:
    where  A/=[], E /={}
          ,(A[dummy0[]],letrec E in [.])

{SR,lll,+,2}    letrec E1 in A[letrec E in R]
                    ==> letrec E1;E in A[R]
    -- constraints:
    where E1 /= {}
         ,E /={}
         ,A/= []
         ,(A[dummy0[]],letrec E in [.])
         ,[E1,letrec E in [.]]

{SR,lll,+,3}    letrec E1;EE^A[X,A[letrec E in R]] in A1[var X]
                    ==> letrec E1;E;EE^A[X,A[R]] in A1[var X]
    -- constraints:
    where E/={}, A/=[]
         ,(A[dummy0[]],letrec E in [.])
         ,[E1,letrec E in [.]]
         ,(var X,letrec E in [.])

-- **
-- ***********************                    
                            
-- =======================
-- Several program transformations
-- =======================
-- 


{lbeta}          T[app (\X.S) R] 
                    ==> T[letrec X=R in S]            
    where (R,\X.[.])
{seq}          T[seq (\X.S) R] 
                    ==> T[R]            
                       
{cpT-in}         T[letrec X1 = \X.S; E in T1[var X1]] 
                    ==> T[letrec X1 = \X.S; E in T1[\X.S]]
    where (\X.S, T1)
          ,(var X1,T1)
         ,(S,T1)              
{cpd-in}         T[letrec X1 = \X.S; E in C1[\Y.T2[var X1]]]
                    ==> T[letrec X1 = \X.S; E in C1[\Y.T2[\X.S]]]
    where (\X.S, C1[\Y.T2])
          ,(var X1,C1[\Y.T2])
         ,(S,C1[\Y.T2])              
            
{cpT-e,1}          T[letrec X1 = \X.S; Y = T1[var X1];E in R] 
                    ==> T[letrec X1 = \X.S; Y = T1[\X.S];E in R] -- note that varchains are not included
    where (\X.S, T1)
          ,(var X1,T1)
          ,(S,T1)
          
{cpd-e,1}           T[letrec X1 = \X.S; Y = C1[\Z.T2[var X1]];E in R] 
                    ==> T[letrec X1 = \X.S; Y = C1[\Z.T2[\X.S]];E in R] -- note that varchains are not included
    where (\X.S, C1[\Z.T2])
          ,(var X1,C1[\Z.T2])
          ,(S,C1[\Z.T2])
             
{llet-in}        T[letrec E1 in letrec E2 in S] 
                    ==> T[letrec E1;E2 in S]   
    where E1/={}
        , E2/={}
        , [E1,letrec E2 in [.]]
        
{llet-e}         T[letrec E1; X=letrec E2 in S1 in R] 
                    ==> T[letrec E1; E2; X=S1 in R] 
    where E2/={}
       , [E1,letrec E2 in [.]]
       , (R,letrec E2 in [.])
       
{lapp}           T[app (letrec E in R) S] 
                    ==> T[letrec E in (app R S)] 
    where E/={}
        ,(S, letrec E in [.])
{lseq}           T[seq (letrec E in R) S] 
                    ==> T[letrec E in (seq R S)] 
    where E/={}
        ,(S, letrec E in [.])
                       
{cpT-e,2}     T[letrec X1 = \X.S; EE^A[Xn,T1[var X1]]; E in R]
                    ==> T[letrec X1 = \X.S; EE^A[Xn,T1[\X.S]]; E in R]
    where (S,T1)
         ,(\X.S,T1)
         ,(var X1,T1)
         
{cpd-e,2}     T[letrec X1 = \X.S; EE^A[Xn,C1[\Z.T2[var X1]]]; E in R]
                    ==> T[letrec X1 = \X.S; EE^A[Xn,C1[\Z.T2[\X.S]]]; E in R]
    where (S,C1[\Z.T2])
         ,(\X.S,C1[\Z.T2])
         ,(var X1,C1[\Z.T2])
      
{cpx-in}        T[letrec X = (var Y); E in C[var X]] 
                    ==> T[letrec X = (var Y); E in C[(var Y)]]
    where (var X, C), 
          (var Y, C)
                        
{cpx-e,1}         T[letrec X = (var Y); Z = C[var X]; E in S] 
                    ==> T[letrec X = (var Y); Z = C[var Y]; E in S]
    where (var X, C), 
          (var Y, C)

-- overlaps already covered by T-cpx-e but inserted for closing diagrams:                       

{cpx-e,2}   T[letrec X = (var Y); EE^A[Z,C[var X]]; E in S] 
                    ==> T[letrec X = (var Y); EE^A[Z,C[var Y]]; E in S]
    where (var X, C), 
          (var Y, C)
          
{xch}            T[letrec X = (var Y); Y = S1; E in S2] 
                    ==> T[letrec X = S1; Y = (var X);  E in S2]
                        
{gc,2}           T[letrec E in S] 
                    ==> T[S]
    where E /= {}
        ,(S,letrec E in [.])

{gc,1}            T[letrec E1;E2 in S] 
                    ==> T[letrec E1 in S]
    where E1 /= {}
         ,E2 /= {}
        ,[E1,letrec E2 in [.]]
        ,(S,letrec E2 in [.])
                         
{ucp,1}       T[letrec X=S; E in T1[var X]]
                ==> T[letrec E in T1[S]]
    where E /= {},(var X,T1),(S,T1),(letrec E in T1[dummy3[]], letrec X=dummy3[] in [.])
         ,(S, letrec X=dummy3[] in [.])

{ucp,2}       T[letrec X=S; E; Y=T1[var X] in S1]
                ==> T[letrec E; Y=T1[S] in S1]
    where  (var X,T1),(S,T1),(letrec  E; Y= T1[dummy3[]] in S1, letrec X=dummy3[] in [.])
          ,(S, letrec X=dummy3[] in [.])

{ucp,3}       T[letrec X=S in T1[var X]]
                ==> T[T1[S]]
    where  (var X,T1),(S,T1),(T1[dummy3[]], letrec X=dummy3[] in [.])
           ,(S, letrec X=dummy3[] in [.])
 
ANSWER \X.S
ANSWER letrec E in \X.S where E /= {}

           
union (cpd,0)       = {(cpd-in,1), (cpd-e,1), (cpd-e,2) }
union (cpT,0)       = {(cpT-in,1), (cpT-e,1), (cpT-e,2) }
union (llet,0)      = { (llet-in,1), (llet-e,1) }           
-- union (lll,0)    = { (llet,0), (lapp,1) }
union (ucp,0)       = { (ucp,1), (ucp,2), (ucp,3)}
union (gc,0)        = { (gc,1), (gc,2) }
union (cpx-e,0)     = { (cpx-e,1), (cpx-e,2) }
union (cpx,0)       = { (cpx-e,0), (cpx-in,1) }
-- union (trans,0)  = { (lll,0),(cp,0),(lbeta,1),(ucp,0), (gc,0)}           
union (SR,lbeta,0)  = { (SR,lbeta,1), (SR,lbeta,2), (SR,lbeta,3) }
union (SR,cp-in,0)  = { (SR,cp-in,1), (SR,cp-in,2) }
union (SR,cp-e,0)   = { (SR,cp-e,1), (SR,cp-e,2) }
union (SR,cp,0)     = { (SR,cp-in,0), (SR,cp-e,0) }
union (SR,lapp,0)   = { (SR,lapp,1), (SR,lapp,2), (SR,lapp,3) }
union (SR,lseq,0)   = { (SR,lseq,1), (SR,lseq,2), (SR,lseq,3) }
union (SR,llet-e,0) = { (SR,llet-e,1),(SR,llet-e,2) }
union (SR,llet,0)   = { (SR,llet-in,1), (SR,llet-e,0) }
union (SR,lll,0)    = { (SR,llet,0), (SR,lapp,0),(SR,lseq,0) }
union (SR,lll,+,0)    = { (SR,lll,+,1), (SR,lll,+,2),(SR,lll,+,3) }