GitLab

Removed a special case in the parser for FuncRefV constants, which
required every SSA variable to have a known type. This required
BundleParser to be rearranged to parse everything else before function
bodies, making functions available to functions defined above them
(something the spec requires, so that's progress!)

Also added support for COMMINST in the parser.

uvmThreadSemantics was becoming a huge file that took several minutes
to compile, so it's been split into uvmThreadsStacks and
uvmInstructionSemantics.

In uvmThreadsStacks, new 'thread_ok' and 'stack_ok' predicates define
basic consistency requirements for thread and stack data structures.
All functions in this file have also been proven to produce valid
thread/stack structures when given valid input. This is a prerequisite
for proving execution state homomorphisms.

'thread_state' has been renamed to 'thread', and 'state_follows' has
been renamed to 'thread_follows'.

The current version of the Mu specification does not use $-variables to
pass return values from terminsts to the normal destination of an EXC
clause, instead allowing terminsts to have normal SSA return values
that may be referenced in the EXC clause. This commit updates the
formalism to match.

Several other refactorings are included, such as making exec_terminst
only return modified stacks, using a simpler representation of common
instructions, and defining prefix/infix operators for SSA variables and
registers in HOL.

The NEWTHREAD instruction isn't parsed yet, but its associated memory message is
now supported, and the scheduler has been modified to support multiple threads.

thread_states are now generated on-demand when they are first executed, provided
there is an associated DoNewThread memory action and its stack ID can be
resolved. This required the 'tid' field of 'Message' to be changed to a
'thread_id option', as there must be an initial DoNewThread action that is not
generated by any thread ID.

The THROW instruction and EXC resume_values have also been updated to have only
one argument, to match the spec.

Translation method now uses an intermediary type datastructure.
It is similar to the previous method which was done in two stages.

To do:
  - Clean up code base
  - Add abstractions
  - Fix the testing script

The translation method has been changed into two phases. The first is to
determine the final type of what the translated term would be. The
second, is with this type information, to create the final translated
term.

To do:
  -- Implement abstractions for translation

The datatype translation seems to be working now for standard sets.
Currently abstractions need to be implementation and also a mechanism to
generally translate theorems and other objects in hol.

Currently the expected translation function works for constants. This
needs to be extended for other term types.

The robustness of the type inference can also be improved on.
Currently the new type is generated by appending new elements to a list
which has an implicit ordering.

Basic testcases work with valid typing.

To do:
  -- Add type-checking to provide an error when set functions cannot be
translated
  -- Add other cases

Appart from creating the standard ml framework for input files for
s-expressions, the majority of the testing with the small language is
complete.

To do:
  - Start translating the main project

Script added parses an s-expression into a statement in the defined
lanugage. Translation is successful. (Note: do notation in function
definitions will not translate)

To do:
  - Create test cases for the s-expression parser
  - Create a parser for enviromental variables
  - Create framework for inputing s-expressions in sml

Bugs fixed are the missing case in the schedule script.
Naming inconsistencies were rectified in the different scripts.
The folder hierarchy was also fixed.

The extExprScript.sml theorem has successfully been able to create a
translation file which has sml code in it.

A seperate script file was created where all the translation of HOL4
code will occur. Another script file will then translate that code from
a theorem to an output .ml.txt file.

Things To Do:
  -- Translate the reset of the files
  -- Remove the translation commands in the original script files

Attempts in proofs also in comments

The new symbolic computation system finally works! Factorial runs again, albeit
slower than before. Load/Store isn't working yet, but only because global cells
aren't preallocated.

Because the Mu spec says that newly-allocated memory locations are zeroed out,
option values for unallocated spaces in data structures have been removed, and
newly-allocated values are filled with 0/NULL.

The "translate" function was called on the find_steps function and the
eval_n_steps function. Holmake did not return an error so the
compatibility of the HOL functions to cakeml is assumed to be good.

Notes:
  -- When functions in HOL are being translated all functions within
that function must be previously translated explicitly.
  -- It seems that CakeML does not translate lambda expressions well.
  -- Functions must be translated explicitly again when calling from
another library/script

Things To Do:
  -- Compile the HOL code using CakeML.
  -- Explore S-expressions.
  -- Fix the fibonacci test, it partially works but fib_n_def does not
seem to evaluate down to a number, only some-kind of expression format.
  -- Prove some properties about the expression language.