Na}{

File Content: `Spec.py`

#._cv_part guppy.heapy.Spec

"""
Contains some experimental set constructions.
In the current state, not to be used by the faint-hearted.
It is likely due for some major refactoring and has probably
many bugs, it was a long time since I run the tests.
You don't get any other documentation than this right now.

"""


DEBUG=1

def briefstr(x):
    try:
	return getattr(x, 'brief')
    except AttributeError:
	if isinstance(x, tuple):
	    return '(%s)'%(','.join([briefstr(xi) for xi in x]))
	return str(x)


class SpecFamily:
    def __init__(self, unisetmod, specmod):
	self.specmod = specmod
	self.defrefining(unisetmod.Anything)
	self.disjoints -= [self]

    def __call__(self, arg):
	return self.Set(self, arg)

    def c_and(self, a, b):
	if isinstance(b, SpecFamily):
	    return self.mod.fam_And._cons((a, b))
	else:
	    return b.fam._and_ATOM(b, a)
	    

    def _and_ID(self, a, b):
	env = self.specmod._static_test_env
	res = self.mod.mutnodeset()
	for bi in b.nodes:
	    try:
		env.test_contains(a, bi, 'select contains')
	    except : #TestError
		pass
	    else:
		res.add(bi)
	return self.mod.fam_Identity._cons(self.mod.immnodeset(res))


    def c_contains(self, a, b):
	env = self.specmod._static_test_env
	try:
	    return env.test_contains(a, b, 'Spec contains')
	except TestError:
	    return False

    def c_getlimstr(self, a, max_len):
	x = a.brief
	if len(x) > max_len:
	    x = x[:max_len-3]+'...'
	return x

    def c_get_brief(self, a):
	return '<%s(%s)>'%(self.__class__.__name__, briefstr(a.arg))

    if 0:

	def c_select(self, a, b):
	    env = self.specmod._static_test_env
	    res = self.mod.mutnodeset()
	    for bi in b:
		try:
		    env.test_contains(a, bi, 'select contains')
		except TestError:
		    pass
		else:
		    res.add(bi)
	    return self.mod.fam_Identity._cons(self.mod.immnodeset(res))

class ArgNamesFamily(SpecFamily):
    def __call__(self, *args):
	return self.Set(self, args)

    def getargnames(self, code):
	inspect = self.specmod._root.inspect
	(args, varargs, varkw) = inspect.getargs(code)
	if varargs is not None:
	    args.append('*%s'%varargs)
	if varkw is not None:
	    args.append('**%s'%varkw)
	return tuple(args)

    def func_argnames(self, f, args):
	try:
	    code = f.func_code
	    return self.getargnames(code) == args
	except AttributeError:
	    return False

    def meth_argnames(self, m, args):
	try:
	    f = m.im_func
	    code = f.func_code
	    return self.getargnames(code)[1:] == args
	except AttributeError:
	    return False

    def c_contains(self, a, x):
	func_argnames = lambda f:self.func_argnames(f, a.arg)
	meth_argnames = lambda m:self.meth_argnames(m, a.arg)
	types = self.mod._root.types
	return (func_argnames(x) or
		meth_argnames(x) or
		(isinstance(x, types.InstanceType) and
		 hasattr(x, '__call__') and
		 meth_argnames(x.__call__)) or
		(isinstance(x, types.ClassType) and
		 (hasattr(x, '__init__') and
		  meth_argnames(x.__init__))) or
		(isinstance(x, types.TypeType) and
		 (hasattr(x, '__init__') and
		  meth_argnames(x.__init__))) or
		 (hasattr(x, '__call__') and
		  meth_argnames(x.__call__))
		)

class AttributeFamily(SpecFamily):
    def __call__(self, name, type=None):
	if type is None:
	    type = self.specmod.any
	else:
	    if not isinstance(type, self.mod.UniSet):
		type = self.c_from(type)
	return self.specotup((name, type))
	
    def c_test_contains(self, a, b, env):
	name, type = a.arg
	x = env.gengetattr(b, name)
	return type.test_contains(x, env)

    def c_get_brieflimstr(self, a):
	x = '<AttributeFamily(%r%%s>'%(a.arg[0],)
	if a.arg[1] is not None:
	    x = x%(','+a.arg[1].brief)
	else:
	    x = x%''
	return x

class AdaptupleFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)
	self.add_export('new', lambda x:x.arg[0])

    def __call__(self, func, type):
	func, doc = self.specmod._exodoc(func)
	type = self.specmod.setcast(type)
	return self.specoargtup((func, type), (doc, type))
	
    def c_test_contains(self, a, b, env):
	func, type = a.arg
	if isinstance(b, tuple):
	    try:
		x = func(*b)
	    except:
		return env.failed_exc_info('calling func failed')
	else:
	    x = b
	return type.test_contains(x, env)


class CartesianProductFamily(SpecFamily):
    def __call__(self, *types):
	return self.Set(self, types)

    def c_domain(self, a):
	types = a.arg
	if len(types) == 2:
	    return types[0]
	raise TypeError, 'Domain is defined on binary relations only'

    def c_get_examples(self, a, env):
	# We have to check length before calling iterpermute - 
	# to give a reasonable error message examples are missing from some set.
	exs = []
	for i, ai in enumerate(a.arg):
	    ex = list(env.get_examples(ai))
	    if not ex: #???
		if not env.failed_coverage('cartesian product', ai, None, 'the argument #%d'%i):
		    return []
	    exs.append(ex)
		      
	return self.mod._root.guppy.etc.iterpermute(*exs)

    def c_len(self, a):
	l = 1
	for ai in a.arg:
	    l = l * len(ai.arg)
	return l

    def c_test_contains(self, a, b, env):
	types = a.arg
	bs = tuple(b)
	if len(types) != len(bs):
	    env.failed('cprod of length %d: argument has length %d'%(len(types), len(bs)))
	else:
	    for t, b in zip(types, bs):
		if not t.test_contains(b, env):
		    return False
	    return True


