diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 23 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 6 | ||||
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 4 |
5 files changed, 21 insertions, 17 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 23f81f0e..cdff2972 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -34,6 +34,9 @@ let inline (>>) m n = m >>= fun _ -> n val exit : forall 'a 'b. 'b -> M 'a let exit s = Fail Nothing +val assert_exp : bool -> string -> M unit +let assert_exp exp msg = if exp then Done () else Fail (Just msg) + val early_return : forall 'r. 'r -> MR unit 'r let early_return r = Return r diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 1ca25b74..cbec7204 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -19,18 +19,18 @@ type sequential_state 'regs = and exception type 'e. *) type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs) -(* Most of the time, we don't distinguish between different types of exceptions *) -type M 'regs 'a = ME 'regs 'a unit +(* By default, we use strings to distinguish between different types of exceptions *) +type M 'regs 'a = ME 'regs 'a string (* For early return, we abuse exceptions by throwing and catching - the return value. The exception type is "maybe 'r", where "Nothing" - represents a proper exception and "Just r" an early return of value "r". *) -type MR 'regs 'a 'r = ME 'regs 'a (maybe 'r) + the return value. The exception type is "either 'r string", where "Right e" + represents a proper exception and "Left r" an early return of value "r". *) +type MR 'regs 'a 'r = ME 'regs 'a (either 'r string) val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r let liftR m s = List.map (function | (Left a, s') -> (Left a, s') - | (Right (), s') -> (Right Nothing, s') + | (Right e, s') -> (Right (Right e), s') end) (m s) val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e @@ -48,17 +48,20 @@ val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b let inline (>>) m n = m >>= fun _ -> n val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a -let exit _ s = [(Right (), s)] +let exit _ s = [(Right "exit", s)] + +val assert_exp : forall 'regs. bool -> string -> M 'regs unit +let assert_exp exp msg s = if exp then [(Left (), s)] else [(Right msg, s)] val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r -let early_return r s = [(Right (Just r), s)] +let early_return r s = [(Right (Left r), s)] val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a let catch_early_return m s = List.map (function - | (Right (Just a), s') -> (Left a, s') - | (Right Nothing, s') -> (Right (), s') + | (Right (Left a), s') -> (Left a, s') + | (Right (Right e), s') -> (Right e, s') | (Left a, s') -> (Left a, s') end) (m s) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 7d0d3459..67febd0a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1029,10 +1029,8 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e;]) | E_assert (e1,e2) -> - (* FIXME needs pretty-printing of E_constraint; ignore for now *) - string "()" - (* let epp = separate space [string "assert'"; expY e1; expY e2] in - if aexp_needed then parens (align epp) else align epp *) + let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in + if aexp_needed then parens (align epp) else align epp | E_app_infix (e1,id,e2) -> (* TODO: Should have been removed by the new type checker; check with Alasdair *) raise (Reporting_basic.err_unreachable l diff --git a/src/rewriter.ml b/src/rewriter.ml index 99f7b15f..c537e196 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -165,7 +165,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_exit e -> union_effects eff (effect_of e) | E_return e -> union_effects eff (effect_of e) | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect - | E_assert (c,m) -> union_eff_exps [c; m] + | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m]) | E_comment _ | E_comment_struc _ -> no_effect | E_internal_cast (_,e) -> effect_of e | E_internal_exp _ -> no_effect diff --git a/src/type_check.ml b/src/type_check.ml index 751e70e5..816f6d04 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1891,7 +1891,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let nc = assert_constraint env constr_exp in 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 + let texp = annot_exp_effect (E_assert (cexp, checked_msg)) unit_typ (mk_effect [BE_escape]) in texp :: check_block l (Env.add_constraint nc env) exps typ with | Not_a_constraint -> check_block l env exps typ @@ -2705,7 +2705,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_assert (test, msg) -> let checked_test = crule check_exp env test bool_typ in let checked_msg = crule check_exp env msg string_typ in - annot_exp (E_assert (checked_test, checked_msg)) unit_typ + annot_exp_effect (E_assert (checked_test, checked_msg)) unit_typ (mk_effect [BE_escape]) | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp) and infer_funapp l env f xs ret_ctx_typ = fst (infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ) |