Quelle pat.vdmsl Sprache: unbekannt

\section{Loose Pattern Matching}

The operation $PatternMatch$ takes a syntactic pattern and a semantic value as
input, and returns the set of possible block environments. In each block
environment the identifiers defined in the input pattern are bound to
the corresponding value from the input semantic value. An empty return set
indicates that no matching can be performed.

\begin{vdm_al}
operations

  PatternMatch : Pattern * VAL ==> set of BlkEnv
  PatternMatch (pat_p, val_v) ==
    cases true:
     (is_PatternName(pat_p))     -> let mk_PatternName(id) = pat_p in
                                       return { MkBlkEnv(id, val_v) },
     (is_MatchVal(pat_p))        -> let lval = LooseEvalExpr(pat_p.val)
                                    in
          (for all mk_(v,m) in set lval do
            if v = val_v
     then return { MkEmptyBlkEnv()};
                  return {}),
     (is_SetEnumPattern(pat_p))  -> MatchSetEnumPattern(pat_p, val_v),
     (is_SetUnionPattern(pat_p)) -> MatchSetUnionPattern(pat_p, val_v),
     others -> error
    end;
\end{vdm_al}
Concerning match values it should be noted that the definition given
above is not entirely correct. In fact the model which are used for
the model should be returned as well, but we have abstracted away from
this for the moment because that would change the usage of the
$PatternMatch$ operation all places. Naturally, the model assumptions
used in the match value should be taken into account in the expression
evaluation function where the pattern occurs.

Note that the $MkBlkEnv$ operation takes into account whether we
are currently matching inside a function body, and if so adds the
relevant information to the unique identifier which is used in the
block environment.

\begin{vdm_al}

MatchSetEnumPattern : SetEnumPattern * VAL ==> set of BlkEnv
MatchSetEnumPattern ( mk_SetEnumPattern(elems_lp), val_v) ==
if is_SET(val_v)
then let mk_SET(val_sv) = val_v in
       if card val_sv = card elems elems_lp
       then let perm_slv = Permute(SetToSeq(val_sv)) in
              return dunion { MatchLists(elems_lp, tmp_lv) |
                              tmp_lv in set perm_slv }
       else return {}
else return {};
\end{vdm_al}

This operation returns the set of all possible binding environments.
The main condition for matching a set enumeration pattern is that the
value is a set value and then that the cardinality of the value
corresponds to the number of elements in the set enumeration pattern. We
first create the set of all permutations of the input semantic value.
The distributed union of all matches of the input pattern list with
the elements from the permutation is returned when a successful
match is found.

\begin{vdm_al}
MatchSetUnionPattern : SetUnionPattern * VAL ==> set of BlkEnv
MatchSetUnionPattern ( mk_SetUnionPattern(lp_p, rp_p), val_v) ==
( dcl envres_sl : set of BlkEnv := {};
  if is_SET(val_v)
  then let mk_SET(val_sv) = val_v in
       ( for all mk_(setl_sv, setr_sv) in set
               { mk_(setl_sv,setr_sv) |
                 setl_sv ,setr_sv in set power val_sv &
                   (setl_sv union setr_sv = val_sv ) and
                   (setl_sv inter setr_sv = {}) } do
           let envl_s = PatternMatch(lp_p, mk_SET(setl_sv)),
               envr_s = PatternMatch(rp_p, mk_SET(setr_sv)) in
             if envl_s <> {} and envr_s <> {}
             then let tmpenv = { CombineBlkEnv(tmp1, tmp2) |
                                 tmp1 in set envl_s, tmp2 in set envr_s }
                  in
                    envres_sl := envres_sl union UnionMatch(tmpenv);
         return envres_sl
       )
  else return {}
);
\end{vdm_al}

In the case of a set union pattern, we first create all pairs of set
values, for which the union is equal to the original input set value, but
are still disjoint. For each pair, we create two sets of binding
environments. These are combined, and inserted into the resulting set of
binding environments after duplicate entries are removed\footnote{Here
it is worth noting that the disjointness criterion which has been
used for both set enumeration patterns and for set comprehension
patterns no longer conforms to the semantics given in the
standard. However, we have decided to retain this here because we have
not yet been able to find any examples where one would like such
patterns to be non-disjoint.}. $UnionMatch$ also ensures that pattern
identifiers which occur multiple times are consistently bound to the
same value everywhere.

\begin{vdm_al}
MatchLists : seq of Pattern * seq of VAL ==> set of BlkEnv
MatchLists (els_lp, val_lv) ==
let tmp_ls = [ PatternMatch(els_lp(i), val_lv(i)) |
                i in set inds els_lp ] in
   if {} not in set elems tmp_ls
   then let perm_s = SeqOfSetOf2SetOfSeqOf(tmp_ls) in
          UnionMatch({ conc l | l in set perm_s })
   else return {};
\end{vdm_al}

For each element from the input pattern sequence, we create a set of
binding environments by matching the pattern with the corresponding element
from the input value sequence. If all elements match, each set of
environments from the sequence $tmp-ls$ is merged into a set with one
single environment.

\begin{vdm_al}
UnionMatch : set of BlkEnv ==> set of BlkEnv
UnionMatch (blk_sl) ==
return { StripDoubles(blk_l) |
         blk_l in set blk_sl &
           forall mk_(id1,v1_v) in seq blk_l,
                  mk_(id2,v2_v) in seq blk_l &
                  SelName(id1) = SelName(id2) => (v1_v = v2_v)};
\end{vdm_al}

This operation removes duplicates from a single environment.

\begin{vdm_al}
StripDoubles : BlkEnv ==> BlkEnv
StripDoubles (blk_l) ==
( dcl tmpblk_l : BlkEnv := blk_l,
      res_l : BlkEnv := [];
  while tmpblk_l <> [] do
    let mk_(id,val_v) = hd tmpblk_l in
    ( if not exists mk_(id1 ,-) in seq tl tmpblk_l & id1 = id
      then res_l := CombineBlkEnv(res_l, MkBlkEnv(SelNameAndPos(id), val_v));
      tmpblk_l := tl tmpblk_l
    );
  return res_l
);
\end{vdm_al}

This operation removes duplicate bindings from an environment. Only the
first binding is kept.

\begin{vdm_al}
EvalBind : Bind ==> set of (BlkEnv * Model)
EvalBind (bind) ==
EvalSetBind(bind);
\end{vdm_al}

This operation is used to evaluate a binding.

\begin{vdm_al}
EvalSetBind : SetBind ==> set of (BlkEnv * Model)
EvalSetBind ( mk_SetBind(pat_p ,set_e )) ==
( dcl env_s : set of (BlkEnv * Model) := {};
  let set_lv = LooseEvalExpr(set_e) in
   (for all mk_(set_v,m) in set set_lv do
     (if is_SET(set_v)
      then let mk_SET(set_sv) = set_v in
           ( for all elm_v in set set_sv do
               (let new_envs = PatternMatch(pat_p, elm_v) in
                env_s := env_s union {mk_(env,m) | env in set new_envs})
           )
      else error);
    return env_s)
)
\end{vdm_al}

This operation returns the set of binding environments for the pattern and
all the elements of the set expression.

quality95%

Quelle pat.vdmsl Sprache: unbekannt

[ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ]