summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2021-02-25 15:01:43 +0000
committerBrian Campbell2021-02-25 15:01:43 +0000
commitace7b32fe420234575ad7564f64c76309e3a74b3 (patch)
tree08d07586ee8199dceff9d0ab77fc453008118f9e /src
parentbb0a81f2170d068f561c6380bff500d568a7ffd3 (diff)
Remove accidental use of too-recent Option module
Also drop a related bit of dead code
Diffstat (limited to 'src')
-rw-r--r--src/sail.ml2
-rw-r--r--src/spec_analysis.ml7
-rw-r--r--src/spec_analysis.mli2
3 files changed, 5 insertions, 6 deletions
diff --git a/src/sail.ml b/src/sail.ml
index 00bff679..60dbc7ab 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -635,7 +635,7 @@ let main () =
let ast, type_envs =
if !opt_infer_effects then
- let ast = Spec_analysis.infer_effects (Option.value !opt_target ~default:"") ast in
+ let ast = Spec_analysis.infer_effects ast in
let _ = if reset_effect_checking then Type_check.opt_no_effects := true in
Type_error.check Type_check.initial_env ast
else ast, type_envs
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2588592b..8d0749fc 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -673,10 +673,9 @@ let update_effects effect_map ast =
in
{ ast with defs = List.map update_def ast.defs }
-let infer_effects target ast =
+let infer_effects ast =
let add_external_effects effect_map = function
- | DEF_spec (VS_aux (VS_val_spec(type_scheme, id, exts, _), _))
- (*when Option.is_some (Ast_util.extern_assoc target exts)*) ->
+ | DEF_spec (VS_aux (VS_val_spec(type_scheme, id, exts, _), _)) ->
let TypSchm_aux (TypSchm_ts (_, ty), _) = type_scheme in
begin match ty with
| Typ_aux (Typ_fn (_, _, eff), _) ->
@@ -691,7 +690,7 @@ let infer_effects target ast =
let components = NameGraph.scc ~original_order:original_order graph in
let add_def_effects effect_map name =
let callees = NameGraph.children graph name in
- let own_effect = Option.value (Namemap.find_opt name effect_map) ~default:no_effect in
+ let own_effect = match Namemap.find_opt name effect_map with Some e -> e | None -> no_effect in
let effects = List.fold_left (fun effects callee ->
match Namemap.find_opt callee effect_map with
| Some effect -> union_effects effects effect
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index b77434e7..2ac7bde1 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -79,7 +79,7 @@ val is_within_machine64 : typ -> nexp_range list -> triple *)
val top_sort_defs : tannot ast -> tannot ast
-val infer_effects : string -> tannot ast -> tannot ast
+val infer_effects : tannot ast -> tannot ast
(** Return the set of mutable variables assigned to in the given AST. *)
val assigned_vars : 'a exp -> IdSet.t