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.

1 files changed, 39 insertions, 86 deletions

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