Simplify AST by removing LB_val_explicit and replace LB_val_implicit with just LB_val in AST

also rename functions in rewriter.ml appropriately.

16 files changed, 72 insertions, 169 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 930af68f..bf9b11aa 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -374,8 +374,7 @@ and 'a pexp =
    Pat_aux of 'a pexp_aux * 'a annot
 
 and 'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+   LB_val of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
 
 and 'a letbind =
    LB_aux of 'a letbind_aux * 'a annot
diff --git a/src/ast_util.ml b/src/ast_util.ml
index a39e570b..c57f2a12 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -85,7 +85,7 @@ let mk_fundef funcls =
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
 
-let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot)
+let mk_letbind pat exp = LB_aux (LB_val (pat, exp), no_annot)
 
 let mk_val_spec vs_aux =
   DEF_spec (VS_aux (vs_aux, no_annot))
@@ -280,8 +280,7 @@ and map_pat_annot_aux f = function
 and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
 and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
 and map_letbind_annot_aux f = function
-  | LB_val_explicit (typschm, pat, exp) -> LB_val_explicit (typschm, map_pat_annot f pat, map_exp_annot f exp)
-  | LB_val_implicit (pat, exp) -> LB_val_implicit (map_pat_annot f pat, map_exp_annot f exp)
+  | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp)
 and map_lexp_annot f (LEXP_aux (lexp, annot)) = LEXP_aux (map_lexp_annot_aux f lexp, f annot)
 and map_lexp_annot_aux f = function
   | LEXP_id id -> LEXP_id id
@@ -526,9 +525,7 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
   | _ -> "LEXP"
 and string_of_letbind (LB_aux (lb, l)) =
   match lb with
