| << Prev | - Up - | Next >> |
DG_Lattice.oz We now turn to the library support for composable lattices.
functor
import FS
export Base Flat Domain Cartesian Avm Set AccumulatingSet
define
%%
%% a lattice has top, bottom, and values. values can be represented
%% either in decoded form (user oriented) or encoded form (e.g. an
%% integer or a set value). encoded values can be combined using
%% lub and glb operations.
%%
Top = {NewName}
Bot = {NewName}
class Base
feat decode encode
attr top bot
meth init
top <- Top
bot <- Bot
self.decode = fun {$ I} {self decode(I $)} end
self.encode = fun {$ V} {self encode(V $)} end
end
meth top($) @top end
meth bot($) @bot end
meth lub(_ _ _) Base,notImplemented(lub ) end
meth glb(_ _ _) Base,notImplemented(glb ) end
meth encode(_ _) Base,notImplemented(encode) end
meth decode(_ _) Base,notImplemented(decode) end
meth notImplemented(Meth)
{Exception.raiseError lattice(notImplemented(Meth))}
end
meth lubN(L $)
{FoldL L fun {$ Accu X} {self lub(Accu X $)} end @bot}
end
meth glbN(L $)
{FoldL L fun {$ Accu X} {self glb(Accu X $)} end @top}
end
end
%%
%% just 1 flat level with all ground values, possibly infinitely
%% may of them
%%
class Flat from Base
meth lub(X Y $)
if X==@bot then Y
elseif Y==@bot then X
elseif X==Y then X
else @top end
end
meth glb(X Y $)
if X==@top then Y
elseif Y==@top then X
elseif X==Y then X
else @bot end
end
end
%%
%% a Domain is a Flat lattice with finitely many values
%% identified by atoms and integers.
%%
class Domain from Flat
feat card values val2int int2val val2ints
meth init(L)
Flat,init
self.card = {Length L}
self.values = L
self.val2int = {List.toRecord o
{List.mapInd L fun {$ I V} V#I-1 end}}
self.int2val = {List.toRecord o
{List.mapInd L fun {$ I V} I-1#V end}}
self.val2ints = {Record.map self.val2int fun {$ V} [V] end}
end
meth encode(V $) self.val2int.V end
meth decode(I $) self.int2val.I end
end
%%
fun {Map2 L1 L2 F}
case L1#L2 of nil#nil then nil
[] (H1|T1)#(H2|T2) then {F H1 H2}|{Map2 T1 T2 F} end
end
%%
class Cartesian from Flat
feat axes card val2ints
meth init(L)
Flat,init
self.axes = L
self.card = if L==nil then 0 else
{FoldL L fun {$ N Axis} N*Axis.card end 1}
end
self.val2ints = {ByNeed fun {$} Cartesian,MkVal2Ints($) end}
end
meth encode(Vs $)
{self encodeInts({Map2 Vs self.axes
fun {$ V Axis} {Axis.encode V} end} $)}
end
meth encodeInts(Is $)
Cartesian,EncodeInternal(Is self.axes 1 $)
end
meth EncodeInternal(Is Axes K $)
case Is#Axes
of nil#nil then 0
[] (I|Is)#(Axis|Axes) then
I*K + Cartesian,EncodeInternal(Is Axes K*Axis.card $)
end
end
meth decode(I $)
Cartesian,DecodeInternal(I self.axes 1 _ $)
end
meth DecodeInternal(I Axes K R L)
case Axes of nil then R=I L=nil
[] Axis|Axes then R2 L2 in
Cartesian,DecodeInternal(I Axes K*Axis.card R2 L2)
R = R2 mod K
L = {Axis.decode R2 div K}|L2
end
end
meth MkVal2Ints($)
Table = {Dictionary.new}
in
{List.forAllInd self.axes
proc {$ I D}
{ForAll D.values
proc {$ V}
{Dictionary.put Table V Cartesian,Val2Ints(V I $)}
end}
end}
{Dictionary.toRecord o Table}
end
meth Val2Ints(V I $)
VI = {{Nth self.axes I} encode(V $)}
L1 = {DomainsToListOfInts {List.drop self.axes I} [nil]}
L2 = {Map L1 fun {$ X} VI|X end}
L3 = {DomainsToListOfInts {List.take self.axes I-1} L2}
in
{Map L3 fun {$ T} {self encodeInts(T $)} end}
end
end
%%
fun {DomainsToListOfInts Ds Suffix}
case Ds of nil then Suffix
[] D|Ds then
L={DomainsToListOfInts Ds Suffix}
in
{FoldR {List.number 0 D.card-1 1}
fun {$ I Accu}
{FoldR L
fun {$ X Accu} (I|X)|Accu end Accu}
end nil}
end
end
%%
class Avm from Base
feat domain
meth init(R)
Base,init
self.domain = R
top <- {Record.map R fun {$ D} {D top($)} end}
bot <- {Record.map R fun {$ D} {D bot($)} end}
end
meth encode(S $)
{Adjoin @top
{Record.mapInd S fun {$ F V} {self.domain.F.encode V} end}}
end
meth decode(S $)
{Record.mapInd S fun {$ F I} {self.domain.F.decode I} end}
end
meth glb(X Y $)
{Record.mapInd self.domain fun {$ F D} {D glb(X.F Y.F $)} end}
end
meth lub(X Y $)
{Record.mapInd self.domain fun {$ F D} {D lub(X.F Y.F $)} end}
end
end
%%
class Set from Base
feat domain full empty card StrictSpecs
meth init(D strictSpecs:S<=false)
Base,init
self.domain = D
self.card = {Pow 2 D.card}
self.empty = FS.value.empty
self.full = {FS.value.make 0#D.card-1}
top <- self.full
bot <- self.empty
self.StrictSpecs = S
end
meth glb(S1 S2 $) {FS.intersect S1 S2} end
meth lub(S1 S2 $) {FS.union S1 S2} end
meth encode(Spec $)
if self.StrictSpecs then {self strictEncode(Spec $)}
else {self encodeDisj(Spec $)} end
end
meth strictEncode(Spec $)
case Spec of compl(Spec)
then {FS.diff self.full {self strictEncode(Spec $)}}
else {FS.value.make {Map Spec self.domain.encode}} end
end
meth decode(S $) Set,decodeLowerBound(S $) end
meth decodeLowerBound(S $)
Set,decodeList({FS.reflect.lowerBoundList S} $)
end
meth decodeUpperBound(S $)
Set,decodeList({FS.reflect.upperBoundList S} $)
end
meth decodeList(L $)
{Map L self.domain.decode}
end
meth encodeDisj(Spec $)
if Spec==nil then self.empty
elseif {IsValue Spec} then
{FS.value.make self.domain.val2ints.Spec}
elseif {IsList Spec} then
{FoldL
{Map Spec fun {$ S} {self encodeConj(S $)} end}
fun {$ Accu S} {FS.union Accu S} end
self.empty}
end
end
meth encodeConj(Spec $)
if Spec==nil then self.full
elseif {IsValue Spec} then
{FS.value.make self.domain.val2ints.Spec}
elseif {IsList Spec} then
{FoldL
{Map Spec fun {$ S} {self encodeDisj(S $)} end}
fun {$ Accu S} {FS.intersect Accu S} end
self.full}
end
end
end
%%
fun {IsValue V} {IsAtom V} orelse {IsInt V} end
%%
class AccumulatingSet from Set
meth init(D)
Set,init(D)
top <- self.empty
bot <- self.full
end
meth glb(S1 S2 $) {FS.union S1 S2} end
meth lub(S1 S2 $) {FS.intersect S1 S2} end
end
end
| << Prev | - Up - | Next >> |