[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

question on operator conversion



Hi,

In the following, I have a couple of conversions declared to uniformly
extend operations over booleans to operations over Objects which are
maps from an abstract type State to booleans, along with some
bookkeeping info (flag).

------------------------------------------------------------------------
tst: theory
begin

  State: TYPE

  boolObj: DATATYPE
   BEGIN
    cons(value: [State -> bool], flag: [State -> bool]): rec
  END boolObj

  op1(f: [bool -> bool]): [boolObj -> boolObj] =
    LAMBDA (c1: boolObj): cons(f(value(c1)), flag(c1))

  CONVERSION op1

  op2(f: [bool, bool -> bool]): [boolObj, boolObj -> boolObj] =
    LAMBDA (c1, c2: boolObj):
  cons(f(value(c1), value(c2)), flag(c1) AND flag(c2))

  CONVERSION op2

  a, b: boolObj

  c: boolObj = NOT a           % implicit conversion to op1(NOT)
  d: boolObj = op2(AND)(a, b)   % *need* explicit conversion to op2(AND)

end tst
------------------------------------------------------------------------

While op1 conversion applies to NOT automatically, op2 does not apply
to AND similarly. If the last declaration was instead given as:

  d: boolObj = a AND b

the following error is reported:
-------------------------------------------
Incompatible types for a
     Found: boolObj
       Expected: booleans.boolean
-------------------------------------------

I don't understand why. Am I missing something here?

More importantly, is this a good way of extending operations on
type T to operations on Objects with value of type [State -> T]
(T = bool in the above), assuming I parametrize Object, op1 and op2
with T?

Any help is very much appreciated.

Thanks,
- Sanjai