Experimenting with power spec

15 files changed, 49 insertions, 43 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 20697005..7e3e0da7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -375,7 +375,7 @@ and map_exp_annot_aux f = function
   | E_comment str -> E_comment str
   | E_comment_struc exp -> E_comment_struc (map_exp_annot f exp)
   | E_internal_value v -> E_internal_value v
-  | E_internal_let (lexp, exp1, exp2) -> E_internal_let (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
+  | E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_return exp -> E_internal_return (map_exp_annot f exp)
 and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_default_annot_aux f df, f annot)
@@ -628,7 +628,7 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_internal_exp_user _ -> "INTERNAL EXP USER"
   | E_comment _ -> "INTERNAL COMMENT"
   | E_comment_struc _ -> "INTERNAL COMMENT STRUC"
-  | E_internal_let _ -> "INTERNAL LET"
+  | E_var _ -> "INTERNAL LET"
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
   | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
   | _ -> "INTERNAL"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index c44a3b42..4fde87cd 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -513,6 +513,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
     | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_var(lexp,exp1,exp2) -> E_var(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
     | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp)
     | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc)
     | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 04ecdca3..e2361a04 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -129,6 +129,7 @@ let kw_table =
      ("in",			 (fun x -> In));
      ("inc",                     (fun _ -> Inc));
      ("let",                     (fun x -> Let_));
+     ("var",                     (fun _ -> Var));
      ("record",                  (fun _ -> Record));
      ("Int",                     (fun x -> Int));
      ("Order",                   (fun x -> Order));
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index ff264642..af3484ec 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -551,7 +551,7 @@ let nexp_subst_fns substs =
       | E_assert (e1,e2) -> re (E_assert (s_exp e1,s_exp e2))
       | E_internal_cast ((l,ann),e) -> re (E_internal_cast ((l,s_tannot ann),s_exp e))
       | E_comment_struc e -> re (E_comment_struc e)
-      | E_internal_let (le,e1,e2) -> re (E_internal_let (s_lexp le, s_exp e1, s_exp e2))
+      | E_var (le,e1,e2) -> re (E_var (s_lexp le, s_exp e1, s_exp e2))
       | E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
       | E_internal_return e -> re (E_internal_return (s_exp e))
       | E_throw e -> re (E_throw (s_exp e))
@@ -1040,7 +1040,7 @@ let split_defs splits defs =
     | E_comment_struc e -> re (E_comment_struc e) assigns
 
     | E_app_infix _
-    | E_internal_let _
+    | E_var _
     | E_internal_plet _
     | E_internal_return _
       -> raise (Reporting_basic.err_unreachable l
@@ -1458,7 +1458,7 @@ let split_defs splits defs =
       | E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
       | E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))
       | E_comment_struc e -> re (E_comment_struc e)
