Merge remote-tracking branch 'origin/sail_new_tc' into experiments

3 files changed, 46 insertions, 59 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 5dbdb157..f148c1ff 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -69,7 +69,7 @@ let bitwise_not_bit = function
   | BU -> BU
   end
 
-let inline (~) = bitwise_not_bit
+(* let inline (~) = bitwise_not_bit *)
 
 val is_one : integer -> bitU
 let is_one i =
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7adccfdf..2619cc51 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -135,6 +135,11 @@ let effectful (Effect_aux (eff,_)) =
   | Effect_var _ -> failwith "effectful: Effect_var not supported"
   | Effect_set effs -> effectful_set effs
 
+let is_regtyp (Typ_aux (typ, _)) env = match typ with
+  | Typ_app(id, _) when string_of_id id = "register" -> true
+  | Typ_id(id) when Env.is_regtyp id env -> true
+  | _ -> false
+
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
   let rec typ regtypes ty = fn_typ regtypes true ty
@@ -463,39 +468,21 @@ let doc_exp_lem, doc_let_lem =
        | _ ->
           begin match annot with
           | Some (env, _, _) when (is_ctor env f) ->
-             let argpp a_needed arg =
-               let t = typ_of arg in
-               if is_vector_typ t then
-                 let call =
-                   if is_bitvector_typ t then "reset_bitvector_start"
-                   else "reset_vector_start" in
-                 let epp = concat [string call;space;expY arg] in
-                 if a_needed then parens epp else epp
-               else expV a_needed arg in
              let epp =
                match args with
                | [] -> doc_id_lem_ctor f
-               | [arg] -> doc_id_lem_ctor f ^^ space ^^ argpp true arg
+               | [arg] -> doc_id_lem_ctor f ^^ space ^^ expV true arg
                | _ ->
                   doc_id_lem_ctor f ^^ space ^^ 
-                    parens (separate_map comma (argpp false) args) in
+                    parens (separate_map comma (expV false) args) in
              if aexp_needed then parens (align epp) else epp
           | _ ->
              let call = (*match annot with
                | Base(_,External (Some n),_,_,_,_) -> string n
                | _ ->*) doc_id_lem f in
-             let argpp a_needed arg =
-               let t = typ_of arg in
-               if is_vector_typ t then
-                 let call =
-                   if is_bitvector_typ t then "reset_bitvector_start"
-                   else "reset_vector_start" in
-                 let epp = concat [string call;space;expY arg] in
-                 if a_needed then parens epp else epp
-               else expV a_needed arg in
              let argspp = match args with
