How to do viewat-restoration?

Google Group
1

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) – 608(line=17, offs=28): error(3): viewat-restoration cannot be performed: mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

2

Ah, right. Thanks!> On Apr 15, 2015, at 10:00, gmhwxi gmh...@gmail.com wrote:

I notice this fails to type check if I replace {0,10} with {…}, why can’t that be inferred?

The typechecker cannot figure out what ‘total’ should be by simply relying on unification.
Yes, it knows ‘total-fill==10’ but this constraint cannot be handled by unification.

On Wednesday, April 15, 2015 at 8:32:25 AM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 10:30 PM, gmhwxi gmh...@gmail.com wrote:

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
var buf = @[byte]10
prval pfbuf = view@(buf)
prval pfemp = array_v_nil{byte}{buf}()
prval partial = partial_buf{byte}{0,10}{…}(pfemp, pfbuf)
prval partial_buf{…}{fill,total}{buf2}(empty, l) = partial
prval _ = array_v_unnil(empty)
prval EQADDR() = eqaddr_make{buf,buf2+fill}()
prval _ = view@(buf) := l
in 0 end

I really don’t know how to explain this. Basically, when you put a proof of some view
into view@(buf), the typechecker expects the view to be of the form T@buf (it is not
okay even if you have the form T@(buf+0)).

Ah ha, I think that makes sense. So the eqaddr_make line is forcing the constraint solver to consider whether buf and buf2 + fill are equal, right?

I notice this fails to type check if I replace {0,10} with {…}, why can’t that be inferred?

On Tuesday, April 14, 2015 at 9:40:21 PM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 9:33 PM, Hongwei Xi gmh...@gmail.com wrote:

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original declaration
has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy sh...@shealevy.com wrote:
Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) – 608(line=17, offs=28): error(3): viewat-restoration cannot be performed: mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com.

–
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 ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com.

–
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 ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com.

–
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/bb963b0b-6812-46e1-a1b0-66622c0dc65c%40googlegroups.com.

3

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original declaration
has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?> On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy <sh...@shealevy.com mailto:sh...@shealevy.com> wrote:

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) – 608(line=17, offs=28): error(3): viewat-restoration cannot be performed: mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang-user...@googlegroups.com mailto:ats-lang-users...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com.

–
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 ats-lang-user...@googlegroups.com mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com?utm_medium=email&utm_source=footer.

4

I notice this fails to type check if I replace {0,10} with {…}, why
can’t that be inferred?

The typechecker cannot figure out what ‘total’ should be by simply relying
on unification.
Yes, it knows ‘total-fill==10’ but this constraint cannot be handled by
unification.On Wednesday, April 15, 2015 at 8:32:25 AM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 10:30 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but
not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so
empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
var buf = @[byte]10
prval pfbuf = view@(buf)
prval pfemp = array_v_nil{byte}{buf}()
prval partial = partial_buf{byte}{0,10}{…}(pfemp, pfbuf)
prval partial_buf{…}{fill,total}{buf2}(empty, l) = partial
prval _ = array_v_unnil(empty)
prval EQADDR() = eqaddr_make{buf,buf2+fill}()
prval _ = view@(buf) := l
in 0 end

I really don’t know how to explain this. Basically, when you put a proof
of some view
into view@(buf), the typechecker expects the view to be of the form T@buf
(it is not
okay even if you have the form T@(buf+0)).

Ah ha, I think that makes sense. So the eqaddr_make line is forcing the
constraint solver to consider whether buf and buf2 + fill are equal, right?

I notice this fails to type check if I replace {0,10} with {…}, why can’t
that be inferred?

On Tuesday, April 14, 2015 at 9:40:21 PM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 9:33 PM, Hongwei Xi gmh...@gmail.com wrote:

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original
declaration
has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but
not the buf: addr?

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so
empty has to be empty, right?

On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy sh...@shealevy.com wrote:

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) –
608(line=17, offs=28): error(3): viewat-restoration cannot be performed:
mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com
.

–
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 ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.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 ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original
declaration
has duplicated quantifiers.

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy sh...@shealevy.com wrote:

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) –
608(line=17, offs=28): error(3): viewat-restoration cannot be performed:
mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com
.

6

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
var buf = @[byte]10
prval pfbuf = view@(buf)
prval pfemp = array_v_nil{byte}{buf}()
prval partial = partial_buf{byte}{0,10}{…}(pfemp, pfbuf)
prval partial_buf{…}{fill,total}{buf2}(empty, l) = partial
prval _ = array_v_unnil(empty)
prval EQADDR() = eqaddr_make{buf,buf2+fill}()
prval _ = view@(buf) := l
in 0 end

I really don’t know how to explain this. Basically, when you put a proof of some view
into view@(buf), the typechecker expects the view to be of the form T@buf (it is not
okay even if you have the form T@(buf+0)).

Ah ha, I think that makes sense. So the eqaddr_make line is forcing the constraint solver to consider whether buf and buf2 + fill are equal, right?

I notice this fails to type check if I replace {0,10} with {…}, why can’t that be inferred?> On Tuesday, April 14, 2015 at 9:40:21 PM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 9:33 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original declaration
has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) – 608(line=17, offs=28): error(3): viewat-restoration cannot be performed: mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com <javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com.

–
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 ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com <javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.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 ats-lang-user...@googlegroups.com mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com?utm_medium=email&utm_source=footer.

7

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but
not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so
empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
var buf = @[byte]10
prval pfbuf = view@(buf)
prval pfemp = array_v_nil{byte}{buf}()
prval partial = partial_buf{byte}{0,10}{…}(pfemp, pfbuf)
prval partial_buf{…}{fill,total}{buf2}(empty, l) = partial
prval _ = array_v_unnil(empty)
prval EQADDR() = eqaddr_make{buf,buf2+fill}()
prval _ = view@(buf) := l
in 0 end

I really don’t know how to explain this. Basically, when you put a proof of
some view
into view@(buf), the typechecker expects the view to be of the form T@buf
(it is not
okay even if you have the form T@(buf+0)).On Tuesday, April 14, 2015 at 9:40:21 PM UTC-4, Shea Levy wrote:

On Apr 14, 2015, at 9:33 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

There are two issues here.

  1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
| { fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

If a parameter is given a name in a dataview declaration, then a universal
quantifier is implicitly introduced for that parameter. So your original
declaration
has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but
not the buf: addr?

  1. Logic.

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

prval partial_buf(empty, l) = partial

The system does not know that ‘empty’ is a proof of an empty array-view;
it only knows that ‘empty’ is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty
has to be empty, right?

On Tue, Apr 14, 2015 at 9:14 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte]10
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) –
608(line=17, offs=28): error(3): viewat-restoration cannot be performed:
mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

–
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 ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com
.

–
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 ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com?utm_medium=email&utm_source=footer
.