class SequenceFamily(SpecFamily):
    def __call__(self, type):
	return self.specoarg(type)

    def c_test_contains(self, a, b, env):
	for x in b:
	    if not a.arg.test_contains(x, env):
		return False
	return True

    def c_get_examples(self, a, env):
	for i in range(env.max_sequence_examples_length):
	    for x in env.get_examples(self.specmod.cprod(*[a.arg]*i)):
		yield x
				      


class MappingFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)
	self.add_export('arrow', lambda x:lambda f:self.c_arrow(x, f))

    def c_arrow(self, a, f):
	tf, ts, ret = a.arg
	return Arrow(ts, ret, f)

    def __call__(self, *args):
	ts = []
	as_ = []
	ret = None
	i = 0
	setcast = self.specmod.setcast
	while i < len(args):
	    ai = args[i]
	    if isinstance(ai, str):
		if ai == '->':
		    i += 1
		    if not i == len(args)-1:
			raise SyntaxError, \
			      "The '->' specifier must be next to last in the argument list"
		    ret = setcast(args[i])
		elif ai.endswith('='):
		    i += 1
		    t = setcast(args[i])
		    as_.append('%s=%args[%d]'%(ai[:-1], len(ts)))
		    ts.append(t)
		elif ai == '*':
		    i += 1
		    t = setcast(args[i])
		    as_.append('*args[%d]'%len(ts))
		    ts.append(self.specmod.sequence(t))
		else:
		    raise SyntaxError, \
			  "Invalid argument specifier: %r"%ai
				     
	    else:
		as_.append('args[%d]'%len(ts))
		ts.append(setcast(ai))
	    i += 1
		
	fn = 'lambda f: lambda *args: f('+','.join(as_)+')'
	f = eval(fn)
	ts = self.specmod.cprod(*ts)
	if ret is None:
	    ret = self.specmod.Anything
	return self.Set(self, (f, ts, ret))

    def c_test_contains(self, a, func, env):
	f, ts, ret = a.arg
	
	f = f(func)
	def g(env, args):
	    try:
		r = f(*args)
	    except: # TypeError, ValueError, AttributeError ... - what not
		raise
		#env.failed('Call exception')
	    else:
		if ret is not None:
		    return env.test_contains(ret, r, "Mapping Return Type")
		else:
		    return True
		
	return env.forall(ts, g)

    def c_get_examples(self, a, env):
	f, ts, ret = a.arg

	return [lambda *args, **kwds: x for x in env.get_examples(ret)]


class PredicateFamily(SpecFamily):
    def __call__(self, arg, doc):
	return self.Set(self, (arg, doc))
	
    def c_test_contains(self, a, b, env):
	pred, doc = a.arg
	if not pred(env, b):
	    return env.failed('pred: doc = %r; failed for element == %s'%(doc, env.name(b)))
	return True

class PowersetFamily(SpecFamily):
    def __init__(self, *args):
	SpecFamily.__init__(self, *args)
	self.add_export('union', lambda x: x.arg)

    def __call__(self, set):
	return self.specoarg(set)

    def c_get_examples(self, a, env):
	x = [self.specmod.Nothing, a.arg]
	try:
	    y = env.get_examples(a.arg)
	except:
	    # xxx complain? We can always generate 2 examples..
	    return x
	# xxx should we make all permutations?..
	return x

    def c_test_contains(self, a, b, env):
	if not b in self.specmod.set:
	    env.failed('powerset.test_contains: not a set: %s'%self.specmod.iso(b))
	set = a.arg
	return env.forall(b, lambda env, x: env.test_contains(set, x, 'powerset'), 'powerset')


class DocFamily(SpecFamily):
    def __call__(self, doc, type=None):
	if type is None:
	    type = self.specmod.UniSet.NotNothing
	else:
	    if not type in self.specmod.set:
		type = self.specmod.UniSet.convert(type)
	return self.Set(self, (doc, type))

    def c_test_contains(self, a, b, env):
	doc, type = a.arg
	return type.test_contains(b, env)

class RelOpFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)
	self.add_export('domain', lambda x:x.arg[0])
	self.add_export('range', lambda x:x.arg[2])
	# The memo dict keeps relops with the same domain, op, and range.
	# Primarily introduced to make equality work with default mechanism,
	# since different compiled func's compared differently even with
	# the same source.
	self.memo = {}

    def __call__(self, domain, op, range=None):
	domain = self.specmod.setcast(domain)
	if range is None:
	    range = domain
	else:
	    range = self.specmod.setcast(range)
	x = self.memo.get((domain, op, range))
	if x is None:
	    if op in ('<', '<=', '==', '!=', '>', '>=', 'in', 'not in', 'is', 'is not'):
		func = eval('lambda x,y: x %s y'%op)
		func.name = op
	    else:
		func = op
		func.name = func.func_name
	    x = self.Set(self, (domain, func, range))
	    self.memo[(domain, op, range)] = x
	return x
    
    def c_get_examples(self, a, env):
	# We have to check length before calling iterpermute - 
	# to give a reasonable error message examples are missing from some set.
	dom = list(env.get_examples(a.domain))
	if not dom:
	    failed_coverage('relation', a.domain, None, 'domain')
	    return []
	
	ran = list(env.get_examples(a.range))
	if not ran:
	    failed_coverage('relation', a.range, None, 'range')
	    return []
	
	exs = []
	for ex in self.specmod._root.guppy.etc.iterpermute(dom, ran):
	    if env.contains(a, ex):
		exs.append(ex)
	return exs

    def c_test_contains(self, a, b, env):
	d, op, r = a.arg
	if not op(*b):
	    return env.failed()
	return True



class EqualsFamily(SpecFamily):
    def __call__(self, *args):
	if not args:
	    return self.specmod.Nothing
	return self.specotup(args)

    def c_test_contains(self, a, b, env):
	if b in a.arg:
	    return True
	return env.failed('equals')

    def c_get_examples(self, a, env):
	return a.arg
	    
class ExampleFamily(SpecFamily):
    def __call__(self, set, *examples):
	return self.Set(self, (set, examples))

    def c_test_contains(self, a, b, env):
	set, examples = a.arg
	return set.test_contains(b, env)

    def c_get_examples(self, a, env):
	set, examples = a.arg
	# for e in examples:	    env.test_contains(set, e, 'ExampleFamily.c_get_examples')
	return examples