-  | LB_val_implicit (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
-  | LB_val_explicit (typschm, pat, exp) ->
-     string_of_typschm typschm ^ " " ^ string_of_pat pat ^ " = " ^ string_of_exp exp
+  | LB_val (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
 
 let rec string_of_index_range (BF_aux (ir, _)) =
   match ir with
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 7b618867..89da69e0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -439,11 +439,8 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
 let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : unit letbind =
   LB_aux(
     (match lb with
-    | Parse_ast.LB_val_explicit(typschm,pat,exp) ->
-      let typsch, k_env, _  = to_ast_typschm k_env def_ord typschm in
-      LB_val_explicit(typsch,to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
-    | Parse_ast.LB_val_implicit(pat,exp) ->
-      LB_val_implicit(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
+    | Parse_ast.LB_val(pat,exp) ->
+      LB_val(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
     ), (l,()))
 
 and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit exp = 
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index e97632ec..e419370e 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -363,9 +363,7 @@ let nexp_subst_fns substs refinements =
          Pat_aux (Pat_when ((*s_pat*) p, s_exp e1, s_exp e2),(l,(*s_tannot*) annot))
     and s_letbind (LB_aux (lb,(l,annot))) =
       match lb with
-      | LB_val_explicit (tysch,p,e) ->
-         LB_aux (LB_val_explicit ((*s_typschm*) tysch,(*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
-      | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
+      | LB_val (p,e) -> LB_aux (LB_val ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
     and s_lexp (LEXP_aux (e,(l,annot))) =
       let re e = LEXP_aux (e,(l,(*s_tannot*) annot)) in
       match e with
@@ -460,8 +458,7 @@ and deexist_pexp (Pat_aux (pe,(l,annot))) =
   | Pat_when (p,e1,e2) -> Pat_aux (Pat_when ((*Type_check.strip_pat*) p,deexist_exp e1,deexist_exp e2),(l,annot))
 and deexist_letbind (LB_aux (lb,(l,annot))) =
   match lb with (* TODO, drop tysc if there's an exist? Do they even appear here? *)
-  | LB_val_explicit (tysc,p,e) -> LB_aux (LB_val_explicit (tysc,(*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
-  | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
+  | LB_val (p,e) -> LB_aux (LB_val ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
 and deexist_lexp (LEXP_aux (le,(l,annot))) =
   let re le = LEXP_aux (le,(l,annot)) in
   match le with
@@ -759,11 +756,8 @@ let split_defs splits defs =
        Pat_aux (Pat_when (p, const_prop_exp substs' e1, const_prop_exp substs' e2),l)
   and const_prop_letbind substs (LB_aux (lb,annot)) =
     match lb with
-    | LB_val_explicit (tysch,p,e) ->
-       (LB_aux (LB_val_explicit (tysch,p,const_prop_exp substs e), annot),
-        remove_bound substs p)
-    | LB_val_implicit (p,e) ->
-       (LB_aux (LB_val_implicit (p,const_prop_exp substs e), annot),
+    | LB_val (p,e) ->
+       (LB_aux (LB_val (p,const_prop_exp substs e), annot),
         remove_bound substs p)
   and const_prop_lexp substs ((LEXP_aux (e,annot)) as le) =
     let re e = LEXP_aux (e,annot) in
@@ -817,7 +811,7 @@ let split_defs splits defs =
       let lg = Generated l in
       let id = match subi with Id_aux (i,l) -> Id_aux (i,lg) in
       let p = P_aux (P_id id, subannot) in
-      E_aux (E_let (LB_aux (LB_val_implicit (p,sube),(lg,annot)), exp),(lg,annot))
+      E_aux (E_let (LB_aux (LB_val (p,sube),(lg,annot)), exp),(lg,annot))
     else 
       let substs = isubst_from_list [subst] in
       let () = nexp_substs := [] in
@@ -1090,8 +1084,7 @@ let split_defs splits defs =
             ) patnsubsts)
     and map_letbind (LB_aux (lb,annot)) =
       match lb with
-      | LB_val_explicit (tysch,p,e) -> LB_aux (LB_val_explicit (tysch,check_single_pat p,map_exp e), annot)
-      | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit (check_single_pat p,map_exp e), annot)
+      | LB_val (p,e) -> LB_aux (LB_val (check_single_pat p,map_exp e), annot)
     and map_lexp ((LEXP_aux (e,annot)) as le) =
       let re e = LEXP_aux (e,annot) in
       match e with
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 2509f8ef..301d53fb 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -141,7 +141,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
 and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
   match lb_aux with
-  | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
+  | LB_val (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
   | _ -> failwith "Ocaml: Explicit letbind found"
 and ocaml_pexps ctx = function
   | [pexp] -> ocaml_pexp ctx pexp
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 1036fab8..cd5edce6 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -318,8 +318,7 @@ and pexp =
    Pat_aux of pexp_aux * l
 
 and letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+   LB_val of pat * exp (* value binding, implicit type (pat must be total) *)
 
 and letbind = 
    LB_aux of letbind_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index c756cf74..70a6d132 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -999,12 +999,7 @@ patsexp:
 
 letbind:
   | Let_ atomic_pat Eq exp
-    { lbloc (LB_val_implicit($2,$4)) }
-  | Let_ typquant atomic_typ atomic_pat Eq exp
-    { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
-/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this
-  | Let_ Lparen typ Rparen atomic_pat Eq exp 
-    { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */
+    { lbloc (LB_val($2,$4)) }
 
 funcl:
   | id atomic_pat Eq exp
diff --git a/src/parser2.mly b/src/parser2.mly
index 02a8f09c..7ee98f41 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -836,7 +836,7 @@ block:
 
 %inline letbind:
   | pat Eq exp
-    { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
+    { LB_aux (LB_val ($1, $3), loc $startpos $endpos) }
 
 atomic_exp:
   | atomic_exp Colon atomic_typ
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a247b973..7f04c495 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -948,8 +948,7 @@ let doc_exp_lem, doc_let_lem =
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
   and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with
-    | LB_val_explicit(_,pat,e)
-      | LB_val_implicit(pat,e) ->
+    | LB_val(pat,e) ->
        prefix 2 1
               (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
               (top_exp sequential mwords early_ret false e)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 48ec37b8..f0f25795 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -349,10 +349,8 @@ let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
 let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
   let print_lb ppf lb =
     match lb with
-      | LB_val_explicit(ts,pat,exp) ->
-        fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
-      | LB_val_implicit(pat,exp) ->
-        fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp in
+      | LB_val(pat,exp) ->
+        fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val" pp_lem_pat pat  pp_lem_exp exp in
   fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
 
 and pp_lem_exp ppf (E_aux(e,(l,annot))) =
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index d94879ee..0b7ca48f 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -439,11 +439,7 @@ let doc_exp_ocaml, doc_let_ocaml =
       "internal expression should have been rewritten before pretty-printing")
   | E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *)
   and let_exp (LB_aux(lb,_)) = match lb with
-  | LB_val_explicit(ts,pat,e) ->
-      prefix 2 1
-        (separate space [string "let"; doc_pat_ocaml pat; equals])
-        (top_exp false e)
-  | LB_val_implicit(pat,e) ->
+  | LB_val(pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_pat_ocaml pat; equals])
         (top_exp false e)
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8101d45f..546f229f 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -341,17 +341,7 @@ let doc_exp, doc_let =
       separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2]
   | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr)
   and let_exp (LB_aux(lb,_)) = match lb with
-    | LB_val_explicit(ts,pat,e) ->
-      (match ts with
-       | TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_no_forall,_),_),_) ->
-         prefix 2 1
-           (separate space [string "let"; parens (doc_typscm_atomic ts); doc_atomic_pat pat; equals])
-           (atomic_exp e)
-       | _ ->
-         prefix 2 1
-           (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
-           (atomic_exp e))
-  | LB_val_implicit(pat,e) ->
+  | LB_val(pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_atomic_pat pat; equals])
         (atomic_exp e)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index ad4b88c4..2f743e45 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -212,8 +212,7 @@ let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
 let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
 | Some (env, typ, eff) ->
   let effsum = match lb with
-    | LB_val_explicit (_,_,e) -> effect_of e
-    | LB_val_implicit (_,e) -> effect_of e in
+    | LB_val (_,e) -> effect_of e in
   LB_aux (lb, (l, Some (env, typ, effsum)))
 | None ->
   LB_aux (lb, (l, None))
@@ -533,11 +532,8 @@ let rewrite_let rewriters (LB_aux(letbind,(l,annot))) =
       | None -> Some(m,s) (*Shouldn't happen*)
       | Some new_m -> Some(new_m,s) in*)
   match letbind with
-  | LB_val_explicit (typschm, pat,exp) ->
-    LB_aux(LB_val_explicit (typschm,rewriters.rewrite_pat rewriters pat,
-                            rewriters.rewrite_exp rewriters exp),(l,annot))
-  | LB_val_implicit ( pat, exp) ->
-    LB_aux(LB_val_implicit (rewriters.rewrite_pat rewriters pat,
+  | LB_val ( pat, exp) ->
+    LB_aux(LB_val (rewriters.rewrite_pat rewriters pat,
                             rewriters.rewrite_exp rewriters exp),(l,annot))
 
 let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
@@ -732,8 +728,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; pat_exp                  : 'pat * 'exp -> 'pexp_aux
   ; pat_when                 : 'pat * 'exp * 'exp -> 'pexp_aux
   ; pat_aux                  : 'pexp_aux * 'a annot -> 'pexp
-  ; lB_val_explicit          : typschm * 'pat * 'exp -> 'letbind_aux
-  ; lB_val_implicit          : 'pat * 'exp -> 'letbind_aux
+  ; lB_val          : 'pat * 'exp -> 'letbind_aux
   ; lB_aux                   : 'letbind_aux * 'a annot -> 'letbind
   ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
   }
@@ -810,8 +805,7 @@ and fold_pexp_aux alg = function
   | Pat_when (pat,e,e') -> alg.pat_when (fold_pat alg.pat_alg pat, fold_exp alg e, fold_exp alg e')
 and fold_pexp alg (Pat_aux (pexp_aux,annot)) = alg.pat_aux (fold_pexp_aux alg pexp_aux, annot)
 and fold_letbind_aux alg = function
-  | LB_val_explicit (t,pat,e) -> alg.lB_val_explicit (t,fold_pat alg.pat_alg pat, fold_exp alg e)
-  | LB_val_implicit (pat,e) -> alg.lB_val_implicit (fold_pat alg.pat_alg pat, fold_exp alg e)
+  | LB_val (pat,e) -> alg.lB_val (fold_pat alg.pat_alg pat, fold_exp alg e)
 and fold_letbind alg (LB_aux (letbind_aux,annot)) = alg.lB_aux (fold_letbind_aux alg letbind_aux, annot)
 
 let id_exp_alg =
@@ -871,8 +865,7 @@ let id_exp_alg =
   ; pat_exp = (fun (pat,e) -> (Pat_exp (pat,e)))
   ; pat_when = (fun (pat,e,e') -> (Pat_when (pat,e,e')))
   ; pat_aux = (fun (pexp,a) -> (Pat_aux (pexp,a)))
-  ; lB_val_explicit = (fun (typ,pat,e) -> LB_val_explicit (typ,pat,e))
-  ; lB_val_implicit = (fun (pat,e) -> LB_val_implicit (pat,e))
+  ; lB_val = (fun (pat,e) -> LB_val (pat,e))
   ; lB_aux = (fun (lb,annot) -> LB_aux (lb,annot))
   ; pat_alg = id_pat_alg
   }
@@ -972,8 +965,7 @@ let compute_exp_alg bot join =
   ; pat_exp = (fun ((vp,pat),(v,e)) -> (join vp v, Pat_exp (pat,e)))
   ; pat_when = (fun ((vp,pat),(v,e),(v',e')) -> (join_list [vp;v;v'], Pat_when (pat,e,e')))
   ; pat_aux = (fun ((v,pexp),a) -> (v, Pat_aux (pexp,a)))
-  ; lB_val_explicit = (fun (typ,(vp,pat),(v,e)) -> (join vp v, LB_val_explicit (typ,pat,e)))
-  ; lB_val_implicit = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val_implicit (pat,e)))
+  ; lB_val = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val (pat,e)))
   ; lB_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot)))
   ; pat_alg = compute_pat_alg bot join
   }
