Class: Unific::Env

Inherits:
Object
  • Object
show all
Defined in:
lib/unific.rb

Overview

An environment (set of variable bindings) resulting from unification

Constant Summary collapse

@@trace = 
0

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(prev = {}) ⇒ Env

Allocate a new environment. Usually not needed – use Unific::unify, instead.

The new environment will be empty unless a hash of variable bindings is included. Use this with care.



15
16
17
 
# File 'lib/unific.rb', line 15

def initialize prev = {}
  @theta = prev.clone
end

Class Method Details

.trace(lvl) ⇒ Object

Turn on tracing (to STDERR) of Unific operations

intended for use by Unific::trace

The optional level argument sets the verbosity – if not passed, each call to this method increases verbosity



25
26
27
28
29
30
31
 
# File 'lib/unific.rb', line 25

def self.trace lvl #:nodoc:
  if lvl
    @@trace = lvl
  else
    @@trace = @@trace + 1
  end
end

.untrace ⇒ Object

Turn off tracing (to STDERR) of Unific operations

intended for use by Unific::trace



36
37
38
 
# File 'lib/unific.rb', line 36

def self.untrace #:nodoc:
  @@trace = 0
end

Instance Method Details

#[](x) ⇒ Object

Return the binding of a variable in this environment, or nil if it is unbound



46
47
48
 
# File 'lib/unific.rb', line 46

def [] x
  @theta[x]
end

#bindings ⇒ Object 



150
151
152
 
# File 'lib/unific.rb', line 150

def bindings
  @theta.keys
end

#fresh?(x) ⇒ Boolean

Return whether a given variable is fresh (not bound) in this environment

Returns:

  • (Boolean) 


41
42
43
 
# File 'lib/unific.rb', line 41

def fresh? x
  not @theta.has_key? x
end

#instantiate(s) ⇒ Object

Given a value, substitute any variables present in the term.

If the passed value is a Ruby Enumerable other than a String, recurs on the members of the Enumerable. Unlike #[], also repeatedly substitutes each variable until it gets a ground (non-variable) term or a free variable



114
115
116
117
118
119
120
121
122
 
# File 'lib/unific.rb', line 114

def instantiate s
  _traverse s do |v|
    if fresh? v
      v
    else
      instantiate @theta[v]
    end
  end
end

#rename(s) ⇒ Object

Perform alpha renaming on an expression

Alpha-renaming an expression replaces all fresh variables in the expression with new variables of the same name. This is used by rulog to to give each Rule its own private copy of all of its variables.



129
130
131
132
133
134
135
136
137
138
139
 
# File 'lib/unific.rb', line 129

def rename s
  _traverse s do |v|
    if fresh? v
      n = Unific::Var.new(v.name)
      @theta[v] = n;
      n
    else
      instantiate @theta[v]
    end
  end
end

#to_s ⇒ Object 



55
56
57
 
# File 'lib/unific.rb', line 55

def to_s
  "{ " + @theta.map{|k, v| "#{k} => #{v}"}.join(", ") + "} "
end

#unify(a, b) ⇒ Object

Unify two values against this environment, returning a new environment

If the two values cannot be unified, ‘false’ is returned. If they can, a new environment is returned which is this environment extended with any new bindings created by unification.

Each value to unify can be

  1. a Unific::Var variable

  2. the wildcard variable, Unific::_

  3. any ruby Enumerable except a String, in which case unification recurs on the members

  4. a String or any other ruby object (as a ground term – unification succeeds

if the two are equal (with ‘==’))

In logic programming terms, the returned env is the Most General Unifier (MGU) of the two terms



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
103
104
105
106
107
 
# File 'lib/unific.rb', line 75

def unify a, b
  puts "unifying #{a.to_s} and #{b.to_s}" if @@trace > 0

  # if either is already bound, substitute up front
  a = instantiate a
  b = instantiate b

  # any remaining Var is fresh.
  if a.kind_of? Var and b.kind_of? Var
    _extend a => b
  elsif a.kind_of? Var
    _extend a => b
  elsif b.kind_of? Var
    _extend b => a
  elsif a.kind_of? String and b.kind_of? String # strings should be treated as ground
    if a == b
      self
    else
      Unific::fail
    end
  elsif a.kind_of? Enumerable and b.kind_of? Enumerable
    return Unific::fail unless a.size == b.size
    a.zip(b).inject(self) do |e, pair|
      e.unify(pair[0], pair[1]) or return Unific::fail
    end
  else # both are ground terms
    if a == b
      self
    else
      Unific::fail
    end
  end
end

#variables(s) ⇒ Object

Return just the variables from an expression, as a flat array



142
143
144
145
146
147
148
 
# File 'lib/unific.rb', line 142

def variables s
  res = []
  _traverse s do |v|
    res << v
  end
  res.uniq
end