Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. So what we want is:
- let getx = fun (r, h) ->
+ let getx : entity dpm = fun (r, h) ->
let obj = List.nth h (r 'x')
in (obj, r, h);;