Allow user defined operations in nexps (experimental)

There are several key changes here:

1) This commit allows for user defined operations in n-expressions
using the Nexp_app constructor. These operations are linked to
operators in the SMT solver, by using the smt extern when defining
operations. Notably, this allows integer division and modular
arithmetic to be used in types. This is best demonstrated with an
example:

infixl 7 /
infixl 7 %

val operator / = {
  smt: "div",
  ocaml: "quotient"
} : forall 'n 'm, 'm != 0. (atom('n), atom('m)) -> {'o, 'o = 'n / 'm. atom('o)}

val mod_atom = {
  smt: "mod",
  ocaml: "modulus"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod_atom('n, 'm). atom('o)}

val "print_int" : (string, int) -> unit

overload operator % = mod_atom

val main : unit -> unit

function main () = {
  let 'm : {'x, 'x % 3 = 1. atom('x)} = 4;
  let 'n = m / 3;
  _prove(constraint(('m - 1) % 3 = 0));
  _prove(constraint('n * 3 + 1 = 'm));
  (* let x = 3 / 0; (* Will fail *) *)
  print_int("n = ", n);
  ()
}

As can be seen, these nexp ops can be arbitrary user defined operators
and even operator overloading works (although there are some caveats).

This feature is very experimental, and some things won't work very
well once you use custom operators - notably unification. However,
this not necissarily a downside, because if restrict yourself to the
subset of sail types that correspond to liquid types, then there is
never a need to unify n-expressions. Looking further ahead, if we
switch to a liquid type system a la minisail, then we no longer need
to treat + - and * specially in n-expressions. So possible future
refactorings could involve collapsing the Nexp datatype.

2) The typechecker is stricter about valspecs (and other types) being
well-formed. This is a breaking change because previously we allowed
things like:

val f : atom('n) -> atom('n)

and now this must be

val f : forall 'n. atom('n) -> atom('n)

if we want to allow the first syntax, then initial-check should
desugar it this way - but it must be well-formed by the time it hits
the type-checker, otherwise it's not clear that we do the right
thing. Note we can actually have top-level type variables by using
top-level let bindings with P_var. There's a future line of
refactoring that would make it so that type variables can shadow each
other properly (we should do this) - currently they all have to have
unique names.

3) atom('n) is no longer syntactic sugar for range('n, 'n). The reason
why we want to do this is that if we wanted to be smart about what
sail operations can be translated into SMT operations at the type
level we care very much that they talk about atoms and not
ranges. Why? Because atom is the term level representation of a
specific type variable so it's clear how to map between term level
functions and type level functions, i.e. (atom('n) -> atom('n)) can be
reflected at the type level by a type level function with kind Int ->
Int, but the same is not true for range. Furthermore, both are
interdefinable as

atom('n) -> range('n, 'n)
range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('n)}

and I think the second is actually slightly more elegant. This change
*should* be backwards compatible, as the type-checker knows how to
convert from atom to ranges and unify them with each other, but there
may be bugs introduced here...

0 files changed, 0 insertions, 0 deletions