some fixes in terms of map

Mainly, make a intermediate function to get the keys we want. 
How does it work?

Since if I use #hasUnionMarker. The #hasUnionMarker function still need to
consider the case when the Set is empty and use the third function to
separate the function into two parts.


On Fri, Jun 6, 2014 at 3:31 PM, Chris Hathhorn <notifications@github.com>
wrote:

> In semantics/language/common/symloc.k:
>
> > @@ -267,19 +267,42 @@ module C-SYMLOC
> >       syntax Bool ::= "#isBases" "(" Provenance ")" [function, klabel('#isBases)]
> >       rule #isBases(basedOn(_)) => true
> >
> > -     rule hasUnionMarker(Loc:SymLoc) => #hasUnionMarker(Loc) ==K true
> > -
> > -     syntax Bool ::= #hasUnionMarker(SymLoc) [function]
> > -     rule #hasUnionMarker(loc(_, _, SetItem(fromUnion(_, _, _)) _)) => true
> > -
> > -     rule isFromArray(Loc:SymLoc) => #isFromArray(Loc) ==K true
> > -
> > -     syntax Bool ::= "#isFromArray" "(" SymLoc ")" [function]
> > -     rule #isFromArray(loc(_, _, SetItem(fromArray(_, _)) _)) => true
> > -
> > -     rule stripFromArray(loc(_, _, (SetItem(fromArray(_, _)) => .Set) _))
> > -     rule stripFromArray(Loc:SymLoc) => Loc
> > -          when notBool isFromArray(Loc)
> > +     rule hasUnionMarker(loc(_,_,.Set)) => false
> > +     rule hasUnionMarker(loc(_,_,SetItem(K:K) S:Set)) => #hasUnionMarker(K,S) ==K true
>
> No, "blah" was an example. Like "foo." The solution is to leave the "blah"
> rules in the form:
>
> rule blah(Loc:SymLoc) => #blah(Loc) ==K true
>
> And then do all pattern matching in the rules for "#blah" -- then you
> don't even need to consider the 2-argument case (in these particular rules).
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/c-semantics/pull/10/files#r13508924>.
>