diff options
| author | Thomas Bauereiss | 2019-02-07 21:05:41 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-02-07 21:05:41 +0000 |
| commit | f397a40e6cf98b685dd15dfcd4ea2c9524cbfad7 (patch) | |
| tree | 69bd2ce0e8ea7dc8691432ef56f194fe420405a0 /src | |
| parent | 6fffd6ef54ab33441d08f40f56f27daa9c5b333e (diff) | |
Replace equality check for declared effects by subset check
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 5 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 4 |
3 files changed, 8 insertions, 2 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 63726304..396d72a3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1196,6 +1196,11 @@ let equal_effects e1 e2 = | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) -> BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0 +let subseteq_effects e1 e2 = + match e1, e2 with + | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) -> + BESet.subset (BESet.of_list base_effs1) (BESet.of_list base_effs2) + let rec kopts_of_nexp (Nexp_aux (nexp,_)) = match nexp with | Nexp_id _ diff --git a/src/ast_util.mli b/src/ast_util.mli index d9b0110a..7100cde7 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -357,6 +357,7 @@ val has_effect : effect -> base_effect_aux -> bool val effect_set : effect -> BESet.t val equal_effects : effect -> effect -> bool +val subseteq_effects : effect -> effect -> bool val union_effects : effect -> effect -> effect val kopts_of_order : order -> KOptSet.t diff --git a/src/type_check.ml b/src/type_check.ml index 7faa0234..b2bf0f5b 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2641,7 +2641,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ annot_exp (E_if (cond', then_branch', else_branch')) typ end | E_exit exp, _ -> - let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in + let checked_exp = crule check_exp env exp unit_typ in annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape]) | E_throw exp, _ -> let checked_exp = crule check_exp env exp exc_typ in @@ -4627,7 +4627,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) else [], env, declared_eff in let env = Env.define_val_spec id env in - if (equal_effects eff declared_eff || !opt_no_effects) + if (subseteq_effects eff declared_eff || !opt_no_effects) then vs_def @ [DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None)))], env else typ_error env l ("Effects do not match: " ^ string_of_effect declared_eff ^ " declared and " ^ string_of_effect eff ^ " found") |