@@ -1199,8 +1191,7 @@ let rewrite_sizeof (Defs defs) =
     ; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e')))
     ; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2')))
     ; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a)))
-    ; lB_val_explicit = (fun (typ,pat,(e,e')) -> (LB_val_explicit (typ,pat,e), LB_val_explicit (typ,pat,e')))
-    ; lB_val_implicit = (fun (pat,(e,e')) -> (LB_val_implicit (pat,e), LB_val_implicit (pat,e')))
+    ; lB_val = (fun (pat,(e,e')) -> (LB_val (pat,e), LB_val (pat,e')))
     ; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot)))
     ; pat_alg = id_pat_alg
     } in
@@ -1272,12 +1263,9 @@ let rewrite_sizeof (Defs defs) =
     | DEF_val (LB_aux (lb, annot)) ->
        begin
          let lb' = match lb with
-         | LB_val_explicit (typschm, pat, exp) ->
-           let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
-           LB_val_explicit (typschm, pat, exp')
-         | LB_val_implicit (pat, exp) ->
+         | LB_val (pat, exp) ->
            let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
-           LB_val_implicit (pat, exp') in
+           LB_val (pat, exp') in
          (params_map, defs @ [DEF_val (LB_aux (lb', annot))])
        end
     | def ->
@@ -1425,7 +1413,7 @@ let remove_vector_concat_pat pat =
         match typ_opt with
         | Some typ -> P_aux (P_typ (typ, P_aux (P_id child,cannot)), cannot)
         | None -> P_aux (P_id child,cannot) in
-      let letbind = fix_eff_lb (LB_aux (LB_val_implicit (id_pat,subv),cannot)) in
+      let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
       (letbind,
        (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))),
        (rootname,childname)) in
@@ -1608,13 +1596,9 @@ let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp,(l,annot)) as ful
        let (pat,_,decls) = remove_vector_concat_pat pat in
        Pat_aux (Pat_when (pat, decls (rewrite_rec guard), decls (rewrite_rec body)),annot') in
      rewrap (E_case (rewrite_rec e, List.map aux ps))
-  | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) ->
+  | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
      let (pat,_,decls) = remove_vector_concat_pat pat in
-     rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'),
-                    decls (rewrite_rec body)))
-  | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) ->
-     let (pat,_,decls) = remove_vector_concat_pat pat in
-     rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'),
+     rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'),
                     decls (rewrite_rec body)))
   | exp -> rewrite_base full_exp
 
