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

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 
file Exp_adt.pvs.
       

______________________________________________________
Exp_adt.pvs:
    ...
    ... 
    15	  reduce_nat(v?_fun: [Variable -> nat],
    16	             app?_fun: [[app1_var: Functor, list[nat]] -> nat]):
    17	   [Exp -> nat] =
    18	      LAMBDA (Exp_adtvar: Exp):
    19	        LET red: [Exp -> nat] = reduce_nat(v?_fun, app?_fun) IN
    20	          CASES Exp_adtvar
    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
_______________________________________________________________