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...

1 files changed, 21 insertions, 19 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index 5dcc10f0..37073ff2 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -3,27 +3,33 @@ open Util
 
 (* ===== Integer Constraints ===== *)
 
-type nexp_op = Plus | Minus | Mult
+type nexp_op = string
 
 type nexp =
-  | NFun of (nexp_op * nexp * nexp)
+  | NFun of (nexp_op * nexp list)
   | N2n of nexp
   | NConstant of big_int
   | NVar of int
 
-let big_int_op : nexp_op -> big_int -> big_int -> big_int = function
-  | Plus -> add_big_int
-  | Minus -> sub_big_int
-  | Mult -> mult_big_int
+let big_int_op : nexp_op -> (big_int -> big_int -> big_int) option = function
+  | "+" -> Some add_big_int
+  | "-" -> Some sub_big_int
+  | "*" -> Some mult_big_int
+  | _ -> None
 
 let rec arith constr =
   let constr' = match constr with
-    | NFun (op, x, y) -> NFun (op, arith x, arith y)
+    | NFun (op, [x; y]) -> NFun (op, [arith x; arith y])
     | N2n c -> N2n (arith c)
     | c -> c
   in
   match constr' with
-  | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y)
+  | NFun (op, [NConstant x; NConstant y]) as c ->
+     begin
+       match big_int_op op with
+       | Some op -> NConstant (op x y)
+       | None -> c
+     end
   | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x)
   | c -> c
 
@@ -63,7 +69,7 @@ module IntSet = Set.Make(
 let rec nexp_vars : nexp -> IntSet.t = function
   | NConstant _ -> IntSet.empty
   | NVar v -> IntSet.singleton v
-  | NFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y)
+  | NFun (_, xs) -> List.fold_left IntSet.union IntSet.empty (List.map nexp_vars xs)
   | N2n x -> nexp_vars x
 
 let rec constraint_vars : nexp constraint_bool -> IntSet.t = function
@@ -98,14 +104,8 @@ let cop_sexpr op x y =
   | Eq -> sfun "=" [x; y]
   | NEq -> sfun "not" [sfun "=" [x; y]]
 
-let iop_sexpr op x y =
-  match op with
-  | Plus -> sfun "+" [x; y]
-  | Minus -> sfun "-" [x; y]
-  | Mult -> sfun "*" [x; y]
-
 let rec sexpr_of_nexp = function
-  | NFun (op, x, y) -> iop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y)
+  | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs)
   | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x]
   | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *)
   | NVar var -> Atom ("v" ^ string_of_int var)
@@ -245,11 +245,13 @@ let neq x y : t = CFun (NEq, x, y)
 
 let pow2 x : nexp = N2n x
 
-let add x y : nexp = NFun (Plus, x, y)
+let add x y : nexp = NFun ("+", [x; y])
+
+let sub x y : nexp = NFun ("-", [x; y])
 
-let sub x y : nexp = NFun (Minus, x, y)
+let mult x y : nexp = NFun ("*", [x; y])
 
-let mult x y : nexp = NFun (Mult, x, y)
+let app f xs : nexp = NFun (f, xs)
 
 let constant (x : big_int) : nexp = NConstant x