some fixes in terms of map

Mainly, make a intermediate function to get the keys we want. 
ok


On Fri, Jun 6, 2014 at 6:10 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
>
> Something like this is what I mean:
>
> rule hasUnionMarker(Loc:SymLoc) => #hasUnionMarker(.K, Loc) ==K true
>
> rule #hasUnionMarker(.K, loc(_, _, SetItem(K:K) Prov:Set) => #hasUnionMarker(K, Prov)
> rule #hasUnionMarker(K:K, Prov:Set) => #hasUnionMarker(.K, Prov)
> when  getKLabel(K) =/=KLabel 'fromUnion
> rule #hasUnionMarker(fromUnion(_, _, _), _) => true
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/c-semantics/pull/10/files#r13514838>.
>