% $Id: Store.oz,v 1.14 2012/01/08 03:58:44 leavens Exp $ % Stores (finite functions from locations to values) % AUTHOR: Gary T. Leavens % Representation (where the store's name is used for printing purposes): % ::= store( >) % ::= det() | undet() % where each list Locs in undet(Locs) is non-empty % ::= record(>) % | closure(> ) % | num() % | primitive() % ::= % > ::= an Oz record containing locations for all fields. \insert 'Environment.oz' \insert 'Unparse.oz' declare local un(uniquename:UniqueName ...) = {UniqueNames &s} fun {Duplicate X N} %% ENSURES: Result is a list of N copies of X if N == 0 then nil else X|{Duplicate X N-1} end end in fun {EmptyStore} %% ENSURES: Result is an empty store store({UniqueName} {EmptyFF}) end fun {AllocStore store(_ FF)} %% ENSURES: Result is a pair of a newly allocated location %% and a store that has that location as undetermined. Used = {DomainFF FF} Loc = {FoldR Used Max ~1}+1 in Loc#store({UniqueName} {ExtendFF FF Loc undet([Loc])}) end fun {NameOfStore store(Name _)} %% ENSURES: Result is the name of the argument Name end fun {HasStore store(_ FF) Loc} %% ENSURES: Result is true when Loc is in the domain of the first argument {HasFF FF Loc} end fun {Read store(_ FF) Loc} %% REQUIRES: Loc is a determined value %% in the domain of the first argument %% ENSURES: Result is the value the store holds at the location case {ApplyFF FF Loc} of det(V) then V else raise notDeterminedYet end end end fun {UnifyLocs store(NOld FF) Loc1 Loc2} %% ENSURES: Result is a new store that is the same as the first argument %% with Loc1 and Loc2 unified N = {UniqueName} in case {ApplyFF FF Loc1}#{ApplyFF FF Loc2} of det(V1)#det(V2) then local store(_ FF) = {UnifyVals store(NOld FF) V1 V2} in store(N {ExtendFFList FF Loc1|Loc2|nil det(V1)|det(V2)|nil}) end [] undet(Locs)#det(V2) then {UnifyLocsVal store(N FF) Locs V2} [] det(V1)#undet(Locs) then {UnifyLocsVal store(N FF) Locs V1} [] undet(Loc1s)#undet(Loc2s) then local Vs = undet({Append Loc1s Loc2s}) in store(N {ExtendFFList FF Loc1|Loc2|nil Vs|Vs|nil}) end end end fun {UnifyLocsVal store(N FF) Locs V2} %% ENSURES: Result is a new store that is the same as the first argument %% with each of the locations in Locs unified with V2 case Locs of nil then store({UniqueName} FF) [] Loc|Rest then {UnifyLocsVal {UnifyLocVal store(N FF) Loc V2} Rest V2} end end fun {UnifyLocVal store(NOld FF) Loc V2} %% ENSURES: Result is a new store that is the same as the first argument %% with Loc unified with V2 N = {UniqueName} in case {ApplyFF FF Loc} of det(V1) then local store(_ FF) = {UnifyVals store(NOld FF) V1 V2} in store(N {ExtendFF FF Loc det(V1)}) end [] undet(Locs) then store(N {ExtendFFList FF Locs {Duplicate det(V2) {Length Locs}}}) end end fun {UnifyVals Sto V1 V2} %% ENSURES: Result is a new store that is the same as the first argument %% with V1 unified with V2 case V1#V2 of record(R1)#record(R2) then if {Label R1} == {Label R2} andthen {Arity R1} == {Arity R2} then {FoldL {Arity R1} fun {$ S FN} {UnifyLocs S R1.FN R2.FN} end Sto} else raise recordMismatch(V1 V2) end end else if V1 == V2 then Sto else raise valMismatch(V1 V2) end end end end fun {Undetermined Sto Loc} %% ENSURES: Result is true when Loc is not determined in Sto {Not {Determined Sto Loc}} end fun {Determined store(_ FF) Loc} %% ENSURES: Result is true when Loc is determined in the first argument case {ApplyFF FF Loc} of det(_) then true [] undet(_) then false end end fun {EqualValue V1 V2} %% ENSURES: Result is true when V1 is equivalent to V2 case V1#V2 of record(R1)#record(R2) then R1 == R2 [] closure(F1 B1 E1)#closure(F2 B2 E2) then F1 == F2 andthen B1 == B2 andthen {EqualEnv E1 E2} [] primitive(OzPrim1)#primitive(OzPrim2) then OzPrim1 == OzPrim2 [] num(N1)#num(N2) then N1 == N2 [] loc(L1)#loc(L2) then L1 == L2 else false end end fun {EqualPUValue PUV1 PUV2} %% ENSURES: Result is true when PUV1 is equivalent to PUV2 case PUV1#PUV2 of det(V1)#det(V2) then {EqualValue V1 V2} [] undet(Locs1)#undet(Locs2) then Locs1 == Locs2 else false end end local EqualFF = {EqualFFMaker EqualPUValue} in fun {EqualStore store(_ FF1) store(_ FF2)} %% ENSURES: Result is true when the two stores are equalivalent {EqualFF FF1 FF2} end end fun {StringForValue V} %% ENSURES: Result is a virtual string that represents V VSBlankSeparate = {VSSeparateMaker ' '} in case V of record(R) then {Value.toVirtualString R 5 20} [] num(N) then {Value.toVirtualString N 5 20} [] bool(B) then {Value.toVirtualString B 5 20} [] loc(L) then {Value.toVirtualString {NameLoc L} 5 20} [] closure(Formals Code Env) then 'closure(proc {$ ' # {VSBlankSeparate Formals} # '} ' # {UnparseStmt Code} # ' end ' # {StringForEnv Env} #')' else {Value.toVirtualString V 5 20} end end fun {StringForStore store(_ FF)} %% ENSURES: Result is a virtual string that represents the argument VSEqSeparate = {VSSeparateMaker '='} fun {Mappings Dom Done} %% ENSURES: Result is a virtual string that represents %% the mappings for the locations in Dom case Dom of nil then nil [] L|Ls then case {ApplyFF FF L} of undet(Loc1|Locs) then if {Member Loc1 Done} % already processed then {Mappings Ls Done} else {VSEqSeparate {Map (Loc1|Locs) NameLoc}} | {Mappings Ls {Append (Loc1|Locs) Done}} end [] det(V) then {NameLoc L}#' = '#{StringForValue V} | {Mappings Ls Done} end end end in '{' # {VSCommaSeparate {Reverse {Mappings {DomainFF FF} nil}}} # '}' end end