diff options
| author | Alasdair | 2019-02-08 00:51:27 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-08 00:51:27 +0000 |
| commit | c2e69e8334cba2f0898c73bcb8ca6cce15858fbf (patch) | |
| tree | 48fe5d17fe94a0fe0e8229ea9e3085470753b3f1 /src/rewrites.ml | |
| parent | f397a40e6cf98b685dd15dfcd4ea2c9524cbfad7 (diff) | |
Remove dead code from type-checker
add_num_def and get_num_def are no longer used. The rewrite pass that
used them would fail on Nexp_ids because of this, but seeing as that
never happened we can probably assume that particular line of code is
simply never touched by any of our models or test suite?
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 5cbc3545..45b6fd6c 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -238,7 +238,7 @@ let lookup_constant_kid env kid = List.fold_left check_nc None (Env.get_constraints env) let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with - | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env) + | Nexp_id id -> Env.expand_nexp_synonyms env nexp_aux | Nexp_var kid -> begin match lookup_constant_kid env kid with @@ -2909,7 +2909,6 @@ let rewrite_defs_internal_lets = type of the storage, so ask the type checker what it really is. *) (match infer_lexp (env_of_annot lannot) (strip_lexp lhs) with | LEXP_aux (_,lexp_annot') -> lexp_annot' - | _ -> lannot | exception _ -> lannot) in let rhs = add_e_cast ltyp (rhs exp) in |
