<feed xmlns='http://www.w3.org/2005/Atom'>
<title>sail/test/ocaml/trycatch, branch sail2</title>
<subtitle>Formal specification language for ISAs</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/'/>
<entry>
<title>Interactive: Refactor sail.ml</title>
<updated>2019-03-27T16:32:08+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2019-03-27T16:21:05+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=790de19f73f1c164aba2259a6fe3f1a50eeff70c'/>
<id>790de19f73f1c164aba2259a6fe3f1a50eeff70c</id>
<content type='text'>
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile &lt;target&gt; command in the
interactive toplevel

Also implement a :rewrites &lt;target&gt; command which performs all the
rewrites for a specific target, so rather than doing e.g.

&gt; sail -c -O -o out $FILES

one could instead interactively do

&gt; sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile &lt;target&gt; command in the
interactive toplevel

Also implement a :rewrites &lt;target&gt; command which performs all the
rewrites for a specific target, so rather than doing e.g.

&gt; sail -c -O -o out $FILES

one could instead interactively do

&gt; sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
</pre>
</div>
</content>
</entry>
<entry>
<title>Make union types consistent in the AST</title>
<updated>2018-03-07T15:57:08+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-03-07T15:42:24+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb'/>
<id>1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb</id>
<content type='text'>
Previously union types could have no-argument constructors, for
example the option type was previously:

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

Now every union constructor must have a type, so option becomes:

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

The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.

This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:

function is_none opt = match opt {
  Some(_) =&gt; false,
  None    =&gt; true
}

it is now matched as

function is_none opt = match opt {
  Some(_) =&gt; false,
  None()  =&gt; true
}

note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.

There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.

The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using

$include &lt;option.sail&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Previously union types could have no-argument constructors, for
example the option type was previously:

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

Now every union constructor must have a type, so option becomes:

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

The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.

This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:

function is_none opt = match opt {
  Some(_) =&gt; false,
  None    =&gt; true
}

it is now matched as

function is_none opt = match opt {
  Some(_) =&gt; false,
  None()  =&gt; true
}

note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.

There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.

The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using

$include &lt;option.sail&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>Update and fix test suite</title>
<updated>2018-01-22T13:41:35+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-01-22T13:41:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=1f8ac16d110e2b964a482c083e3782f406e94b69'/>
<id>1f8ac16d110e2b964a482c083e3782f406e94b69</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>More OCaml test cases</title>
<updated>2017-12-07T19:53:14+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2017-12-07T19:53:14+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=47f1892406b5c10d06eb99af40d4523b93b2f254'/>
<id>47f1892406b5c10d06eb99af40d4523b93b2f254</id>
<content type='text'>
Improved handling of try/catch

Better handling of unprovable constraints when the environment contains
false
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Improved handling of try/catch

Better handling of unprovable constraints when the environment contains
false
</pre>
</div>
</content>
</entry>
</feed>
