let expression interprets tail of a seq1 as a seq1

[ivor-spence]

Description

In a let expression of the form let n = tl l in ...
in which l is of type seq1, the type of n is taken to be seq1 as well. This causes problems if l is of length 1.

Steps to Reproduce

In the quick interpreter type

let n = tl [1] in n

Expected behavior: [What you expect to happen]

I would expect the result to be []

Actual behavior: [What actually happens]

An error is reported because the type of n is assumed to be seq1 of nat meaning that it can't be empty. Its type should be seq of nat.

Reproduces how often: [What percentage of the time does it reproduce?]

Every time.

Versions

Which version of Overture are you using? Also, please include the OS and what version of the OS you're running.

Version 2.5.4 of Overture running on Windows 10

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[peterwvj]

Yes, this definitely looks like a bug. I can produce it using Overture 2.6.0 as well.

[nickbattle]

Thanks for reporting this. It should be a simple fix. I'll look at it later today.

[nickbattle]

This was an error in the type checking of the tail expression. It didn't correctly deal with seq1, assuming that the result of the tail was the same type as the argument. The change affects the proof obligation tests as well, as you might expect. Just testing now, then I'll check it in.

[ivor-spence]

Nick, Thanks for your quick response and I’m glad that you have been able to track down the issue. Ivor From: Nick Battle [mailto:notifications@github.com] Sent: 02 March 2018 12:23 To: overturetool/overture <overture@noreply.github.com> Cc: Ivor Spence <I.Spence@qub.ac.uk>; Author <author@noreply.github.com> Subject: Re: [overturetool/overture] let expression interprets tail of a seq1 as a seq1 (#669) This was an error in the type checking of the tail expression. It didn't correctly deal with seq1, assuming that the result of the tail was the same type as the argument. The change affects the proof obligation tests as well, as you might expect. Just testing now, then I'll check it in. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub<#669 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AjQdYdggCuA9XybY2oi6s17RvypyYKDHks5taTm2gaJpZM4SY7K4>.