diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 14 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 |
2 files changed, 17 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 9be7a323..a253126a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -766,6 +766,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (lb',t_env',cs,ef) = (check_lbind envs lbind) in let (e,t,_,cs',_) = check_exp (Env(d_env,Envmap.union t_env t_env')) expect_t body in (E_aux(E_let(lb',e),(l,Some(([],t),Emp,cs@cs',pure_e))),t,t_env,cs@cs',pure_e) + | E_assign(lexp,exp) -> + let (lexp',t',t_env',tag,ef) = check_lexp envs lexp in + let (exp',t'',_,cs,ef) = check_exp envs t' exp in + let (t',c') = type_consistent l d_env unit_t expect_t in + (E_aux(E_assign(lexp',exp'),(l,(Some(([],unit_t),tag,cs,ef)))),unit_t,t_env',cs,ef) | _ -> (E_aux(e,(l,annot)),expect_t,t_env,[],pure_e) and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) = @@ -796,6 +801,15 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r t'', csl@cs_p@cs_p'@cs2,union_effects efl ef2) +and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *effect) = + let (Env(d_env,t_env)) = envs in + match lexp with + | LEXP_id id -> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + | LEXP_memory(id,exps) -> (LEXP_aux(lexp,(l,annot)),new_t(),t_env,Emp,pure_e) + | LEXP_vector(vec,acc) -> (LEXP_aux(lexp,(l,annot)),new_t(),t_env,Emp,pure_e) + | LEXP_vector_range(vec,base,range)-> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + | LEXP_field(vec,id)-> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect = let Env(d_env,t_env) = envs in match lbind with diff --git a/src/type_internal.ml b/src/type_internal.ml index bb9801a3..5b196e8b 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -200,7 +200,9 @@ let initial_typ_env = Envmap.from_list [ ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External,[],pure_e)); ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); - ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External,[],pure_e)); ] let initial_abbrev_env = |