Add well-formedness check for type schemes in valspecs.

Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).

4 files changed, 19 insertions, 7 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7a42950c..1f550c73 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1855,7 +1855,13 @@ let order_subst_aux sv subst = function
 
 let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l)
 
-let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
+let rec nexp_subst sv subst = function
+  | (Nexp_aux (Nexp_var kid, l)) as nexp ->
+     begin match subst with
+     | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> n
+     | _ -> nexp
+     end
+  | Nexp_aux (nexp, l) -> Nexp_aux (nexp_subst_aux sv subst nexp, l)
 and nexp_subst_aux sv subst = function
   | Nexp_var kid ->
      begin match subst with
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 93579420..8670139f 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3439,7 +3439,7 @@ let add_bitvector_casts (Defs defs) =
       mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false))
     in
     let defs = List.map mkfn (IdSet.elements !specs_required) in
-    check Env.empty (Defs defs)
+    check initial_env (Defs defs)
   in Defs (cast_specs @ defs)
 end
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 4ea52c4d..e3864a7f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1440,7 +1440,7 @@ let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base
      write_reg_ref (vector_access (GPR, i)) exp
  *)
 let rewrite_register_ref_writes (Defs defs) =
-  let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
+  let (Defs write_reg_spec) = fst (Type_error.check initial_env (Defs (List.map gen_vs
     [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in
   let lexp_ref_exp (LEXP_aux (_, annot) as lexp) =
     try
@@ -1630,7 +1630,7 @@ let rewrite_defs_early_return env (Defs defs) =
     FD_aux (FD_function (rec_opt, tannot_opt, effect_opt,
       List.map (rewrite_funcl_early_return rewriters) funcls), a) in
 
-  let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs
+  let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs
     ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in
 
   rewrite_defs_base
@@ -3771,7 +3771,7 @@ let rewrite_defs_remove_superfluous_returns env =
 
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
-  let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
+  let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs
     [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
      ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
      ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
diff --git a/src/type_check.ml b/src/type_check.ml
index 9c37f5c9..02e32f4d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -825,10 +825,11 @@ end = struct
     | A_typ typ -> wf_typ ~exs:exs env typ
     | A_order ord -> wf_order env ord
     | A_bool nc -> wf_constraint ~exs:exs env nc
-  and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
+  and wf_nexp ?exs:(exs=KidSet.empty) env nexp =
     wf_debug "nexp" string_of_nexp nexp exs;
+    let Nexp_aux (nexp_aux, l) = expand_nexp_synonyms env nexp in
     match nexp_aux with
-    | Nexp_id _ -> ()
+    | Nexp_id id -> typ_error env l ("Undefined synonym " ^ string_of_id id)
     | Nexp_var kid when KidSet.mem kid exs -> ()
     | Nexp_var kid ->
        begin match get_typ_var kid env with
@@ -1324,6 +1325,10 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
 let expand_bind_synonyms l env (typq, typ) =
   typq, Env.expand_synonyms (add_typquant l typq env) typ
 
+let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) =
+  let env = add_typquant l typq env in
+  Env.wf_typ env typ
+
 (* Create vectors with the default order from the environment *)
 
 let default_order_error_string =
@@ -4899,6 +4904,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
   let vs, id, typq, typ, env = match vs with
     | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) ->
        typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
+       wf_typschm env typschm;
        let env = Env.add_extern id exts env in
        let env = if is_cast then Env.add_cast id env else env in
        let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in