20.5 DG_Selection.oz

We now turn to the implementation of the selection constraint

<DG_Selection.oz>=

functor 
import FS W(weightC:WeightC) at 'DG_Weight.ozf' 
export Select
define 
   %% implements the selection constraint on sets
   %% L[I] = S
   proc {Select L I S1}
      L2 = {List.mapInd L
            fun {$ J S2}
               B=(I=:J)
            in 
               B#S2#{WeightC B S2}
            end}
   in 
      %% first instantiate S1
      {FS.unionN {Map L2 fun {$ _#_#S3} S3 end} S1}
      %% then reified.equal won't block
      {ForAll L2
       proc {$ B#S2#_}
          B=<:{FS.reified.equal S1 S2}
       end}
   end 
end