@@ -1638,14 +1622,10 @@ let rewrite_defs_remove_vector_concat (Defs defs) =
   let rewrite_def d =
     let d = rewriters.rewrite_def rewriters d in
     match d with
-    | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) ->
+    | DEF_val (LB_aux (LB_val (pat,exp),a)) ->
        let (pat,letbinds,_) = remove_vector_concat_pat pat in
        let defvals = List.map (fun lb -> DEF_val lb) letbinds in
-       [DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a))] @ defvals
-    | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) -> 
-       let (pat,letbinds,_) = remove_vector_concat_pat pat in
-       let defvals = List.map (fun lb -> DEF_val lb) letbinds in
-       [DEF_val (LB_aux (LB_val_implicit (pat,exp),a))] @ defvals
+       [DEF_val (LB_aux (LB_val (pat,exp),a))] @ defvals
     | d -> [d] in
   Defs (List.flatten (List.map rewrite_def defs))
 
@@ -1918,7 +1898,7 @@ let remove_bitvector_pat pat =
     let rannot = simple_annot l typ in
     let elem = access_bit_exp (rootid,rannot) l idx in
     let e = P_aux (P_id id, simple_annot l bit_typ) in
-    let letbind = LB_aux (LB_val_implicit (e,elem), simple_annot l bit_typ) in
+    let letbind = LB_aux (LB_val (e,elem), simple_annot l bit_typ) in
     let letexp = (fun body ->
       let (E_aux (_,(_,bannot))) = body in
       E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in
@@ -2049,13 +2029,9 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
        | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp guard guard', body'), annot')
        | None -> Pat_aux (Pat_when (pat', guard, body'), annot')) in
     rewrap (E_case (e, List.map rewrite_pexp ps))
-  | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) ->
-     let (pat,(_,decls,_)) = remove_bitvector_pat pat in
-     rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'),
-                    decls (rewrite_rec body)))
-  | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) ->
+  | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
      let (pat,(_,decls,_)) = remove_bitvector_pat pat in