-      | E_internal_let (le,e1,e2) -> re (E_internal_let (map_lexp le, map_exp e1, map_exp e2))
+      | E_var (le,e1,e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
       | E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
       | E_internal_return e -> re (E_internal_return (map_exp e))
     and map_opt_default ((Def_val_aux (ed,annot)) as eda) =
@@ -2227,7 +2227,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
       -> raise (Reporting_basic.err_unreachable l
                   ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
        
-    | E_internal_let (lexp,e1,e2) ->
+    | E_var (lexp,e1,e2) ->
        (* Really we ought to remove the assignment after e2 *)
        let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in
        let assigns,r' = analyse_lexp fn_id env assigns d1 lexp in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 273ca829..f753b907 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -254,7 +254,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_let (lb, exp) ->
      separate space [string "let"; ocaml_letbind ctx lb; string "in"]
      ^/^ ocaml_exp ctx exp
-  | E_internal_let (lexp, exp1, exp2) ->
+  | E_var (lexp, exp1, exp2) ->
      separate space [string "let"; ocaml_atomic_lexp ctx lexp;
                      equals; string "ref"; parens (ocaml_atomic_exp ctx exp1 ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (Rewrites.simple_typ (typ_of exp1))); string "in"]
      ^/^ ocaml_exp ctx exp2
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index bfbb0090..df4c2d2c 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -296,7 +296,7 @@ exp_aux =  (* Expression *)
  | E_try of exp * pexp list
  | E_return of exp
  | E_assert of exp * exp
- | E_internal_let of exp * exp * exp
+ | E_var of exp * exp * exp
 
 and exp = 
    E_aux of exp_aux * l
diff --git a/src/parser2.mly b/src/parser2.mly
index 140f1b86..74812d1e 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -152,7 +152,7 @@ let rec desugar_rchain chain s e =
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union With Val Constraint Throw Try Catch Exit
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
-%token Repeat Until While Do Record Mutual
+%token Repeat Until While Do Record Mutual Var
 
 %nonassoc Then
 %nonassoc Else
@@ -705,6 +705,8 @@ exp:
     { mk_exp (E_assign ($1, $3)) $startpos $endpos }
   | Let_ letbind In exp
     { mk_exp (E_let ($2, $4)) $startpos $endpos }
+  | Var atomic_exp Eq exp In exp
+    { mk_exp (E_var ($2, $4, $6)) $startpos $endpos }
   | Lcurly block Rcurly
     { mk_exp (E_block $2) $startpos $endpos }
   | Return exp
@@ -935,6 +937,8 @@ block:
     { [$1] }
   | Let_ letbind Semi block
     { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] }
+  | Var atomic_exp Eq exp Semi block
+    { [mk_exp (E_var ($2, $4, mk_exp (E_block $6) $startpos($6) $endpos)) $startpos $endpos] }
   | exp Semi /* Allow trailing semicolon in block */
     { [$1] }
   | exp Semi block
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ae332b39..3827376f 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -847,8 +847,8 @@ let doc_exp_lem, doc_let_lem =
     | E_app_infix (e1,id,e2) ->
        raise (Reporting_basic.err_unreachable l
          "E_app_infix should have been rewritten before pretty-printing")
-    | E_internal_let(lexp, eq_exp, in_exp) ->
-       raise (report l "E_internal_lets should have been removed before pretty-printing")
+    | E_var(lexp, eq_exp, in_exp) ->
+       raise (report l "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
        let epp =
          let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index bcf997d4..176fcd2e 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -432,8 +432,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
       raise (Reporting_basic.err_unreachable l "Found internal cast or exp")
     | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user"))
     | E_sizeof_internal _ -> (raise (Reporting_basic.err_unreachable l "Internal sizeof not removed"))
-    | E_internal_let (lexp,exp1,exp2) ->
-      fprintf ppf "@[<0>(E_aux (E_internal_let %a %a %a) (%a, %a))@]"
+    | E_var (lexp,exp1,exp2) ->
+      fprintf ppf "@[<0>(E_aux (E_var %a %a %a) (%a, %a))@]"
         pp_lem_lexp lexp pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_l l pp_annot annot
     | E_internal_return exp ->
       fprintf ppf "@[<0>(E_aux (E_internal_return %a) (%a, %a))@]"
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b7cd3761..30eb71e0 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -186,7 +186,7 @@ let doc_exp, doc_let =
   | E_app_infix(l,(Id_aux(Id "**",_) as op),r) ->
       doc_op (doc_id op) (starstar_exp l) (app_exp r)
   | E_if _ | E_for _ | E_loop _ | E_let _
-  | E_internal_let _ | E_internal_plet _ -> right_atomic_exp expr
+  | E_var _ | E_internal_plet _ -> right_atomic_exp expr
   | _ -> app_exp expr
   and right_atomic_exp ((E_aux(e,_)) as expr) = match e with
   (* Special case: omit "else ()" when the else branch is empty. *)
@@ -217,7 +217,7 @@ let doc_exp, doc_let =
       )) ^/^
       exp exp4
   | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
-  | E_internal_let (lexp, exp1, exp2) ->
+  | E_var (lexp, exp1, exp2) ->
      let le =
        prefix 2 1
          (separate space [string "internal_let"; doc_lexp lexp; equals])
