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

question on operator conversion


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

  State: TYPE

  boolObj: DATATYPE
    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))


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


  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.

- Sanjai