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

*To*: pvs-help@csl.sri.com*Subject*: Dependent types lost in reduce combinators*From*: Venkatesh Choppella <choppellav@ornl.gov>*Date*: Thu, 13 Feb 2003 09:25:35 -0500 (EST)*Cc*: choppellav@ornl.gov*Sender*: pvs-help-owner@csl.sri.com

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 _______________________________________________________________

- Prev by Date:
**"<" on a subset of nat is well_founded** - Next by Date:
**Re: "<" on a subset of nat is well_founded** - Prev by thread:
**Re: Proof of override expressions** - Next by thread:
**"<" on a subset of nat is well_founded** - Index(es):