@@ -324,7 +324,7 @@ let doc_exp, doc_let =
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
   | E_if _ | E_for _ | E_loop _ | E_let _
-  | E_internal_let _ | E_internal_plet _
+  | E_var _ | E_internal_plet _
   | E_vector_append _
   | E_app_infix (_,
     (* for every app_infix operator caught at a higher precedence,
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 71fcd587..0f1ee016 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -304,7 +304,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
          (separate space [string "internal_plet"; doc_pat pat; equals])
          (doc_exp exp1) in
      doc_op (string "in") le (doc_exp exp2)
-  | E_internal_let (lexp, binding, exp) ->
+  | E_var (lexp, binding, exp) ->
      separate space [string "var"; doc_lexp lexp; equals; doc_exp binding; string "in"; doc_exp exp]
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
@@ -384,7 +384,7 @@ and doc_block = function
   | [] -> string "()"
   | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
      separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
-  | [E_aux (E_internal_let (lexp, binding, E_aux (E_block exps, _)), _)] ->
+  | [E_aux (E_var (lexp, binding, E_aux (E_block exps, _)), _)] ->
      separate space [string "var"; doc_lexp lexp; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
   | [exp] -> doc_exp exp
   | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps
diff --git a/src/rewriter.ml b/src/rewriter.ml
index a639dd3f..fb82b80f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -142,7 +142,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_internal_cast (_,e) -> effect_of e
     | E_internal_exp _ -> no_effect
     | E_internal_exp_user _ -> no_effect
-    | E_internal_let (lexp,e1,e2) ->
+    | E_var (lexp,e1,e2) ->
       union_effects (effect_of_lexp lexp)
         (union_effects (effect_of e1) (effect_of e2))
     | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2)
@@ -322,8 +322,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
   | E_internal_cast (casted_annot,exp) ->
     rewrap (E_internal_cast (casted_annot, rewrite exp))
-  | E_internal_let (lexp, e1, e2) ->
-     rewrap (E_internal_let (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
+  | E_var (lexp, e1, e2) ->
+     rewrap (E_var (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
   | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
   | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced")
   | _ -> rewrap exp
@@ -579,7 +579,7 @@ let rec fold_exp_aux alg = function
   | E_internal_exp_user (annot1,annot2) -> alg.e_internal_exp_user (annot1,annot2)
   | E_comment c -> alg.e_comment c
   | E_comment_struc e -> alg.e_comment_struc (fold_exp alg e)
-  | E_internal_let (lexp,e1,e2) ->
+  | E_var (lexp,e1,e2) ->
      alg.e_internal_let (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
   | E_internal_plet (pat,e1,e2) ->
      alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2)
@@ -652,7 +652,7 @@ let id_exp_alg =
   ; e_internal_exp_user = (fun (a1,a2) -> E_internal_exp_user (a1,a2))
   ; e_comment = (fun c -> E_comment c)
   ; e_comment_struc = (fun e -> E_comment_struc e)
-  ; e_internal_let = (fun (lexp, e2, e3) -> E_internal_let (lexp,e2,e3))
+  ; e_internal_let = (fun (lexp, e2, e3) -> E_var (lexp,e2,e3))
   ; e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat,e1,e2))
   ; e_internal_return = (fun e -> E_internal_return e)
   ; e_internal_value = (fun v -> E_internal_value v)
@@ -753,7 +753,7 @@ let compute_exp_alg bot join =
   ; e_comment = (fun c -> (bot, E_comment c))
   ; e_comment_struc = (fun (v,e) -> (bot, E_comment_struc e)) (* ignore value by default, since it is comes from a comment *)
   ; e_internal_let = (fun ((vl, lexp), (v2,e2), (v3,e3)) ->
-    (join_list [vl;v2;v3], E_internal_let (lexp,e2,e3)))
+    (join_list [vl;v2;v3], E_var (lexp,e2,e3)))
   ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) ->
     (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2)))
   ; e_internal_return = (fun (v,e) -> (v, E_internal_return e))
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e96dd17f..25953776 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -362,7 +362,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_internal_exp_user = (fun (a1,a2) -> (E_internal_exp_user (a1,a2), E_internal_exp_user (a1,a2)))
     ; e_comment = (fun c -> (E_comment c, E_comment c))
     ; e_comment_struc = (fun (e,e') -> (E_comment_struc e, E_comment_struc e'))
