% $Id: FiniteFun.oz,v 1.4 2009/01/10 18:12:21 leavens Exp $ % Finite Functions % AUTHOR: Gary T. Leavens % Representation: % ::= ff() | extendedff( ) \insert 'Assoc.oz' declare fun {EmptyFF} %% ENSURES: Result is an empty finite function ff(nil) end fun {ApplyFF FF V} %% REQUIRES: {HasFF FF V} %% ENSURES: Result is what FF associates with V case FF of ff(AL) then case {Assoc AL V} of X|_ then X else raise applyNoValueForIn(V AL) end end [] extendedff(AL FF2) then case {Assoc AL V} of X|_ then X else {ApplyFF FF2 V} end end end fun {HasFF FF V} %% ENSURES: Result is true if V is in the domain of FF case FF of ff(AL) then {Assoc AL V} \= nil [] extendedff(AL FF2) then {Assoc AL V} \= nil orelse {HasFF FF2 V} end end local fun {DomainAL AL} %% ENSURES: Result is the domain of AL {Map AL fun {$ X#_} X end} end fun {Union L1 L2} %% ENSURES: Result is the union of L1 and L2 (as sets) case L1 of nil then L2 [] H|T then if {Member H L2} orelse {Member H T} then {Union T L2} else H|{Union T L2} end end end in fun {DomainFF FF} %% ENSURES: Result is a list representing the domain of FF case FF of ff(AL) then {DomainAL AL} [] extendedff(AL FF2) then {Union {DomainAL AL} {DomainFF FF2}} end end end fun {ExtendFF FF V X} %% ENSURES: Result is FF with the addition of the mapping from V to X extendedff([V#X] FF) end fun {ExtendFFList FF Vs Xs} %% REQUIRES: {Length Vs} == {Length Xs} %% ENSURES: Result is FF with the addition of the mappings %% from each V in Vs to the corresponding X in Xs extendedff( for V in Vs X in Xs collect: C do {C V#X} end FF) end fun {EqualFFMaker EqualValues} fun {$ FF1 FF2} %% ENSURES: Result is true when FF1 and FF2 have %% the same domains and equal values at each domain element Dom1 = {DomainFF FF1} Dom2 = {DomainFF FF2} in {Length Dom1} == {Length Dom2} andthen {All Dom1 fun {$ X} {Member X Dom2} andthen {EqualValues {ApplyFF FF1 X} {ApplyFF FF2 X}} end} end end