class SynonymsFamily(SpecFamily):
    def __call__(self, *names):
	return self.Set(self, names)

    def c_test_contains(self, a, b, env):
	names = a.arg
	ms = self.specmod.UniSet.mutnodeset()
	for name in names:
	    x = env.getattr(b, name)
	    ms.add(x)
	if not len(ms):
	    env.failed('Synonyms: no such names: %r'%names)
	if len(ms) > 1:
	    env.failed('Synonyms: %d different nodes for names: %r'%(len(ms), names))
	return True
		       
class InstanceFamily(SpecFamily):
    def c_test_contains(self, a, b, env):
	if not isinstance(b, a.arg):
	    env.failed('InstanceFamily: %s is not an instance of %s'%(
		self.specmod.iso(b), a.arg))
	return True

    def c_get_examples(self, a, env):
	return env.get_examples(self.specmod.setcast(a.arg))

    def _and_ID(self, a, b):
	return self.mod.fam_Identity(*[bi for bi in b.nodes if isinstance(bi, a.arg)])


class ExpressionPredicateFamily(SpecFamily):
    def __call__(self, names, expression):
	func = None
	return self.Set(self, (names, expression, func))

    def c_test_contains(self, a, b, env):
	names, expression, func = a.arg
	func = eval('lambda %s:%s'%(','.join(names), expression))
	d = {}
	for name in names:
	    x = env.getattr(b, name)
	    d[name] = x
	try:
	    x = func(**d)
	except:
	    raise
	if not x:
	    env.failed('False expression: %s'%expression)
	return True
		       
class ExpressionSetFamily(SpecFamily):
    def __call__(self, expression, *names):
	func = None
	return self.Set(self, (names, expression, func))

    def c_test_contains(self, a, b, env):
	names, expression, func = a.arg
	func = self.specmod.eval('lambda %s:(%s)'%(','.join(('LE',)+tuple(names)), expression))
	d = {'LE':env.LE}
	for name in names:
	    x = env.getattr(b, name)
	    d[name] = x
	try:
	    x = func(**d)
	except:
	    raise
	return env.test_contains(x, b, 'expset(%s, %s)'%(expression, ','.join(names)))

class MatchesFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)
	self.sre = self.specmod._root.sre
	    
    def __call__(self, regexp):
	return self.specoargtup(self.sre.compile(regexp), (regexp,))

    def c_test_contains(self, a, b, env):
	regexpobj = a.arg
	m = self.sre.match(regexpobj, b)
	if m is None:
	    return env.failed('Did not match')
	return True

class RecurSelfFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)

	class RecurSpec(self.Set):
	    __slots__ = 'func', 'recursion_level', 'recursion_limit'

	self.RecurSpec = RecurSpec

    def __call__(self, expr, recursion_limit = 10):
	s = self.RecurSpec(self, expr)
	s.recursion_limit = recursion_limit
	s.recursion_level = 0
	return s

    def c_test_contains(self, a, b, env):
	try:
	    func = a.func
	except AttributeError:
	    expr = a.arg
	    func = a.func = env.eval('lambda self:%s'%expr)
	s = func(self.specmod.Nothing)
	try:
	    tf = env.test_contains(s, b, 'recur with Nothing, ok to fail')
	    if not tf:
		raise TestError
	except : # TestError: eg for match, we got a TypeError..
	    s = func(a)
	    rl = a.recursion_level
	    try:
		if rl >= a.recursion_limit:
		    return env.failed('recurself: recursion_level = %s'%a.recursion_limit)
		else:
		    a.recursion_level = rl + 1
		tf = env.test_contains(s, b, 'recur')
	    finally:
		a.recursion_level = rl
	return tf

class Dummy:
    pass

class TupleformFamily(SpecFamily):
    def __call__(self, form, set):
	return self.specotup((form, set))

    def c_test_contains(self, a, b, env):
	form, set = a.arg

	bt = tuple(b)

	if len(bt) != len(form):
	    return env.failed('tupleform: wrong length: got %d expected %d'%(len(bt), len(form)))

	ob = Dummy()
	for name, val in zip(form, bt):
	    setattr(ob, name, val)

	return env.test_contains(set, ob, 'tupleform')
	    

class Arrow:
    def __init__(self, category, source, target):
	self.category = category
	self.source = source
	self.target = target

    def of(self, other):
	# compose self <-- other 
	# (Standard composition order)
	other = self.category.validate(other)
	return self.category.compose(self, other)

    def to(self, other):
	# compose self --> other
	# (Nonstandard composition order; sometimes seems more natural)
	other = self.category.validate(other)
	return self.category.compose(other, self)

class IdentityArrow(Arrow):
    def __init__(self, category, object):
	Arrow.__init__(self, category, object, object)

    def __call__(self, x):
	return x

class FunctionArrow(Arrow):
    def __init__(self, category, source, target, function):
	Arrow.__init__(self, category, source, target)
	self.__call__ = function

class RepresentationCategory:
    _derive_origin_ = None
    _origin_ = None
    def __init__(self, mod, spec):
	fam = mod.family(RepresentationObjectFamily)
	fam.init2(self, spec)
	self._fam = fam

    def __eq__(self, other):
	return self is other

    def __hash__(self):
	return hash(id(self))

    def __getattr__(self, name):
	r = self._fam.getobject(name)
	self.__dict__[name] = r
	return r

