/home_Python/note_/VDM/vdmSeq.py

｜INDEX｜ Python.use(better)

》作業中です《

from vdmSet import *
from vdmMap import *
#....+....1....+....2....+....3....+....4....+....5....+....6....+....7....+

# ==========
def hd(seq):
    """
    hd l
        ; seq1 of A -> A
        ;
        ; Head
        ;   yields the first element of l. l must be a non- 
        ;   empty sequence. 
    """
    assert _pre_Head(seq)
    return seq.list[0]
def _pre_Head(seq):
    assert len(seq) > 0,(
        "::: hd %s \n"
            %(seq)+
        ":::\t len(>>%s<<) > 0 \n"
            %(seq)+
        ":::\t hd l: l must be a nonempty sequence"
        )
    return True

# ==========
def tl(seq):
    """tl l
        ; seq1 of A -> seq of A
        ;
        ; Tail
        ;   yields the subsequence of l where the first element 
        ;   is removed. l must be a non-empty sequence.
    """
    assert _pre_Tail(seq)
    return VDM_Seq(seq.list[1:])
def _pre_Tail(seq):
##    print len(seq),"<<<<<<"
    assert len(seq) > 0,(
        "::: tl %s \n"
            %(seq)+
        ":::\t len(>>%s<<) > 0 \n"
            %(seq)+
        ":::\t hd l: l must be a nonempty sequence"
        )
    return True

# ==========
def elems(seq):
    """
    elems l
        ; seq of A -> set of A
        ;
        ; Elements
        ;   yields the set containing all the elements of l.
    """
    return VDM_Set(seq.list)

# ==========
def inds(seq):
    """
    inds l
        ; seq of A -> set of nat1
        ;
        ; Indexes
        ;   yields the set of indexes of l, i.e. the set 
        ;   {1,...,len l}. 
    """
    return VDM_Set(range(1,len(seq)+1))

# ==========
def conc(seq):
    """
    conc ll
        ; seq of seq of A -> seq of A
        ;
        ; Distributed concatenation
        ;   yields the sequence where the elements (these are 
        ;   sequences themselves) of ll are concatenated: the 
        ;   first and the second, and then the third, etc. 
    """
    return VDM_Seq(_Distributed_concatenation(seq))
def _Distributed_concatenation(seq):
    s = 
    for e in seq.list:
        s += e.list[:]
    return s

# ----------
class VDM_Seq:
    def __init__(self,enclosure=None):
        self.list = self._list(enclosure)
    def _list(self,enclosure):
        if enclosure is None: return 
        return enclosure

    def __str__(self):
        s = ""
        for e in self.list:
            s += "%s, "%e
        return "[%s]"%s[:len(s)-2]

    def copy(self):
        s = VDM_Seq()
        s.list = self.list[:]
        return s

# ==========
    def __len__(seq):
        """
        len l
            ; seq of A -> nat
            ;
            ; Length
            ;   yields the length of l.
        """
        return len(seq.list)

# ==========
    def __xor__(s1,s2):
        """
        l1 ^ l2
            ; seq of A * seq of A -> seq of A
            ;
            ; Concatenation
            ;   yields the concatenation of l1 and l2, i.e. the se- 
            ;   quence consisting of the elements of l1 followed by 
            ;   those of l2, in order. 
        """
        return VDM_Seq(s1.list + s2.list)

    def mconc(seq):
        s = VDM_Seq()
        s.list = seq._mconc()
        return s
    def _mconc(seq):
        if len(seq) == 0: return []
        head = hd(seq); tail = tl(seq)
        if head.__class__ != VDM_Seq:
            return [head] + tail._mconc()
        else:
            return head._mconc() + tail._mconc()

# ==========
    def __add__(s,m):
        """
        l ++ m
            ; seq of A * map nat1 to A -> seq of A 
            ;
            ; Sequence modification
            ;   the elements of l whose indexes are in the domain of
            ;   m are modified to the range value that the index maps
            ;   into. dom m must be a subset of inds l 
        """
        assert s._pre_Sequence_modification(m)
        return VDM_Seq(s._Sequence_modification(m))
    def _pre_Sequence_modification(s,m):
        s1,s2 = dom(m),inds(s)
        assert s1.subset(s2),(
            "::: %s ++ %s \n"
                %(s,m)+
            ":::\t (>>%s<<).subset.(>>%s<<)\n"
                %(s1,s2)+
            ":::\t l ++ m: dom m must be a subset of inds l"
            )
        return True
    def _Sequence_modification(seq,m):
        s = seq.list[:]
        for k,v in m.dict.items():
            s[k] = v
        return s

# ==========
    def __getitem__(seq,key):
        """
        l(i)
            ; seq of A * nat1 -> A
            ;
            ; Sequence application
            ;   yields the element of index from l. i must be in 
            ;   the indexes of l. 
        """
        assert seq._pre_Sequence_application(key)
        return seq.list[key-1]
    def _pre_Sequence_application(s,i):
        ind = inds(s)
        assert i in ind,(
            "::: %s(%s)\n"
                %(s,i)+
            ":::\t (>>%s<<) in %s\n"
                %(i,ind)+
            ":::\t l(i): i must be in the indexes of l"
            )
        return True

# ==========
    def __eq__(s1,s2):
        """
        l1 = l2
            ; seq of A * seq of A -> bool
            ;
            ; Equality
        """
        if len(s1) <> len(s2): return False
        return s1.list == s2.list

# ==========
    def __ne__(s1,s2):
        """
        l1 <> l2
            ; seq of A * seq of A -> bool
            ;
            ; Inequality
        """
        return not s1 == s2

# ----------
from Ex import *
signature("-",__file__,'1.0.1b')
#....+....1....+....2....+....3....+....4....+....5....+....6....+....7....+

Last updated♪2010/03/12