Add subtraction to nexp grammar (removing the need to do a + (-1 * b))

Fix up parsing on 2** precedence
Fix errors on type variables in function definition

1 files changed, 3 insertions, 2 deletions

diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 2724ba9c..1ea6df3e 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -141,12 +141,13 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   and nexp ne = sum_typ ne
   and sum_typ ((Nexp_aux(n,_)) as ne) = match n with
   | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2)
+  | Nexp_minus(n1,n2) -> doc_op minus (sum_typ n1) (star_typ n2)
   | _ -> star_typ ne
   and star_typ ((Nexp_aux(n,_)) as ne) = match n with
   | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2)
   | _ -> exp_typ ne
   and exp_typ ((Nexp_aux(n,_)) as ne) = match n with
-  | Nexp_exp n1 -> doc_unop (string "2**") (neg_typ n1)
+  | Nexp_exp n1 -> doc_unop (string "2**") (atomic_nexp_typ n1)
   | _ -> neg_typ ne
   and neg_typ ((Nexp_aux(n,_)) as ne) = match n with
   | Nexp_neg n1 ->
@@ -158,7 +159,7 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
   | Nexp_var v -> doc_var v
   | Nexp_constant i -> doc_int i
-  | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ ->
+  | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _ ->
       group (parens (nexp ne))
 
   (* expose doc_typ, doc_atomic_typ and doc_nexp *)