Module: UnificationAssertion

Defined in:
lib/unification_assertion.rb,
lib/unification_assertion/version.rb

Constant Summary collapse

VERSION = 
"0.0.2"
@@comparators = 
{}
@@substituters = 
{}

Class Method Summary collapse

Class Method Details

.assert_unifiable(a, b, message = "", options = {}, &block) ⇒ Object

Run unification between |a| and |b|, and fails if they are not unifiable. |assert_unifiable| can have block, which yields the unifier for |a| and |b| if exists.



135
136
137
138
139
140
141
142
143
 
# File 'lib/unification_assertion.rb', line 135

def assert_unifiable(a, b, message = "", options = {}, &block)
  unifier = unify([[a, b]], message, {}, options) do |a, b, message|
    assert_equal(a, b, message)
  end

  if block
    yield(unifier)
  end
end

.comparators ⇒ Object

Comparators are hash from a class to its comparator. It is used to check unifiability of two object of the given hash.

There are two comparators defined by default; for |Array| and |Hash|.

Example ==

UnificationAssertion.comparators[Array] = lambda do |a, b, message, eqs, unifier, &block|
  block.call(a.length, bl.ength, message + " (Array length mismatch)")
  eqs.concat(a.zip(b))
end

This is our comparator for |Array|. It first tests if the length of the two arrays are equal. And then, it pushes the equations of each components of the arrays. The components of the arrays will be tested unifiability later.

Comparator ==

Comparator is a lambda which takes 5 arguments and block and checks the unifiability of the first two arguments.

  • |a|, |b| Objects they are compared.

  • |message| Message given to |unify|.

  • |eqs| Equations array. This is for output.

  • |unifier| Current unifier. This is just for reference.

  • |&block| Block given to |unify|, which can be used to check the equality of two values.



44
45
46
 
# File 'lib/unification_assertion.rb', line 44

def comparators
  @@comparators
end

.substitute(unifier, a) ⇒ Object 



123
124
125
126
127
128
129
130
 
# File 'lib/unification_assertion.rb', line 123

def substitute(unifier, a)
  subst = @@substituters[a.class]
  if subst
    subst.call(unifier, a)
  else
    a
  end
end

.substitutions ⇒ Object 



119
120
121
 
# File 'lib/unification_assertion.rb', line 119

def substitutions
  @@substituters
end

.unify(eqs, message = "", unifier = {}, options = {}, &block) ⇒ Object

Run unification algorithm for given equations. If all equations in |eqs| are unifiable, |unify| returns (the most-general) unifier.

Which identifies an symbol as a meta variable if the name matches with |options|. The default of the meta variable pattern is |/^_/|. For example, |:_a| and |:_xyz| are meta variable, but |:a| and |:hello_world| are not.

It also accepts wildcard variable. Which matches with any value, but does not introduce new equational constraints. The default wildcard is |:_|.

|unify| takes a block to test equation of two values. The simplest form should be using |assert_equal|, however it can be customized as you like.

Example ==

unify([[:_a, 1], [{ :x => :_b, :y => 1 }, { :x => 3, :y => 1 }]], "Example!!") do |x, y, message|
  assert_equal(x,y,message)
end

The |unify| call will return an hash |{ :_a => 1, :_b => 3 }|. The block will be used to test equality between 1 and 1 (it will pass.)



69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
 
# File 'lib/unification_assertion.rb', line 69

def unify(eqs, message = "", unifier = {}, options = {}, &block)
  options = { :meta_pattern => /^_/, :wildcard => :_ }.merge!(options)
  
  pattern = options[:meta_pattern]
  wildcard = options[:wildcard]
  
  while eq = eqs.shift
    a,b = eq
    case
    when (Symbol === a and a.to_s =~ pattern)
      unless a == wildcard
        eqs = substitute({ a => b }, eqs)
        unifier = substitute({ a => b }, unifier).merge!(a => b)
      end
    when (Symbol === b and b.to_s =~ pattern)
      unless b == wildcard
        eqs = substitute({ b => a }, eqs)
        unifier = substitute({ b => a }, unifier).merge!(b => a)
      end
    when (a.class == b.class and @@comparators[a.class])
      @@comparators[a.class].call(a, b, message, eqs, unifier, &block)
    else
      yield(a, b, message)
    end
  end
  
  unifier.inject({}) {|acc, (key, value)|
    if key == value
      acc
    else
      acc.merge!(key => value)
    end
  }
end