[PVS-Help] Help with Theory as parameters and Theory instantiation

[Renaud CLAVEL <renaud.clavel@xxxxxxx>]

Hi,
I want to use a theory as parameter. So I define a general theory, and 
some instances of it. But I have some problems while doing it :

First of all, I get the following error (Map lhs inject does not resolve 
to an uninterpreted type, constant, or theory within theory: 
TEMPLATE_ELTS1), with this code :


TEMPLATE_ELTS1 : THEORY BEGIN
   elts : TYPE+
   inject : TYPE FROM [elts -> elts]
END TEMPLATE_ELTS1

INST_ELTS1 : THEORY BEGIN
   th : THEORY = TEMPLATE_ELTS1{{elts := int, inject := [int -> int]}}
END INST_ELTS1


elts is an uninterpreted type, [elts -> elts] is an interpreted type, 
and inject is an interpreted type. So the error message is correct. I 
don't understand why I need an uninterpreted type, and not just an 
undefine type.
The only solution I found, is to use the predicate to identify the 
inject type :


TEMPLATE_ELTS2 : THEORY BEGIN
   elts : TYPE+
   inject? : [[elts -> elts] -> bool]
   inject : TYPE = (inject?)
END TEMPLATE_ELTS2

INST_ELTS2 : THEORY BEGIN
   th : THEORY = TEMPLATE_ELTS2{{elts := int, inject? := LAMBDA(x:[int 
-> int]):TRUE}}
END INST_ELTS2

In this case, I have no error, but I cannot see any real difference.
Futhermore, I would like to use a theory parameter in my instantiation, 
like this :

INST_ELTS3[t : TYPE+] : THEORY BEGIN
   th : THEORY = TEMPLATE_ELTS2{{elts := t, inject? := LAMBDA(x:[t -> 
t]):TRUE}}
END INST_ELTS3

In this case, I get the following error : Illegal reference to t. May 
not use theory declarations with actuals or mappings that reference 
entities declared in this theory.
I don't understand this error :  why is it illegal to use a entities 
declared in the theory ?

Thanks for your time

-- 
==================================
Renaud CLAVEL - PhD Candidate
==================================
TIMA Laboratory, VDS Team
http://tima.imag.fr/vds

Office T101, +33 (0)4 76 57 48 73
Renaud.Clavel@imag.fr
==================================