class RepresentationObjectFamily(SpecFamily):
    def init2(self, cat, spec):
	self.cat = cat
	self.objects = {}
	self.specs = {}
	self.arrows = {}


	self.add_export('fromuniversal', self.fromuniversal)

	Set = self.Set
	class RepresentationObject(Set):
	    __slots__ = 'to', 'from'

	self.Set = RepresentationObject

	class RepresentationCategorySpec(spec):
	    def __init__(self, fam):
		self._fam = fam
		self._cat = fam.cat

	    def __getattr__(self, name):
		if hasattr(self.__class__, '_get_%s'%name):
		    r = getattr(self, '_get_%s'%name)(self._fam.specmod)
		    self.__dict__[name] = r
		    return r
		raise AttributeError, name

	self.spec = RepresentationCategorySpec(self)




    def getarrow(self, dom, cod):
	dc = (dom, cod)
	if dc in self.arrows:
	    return self.arrows[dc]

	raise SpecError

    def getobject(self, name):
	if name in self.objects:
	    return self.objects[name]
	normname = self.normoname(name)
	if normname in self.objects:
	    self.objects[name] = self.objects[normname]
	    return self.objects[normname]

	o = self(normname)
	self.objects[normname] = self.objects[name] = o
	return o

	raise SpecError, 'No such object: %r'%name

    def getspec(self, obj):
	name = obj.arg
	if name in self.specs:
	    return self.specs[name]
	
	gs = getattr(self.spec, '_get_spec_%s'%name, None)
	if gs is not None:
	    sp = gs(self.specmod)
	    self.specs[name] = sp
	    return sp

	raise SpecError, 'getspec: No spec of %r'%name

    def fromuniversal(self, target):
	# Find a most general arrow into 'target'
	# 1. Find all predefined arrows to target 
	# 2. Make a category sum of the set of sources S of all such arrows
	# 3. Make a specification-set P for this sum, which is that:
	#    a. The element should be isomorphic to a tuple (O, A) where
	#    b. O, the tag, should be an object in S
	#    c. A, the value,  should be an element in O

	# Return an arrow taking this object to target.
	#
	# Arrows thus created are memoized.

	name = target.arg
	arrowname = '%s.fromuniversal'%name
	if arrowname in self.arrows:
	    return self.arrows[arrowname]

	S = {}

	S[name] = IdentityArrow(self.cat, target)

	for an in dir(self.spec):
	    if not (an.startswith('map_') and '_to_' in an):
		continue
	    s, t = an.split('_to_')
	    s = s[4:]
	    if t == name:
		f = getattr(self.spec, an)
		S[s] = FunctionArrow(self.cat, getattr(self.cat, s), target,
				     lambda x: f(self.specmod, x))
		    
	def p(env, e):
	    try:
		O, A = e
	    except:
		return env.failed('Not a sequence with length 2')
	    fam = getattr(O, 'fam', None)
	    if fam is not self:
		return env.failed('Tag is not an object of this family')
	    name_ = getattr(O, 'arg', None)
	    if name_ not in S:
		return env.failed('Object is not a source of this target')
	    return env.test_contains(O, A, 'Value is not an element of this object')

	uniname = '%s.universal'%name
	P = self.specmod.predicate(p, 'Specification-set for %r'%uniname)
	self.specs[uniname] = P
	source = self(uniname)

	class AlphaSum(Arrow):
	    def __init__(self, category, source, target, S):
		Arrow.__init__(self, category, source, target)

		self._S = S

	    def __getitem__(self, x):	# Don't know what to call this unique arrow
		return self._S[self.source.fam.normoname(x)]

	    def __call__(self, (O, E)):
		return self[O.arg](E)
	    

	arrow = AlphaSum(self.cat, source, target, S)
	self.arrows[arrowname] = arrow
	return arrow

    def normoname(self, on):
	isos = getattr(self.spec, '_isos_', None)
	if isos is not None:
	    for l in self.spec._isos_:
		nn = None
		for n in l:
		    if n.isdigit():
			nn = n
		    if n == on:
			if nn is not None:
			    return nn
			raise SpecError, 'No numeric object name corresponding to %r'%on
	return on

    def __call__(self, name):
	r = self.specoarg(name)
	class To:
	    __slots__ = 'source',
	    def __init__(self, source):
		self.source = source
		
	    def __call__(self, target):
		return self.source.fam.getarrow(self.source, target)

	    def __getattr__(self, name):
		source = self.source
		fam = source.fam
		target = fam.getobject(name)
		return fam.getarrow(source, target)

	r.to = To(r)
	return r

    def c_test_contains(self, a, b, env):
	set = self.getspec(a)
	return env.test_contains(set, b, 'RepresentationObjectFamily: not in object specification')

    def c_get_examples(self, a, env):
	set = self.getspec(a)
	return env.get_examples(set)

class AbstractSetFamily(SpecFamily):
    def __init__(self, *a, **k):
	SpecFamily.__init__(self, *a, **k)
	class AbstractSet(self.Set):
	    __slots__ = '_memo',
	    def __init__(self, fam, arg):
		self.fam = fam
		self.arg = arg
		self._origin_ = None
		self._memo = {}
	self.Set = AbstractSet

    def __call__(self, arrow, set):
	r = self.specotup((arrow, set))
	r._memo = {}
	return r

    def c_and(self, a, b):
	if b.fam is self:
	    aa, sa = a.arg
	    ab, sb = b.arg
	    if aa is ab:
		return self(aa, sa & sb)
	return b.fam._rand_ATOM(b, a)

    def c_getattr2(self, a, b):
	if b in a._memo:
	    return a._memo[b]
	arrow, set = a.arg

	pararrow = arrow[b]
	srcset = pararrow.source

	def p(env, x):
	    t = env.test_contains(srcset, x, 'AbstractSet: not in arrow.source')
	    if t:
		e = pararrow(x)
		t = env.test_contains(set, e, 'AbstractSet: not in argument set')
	    return t

	    return env.contains(set, y)

	s = self.specmod.predicate(p, 'Abstract set attribute: %r'%b) #...
	a._memo[b] = s
	return s

    def c_test_contains(self, a, b, env):
	arrow, set = a.arg
	t = env.test_contains(arrow.source, b, 'AbstractSet: not in arrow.source')
	if t:
	    e = arrow(b)
	    t = env.test_contains(set, e, 'AbstractSet: not in argument set')
	return t
							  
class ElemFamily(SpecFamily):
    def __call__(self, func):
	return self.specoarg(func)

    def c_test_contains(self, a, b, env):
	func = a.arg
	s = func(b)
	return env.test_contains(s, b, 'ElemFamily')

class IntersectionFamily(SpecFamily):
    def __call__(self, domain, function):
	return self.specotup((domain, function))

    def c_test_contains(self, a, b, env):
	domain, function = a.arg
	return env.forall(domain, lambda env, x:
			  env.test_contains(function(x), b, 'Intersection'))
		   

class SpecError(Exception):
    pass

class TestError(Exception):
    pass

class CoverageError(Exception):
    pass



class LocalEnv:
    _derive_origin_ = 'ADD'
    def __init__(self, mod, spec, nodoc=1):
	self._mod = mod
	self._spec = spec
	self._origin_ = None
	self.nodoc = nodoc


    def __getattr__(self, attribute_name):
	mod = self._mod
	f = getattr(self._spec, attribute_name)
	d = self._mod._load_names(mod._root.guppy.etc.Code.co_findloadednames(f.func_code))
	nf = mod._root.new.function(
	    f.func_code,
	    d,
	    f.func_name,
	    f.func_defaults,
	    f.func_closure)
	r = nf(())
	self.__dict__[attribute_name] = r
	return r
			    

class TestEnv:
    _derive_origin_ = 'ADD'
    iscomplete = False
    issilent = False
    max_sequence_examples_length = 2	# ie. (), cprod(x) cprod(x, y) are yielded by default
    TestError = TestError
    def __init__(self, mod, Spec):
	self.mod = mod
	self.messages = []
	self.examples = {}
	if Spec is not None:
	    self.spec = spec = Spec()
	    try:
		lex = spec.LocalEnvExpr
	    except AttributeError:
		lex = ''
	    LE = LocalEnv(mod, lex)
	    LE._OBJ_ = mod
	    self.LE = LE

	    self.topspec = self.eval(spec.GlueTypeExpr)

    def eval(self, expr):
	mod = self.mod
	types = mod._root.types
	if isinstance(expr, types.StringTypes):
	    func = self.mod.eval('lambda LE:(\n%s\n)'%expr)
	    return func(self.LE)
	
	ls = []
	selfset = None
	#print 1

	names = expr.__dict__.keys()
	names.sort()

	for name in names:
	    f = getattr(expr, name)
	    try:
		co = f.func_code
	    except AttributeError:
		continue
	    if co.co_varnames[:co.co_argcount] == ('IN',):
		d = mod._load_names(mod._root.guppy.etc.Code.co_findloadednames(co))
		#d = mod._load_names()

		nf = mod._root.new.function(
		    f.func_code,
		    d,
		    f.func_name,
		    f.func_defaults,
		    f.func_closure)
		s = nf(())
		if name == '_SELF_':
		    selfset = s
		else:
		    ls.append(mod.attr(name, s))
	    else:
		raise SpecError, 'TestEnv.eval: invalid argument mode'
	# Constructing an AND in one sweep = faster
	# We assume they are not disjoint - which
	# would be determined by testing that we are going to do
	# (We know they are all attr's of different names here)

	# Except that selfset may perhaps be disjoint; but why care here
	#
	if selfset is not None:
	    ls.append(selfset)

	    # Alternatively: r = r & selfset afterwards,
	    # but could be unnecessarily slow

	#print 2
	r = mod.UniSet.fam_And._cons(ls)
	#print 3
	return r
		

    def get_examples(self, collection):
	try:
	    it = iter(collection)
	except TypeError:
	    try:
		ex = self.examples[collection]
	    except KeyError:
		if isinstance(collection, self.mod.UniSet.UniSet):
		    ex = collection.get_examples(self)
		else:
		    ex = list(collection)
	    it = iter(ex)
	return it

    def getattr(self, obj, name):
	if '.' in name:
	    x = obj
	    for subname in name.split('.'):
		try:
		    x = getattr(x, subname)
		except:
		    return self.failed('getattr: %s has no attribute %r'%(self.name(obj), name)+
				      ',\nbecause %s has no attribute %r'%(self.name(x), subname))
	else:
	    try:
		x = getattr(obj, name)
	    except:
		if DEBUG:
		    raise
		return self.failed('attr: %s has no attribute %r'%(self.name(obj), name))
	return x
	    
    def gengetattr(self, obj, name_or_tuple):
	if isinstance(name_or_tuple, str):
	    return self.getattr(obj, name_or_tuple)
	elif isinstance(name_or_tuple, tuple):
	    if len(name_or_tuple) == 2 and name_or_tuple[0] is self.mod.quote:
		return name_or_tuple[1]
	    else:
		return tuple([self.gengetattr(obj, nt) for nt in name_or_tuple])
	else:
	    raise TypeError, 'gengetattr: I am picky, required string or tuple'
	
    def log(self, message):
	self.messages.append(message)

    def name(self, obj):
	if isinstance(obj, self.mod.UniSet.UniSet):
	    return str(obj)
	else:
	    return '%s'%self.mod.iso(obj)

    def name_coll(self, collection):
	return '%s'%collection

    def test(self, obj):
	self.get_obj_examples(obj)
	try:
	    self.test_contains(self.topspec, obj, 'Top spec')
	except:
	    tvt = self.mod._root.sys.exc_info()
	    self.dump_failure(tvt)

    def get_obj_examples(self, obj):
	ex = self.spec.GetExamples(self, obj)
	for e in ex:
	    vs = e[1:]
	    e = e[0]
	    s = self.examples.setdefault(e, [])
	    for v in vs:
		s.append(v)
		self.test_contains(e, v, 'testing example of set')

	

    def dump_failure(self, (type, value, traceback), noraise=0):
	list = []
	tb = traceback
	while tb is not None:
	    f = tb.tb_frame
	    if f.f_code is self.test_contains.im_func.func_code:
		list.append(f)
	    tb = tb.tb_next
	for f in list:
	    lo = f.f_locals
	    print 'a = %r' % (lo['a'],)
	    print 'b = %r' % (lo['b'],)
	    print 'message = ', lo['message']
	    print '-----'
	if noraise:
	    self.mod._root.traceback.print_exception(type, value, traceback)
	else:
	    raise

    def contains(self, a, b):
	try:
	    x = self.test_contains(a, b, 'contains')
	except CoverageError:
	    raise
	except:
	    return False
	return x

    def test_contains(self, a, b, message):
	if 0:
	    try:
		a.test_contains(b, self)
	    except TestError:
		raise
		# return self.failed('test_contains, from: %s'% message)
	    return True
	else:
	    return a.test_contains(b, self)

    def test_contains_not(self, a, b, message):
	try:
	    a.test_contains(b, self)
	except CoverageError:
	    raise
	except:	# TestError: # well we axcept anything.. ok?
	    return True
	else:
	    return self.failed('test_contains_not, from: %s'%message)

    def failed(self, message=''):
	if not self.issilent:
	    self.log( 'Failed:' + message)
	    raise TestError, message
	return False

    def failed_coverage(self, forwhat, collection, func, message):
	if collection is self.mod.Nothing:
	    return True
	raise CoverageError, '%s: no examples for collection = %s, message: %s'%(forwhat, collection, message)

    def failed_exc_info(self, message):
	exc_info = self.mod._root.sys.exc_info()
	type, value, traceback = exc_info
	if not self.issilent:
	    self.log( 'Failed:' + message)
	    raise type, value
	return False

    def forall(self, collection, func, message=''):
	ex = self.get_examples(collection)
	n = 0
	for e in ex:
	    if not func(self, e):
		return self.failed('forall: e = %s, from: %s'%(self.name(e), message))
	    n += 1
	if not n:
	    try:
		a = len(collection)
		if a > 0:
		    raise CoverageError
		# Otherwise ok, it was really an Nothing collection.
	    except:
		self.failed_coverage('forall', collection, func, message)

	return True
	    
    def forall_pairs(self, collection, func, message=''):
	as_ = self.get_examples(collection)
	n = 0
	for a in as_:
	    for b in self.get_examples(collection):
		if not func(self, a, b):
		    self.failed('forall_pairs: a = %s, b = %s, from: %s'%(
			self.name(a), self.name(b), message))
		n += 1
	if not n:
	    self.failed_coverage('forall_pairs', collection, func, message)
	return True

    def forall_triples(self, collection, func, message=''):
	as_ = self.get_examples(collection)
	n = 0
	for a in as_:
	    for b in self.get_examples(collection):
		for c in self.get_examples(collection):
		    if not func(self, a, b, c):
			self.failed('forall_triples: a = %s, b = %s, c=%s, from: %s'%(
			    self.name(a), self.name(b), self.name(c), message))
		    n += 1
	if not n:
	    self.failed_coverage('forall_triples', collection, func, message)
	return True


    def forsome(self, collection, func, message=''):
	failures = []
	for i, x in enumerate(collection):
	    try:
		b = func(x)
	    except : # TestError:
		failures.append((i, self.mod._root.sys.exc_info()))
		continue
	    if b:
		return True
	for (i, tvt) in failures:
	    print 'forsome: exception at collection[%d]:'%i
	    self.dump_failure(tvt, noraise=1)
	self.failed(message)
	

class _GLUECLAMP_:

    _chgable_ = '_loaded',
    _nowrap_ = ('_origin_', 'Doc', 'family', 'eval', 'setcast', 'compile', 'wrap_source_string',
		'_load_names', 'iso')

    _preload_ = '_hiding_tag_',

    # 'imports'

    _imports_ = (
	'_parent:Use',
	'_parent.Use:iso',
	'_parent.Use:Nothing',
	)

    def _get_AbstractAlgebra(self):	return self._parent.AbstractAlgebra
    def _get_UniSet(self):		return self._parent.UniSet
    def _get_Doc(self):			return self._parent.Doc
    def _get_View(self):		return self._parent.View

    #

    def _get__origin_(self):
	return self.Doc.attribute(self.Doc.root, 'guppy.heapy.Spec')	

    def _wrapattr_(self, obj, name):
	Doc = self.Doc
	if name == 'setof':
	    pass
	    #pdb.set_trace()
	try:
	    obj = Doc.wrap(obj, Doc.attribute(self._origin_, name))
	except Doc.DocError:
	    print 'no wrap:', name
	return obj

    def _get_AA(self):
	return self.AbstractAlgebra

    def _get_abstractset(self):
	return self.family(AbstractSetFamily)

    def _get_adaptuple(self):
	return self.family(AdaptupleFamily)

    def _get_any(self):
	return ~self.Nothing

    def _get_argnames(self):
	return self.family(ArgNamesFamily)

    def _get_attr(self):
	return self.family(AttributeFamily)

    def attrs(self, names, type=None):
	x = self.any
	for n in names:
	    x &= self.attr(n, type)
	return x

    def _get_boolean(self):
	def p(env, x):
	    try:
		if x:
		    pass
	    except:
		env.failed("boolean: 'if x' raised an exception")
	    return True
	return self.predicate(p, 'boolean')


    def _get_callable(self):
	return self.predicate(lambda env, x:callable(x), 'callable')

    def _get_compile(self):
	token = self._root.token
	parser = self._root.parser
	symbol = self._root.symbol

	def mapchildren_id(node, f):
	    return node

	def mapchildren_default(node, f):
	    return [node[0]] + [f(n) for n in node[1:]]

	mapchildren_dispatch = dict([(value, mapchildren_id) for value in range(token.N_TOKENS)])

	mapchildren_dispatch.update(dict([(value, mapchildren_default)
				     for value, name in symbol.sym_name.items()]))

	def mapchildren(node, f):
	    return mapchildren_dispatch[node[0]](node, f)

	def visitor(C):
	    d = mapchildren_dispatch.copy()
	    for value, name in symbol.sym_name.items():
		if hasattr(C, name):
		    d[value] = getattr(C, name).im_func
	    _visit = lambda node: d[node[0]](node, _visit)
	    return _visit

	def recover_source_node(node, l):
	    for n in node[1:]:
		recover_source_dispatch[n[0]] (n, l)

	def recover_source_token(node, l):
	    if l and l[-1] != '(':
		l.append(' ')
	    l.append(node[1])

	def recover_source_name(node, l):
	    if l and l[-1] not in ('.', '('):
		l.append(' ')
	    l.append(node[1])

	    
	def recover_source_tight_left(node, l):
	    l.append(node[1])

	def recover_source_lpar(node, l):
	    if l and not (l[-1][-1:].isalnum() or l[-1] == '('):
		l.append(' ')
	    l.append(node[1])


	recover_source_dispatch = dict([(value, recover_source_node)
				     for value, name in symbol.sym_name.items()])
	recover_source_dispatch.update(
	    dict([(value, recover_source_token) for value in range(token.N_TOKENS)]))

	recover_source_dispatch[token.NAME] = recover_source_name

	for tok in ('RPAR', 'LSQB', 'RSQB', 'COLON', 'COMMA', 'SEMI',
		    'DOT', 'LBRACE', 'RBRACE'):
	    recover_source_dispatch[getattr(token, tok)] = recover_source_tight_left

	recover_source_dispatch[token.LPAR] = recover_source_lpar


	def recover_source(node):
	    l = []
	    recover_source_dispatch[node[0]] (node, l)
	    return ''.join(l)

	class wrap_lambdef:
	    def test(node, f):
		# and_test ('or' and_test)* | lambdef
		if len(node) == 2 and node[1][0] == symbol.lambdef:
		    lsource = recover_source(node[1])
		    lnode = mapchildren(node[1], f)

		    return (
			292, (293, (294, (295, (297, (298, (299, (300, (301,
			(302, (303, (304, (305, (1, 'wrap_source_string')),
			(308, (7, '('),	(317, (318, (292, lnode)), (12, ','),
			(318, (292, (293, (294, (295, (297, (298, (299, (300,
			(301, (302, (303, (304, (305, (3, '%r'%lsource
			)))))))))))))))), (8, ')'))))))))))))))


		return mapchildren(node, f)

	wrap_lambdef = visitor(wrap_lambdef)

	def compile_(source, filename, mode, *args):
	    if mode != 'spec':
		return compile(source, filename, mode, *args)
	    ast = parser.expr(source)
	    node = parser.ast2tuple(ast, line_info=1)
	    node = mapchildren(node, wrap_lambdef)

	    ast = parser.tuple2ast(node)
	
	    co = parser.compileast(ast)
	    return co

	return compile_

    def _get_cprod(self):
	return self.family(CartesianProductFamily)

    def dictof(self, set=None):
	return self.UniSet.byclodo.dictof(set)

    def _get_doc(self):
	return self.family(DocFamily)

    def docof(self, set):
	doc = (set.doc % self._origin_).shortest()
	do = str(doc)
	print do
	return do

    def eval(self, expr, init=None, nodoc=0):
	if nodoc:
	    mode = 'eval'
	else:
	    mode = 'spec'
	co = self.compile(expr, '', mode)


	d = self._load_names(self._root.guppy.etc.Code.co_findloadednames(co))
	if init is not None:
	    d = d.copy()
	    exec init in d
	    

	return eval(co, d)
	
    def _get_all_names(self):
	names = {'_root':1}
	for x in _GLUECLAMP_.__dict__:
	    # print 'x', x
	    if x.startswith('_get_'):
		x = x[5:]
	    names[x] = 1
	return names
	

    def _load_names(self, names = None):
	if names is None:
	    if '_loaded' not in self.__dict__:
		for x in self.all_names:
		    getattr(self, x)
		self._loaded = 1
	else:
	    all = self.all_names
	    for name in names:
		if name in all:
		    getattr(self, name)
	d = self.__dict__
	d['__builtins__'] = self._load_names.func_globals['__builtins__']
	return d

	

    def _get_eg(self):
	return self.family(ExampleFamily)

    def _get_elem(self):
	return self.family(ElemFamily)

    def _exodoc(self, expr):
	if expr in self.LE.string:
	    r = self.eval(expr)
	    return r, self.Doc.anon(expr)
	elif (expr in self.Type.Function and
	      expr.func_code.co_name == '<lambda>' and
	      expr.func_code.co_filename.startswith('<!SPECEVAL!>')):
	      fn = expr.func_code.co_filename
	      lines = fn.split('\n')
	      lnum = expr.func_code.co_firstlineno
	      inspect = self._root.inspect
	      print lines[lnum:]
	      block = inspect.getblock(lines[lnum:])
	      source = '\n'.join(block)
	      return expr, self.Doc.getdoc(source)
	      
	    
	else:
	    return expr, self.Doc.getdoc(expr)
	    

    def _get_expred(self):
	return self.family(ExpressionPredicateFamily)

    def _get_expression(self):
	def p(env, x):
	    try:
		eval( 'lambda : %s'%x )
	    except SyntaxError:
		env.failed('Not a valid expression: %r'%x)
	    return True
	return self.predicate(p, 'expression')

    def _get_expset(self):
	return self.family(ExpressionSetFamily)

    def _get_equals(self):
	return self.family(EqualsFamily)

    def family(self, fam, *args, **kwds):
	return self.UniSet.fam_mixin_argatom(fam, self, *args, **kwds)

    def _get__hiding_tag_(self):
	return self.UniSet._hiding_tag_

    def _get_instance(self):
	return self.family(InstanceFamily)

    def _get_intersection(self):
	return self.family(IntersectionFamily)

    def _get_LE(self):
	return LocalEnv(self, self._Specification_.LocalEnvExpr)

    def _get_SPLE(self):
	return self.LE


    def _get_mapping(self):
	return self.family(MappingFamily)

    def _get_matches(self):
	return self.family(MatchesFamily)

    def mkTestEnv(self, Spec):
	return TestEnv(self, Spec)

    def newtype(self, name):
	return self.predicate(lambda e, x: 1, name) # xxx new family? 

    def _get_nothing(self):
	return self.Use.Nothing
	
    def partition(self, set):
	return self.doc('partition',
			self.union_equals(set) &
			self.LE.nonempty &
			self.set_of_disjoint_sets
			)

    def _get_predicate(self):
	return self.family(PredicateFamily)

    def _get_powerset(self):
	return self.family(PowersetFamily)

    def _get_Anything(self):
	return self.UniSet.Anything

    def _get_quote(self):
	return []

    def _get_recurself(self):
	return self.family(RecurSelfFamily)

    def _get_relation(self):
	# relation is a representation category
	# We have the following representation objects:
	# 1. set of pairs with attribute dom, cod
	# 2. set of pairs with dom is cod
	# 3. fuop = func | op, string in ('==',..)
	# 4. (A, fuop), where A is a set
	# 5. (A, fuop, B), where A and B are sets
	#
	# A final object is 1.
	class RelationSpec:
	    _isos_ = [
		('1', 'paxb'),
		('2', 'paxa'), 
		('3', 'defiop', 'fuop', ),
		('4', 'defipair'),
		('5', 'defitriple'),
		]
		 
	    def _get_spec_1(self, e):
		return e.setof(e.cprod(e.Anything, e.Anything))
		
	    def _get_spec_2(self, e):
		return (e.setof(e.cprod(e.Anything, e.Anything)))

	    def _get_spec_3(self, e):
		return (e.boolean << (e.Anything, e.Anything) |
			e.equals('<', '<=', '==', '!=', '>', '>=', 'in', 'not in', 'is', 'is not'))
			
	    def _get_spec_4(self, e):
		return e.cprod(e.set, self._cat.fuop)
		
	    def _get_spec_5(self, e):
		return e.cprod(e.set, self._cat.fuop, e.set)
		
	    def _get__relop(self, e):
		return e.family(RelOpFamily)

	    map_2_to_1 = id
	    def map_3_to_4(self, e, fuop):	return (e.Anything, fuop)
	    def map_3_to_2(self, e, fuop):	return self._relop(e.Anything, fuop) # redundant
	    def map_4_to_2(self, e, (A, fuop)):	return self._relop(A, fuop)
	    def map_5_to_1(self, e, (A,fuop,B)):return self._relop(A, fuop, B)

	return self.repcat(RelationSpec)

    def _get_relop(self):
	return self.relation.defiop.to.paxa

    def repcat(self, spec):
	return RepresentationCategory(self, spec)

    def _get_sequence(self):
	return self.family(SequenceFamily)

    def _get_set(self):
	return self.instance(self.UniSet.UniSet)

    def _get_set_of_disjoint_sets(self):
	def p(env, x):
	    return env.forall_pairs(x, lambda env, a, b: a == b or a.disjoint(b),
				    'a == b or a.disjoint(b)')
	return self.predicate(p, 'set of disjoint sets')

    def setcast(self, arg):
	if not isinstance(arg, self.UniSet.UniSet):
	    arg = self.UniSet.convert(arg)
	    arg = self.Doc.wrap(arg, self.Doc.callfunc(
		self.Doc.attribute(self._origin_, 'setcast'),
		arg))
	return arg

    def _get_setof(self):
	return self.powerset

    def _get__static_test_env(self):
	return self.mkTestEnv(None)

    def _get_synonyms(self):
	return self.family(SynonymsFamily)

    def _get_tupleform(self):
	return self.family(TupleformFamily)

    def _get_Type(self):
	return self.Use.Type

    def union_equals(self, set):
	return self.eg(self.attr('union', self.equals(set)),
		  self.powerset(set))

    def wrap_source_string(self, func, str):
	func._origin_ = self.Doc.source(str)
	return func
