From ace7b32fe420234575ad7564f64c76309e3a74b3 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 25 Feb 2021 15:01:43 +0000 Subject: Remove accidental use of too-recent Option module Also drop a related bit of dead code --- src/sail.ml | 2 +- src/spec_analysis.ml | 7 +++---- src/spec_analysis.mli | 2 +- 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 -- cgit v1.2.3