Dependent types lost in reduce combinators

```
When using dependent types within ADT definitions, the dependent
type information is lost in the generated reduce functions.

The following is a simple definition of "Exp"s over a Signature and
Variable type.  The dependent type is on line 11

________________________________________
Signature.pvs:
1	Signature: THEORY
2	  BEGIN
3		Functor: TYPE+
4	        arity:  [Functor -> nat]
5	        Variable: TYPE+
6	  END Signature

Exp.pvs:
7	Exp: DATATYPE
8	BEGIN
9	   IMPORTING Signature
10	       v(x: Variable): v?
11	       app(f: Functor, rands: {rands: list[Exp] | length(rands)=arity(f)}): app?
12	END Exp

PVS generates the  following definition of reduce_nat in the

______________________________________________________
...
...
15	  reduce_nat(v?_fun: [Variable -> nat],
16	             app?_fun: [[app1_var: Functor, list[nat]] -> nat]):
17	   [Exp -> nat] =
19	        LET red: [Exp -> nat] = reduce_nat(v?_fun, app?_fun) IN
21	            OF v(v1_var): v?_fun(v1_var),
22	               app(app1_var, app2_var):
23	                 app?_fun(app1_var, map[Exp, nat](red)(app2_var))
24	            ENDCASES;
________________________________________________

Instead of the type given on line 16, one would expect app?_fun
(line 16) to have the following dependent type:

app?_fun: [[app1_var: Functor,
app2_var: {ls: list[Exp] | length(ls)=arity(app1_var)}]
-> nat]

Why is the dependent type information lost in the reduce_nat
function?   The other reduce
functions generated in the _adt.pvs file also have the same
problem; the induction axioms don't.

I'm running

"PVS Version 3.0 - Allegro CL Enterprise Edition 6.2 [Linux
(x86)] (Dec 19, 2002 3:09)"

Best Wishes.

- venkatesh choppella

_______________________________________________________________
Venkatesh Choppella
Computer Science and Mathematics Division    Bethel Valley Road
Oak Ridge National Laboratory                     P.O. Box 2008
Ph:  865 576 4292                                     Bldg 6012
Fax: 865 574 0680                       Oak Ridge TN 37831-6367
email: choppellav@ornl.gov                                  USA
_______________________________________________________________

```