'kept' : pf is held by the type-checker and no longer available when '!p' is type-checked.
On Wed, Dec 12, 2018 at 3:13 PM Scott Murphy <[email protected]> wrote: > What is meant by kept? > > On Wednesday, December 12, 2018 at 9:47:33 AM UTC-6, gmhwxi wrote: >> >> Not sure if I understand your question. >> >> When constructing (pf | !p), 'pf' is kept and then !p could no longer >> find the view it needs >> in order to fetch the data. So the data needs to be fetched first: let >> val x = !p in (pf | x) >> >> On Wed, Dec 12, 2018 at 10:19 AM Scott Murphy <[email protected]> >> wrote: >> >>> Okay so binding has nothing to do with proof consumption then? >>> Maybe I understand now lol. >>> >>> On Tuesday, December 11, 2018 at 8:13:09 PM UTC-6, gmhwxi wrote: >>>> >>>> >>(pf | !p) >>>> >>>> This does not work because type-checking is performed from >>>> left to right. So you need >>>> >>>> let val x = !p in (pf | x) end >>>> >>>> >>>> On Tue, Dec 11, 2018 at 6:57 PM Scott Murphy <[email protected]> >>>> wrote: >>>> >>>>> Thank you so much. >>>>> So the binding with val A is what forces pf to be considered >>>>> consumed. >>>>> >>>>> I have tried: >>>>> fun{a:t@ype} >>>>> ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) = (pf|!p) >>>>> and seen the consumption error so many times but wasn't sure exactly >>>>> what consumption meant! >>>>> >>>>> >>>>> >>>>> On Tuesday, December 11, 2018 at 4:41:24 PM UTC-6, Richard wrote: >>>>>> >>>>>> Not sure if this is completely correct however, it typechecks >>>>>> >>>>>> extern fun {a:t@ype} >>>>>> ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) >>>>>> >>>>>> implement {a} ptr_get0 {l} (pf | p) = (pf | A) where { val A = !p } >>>>>> >>>>>> -- >>>>> You received this message because you are subscribed to the Google >>>>> Groups "ats-lang-users" group. >>>>> To unsubscribe from this group and stop receiving emails from it, send >>>>> an email to [email protected]. >>>>> To post to this group, send email to [email protected]. >>>>> Visit this group at https://groups.google.com/group/ats-lang-users. >>>>> To view this discussion on the web visit >>>>> https://groups.google.com/d/msgid/ats-lang-users/9689d6a2-2dfb-4110-b8e1-c8e616b35696%40googlegroups.com >>>>> <https://groups.google.com/d/msgid/ats-lang-users/9689d6a2-2dfb-4110-b8e1-c8e616b35696%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>> -- >>> You received this message because you are subscribed to the Google >>> Groups "ats-lang-users" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To post to this group, send email to [email protected]. >>> Visit this group at https://groups.google.com/group/ats-lang-users. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/ats-lang-users/3f188543-4655-42ca-8696-bb371641172f%40googlegroups.com >>> <https://groups.google.com/d/msgid/ats-lang-users/3f188543-4655-42ca-8696-bb371641172f%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "ats-lang-users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/ats-lang-users. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/b6c63a79-458e-4e3a-b981-e2adbae17819%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/b6c63a79-458e-4e3a-b981-e2adbae17819%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpjJusLCqcwmMPCB1p9E_BvPH1%3DaStsd1nL9A68XEMBLQ%40mail.gmail.com.
