Mono: correct some type annotations in constant propagation

Including fixing nexp substitution in terms so that it doesn't remove attributes.
rems-project · Dec 7, 2023 · eb350e8 · eb350e8
1 parent 1ccaff3
commit eb350e8
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/src/lib/constant_propagation.ml b/src/lib/constant_propagation.ml
@@ -525,12 +525,12 @@ let const_props target ast =
         )
       | E_let (lb, e2) -> begin
           match lb with
-          | LB_aux (LB_val (p, e), annot) -> (
+          | LB_aux (LB_val (p, e), lb_annot) -> (
               let e', assigns = const_prop_exp substs assigns e in
               let substs' = remove_bound substs p in
               let plain () =
                 let e2', assigns = const_prop_exp substs' assigns e2 in
-                re (E_let (LB_aux (LB_val (p, e'), annot), e2')) assigns
+                re (E_let (LB_aux (LB_val (p, e'), lb_annot), e2')) assigns
               in
               match can_match l e' [Pat_aux (Pat_exp (p, e2), (Unknown, empty_tannot))] substs assigns with
               | None -> plain ()
@@ -542,10 +542,11 @@ let const_props target ast =
                   let tail_exp, tail_assigns = const_prop_exp substs'' assigns e'' in
                   ( List.fold_left
                       (fun (E_aux (_, t_annot) as t_exp) (id, bind_exp) ->
+                        let p_tannot = mk_tannot (env_of_annot (l, annot)) (typ_of bind_exp) in
                         E_aux
                           ( E_let
                               ( LB_aux
-                                  ( LB_val (P_aux (P_id id, (Generated l, empty_tannot)), bind_exp),
+                                  ( LB_val (P_aux (P_id id, (Generated l, p_tannot)), bind_exp),
                                     (Generated l, empty_tannot)
                                   ),
                                 t_exp

diff --git a/src/lib/spec_analysis.ml b/src/lib/spec_analysis.ml
@@ -727,8 +727,8 @@ let nexp_subst_fns substs =
   let s_typschm tsh = tsh in*)
   let s_tannot tannot =
     match Type_check.destruct_tannot tannot with
-    | None -> Type_check.empty_tannot
-    | Some (env, t) -> Type_check.mk_tannot env (s_t t)
+    | None -> tannot
+    | Some (_env, t) -> Type_check.replace_typ (s_t t) tannot
     (* TODO: what about env? *)
   in
   let rec s_pat (P_aux (p, (l, annot))) =