Re: [PVS-Help] Typechecking problem

[Sam Owre <owre@csl.sri.com>]

Hi Aditya,

The problem here is that in your importing, you are asking for a
set of lists of reals, so "(: 1 :)" is converted to a set of
lists by using the singleton conversion, but there is no
conversion that will work for the b assignment.

What you want is to import T1[real], and then the conversions
work as you expect.

Regards,
Sam

Aditya Kanade <aditya@cse.iitb.ac.in> wrote:

> hi,
> 
> I'm getting a typechecking error where I atmost expect a
> TCC. Following is the scenario:
> 
> T1[t:type+]:theory
> begin
>   t1:type = [# a: set[t], b:set[[(a),(a)]] #]
> end T1
> 
> T2:theory
> begin
>   importing T1[list[real]]
> 
>   e:t1 = (# a := (: 1 :), b := (: (1,1) :) #)
> end T2
> 
> The typechecking error is:
> 
> Incompatible types for (: (1, 1) :)
>      Found: (list_adt[[real, real]].cons?)
>   Expected: sets
>                 [[(singleton[(cons?[real])]((: 1 :))),
>                   (singleton[(cons?[real])]((: 1 :)))]].set
> 
> Now, AFAIK, PVS should have applied the list2set conversion to 
> the list (: (1,1) :). I think it does that for a := (: 1 :). If I
> explicitly write list2set((: (1,1) :)), then it gives the same error,
> this time for the list2set conversion!
> 
> At least conceptually, what I'm trying to do should work. Can anyone
> please explain the problem? And any solution to this?
> 
> Regards,
> Aditya.