[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: question on dependent typing
Kurt,
TCCs of the form "FORALL ... IFF ... " are usually, as in this
case, due to a domain mismatch. What is going on is that t`c
is of type [(b) -> bool], whereas add(d,t)`c needs to be of
type [(add(d, t`b)) -> bool]. The type system insists that
these domains be the same, and you get the TCC.
You can fix this by including the update to c at the same
time, e.g., either
add(d,t) : a_type = t with [b := add(d, t`b),
c := {x: (add(d, t`b))| t`b(x)}]
or, since all the fields are being updated,
add(d,t) : a_type = (# b := add(d, t`b),
c := {x: (add(d, t`b))| t`b(x)} #)
If the typechecker knew that (t`b) was a subtype of (add(d, t`b)),
then you would not get the TCC, as the typechecker would
insert the extend_bool conversion automatically.
Unfortunately, the judgement facility does not currently
support this form of subtype judgement, as there would be a
free variable on the right-hand side. We plan on exploring
such extensions in the future, though they may slow down
typechecking too much to be incorporated into the system.
Regards,
Sam Owre
> Hi,
> The following spec gives what appears to be an unprovable TCC:
>
> t1 : THEORY
>
> BEGIN
>
> a_type : type = [#
> b : setof[int],
> c : setof[(b)]
> #]
>
> d : var int
> t : var a_type
>
>
> add(d,t) : a_type = t with [b := add(d, t`b)]
>
> END t1
>
> ... and yields:
>
> % Subtype TCC generated (at line 16, column 20) for c(t)
> % unfinished
> add_TCC1: OBLIGATION
> FORALL (d, t): FORALL (x: int): t`b(x) IFF add[int](d, t`b)(x);
>
> I'm unsure why I'm getting this. Can anyone shed some insight?
>
> Thanks very much in advance,
> Kurt