diff options
| author | Brian Campbell | 2018-07-09 18:48:17 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-09 19:03:16 +0100 |
| commit | 53ce89769a10be9a47af72b5fb440afa74bb4d02 (patch) | |
| tree | 6d7457af1b7c0e33ee4e269be9808ce247def52e /src | |
| parent | b71a0574ee9b9ae1d80e91a13915b16fbdf0f405 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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 |