diff options
| -rw-r--r-- | src/type_check.ml | 11 | ||||
| -rw-r--r-- | src/type_internal.ml | 12 |
2 files changed, 15 insertions, 8 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 897ef522..1458940b 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1583,9 +1583,12 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | Tabbrev(_,t) -> t,false | _ -> vec_t,false in (match vec_actual.t with | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t]) -> - let acc_t = match ord.order with - | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp (mk_sub (mk_add base rise) n_one)])} - | Odec -> {t = Tapp("range",[TA_nexp (mk_sub rise (mk_add base n_one)); TA_nexp base])} + let acc_n = new_n () in + let acc_t,cs_t = match ord.order with + | Oinc -> mk_atom acc_n, [LtEq(Specc l, Require, base, acc_n); + LtEq(Specc l, Require, acc_n, (mk_sub (mk_add base rise) n_one))] + | Odec -> mk_atom acc_n, [GtEq(Specc l, Require, base, acc_n); + GtEq(Specc l, Require, acc_n, (mk_sub (mk_add base n_one) rise))] | _ -> typ_error l ("Assignment to one vector element requires a non-polymorphic order") in let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param false acc_t acc in @@ -1602,7 +1605,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) else (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],item_t),tag,csi,efl,efr,nob))), item_t,reg_required && reg_still_required, - env,tag,csi@cs',bounds,efl,efr) + env,tag,csi@cs'@cs_t,bounds,efl,efr) | Tuvar _ -> typ_error l "Assignment expected a vector with a known order, try adding an annotation." | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) diff --git a/src/type_internal.ml b/src/type_internal.ml index 9e47ba88..352b980e 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -3587,7 +3587,8 @@ let rec simple_constraint_check in_env cs = (match check_not_eq n1 n2 with | None -> (check cs) | Some(c) -> c::(check cs)) - | GtEq(co,enforce,n1,n2)::cs -> + | GtEq(co,enforce,n1,n2)::cs -> + let n1,n2 = resolve_nsubst n1, resolve_nsubst n2 in (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in @@ -3627,7 +3628,8 @@ let rec simple_constraint_check in_env cs = ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> GtEq(co,enforce,n1',n2')::(check cs)))) - | Gt(co,enforce,n1,n2)::cs -> + | Gt(co,enforce,n1,n2)::cs -> + let n1,n2 = resolve_nsubst n1, resolve_nsubst n2 in (*let _ = Printf.eprintf "> check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in @@ -3647,7 +3649,8 @@ let rec simple_constraint_check in_env cs = ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> Gt(co,enforce,n1',n2')::(check cs))) - | LtEq(co,enforce,n1,n2)::cs -> + | LtEq(co,enforce,n1,n2)::cs -> + let n1,n2 = resolve_nsubst n1, resolve_nsubst n2 in (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in @@ -3666,7 +3669,8 @@ let rec simple_constraint_check in_env cs = ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string n1 ^ " to be less than or equal to " ^ (n_to_string n2)) | Maybe -> LtEq(co,enforce,n1',n2')::(check cs))) - | Lt(co,enforce,n1,n2)::cs -> + | Lt(co,enforce,n1,n2)::cs -> + let n1,n2 = resolve_nsubst n1, resolve_nsubst n2 in (*let _ = Printf.eprintf "< check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in |