-    ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3')))
+    ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_var (lexp,e2,e3), E_var (lexp',e2',e3')))
     ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
     ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
     ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
@@ -1438,7 +1438,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
         let exps' = walker exps in
         let effects = union_eff_exps exps' in
         let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in
-        [fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))]
+        [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
       (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps ->
         let vars_t = introduced_variables t in
         let vars_e = introduced_variables e in
@@ -1475,7 +1475,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
                            (Parse_ast.Generated l, simple_annot t))
                   | _ -> e in
                 let unioneffs = union_effects effects (get_effsum_exp set_exp) in
-                ([E_aux (E_internal_let (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Generated l)),
+                ([E_aux (E_var (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Generated l)),
                                                   (Parse_ast.Generated l, (tag_annot t Emp_intro))),
                                         set_exp,
                                         E_aux (E_block res, (Parse_ast.Generated l, (simple_annot_efr unit_t effects)))),
@@ -1491,7 +1491,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     let e' = re' (rewrite_base e) in
     let block = annot_exp (E_block []) l (env_of full_exp) unit_typ in
     check_exp (env_of full_exp)
-      (strip_exp (E_aux (E_internal_let(le', e', block), annot))) (typ_of full_exp)
+      (strip_exp (E_aux (E_var(le', e', block), annot))) (typ_of full_exp)
   | _ -> rewrite_base full_exp
 
 let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) =
@@ -1622,8 +1622,8 @@ let rewrite_register_ref_writes (Defs defs) =
                        (fun (Pat_aux (Pat_exp(p,e),pannot)) -> 
                           Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite_rec e),pannot)) pexps)))
   | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite_rec body))
-  | E_internal_let (lexp,exp,body) ->
-    rewrap (E_internal_let (rewriters.rewrite_lexp rewriters nmap lexp, rewrite_rec exp, rewrite_rec body))
+  | E_var (lexp,exp,body) ->
+    rewrap (E_var (rewriters.rewrite_lexp rewriters nmap lexp, rewrite_rec exp, rewrite_rec body))
   | _ -> rewrite_base full_exp
 
 let rewrite_defs_separate_numbs defs = rewrite_defs_base
@@ -2377,10 +2377,10 @@ let rewrite_defs_letbind_effects  =
        k (rewrap (E_internal_cast (annot',exp'))))
     | E_internal_exp _ -> k exp
     | E_internal_exp_user _ -> k exp
-    | E_internal_let (lexp,exp1,exp2) ->
+    | E_var (lexp,exp1,exp2) ->
        n_lexp lexp (fun lexp ->
        n_exp exp1 (fun exp1 ->
-       rewrap (E_internal_let (lexp,exp1,n_exp exp2 k))))
+       rewrap (E_var (lexp,exp1,n_exp exp2 k))))
     | E_internal_return exp1 ->
        n_exp_name exp1 (fun exp1 ->
        k (rewrap (E_internal_return exp1)))
@@ -2457,7 +2457,7 @@ let rewrite_defs_internal_lets =
        (P_id id, annot)
     | LEXP_aux (LEXP_cast (typ, id), annot) ->
        (P_typ (typ, P_aux (P_id id, annot)), annot)
-    | _ -> failwith "E_internal_let with unexpected lexp" in
+    | _ -> failwith "E_var with unexpected lexp" in
     if effectful exp1 then
       E_internal_plet (P_aux (paux, annot), exp1, exp2)
     else
@@ -2565,9 +2565,9 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
     | E_let (lb,exp) ->
        let exp = add_vars overwrite exp vars in
        E_aux (E_let (lb,exp),swaptyp (typ_of exp) annot)
