Put missing cases into nexp_eq_check

4 files changed, 14 insertions, 7 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 25a9f41b..c56293ad 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1176,6 +1176,10 @@ let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc
 
 let pp_defs f d = print f (doc_defs d)
 let pp_exp b e = to_buf b (doc_exp e)
+let pat_to_string p = 
+  let b = Buffer.create 20 in
+  to_buf b (doc_pat p);
+  Buffer.contents b
 
 (****************************************************************************
  * PPrint-based sail-to-ocaml pretty printer, primarily for types
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 3fdf7841..dd12dd54 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -4,6 +4,7 @@ open Type_internal
 (* Prints the defs following source syntax *)
 val pp_defs : out_channel -> tannot defs -> unit
 val pp_exp : Buffer.t -> exp -> unit
+val pat_to_string : tannot pat -> string
 
 (* Prints on formatter the defs as Lem Ast nodes *)
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 9e28f6f5..93908eee 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -39,7 +39,7 @@ let rec rewrite_nexp_to_exp program_vars l nexp =
       | Nvar v -> (*TODO these need to generate an error as it's a place where there's insufficient specification. 
 		    But, for now I need to permit this to make power.sail compile, and most errors are in trap 
 		    or vectors *)
-	      (*let _ = Printf.eprintf "unbound variable here %s\n" v in *)
+	      (*let _ = Printf.eprintf "unbound variable here %s\n" v in*) 
 	E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) in
   match program_vars with
     | None -> actual_rewrite_n nexp
@@ -132,7 +132,7 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
     | E_internal_exp (l,impl) ->
       (match impl with
 	| Base((_,t),_,_,_,bounds) ->
-	  (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in *)
+	  (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in*) 
 	  match t.t with
 	    (*Old case; should possibly be removed*)
 	    | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
@@ -179,7 +179,7 @@ and rewrite_lexp (LEXP_aux(lexp,(l,annot))) =
 
 let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) = 
   let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = 
-    (*let _ = Printf.eprintf "Rewriting function %s\n" (match id with (Id_aux (Id i,_)) -> i) in*)
+    (*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n" (match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*)
     (FCL_aux (FCL_Funcl (id,pat,rewrite_exp exp),(l,annot))) 
   in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,annot))
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index eae11d6e..89f41bb0 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -761,9 +761,11 @@ and occurs_check_e (e_box : effect) (e : effect) : unit =
 (* Is checking for structural equality only, other forms of equality will be handeled by constraints *)
 let rec nexp_eq_check n1 n2 =
   match n1.nexp,n2.nexp with
+  | Npos_inf,Npos_inf | Nneg_inf,Nneg_inf | Ninexact,Ninexact -> true 
   | Nvar v1,Nvar v2 -> v1=v2
   | Nconst n1,Nconst n2 -> eq_big_int n1 n2
-  | Nadd(nl1,nl2), Nadd(nr1,nr2) | Nmult(nl1,nl2), Nmult(nr1,nr2) -> nexp_eq_check nl1 nr1 && nexp_eq_check nl2 nr2
+  | Nadd(nl1,nl2), Nadd(nr1,nr2) | Nmult(nl1,nl2), Nmult(nr1,nr2) | Nsub(nl1,nl2),Nsub(nr1,nr2) 
+    -> nexp_eq_check nl1 nr1 && nexp_eq_check nl2 nr2
   | N2n(n,Some i),N2n(n2,Some i2) -> eq_big_int i i2
   | N2n(n,_),N2n(n2,_) -> nexp_eq_check n n2
   | Nneg n,Nneg n2 -> nexp_eq_check n n2
@@ -2088,10 +2090,10 @@ let find_var_from_nexp n bounds =
 	| [] -> None
 	| b::bs -> (match b with
 	    | VR_eq(ev,n1) ->
-	      (*let _ = Printf.eprintf "checking if %s is eq to %s\n" (n_to_string n) (n_to_string n1) in*)
+	      (*let _ = Printf.eprintf "checking if %s is eq to %s, to bind to %s, eq? %b\n" (n_to_string n) (n_to_string n1) ev (nexp_eq_check n1 n) in*)
 	      if nexp_eq_check n1 n then Some (None,ev) else find_rec bs
 	    | VR_vec_eq (ev,n1)->
-	      (*let _ = Printf.eprintf "checking if %s is eq to %s\n" (n_to_string n) (n_to_string n1) in*)
+	      (*let _ = Printf.eprintf "checking if %s is eq to %s, to bind to %s, eq? %b\n" (n_to_string n) (n_to_string n1) ev (nexp_eq_check n1 n) in*)
 	      if nexp_eq_check n1 n then Some (Some "length",ev) else find_rec bs
 	    | _ -> find_rec bs) in
       find_rec bs
@@ -2668,7 +2670,7 @@ let rec simple_constraint_check in_env cs =
 	let occurs = occurs_in_nexp n2' n1' in
 	let leave = leave_nu_as_var n1' in
 	(*let _ = Printf.eprintf "occurs? %b, leave? %b n2' %s in n1' %s\n" occurs leave (n_to_string n2') (n_to_string n1') in*)
-        if (*not(u.nin) && *)ok_to_set && not(occurs) && not(leave)
+        if (*not(u.nin) &&*) ok_to_set && not(occurs) && not(leave)
         then if equate_n n1' n2' then None else (Some (Eq(co,n1',n2')))
         else if occurs
 	then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end