From 53ce89769a10be9a47af72b5fb440afa74bb4d02 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 9 Jul 2018 18:48:17 +0100
Subject: Lem: prefer type variables to constants when looking for equivalent
 nexps If we have an nexp that we can't print, look for an equivalent type
 variable before looking for a constant - the constant may only be valid
 locally (e.g., under an if) while the type variable will be valid throughout
 the function. Fixes a problem with aget_Mem on aarch64.

---
 src/pretty_print_lem.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'src/pretty_print_lem.ml')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c872d420..9897bb7c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -334,14 +334,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp = 
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
-       | Some n -> mk_typ (nconstant n)
-       | None ->
-          let is_equal nexp =
-            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-          | nexp -> mk_typ nexp
-          | exception Not_found -> None
+       let is_equal nexp =
+         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+       | nexp -> mk_typ nexp
+       | exception Not_found ->
+          match Type_check.solve env size with
+          | Some n -> mk_typ (nconstant n)
+          | None -> None
      end
   | _ -> None
 
-- 
cgit v1.2.3