-    | E_internal_let (lexp,exp1,exp2) ->
+    | E_var (lexp,exp1,exp2) ->
        let exp2 = add_vars overwrite exp2 vars in
-       E_aux (E_internal_let (lexp,exp1,exp2), swaptyp (typ_of exp2) annot)
+       E_aux (E_var (lexp,exp1,exp2), swaptyp (typ_of exp2) annot)
     | E_internal_plet (pat,exp1,exp2) ->
        let exp2 = add_vars overwrite exp2 vars in
        E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (typ_of exp2) annot)
@@ -2761,8 +2761,8 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
           annot_letbind (pat, v) (get_loc_exp v) env (typ_of v)
        | Same_vars v -> LB_aux (LB_val (pat, v),lbannot) in
      propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
-  | E_internal_let (lexp,v,body) ->
-     (* Rewrite E_internal_let into E_let and call recursively *)
+  | E_var (lexp,v,body) ->
+     (* Rewrite E_var into E_let and call recursively *)
      let paux, typ = match lexp with
        | LEXP_aux (LEXP_id id, _) ->
           P_id id, typ_of v
@@ -2770,7 +2770,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
           P_typ (typ, annot_pat (P_id id) l env (typ_of v)), typ
        | _ ->
          raise (Reporting_basic.err_unreachable l
-           "E_internal_let with a lexp that is not a variable") in
+           "E_var with a lexp that is not a variable") in
      let lb = annot_letbind (paux, v) l env typ in
      let exp = propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body)) in
      rewrite_var_updates exp
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 81296027..b9affe12 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -342,7 +342,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
   | E_let(lebind,e) ->
     let b,u,s = fv_of_let consider_var bound used set lebind in
     fv_of_exp consider_var b u s e
-  | E_internal_let (lexp, exp1, exp2) ->
+  | E_var (lexp, exp1, exp2) ->
     let b,u,s = fv_of_lexp consider_var bound used set lexp in
     let _,used,set = fv_of_exp consider_var bound used set exp1 in
     fv_of_exp consider_var b used set exp2
diff --git a/src/type_check.ml b/src/type_check.ml
index 756efbfd..c2467cee 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2136,13 +2136,13 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_throw exp, _ ->
      let checked_exp = crule check_exp env exp exc_typ in
      annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
-  | E_internal_let (lexp, bind, exp), _ ->
+  | E_var (lexp, bind, exp), _ ->
      let lexp, bind, env = match bind_assignment env lexp bind with
        | E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env
        | _, _ -> assert false
      in
      let checked_exp = crule check_exp env exp typ in
-     annot_exp (E_internal_let (lexp, bind, checked_exp)) typ
+     annot_exp (E_var (lexp, bind, checked_exp)) typ
   | E_internal_return exp, _ ->
      let checked_exp = crule check_exp env exp typ in
      annot_exp (E_internal_return checked_exp) typ
@@ -3200,11 +3200,11 @@ and propagate_exp_effect_aux = function
      let p_lexp = propagate_lexp_effect lexp in
      let p_exp = propagate_exp_effect exp in
      E_assign (p_lexp, p_exp), union_effects (effect_of p_exp) (effect_of_lexp p_lexp)
-  | E_internal_let (lexp, bind, exp) ->
+  | E_var (lexp, bind, exp) ->
      let p_lexp = propagate_lexp_effect lexp in
      let p_bind = propagate_exp_effect bind in
      let p_exp = propagate_exp_effect exp in
-     E_internal_let (p_lexp, p_bind, p_exp), union_effects (effect_of_lexp p_lexp) (collect_effects [p_bind; p_exp])
+     E_var (p_lexp, p_bind, p_exp), union_effects (effect_of_lexp p_lexp) (collect_effects [p_bind; p_exp])
   | E_sizeof nexp -> E_sizeof nexp, no_effect
   | E_constraint nc -> E_constraint nc, no_effect
   | E_exit exp ->