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/CAPPSPLpjoPrSwwQh%2BmO7PWJ3mMpquz8yk70OJ818BOdTQBsPwg%40mail.gmail.com.
