module Dynamic
  class << self
    Thread.main[:DYNAMIC] = Hash.new { |hash, key|
      raise NameError, "no such dynamic variable: #{key}"
    }

    def here!
      Thread.current[:DYNAMIC] = Hash.new { |hash, key|
        raise NameError, "no such dynamic variable: #{key}"
      }.update Thread.main[:DYNAMIC]
    end

    def variables
      Thread.current[:DYNAMIC] or here!
    end
    
    def variable(definition)
      case definition
      when Symbol
        if variables.has_key? definition
          raise NameError, "dynamic variable `#{definition}' already exists"
        end
        variables[definition] = nil
      when Hash
        definition.each { |key, value|
          if variables.has_key? key
            raise NameError, "dynamic variable `#{key}' already exists"
          end
          variables[key] = value
        }
      else
        raise ArgumentError,
        "can't create a new dynamic variable from #{definition.class}"
      end
    end
    
    def [](key)
      variables[key]
    end
    
    def []=(key, value)
      variables[key] = value
    end

    def undefine(*keys)
      keys.each { |key|
        self[key]
        variables.delete key
      }
    end

    def let(bindings, &block)
      save = {}
      bindings.to_hash.collect { |key, value|
        save[key] = self[key]
        self[key] = value
      }
      block.call
      variables.update save
    end

    def method_missing(name, *args)
      if match = /=\Z/.match(name.to_s)    # setter?
        raise ArgumentError, "invalid setter call"  unless args.size == 1
        self[match.pre_match.intern] = args.first
      else
        raise ArgumentError, "invalid getter call"  unless args.empty?
        self[name]
      end
    end
  end
end

Dynamic.variable :solve_environment

module Solve
  @@id = 0
  def self.genid
    @@id += 1
    "_#{@@id}"
  end

  module Operators
    def &(other)
      And.new(self, other)
    end

    def |(other)
      Or.new(self, other)
    end

    def ~@
      Not.new(self)
    end
  end

  def self.variables(*names)
    names.map { |name| Variable.new name }
  end
  
  class Variable
    include Operators
    attr_reader :name
    
    def initialize(name=Solve.genid)
      @name = name.to_sym
      @set = false
      @unify_with = nil
    end

    def ==(value)
      if @set
        Variable.new(@name) == value
      else
        @set = true
        @unify_with = value
        self
      end
    end

    def oneof(range)
      RangeExpr.new(name, range)
    end

    def unify
      env = Dynamic.solve_environment
      if env.has_key? name
        if env[name] == unify_with
          yield
        else
          # do nothing
        end
      else
        Dynamic.let :solve_environment => env.merge({name => unify_with}) do
          yield
        end
      end
    end

    def unify_with
      if Variable === @unify_with && @unify_with != self
        @unify_with.unify_with
      else
        @unify_with
      end
    end

#    def inspect
#      if @set && @unify_with != self
#        ":#{name} = #{@unify_with.inspect}"
#      else
#        ":#{name}"
#      end
#    end
  end


  class And
    include Operators

    def initialize(a, b)
      @a, @b = a, b
    end

    def unify
      @a.unify {
        @b.unify {
          yield
        }
      }
    end

    def inspect
      "(and #{@a.inspect} #{@b.inspect})"
    end
  end

  class Or
    include Operators

    def initialize(*elts)
      @elts = elts
    end

#    def |(other)
#      @elts << other
#      self
#    end
    
    def unify
      @elts.each { |e|
        e.unify { yield }
      }
    end

    def inspect
      "(or" + @elts.map { |e| " #{e.inspect}" }.join + ")"
    end
  end

  class Not
    def initialize(expr)
      @expr = expr
    end

    def unify
      succeed = false
      @expr.unify { succeed = true }
      unless succeed
        yield
      end
    end

    def inspect
      "(not #{@expr.inspect})"
    end
  end

  class RangeExpr
    include Operators

    def initialize(name, range)
      @name = name
      @range = range
    end

    def unify
      env = Dynamic.solve_environment
      if env.include?(@name)
        if @range.include?(env[@name])
          yield
        else
          # fail
        end
      else
        @range.each { |v|
          Dynamic.let :solve_environment => env.merge({@name => v}) do
            yield
          end
        }
      end
    end

    def inspect
      ":#{@name} in #{@range}"
    end
  end

  class Truth
    include Operators

    def unify
      yield
    end

    def inspect
      "true"
    end
  end
  True = Truth.new

  class Falsehood
    include Operators

    def unify
      # fail
    end

    def inspect
      "false"
    end
  end
  False = Falsehood.new
  
  # for lazy evaluation
  class Then
    def self.do(&block)
      new(&block)
    end
    
    def initialize(&block)
      @block = block
    end
    
    def unify
      @block.call.unify { yield }
    end
  end

  def self.solve(expr, &block)
    r = []
    Dynamic.let :solve_environment => {} do
      expr.unify {
        result = Dynamic.solve_environment
        if block_given?
          yield result
        else
          r << result
        end
      }
    end

    if block_given?
      not r.empty?
    else
      r
    end
  end

  def self.forall(enum, &block)
    enum.inject(Solve::True) { |a,e| a & block[e] }
  end

  def self.forany(enum, &block)
    enum.inject(Solve::False) { |a,e| a | block[e] }
  end

end

Then = Solve::Then

module Kernel
  private
  def solve(expr, &block)
    Solve.solve(expr, &block)
  end
end