-               | [arg] -> argpp true arg
-               | args -> parens (align (separate_map (comma ^^ break 0) (argpp false) args)) in
+               | [arg] -> expV true arg
+               | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in
              let epp = align (call ^//^ argspp) in
              let (taepp,aexp_needed) =
                let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -536,15 +523,16 @@ let doc_exp_lem, doc_let_lem =
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let ft = typ_of_annot (l,fannot) in
        (match fannot with
-        | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_regtyp tid env ->
+        | Some(env, ftyp, _) when is_regtyp ftyp env ->
            let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+           let eff = effect_of full_exp in
            let field_f = string
              (if is_bit_typ t
              then "read_reg_bitfield"
              else "read_reg_field") in
            let (ta,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then (doc_tannot_lem regtypes true t, true)
+             then (doc_tannot_lem regtypes (effectful eff) t, true)
              else (empty, aexp_needed) in
            let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in
            if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
@@ -560,17 +548,17 @@ let doc_exp_lem, doc_let_lem =
     | E_block exps -> raise (report l "Blocks should have been removed till now.")
     | E_nondet exps -> raise (report l "Nondet blocks not supported.")
     | E_id id ->
-       let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
-       (match annot with
-        | Some (env, Typ_aux (Typ_id tid, _), eff) when Env.is_regtyp tid env ->
-           if has_effect eff BE_rreg then
-             let epp = separate space [string "read_reg";doc_id_lem id] in
-             if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then parens (epp ^^ doc_tannot_lem regtypes true t)
-             else epp
-           else
-             doc_id_lem id
-        | Some (env, _, _) when (is_ctor env id) -> doc_id_lem_ctor id
+       let env = env_of full_exp in
+       let typ = typ_of full_exp in
+       let eff = effect_of full_exp in
+       let base_typ = Env.base_typ_of env typ in
+       if has_effect eff BE_rreg then
+         let epp = separate space [string "read_reg";doc_id_lem id] in
+         if contains_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
+         then parens (epp ^^ doc_tannot_lem regtypes true base_typ)
+         else epp
+       else if is_ctor env id then doc_id_lem_ctor id
+       else doc_id_lem id
         (*| Base((_,t),Alias alias_info,_,eff,_,_) ->
            (match alias_info with
             | Alias_field(reg,field) ->
@@ -604,20 +592,9 @@ let doc_exp_lem, doc_let_lem =
                     separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
            )*)
-        | _ -> doc_id_lem id)
     | E_lit lit -> doc_lit_lem false lit annot
     | E_cast(typ,e) ->
-       let typ = Env.base_typ_of (env_of full_exp) typ in
-       if is_vector_typ typ then
-         let (start,_,_,_) = vector_typ_args_of typ in
-         let call =
-           if is_bitvector_typ typ then "set_bitvector_start"
-           else "set_vector_start" in
-         let epp = (concat [string call;space;doc_nexp start]) ^//^
-                     expY e in
-         if aexp_needed then parens epp else epp
-       else
-         expV aexp_needed e (*
+       expV aexp_needed e (*
        (match annot with
         | Base((_,t),External _,_,_,_,_) ->
            (* TODO: Does this case still exist with the new type checker? *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 0cf25103..8cf682bf 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -101,17 +101,27 @@ let fresh_id_pat pre ((l,annot)) =
 let union_eff_exps es =
   List.fold_left union_effects no_effect (List.map effect_of es)
 
+let fun_app_effects id env =
+  try
+    match Env.get_val_spec id env with
+    | (_, Typ_aux (Typ_fn (_,_,feff), _)) -> feff
+    | _ -> no_effect
+  with
+  | _ -> no_effect
+
 let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
 | Some (env, typ, eff) ->
-  let effsum = union_effects eff (match e with
+  let effsum = match e with
     | E_block es -> union_eff_exps es
     | E_nondet es -> union_eff_exps es
     | E_id _
-    | E_lit _ -> no_effect
+    | E_lit _ -> eff
     | E_cast (_,e) -> effect_of e
-    | E_app (_,es)
+    | E_app (f,es) ->
+      union_effects (fun_app_effects f env) (union_eff_exps es)
     | E_tuple es -> union_eff_exps es
-    | E_app_infix (e1,_,e2) -> union_eff_exps [e1;e2]
+    | E_app_infix (e1,f,e2) ->
+      union_effects (fun_app_effects f env) (union_eff_exps [e1;e2])
     | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
     | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4]
     | E_vector es -> union_eff_exps es
@@ -136,7 +146,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_exit e -> effect_of e
     | E_return e -> effect_of e
     | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
-    | E_assert (c,m) -> no_effect
+    | E_assert (c,m) -> eff
     | E_comment _ | E_comment_struc _ -> no_effect
     | E_internal_cast (_,e) -> effect_of e
     | E_internal_exp _ -> no_effect
@@ -145,7 +155,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
       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)
-    | E_internal_return e1 -> effect_of e1)
+    | E_internal_return e1 -> effect_of e1
   in
   E_aux (e, (l, Some (env, typ, effsum)))
 | None ->
@@ -189,18 +199,18 @@ let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match snd
 
 let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
 | Some (env, typ, eff) ->
-  let effsum = union_effects eff (match pexp with
+  let effsum = match pexp with
     | Pat_exp (_,e) -> effect_of e
-    | Pat_when (_,e,e') -> union_effects (effect_of e) (effect_of e')) in
+    | Pat_when (_,e,e') -> union_effects (effect_of e) (effect_of e') in
   Pat_aux (pexp, (l, Some (env, typ, effsum)))
 | None ->
   Pat_aux (pexp, (l, None))
 
 let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
 | Some (env, typ, eff) ->
-  let effsum = union_effects eff (match lb with
+  let effsum = match lb with
     | LB_val_explicit (_,_,e) -> effect_of e
-    | LB_val_implicit (_,e) -> effect_of e) in
+    | LB_val_implicit (_,e) -> effect_of e in
   LB_aux (lb, (l, Some (env, typ, effsum)))
 | None ->
   LB_aux (lb, (l, None))
@@ -1961,7 +1971,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
     if (effectful e) then
       let e = rewrite_rec e in
       let (E_aux (_,(el,eannot))) = e in
-      let pat_e' = fresh_id_pat "p__" (el,eannot) 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 exp' = case_exp exp_e' (typ_of full_exp) clauses in