<feed xmlns='http://www.w3.org/2005/Atom'>
<title>sail/src/trace_viewer, branch sail2</title>
<subtitle>Formal specification language for ISAs</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/'/>
<entry>
<title>Remove trace viewer application from repository</title>
<updated>2018-02-01T15:27:51+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-02-01T15:27:18+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=3630fd36d5963ec6e4299f52930db7c0d2cf2f01'/>
<id>3630fd36d5963ec6e4299f52930db7c0d2cf2f01</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Added monomorphism restriction to undefined values.</title>
<updated>2017-11-02T18:32:34+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2017-11-02T18:19:29+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=ce3cd80585a943479614e2112b51a631c3e1376b'/>
<id>ce3cd80585a943479614e2112b51a631c3e1376b</id>
<content type='text'>
What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.

As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.

val test : forall ('a:Type). list('a) -&gt; unit effect {wreg, undef}

function test xs = {
  xs_mut = xs;
  xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
  ()
}

There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:

union option ('a:Type) = {
  Some : 'a,
  None
}

These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.

Also: Fixed some test cases that were broken due to escape effect being added to assert.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.

As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.

val test : forall ('a:Type). list('a) -&gt; unit effect {wreg, undef}

function test xs = {
  xs_mut = xs;
  xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
  ()
}

There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:

union option ('a:Type) = {
  Some : 'a,
  None
}

These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.

Also: Fixed some test cases that were broken due to escape effect being added to assert.
</pre>
</div>
</content>
</entry>
<entry>
<title>Fixed wrong image for List-remove.svg</title>
<updated>2017-10-31T17:36:00+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2017-10-31T17:36:00+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=d610decb92eea6c0e55456f62d5c73cd03d1997b'/>
<id>d610decb92eea6c0e55456f62d5c73cd03d1997b</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Added trace viewer application for traces produced by sail -ocaml_trace</title>
<updated>2017-10-31T17:32:33+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2017-10-31T17:32:33+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=e8de662b4d8d5e4bcc7368277d8607f9a8bc3405'/>
<id>e8de662b4d8d5e4bcc7368277d8607f9a8bc3405</id>
<content type='text'>
See README file for how to set up and use
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
See README file for how to set up and use
</pre>
</div>
</content>
</entry>
</feed>
