зеркало из https://github.com/microsoft/ivy.git
more forgotten files
This commit is contained in:
Ken McMillan
Родитель
863b06b277
Коммит
0d6027ca23
|
|
@ -26,4 +26,13 @@ build
|
|||
dist
|
||||
|
||||
# vagrant
|
||||
/.vagrant
|
||||
/.vagrant
|
||||
|
||||
# Temporary files are put in directories called temp
|
||||
temp
|
||||
|
||||
# The file 'specs' is generated by ivy_libs
|
||||
specs
|
||||
|
||||
# These are library directories
|
||||
gnutls
|
||||
|
|
|
|||
|
|
@ -0,0 +1,39 @@
|
|||
#lang ivy1.6
|
||||
|
||||
########################################
|
||||
# A shard contains an interval of keys [lo,hi) from a hash table
|
||||
#
|
||||
|
||||
include order
|
||||
include collections
|
||||
|
||||
module table_shard(key,data) = {
|
||||
|
||||
type pair = struct {
|
||||
p_key : key.t,
|
||||
p_value : data
|
||||
}
|
||||
|
||||
instance index : unbounded_sequence
|
||||
|
||||
instance arr : array(index.t,pair)
|
||||
|
||||
type t = struct {
|
||||
lo : key.iter.t,
|
||||
hi : key.iter.t,
|
||||
pairs : arr.t
|
||||
}
|
||||
|
||||
function key_at(S,I) = p_key(arr.value(pairs(S),I))
|
||||
function value_at(S,I) = p_value(arr.value(pairs(S),I))
|
||||
function at(S,X,I) = (0 <= I & I < arr.end(pairs(S)) & key_at(S,I) = X)
|
||||
|
||||
function rel(S:t,x:key.t) = exists Y. at(S,x,Y)
|
||||
function valid(s:t) = forall X,Y,Z. at(s,X,Y) & at(s,X,Z) -> Y = Z
|
||||
|
||||
}
|
||||
|
||||
type t = struct {
|
||||
f(X:t) : q
|
||||
r(X:t) : bool
|
||||
}
|
||||
|
|
@ -0,0 +1,143 @@
|
|||
#lang ivy1.6
|
||||
|
||||
# Here, we prove a basic fact about finite sets: is X and Y are disjoint
|
||||
# subsets of S, then |X| + |Y| <= |S|. This can be used to show that any two
|
||||
# majorities of S have an element in common.
|
||||
|
||||
# We set up the problem with two types: the *basis* type and the
|
||||
# *index* type, both isomorphic to the integers. Our sets are subsets
|
||||
# of the basis type, while their cardinalities a members of the index
|
||||
# type. In other words ordinals are in basis, while cardinals are in
|
||||
# index. The separation of these two types is used to avoid
|
||||
# non-stratified functions.
|
||||
|
||||
# We definte a module that takes basis and index types, and provides the following
|
||||
# interface:
|
||||
|
||||
# 1) a type *set* representing finite subsets of the basis type
|
||||
# 2) a basis element *n* that is an upper bound on set elements (so the basis is finite)
|
||||
# 3) a *member* relation
|
||||
# 4) a relation *disjoint* beteween sets
|
||||
# 5) a function *card* giving the cardinality of a set as an index
|
||||
# 6) a function *cnt* gives the cardinality of the basis elements less than E
|
||||
# 7) an action `empty` returning the empty set
|
||||
|
||||
# The spec can then be stated as disjoint(X,Y) -> card(X)+card(Y) <= cnt(n).
|
||||
|
||||
# The implementation defines card and cnt recursively over the basis type. Ideally, the
|
||||
# basis type should provide a recursion schema, but here we just give the instantions
|
||||
# of the recursion schema as axioms.
|
||||
|
||||
# We then give an inductive invariant with parameter B. This states that the theorem holds
|
||||
# for elements of the sets X and Y less than B. We then instantiate the induction schema for
|
||||
# basis using the invariant.
|
||||
|
||||
# This all seems straightforward, but it was tricky to figure out how to set up the problem
|
||||
# without function cycles. Also, see the comment below about integer arithmetic. For the
|
||||
# basis type, we used the succesor relation to avoid using airthmetic on this type.
|
||||
|
||||
include collections
|
||||
include order
|
||||
|
||||
module indexset(basis,index) = {
|
||||
|
||||
type set
|
||||
|
||||
individual n : basis.t
|
||||
relation member(E:basis.t,S:set)
|
||||
relation disjoint(X:set,Y:set)
|
||||
function card(S:set) : index.t
|
||||
function cnt(E:basis.t) : index.t
|
||||
|
||||
action empty returns(s:set)
|
||||
action add(s:set,e:basis.t) returns (s:set)
|
||||
|
||||
axiom n >= 0
|
||||
|
||||
object spec = {
|
||||
property disjoint(X,Y) -> card(X) + card(Y) <= cnt(n)
|
||||
|
||||
after empty {
|
||||
assert ~member(E,s);
|
||||
}
|
||||
|
||||
after add {
|
||||
assert member(X,s) <-> (member(X,old s) | X = e)
|
||||
}
|
||||
}
|
||||
|
||||
object impl = {
|
||||
|
||||
|
||||
|
||||
definition disjoint(X,Y) = forall E. ~(member(E,X) & member(E,Y))
|
||||
|
||||
# recursive definiton of cnt
|
||||
|
||||
axiom cnt(0) = 0
|
||||
axiom basis.succ(E,F) -> cnt(F) = cnt(E) + 1
|
||||
|
||||
# recursive definition of card
|
||||
|
||||
function cardUpTo(S:set,B:basis.t) : index.t
|
||||
|
||||
axiom cardUpTo(S,0) = 0
|
||||
axiom basis.succ(B,BS) -> cardUpTo(S,BS) = cardUpTo(S,B)+1 if member(B,S) else cardUpTo(S,B)
|
||||
|
||||
definition card(S) = cardUpTo(S,n)
|
||||
|
||||
# invariant
|
||||
|
||||
derived inv(B,X,Y) =
|
||||
disjoint(X,Y) -> cardUpTo(X,B) + cardUpTo(Y,B) <= cnt(B)
|
||||
|
||||
|
||||
# induction schema instance: basis.t is well-founded, and every
|
||||
# element > 0 has a predecessor
|
||||
|
||||
derived lerr(X,Y) = some E. (E >= 0 & ~inv(E,X,Y))
|
||||
axiom ~(E >= 0 & ~inv(E,X,Y) & E < lerr(X,Y))
|
||||
axiom lerr(X,Y) > 0 -> exists E. basis.succ(E,lerr(X,Y))
|
||||
|
||||
# tricky: we interpret the index type as the integers, so we can use addition
|
||||
# without axioms. we have set up the above so the index type is never the domain of
|
||||
# a function. a bug in IVy's logic fragmetn checker seems to allow us to get away with this,
|
||||
# and it works, but I don't know if Z3 is actually a decision procedure for this case.
|
||||
|
||||
interpret index.t -> int
|
||||
|
||||
# Here is the implementation of the set type using an unsorted array. The above reasoning
|
||||
# is actually independent of the definition of "member" below. Hopefully, this definition
|
||||
# will not confuse Z3. If it did, we would have to put these definitions into their own isolate.
|
||||
|
||||
instance arridx : unbounded_sequence
|
||||
instance arr:array(arridx.t,basis.t)
|
||||
|
||||
# Tricky: this is a bit of aspect-orientation. It turns the type `set` into a struct
|
||||
# with just one field called `repr`. This field gives the concrete representation of a
|
||||
# set as an array. To an isolate the doesn't use the definition of `member` below,
|
||||
# the tpye `set` will still appear to be uninterpreted.
|
||||
|
||||
destructor repr(X:set) : arr.t
|
||||
|
||||
definition member(y:basis.t,X:set) = exists Z. 0 <= Z & Z < repr(X).end & repr(X).value(Z) = y
|
||||
|
||||
implement empty {
|
||||
repr(s) := arr.create(0,0)
|
||||
}
|
||||
|
||||
implement add {
|
||||
if ~member(e,s) {
|
||||
repr(s) := repr(s).resize(repr(s).end.next,e)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
instance bss : unbounded_sequence
|
||||
instance idx : unbounded_sequence
|
||||
instance s : indexset(bss,idx)
|
||||
|
||||
isolate iso = s with idx,bss
|
||||
|
|
@ -0,0 +1,642 @@
|
|||
#lang ivy1.7
|
||||
|
||||
type id
|
||||
type cache_state_ = { invalid, shared, exclusive }
|
||||
type wait_type = { none, get, getX }
|
||||
|
||||
module cache_line = {
|
||||
individual wait : wait_type
|
||||
relation invmarked
|
||||
individual state_ : cache_state_
|
||||
}
|
||||
|
||||
module header = {
|
||||
relation pending
|
||||
relation local_
|
||||
relation dirty
|
||||
relation head
|
||||
individual hptr : id
|
||||
relation list
|
||||
relation real(X:id)
|
||||
relation upgrade
|
||||
relation shlist(X:id)
|
||||
}
|
||||
|
||||
module network = {
|
||||
relation get(S:id,D:id)
|
||||
relation put(S:id,D:id)
|
||||
relation getX(S:id,D:id)
|
||||
relation putX(S:id,D:id)
|
||||
relation nak(S:id,D:id)
|
||||
relation fack(S:id,D:id)
|
||||
relation shwb(S:id,D:id)
|
||||
}
|
||||
|
||||
module wb_network = {
|
||||
individual proc : id
|
||||
relation wb
|
||||
}
|
||||
|
||||
individual home : id
|
||||
instantiate cache(X:id) : cache_line
|
||||
instantiate dir : header
|
||||
relation collecting
|
||||
individual requester : id
|
||||
instantiate net : network
|
||||
relation rp_net(X:id)
|
||||
individual real_owner : id
|
||||
individual fwd_get : wait_type
|
||||
instantiate wbnet : wb_network
|
||||
individual last_WB : id
|
||||
relation nakc
|
||||
relation invnet(X:id)
|
||||
relation invack(X:id)
|
||||
|
||||
# locals used in actions
|
||||
|
||||
individual src : id
|
||||
individual dst : id
|
||||
|
||||
after init {
|
||||
cache(X).state_ := invalid;
|
||||
cache(X).wait := none;
|
||||
cache(X).invmarked := false;
|
||||
dir.pending := false;
|
||||
dir.dirty := false;
|
||||
collecting := false;
|
||||
net.get(X,Y) := false;
|
||||
net.put(X,Y) := false;
|
||||
net.getX(X,Y) := false;
|
||||
net.putX(X,Y) := false;
|
||||
net.fack(X,Y) := false;
|
||||
net.shwb(X,Y) := false;
|
||||
net.nak(X,Y) := false;
|
||||
dir.list := false;
|
||||
dir.head := false;
|
||||
dir.shlist(X) := false;
|
||||
rp_net(X) := false;
|
||||
fwd_get := none;
|
||||
wbnet.wb := false;
|
||||
real_owner := home;
|
||||
invnet(X) := false;
|
||||
invack(X) := false;
|
||||
nakc := false
|
||||
}
|
||||
|
||||
action pi_Local_Get_dirty = {
|
||||
assume cache(home).state_ = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume dir.dirty;
|
||||
dir.pending := true;
|
||||
collecting := false;
|
||||
cache(home).wait := get;
|
||||
net.get(home,dir.hptr) := true;
|
||||
requester := home
|
||||
}
|
||||
|
||||
action pi_Local_Get = {
|
||||
assume cache(home).state_ = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume ~dir.dirty;
|
||||
assume ~cache(home).invmarked;
|
||||
dir.local_ := true;
|
||||
cache(home).state_ := shared
|
||||
}
|
||||
|
||||
# TODO: can this ever happen?
|
||||
|
||||
action pi_Local_Get_im = {
|
||||
assume cache(home).state_ = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume ~dir.dirty;
|
||||
assume cache(home).invmarked;
|
||||
cache(home).invmarked := false
|
||||
}
|
||||
|
||||
action pi_Remote_Get = {
|
||||
assume src ~= home;
|
||||
assume cache(src).state_ = invalid;
|
||||
assume cache(src).wait = none;
|
||||
cache(src).wait := get;
|
||||
net.get(src,home) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# action ni_Local_Get_nak = {
|
||||
# assume net.get(src,home);
|
||||
# assume home ~= src;
|
||||
# assume ~rp_net(src);
|
||||
# assume dir.pending | (dir.dirty & dir.local_ & cache(home).state_~=exclusive) | (dir.dirty & ~dir.local_ & src = dir.hptr);
|
||||
# net.get(src,home) := false;
|
||||
# net.nak(home,src) := true
|
||||
# }
|
||||
|
||||
# action ni_Local_Get = {
|
||||
# assume net.get(src,home);
|
||||
# assume home ~= src;
|
||||
# assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
|
||||
# net.get(src,home) := false;
|
||||
# net.put(home,src) := true;
|
||||
# if (dir.head) {
|
||||
# dir.list := true;
|
||||
# dir.shlist(src) := true;
|
||||
# dir.real := dir.shlist # what is this?
|
||||
# }
|
||||
# else {
|
||||
# dir.head := true;
|
||||
# dir.hptr := src
|
||||
# }
|
||||
# }
|
||||
|
||||
action ni_Local_Get = {
|
||||
assume net.get(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
|
||||
net.get(src,home) := false;
|
||||
net.put(home,src) := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.shlist(src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Local_Get_fwd = {
|
||||
assume net.get(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr;
|
||||
net.get(src,home) := false;
|
||||
dir.pending := true;
|
||||
net.get(src,dir.hptr) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Remote_Put = {
|
||||
assume dst ~= home;
|
||||
assume net.put(src,dst);
|
||||
net.put(src,dst) := false;
|
||||
cache(dst).wait := none;
|
||||
cache(dst).state_ := shared;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
# Non-deterministically drop a shared line from the cache. Send an rp message.
|
||||
# informing the directory.
|
||||
|
||||
action pi_Remote_Replace = {
|
||||
assume cache(src).state_=shared & cache(src).wait=none & src ~= home;
|
||||
cache(src).state_ := invalid;
|
||||
rp_net(src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives a replace message, removes sender from sharing list, assuming it is not head.
|
||||
|
||||
action ni_Replace_list = {
|
||||
assume rp_net(src);
|
||||
assume dir.hptr ~= src;
|
||||
rp_net(src) := false;
|
||||
dir.shlist(src) := false;
|
||||
dir.real(src) := false;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Remote is invalid and wants an exclusive copy
|
||||
|
||||
action pi_Remote_GetX = {
|
||||
assume cache(src).state_=invalid & cache(src).wait=none & src ~= home;
|
||||
cache(src).wait := getX;
|
||||
net.getX(src,home) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when no invalidation is needed, that is, there is no exclusive
|
||||
# copy and either the sharing list is empty or it contains only the
|
||||
# source.
|
||||
|
||||
action ni_Local_GetX = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty;
|
||||
assume ~dir.head | src = dir.hptr;
|
||||
assume ~dir.head | ~dir.shlist(X) | X = src;
|
||||
net.getX(src,home) := false;
|
||||
dir.dirty := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.real(X) := X = src;
|
||||
dir.shlist(X) := X = src;
|
||||
net.putX(home,src) := true;
|
||||
real_owner := src; # ghost
|
||||
cache(home).state_ := invalid;
|
||||
cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when the request is nak'd
|
||||
|
||||
action ni_Local_GetX_nak = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume dir.pending | dir.dirty & cache(home).state_ ~= exclusive | src = dir.hptr;
|
||||
net.getX(src,home) := false;
|
||||
net.nak(home,src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when the request is pended.
|
||||
|
||||
action ni_Local_GetX_pend = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr;
|
||||
net.getX(src,home) := false;
|
||||
dir.pending := true;
|
||||
collecting := false;
|
||||
net.getX(src,dir.hptr) := true;
|
||||
fwd_get := getX;
|
||||
requester := src;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when invalidations are sent out.
|
||||
|
||||
action ni_localGetX_inv = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty & ~dir.local_;
|
||||
assume dir.head;
|
||||
assume src ~= dir.hptr | (dir.shlist(dst) & dst~=src);
|
||||
net.getX(src,home) := false;
|
||||
invnet(X) := X ~= home & X ~= src & dir.shlist(X);
|
||||
collecting := true;
|
||||
# m1 := m;
|
||||
# last_other_invack := (dir.hptr ~= src) ? dir.hptr . {i . i in Proc, dir.shlist(i) & i~=src};
|
||||
cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
|
||||
dir.local_ := false;
|
||||
dir.dirty := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.pending := true;
|
||||
dir.real(X) := X ~= home & X ~= src & dir.shlist(X);
|
||||
dir.shlist(X) := X = src;
|
||||
net.putX(home,src) := true;
|
||||
real_owner := src;
|
||||
cache(home).state_ := invalid;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_PutX = {
|
||||
assume net.putX(src,dst);
|
||||
assume dst~=home & cache(dst).wait = getX;
|
||||
net.putX(src,dst) := false;
|
||||
cache(dst).wait :=none;
|
||||
cache(dst).invmarked := false;
|
||||
cache(dst).state_ :=exclusive;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action pi_Remote_PutX = {
|
||||
assume cache(src).state_ = exclusive & src ~= home; # cache(src).wait=none ???
|
||||
cache(src).state_ := invalid;
|
||||
wbnet.proc := src;
|
||||
wbnet.wb := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Inv = {
|
||||
assume invnet(dst) & dst~=home;
|
||||
invnet(dst) := false;
|
||||
invack(dst) := true;
|
||||
cache(dst).invmarked := (cache(dst).wait = get) | cache(dst).invmarked;
|
||||
cache(dst).state_ := invalid;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_InvAck = {
|
||||
assume dir.pending & invack(src) & src~=home;
|
||||
assume dir.real(dst) & dst ~= src;
|
||||
invack(src) := false;
|
||||
dir.real(src) := false;
|
||||
# last_invack := src;
|
||||
# last_other_invack := {i : i in Proc, dir.real(i) & i ~= src};
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_InvAck_last = {
|
||||
assume dir.pending & invack(src) & src~=home;
|
||||
assume ~dir.real(X) | X = src;
|
||||
dir.pending := false;
|
||||
collecting := false;
|
||||
# m1 := undefined; ???
|
||||
invack(src) := false;
|
||||
dir.real(src) := false;
|
||||
# last_invack := src;
|
||||
if ( dir.local_ & ~ dir.dirty) {
|
||||
dir.local_ := false
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
action ni_WB = {
|
||||
assume wbnet.wb;
|
||||
wbnet.wb := false;
|
||||
dir.dirty := false;
|
||||
dir.head := false;
|
||||
dir.shlist(X) := false;
|
||||
last_WB := wbnet.proc
|
||||
}
|
||||
|
||||
action ni_Remote_GetX_nak = {
|
||||
assume net.getX(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state_ ~= exclusive;
|
||||
net.getX(src,dst) := false;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
nakc := true;
|
||||
net.nak(dst,src) := true;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_GetX_fwd = {
|
||||
assume net.getX(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state_ = exclusive;
|
||||
net.getX(src,dst) := false;
|
||||
cache(dst).state_ := invalid;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
net.putX(dst,src) := true;
|
||||
real_owner := src;
|
||||
if src~=home {
|
||||
net.fack(src,home) := true
|
||||
};
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_FAck = {
|
||||
assume net.fack(src,home);
|
||||
net.fack(src,home) := false;
|
||||
dir.pending := false;
|
||||
if dir.dirty {
|
||||
dir.hptr := src;
|
||||
dir.shlist(X) := X = src
|
||||
};
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Remote_Get_nak = {
|
||||
assume net.get(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state_ ~= exclusive;
|
||||
net.get(src,dst) := false;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
nakc := true;
|
||||
net.nak(dst,src) := true;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_Get_fwd = {
|
||||
assume net.get(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state_ = exclusive;
|
||||
net.get(src,dst) := false;
|
||||
# assume ~cache(src).invmarked; TODO: ???
|
||||
cache(dst).state_ := shared;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
net.put(dst,src) := true;
|
||||
if src~=home {
|
||||
real_owner := home;
|
||||
net.shwb(src,home) := true
|
||||
};
|
||||
# shwb_src := dst;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_ShWB = {
|
||||
assume net.shwb(src,home);
|
||||
net.shwb(src,home) := false;
|
||||
dir.pending := false;
|
||||
dir.dirty := false;
|
||||
dir.shlist(src) := true;
|
||||
dir.real(X) := dir.shlist(X);
|
||||
# last_WB := shwb_src;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_NAK_Clear = {
|
||||
assume nakc;
|
||||
dir.pending := false;
|
||||
nakc := false
|
||||
}
|
||||
|
||||
export pi_Local_Get_dirty
|
||||
export pi_Local_Get
|
||||
export pi_Local_Get_im
|
||||
export pi_Remote_Get
|
||||
#export ni_Local_Get_nak
|
||||
#export ni_Local_Get
|
||||
export ni_Local_Get
|
||||
export ni_Local_Get_fwd
|
||||
export ni_Remote_Put
|
||||
export pi_Remote_Replace
|
||||
export ni_Replace_list
|
||||
export pi_Remote_GetX
|
||||
export ni_Local_GetX
|
||||
export ni_Local_GetX_nak
|
||||
export ni_Local_GetX_pend
|
||||
export ni_localGetX_inv
|
||||
export ni_Remote_PutX
|
||||
export pi_Remote_PutX
|
||||
export ni_Inv
|
||||
export ni_InvAck
|
||||
export ni_InvAck_last
|
||||
export ni_WB
|
||||
export ni_Remote_GetX_nak
|
||||
export ni_Remote_GetX_fwd
|
||||
export ni_FAck
|
||||
export ni_Remote_Get_nak
|
||||
export ni_Remote_Get_fwd
|
||||
export ni_ShWB
|
||||
export ni_NAK_Clear
|
||||
|
||||
conjecture [coherent]
|
||||
~(cache(X).state_ = exclusive & cache(X).wait = none &
|
||||
cache(Y).state_ = exclusive & cache(Y).wait = none &
|
||||
X ~= Y)
|
||||
|
||||
|
||||
invariant [aux]
|
||||
((Y = Z | ~net.put(Y,X) | ~net.put(Z,X)) &
|
||||
(Y = Z | ~net.get(X,Y) | ~net.get(X,Z)) &
|
||||
(Y = Z | ~net.putX(Y,X) | ~net.putX(Z,X)) &
|
||||
(Y = Z | ~net.getX(X,Y) | ~net.getX(X,Z)) &
|
||||
(~net.get(X,Z) | ~net.put(Y,X)) &
|
||||
(~net.getX(X,Z) | ~net.putX(Y,X)) &
|
||||
~net.getX(home,Y) &
|
||||
(dir.shlist(dir.hptr) | ~dir.head) &
|
||||
(cache.wait(X) = get | ~net.get(X,home)) &
|
||||
(cache.wait(X) = get | ~net.put(home,X)) &
|
||||
(~net.put(home,X) | ~rp_net(X)) &
|
||||
(cache.state_(X) ~= exclusive | cache.wait(X) ~= getX) &
|
||||
(cache.wait(X) = getX | ~net.getX(X,home)) &
|
||||
(cache.wait(X) = getX | ~net.putX(home,X)) &
|
||||
(~net.getX(V1,V0) | cache.wait(V1) ~= none) &
|
||||
(Y = home | ~net.shwb(X,Y)) &
|
||||
(cache.state_(V0) = invalid | ~net.get(V0,V1)) &
|
||||
(cache.state_(V0) = invalid | ~net.put(V1,V0)) &
|
||||
(cache.wait(V0) = get | ~net.get(V0,V1)) &
|
||||
(cache.wait(V0) = get | ~net.put(V1,V0)) &
|
||||
(cache.wait(V0) = getX | ~net.getX(V0,V1)) &
|
||||
(cache.wait(V0) = getX | ~net.putX(V1,V0)) &
|
||||
(V1 = home | ~net.fack(V0,V1)))
|
||||
|
||||
|
||||
invariant (cache.state_(V0) = invalid | ~net.get(V0,V1))
|
||||
invariant (cache.state_(V0) = invalid | ~net.put(V1,V0))
|
||||
invariant (cache.state_(X) ~= exclusive | cache.wait(X) ~= getX)
|
||||
invariant (cache.state_(X) ~= exclusive | dir.head)
|
||||
invariant (cache.state_(X) = invalid | ~invack(X))
|
||||
invariant (cache.state_(X) ~= shared | cache.wait(X) ~= get)
|
||||
invariant cache.wait(real_owner) ~= get
|
||||
invariant (cache.wait(V0) = get | ~net.get(V0,V1))
|
||||
invariant (cache.wait(V0) = get | ~net.put(V1,V0))
|
||||
invariant (cache.wait(V0) = getX | ~net.getX(V0,V1))
|
||||
invariant (cache.wait(V0) = getX | ~net.putX(V1,V0))
|
||||
invariant (cache.wait(X) = get | ~net.get(X,home))
|
||||
invariant (cache.wait(X) = get | ~net.put(home,X))
|
||||
invariant (cache.wait(X) = getX | ~net.getX(X,home))
|
||||
invariant (cache.wait(X) = getX | ~net.putX(home,X))
|
||||
invariant (dir.hptr = real_owner | ~dir.dirty | dir.pending)
|
||||
invariant (dir.hptr = real_owner | ~net.putX(home,X))
|
||||
invariant (dir.real(X) | X = real_owner | cache.state_(X) = invalid)
|
||||
invariant (dir.shlist(dir.hptr) | ~dir.head)
|
||||
invariant (dir.shlist(V0) | V0 = requester | cache.state_(V0) ~= exclusive)
|
||||
invariant (dir.shlist(V1) | V1 = home | ~net.put(V0,V1))
|
||||
invariant (dir.shlist(X) | cache.state_(X) ~= exclusive)
|
||||
invariant (~dir.shlist(X) | dir.head)
|
||||
invariant (~dir.shlist(X) | ~net.get(X,home))
|
||||
invariant (dir.shlist(X) | ~net.put(home,X))
|
||||
invariant (dir.shlist(X) | ~net.putX(home,X))
|
||||
invariant (dir.shlist(Y) | ~net.put(X,Y))
|
||||
invariant (dir.shlist(Y) | ~net.put(X,Y) | dir.dirty)
|
||||
invariant (dir.shlist(Y) | ~net.put(X,Y) | dir.pending)
|
||||
invariant (~invack(V0) | cache.state_(V0) ~= shared)
|
||||
invariant (~invack(X) | ~invnet(X))
|
||||
invariant ~net.fack(requester,home)
|
||||
invariant ~net.get(home,Y)
|
||||
invariant ~net.getX(home,Y)
|
||||
invariant (~net.getX(V1,V0) | cache.wait(V1) ~= none)
|
||||
invariant (~net.getX(X,Z) | ~net.putX(Y,X))
|
||||
invariant (~net.get(X,Z) | ~net.put(Y,X))
|
||||
invariant ~net.put(dir.hptr,V0)
|
||||
invariant ~net.put(home,X)
|
||||
invariant (~net.put(home,X) | ~rp_net(X))
|
||||
invariant (~net.put(V1,V0) | ~rp_net(V0))
|
||||
invariant ~net.putX(home,X)
|
||||
invariant (~net.putX(home,X) | dir.head)
|
||||
invariant ~net.putX(real_owner,X)
|
||||
invariant (~net.putX(Y,X) | dir.dirty)
|
||||
invariant (~net.putX(Y,X) | dir.head)
|
||||
invariant (~net.put(Y,X) | dir.head)
|
||||
invariant ~net.shwb(X,home)
|
||||
invariant (real_owner = Y | ~net.putX(X,Y))
|
||||
invariant (~rp_net(X) | cache.state_(X) ~= shared)
|
||||
invariant (V0 = home | ~net.putX(V0,V1))
|
||||
invariant (V0 = real_owner | cache.state_(V0) ~= shared)
|
||||
invariant (V1 = home | ~net.fack(V0,V1))
|
||||
invariant (V1 = V0 | ~net.shwb(V0,home) | ~net.shwb(V1,home))
|
||||
invariant (X = dir.hptr | cache.state_(X) ~= exclusive)
|
||||
invariant (X = dir.hptr | ~net.putX(home,X))
|
||||
invariant (X = real_owner | cache.state_(X) ~= exclusive)
|
||||
invariant (X = real_owner | ~net.fack(X,Y))
|
||||
invariant (X = requester | Y = home | ~net.getX(X,Y))
|
||||
invariant (Y = home | ~net.getX(X,Y))
|
||||
invariant (Y = home | ~net.getX(X,Y) | dir.dirty)
|
||||
invariant (Y = home | ~net.getX(X,Y) | dir.head)
|
||||
invariant (Y = home | ~net.get(X,Y) | dir.dirty)
|
||||
invariant (Y = home | ~net.get(X,Y) | dir.head)
|
||||
invariant (Y = home | ~net.putX(Y,X))
|
||||
invariant (Y = home | ~net.putX(Y,X) | dir.dirty)
|
||||
invariant (Y = home | ~net.putX(Y,X) | dir.head)
|
||||
invariant (Y = home | ~net.put(Y,X) | dir.dirty)
|
||||
invariant (Y = home | ~net.shwb(X,Y))
|
||||
invariant (Y = home | Y = real_owner | ~net.getX(X,Y))
|
||||
invariant (Y = home | Y = real_owner | ~net.get(X,Y))
|
||||
invariant (Y = home | Y = real_owner | ~net.putX(Y,X))
|
||||
invariant (Y = home | Y = real_owner | ~net.put(Y,X))
|
||||
invariant (Y = Z | ~net.getX(X,Y) | ~net.getX(X,Z))
|
||||
invariant (Y = Z | ~net.get(X,Y) | ~net.get(X,Z))
|
||||
invariant (Y = Z | ~net.putX(Y,X) | ~net.putX(Z,X))
|
||||
invariant (Y = Z | ~net.put(Y,X) | ~net.put(Z,X))
|
||||
|
||||
|
||||
|
||||
# invariant [net1] ~(net.put(Y,X) & net.put(Z,X) & Y ~= Z)
|
||||
# invariant [net2] ~(net.get(X,Y) & net.get(X,Z) & Y ~= Z)
|
||||
# invariant [net3] ~(net.putX(Y,X) & net.putX(Z,X) & Y ~= Z)
|
||||
# invariant [net4] ~(net.getX(X,Y) & net.getX(X,Z) & Y ~= Z)
|
||||
# invariant [net5] ~(net.put(Y,X) & net.get(X,Z))
|
||||
# invariant [net6] ~(net.putX(Y,X) & net.getX(X,Z))
|
||||
# invariant [n1] ~((net.get(X,Y) + net.put(Y,X)) & nh(Y) & Y ~= home)
|
||||
# invariant [n2] ~((net.getX(X,Y) + net.putX(Y,X)) & nh(Y) & Y ~= home)
|
||||
# invariant [n3] ~(net.get(home,Y) + net.getX(home,Y))
|
||||
# invariant [l1] ~((~dir.head & dir.shlist(X)) + (dir.head & ~dir.shlist(dir.hptr)))
|
||||
# invariant [c2] ~(cache(X).wait = get & cache(X).state_ = shared)
|
||||
# invariant [c3] ~((cache(X).wait ~= get + dir.shlist(X)) & net.get(X,home))
|
||||
# invariant [c4] ~((cache(X).wait ~= get + ~dir.shlist(X)) & net.put(home,X))
|
||||
# invariant [c5] ~((cache(X).wait = get + ~dir.shlist(X)) & cache(X).state_ = shared)
|
||||
# invariant [c6] ~((cache(X).state_ = shared + ~dir.shlist(X)) & rp_net(X))
|
||||
# invariant [r1] ~(net.put(home,X) & rp_net(X))
|
||||
# invariant [c2x] ~(cache(X).wait = getX & cache(X).state_ = exclusive)
|
||||
# invariant [c3x] ~((cache(X).wait ~= getX + dir.shlist(X)) & net.getX(X,home))
|
||||
# invariant [c4x] ~((cache(X).wait ~= getX + ~dir.shlist(X) + X ~= dir.hptr + dir.hptr ~= real_owner) & net.putX(home,X))
|
||||
# invariant [c5x] ~((cache(X).wait = getX + ~dir.shlist(X) + X ~= real_owner) & cache(X).state_ = exclusive)
|
||||
# invariant [pe] ~((net.putX(home,X) + cache(X).state_ = exclusive) & (~dir.head + X ~= dir.hptr))
|
||||
# invariant [c6x] ~((cache(X).state_ = exclusive + ~dir.shlist(wbnet.proc)) & wbnet.wb)
|
||||
# invariant [r1x] ~((net.putX(home,X) + wbnet.proc ~= dir.hptr + cache(real_owner).state_ ~= invalid) & wbnet.wb)
|
||||
# invariant [itp_a] ~(cache.wait(V1) = none & net.getX(V1, V0))
|
||||
# invariant [fa1] ~(net.fack(X,Y) & (X ~= real_owner + X ~= requester))
|
||||
# invariant [itp_b] ~(V0 ~= home & net.putX(V0,V1) & ~dir.pending)
|
||||
# invariant [ro1] ~(net.putX(X,Y) & real_owner ~= Y)
|
||||
# invariant [itp_c]net.putX(real_owner,X)
|
||||
# invariant [misc] ~(~dir.pending + dir.pending + ~dir.dirty + dir.dirty)
|
||||
# invariant [p1] ~(~dir.pending & dir.dirty & dir.hptr ~= real_owner)
|
||||
# invariant [shwb1] ~(net.shwb(X,Y) & Y ~= home)
|
||||
# invariant [shwb2] ~((net.put(X,Y) + cache(Y).state_ = shared) & ~dir.shlist(Y) & (~net.shwb(Y,home) + ~dir.dirty + ~dir.pending))
|
||||
# invariant [itp_d] ~(~V0 = home & net.put(dir.hptr, V0) & ~net.shwb(V0, home))
|
||||
# invariant [itp_e] ~(~V1 = home & net.put(V0, V1) & ~net.shwb(V1, home))
|
||||
# invariant [itp_f] ~(~V1 = V0 & net.shwb(V0, home) & net.shwb(V1, home))
|
||||
# invariant [itp_g] ~(~V1 = home & ~dir.shlist(V1) & net.put(V0, V1))
|
||||
# invariant [itp_h] ~(cache.state_(V0) ~= invalid & (net.get(V0, V1) + net.put(V1,V0)))
|
||||
# invariant [ro2] ~((net.get(Y,X) + net.put(X,Y) + net.getX(Y,X)) & real_owner = Y)
|
||||
# invariant [ro3] ~(cache(Y).state_ ~= exclusive & cache(Y).wait ~= getX & real_owner = Y)
|
||||
# invariant [itp_i] ~(rp_net(V0) & net.put(V1, V0))
|
||||
# invariant [itp_j] ~(cache.wait(V0) ~= get & (net.get(V0, V1) + net.put(V1, V0)))
|
||||
# invariant [itp_j2] ~(cache.wait(V0) ~= getX & (net.getX(V0, V1)+ net.putX(V1, V0)))
|
||||
# invariant [iv1] ~(invack(X) & (invnet(X) + cache(X).state_ ~= invalid + X = real_owner))
|
||||
# invariant [iv2] ~(~dir.real(X) & X ~= real_owner & cache(X).state_ ~= invalid)
|
||||
# invariant [itp_k] ~(~V0 = real_owner & cache.state_(V0) = shared)
|
||||
# invariant [itp_l] ~(invack(V0) & cache.state_(V0) = shared)
|
||||
# invariant [itp_m] ~(~V1 = home & net.fack(V0, V1))
|
||||
# invariant [itp_n = cache.wait]get
|
||||
# invariant [nakc1] ~((nakc + net.fack(requester, home)) & net.getX(X,Y) & Y ~= home)
|
||||
# invariant [getx1] ~((net.getX(X,Y) + net.putX(Y,X)) & Y ~= home & X ~= requester)
|
||||
# invariant [shwb3] ~(net.shwb(X,home) & cache(Y).state_ = exclusive)
|
||||
# invariant [shwb4] ~(net.shwb(X,home) & net.putX(Y,Z))
|
||||
# invariant [itp_o] ~((nakc + ~V0 = requester) & ~dir.shlist(V0) & cache.state_(V0) = exclusive)
|
||||
# invariant [nf1] ~(nakc & net.fack(requester,home))
|
||||
|
|
@ -0,0 +1,493 @@
|
|||
#lang ivy1.7
|
||||
|
||||
type id
|
||||
type cache_state = { invalid, shared, exclusive }
|
||||
type wait_type = { none, get, getX }
|
||||
|
||||
module cache_line = {
|
||||
individual wait : wait_type
|
||||
relation invmarked
|
||||
individual state : cache_state
|
||||
}
|
||||
|
||||
module header = {
|
||||
relation pending
|
||||
relation local_
|
||||
relation dirty
|
||||
relation head
|
||||
individual hptr : id
|
||||
relation list
|
||||
relation real(X:id)
|
||||
relation upgrade
|
||||
relation shlist(X:id)
|
||||
}
|
||||
|
||||
module network = {
|
||||
relation get(S:id,D:id)
|
||||
relation put(S:id,D:id)
|
||||
relation getX(S:id,D:id)
|
||||
relation putX(S:id,D:id)
|
||||
relation nak(S:id,D:id)
|
||||
relation fack(S:id,D:id)
|
||||
relation shwb(S:id,D:id)
|
||||
}
|
||||
|
||||
module wb_network = {
|
||||
individual proc : id
|
||||
relation wb
|
||||
}
|
||||
|
||||
individual home : id
|
||||
instantiate cache(X:id) : cache_line
|
||||
instantiate dir : header
|
||||
relation collecting
|
||||
individual requester : id
|
||||
instantiate net : network
|
||||
relation rp_net(X:id)
|
||||
individual real_owner : id
|
||||
individual fwd_get : wait_type
|
||||
instantiate wbnet : wb_network
|
||||
individual last_WB : id
|
||||
relation nakc
|
||||
relation invnet(X:id)
|
||||
relation invack(X:id)
|
||||
|
||||
# locals used in actions
|
||||
|
||||
individual src : id
|
||||
individual dst : id
|
||||
|
||||
after init {
|
||||
cache(X).state := invalid;
|
||||
cache(X).wait := none;
|
||||
cache(X).invmarked := false;
|
||||
dir.pending := false;
|
||||
dir.dirty := false;
|
||||
collecting := false;
|
||||
net.get(X,Y) := false;
|
||||
net.put(X,Y) := false;
|
||||
net.getX(X,Y) := false;
|
||||
net.putX(X,Y) := false;
|
||||
net.fack(X,Y) := false;
|
||||
net.shwb(X,Y) := false;
|
||||
net.nak(X,Y) := false;
|
||||
dir.list := false;
|
||||
dir.head := false;
|
||||
dir.shlist(X) := false;
|
||||
rp_net(X) := false;
|
||||
fwd_get := none;
|
||||
wbnet.wb := false;
|
||||
real_owner := home;
|
||||
invnet(X) := false;
|
||||
invack(X) := false;
|
||||
nakc := false
|
||||
}
|
||||
|
||||
action pi_Local_Get_dirty = {
|
||||
assume cache(home).state = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume dir.dirty;
|
||||
dir.pending := true;
|
||||
collecting := false;
|
||||
cache(home).wait := get;
|
||||
net.get(home,dir.hptr) := true;
|
||||
requester := home
|
||||
}
|
||||
|
||||
action pi_Local_Get = {
|
||||
assume cache(home).state = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume ~dir.dirty;
|
||||
assume ~cache(home).invmarked;
|
||||
dir.local_ := true;
|
||||
cache(home).state := shared
|
||||
}
|
||||
|
||||
# TODO: can this ever happen?
|
||||
|
||||
action pi_Local_Get_im = {
|
||||
assume cache(home).state = invalid;
|
||||
assume cache(home).wait = none;
|
||||
assume ~dir.pending;
|
||||
assume ~dir.dirty;
|
||||
assume cache(home).invmarked;
|
||||
cache(home).invmarked := false
|
||||
}
|
||||
|
||||
action pi_Remote_Get = {
|
||||
assume src ~= home;
|
||||
assume cache(src).state = invalid;
|
||||
assume cache(src).wait = none;
|
||||
cache(src).wait := get;
|
||||
net.get(src,home) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# action ni_Local_Get_nak = {
|
||||
# assume net.get(src,home);
|
||||
# assume home ~= src;
|
||||
# assume ~rp_net(src);
|
||||
# assume dir.pending | (dir.dirty & dir.local_ & cache(home).state~=exclusive) | (dir.dirty & ~dir.local_ & src = dir.hptr);
|
||||
# net.get(src,home) := false;
|
||||
# net.nak(home,src) := true
|
||||
# }
|
||||
|
||||
# action ni_Local_Get = {
|
||||
# assume net.get(src,home);
|
||||
# assume home ~= src;
|
||||
# assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
|
||||
# net.get(src,home) := false;
|
||||
# net.put(home,src) := true;
|
||||
# if (dir.head) {
|
||||
# dir.list := true;
|
||||
# dir.shlist(src) := true;
|
||||
# dir.real := dir.shlist # what is this?
|
||||
# }
|
||||
# else {
|
||||
# dir.head := true;
|
||||
# dir.hptr := src
|
||||
# }
|
||||
# }
|
||||
|
||||
action ni_Local_Get = {
|
||||
assume net.get(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
|
||||
net.get(src,home) := false;
|
||||
net.put(home,src) := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.shlist(src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Local_Get_fwd = {
|
||||
assume net.get(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr;
|
||||
net.get(src,home) := false;
|
||||
dir.pending := true;
|
||||
net.get(src,dir.hptr) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Remote_Put = {
|
||||
assume dst ~= home;
|
||||
assume net.put(src,dst);
|
||||
net.put(src,dst) := false;
|
||||
cache(dst).wait := none;
|
||||
cache(dst).state := shared;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
# Non-deterministically drop a shared line from the cache. Send an rp message.
|
||||
# informing the directory.
|
||||
|
||||
action pi_Remote_Replace = {
|
||||
assume cache(src).state=shared & cache(src).wait=none & src ~= home;
|
||||
cache(src).state := invalid;
|
||||
rp_net(src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives a replace message, removes sender from sharing list, assuming it is not head.
|
||||
|
||||
action ni_Replace_list = {
|
||||
assume rp_net(src);
|
||||
assume dir.hptr ~= src;
|
||||
rp_net(src) := false;
|
||||
dir.shlist(src) := false;
|
||||
dir.real(src) := false;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Remote is invalid and wants an exclusive copy
|
||||
|
||||
action pi_Remote_GetX = {
|
||||
assume cache(src).state=invalid & cache(src).wait=none & src ~= home;
|
||||
cache(src).wait := getX;
|
||||
net.getX(src,home) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when no invalidation is needed, that is, there is no exclusive
|
||||
# copy and either the sharing list is empty or it contains only the
|
||||
# source.
|
||||
|
||||
action ni_Local_GetX = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty;
|
||||
assume ~dir.head | src = dir.hptr;
|
||||
assume ~dir.head | ~dir.shlist(X) | X = src;
|
||||
net.getX(src,home) := false;
|
||||
dir.dirty := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.real(X) := X = src;
|
||||
dir.shlist(X) := X = src;
|
||||
net.putX(home,src) := true;
|
||||
real_owner := src; # ghost
|
||||
cache(home).state := invalid;
|
||||
cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when the request is nak'd
|
||||
|
||||
action ni_Local_GetX_nak = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume dir.pending | dir.dirty & cache(home).state ~= exclusive | src = dir.hptr;
|
||||
net.getX(src,home) := false;
|
||||
net.nak(home,src) := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when the request is pended.
|
||||
|
||||
action ni_Local_GetX_pend = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr;
|
||||
net.getX(src,home) := false;
|
||||
dir.pending := true;
|
||||
collecting := false;
|
||||
net.getX(src,dir.hptr) := true;
|
||||
fwd_get := getX;
|
||||
requester := src;
|
||||
src := *
|
||||
}
|
||||
|
||||
# Directory receives an exclusive request. This action handles the
|
||||
# case when invalidations are sent out.
|
||||
|
||||
action ni_localGetX_inv = {
|
||||
assume net.getX(src,home);
|
||||
assume home ~= src;
|
||||
assume ~dir.pending & ~dir.dirty & ~dir.local_;
|
||||
assume dir.head;
|
||||
assume src ~= dir.hptr | (dir.shlist(dst) & dst~=src);
|
||||
net.getX(src,home) := false;
|
||||
invnet(X) := X ~= home & X ~= src & dir.shlist(X);
|
||||
collecting := true;
|
||||
# m1 := m;
|
||||
# last_other_invack := (dir.hptr ~= src) ? dir.hptr . {i . i in Proc, dir.shlist(i) & i~=src};
|
||||
cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
|
||||
dir.local_ := false;
|
||||
dir.dirty := true;
|
||||
dir.head := true;
|
||||
dir.hptr := src;
|
||||
dir.pending := true;
|
||||
dir.real(X) := X ~= home & X ~= src & dir.shlist(X);
|
||||
dir.shlist(X) := X = src;
|
||||
net.putX(home,src) := true;
|
||||
real_owner := src;
|
||||
cache(home).state := invalid;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_PutX = {
|
||||
assume net.putX(src,dst);
|
||||
assume dst~=home & cache(dst).wait = getX;
|
||||
net.putX(src,dst) := false;
|
||||
cache(dst).wait :=none;
|
||||
cache(dst).invmarked := false;
|
||||
cache(dst).state :=exclusive;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action pi_Remote_PutX = {
|
||||
assume cache(src).state = exclusive & src ~= home; # cache(src).wait=none ???
|
||||
cache(src).state := invalid;
|
||||
wbnet.proc := src;
|
||||
wbnet.wb := true;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Inv = {
|
||||
assume invnet(dst) & dst~=home;
|
||||
invnet(dst) := false;
|
||||
invack(dst) := true;
|
||||
cache(dst).invmarked := (cache(dst).wait = get) | cache(dst).invmarked;
|
||||
cache(dst).state := invalid;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_InvAck = {
|
||||
assume dir.pending & invack(src) & src~=home;
|
||||
assume dir.real(dst) & dst ~= src;
|
||||
invack(src) := false;
|
||||
dir.real(src) := false;
|
||||
# last_invack := src;
|
||||
# last_other_invack := {i : i in Proc, dir.real(i) & i ~= src};
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_InvAck_last = {
|
||||
assume dir.pending & invack(src) & src~=home;
|
||||
assume ~dir.real(X) | X = src;
|
||||
dir.pending := false;
|
||||
collecting := false;
|
||||
# m1 := undefined; ???
|
||||
invack(src) := false;
|
||||
dir.real(src) := false;
|
||||
# last_invack := src;
|
||||
if ( dir.local_ & ~ dir.dirty) {
|
||||
dir.local_ := false
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
action ni_WB = {
|
||||
assume wbnet.wb;
|
||||
wbnet.wb := false;
|
||||
dir.dirty := false;
|
||||
dir.head := false;
|
||||
dir.shlist(X) := false;
|
||||
last_WB := wbnet.proc
|
||||
}
|
||||
|
||||
action ni_Remote_GetX_nak = {
|
||||
assume net.getX(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
|
||||
net.getX(src,dst) := false;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
nakc := true;
|
||||
net.nak(dst,src) := true;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_GetX_fwd = {
|
||||
assume net.getX(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
|
||||
net.getX(src,dst) := false;
|
||||
cache(dst).state := invalid;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
net.putX(dst,src) := true;
|
||||
real_owner := src;
|
||||
if src~=home {
|
||||
net.fack(src,home) := true
|
||||
};
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_FAck = {
|
||||
assume net.fack(src,home);
|
||||
net.fack(src,home) := false;
|
||||
dir.pending := false;
|
||||
if dir.dirty {
|
||||
dir.hptr := src;
|
||||
dir.shlist(X) := X = src
|
||||
};
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_Remote_Get_nak = {
|
||||
assume net.get(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
|
||||
net.get(src,dst) := false;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
nakc := true;
|
||||
net.nak(dst,src) := true;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_Remote_Get_fwd = {
|
||||
assume net.get(src,dst);
|
||||
assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
|
||||
net.get(src,dst) := false;
|
||||
# assume ~cache(src).invmarked; TODO: ???
|
||||
cache(dst).state := shared;
|
||||
fwd_get := none;
|
||||
# fwd_src := src;
|
||||
net.put(dst,src) := true;
|
||||
if src~=home {
|
||||
real_owner := home;
|
||||
net.shwb(src,home) := true
|
||||
};
|
||||
# shwb_src := dst;
|
||||
src := *;
|
||||
dst := *
|
||||
}
|
||||
|
||||
action ni_ShWB = {
|
||||
assume net.shwb(src,home);
|
||||
net.shwb(src,home) := false;
|
||||
dir.pending := false;
|
||||
dir.dirty := false;
|
||||
dir.shlist(src) := true;
|
||||
dir.real(X) := dir.shlist(X);
|
||||
# last_WB := shwb_src;
|
||||
src := *
|
||||
}
|
||||
|
||||
action ni_NAK_Clear = {
|
||||
assume nakc;
|
||||
dir.pending := false;
|
||||
nakc := false
|
||||
}
|
||||
|
||||
export pi_Local_Get_dirty
|
||||
export pi_Local_Get
|
||||
export pi_Local_Get_im
|
||||
export pi_Remote_Get
|
||||
#export ni_Local_Get_nak
|
||||
#export ni_Local_Get
|
||||
export ni_Local_Get
|
||||
export ni_Local_Get_fwd
|
||||
export ni_Remote_Put
|
||||
export pi_Remote_Replace
|
||||
export ni_Replace_list
|
||||
export pi_Remote_GetX
|
||||
export ni_Local_GetX
|
||||
export ni_Local_GetX_nak
|
||||
export ni_Local_GetX_pend
|
||||
export ni_localGetX_inv
|
||||
export ni_Remote_PutX
|
||||
export pi_Remote_PutX
|
||||
export ni_Inv
|
||||
export ni_InvAck
|
||||
export ni_InvAck_last
|
||||
export ni_WB
|
||||
export ni_Remote_GetX_nak
|
||||
export ni_Remote_GetX_fwd
|
||||
export ni_FAck
|
||||
export ni_Remote_Get_nak
|
||||
export ni_Remote_Get_fwd
|
||||
export ni_ShWB
|
||||
export ni_NAK_Clear
|
||||
|
||||
invariant [coherent]
|
||||
cache(X).state = exclusive -> X = real_owner
|
||||
|
||||
invariant [nodups]
|
||||
cache(X).state = exclusive -> dir.dirty & ~wbnet.wb & ~net.shwb(Y,home)
|
||||
|
||||
invariant net.putX(X,Y) -> Y = real_owner & dir.dirty & ~wbnet.wb & ~net.shwb(Z,home) & cache(Z).state ~= exclusive
|
||||
|
||||
invariant net.shwb(Z,home) -> dir.dirty & ~wbnet.wb & ~net.putX(X,Y) & cache(X).state ~= exclusive
|
||||
|
||||
invariant wbnet.wb -> dir.dirty & ~net.putX(X,Y) & ~net.shwb(Z,home) & cache(X).state ~= exclusive
|
||||
|
||||
invariant net.putX(X,Y) & net.putX(Z,Y) -> X = Z
|
||||
|
||||
invariant net.shwb(X,home) & net.shwb(Z,home) -> X = Z
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,9 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include indexset
|
||||
|
||||
instance bss : unbounded_sequence
|
||||
instance idx : unbounded_sequence
|
||||
instance s : indexset(bss,idx)
|
||||
|
||||
isolate iso = s with idx,bss
|
||||
|
|
@ -0,0 +1,39 @@
|
|||
#lang ivy1.6
|
||||
|
||||
|
||||
type node
|
||||
type value
|
||||
type quorum
|
||||
|
||||
relation member(N:node, Q:quorum)
|
||||
axiom forall Q1:quorum, Q2:quorum. exists N:node. member(N, Q1) & member(N, Q2)
|
||||
|
||||
relation vote(N:node, V:value)
|
||||
relation decision(V:value)
|
||||
|
||||
init ~vote(N,V)
|
||||
init ~decision(V)
|
||||
|
||||
action cast_vote(n:node, v:value) = {
|
||||
assume ~vote(n,V);
|
||||
vote(n, v) := true
|
||||
}
|
||||
|
||||
action decide(v:value, q:quorum) = {
|
||||
assume member(N, q) -> vote(N, v);
|
||||
decision(v) := true
|
||||
}
|
||||
|
||||
export cast_vote
|
||||
export decide
|
||||
|
||||
# safety property:
|
||||
conjecture decision(V1) & decision(V2) -> V1 = V2
|
||||
|
||||
# inductive invariant:
|
||||
conjecture vote(N,V1) & vote(N,V2) -> V1 = V2
|
||||
conjecture decision(V) -> exists Q:quorum. forall N:node. member(N, Q) -> vote(N,V)
|
||||
|
||||
interpret quorum -> bv[2]
|
||||
interpret node -> bv[2]
|
||||
interpret value -> bv[2]
|
||||
|
|
@ -0,0 +1,353 @@
|
|||
|
||||
from parser1 import *
|
||||
from python1 import *
|
||||
|
||||
defwhite = WhiteSpace(RegEx(Unit,'([ \t\n]|(#[^\n]*))*',dflt=' '))
|
||||
|
||||
with defwhite:
|
||||
grammar = Grammar (
|
||||
rules =
|
||||
[ Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'Ident' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = ':' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'type' ) ]
|
||||
) , cls = 'Field' ) , lhs = 'Field' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) , Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Field' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'fields'
|
||||
) , Exact ( text = '}' ) ] ) , cls = 'StructType' ) ,
|
||||
lhs = 'Type' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'type' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Type' ) , fld = 'type' ) ]
|
||||
) , cls = 'TypeDecl' ) , lhs = 'TypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'text' ) ,
|
||||
Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '~' ) ,
|
||||
Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'exp' ) ,
|
||||
Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'RegEx' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'nowhite' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'NoWhite' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'meta' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Meta' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'line' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Line' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'indent' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Indent' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'escape' ) ,
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'spec'
|
||||
) ,
|
||||
Exact ( text = '\'' ) ] ) )
|
||||
,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Escape' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'breakable' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Breakable' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '<' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'fld' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) , Exact ( text = '>' ) ] ) ,
|
||||
cls = 'Assign' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'Exact' ) ,
|
||||
fld = 'delim' ) ) ,
|
||||
Exact ( text = '...' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign ( fmt = Exact ( text = '+' ) ,
|
||||
fld = 'plus' ) ) ,
|
||||
Exact ( text = ']' ) ] ) , cls = 'List' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = ')' ) ] ) , cls = 'Seq' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'cls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Struct' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'name' ) , cls = 'NonTerm' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '?' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'elem' ) ] ) , cls = 'Option' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = '}' ) ] ) , cls = 'Alt' ) ] ) ,
|
||||
lhs = 'Format' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '([^\']|(\\\'\\\'))*' )
|
||||
, fld = 'text' ) , Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) , lhs = 'Exact' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'format' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '[_a-zA-Z0-9]+' )
|
||||
, fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
NonTerm ( name = 'Format' )
|
||||
, fld = 'rhs' ) ] ) ,
|
||||
cls = 'Rule' ) ) , fld = 'rules' ) , cls = 'Grammar'
|
||||
) , lhs = 'Grammar' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign ( fmt = List ( fmt = NonTerm ( name = 'TypeDecl' ) )
|
||||
, fld = 'typedecls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Grammar' ) ,
|
||||
fld = 'grammar' ) , Exact ( text = '>>>' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'Top' ) ,
|
||||
Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'PyIdent' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'PyExpr' ) , fld = 'rhs' ) ]
|
||||
) , cls = 'PyArg' ) , lhs = 'PyArg' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'func' ) ,
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyArg' )
|
||||
, delim = Exact ( text = ',' ) ) ,
|
||||
fld = 'args' ) , Exact ( text = ')' ) ] ) ]
|
||||
) , cls = 'PyApply' ) , lhs = 'PyApply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'elems' )
|
||||
, Exact ( text = ']' ) ] ) , cls = 'PyList' ) ,
|
||||
lhs = 'PyList' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '([^\']|(\\\'\\\'))*' )
|
||||
, fld = 'val' ) , Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'PyStr' ) , lhs = 'PyStr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[ NonTerm ( name = 'PyApply' ) , NonTerm ( name = 'PyIdent' ) ,
|
||||
NonTerm ( name = 'PyList' ) , NonTerm ( name = 'PyStr' ) ] ) ,
|
||||
lhs = 'PyExpr' ) ] )
|
||||
|
||||
class Field(Format):
|
||||
def __init__(self,name,type):
|
||||
self.name,self.type = name,type
|
||||
|
||||
class NamedType(Format):
|
||||
def __init__(self,name):
|
||||
self.name = name
|
||||
|
||||
class StructType(Format):
|
||||
def __init__(self,name):
|
||||
self.name = name
|
||||
|
||||
class TypeDecl(Format):
|
||||
def __init__(self,name,type):
|
||||
self.name,self.type = name,type
|
||||
|
||||
class Top(Format):
|
||||
def __init__(self,typedecls,grammar):
|
||||
self.typedecls,self.grammar = typedecls,grammar
|
||||
|
||||
src = "stage3.src"
|
||||
obj = "stage3.py"
|
||||
with defwhite:
|
||||
with grammar:
|
||||
with PyExprSemantics():
|
||||
thing = parse_file("Top",src)
|
||||
with DefaultSemantics(globals()):
|
||||
with open(obj,"w") as f:
|
||||
f.write("from parser1 import *\n")
|
||||
f.write("from python1 import *\n")
|
||||
for t in thing.find('typedecls').elems:
|
||||
f.write("class {}(Format):\n".format(t.find('name').val))
|
||||
flds = t.find('type').find('fields').elems
|
||||
f.write(" def __init__(self,{}):\n".format(",".join(fl.find('name').val for fl in flds)))
|
||||
for fl in flds:
|
||||
fldnm = fl.find('name').val
|
||||
f.write(" self.{} = {}\n".format(fldnm,fldnm))
|
||||
f.write("with ivywhite: grammar = ")
|
||||
f.write(pretty_to_string("PyExpr",thing.find('grammar')))
|
||||
f.write("\n{}".format(thing.find('code').val))
|
||||
|
|
@ -0,0 +1,585 @@
|
|||
from parser1 import *
|
||||
from python1 import *
|
||||
class Field(Format):
|
||||
def __init__(self,name,type):
|
||||
self.name = name
|
||||
self.type = type
|
||||
class StructType(Format):
|
||||
def __init__(self,fields):
|
||||
self.fields = fields
|
||||
class TypeDecl(Format):
|
||||
def __init__(self,name,type):
|
||||
self.name = name
|
||||
self.type = type
|
||||
class Top(Format):
|
||||
def __init__(self,typedecls,grammar,code):
|
||||
self.typedecls = typedecls
|
||||
self.grammar = grammar
|
||||
self.code = code
|
||||
with ivywhite: grammar = Grammar (
|
||||
rules =
|
||||
[ Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'Ident' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = ':' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'type' ) ]
|
||||
) , cls = 'Field' ) , lhs = 'Field' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) , Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Field' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'fields'
|
||||
) , Exact ( text = '}' ) ] ) , cls = 'StructType' ) ,
|
||||
lhs = 'Type' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'type' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Type' ) , fld = 'type' ) ]
|
||||
) , cls = 'TypeDecl' ) , lhs = 'TypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'func' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
NonTerm ( name = 'Expr'
|
||||
) ,
|
||||
delim = Exact ( text = ',' )
|
||||
) , fld = 'args' ) ,
|
||||
Exact ( text = ')' ) ] ) ) ] ) ,
|
||||
cls = 'Apply' ) , lhs = 'Apply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign (
|
||||
fmt =
|
||||
List ( delim = Exact ( text = '.' ) ,
|
||||
fmt = NonTerm ( name = 'Apply' ) , plus = '+' )
|
||||
, fld = 'apps' ) ] ) , cls = 'Expr' ) , lhs = 'Expr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'text' ) ,
|
||||
Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '~' ) ,
|
||||
Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'exp' ) ,
|
||||
Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'RegEx' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'nowhite' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'NoWhite' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'meta' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Meta' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'line' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Line' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'indent' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Indent' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'escape' ) ,
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\']|(\\\'\\\'))*'
|
||||
) , fld = 'spec'
|
||||
) ,
|
||||
Exact ( text = '\'' ) ] ) )
|
||||
,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Escape' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'breakable' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Breakable' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '<' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'fld' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) , Exact ( text = '>' ) ] ) ,
|
||||
cls = 'Assign' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'Exact' ) ,
|
||||
fld = 'delim' ) ) ,
|
||||
Exact ( text = '...' ) , Exact ( text = ']' ) ]
|
||||
) , cls = 'List' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = ')' ) ] ) , cls = 'Seq' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'cls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Struct' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'var' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) ,
|
||||
fld = 'name' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Expr' ) ,
|
||||
fld = 'value' ) , Exact ( text = 'in' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Var' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '$' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Expr' ) ,
|
||||
fld = 'expr' ) , Exact ( text = '$' ) ] ) ,
|
||||
cls = 'EvalExpr' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'name' ) , cls = 'NonTerm' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '?' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'elem' ) ] ) , cls = 'Option' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = '}' ) ] ) , cls = 'Alt' ) ] ) ,
|
||||
lhs = 'Format' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '([^\']|(\\\'\\\'))*' )
|
||||
, fld = 'text' ) , Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) , lhs = 'Exact' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'format' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '[_a-zA-Z0-9]+' )
|
||||
, fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
NonTerm ( name = 'Format' )
|
||||
, fld = 'rhs' ) ] ) ,
|
||||
cls = 'Rule' ) ) , fld = 'rules' ) , cls = 'Grammar'
|
||||
) , lhs = 'Grammar' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign ( fmt = List ( fmt = NonTerm ( name = 'TypeDecl' ) )
|
||||
, fld = 'typedecls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Grammar' ) ,
|
||||
fld = 'grammar' ) , Exact ( text = '>>>' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'Top' ) ,
|
||||
Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'PyIdent' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'PyExpr' ) , fld = 'value' )
|
||||
] ) , cls = 'MetaField' ) , lhs = 'PyArg' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'cls' ) ,
|
||||
Breakable (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
NonTerm ( name = 'PyArg'
|
||||
) ,
|
||||
delim = Exact ( text = ',' )
|
||||
) , fld = 'args' ) ,
|
||||
Exact ( text = ')' ) ] ) ) ] ) ,
|
||||
cls = 'MetaStruct' ) , lhs = 'PyApply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'elems' )
|
||||
, Exact ( text = ']' ) ] ) , cls = 'MetaList' ) ,
|
||||
lhs = 'PyList' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Escape (
|
||||
fmt =
|
||||
RegEx ( exp = '([^\']|(\\\'\\\'))*'
|
||||
) , spec = '\\\\\'' ) ,
|
||||
fld = 'val' ) , Exact ( text = '\'' ) ] ) ) ,
|
||||
cls = 'MetaString' ) , lhs = 'PyStr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Meta (
|
||||
fmt =
|
||||
Alt (
|
||||
elems =
|
||||
[ NonTerm ( name = 'PyApply' ) , NonTerm ( name = 'PyList' ) ,
|
||||
NonTerm ( name = 'PyStr' ) ] ) ) , lhs = 'PyExpr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'class ' ) ,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyIdent' ) ,
|
||||
fld = 'name' ) ,
|
||||
Exact ( text = '(Format):' ) ] ) ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Indent (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'def __init__(self,'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
List
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Struct
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
)
|
||||
,
|
||||
delim
|
||||
=
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
','
|
||||
)
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'fields'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'):'
|
||||
)
|
||||
] )
|
||||
) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt
|
||||
=
|
||||
Indent
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Line
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Seq
|
||||
(
|
||||
elems
|
||||
=
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'self.'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
' = '
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
) )
|
||||
, fld = 'fields' ) ]
|
||||
) ) , cls = 'StructType' ) ,
|
||||
fld = 'type' ) ] ) , cls = 'TypeDecl' ) ,
|
||||
lhs = 'PyTypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Line ( fmt = Exact ( text = 'from parser1 import *' ) ) ,
|
||||
Assign (
|
||||
fmt = List ( fmt = NonTerm ( name = 'PyTypeDecl' ) ) ,
|
||||
fld = 'typedecls' ) ,
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact (
|
||||
text = 'with ivywhite: grammar = ' )
|
||||
,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
fld = 'grammar' ) ] ) ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'PyTop' ) ] )
|
||||
src = "stage4.src"
|
||||
obj = "stage4.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
|
@ -0,0 +1,43 @@
|
|||
from parser1 import *
|
||||
with ivywhite: grammar = Grammar (
|
||||
rules =
|
||||
[
|
||||
Rule (
|
||||
rhs = List ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) , delim = Exact ( text = '+' ) )
|
||||
, lhs = 'inp' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Var (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
EvalExpr (
|
||||
expr =
|
||||
Expr (
|
||||
apps =
|
||||
[ Apply ( func = 'sum' ) ,
|
||||
Apply (
|
||||
args =
|
||||
[
|
||||
Expr (
|
||||
apps =
|
||||
[
|
||||
Apply (
|
||||
func = 'this' )
|
||||
] ) ] , func = 'add'
|
||||
) ] ) ) ) , name = 'sum' ,
|
||||
value =
|
||||
Expr (
|
||||
apps =
|
||||
[
|
||||
Apply (
|
||||
args = [ Expr ( apps = [ Apply ( func = 'foo' ) ] ) ] ,
|
||||
func = 'set' ) ] ) ) , lhs = 'out' ) ] )
|
||||
src = "test1_inp.txt"
|
||||
obj = "test1_out.txt"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("inp",src)
|
||||
pretty_to_file("out",thing,obj)
|
||||
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
# This is the stage three compiler
|
||||
|
||||
# These are the data type not already resent in the Python preamble
|
||||
# The field types are just placeholders. They are not currently checked.
|
||||
|
||||
type Field = struct
|
||||
{
|
||||
name : str,
|
||||
type : Type
|
||||
}
|
||||
|
||||
type StructType = struct
|
||||
{
|
||||
fields : FieldList
|
||||
}
|
||||
|
||||
type TypeDecl = struct
|
||||
{
|
||||
name : str,
|
||||
type : StructType
|
||||
}
|
||||
|
||||
type Top = struct
|
||||
{
|
||||
typedecls : TypeDeclList,
|
||||
grammar : Grammar,
|
||||
code : str
|
||||
}
|
||||
|
||||
# This is the input format
|
||||
|
||||
format Ident = ~'[_a-zA-Z0-9]+'
|
||||
|
||||
format Field =
|
||||
struct Field ( < name := Ident > ':' < type := Ident > )
|
||||
|
||||
format Type =
|
||||
struct StructType ( 'struct' '{' < fields := [ Field ',' ...] > '}' )
|
||||
|
||||
format TypeDecl =
|
||||
struct TypeDecl ( 'type' < name := Ident > '=' < type := Type> )
|
||||
|
||||
format Format =
|
||||
{
|
||||
struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct RegEx nowhite ( '~' '''' < exp := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct NoWhite ( 'nowhite' < fmt := Format > )
|
||||
struct Meta ( 'meta' < fmt := Format > )
|
||||
struct Line ( 'line' < fmt := Format > )
|
||||
struct Indent ( 'indent' < fmt := Format > )
|
||||
struct Escape ( 'escape' nowhite ( '''' < spec := ~'([^'']|(\''\''))*' > '''' ) < fmt := Format > )
|
||||
struct Breakable ( 'breakable' < fmt := Format > )
|
||||
struct Assign ( '<' < fld := ~'[_a-zA-Z0-9]+' > ':=' < fmt := Format > '>' )
|
||||
struct List ( '[' < fmt := Format > ? < delim := Exact > '...' ']' )
|
||||
struct Seq ( '(' < elems := [ Format ... ] > ')' )
|
||||
struct Struct ( 'struct' < cls := ~'[_a-zA-Z0-9]+' > < fmt := Format > )
|
||||
struct NonTerm < name := ~'[_a-zA-Z0-9]+' > struct Option ( '?' < elem := Format > )
|
||||
struct Alt ( '{' < elems := [ Format ... ] > '}' )
|
||||
}
|
||||
|
||||
format Exact = struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
|
||||
format Grammar =
|
||||
struct Grammar
|
||||
< rules :=
|
||||
[ struct Rule ( 'format' < lhs := ~'[_a-zA-Z0-9]+' > '=' < rhs := Format > ) ... ] >
|
||||
|
||||
format Top =
|
||||
struct Top ( < typedecls := [ TypeDecl ... ] > < grammar := Grammar > '>>>' < code := ~'.*' > )
|
||||
|
||||
# The output format
|
||||
|
||||
format PyIdent = ~'[_a-zA-Z0-9]+'
|
||||
format PyArg = struct MetaField ( < name := PyIdent > '=' < value := PyExpr > )
|
||||
format PyApply = struct MetaStruct ( < cls := PyIdent > breakable ( '(' < args := [ PyArg ',' ... ] > ')' ) )
|
||||
format PyList = struct MetaList ( '[' < elems := [ PyExpr ',' ... ] > ']' )
|
||||
format PyStr = struct MetaString nowhite ( '''' < val := escape '\\''' ~'([^'']|(\''\''))*' > '''' )
|
||||
format PyExpr = meta { PyApply PyList PyStr}
|
||||
|
||||
format PyTypeDecl = struct TypeDecl (
|
||||
line ( 'class ' < name := PyIdent > '(Format):' )
|
||||
< type := struct StructType indent (
|
||||
line ( 'def __init__(self,' < fields := [ struct Field < name := PyIdent > ',' ... ] > '):' )
|
||||
< fields := [ struct Field indent line ( 'self.' < name := PyIdent > ' = ' < name := PyIdent > ) ... ] > ) > )
|
||||
|
||||
format PyTop = struct Top (
|
||||
line 'from parser1 import *'
|
||||
< typedecls := [ PyTypeDecl ... ] >
|
||||
line ( 'with ivywhite: grammar = ' < grammar := PyExpr > )
|
||||
< code := ~'.*' > )
|
||||
|
||||
>>>
|
||||
|
||||
src = "stage5.src"
|
||||
obj = "stage5.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
|
@ -0,0 +1,538 @@
|
|||
from parser1 import *
|
||||
class Field (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class StructType (Format):
|
||||
def __init__(self, fields ):
|
||||
self. fields = fields
|
||||
class TypeDecl (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class Top (Format):
|
||||
def __init__(self, typedecls , grammar , code ):
|
||||
self. typedecls = typedecls
|
||||
self. grammar = grammar
|
||||
self. code = code
|
||||
with ivywhite: grammar = Grammar (
|
||||
rules =
|
||||
[ Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'Ident' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = ':' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'type' ) ]
|
||||
) , cls = 'Field' ) , lhs = 'Field' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) , Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Field' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'fields'
|
||||
) , Exact ( text = '}' ) ] ) , cls = 'StructType' ) ,
|
||||
lhs = 'Type' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'type' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Type' ) , fld = 'type' ) ]
|
||||
) , cls = 'TypeDecl' ) , lhs = 'TypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'text' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '~' ) ,
|
||||
Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'exp' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'RegEx' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'nowhite' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'NoWhite' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'meta' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Meta' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'line' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Line' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'indent' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Indent' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'escape' ) ,
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'spec'
|
||||
) ,
|
||||
Exact ( text = '\'\'' ) ] )
|
||||
) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Escape' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'breakable' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Breakable' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '<' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'fld' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) , Exact ( text = '>' ) ] ) ,
|
||||
cls = 'Assign' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'Exact' ) ,
|
||||
fld = 'delim' ) ) ,
|
||||
Exact ( text = '...' ) , Exact ( text = ']' ) ]
|
||||
) , cls = 'List' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = ')' ) ] ) , cls = 'Seq' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'cls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Struct' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'name' ) , cls = 'NonTerm' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '?' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'elem' ) ] ) , cls = 'Option' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = '}' ) ] ) , cls = 'Alt' ) ] ) ,
|
||||
lhs = 'Format' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx ( exp = '([^\'\']|(\\\'\'\\\'\'))*' )
|
||||
, fld = 'text' ) , Exact ( text = '\'\'' ) ] ) )
|
||||
, cls = 'Exact' ) , lhs = 'Exact' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'format' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '[_a-zA-Z0-9]+' )
|
||||
, fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
NonTerm ( name = 'Format' )
|
||||
, fld = 'rhs' ) ] ) ,
|
||||
cls = 'Rule' ) ) , fld = 'rules' ) , cls = 'Grammar'
|
||||
) , lhs = 'Grammar' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign ( fmt = List ( fmt = NonTerm ( name = 'TypeDecl' ) )
|
||||
, fld = 'typedecls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Grammar' ) ,
|
||||
fld = 'grammar' ) , Exact ( text = '>>>' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'Top' ) ,
|
||||
Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'PyIdent' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'PyExpr' ) , fld = 'value' )
|
||||
] ) , cls = 'MetaField' ) , lhs = 'PyArg' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'cls' ) ,
|
||||
Breakable (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
NonTerm ( name = 'PyArg'
|
||||
) ,
|
||||
delim = Exact ( text = ',' )
|
||||
) , fld = 'args' ) ,
|
||||
Exact ( text = ')' ) ] ) ) ] ) ,
|
||||
cls = 'MetaStruct' ) , lhs = 'PyApply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'elems' )
|
||||
, Exact ( text = ']' ) ] ) , cls = 'MetaList' ) ,
|
||||
lhs = 'PyList' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Escape (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , spec = '\\\\\'\'' ) ,
|
||||
fld = 'val' ) , Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'MetaString' ) , lhs = 'PyStr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Meta (
|
||||
fmt =
|
||||
Alt (
|
||||
elems =
|
||||
[ NonTerm ( name = 'PyApply' ) , NonTerm ( name = 'PyList' ) ,
|
||||
NonTerm ( name = 'PyStr' ) ] ) ) , lhs = 'PyExpr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'class ' ) ,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyIdent' ) ,
|
||||
fld = 'name' ) ,
|
||||
Exact ( text = '(Format):' ) ] ) ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Indent (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'def __init__(self,'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
List
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Struct
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
)
|
||||
,
|
||||
delim
|
||||
=
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
','
|
||||
)
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'fields'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'):'
|
||||
)
|
||||
] )
|
||||
) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt
|
||||
=
|
||||
Indent
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Line
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Seq
|
||||
(
|
||||
elems
|
||||
=
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'self.'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
' = '
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
) )
|
||||
, fld = 'fields' ) ]
|
||||
) ) , cls = 'StructType' ) ,
|
||||
fld = 'type' ) ] ) , cls = 'TypeDecl' ) ,
|
||||
lhs = 'PyTypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Line ( fmt = Exact ( text = 'from parser1 import *' ) ) ,
|
||||
Assign (
|
||||
fmt = List ( fmt = NonTerm ( name = 'PyTypeDecl' ) ) ,
|
||||
fld = 'typedecls' ) ,
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact (
|
||||
text = 'with ivywhite: grammar = ' )
|
||||
,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
fld = 'grammar' ) ] ) ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'PyTop' ) ] )
|
||||
src = "stage6.src"
|
||||
obj = "stage6.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
# This is the stage three compiler
|
||||
|
||||
# These are the data type not already resent in the Python preamble
|
||||
# The field types are just placeholders. They are not currently checked.
|
||||
|
||||
type Field = struct
|
||||
{
|
||||
name : str,
|
||||
type : Type
|
||||
}
|
||||
|
||||
type StructType = struct
|
||||
{
|
||||
fields : FieldList
|
||||
}
|
||||
|
||||
type TypeDecl = struct
|
||||
{
|
||||
name : str,
|
||||
type : StructType
|
||||
}
|
||||
|
||||
type Top = struct
|
||||
{
|
||||
typedecls : TypeDeclList,
|
||||
grammar : Grammar,
|
||||
code : str
|
||||
}
|
||||
|
||||
# This is the input format
|
||||
|
||||
format Ident = ~'[_a-zA-Z0-9]+'
|
||||
|
||||
format Field =
|
||||
struct Field ( < name := Ident > ':' < type := Ident > )
|
||||
|
||||
format Type =
|
||||
struct StructType ( 'struct' '{' < fields := [ Field ',' ...] > '}' )
|
||||
|
||||
format TypeDecl =
|
||||
struct TypeDecl ( 'type' < name := Ident > '=' < type := Type> )
|
||||
|
||||
format Format =
|
||||
{
|
||||
struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct RegEx nowhite ( '~' '''' < exp := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct NoWhite ( 'nowhite' < fmt := Format > )
|
||||
struct Meta ( 'meta' < fmt := Format > )
|
||||
struct Line ( 'line' < fmt := Format > )
|
||||
struct Indent ( 'indent' < fmt := Format > )
|
||||
struct Escape ( 'escape' nowhite ( '''' < spec := ~'([^'']|(\''\''))*' > '''' ) < fmt := Format > )
|
||||
struct Breakable ( 'breakable' < fmt := Format > )
|
||||
struct Assign ( '<' < fld := ~'[_a-zA-Z0-9]+' > ':=' < fmt := Format > '>' )
|
||||
struct List ( '[' < fmt := Format > ? < delim := Exact > '...' ']' )
|
||||
struct Seq ( '(' < elems := [ Format ... ] > ')' )
|
||||
struct Struct ( 'struct' < cls := ~'[_a-zA-Z0-9]+' > < fmt := Format > )
|
||||
struct NonTerm < name := ~'[_a-zA-Z0-9]+' > struct Option ( '?' < elem := Format > )
|
||||
struct Alt ( '{' < elems := [ Format ... ] > '}' )
|
||||
}
|
||||
|
||||
format Exact = struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
|
||||
format Grammar =
|
||||
struct Grammar
|
||||
< rules :=
|
||||
[ struct Rule ( 'format' < lhs := ~'[_a-zA-Z0-9]+' > '=' < rhs := Format > ) ... ] >
|
||||
|
||||
format Top =
|
||||
struct Top ( < typedecls := [ TypeDecl ... ] > < grammar := Grammar > '>>>' < code := ~'.*' > )
|
||||
|
||||
# The output format
|
||||
|
||||
format PyIdent = ~'[_a-zA-Z0-9]+'
|
||||
format PyArg = struct MetaField ( < name := PyIdent > '=' < value := PyExpr > )
|
||||
format PyApply = struct MetaStruct ( < cls := PyIdent > breakable ( '(' < args := [ PyArg ',' ... ] > ')' ) )
|
||||
format PyList = struct MetaList ( '[' < elems := [ PyExpr ',' ... ] > ']' )
|
||||
format PyStr = struct MetaString nowhite ( '''' < val := escape '\\''' ~'([^'']|(\''\''))*' > '''' )
|
||||
format PyExpr = meta { PyApply PyList PyStr}
|
||||
|
||||
format PyTypeDecl = struct TypeDecl (
|
||||
line ( 'class ' < name := PyIdent > '(Format):' )
|
||||
< type := struct StructType indent (
|
||||
line ( 'def __init__(self,' < fields := [ struct Field < name := PyIdent > ',' ... ] > '):' )
|
||||
< fields := [ struct Field indent line ( 'self.' < name := PyIdent > ' = ' < name := PyIdent > ) ... ] > ) > )
|
||||
|
||||
format PyTop = struct Top (
|
||||
line 'from parser1 import *'
|
||||
< typedecls := [ PyTypeDecl ... ] >
|
||||
line ( 'with ivywhite: grammar = ' < grammar := PyExpr > )
|
||||
< code := ~'.*' > )
|
||||
|
||||
>>>
|
||||
|
||||
src = "stage6.src"
|
||||
obj = "stage6.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
|
@ -0,0 +1,538 @@
|
|||
from parser1 import *
|
||||
class Field (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class StructType (Format):
|
||||
def __init__(self, fields ):
|
||||
self. fields = fields
|
||||
class TypeDecl (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class Top (Format):
|
||||
def __init__(self, typedecls , grammar , code ):
|
||||
self. typedecls = typedecls
|
||||
self. grammar = grammar
|
||||
self. code = code
|
||||
with ivywhite: grammar = Grammar (
|
||||
rules =
|
||||
[ Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'Ident' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = ':' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'type' ) ]
|
||||
) , cls = 'Field' ) , lhs = 'Field' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) , Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Field' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'fields'
|
||||
) , Exact ( text = '}' ) ] ) , cls = 'StructType' ) ,
|
||||
lhs = 'Type' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'type' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Type' ) , fld = 'type' ) ]
|
||||
) , cls = 'TypeDecl' ) , lhs = 'TypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'text' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '~' ) ,
|
||||
Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'exp' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'RegEx' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'nowhite' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'NoWhite' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'meta' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Meta' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'line' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Line' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'indent' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Indent' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'escape' ) ,
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'spec'
|
||||
) ,
|
||||
Exact ( text = '\'\'' ) ] )
|
||||
) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Escape' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'breakable' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Breakable' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '<' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'fld' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) , Exact ( text = '>' ) ] ) ,
|
||||
cls = 'Assign' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'Exact' ) ,
|
||||
fld = 'delim' ) ) ,
|
||||
Exact ( text = '...' ) , Exact ( text = ']' ) ]
|
||||
) , cls = 'List' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = ')' ) ] ) , cls = 'Seq' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'cls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Struct' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'name' ) , cls = 'NonTerm' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '?' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'elem' ) ] ) , cls = 'Option' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = '}' ) ] ) , cls = 'Alt' ) ] ) ,
|
||||
lhs = 'Format' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx ( exp = '([^\'\']|(\\\'\'\\\'\'))*' )
|
||||
, fld = 'text' ) , Exact ( text = '\'\'' ) ] ) )
|
||||
, cls = 'Exact' ) , lhs = 'Exact' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'format' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '[_a-zA-Z0-9]+' )
|
||||
, fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
NonTerm ( name = 'Format' )
|
||||
, fld = 'rhs' ) ] ) ,
|
||||
cls = 'Rule' ) ) , fld = 'rules' ) , cls = 'Grammar'
|
||||
) , lhs = 'Grammar' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign ( fmt = List ( fmt = NonTerm ( name = 'TypeDecl' ) )
|
||||
, fld = 'typedecls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Grammar' ) ,
|
||||
fld = 'grammar' ) , Exact ( text = '>>>' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'Top' ) ,
|
||||
Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'PyIdent' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'PyExpr' ) , fld = 'value' )
|
||||
] ) , cls = 'MetaField' ) , lhs = 'PyArg' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'cls' ) ,
|
||||
Breakable (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
NonTerm ( name = 'PyArg'
|
||||
) ,
|
||||
delim = Exact ( text = ',' )
|
||||
) , fld = 'args' ) ,
|
||||
Exact ( text = ')' ) ] ) ) ] ) ,
|
||||
cls = 'MetaStruct' ) , lhs = 'PyApply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'elems' )
|
||||
, Exact ( text = ']' ) ] ) , cls = 'MetaList' ) ,
|
||||
lhs = 'PyList' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Escape (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , spec = '\\\\\'\'' ) ,
|
||||
fld = 'val' ) , Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'MetaString' ) , lhs = 'PyStr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Meta (
|
||||
fmt =
|
||||
Alt (
|
||||
elems =
|
||||
[ NonTerm ( name = 'PyApply' ) , NonTerm ( name = 'PyList' ) ,
|
||||
NonTerm ( name = 'PyStr' ) ] ) ) , lhs = 'PyExpr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'class ' ) ,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyIdent' ) ,
|
||||
fld = 'name' ) ,
|
||||
Exact ( text = '(Format):' ) ] ) ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Indent (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'def __init__(self,'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
List
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Struct
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
)
|
||||
,
|
||||
delim
|
||||
=
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
','
|
||||
)
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'fields'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'):'
|
||||
)
|
||||
] )
|
||||
) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt
|
||||
=
|
||||
Indent
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Line
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Seq
|
||||
(
|
||||
elems
|
||||
=
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'self.'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
' = '
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
) )
|
||||
, fld = 'fields' ) ]
|
||||
) ) , cls = 'StructType' ) ,
|
||||
fld = 'type' ) ] ) , cls = 'TypeDecl' ) ,
|
||||
lhs = 'PyTypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Line ( fmt = Exact ( text = 'from parser1 import *' ) ) ,
|
||||
Assign (
|
||||
fmt = List ( fmt = NonTerm ( name = 'PyTypeDecl' ) ) ,
|
||||
fld = 'typedecls' ) ,
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact (
|
||||
text = 'with ivywhite: grammar = ' )
|
||||
,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
fld = 'grammar' ) ] ) ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'PyTop' ) ] )
|
||||
src = "stage7.src"
|
||||
obj = "stage7.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
# This is the stage three compiler
|
||||
|
||||
# These are the data type not already resent in the Python preamble
|
||||
# The field types are just placeholders. They are not currently checked.
|
||||
|
||||
type Field = struct
|
||||
{
|
||||
name : str,
|
||||
type : Type
|
||||
}
|
||||
|
||||
type StructType = struct
|
||||
{
|
||||
fields : FieldList
|
||||
}
|
||||
|
||||
type TypeDecl = struct
|
||||
{
|
||||
name : str,
|
||||
type : StructType
|
||||
}
|
||||
|
||||
type Top = struct
|
||||
{
|
||||
typedecls : TypeDeclList,
|
||||
grammar : Grammar,
|
||||
code : str
|
||||
}
|
||||
|
||||
# This is the input format
|
||||
|
||||
format Ident = ~'[_a-zA-Z0-9]+'
|
||||
|
||||
format Field =
|
||||
struct Field ( < name := Ident > ':' < type := Ident > )
|
||||
|
||||
format Type =
|
||||
struct StructType ( 'struct' '{' < fields := [ Field ',' ...] > '}' )
|
||||
|
||||
format TypeDecl =
|
||||
struct TypeDecl ( 'type' < name := Ident > '=' < type := Type> )
|
||||
|
||||
format Format =
|
||||
{
|
||||
struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct RegEx nowhite ( '~' '''' < exp := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct NoWhite ( 'nowhite' < fmt := Format > )
|
||||
struct Meta ( 'meta' < fmt := Format > )
|
||||
struct Line ( 'line' < fmt := Format > )
|
||||
struct Indent ( 'indent' < fmt := Format > )
|
||||
struct Escape ( 'escape' nowhite ( '''' < spec := ~'([^'']|(\''\''))*' > '''' ) < fmt := Format > )
|
||||
struct Breakable ( 'breakable' < fmt := Format > )
|
||||
struct Assign ( '<' < fld := ~'[_a-zA-Z0-9]+' > ':=' < fmt := Format > '>' )
|
||||
struct List ( '[' < fmt := Format > ? < delim := Exact > '...' ']' )
|
||||
struct Seq ( '(' < elems := [ Format ... ] > ')' )
|
||||
struct Struct ( 'struct' < cls := ~'[_a-zA-Z0-9]+' > < fmt := Format > )
|
||||
struct NonTerm < name := ~'[_a-zA-Z0-9]+' > struct Option ( '?' < elem := Format > )
|
||||
struct Alt ( '{' < elems := [ Format ... ] > '}' )
|
||||
}
|
||||
|
||||
format Exact = struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
|
||||
format Grammar =
|
||||
struct Grammar
|
||||
< rules :=
|
||||
[ struct Rule ( 'format' < lhs := ~'[_a-zA-Z0-9]+' > '=' < rhs := Format > ) ... ] >
|
||||
|
||||
format Top =
|
||||
struct Top ( < typedecls := [ TypeDecl ... ] > < grammar := Grammar > '>>>' < code := ~'.*' > )
|
||||
|
||||
# The output format
|
||||
|
||||
format PyIdent = ~'[_a-zA-Z0-9]+'
|
||||
format PyArg = struct MetaField ( < name := PyIdent > '=' < value := PyExpr > )
|
||||
format PyApply = struct MetaStruct ( < cls := PyIdent > breakable ( '(' < args := [ PyArg ',' ... ] > ')' ) )
|
||||
format PyList = struct MetaList ( '[' < elems := [ PyExpr ',' ... ] > ']' )
|
||||
format PyStr = struct MetaString nowhite ( '''' < val := escape '\\''' ~'([^'']|(\''\''))*' > '''' )
|
||||
format PyExpr = meta { PyApply PyList PyStr}
|
||||
|
||||
format PyTypeDecl = struct TypeDecl (
|
||||
line ( 'class ' < name := PyIdent > '(Format):' )
|
||||
< type := struct StructType indent (
|
||||
line ( 'def __init__(self,' < fields := [ struct Field < name := PyIdent > ',' ... ] > '):' )
|
||||
< fields := [ struct Field indent line ( 'self.' < name := PyIdent > ' = ' < name := PyIdent > ) ... ] > ) > )
|
||||
|
||||
format PyTop = struct Top (
|
||||
line 'from parser1 import *'
|
||||
< typedecls := [ PyTypeDecl ... ] >
|
||||
line ( 'with ivywhite: grammar = ' < grammar := PyExpr > )
|
||||
< code := ~'.*' > )
|
||||
|
||||
>>>
|
||||
|
||||
src = "stage7.src"
|
||||
obj = "stage7.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
|
@ -0,0 +1,538 @@
|
|||
from parser1 import *
|
||||
class Field (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class StructType (Format):
|
||||
def __init__(self, fields ):
|
||||
self. fields = fields
|
||||
class TypeDecl (Format):
|
||||
def __init__(self, name , type ):
|
||||
self. name = name
|
||||
self. type = type
|
||||
class Top (Format):
|
||||
def __init__(self, typedecls , grammar , code ):
|
||||
self. typedecls = typedecls
|
||||
self. grammar = grammar
|
||||
self. code = code
|
||||
with ivywhite: grammar = Grammar (
|
||||
rules =
|
||||
[ Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'Ident' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = ':' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'type' ) ]
|
||||
) , cls = 'Field' ) , lhs = 'Field' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) , Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Field' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'fields'
|
||||
) , Exact ( text = '}' ) ] ) , cls = 'StructType' ) ,
|
||||
lhs = 'Type' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'type' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Ident' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Type' ) , fld = 'type' ) ]
|
||||
) , cls = 'TypeDecl' ) , lhs = 'TypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Alt (
|
||||
elems =
|
||||
[
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'text' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'Exact' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '~' ) ,
|
||||
Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'exp' ) ,
|
||||
Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'RegEx' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'nowhite' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'NoWhite' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'meta' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Meta' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'line' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Line' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'indent' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Indent' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'escape' ) ,
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , fld = 'spec'
|
||||
) ,
|
||||
Exact ( text = '\'\'' ) ] )
|
||||
) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Escape' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'breakable' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Breakable' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '<' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'fld' ) , Exact ( text = ':=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) , Exact ( text = '>' ) ] ) ,
|
||||
cls = 'Assign' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ,
|
||||
Option (
|
||||
elem =
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'Exact' ) ,
|
||||
fld = 'delim' ) ) ,
|
||||
Exact ( text = '...' ) , Exact ( text = ']' ) ]
|
||||
) , cls = 'List' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = ')' ) ] ) , cls = 'Seq' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'struct' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'cls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'fmt' ) ] ) , cls = 'Struct' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Assign ( fmt = RegEx ( exp = '[_a-zA-Z0-9]+' ) ,
|
||||
fld = 'name' ) , cls = 'NonTerm' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '?' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Format' ) ,
|
||||
fld = 'elem' ) ] ) , cls = 'Option' ) ,
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '{' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'Format' )
|
||||
) , fld = 'elems' ) ,
|
||||
Exact ( text = '}' ) ] ) , cls = 'Alt' ) ] ) ,
|
||||
lhs = 'Format' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx ( exp = '([^\'\']|(\\\'\'\\\'\'))*' )
|
||||
, fld = 'text' ) , Exact ( text = '\'\'' ) ] ) )
|
||||
, cls = 'Exact' ) , lhs = 'Exact' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'format' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp = '[_a-zA-Z0-9]+' )
|
||||
, fld = 'lhs' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
NonTerm ( name = 'Format' )
|
||||
, fld = 'rhs' ) ] ) ,
|
||||
cls = 'Rule' ) ) , fld = 'rules' ) , cls = 'Grammar'
|
||||
) , lhs = 'Grammar' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Assign ( fmt = List ( fmt = NonTerm ( name = 'TypeDecl' ) )
|
||||
, fld = 'typedecls' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'Grammar' ) ,
|
||||
fld = 'grammar' ) , Exact ( text = '>>>' ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'Top' ) ,
|
||||
Rule ( rhs = RegEx ( exp = '[_a-zA-Z0-9]+' ) , lhs = 'PyIdent' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'name' ) ,
|
||||
Exact ( text = '=' ) ,
|
||||
Assign ( fmt = NonTerm ( name = 'PyExpr' ) , fld = 'value' )
|
||||
] ) , cls = 'MetaField' ) , lhs = 'PyArg' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Assign ( fmt = NonTerm ( name = 'PyIdent' ) , fld = 'cls' ) ,
|
||||
Breakable (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '(' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
NonTerm ( name = 'PyArg'
|
||||
) ,
|
||||
delim = Exact ( text = ',' )
|
||||
) , fld = 'args' ) ,
|
||||
Exact ( text = ')' ) ] ) ) ] ) ,
|
||||
cls = 'MetaStruct' ) , lhs = 'PyApply' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '[' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List ( fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
delim = Exact ( text = ',' ) ) , fld = 'elems' )
|
||||
, Exact ( text = ']' ) ] ) , cls = 'MetaList' ) ,
|
||||
lhs = 'PyList' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
NoWhite (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = '\'\'' ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Escape (
|
||||
fmt =
|
||||
RegEx (
|
||||
exp =
|
||||
'([^\'\']|(\\\'\'\\\'\'))*'
|
||||
) , spec = '\\\\\'\'' ) ,
|
||||
fld = 'val' ) , Exact ( text = '\'\'' ) ] ) ) ,
|
||||
cls = 'MetaString' ) , lhs = 'PyStr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Meta (
|
||||
fmt =
|
||||
Alt (
|
||||
elems =
|
||||
[ NonTerm ( name = 'PyApply' ) , NonTerm ( name = 'PyList' ) ,
|
||||
NonTerm ( name = 'PyStr' ) ] ) ) , lhs = 'PyExpr' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Exact ( text = 'class ' ) ,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyIdent' ) ,
|
||||
fld = 'name' ) ,
|
||||
Exact ( text = '(Format):' ) ] ) ) ,
|
||||
Assign (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt =
|
||||
Indent (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'def __init__(self,'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
List
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Struct
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
)
|
||||
,
|
||||
delim
|
||||
=
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
','
|
||||
)
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'fields'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'):'
|
||||
)
|
||||
] )
|
||||
) ,
|
||||
Assign (
|
||||
fmt =
|
||||
List (
|
||||
fmt =
|
||||
Struct (
|
||||
fmt
|
||||
=
|
||||
Indent
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Line
|
||||
(
|
||||
fmt
|
||||
=
|
||||
Seq
|
||||
(
|
||||
elems
|
||||
=
|
||||
[
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
'self.'
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
,
|
||||
Exact
|
||||
(
|
||||
text
|
||||
=
|
||||
' = '
|
||||
)
|
||||
,
|
||||
Assign
|
||||
(
|
||||
fmt
|
||||
=
|
||||
NonTerm
|
||||
(
|
||||
name
|
||||
=
|
||||
'PyIdent'
|
||||
)
|
||||
,
|
||||
fld
|
||||
=
|
||||
'name'
|
||||
)
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
,
|
||||
cls
|
||||
=
|
||||
'Field'
|
||||
) )
|
||||
, fld = 'fields' ) ]
|
||||
) ) , cls = 'StructType' ) ,
|
||||
fld = 'type' ) ] ) , cls = 'TypeDecl' ) ,
|
||||
lhs = 'PyTypeDecl' ) ,
|
||||
Rule (
|
||||
rhs =
|
||||
Struct (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[ Line ( fmt = Exact ( text = 'from parser1 import *' ) ) ,
|
||||
Assign (
|
||||
fmt = List ( fmt = NonTerm ( name = 'PyTypeDecl' ) ) ,
|
||||
fld = 'typedecls' ) ,
|
||||
Line (
|
||||
fmt =
|
||||
Seq (
|
||||
elems =
|
||||
[
|
||||
Exact (
|
||||
text = 'with ivywhite: grammar = ' )
|
||||
,
|
||||
Assign (
|
||||
fmt = NonTerm ( name = 'PyExpr' ) ,
|
||||
fld = 'grammar' ) ] ) ) ,
|
||||
Assign ( fmt = RegEx ( exp = '.*' ) , fld = 'code' ) ] ) ,
|
||||
cls = 'Top' ) , lhs = 'PyTop' ) ] )
|
||||
src = "stage8.src"
|
||||
obj = "stage8.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
# This is the stage three compiler
|
||||
|
||||
# These are the data type not already resent in the Python preamble
|
||||
# The field types are just placeholders. They are not currently checked.
|
||||
|
||||
type Field = struct
|
||||
{
|
||||
name : str,
|
||||
type : Type
|
||||
}
|
||||
|
||||
type StructType = struct
|
||||
{
|
||||
fields : FieldList
|
||||
}
|
||||
|
||||
type TypeDecl = struct
|
||||
{
|
||||
name : str,
|
||||
type : StructType
|
||||
}
|
||||
|
||||
type Top = struct
|
||||
{
|
||||
typedecls : TypeDeclList,
|
||||
grammar : Grammar,
|
||||
code : str
|
||||
}
|
||||
|
||||
# This is the input format
|
||||
|
||||
format Ident = ~'[_a-zA-Z0-9]+'
|
||||
|
||||
format Field =
|
||||
struct Field ( < name := Ident > ':' < type := Ident > )
|
||||
|
||||
format Type =
|
||||
struct StructType ( 'struct' '{' < fields := [ Field ',' ...] > '}' )
|
||||
|
||||
format TypeDecl =
|
||||
struct TypeDecl ( 'type' < name := Ident > '=' < type := Type> )
|
||||
|
||||
format Format =
|
||||
{
|
||||
struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct RegEx nowhite ( '~' '''' < exp := ~'([^'']|(\''\''))*' > '''' )
|
||||
struct NoWhite ( 'nowhite' < fmt := Format > )
|
||||
struct Meta ( 'meta' < fmt := Format > )
|
||||
struct Line ( 'line' < fmt := Format > )
|
||||
struct Indent ( 'indent' < fmt := Format > )
|
||||
struct Escape ( 'escape' nowhite ( '''' < spec := ~'([^'']|(\''\''))*' > '''' ) < fmt := Format > )
|
||||
struct Breakable ( 'breakable' < fmt := Format > )
|
||||
struct Assign ( '<' < fld := ~'[_a-zA-Z0-9]+' > ':=' < fmt := Format > '>' )
|
||||
struct List ( '[' < fmt := Format > ? < delim := Exact > '...' ']' )
|
||||
struct Seq ( '(' < elems := [ Format ... ] > ')' )
|
||||
struct Struct ( 'struct' < cls := ~'[_a-zA-Z0-9]+' > < fmt := Format > )
|
||||
struct NonTerm < name := ~'[_a-zA-Z0-9]+' > struct Option ( '?' < elem := Format > )
|
||||
struct Alt ( '{' < elems := [ Format ... ] > '}' )
|
||||
}
|
||||
|
||||
format Exact = struct Exact nowhite ( '''' < text := ~'([^'']|(\''\''))*' > '''' )
|
||||
|
||||
format Grammar =
|
||||
struct Grammar
|
||||
< rules :=
|
||||
[ struct Rule ( 'format' < lhs := ~'[_a-zA-Z0-9]+' > '=' < rhs := Format > ) ... ] >
|
||||
|
||||
format Top =
|
||||
struct Top ( < typedecls := [ TypeDecl ... ] > < grammar := Grammar > '>>>' < code := ~'.*' > )
|
||||
|
||||
# The output format
|
||||
|
||||
format PyIdent = ~'[_a-zA-Z0-9]+'
|
||||
format PyArg = struct MetaField ( < name := PyIdent > '=' < value := PyExpr > )
|
||||
format PyApply = struct MetaStruct ( < cls := PyIdent > breakable ( '(' < args := [ PyArg ',' ... ] > ')' ) )
|
||||
format PyList = struct MetaList ( '[' < elems := [ PyExpr ',' ... ] > ']' )
|
||||
format PyStr = struct MetaString nowhite ( '''' < val := escape '\\''' ~'([^'']|(\''\''))*' > '''' )
|
||||
format PyExpr = meta { PyApply PyList PyStr}
|
||||
|
||||
format PyTypeDecl = struct TypeDecl (
|
||||
line ( 'class ' < name := PyIdent > '(Format):' )
|
||||
< type := struct StructType indent (
|
||||
line ( 'def __init__(self,' < fields := [ struct Field < name := PyIdent > ',' ... ] > '):' )
|
||||
< fields := [ struct Field indent line ( 'self.' < name := PyIdent > ' = ' < name := PyIdent > ) ... ] > ) > )
|
||||
|
||||
format PyTop = struct Top (
|
||||
line 'from parser1 import *'
|
||||
< typedecls := [ PyTypeDecl ... ] >
|
||||
line ( 'with ivywhite: grammar = ' < grammar := PyExpr > )
|
||||
< code := ~'.*' > )
|
||||
|
||||
>>>
|
||||
|
||||
src = "stage8.src"
|
||||
obj = "stage8.py"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("Top",src)
|
||||
pretty_to_file("PyTop",thing,obj)
|
||||
|
|
@ -0,0 +1,15 @@
|
|||
# This is a test of Eval
|
||||
|
||||
format inp = [ ~'[_a-zA-Z0-9]+' '+' ... ]
|
||||
|
||||
format out = var sum := set() [ $ sum.add(this) $ ... ]
|
||||
|
||||
>>>
|
||||
|
||||
src = "test1_inp.txt"
|
||||
obj = "test1_out.txt"
|
||||
with ivywhite:
|
||||
with grammar:
|
||||
with DefaultSemantics(globals()):
|
||||
thing = parse_file("inp",src)
|
||||
pretty_to_file("out",thing,obj)
|
||||
|
|
@ -0,0 +1,190 @@
|
|||
# coding: utf-8
|
||||
import ivy_init
|
||||
import ivy_logic as il
|
||||
import ivy_module as im
|
||||
import ivy_utils as iu
|
||||
import ivy_actions as ia
|
||||
import logic as lg
|
||||
import logic_util as lu
|
||||
import ivy_logic_utils as ilu
|
||||
import ivy_compiler as ic
|
||||
import ivy_isolate as iso
|
||||
import ivy_ast
|
||||
import itertools
|
||||
import ivy_theory as ith
|
||||
|
||||
things = []
|
||||
|
||||
preamble = """
|
||||
import .ivy_pl
|
||||
namespace ivy
|
||||
open ivy_logic
|
||||
|
||||
"""
|
||||
|
||||
postamble = """
|
||||
|
||||
end ivy
|
||||
"""
|
||||
|
||||
def emit(str):
|
||||
things.append(str)
|
||||
|
||||
def emit_eol():
|
||||
emit("\n")
|
||||
|
||||
def sort_to_string(sort):
|
||||
if isinstance(sort,lg.UninterpretedSort):
|
||||
return '(sort.ui "' + sort.name + '")'
|
||||
elif isinstance(sort,lg.BooleanSort):
|
||||
return "sort.bool"
|
||||
elif isinstance(sort,lg.FunctionSort):
|
||||
return ('(' + ' × '.join(sort_to_string(s) for s in sort.domain) + ' ↦ ' +
|
||||
sort_to_string(sort.range) + ')')
|
||||
else:
|
||||
raise iu.IvyError(None,"enumerated sorts not supported yet")
|
||||
|
||||
def emit_symbol_def(sym):
|
||||
emit('def ' + sym.name + ' := mk_cnst "' + sym.name + '" ' + sort_to_string(sym.sort))
|
||||
emit_eol()
|
||||
|
||||
def emit_expr(f):
|
||||
if isinstance(f,lg.Var):
|
||||
emit('("'+f.name+'",'+sort_to_string(f.sort)+')')
|
||||
elif isinstance(f,lg.Const):
|
||||
emit(f.name)
|
||||
elif isinstance(f,lg.Apply):
|
||||
emit(f.name + '(')
|
||||
first = True
|
||||
for x in f.terms:
|
||||
if not first:
|
||||
emit(',')
|
||||
emit_expr(x)
|
||||
first = False
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Eq) or isinstance(f,lg.Iff):
|
||||
emit('(fmla.eq ')
|
||||
emit_expr(f.terms[0])
|
||||
emit(' ')
|
||||
emit_expr(f.terms[1])
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Ite):
|
||||
emit('(ite_fmla ')
|
||||
for idx in range(3):
|
||||
emit(' ')
|
||||
emit_expr(f.terms[idx])
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Not):
|
||||
emit('¬')
|
||||
emit_expr(f.body)
|
||||
elif isinstance(f,lg.And) or isinstance(f,lg.Or):
|
||||
if len(f.terms) == 0:
|
||||
emit('ltrue' if isinstance(f,lg.And) else 'lfalse')
|
||||
else:
|
||||
emit ('(')
|
||||
first = True
|
||||
for x in f.terms:
|
||||
if not first:
|
||||
emit('∧' if isinstance(f,lg.And) else '∨')
|
||||
emit_expr(x)
|
||||
first = False
|
||||
emit (')')
|
||||
elif isinstance(f,lg.Implies):
|
||||
emit('(')
|
||||
emit_expr(f.terms[0])
|
||||
emit(' ⇒ ')
|
||||
emit_expr(f.terms[1])
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Forall):
|
||||
emit('¬')
|
||||
for v in f.variables:
|
||||
emit('(fmla.proj ')
|
||||
emit_expr(v)
|
||||
emit(' ')
|
||||
emit('¬')
|
||||
emit_expr(f.body)
|
||||
for v in f.variables:
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Exists):
|
||||
for v in f.variables:
|
||||
emit('(fmla.proj ')
|
||||
emit_expr(v)
|
||||
emit(' ')
|
||||
emit_expr(f.body)
|
||||
for v in f.variables:
|
||||
emit(')')
|
||||
elif isinstance(f,lg.Lambda):
|
||||
for v in f.variables:
|
||||
emit('(fmla.lambda ')
|
||||
emit_expr(v)
|
||||
emit(' ')
|
||||
emit_expr(f.body)
|
||||
for v in f.variables:
|
||||
emit(')')
|
||||
|
||||
def emit_action(a):
|
||||
if isinstance(a,ia.AssignAction):
|
||||
vars = [(x if isinstance(x,lg.Variable) else lg.Variable('$V'+ str(idx)))
|
||||
for x,idx in enumerate(a.args[0].args)]
|
||||
emit(' ' + a.args[0].rep.name + ' ::= ')
|
||||
rhs = a.args[1]
|
||||
if len(vars) != 0:
|
||||
cond = lg.And(*[lg.Eq(v,w) for v,w in zip(vars,a.args[0].args) if v != w])
|
||||
rhs = lg.Ite(cond,rhs,lg.Apply(a.func,vars))
|
||||
emit_expr(rhs)
|
||||
elif isinstance(a,ia.Sequence):
|
||||
emit('(')
|
||||
first = True
|
||||
for x in a.args:
|
||||
if not first:
|
||||
emit(';\n')
|
||||
emit_action(x)
|
||||
first = False
|
||||
emit (')')
|
||||
elif isinstance(a,ia.IfAction):
|
||||
emit('(PL.pterm.ite ')
|
||||
emit_expr(a.args[0])
|
||||
emit_action(a.args[1])
|
||||
if len(a.args) > 2:
|
||||
emit_action(a.args[1])
|
||||
else:
|
||||
emit('PL.pterm.skip')
|
||||
else:
|
||||
raise iu.IvyError(a,'action not supported yet')
|
||||
|
||||
|
||||
def main():
|
||||
with im.Module():
|
||||
ivy_init.ivy_init(create_isolate=False)
|
||||
emit(preamble)
|
||||
for sym in il.all_symbols():
|
||||
emit_symbol_def(sym)
|
||||
emit('def P := (PL.prog.letrec')
|
||||
emit_eol()
|
||||
for name,act in im.module.actions.iteritems():
|
||||
emit(' (@bndng.cons PL.pterm ("'+name+'",\n')
|
||||
emit_action(act)
|
||||
emit_eol()
|
||||
emit(' ) ')
|
||||
emit_eol()
|
||||
emit(' (bndng.default PL.pterm.skip)')
|
||||
for name,act in im.module.actions.iteritems():
|
||||
emit(')')
|
||||
emit_eol()
|
||||
exports = sorted(list(im.module.public_actions))
|
||||
if len(exports) == 0:
|
||||
emit('PL.pterm.skip')
|
||||
else:
|
||||
emit('(('+ ' + '.join('(PL.pterm.call "'+x+'")' for x in exports) + ')**))')
|
||||
emit(postamble)
|
||||
basename = im.module.name
|
||||
f = open(basename+'.lean','w')
|
||||
f.write("".join(things))
|
||||
f.close()
|
||||
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
import ivy_lexer
|
||||
import sys
|
||||
|
||||
f = open(sys.argv[1],'r')
|
||||
ivy_lexer.lexer.input(f.read())
|
||||
|
||||
count = 0
|
||||
|
||||
while True:
|
||||
tok = ivy_lexer.lexer.token()
|
||||
if not tok:
|
||||
break # No more input
|
||||
count += 1
|
||||
|
||||
print count
|
||||
|
||||
Загрузка…
Ссылка в новой задаче