Name	Size	Permission
test	---	0755
AbstractAlgebra.py	22134 bytes	0644
AbstractAlgebra.pyc	40919 bytes	0644
AbstractAlgebra.pyo	40791 bytes	0644
Classifiers.py	39160 bytes	0644
Classifiers.pyc	73221 bytes	0644
Classifiers.pyo	73166 bytes	0644
Console.py	777 bytes	0644
Console.pyc	1514 bytes	0644
Console.pyo	1514 bytes	0644
Doc.py	6806 bytes	0644
Doc.pyc	17489 bytes	0644
Doc.pyo	17489 bytes	0644
ImpSet.py	957 bytes	0644
ImpSet.pyc	2273 bytes	0644
ImpSet.pyo	2273 bytes	0644
Monitor.py	12734 bytes	0644
Monitor.pyc	17974 bytes	0644
Monitor.pyo	17943 bytes	0644
OutputHandling.py	6844 bytes	0644
OutputHandling.pyc	13473 bytes	0644
OutputHandling.pyo	13473 bytes	0644
Part.py	19486 bytes	0644
Part.pyc	28552 bytes	0644
Part.pyo	28386 bytes	0644
Path.py	12910 bytes	0644
Path.pyc	25449 bytes	0644
Path.pyo	25322 bytes	0644
Prof.py	75689 bytes	0644
Prof.pyc	94077 bytes	0644
Prof.pyo	93907 bytes	0644
RM.py	121 bytes	0644
RM.pyc	222 bytes	0644
RM.pyo	222 bytes	0644
RefPat.py	15016 bytes	0644
RefPat.pyc	22807 bytes	0644
RefPat.pyo	22762 bytes	0644
Remote.py	13529 bytes	0644
Remote.pyc	15742 bytes	0644
Remote.pyo	15742 bytes	0644
RemoteConstants.py	210 bytes	0644
RemoteConstants.pyc	341 bytes	0644
RemoteConstants.pyo	341 bytes	0644
Spec.py	40799 bytes	0644
Spec.pyc	75720 bytes	0644
Spec.pyo	75720 bytes	0644
Target.py	118 bytes	0644
Target.pyc	678 bytes	0644
Target.pyo	678 bytes	0644
UniSet.py	59374 bytes	0644
UniSet.pyc	103523 bytes	0644
UniSet.pyo	103391 bytes	0644
Use.py	21055 bytes	0644
Use.pyc	23879 bytes	0644
Use.pyo	23879 bytes	0644
View.py	15803 bytes	0644
View.pyc	21390 bytes	0644
View.pyo	21390 bytes	0644
__init__.py	862 bytes	0644
__init__.pyc	827 bytes	0644
__init__.pyo	827 bytes	0644
heapyc.so	126808 bytes	0755
pbhelp.py	15757 bytes	0644
pbhelp.pyc	14048 bytes	0644
pbhelp.pyo	14048 bytes	0644
File Content: Spec.py

File Content: `Spec.py`
