summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/type_check.ml70
-rw-r--r--src/type_internal.ml1
2 files changed, 45 insertions, 26 deletions
diff --git a/src/type_check.ml b/src/type_check.ml
index 4c59791e..2b07e421 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -583,6 +583,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
in
let check_result ret imp tag cs ef parms =
(*TODO How do I want to pass the information about start along?*)
+
+ (* TODO MAJOR!!!! It may be that the return is a tuple or some bigger structure. THIS IS OK. I need to tie the variable in the implicit to the variable in the type and then put that type here. *)
match (imp,imp_param) with
| (IP_length,None) | (IP_var _,None) ->
(*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*)
@@ -900,46 +902,61 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef (union_effects ef' ef_i))
| E_vector_subrange(vec,i1,i2) ->
let base,rise,ord = new_n(),new_n(),new_o() in
- let min1,m_rise1 = new_n(),new_n() in
- let min2,m_rise2 = new_n(),new_n() in
- let base_n,rise_n,ord_n,item_t = match expect_t.t with
+ let new_base,new_rise = new_n(),new_n() in
+ let n1,min1,max1 = new_n(), new_n(),new_n() in
+ let n2,min2,max2 = new_n(), new_n(),new_n() in
+ let base_e,rise_e,ord_e,item_t = match expect_t.t with
| Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> base_n,rise_n,ord_n,item_t
| _ -> new_n(),new_n(),new_o(),new_t() in
let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
let (vec',t',_,cs,ef) = check_exp envs imp_param vt vec in
- let i1t = {t=Tapp("range",[TA_nexp min1;TA_nexp m_rise1])} in
+ let i1t = {t=Tapp("atom",[TA_nexp n1])} in
let (i1', ti1, _,cs_i1,ef_i1) = check_exp envs imp_param i1t i1 in
- let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in
+ let i2t = {t=Tapp("atom",[TA_nexp n2])} in
let (i2', ti2, _,cs_i2,ef_i2) = check_exp envs imp_param i2t i2 in
let cs_loc =
match (ord.order,d_env.default_o.order) with
| (Oinc,_) ->
- [LtEq((Expr l),base,min1);
- LtEq((Expr l),{nexp=Nadd({nexp=Nadd(min1,m_rise1)},{nexp=Nconst (Big_int.big_int_of_int 1)})},
- {nexp=Nadd(min2,m_rise2)});
- LtEq((Expr l),{nexp=Nadd({nexp=Nadd(min2,m_rise2)},{nexp=Nconst (Big_int.big_int_of_int 1)})},
- {nexp=Nadd(base,rise)});
- LtEq((Expr l),min1,base_n); LtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
- LtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+ [Eq((Expr l), new_base, n1);
+ Eq((Expr l), new_rise, {nexp=Nadd(n2, {nexp = Nneg n1})});
+ LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1);
+ LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2);
+ LtEq((Expr l),base,n1);
+ LtEq((Expr l),base,max1);
+ LtEq((Expr l),n2,{nexp=Nadd(base,rise)});
+ LtEq((Expr l),max2,{nexp=Nadd(base,rise)});]
| (Odec,_) ->
- [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
- GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});
- GtEq((Expr l),min1,base_n); GtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
- GtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+ [Eq((Expr l), new_base, n1);
+ Eq((Expr l), new_rise, {nexp= Nadd({nexp=Nadd(n1, {nexp = Nneg n2})}, {nexp = Nconst one})});
+ LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1);
+ LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2);
+ GtEq((Expr l),base,n1);
+ GtEq((Expr l),base,max1);
+ LtEq((Expr l),n2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});
+ LtEq((Expr l),max2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});]
| (_,Oinc) ->
- [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
- LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});
- LtEq((Expr l),min1,base_n); LtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
- LtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+ [Eq((Expr l), new_base, n1);
+ Eq((Expr l), new_rise, {nexp=Nadd(n2, {nexp = Nneg n1})});
+ LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1);
+ LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2);
+ LtEq((Expr l),base,n1);
+ LtEq((Expr l),base,max1);
+ LtEq((Expr l),n2,{nexp=Nadd(base,rise)});
+ LtEq((Expr l),max2,{nexp=Nadd(base,rise)});]
| (_,Odec) ->
- [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
- GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});
- GtEq((Expr l),min1,base_n); GtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
- GtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+ [Eq((Expr l), new_base, n1);
+ Eq((Expr l), new_rise, {nexp= Nadd({nexp=Nadd(n1, {nexp = Nneg n2})}, {nexp = Nconst one})});
+ LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1);
+ LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2);
+ GtEq((Expr l),base,n1);
+ GtEq((Expr l),base,max1);
+ LtEq((Expr l),n2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});
+ LtEq((Expr l),max2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});]
| _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in
- let nt = {t=Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord;TA_typ item_t])} in
+ let nt = {t=Tapp("vector",[TA_nexp new_base;TA_nexp new_rise; TA_ord ord;TA_typ item_t])} in
let (t,cs3,ef3,e') =
- type_coerce (Expr l) d_env false false nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env false false nt
+ (E_aux(E_vector_subrange(vec',i1',i2'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,(union_effects ef (union_effects ef3 (union_effects ef_i1 ef_i2))))
| E_vector_update(vec,i,e) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -1659,6 +1676,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
(*let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
(*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
+ let t', _ = type_consistent (Patt l) d_env false param_t t' in
let exp',_,_,cs_e,ef =
check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env')) imp_param ret_t exp in
(*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 95f48461..0598b61f 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1874,6 +1874,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 =
let cs = csp@[Eq(co,r1,r2)] in
let t',cs' = type_consistent co d_env widen t1i t2i in
let tannot = Base(([],t2),Emp_local,cs@cs',pure_e) in
+ (*let _ = Printf.printf "looking at vector vector coerce, t1 %s, t2 %s\n" (t_to_string t1) (t_to_string t2) in*)
let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e))),e),(l,tannot)) in
(t2,cs@cs',pure_e,e')
| _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 14:10:42 +0000