/**
 * Syntactic unification, no variable bindings are taken into account.
 */
module strategy/general/unification
imports 
  collection/list/-
  term/common
  term/properties 
  strategy/general/substitution

strategies
  
  equal = 
    for(id ,[], UfIdem <+ UfDecompose
                //<+ debug(!"not equal: "); FAIL
    )

rules 

  UfIdem : 
    [(x,x) | ps] -> ps

  UfDecompose : 
    [(f#(xs), f#(ys)) | ps] -> <conc>(<zip(id)>(xs, ys), ps)

strategies

  diff =  
    for(\ ps -> ([],ps) \ , (id,[]), (id, UfIdem <+ UfDecompose) <+ UfShift)

rules

  UfShift :
    (ps1, [p | ps2]) -> ([p | ps1], ps2)
    
strategies

  pattern-match(isvar) = 
    for(\ pairs -> (pairs, []) \
       ,\ ([], sbs) -> sbs \
       ,(UfIdem, id) <+ MatchVar(isvar) + (UfDecompose, id))

rules

  MatchVar(isvar) : 
    ([(x,y) | ps], sbs) -> (ps, [(x, y) | sbs])
    where <isvar> x; <not(fetch({z: ?(x,z); <not(eq)> (y, z)}))> sbs

strategies

 /**
  * The strategy unify unifies a list of pairs of terms and creates the
  * most general unifier for them. The strategy is parameterized
  * by a strategy \verb|isvar| that determines the shape of variables.
  *
  * The result is a list of pairs \verb|(x1,p1)|, where \verb|x1| is
  * a term for which \verb|isvar| succeeds and \verb|p1| is the term
  * it should be substituted with to unify the terms.
  *
  * E.g. <unify(isvar)> [(t1,t2),(t3,t4),...] => [(x1,p1),(x2,p2),...]
  */
  unify(isvar) =
    for(\ pairs -> (pairs, []) \
       ,\ ([], sbs) -> sbs \
       ,(UfIdem, id) <+ UfVar(isvar) + UfSwap(isvar) <+ (UfDecompose, id))

rules

  UfVar(isvar) : 
	([(x,y) | ps], sbs) -> (ps', [(x, y) | sbs''])
	where <isvar> x; <not(is-subterm)>(x,y); 
              <substitute(isvar)> ([(x,y)], (sbs, ps)) => (sbs'', ps')

  UfSwap(isvar) : 
	([(x,y) | ps], sbs) -> ([(y,x) | ps], sbs)
	where <not(isvar)> x; <isvar> y

strategies

  equal(fltr) =
    for(id ,[], UfIdem 
                <+ try([(fltr,fltr)|id]); UfDecompose
                //<+ debug(!"not equal: "); FAIL
    )

strategies

 /**
  * The following equality strategy has an additional filter 
  * that can be used for checking equality modulo alpha renaming. 
  * The filter applies to the entire pair and can change something 
  * in one term based on the other term.
  */
  equal(fltr1, fltr2) =
    for(id ,[], UfIdem 
                <+ [(try(fltr1),try(fltr1)); try(fltr2)|id]; UfDecompose
                //<+ debug(!"not equal: "); FAIL
    )