-     rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'),
+     rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'),
                     decls (rewrite_rec body)))
   | _ -> rewrite_base full_exp
 
@@ -2086,14 +2062,10 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
   let rewrite_def d =
     let d = rewriters.rewrite_def rewriters d in
     match d with
-    | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) ->
+    | DEF_val (LB_aux (LB_val (pat,exp),a)) ->
        let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in
        let defvals = List.map (fun lb -> DEF_val lb) letbinds in
-       [DEF_val (LB_aux (LB_val_explicit (t,pat',exp),a))] @ defvals
-    | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) ->
-       let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in
-       let defvals = List.map (fun lb -> DEF_val lb) letbinds in
-       [DEF_val (LB_aux (LB_val_implicit (pat',exp),a))] @ defvals
+       [DEF_val (LB_aux (LB_val (pat',exp),a))] @ defvals
     | d -> [d] in
   (* FIXME See above in rewrite_sizeof *)
   (* fst (check initial_env ( *)
@@ -2124,7 +2096,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
       let (E_aux (_,(el,eannot))) = e in
       let pat_e' = fresh_id_pat "p__" (el, Some (env_of e, typ_of e, no_effect)) in
       let exp_e' = pat_to_exp pat_e' in
-      let letbind_e = LB_aux (LB_val_implicit (pat_e',e), (el,eannot)) in
+      let letbind_e = LB_aux (LB_val (pat_e',e), (el,eannot)) in
       let exp' = case_exp exp_e' (typ_of full_exp) clauses in
       rewrap (E_let (letbind_e, exp'))
     else case_exp e (typ_of full_exp) clauses
@@ -2599,7 +2571,7 @@ let rewrite_defs_remove_blocks =
     let annot_pat = (simple_annot l (typ_of v)) in
     let annot_lb = (Parse_ast.Generated l, tannot) in
     let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
-    E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
+    E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
 
   let rec f l = function
     | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ))
@@ -2636,7 +2608,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
      let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
      let pat = P_aux (P_wild,annot_pat) in
      
-     E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
+     E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
   | Some (env, typ, eff) ->
      let id = fresh_id "w__" l in
      let annot_pat = simple_annot l (typ_of v) in
@@ -2647,7 +2619,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
      let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
      let pat = P_aux (P_id id,annot_pat) in
      
-     E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
+     E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
   | None ->
      raise (Reporting_basic.err_unreachable l "no type information")
 
@@ -2711,12 +2683,9 @@ let rewrite_defs_letbind_effects  =
   and n_lb (lb : 'a letbind) (k : 'a letbind -> 'a exp) : 'a exp =
     let (LB_aux (lb,annot)) = lb in
     match lb with
-    | LB_val_explicit (typ,pat,exp1) ->
-       n_exp exp1 (fun exp1 -> 
-       k (fix_eff_lb (LB_aux (LB_val_explicit (typ,pat,exp1),annot))))
-    | LB_val_implicit (pat,exp1) ->
+    | LB_val (pat,exp1) ->
        n_exp exp1 (fun exp1 -> 
-       k (fix_eff_lb (LB_aux (LB_val_implicit (pat,exp1),annot))))
+       k (fix_eff_lb (LB_aux (LB_val (pat,exp1),annot))))
 
   and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp =
     let (LEXP_aux (lexp_aux,annot)) = lexp in
@@ -2901,10 +2870,8 @@ let rewrite_defs_letbind_effects  =
       let rewrap lb = DEF_val (LB_aux (lb, annot)) in
       begin
         match lb with
-        | LB_val_implicit (pat, exp) ->
-          rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp))
-        | LB_val_explicit (ts, pat, exp) ->
-          rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp))
+        | LB_val (pat, exp) ->
+          rewrap (LB_val (pat, n_exp_term (effectful exp) exp))
       end
     | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef)
     | d -> d in
@@ -2928,13 +2895,12 @@ let rewrite_defs_effectful_let_expressions =
 
   let e_let (lb,body) =
     match lb with
-    | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
+    | LB_aux (LB_val (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
       when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) ->
       (* Rewrite assignments to local variables into let bindings *)
       let (lhs, rhs) = rewrite_local_lexp le in
-      E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
-    | LB_aux (LB_val_explicit (_,pat,exp'),annot')
-    | LB_aux (LB_val_implicit (pat,exp'),annot') ->
+      E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs exp), annot), body)
+    | LB_aux (LB_val (pat,exp'),annot') ->
        if effectful exp'
        then E_internal_plet (pat,exp',body)
        else E_let (lb,body) in
@@ -2946,7 +2912,7 @@ let rewrite_defs_effectful_let_expressions =
        if effectful exp1 then
          E_internal_plet (P_aux (P_id id,annot),exp1,exp2)
        else
-         let lb = LB_aux (LB_val_implicit (P_aux (P_id id,annot), exp1), annot) in
+         let lb = LB_aux (LB_val (P_aux (P_id id,annot), exp1), annot) in
          E_let (lb, exp2)
     | _ -> failwith "E_internal_let with unexpected lexp" in
 
@@ -3206,20 +3172,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
   | E_let (lb,body) ->
      let body = rewrite_var_updates body in
      let (eff,lb) = match lb with
-       | LB_aux (LB_val_implicit (pat,v),lbannot) ->
+       | LB_aux (LB_val (pat,v),lbannot) ->
           (match rewrite v pat with
            | Added_vars (v,pat) ->
               let (E_aux (_,(l,_))) = v in
               let lbannot = (simple_annot l (typ_of v)) in
-              (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
-           | Same_vars v -> (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot)))
-       | LB_aux (LB_val_explicit (typ,pat,v),lbannot) ->
-          (match rewrite v pat with 
-           | Added_vars (v,pat) ->
-              let (E_aux (_,(l,_))) = v in
-              let lbannot = (simple_annot l (typ_of v)) in
-              (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
-           | Same_vars v -> (effect_of v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in
+              (effect_of v,LB_aux (LB_val (pat,v),lbannot))
+           | Same_vars v -> (effect_of v,LB_aux (LB_val (pat,v),lbannot))) in
      let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in
      E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot))
   | E_internal_let (lexp,v,body) ->
@@ -3235,7 +3194,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
      let bodyeff = effect_of body in
      let pat = P_aux (P_id id, (simple_annot l vtyp)) in
      let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in
-     let lb = LB_aux (LB_val_implicit (pat,v),lbannot) in
+     let lb = LB_aux (LB_val (pat,v),lbannot) in
      let exp = E_aux (E_let (lb,body),(Parse_ast.Generated l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
      rewrite_var_updates exp
   | E_internal_plet (pat,v,body) ->
@@ -3290,21 +3249,15 @@ let rewrite_defs_remove_superfluous_letbinds =
     | E_let (lb,exp2) ->
        begin match lb,exp2 with
        (* 'let x = EXP1 in x' can be replaced with 'EXP1' *)
-       | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
-         E_aux (E_id (Id_aux (id',_)),_)
-       | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
-         E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_)
-       | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+       | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
          E_aux (E_id (Id_aux (id',_)),_)
-       | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+       | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
          E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_)
             when id = id' ->
           exp1
        (* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at
           least when EXP1 is 'small' enough *)
-       | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
-         E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
-       | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+       | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
          E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
             when id = id' && small exp1 ->
           let (E_aux (_,e1annot)) = exp1 in
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 645ecbf4..32974bd0 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -142,8 +142,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; pat_exp                  : 'pat * 'exp -> 'pexp_aux
  ; pat_when                 : 'pat * 'exp * 'exp -> 'pexp_aux
  ; pat_aux                  : 'pexp_aux * 'a annot -> 'pexp
- ; lB_val_explicit          : typschm * 'pat * 'exp -> 'letbind_aux
- ; lB_val_implicit          : 'pat * 'exp -> 'letbind_aux
+ ; lB_val          : 'pat * 'exp -> 'letbind_aux
  ; lB_aux                   : 'letbind_aux * 'a annot -> 'letbind
  ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
  }
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index e04b7d33..3f3df45a 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -358,12 +358,7 @@ and fv_of_pes consider_var bound used set pes =
     fv_of_pes consider_var bound us_e set_e pes
     
 and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
-  | LB_val_explicit(typsch,pat,exp) ->
-    let bound_t,us_t = fv_of_typschm consider_var bound used typsch in
-    let bound_p, us_p = pat_bindings consider_var (Nameset.union bound bound_t) used pat in
-    let _,us_e,set_e = fv_of_exp consider_var (Nameset.union bound bound_t) used set exp in
-    (Nameset.union bound_t bound_p),Nameset.union us_t (Nameset.union us_p us_e),set_e
-  | LB_val_implicit(pat,exp) ->
+  | LB_val(pat,exp) ->
     let bound_p, us_p = pat_bindings consider_var bound used pat in
     let _,us_e,set_e = fv_of_exp consider_var bound used set exp in
     bound_p,Nameset.union us_p us_e,set_e
diff --git a/src/type_check.ml b/src/type_check.ml
index 5813b081..bfd336d9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1946,15 +1946,14 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
-       | LB_val_explicit (typschm, pat, bind) -> assert false
-       | LB_val_implicit (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
+       | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
           let checked_bind = crule check_exp env bind ptyp in
           let tpat, env = bind_pat env pat ptyp in
-          annot_exp (E_let (LB_aux (LB_val_implicit (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
-       | LB_val_implicit (pat, bind) ->
+          annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+       | LB_val (pat, bind) ->
           let inferred_bind = irule infer_exp env bind in
           let tpat, env = bind_pat env pat (typ_of inferred_bind) in
-          annot_exp (E_let (LB_aux (LB_val_implicit (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+          annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
      end
   | E_app_infix (x, op, y), _ when List.length (Env.get_overloads (deinfix op) env) > 0 ->
      check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
@@ -2965,15 +2964,10 @@ and propagate_letbind_effect (LB_aux (lb, (l, annot))) =
   | Some (typq, typ, eff) -> LB_aux (p_lb, (l, Some (typq, typ, eff))), eff
   | None -> LB_aux (p_lb, (l, None)), eff
 and propagate_letbind_effect_aux = function
-  | LB_val_explicit (typschm, pat, exp) ->
+  | LB_val (pat, exp) ->
      let p_pat = propagate_pat_effect pat in
      let p_exp = propagate_exp_effect exp in
-     LB_val_explicit (typschm, p_pat, p_exp),
-     union_effects (effect_of_pat p_pat) (effect_of p_exp)
-  | LB_val_implicit (pat, exp) ->
-     let p_pat = propagate_pat_effect pat in
-     let p_exp = propagate_exp_effect exp in
-     LB_val_implicit (p_pat, p_exp),
+     LB_val (p_pat, p_exp),
      union_effects (effect_of_pat p_pat) (effect_of p_exp)
 
 and propagate_lexp_effect (LEXP_aux (lexp, annot)) =
@@ -3010,15 +3004,14 @@ and propagate_lexp_effect_aux = function
 let check_letdef env (LB_aux (letbind, (l, _))) =
   begin
     match letbind with
-    | LB_val_explicit (typschm, pat, bind) -> assert false
-    | LB_val_implicit (P_aux (P_typ (typ_annot, pat), _), bind) ->
+    | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) ->
        let checked_bind = crule check_exp env (strip_exp bind) typ_annot in
        let tpat, env = bind_pat env (strip_pat pat) typ_annot in
-       [DEF_val (LB_aux (LB_val_implicit (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env
-    | LB_val_implicit (pat, bind) ->
+       [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+    | LB_val (pat, bind) ->
        let inferred_bind = irule infer_exp env (strip_exp bind) in
        let tpat, env = bind_pat env (strip_pat pat) (typ_of inferred_bind) in
-       [DEF_val (LB_aux (LB_val_implicit (tpat, inferred_bind), (l, None)))], env
+       [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
   end
 
 let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ =