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

[PVS-Help] Abtract datatypes: diffenrence between curried and uncurried map



Hi,

I have the following abstract data type:

==

Term[ V 	: TYPE,       % for variables
     F 	: TYPE,       % for operations
     ar 	: [F -> nat]  % for arity of operations
] : DATATYPE BEGIN
	tvar(var_id:V)	:tvar?
	tapp(op:F, args:[below(ar(op)) -> Term]) : tapp?
END Term

==

And I'm trying to define the following composition property about map (that
I've copied form the prelude where it was given for lists and sequences)

==

T_map_props [F : TYPE, ar : [F -> nat], T1, T2, T3: TYPE]: THEORY
BEGIN
 IMPORTING Term
 f1: VAR [T1 -> T2]
 f2: VAR [T2 -> T3]
 t:  VAR Term[T1,F,ar]

 map_T_composition: LEMMA map(f2)(map(f1)(t)) = map(f2 o f1)(t)

END T_map_props

==
This definition will not compile; it produces the error:
==
Could not determine the full theory instance for =
 Theory instance: equalities
                      [Term_adt
                           [Term_adt_map.V1, Term_adt_map.F,
                            Term_adt_map.ar].Term]

==

If I use the uncurried map :

==
 map_T_composition: LEMMA map(f2,map(f1,t)) = map(f2 o f1,t)
==
Pvs is satisfied.

What's the difference? What do i have to do to get the first version
accepted? I've tried almost anything I could think of (in terms of imports,
or qualified names), but nothing seems to work . Actually I would prefer the
following version

==
 map_T_composition: LEMMA (map(f2) o map(f1))(t) = map(f2 o f1,t)
==

which doesn't work either,

Thanks,

Sjaak Smetsers