sail/test/typecheck/pass, branch sail2 Formal specification language for ISAs Enum value feature request for Alexandre 2021-01-05T11:11:04+00:00 Alasdair 2020-12-01T03:26:33+00:00 8b2a3fa0eae0f49b78c0c5f845d3824d21f98df3 






Don't allow type synonyms with the same name as existing types
2021-01-05T11:11:04+00:00

Alasdair

2020-11-23T14:18:58+00:00

c4723c747fec4557776858641b03e1eb4a0a5878












Remove bogus pattern completeness warning on singleton enums and unions
2020-11-25T22:40:29+00:00

Brian Campbell

2020-11-25T22:40:29+00:00

3c43a474e03ef94839ebef530f5a2bbd173add5b












Fix Lem output for single element enum
2020-11-25T21:46:03+00:00

Brian Campbell

2020-11-25T21:45:49+00:00

3d0064a157a711f21d23f56dc2c423b2e3b1d74a












Make `if cond { ... return() };` assert cond in the type environment
2020-06-17T14:28:42+00:00

Brian Campbell

2020-06-17T14:28:42+00:00

a7d351c71d43585d789bc92df3ba27f4e533d1b7

Avoids generating an assert expression with an escape effect.
Mirrors existing case for `if cond { throw(...); };`.
No longer requires `-non_lexical_flow`.





Avoids generating an assert expression with an escape effect.
Mirrors existing case for `if cond { throw(...); };`.
No longer requires `-non_lexical_flow`.







Add test for if-return pattern
2020-06-17T13:57:29+00:00

Brian Campbell

2020-06-17T13:57:29+00:00

60284d322dd9c240d65954a67488c2a880ef5907

(currently supported in nl_flow)





(currently supported in nl_flow)







Merge branch 'sail2' into mono-tweaks
2020-05-21T14:30:43+00:00

Alasdair

2020-05-21T14:30:43+00:00

8320ddc4b19d622f8ab5ab8625dde45fccbf383b












Update type error messages for jenkins
2020-05-15T11:10:22+00:00

Alasdair

2020-05-15T11:10:22+00:00

74da1d93d78e606a7c855f2a427dbd171fd861c5

Location info fixes changed the location reported for an expected type error very slightly





Location info fixes changed the location reported for an expected type error very slightly







Update test error messages, hopefully will make Jenkins happy again
2020-04-28T19:45:21+00:00

Alasdair

2020-04-28T19:45:21+00:00

88fe9754f897d3d96533748c6fc73a2d8da76fec












Tweak types of loop combinators for prover combinators
2020-04-21T01:20:11+00:00

Thomas Bauereiss

2020-04-04T16:20:06+00:00

e1a2b0d2a88e4797d714ad0cb941c3cbf019720b

Split the variable (tuple) type into an input and output type.  They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it).  The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.





Split the variable (tuple) type into an input and output type.  They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it).  The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.