зеркало из https://github.com/microsoft/ivy.git
working on named
This commit is contained in:
Ken McMillan
Родитель
fe9c6fb64f
Коммит
00f13ae469
|
|
@ -515,6 +515,12 @@ class ProofDecl(Decl):
|
|||
def name(self):
|
||||
return 'proof'
|
||||
|
||||
class NamedDecl(Decl):
|
||||
def name(self):
|
||||
return 'named'
|
||||
def defines(self):
|
||||
return [(c.rep,lineno(c)) for c in self.args]
|
||||
|
||||
class SchemaDecl(Decl):
|
||||
def name(self):
|
||||
return 'schema'
|
||||
|
|
|
|||
|
|
@ -95,6 +95,8 @@ def check_module():
|
|||
|
||||
missing = []
|
||||
|
||||
for x,y in im.module.isolates.iteritems():
|
||||
print 'isolate= {}:{} '.format(x,y)
|
||||
isolate = ivy_compiler.isolate.get()
|
||||
if isolate != None:
|
||||
isolates = [isolate]
|
||||
|
|
|
|||
|
|
@ -549,9 +549,10 @@ def compile_schema_prem(self,sig):
|
|||
def compile_schema_conc(self,sig):
|
||||
iu.dbg('type(self)')
|
||||
iu.dbg('self')
|
||||
if isinstance(self,ivy_ast.Definition):
|
||||
with ivy_logic.WithSymbols(sig.all_symbols()):
|
||||
with ivy_logic.WithSymbols(sig.all_symbols()):
|
||||
if isinstance(self,ivy_ast.Definition):
|
||||
return compile_defn(self)
|
||||
return sortify_with_inference(self)
|
||||
|
||||
def compile_schema_body(self):
|
||||
sig = ivy_logic.Sig()
|
||||
|
|
@ -594,7 +595,42 @@ class IvyDomainSetup(IvyDeclInterp):
|
|||
def axiom(self,ax):
|
||||
self.domain.labeled_axioms.append(ax.compile())
|
||||
def property(self,ax):
|
||||
self.domain.labeled_props.append(ax.compile())
|
||||
lf = ax.compile()
|
||||
self.domain.labeled_props.append(lf)
|
||||
self.last_fact = lf
|
||||
def named(self,lhs):
|
||||
cond = ivy_logic.drop_universals(self.last_fact.formula)
|
||||
if not ivy_logic.is_exists(cond) or len(cond.variables) != 1:
|
||||
raise IvyError(lhs,'property is not existential')
|
||||
rng = list(cond.variables)[0].sort
|
||||
vmap = dict((x.name,x) for x in lu.variables_ast(cond))
|
||||
used = set()
|
||||
print 'foo!'
|
||||
iu.dbg('lhs.args[0].sort')
|
||||
with ivy_logic.UnsortedContext():
|
||||
args = [arg.compile() for arg in lhs.args]
|
||||
print 'bar!'
|
||||
targs = []
|
||||
for a in args:
|
||||
if a.name in used:
|
||||
raise IvyError(lhs,'repeat parameter: {}'.format(a.name))
|
||||
used.add(a.name)
|
||||
if a.name in vmap:
|
||||
v = vmap[a.name]
|
||||
targs.append(v)
|
||||
if not (ivy_logic.is_topsort(a.sort) or a.sort != v.sort):
|
||||
raise IvyError(lhs,'bad sort for {}'.format(a.name))
|
||||
else:
|
||||
if ivy_logic.is_topsort(a.sort):
|
||||
raise IvyError(lhs,'cannot infer sort for {}'.format(a.name))
|
||||
targs.append(a)
|
||||
for x in vmap:
|
||||
if x not in used:
|
||||
raise IvyError(lhs,'{} must be a parameter of {}'.format(x,lhs.rep))
|
||||
dom = [x.sort for x in targs]
|
||||
sym = self.domain.sig.add_symbol(lhs.rep,ivy_logic.FuncConstSort(*(dom+[rng])))
|
||||
iu.dbg('repr(sym)')
|
||||
self.domain.named.append((self.last_fact,sym(*targs) if targs else sym))
|
||||
def schema(self,sch):
|
||||
if isinstance(sch.defn.args[1],ivy_ast.SchemaBody):
|
||||
self.domain.schemata[sch.defn.defines()] = sch.defn.args[1].compile()
|
||||
|
|
@ -1024,7 +1060,30 @@ def check_definitions(mod):
|
|||
raise iu.IvyError(d,'definition of {} requires an recursion schema'.format(d.formula.defines()))
|
||||
prover.admit_definition(d,pmap[d.id])
|
||||
|
||||
|
||||
def check_properties(mod):
|
||||
props = mod.labeled_props
|
||||
mod.labeled_props = []
|
||||
pmap = dict((lf.id,p) for lf,p in mod.proofs)
|
||||
nmap = dict((lf.id,n) for lf,n in mod.named)
|
||||
import ivy_proof
|
||||
prover = ivy_proof.ProofChecker([],[],mod.schemata)
|
||||
for prop in props:
|
||||
if prop.id in pmap:
|
||||
print 'checking {}...'.format(prop.label)
|
||||
prover.admit_proposition(prop,pmap[prop.id])
|
||||
if prop.id in nmap:
|
||||
name = nmap[prop.id]
|
||||
fmla = ivy_logic.drop_universals(prop.formula)
|
||||
v = list(fmla.variables)[0]
|
||||
fmla = fmla.body
|
||||
iu.dbg('v.sort')
|
||||
iu.dbg('name.sort')
|
||||
fmla = lu.substitute_ast(fmla,{v.name:name})
|
||||
iu.dbg('fmla')
|
||||
prop = prop.clone([prop.label,fmla])
|
||||
mod.labeled_axioms.append(prop)
|
||||
else:
|
||||
mod.labeled_props.append(prop)
|
||||
|
||||
|
||||
def ivy_compile(decls,mod=None,create_isolate=True,**kwargs):
|
||||
|
|
@ -1057,6 +1116,7 @@ def ivy_compile(decls,mod=None,create_isolate=True,**kwargs):
|
|||
|
||||
create_sort_order(mod)
|
||||
check_definitions(mod)
|
||||
check_properties(mod)
|
||||
if create_isolate:
|
||||
iso.create_isolate(isolate.get(),mod,**kwargs)
|
||||
im.module.labeled_axioms.extend(im.module.labeled_props)
|
||||
|
|
|
|||
|
|
@ -119,6 +119,7 @@ reserved = all_reserved = {
|
|||
'of' : 'OF',
|
||||
'scenario' : 'SCENARIO',
|
||||
'proof' : 'PROOF',
|
||||
'named' : 'NAMED',
|
||||
}
|
||||
|
||||
tokens += tuple(all_reserved.values())
|
||||
|
|
|
|||
|
|
@ -154,6 +154,7 @@ Symbol.is_relation = lambda self: isinstance(self.sort.rng,lg.BooleanSort)
|
|||
Symbol.args = property(lambda self : [])
|
||||
Symbol.is_numeral = lambda self : is_numeral_name(self.name)
|
||||
Symbol.clone = lambda self,args : self
|
||||
Symbol.resort = lambda self,sort : Symbol(self.name,sort)
|
||||
|
||||
BooleanSort = lg.BooleanSort
|
||||
|
||||
|
|
@ -668,6 +669,9 @@ def is_boolean(term):
|
|||
def is_first_order_sort(s):
|
||||
return isinstance(s,UninterpretedSort)
|
||||
|
||||
def FuncConstSort(*sorts):
|
||||
return FunctionSort(*sorts) if len(sorts) > 1 else sorts[0]
|
||||
|
||||
def RelationSort(dom):
|
||||
return FunctionSort(*(list(dom) + [lg.Boolean])) if len(dom) else lg.Boolean
|
||||
|
||||
|
|
@ -682,6 +686,9 @@ TopS = lg.TopS
|
|||
def apply(symbol,args):
|
||||
return App(symbol,*args)
|
||||
|
||||
def is_topsort(sort):
|
||||
return isinstance(sort,lg.TopSort)
|
||||
|
||||
def sortify(ast):
|
||||
args = [sortify(arg) for arg in ast.args]
|
||||
if (isinstance(ast,App)) and isinstance(ast.rep.sort,lg.TopSort):
|
||||
|
|
|
|||
|
|
@ -264,7 +264,7 @@ def variables_ast(ast):
|
|||
|
||||
# extend to clauses, etc...
|
||||
|
||||
variables_clause = variables_cube = apply_gen_to_list(variables_ast)
|
||||
variables_clause = variables_cube = used_variables_asts = apply_gen_to_list(variables_ast)
|
||||
variables_clauses = variables_cubes = apply_gen_to_clauses(variables_ast)
|
||||
|
||||
# get set of variables occurring
|
||||
|
|
@ -950,10 +950,10 @@ def variables_distinct_ast(ast1,ast2):
|
|||
map1 = distinct_variable_renaming(used_variables_ast(ast1),used_variables_ast(ast2))
|
||||
return substitute_ast(ast1,map1)
|
||||
|
||||
def rename_variables_distinct_ast(vars,ast2):
|
||||
""" rename variables in vars so they don't occur in ast2.
|
||||
def rename_variables_distinct_asts(vars,asts):
|
||||
""" rename variables in vars so they don't occur in asts.
|
||||
"""
|
||||
map1 = distinct_variable_renaming(vars,used_variables_ast(ast2))
|
||||
map1 = distinct_variable_renaming(vars,used_variables_asts(asts))
|
||||
return [map1[v.name] for v in vars]
|
||||
|
||||
def variables_distinct_list_ast(ast_list,ast2):
|
||||
|
|
|
|||
|
|
@ -70,6 +70,7 @@ class Module(object):
|
|||
self.variants = defaultdict(list) # map from sort name to list of sort
|
||||
self.ext_preconds = {} # map from action name to formula
|
||||
self.proofs = [] # list of pair (labeled formula, proof)
|
||||
self.named = [] # list of pair (labeled formula, atom)
|
||||
|
||||
self.sig = il.sig.copy() # capture the current signature
|
||||
|
||||
|
|
|
|||
|
|
@ -234,12 +234,25 @@ def p_top_axiom_labeledfmla(p):
|
|||
d.lineno = get_lineno(p,2)
|
||||
p[0].declare(d)
|
||||
|
||||
def p_optskolem(p):
|
||||
'optskolem : '
|
||||
p[0] = None
|
||||
|
||||
def p_optskolem_symbol(p):
|
||||
'optskolem : NAMED defnlhs'
|
||||
p[0] = p[2]
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
def p_top_property_labeledfmla(p):
|
||||
'top : top PROPERTY labeledfmla'
|
||||
'top : top PROPERTY labeledfmla optskolem optproof'
|
||||
p[0] = p[1]
|
||||
d = PropertyDecl(p[3])
|
||||
d.lineno = get_lineno(p,2)
|
||||
p[0].declare(d)
|
||||
if p[4] is not None:
|
||||
p[0].declare(NamedDecl(p[4]))
|
||||
if p[5] is not None:
|
||||
p[0].declare(ProofDecl(p[5]))
|
||||
|
||||
def p_top_conjecture_labeledfmla(p):
|
||||
'top : top CONJECTURE labeledfmla'
|
||||
|
|
@ -334,6 +347,10 @@ def p_schconc_defdecl(p):
|
|||
'schconc : DEFINITION defn'
|
||||
p[0] = p[2]
|
||||
|
||||
def p_schconc_propdecl(p):
|
||||
'schconc : PROPERTY fmla'
|
||||
p[0] = p[2]
|
||||
|
||||
def p_schdecls(p):
|
||||
'schdecls :'
|
||||
p[0] = []
|
||||
|
|
@ -1394,7 +1411,7 @@ def p_callatom_atom(p):
|
|||
if not (iu.get_numeric_version() <= [1,5]):
|
||||
def p_callatom_this(p):
|
||||
'callatom : THIS'
|
||||
p[0] = This()
|
||||
p[0] = Atom(This())
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
|
||||
|
|
|
|||
244
ivy/ivy_proof.py
244
ivy/ivy_proof.py
|
|
@ -16,6 +16,12 @@ class NoMatch(iu.IvyError):
|
|||
class ProofError(iu.IvyError):
|
||||
pass
|
||||
|
||||
class MatchProblem(object):
|
||||
def __init__(self,pat,inst,freesyms,constants):
|
||||
self.pat,self.inst,self.freesyms,self.constants = pat,inst,freesyms,constants
|
||||
def __str__(self):
|
||||
return '{{pat:{},inst:{},freesyms:{}}}'.format(self.pat,self.inst,map(str,self.freesyms))
|
||||
|
||||
class ProofChecker(object):
|
||||
""" This is IVY's built-in proof checker """
|
||||
|
||||
|
|
@ -55,6 +61,20 @@ class ProofChecker(object):
|
|||
raise NoMatch(defn,"recursive definition does not match the given schema")
|
||||
self.definitions[sym] = defn
|
||||
|
||||
def admit_proposition(self,prop,proof=None):
|
||||
""" Admits a proposition with proof. If a proof is given it
|
||||
is used to match the definition to a schema, else default
|
||||
heuristic matching is used.
|
||||
|
||||
- prop is an ivy_ast.LabeledFormula
|
||||
"""
|
||||
|
||||
if proof is None:
|
||||
raise NoMatch(prop,"no proof given for property")
|
||||
if self.match_schema(prop.formula,proof) is None:
|
||||
raise NoMatch(proof,"goal does not match the given schema")
|
||||
self.axioms.append(prop)
|
||||
|
||||
def match_schema(self,decl,proof):
|
||||
""" attempt to match a definition or property decl to a schema
|
||||
|
||||
|
|
@ -68,60 +88,119 @@ class ProofChecker(object):
|
|||
if schemaname not in self.schemata:
|
||||
raise ProofError(proof,"No schema {} exists".format(schemaname))
|
||||
schema = self.schemata[schemaname]
|
||||
conc = schema.conc()
|
||||
if type(conc) is not type(decl):
|
||||
iu.dbg('type(conc)')
|
||||
iu.dbg('type(decl)')
|
||||
return None
|
||||
freesyms = set(x.args[0] for x in schema.prems() if isinstance(x,ia.ConstantDecl))
|
||||
freesyms.update(x for x in schema.prems() if isinstance(x,il.UninterpretedSort))
|
||||
if isinstance(decl,il.Definition):
|
||||
declsym = decl.defines()
|
||||
concsym = conc.defines()
|
||||
declargs = decl.lhs().args
|
||||
concargs = conc.lhs().args
|
||||
if len(declargs) != len(concargs):
|
||||
return None
|
||||
declrhs = decl.rhs()
|
||||
concrhs = conc.rhs()
|
||||
vmap = dict((x.name,il.Variable(y.name,x.sort)) for x,y in zip(concargs,declargs))
|
||||
concrhs = lu.substitute_ast(concrhs,vmap)
|
||||
dmatch = {concsym:declsym}
|
||||
for x,y in zip(func_sorts(concsym),func_sorts(declsym)):
|
||||
if x in freesyms:
|
||||
if x in dmatch and dmatch[x] != y:
|
||||
print "lhs sorts didn't match"
|
||||
return None
|
||||
dmatch[x] = y
|
||||
else:
|
||||
if x != y:
|
||||
print "lhs sorts didn't match"
|
||||
return None
|
||||
concrhs = apply_match(dmatch,concrhs)
|
||||
iu.dbg('concrhs')
|
||||
inst = declrhs
|
||||
pat = concrhs
|
||||
else:
|
||||
raise ProofError(proof,"Property schemata not supported yet")
|
||||
pmatch = compile_match(proof,freesyms,schemaname)
|
||||
iu.dbg('pmatch')
|
||||
pat = apply_match(pmatch,pat)
|
||||
iu.dbg('pat')
|
||||
iu.dbg('freesyms')
|
||||
res = match(pat,inst,freesyms)
|
||||
iu.dbg('res')
|
||||
schema = transform_defn_schema(schema,decl)
|
||||
prob = match_problem(schema,decl)
|
||||
prob = transform_defn_match(prob)
|
||||
pmatch = compile_match(proof,prob,schemaname)
|
||||
prob.pat = apply_match(pmatch,prob.pat)
|
||||
iu.dbg('prob')
|
||||
res = match(prob.pat,prob.inst,prob.freesyms,prob.constants)
|
||||
res = merge_matches(res,pmatch)
|
||||
print res
|
||||
show_match(res)
|
||||
return res
|
||||
|
||||
def show_match(m):
|
||||
if m is None:
|
||||
print 'no match'
|
||||
return
|
||||
print 'match {'
|
||||
for x,y in m.iteritems():
|
||||
print '{} : {}'.format(x,y)
|
||||
print '}'
|
||||
|
||||
def match_problem(schema,decl):
|
||||
""" Creating a matching problem from a schema and a declaration """
|
||||
freesyms = set(x.args[0] for x in schema.prems() if isinstance(x,ia.ConstantDecl))
|
||||
freesyms.update(x for x in schema.prems() if isinstance(x,il.UninterpretedSort))
|
||||
freesyms.update(lu.variables_ast(schema.conc()))
|
||||
return MatchProblem(schema.conc(),decl,freesyms,set(lu.variables_ast(decl)))
|
||||
|
||||
def transform_defn_schema(schema,decl):
|
||||
""" Transform definition schema to match a definition. """
|
||||
conc = schema.conc()
|
||||
if not(isinstance(decl,il.Definition) and isinstance(conc,il.Definition)):
|
||||
return schema
|
||||
declargs = decl.lhs().args
|
||||
concargs = conc.lhs().args
|
||||
if len(declargs) > len(concargs):
|
||||
schema = parameterize_schema([x.sort for x in declargs[:len(declargs)-len(concargs)]],schema)
|
||||
iu.dbg('schema')
|
||||
return schema
|
||||
|
||||
def transform_defn_match(prob):
|
||||
""" Transform a problem of matching definitions to a problem of
|
||||
matching the right-hand sides. Requires prob.inst is a definition. """
|
||||
|
||||
conc,decl,freesyms = prob.pat,prob.inst,prob.freesyms
|
||||
if not(isinstance(decl,il.Definition) and isinstance(conc,il.Definition)):
|
||||
return prob
|
||||
declsym = decl.defines()
|
||||
concsym = conc.defines()
|
||||
# dmatch = match(conc.lhs(),decl.lhs(),freesyms)
|
||||
# if dmatch is None:
|
||||
# print "left-hand sides didn't match: {}, {}".format(conc.lhs(),decl.lhs())
|
||||
# return None
|
||||
declargs = decl.lhs().args
|
||||
concargs = conc.lhs().args
|
||||
if len(declargs) < len(concargs):
|
||||
return None
|
||||
declrhs = decl.rhs()
|
||||
concrhs = conc.rhs()
|
||||
vmap = dict((x.name,il.Variable(y.name,x.sort)) for x,y in zip(concargs,declargs))
|
||||
concrhs = lu.substitute_ast(concrhs,vmap)
|
||||
dmatch = {concsym:declsym}
|
||||
print 'func_sorts(concsym) = {}'.format(func_sorts(concsym))
|
||||
print 'func_sorts(declsym) = {}'.format(func_sorts(declsym))
|
||||
for x,y in zip(func_sorts(concsym),func_sorts(declsym)):
|
||||
if x in freesyms:
|
||||
if x in dmatch and dmatch[x] != y:
|
||||
print "lhs sorts didn't match: {}, {}".format(x,y)
|
||||
return None
|
||||
dmatch[x] = y
|
||||
else:
|
||||
if x != y:
|
||||
print "lhs sorts didn't match: {}, {}".format(x,y)
|
||||
return None
|
||||
iu.dbg('dmatch')
|
||||
iu.dbg('concrhs')
|
||||
concrhs = apply_match(dmatch,concrhs)
|
||||
freesyms = apply_match_freesyms(dmatch,freesyms)
|
||||
freesyms = [x for x in freesyms if x not in concargs]
|
||||
constants = set(x for x in prob.constants if x not in declargs)
|
||||
iu.dbg('freesyms')
|
||||
iu.dbg('concrhs')
|
||||
return MatchProblem(concrhs,declrhs,freesyms,constants)
|
||||
|
||||
|
||||
def parameterize_schema(sorts,schema):
|
||||
""" Add initial parameters to all the free symbols in a schema.
|
||||
|
||||
Takes a list of sorts and an ivy_ast.SchemaBody. """
|
||||
|
||||
vars = make_distinct_vars(sorts,schema.conc())
|
||||
match = {}
|
||||
prems = []
|
||||
for prem in schema.prems():
|
||||
if isinstance(prem,ia.ConstantDecl):
|
||||
sym = prem.args[0]
|
||||
vs2 = [il.Variable('X'+str(i),y) for i,y in enumerate(sym.sort.dom)]
|
||||
sym2 = sym.resort(il.FuncConstSort(*(sorts + list(sym.sort.dom) + [sym.sort.rng])))
|
||||
print repr(sym2)
|
||||
match[sym] = il.Lambda(vs2,sym2(*(vars+vs2)))
|
||||
prems.append(ia.ConstantDecl(sym2))
|
||||
else:
|
||||
prems.append(prem)
|
||||
conc = apply_match(match,schema.conc())
|
||||
return schema.clone(prems + [conc])
|
||||
|
||||
# A "match" is a map from symbols to lambda terms
|
||||
|
||||
def compile_match(proof,freesyms,schemaname):
|
||||
def compile_match(proof,prob,schemaname):
|
||||
""" Compiles match in a proof. Only the symbols in
|
||||
freesyms may be used in the match."""
|
||||
|
||||
match = proof.match
|
||||
freesyms = prob.freesyms
|
||||
res = dict()
|
||||
for m in proof.match():
|
||||
sym = m.defines()
|
||||
|
|
@ -140,13 +219,22 @@ def apply_match(match,fmla):
|
|||
args = [apply_match(match,f) for f in fmla.args]
|
||||
if il.is_app(fmla):
|
||||
if fmla.rep in match:
|
||||
return match[fmla.rep](*args)
|
||||
sorts = func_sorts(fmla.rep)
|
||||
sorts = [match.get(s,s) for s in sorts]
|
||||
func = il.Symbol(fmla.rep.name,sorts[0] if len(sorts) == 1 else il.FunctionSort(*sorts))
|
||||
return func(*args)
|
||||
func = match[fmla.rep]
|
||||
return func(*args)
|
||||
return apply_match_func(match,fmla.rep)(*args)
|
||||
return fmla.clone(args)
|
||||
|
||||
def apply_match_func(match,func):
|
||||
sorts = func_sorts(func)
|
||||
sorts = [match.get(s,s) for s in sorts]
|
||||
return il.Symbol(func.name,sorts[0] if len(sorts) == 1 else il.FunctionSort(*sorts))
|
||||
|
||||
def apply_match_sym(match,sym):
|
||||
return match.get(sym,sym) if isinstance(sym,il.UninterpretedSort) else apply_match_func(match,sym)
|
||||
|
||||
def apply_match_freesyms(match,freesyms):
|
||||
return [apply_match_sym(match,sym) for sym in freesyms if sym not in match]
|
||||
|
||||
def func_sorts(func):
|
||||
return list(func.sort.dom) + [func.sort.rng]
|
||||
|
||||
|
|
@ -170,13 +258,17 @@ def heads_match(pat,inst,freesyms):
|
|||
or not il.is_app(pat) and not il.is_quantifier(pat)
|
||||
and type(pat) is type(inst) and len(pat.args) == len(inst.args))
|
||||
|
||||
def make_distinct_vars(sorts,*asts):
|
||||
vars = [il.Variable('V'+str(i),sort) for i,sort in enumerate(sorts)]
|
||||
return lu.rename_variables_distinct_asts(vars,asts)
|
||||
|
||||
|
||||
def extract_terms(inst,terms):
|
||||
""" Returns a lambda term t such that t(terms) = inst and
|
||||
terms do not occur in t. vars is a list of distinct variables
|
||||
of same types as terms that are not free in inst. """
|
||||
|
||||
vars = [il.Variable('V'+str(i),t.sort) for i,t in enumerate(terms)]
|
||||
vars = lu.rename_variables_distinct_ast(vars,inst)
|
||||
vars = make_distinct_vars([t.sort for t in terms], inst)
|
||||
def rec(inst):
|
||||
for term,var in zip(terms,vars):
|
||||
if term == inst:
|
||||
|
|
@ -184,7 +276,7 @@ def extract_terms(inst,terms):
|
|||
return inst.clone(map(rec,inst.args))
|
||||
return il.Lambda(vars,rec(inst))
|
||||
|
||||
def match(pat,inst,freesyms):
|
||||
def match(pat,inst,freesyms,constants):
|
||||
""" Match an instance to a pattern.
|
||||
|
||||
A match is an assignment sigma to freesyms such
|
||||
|
|
@ -194,15 +286,37 @@ def match(pat,inst,freesyms):
|
|||
|
||||
iu.dbg('pat')
|
||||
iu.dbg('inst')
|
||||
if il.is_quantifier(pat):
|
||||
return match_quants(pat,inst,freesyms,constants)
|
||||
if heads_match(pat,inst,freesyms):
|
||||
matches = [match(x,y,freesyms) for x,y in zip(pat.args,inst.args)]
|
||||
matches = [match(x,y,freesyms,constants) for x,y in zip(pat.args,inst.args)]
|
||||
matches.extend([match_sort(x,y,freesyms) for x,y in zip(term_sorts(pat),term_sorts(inst))])
|
||||
return merge_matches(*matches)
|
||||
if il.is_app(pat) and pat.rep in freesyms:
|
||||
B = extract_terms(inst,pat.args)
|
||||
iu.dbg('B')
|
||||
if lu.is_ground_ast(B):
|
||||
if all(v in constants for v in lu.variables_ast(B)):
|
||||
return {pat.rep:B}
|
||||
else:
|
||||
iu.dbg('constants')
|
||||
|
||||
|
||||
def match_quants(pat,inst,freesyms,constants):
|
||||
""" Match an instance to a pattern that is a quantifier.
|
||||
"""
|
||||
|
||||
if type(pat) is not type(inst) or len(pat.variables) != len(inst.variables):
|
||||
return None
|
||||
with AddSymbols(freesyms,pat.variables):
|
||||
matches = [match(x,y,freesyms,constants) for x,y in zip(pat.variables,inst.variables)]
|
||||
matches.append(match(pat.body,inst.body,freesyms,constants))
|
||||
mat = merge_matches(*matches)
|
||||
if mat is not None:
|
||||
for x in pat.variables:
|
||||
if x in mat:
|
||||
del mat[x]
|
||||
return mat
|
||||
|
||||
|
||||
def match_sort(pat,inst,freesyms):
|
||||
if pat in freesyms:
|
||||
|
|
@ -214,7 +328,6 @@ def merge_matches(*matches):
|
|||
return dict()
|
||||
if any(match is None for match in matches):
|
||||
return None
|
||||
iu.dbg('matches[0]')
|
||||
res = dict(matches[0].iteritems())
|
||||
for match2 in matches[1:]:
|
||||
for sym,lmda in match2.iteritems():
|
||||
|
|
@ -235,3 +348,24 @@ def equiv_alpha(x,y):
|
|||
return x.body == il.substitute(y.body,zip(x.variables,y.variables))
|
||||
return false
|
||||
pass
|
||||
|
||||
class AddSymbols(object):
|
||||
""" temporarily add some symbols to a set of symbols """
|
||||
def __init__(self,symset,symlist):
|
||||
self.symset,self.symlist = symset,list(symlist)
|
||||
def __enter__(self):
|
||||
global sig
|
||||
self.saved = []
|
||||
for sym in self.symlist:
|
||||
if sym in self.symset:
|
||||
self.saved.append(sym)
|
||||
self.remove(sym)
|
||||
self.symset.add(sym)
|
||||
return self
|
||||
def __exit__(self,exc_type, exc_val, exc_tb):
|
||||
global sig
|
||||
for sym in self.symlist:
|
||||
self.symset.remove(sym)
|
||||
for sym in self.saved:
|
||||
self.symset.add(sym)
|
||||
return False # don't block any exceptions
|
||||
|
|
|
|||
|
|
@ -527,7 +527,8 @@ def collect_numerals(z3term):
|
|||
|
||||
def from_z3_numeral(z3term,sort):
|
||||
name = str(z3term)
|
||||
assert name[0].isdigit() or name[0] == '"'
|
||||
if not(name[0].isdigit() or name[0] == '"'):
|
||||
print "unexpected numeral from Z3 model: {}".format(name)
|
||||
return ivy_logic.Symbol(name,sort)
|
||||
|
||||
def collect_model_values(sort,model,sym):
|
||||
|
|
|
|||
|
|
@ -234,7 +234,8 @@ class And(recstruct('And', [], ['*terms'])):
|
|||
', '.join(str(t) for t in terms),
|
||||
bad_sorts,
|
||||
))
|
||||
return sorted(set(terms))
|
||||
return tuple(terms)
|
||||
# return sorted(set(terms))
|
||||
def __str__(self):
|
||||
return 'And({})'.format(
|
||||
', '.join(str(t) for t in self)
|
||||
|
|
@ -330,7 +331,7 @@ class Lambda(recstruct('Lambda', ['variables'], ['body'])):
|
|||
def _preprocess_(cls, variables, body):
|
||||
if not all(type(v) is Var for v in variables):
|
||||
raise IvyError("Can only abstract over variables")
|
||||
return frozenset(variables), body
|
||||
return tuple(variables), body
|
||||
def __str__(self):
|
||||
return '(Lambda {}. {})'.format(
|
||||
', '.join('{}:{}'.format(v.name, v.sort) for v in sorted(self.variables)),
|
||||
|
|
|
|||
104
test/schema1.ivy
104
test/schema1.ivy
|
|
@ -2,31 +2,95 @@
|
|||
|
||||
type t
|
||||
type r
|
||||
|
||||
|
||||
schema foo = {
|
||||
type q
|
||||
function base(X:t) : q
|
||||
function step(X:q) : q
|
||||
function fun(X:t) : q
|
||||
#---------------------------------------------------------
|
||||
definition fun(X:t) = base(X) if X <= 0 else step(fun(X-1))
|
||||
}
|
||||
|
||||
function bif(X:t):r
|
||||
|
||||
definition bif(X) = 0 if X <= 0 else bif(X-1) + 1
|
||||
#proof foo with base(X) = 0, step(X) = X + 1
|
||||
proof foo
|
||||
|
||||
function succ(X:t,Y:t) = (Y-1 = X)
|
||||
type s
|
||||
|
||||
axiom (T:t < U & U < V) -> (T < V)
|
||||
axiom ~(T:t < U & U < T)
|
||||
axiom T:t < U | T = U | U < T
|
||||
|
||||
property [bif_base] bif(0) = 0
|
||||
property [bif_step] F > 0 & succ(E,F) -> bif(F) = bif(E) + 1
|
||||
relation succ(X:t,Y:t)
|
||||
|
||||
|
||||
schema rec[t] = {
|
||||
type q
|
||||
function base(X:t) : q
|
||||
function step(X:q,Y:t) : q
|
||||
function fun(X:t) : q
|
||||
#---------------------------------------------------------
|
||||
definition fun(X:t) = base(X) if X <= 0 else step(fun(X-1),X)
|
||||
}
|
||||
|
||||
schema lep[t] = {
|
||||
function p(X:t) : bool
|
||||
#---------------------------------------------------------
|
||||
property exists L. (L >= 0 & forall B. (B >= 0 & p(B)-> p(L) & L <= B))
|
||||
}
|
||||
|
||||
relation member(X:t,S:s)
|
||||
|
||||
function cnt(X:t):r
|
||||
function card(S:s) : r
|
||||
function cardUpTo(S:s,B:t) : r
|
||||
individual n : t
|
||||
axiom n > 0
|
||||
|
||||
object counting = {
|
||||
|
||||
object spec = {
|
||||
|
||||
property [cnt_base] cnt(0) = 0
|
||||
property [cnt_step] F > 0 & succ(E,F) -> cnt(F) = cnt(E) + 1
|
||||
|
||||
property [cardUpTo_base] cardUpTo(S,0) = 0
|
||||
property [cardUpTo_step] succ(B,BS) & BS > 0 ->
|
||||
cardUpTo(S,BS) = cardUpTo(S,B)+1 if member(B,S) else cardUpTo(S,B)
|
||||
}
|
||||
|
||||
object impl = {
|
||||
|
||||
definition cnt(X) = 0 if X <= 0 else cnt(X-1) + 1
|
||||
proof rec[t]
|
||||
|
||||
definition cardUpTo(S,B) =
|
||||
0 if B <= 0 else (cardUpTo(S,B-1)+1 if member(B-1,S) else cardUpTo(S,B-1))
|
||||
proof rec[t]
|
||||
|
||||
definition succ(X:t,Y:t) = (Y-1 = X)
|
||||
|
||||
}
|
||||
|
||||
isolate iso = spec with impl
|
||||
}
|
||||
|
||||
object disjointness = {
|
||||
|
||||
object spec = {
|
||||
axiom succ(X,Y) -> X < Y
|
||||
axiom ~(X < Y & Y < Z & succ(X,Z))
|
||||
|
||||
relation disjoint(X:s,Y:s)
|
||||
|
||||
definition disjoint(X,Y) = forall E. ~(member(E,X) & member(E,Y))
|
||||
|
||||
derived inv(X,Y,B) =
|
||||
disjoint(X,Y) -> cardUpTo(X,B) + cardUpTo(Y,B) <= cnt(B)
|
||||
|
||||
property exists L. (L >= 0 & forall B. (B >= 0 & ~inv(X,Y,B) -> ~inv(X,Y,L) & L <= B))
|
||||
named lerr(X,Y)
|
||||
proof lep[t]
|
||||
|
||||
axiom [induc] exists E. succ(E,lerr(X,Y))
|
||||
|
||||
definition card(S) = cardUpTo(S,n)
|
||||
|
||||
property disjoint(X,Y) -> card(X) + card(Y) <= cnt(n)
|
||||
|
||||
interpret r->int
|
||||
}
|
||||
|
||||
isolate iso = spec with counting
|
||||
}
|
||||
|
||||
|
||||
|
||||
# fun(X) = bif(X)
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче