зеркало из https://github.com/microsoft/ivy.git
cleaning up
This commit is contained in:
Родитель
66616510cc
Коммит
27cd798e61
|
@ -4,6 +4,7 @@ helloworld
|
|||
account
|
||||
account2
|
||||
account3
|
||||
leader_election_ring
|
||||
leader_election_ring_repl
|
||||
udp
|
||||
leader_election_ring_udp
|
||||
|
@ -15,3 +16,6 @@ udp_test
|
|||
udp_test2
|
||||
udp_test_struct
|
||||
udp_test_array
|
||||
interference
|
||||
token_ring
|
||||
delmap_test
|
||||
|
|
|
@ -1,2 +1,5 @@
|
|||
*.cpp
|
||||
*.h
|
||||
arraygen
|
||||
genstruct
|
||||
strlit1
|
||||
|
|
|
@ -0,0 +1,39 @@
|
|||
|
||||
from ivy import ivy_module as im
|
||||
from ivy.ivy_compiler import ivy_from_string
|
||||
from ivy.tk_ui import new_ui
|
||||
from ivy import ivy_utils as iu
|
||||
from ivy import ivy_interp as itp
|
||||
from ivy import ivy_isolate as ivy_isolate
|
||||
from ivy import ivy_check as ick
|
||||
|
||||
prog = """#lang ivy1.6
|
||||
|
||||
type s
|
||||
interpret s -> strlit
|
||||
|
||||
individual x:s
|
||||
property [foo] ~(x = "0" & x = "1")
|
||||
|
||||
|
||||
|
||||
"""
|
||||
|
||||
with im.Module():
|
||||
iu.set_parameters({'mode':'induction','show_compiled':'true'})
|
||||
ivy_from_string(prog,create_isolate=False)
|
||||
try:
|
||||
ick.check_module()
|
||||
except iu.IvyError as e:
|
||||
print str(e)
|
||||
assert False,"property should have been true"
|
||||
|
||||
|
||||
# with im.module.copy():
|
||||
# ivy_isolate.create_isolate(None) # ,ext='ext'
|
||||
# gui = new_ui()
|
||||
# gui.tk.update_idletasks() # so that dialog is on top of main window
|
||||
# gui.try_property()
|
||||
# gui.mainloop()
|
||||
|
||||
|
|
@ -0,0 +1,19 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include order
|
||||
include collections
|
||||
|
||||
type a # network addresses
|
||||
type index
|
||||
type t
|
||||
instance arr : array(index,t)
|
||||
|
||||
include udp
|
||||
instance foo : udp_simple(a,arr.t)
|
||||
|
||||
import foo.recv
|
||||
export foo.send
|
||||
|
||||
interpret a->bv[1]
|
||||
|
||||
extract iso_impl = foo.impl, arr
|
|
@ -0,0 +1,18 @@
|
|||
#lang ivy1.6
|
||||
|
||||
type a # network addresses
|
||||
type t
|
||||
type p = struct {
|
||||
x : t,
|
||||
y : t
|
||||
}
|
||||
|
||||
include udp
|
||||
instance foo : udp_simple(a,p)
|
||||
|
||||
import foo.recv
|
||||
export foo.send
|
||||
|
||||
interpret a->bv[1]
|
||||
|
||||
extract iso_impl = foo.impl
|
Загрузка…
Ссылка в новой задаче