diff options
| author | Brian Campbell | 2017-08-14 15:04:38 +0100 |
|---|---|---|
| committer | Brian Campbell | 2017-08-14 15:04:38 +0100 |
| commit | 42a0675290b5fbf61cab24c1d87ce2d85da639cd (patch) | |
| tree | a982c898d0e541bc0cad1f8488438a88eadd06da /src | |
| parent | 9650491762d389fe84aa96a63efc535bdbd9c5de (diff) | |
Keep all asserts in the program during type checking
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index dbaeb98f..a2481f3f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1852,7 +1852,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ begin try let nc = assert_constraint const_expr in - check_block l (Env.add_constraint nc env) exps typ + let cexp = annot_exp (E_constraint nc) bool_typ in + let checked_msg = crule check_exp env assert_msg string_typ in + let texp = annot_exp (E_assert (cexp, checked_msg)) unit_typ in + texp :: check_block l (Env.add_constraint nc env) exps typ with | Not_a_constraint -> check_block l env exps typ end |
