Adding Support for User Defined Datatypes and Logical Functions

[NatKarmios]

Originally from #342; made a new PR so the branch can be under this repo.

Example of the type of specifications that these new features allow for can be found in wisl/examples/SLL_adt.wisl.

User Defined Datatypes

Added WISL support for user defined datatypes:

• Updated parser
• Extended AST
• Updated compiler

Added support for user defined datatypes in core Gillian:

• Created a Datatype_env to hold definitions
• Extended AST to allow application of datatype constructors within GIL expressions
• Extended AST to allow matching of expressions with datatype constructors
• Extended typing algorithm to handle expressions involving constructor application / case matching
• Extended matching plans to allow bindings to be learnt from equalities involiving constructor applications
• Added reductions of expressions involving constructor applications
• Implemented encoding into SMT

User Defined Functions

Added WISL support for user defined functions:

• Updated parser
• Extended AST
• Updated compiler

Added support for user defined functions in core Gillian:

• Created a Function_env to hold definitions
• Extended AST to allow application of functions within GIL expressions
• Extended typing algorithm to handle expressions involving function application
• Implemented encoding into SMT

Notes

General

• Constructor applications in WISL are prefixed by a quote mark ' to differentiate it from function application in the parsing. This was mainly a quick fix, and I'm happy to take suggestions on other approaches!
• Similarly, pure function denotes a logical function used in specifications, whereas function represents a procedure.
• Moved smt.ml into engine/FOLogic/ in order to avoid circular dependencies: smt.ml requires Datatype_env, from the engine module, but engine requires smt.ml.
• Datatype_env and Function_env are mutable global references. This is for a couple of reasons. Firstly, unlike the typing environment, they aren't modified or copied or replaced during symbolic execution. They are initialised once and stay constant throughout. Secondly, it is too much of a pain to refactor every occurence of gamma to also carry around a Datatype_env and a Function_env. There are some functions which even make gamma optional, however, the other two environments are always a necessity! I did try this approach but it proved to be too much work.
  Datatype_env and Function_env are provided via effects and relevant handlers; see Prog_env under Gil_syntax for more.
• Unsure of how to handle compilation of wisl pointer arithmetic in the body of pure functions. Have just compiled as plain addition / subtraction for now. Could introduce if then else expressions, and then these pointer arithmetic operations would be expressible as a GIL Expression.

SMT Encoding

• The initial declarations are dependent on the datatypes and functions declared, so initialisation is now delayed until the first query is given to the solver. At this point, the Datatype_env and Function_env are assumed to be initialised.
• Added extra assertions when applying a destructor to an SMT-LIB ADT: In SMT-LIB, if you apply a destructor of a datatype to a value not constructed by the corresponding constructor, the behavior is generally unspecified. This lead to some queries returning sat when they should have been unsat. As a result, we add additional assertions to ensure that expressions were in-fact constructed by the constructor corresponding to the destructor.

[NatKarmios]

From @AndreasLoow:

Repeating here what I said in Discord:

Constructor applications in WISL are prefixed by a quote mark ' to differentiate it from function application in the parsing. This was mainly a quick fix, and I'm happy to take suggestions on other approaches!

I think this should be fixed before merge.

[NatKarmios]

Not a fan of global singletons 😛

[shiva-tk]

Yeah I remember this bit was super ugly! I didn't have time in my master's project to do the robust thing, and carry the env around everywhere.

Maybe after POPL deadline I'll get round to fixing this.

[NatKarmios]

I have a couple days to kill until my internship, I'm taking a look now :-)

[NatKarmios]

That was a hell of a merge hahah
I've moved Datatype_env and Function_env under a Prog_env, which is part of Gil_syntax. Instead of a global reference, it's managed with effect handlers.
Any entrypoint to Gillian should now use Prog_env.using_prog or similar after compilation.

[NatKarmios]

waow it's passing tests