# Path: etb/terms.py
# def mk_subst(**bindings):
#     """Named arguments constructor for substitutions. It builds
#     terms from its named arguments.
# 
#     >>> mk_subst(X=mk_numberconst(42), Y=mk_array([mk_numberconst(1),mk_numberconst(2),mk_numberconst(3)]))
#     subst(X = 42, Y = [1, 2, 3])
#     """
#     term_bindings = dict((mk_var(k), v) for k, v in bindings.iteritems())
#     return Subst(term_bindings)
# 
# def mk_map(entries):
#     """
#     Make a map from the given pairs. Pairs are converted to
#     pairs of terms if needed.
#     """
#     if isinstance(entries, Map):
#         return entries.hashcons()
#     else:
#         t = Map(entries)
#         return t.hashcons()
# 
# def mk_stringconst(val):
#     """
#     Make a string constant term out of the given value
#     :parameters:
#     - `val`: a basestring or a StringConst
#     :returntype:
#     - a hashconsed `StringConst` instance
#     """
#     if isinstance(val, StringConst):
#         return val.hashcons()
#     else:
#         t = StringConst(val)
#         return t.hashcons()
# 
# def mk_literal(pred, args):
#     """
#     Makes a literal from pred (a string) and args (a list or tuple of terms)
#     """
#     l = Literal(pred, args)
#     return l.hashcons()
# 
# def mk_idconst(val):
#     """
#     Make an id constant term out of the given string value.
#     :parameters:
#     - `val`: a basestring or an IdConst
#     :returntype:
#     - a hashconsed `IdConst` instance
#     """
#     if isinstance(val, IdConst):
#         return val.hashcons()
#     else:
#         t = IdConst(val)
#         return t.hashcons()


from etb_manager import ETBNetwork
from etb_tests import etb_test, ETBTest
from etb.terms import mk_subst, mk_map, mk_stringconst, mk_literal, mk_idconst
import os


class FileTest(ETBTest):

    @etb_test
    def find_thms(self):
        file = self.etb.put_file(os.path.abspath('short.sal'), 'short.sal')
        q = 'find_theorems(%s, ThmFile)' % file
        query = self.etb.etb().query(q)
        self.etb.etb().query_wait(query)
        return(self.etb.query_answers(query),

# Path: etb/terms.py
# def mk_subst(**bindings):
#     """Named arguments constructor for substitutions. It builds
#     terms from its named arguments.
# 
#     >>> mk_subst(X=mk_numberconst(42), Y=mk_array([mk_numberconst(1),mk_numberconst(2),mk_numberconst(3)]))
#     subst(X = 42, Y = [1, 2, 3])
#     """
#     term_bindings = dict((mk_var(k), v) for k, v in bindings.iteritems())
#     return Subst(term_bindings)
# 
# def mk_map(entries):
#     """
#     Make a map from the given pairs. Pairs are converted to
#     pairs of terms if needed.
#     """
#     if isinstance(entries, Map):
#         return entries.hashcons()
#     else:
#         t = Map(entries)
#         return t.hashcons()
# 
# def mk_stringconst(val):
#     """
#     Make a string constant term out of the given value
#     :parameters:
#     - `val`: a basestring or a StringConst
#     :returntype:
#     - a hashconsed `StringConst` instance
#     """
#     if isinstance(val, StringConst):
#         return val.hashcons()
#     else:
#         t = StringConst(val)
#         return t.hashcons()
# 
# def mk_literal(pred, args):
#     """
#     Makes a literal from pred (a string) and args (a list or tuple of terms)
#     """
#     l = Literal(pred, args)
#     return l.hashcons()
# 
# def mk_idconst(val):
#     """
#     Make an id constant term out of the given string value.
#     :parameters:
#     - `val`: a basestring or an IdConst
#     :returntype:
#     - a hashconsed `IdConst` instance
#     """
#     if isinstance(val, IdConst):
#         return val.hashcons()
#     else:
#         t = IdConst(val)
#         return t.hashcons()


# Path: tests/files.py
from etb_manager import ETBNetwork
from etb_tests import etb_test, ETBTest
from etb.terms import mk_subst, mk_map, mk_stringconst, mk_literal, mk_idconst
import os



class FileTest(ETBTest):

    @etb_test
    def find_thms(self):
        file = self.etb.put_file(os.path.abspath('short.sal'), 'short.sal')
        q = 'find_theorems(%s, ThmFile)' % file
        query = self.etb.etb().query(q)
        self.etb.etb().query_wait(query)
        return(self.etb.query_answers(query),

               [mk_subst(ThmFile = mk_map({"file": mk_stringconst("theorems"), "sha1": mk_stringconst("263cfc9907a248d65f98e9b0e3020e2045d4eccb")}))])