some fixes in terms of map

Mainly, make a intermediate function to get the keys we want. 
Basically, I almost never use "=> false" because I like all my predicates
to be total functions by default.


On Fri, Jun 6, 2014 at 6:11 PM, Liyi Li <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
>
> ok
> … <#14673739335c0fe3_>
> 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>.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/c-semantics/pull/10/files#r13514861>.
>