diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 4a429423..61acd867 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1471,6 +1471,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top),lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) (l,annot))))) (fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot))))) + | E_exit exp -> + (Action (Exit exp) (Thunk_frame (E_aux (E_lit (L_aux L_unit Unknown)) (l, intern_annot annot)) t_level l_env l_mem Top),l_mem, l_env) | E_let (lbind : letbind tannot) exp -> match (interp_letbind mode t_level l_env l_mem lbind) with | ((Value v tag_l,lm,le),_) -> diff --git a/src/type_check.ml b/src/type_check.ml index e68337ab..902785df 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1503,7 +1503,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = | (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]), Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) -> let _ = type_consistent (Specc l) d_env item_t item_t2 in - let t = {t= Tapp("vector",[TA_nexp b1; TA_nexp {nexp = Nadd(r,r2)}; TA_ord {order = Oinc}; TA_typ item_t])} in + let t = {t= Tapp("register",[TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp {nexp = Nadd(r,r2)}; TA_ord {order = Oinc}; TA_typ item_t])}])} in let tannot = Base(([],t),Alias,[],pure_e) in let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg1,tannot))} in (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env)) |