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

*To*: <pvs-help@csl.sri.com>*Subject*: question on operator conversion*From*: Sanjai Rayadurgam <rsanjai@cs.umn.edu>*Date*: Sun, 28 Oct 2001 19:30:17 -0600 (CST)*Sender*: pvs-help-owner@csl.sri.com

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

- Prev by Date:
**Re: Looking for old finite_set library** - Next by Date:
**Petri-nets !** - Prev by thread:
**Petri-nets !** - Next by thread:
**Looking for old finite_set library** - Index(es):