diff options
| author | Brian Campbell | 2019-06-10 17:53:58 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-06-10 17:53:58 +0100 |
| commit | 3eadd260f7382f98eb7dcbd706a3ed3e910167eb (patch) | |
| tree | ab2d8fec7c2c765abc6af3954c8694bab30a707e /src/rewrites.ml | |
| parent | 534b659d7acccabe7219dc3773f6b09d612bbd86 (diff) | |
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).
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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"); |