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

*To*: Kurt Lichtner <kurt@csg.uwaterloo.ca>*Subject*: Re: question on dependent typing*From*: Sam Owre <owre@csl.sri.com>*Date*: Tue, 23 Nov 1999 11:44:34 -0800*cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Tue, 23 Nov 1999 13:44:13 EST." <383AE07D.8AEB6FAF@csg.uwaterloo.ca>

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

- Prev by Date:
**question on dependent typing** - Next by Date:
**Re: question on dependent typing** - Prev by thread:
**question on dependent typing** - Next by thread:
**Re: question on dependent typing** - Index(es):