From 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 17 May 2019 17:59:03 +0100
Subject: Add constraints to undefined vector functions to ensure that lengths
 are sane, and an incomplete check on undefined literals.

---
 src/initial_check.ml |  6 +++---
 src/type_check.ml    | 13 ++++++++++++-
 2 files changed, 15 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..3f5592ba 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -923,9 +923,9 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}";
    extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-   (* Only used with lem_mwords *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order), 'n >= 0. (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
+   (* Only used with lem_mwords or coq *)
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n, 'n >= 0. atom('n) -> vector('n, dec, bit) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 2be68ade..3b42e4fa 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2900,7 +2900,18 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      else typ_error env l "List length didn't match" (* FIXME: improve error message *)
   | E_lit (L_aux (L_undef, _) as lit), _ ->
      if is_typ_monomorphic typ || Env.polymorphic_undefineds env
-     then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
+     then
+       (* This is a bit of a stop-gap measure; TODO: check undefined
+          literals for types that contain embedded vectors. *)
+       let () =
+         match destruct_vec_typ l env typ with
+         | (len, _, _) ->
+            if prove __POS__ env (nc_gteq len (nint 0))
+            then ()
+            else typ_error env l "Unable to prove that undefined vector has non-negative length"
+         | exception _ -> ()
+       in
+       annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
      else typ_error env l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
   | _, _ ->
      let inferred_exp = irule infer_exp env exp in
-- 
cgit v1.2.3