diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/test/test2.sail | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 7 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 |
3 files changed, 8 insertions, 4 deletions
diff --git a/src/test/test2.sail b/src/test/test2.sail index 0add0c94..57542d3f 100644 --- a/src/test/test2.sail +++ b/src/test/test2.sail @@ -1,11 +1,14 @@ function nat id ( n ) = n +register (bit[5]) c + function unit f() = { (if( true ) then a := (nat) (3 + 0b01) mod 4 else a := 4 ); + c := (bit[5]) (3 + 0b00001) mod 2; b := a; } diff --git a/src/type_check.ml b/src/type_check.ml index 58df0f14..395a0e73 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -343,9 +343,10 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in (E_aux(E_block(exps'),(l,annot')),t, t_env',sc,ef) | E_nondet exps -> - let checked_exps = List.map (check_exp envs unit_t) exps in - let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in (* WRONG WRONG, place holder. Needs to be a map, intersection of envs, and each should return unit *) - (E_aux(E_nondet(exps'),(l,annot')),t,t_env,sc,ef) + let (ces, sc, ef) = List.fold_right (fun e (es,sc,ef) -> let (e,_,_,sc',ef') = (check_exp envs unit_t e) in + (e::es,sc@sc',union_effects ef ef')) exps ([],[],pure_e) in + let _,cs = type_consistent (Expr l) d_env unit_t expect_t in + (E_aux (E_nondet ces,(l,Base(([],unit_t), Emp_local,sc,ef))),unit_t,t_env,sc,ef) | E_id id -> let i = id_to_string id in (match Envmap.apply t_env i with diff --git a/src/type_internal.ml b/src/type_internal.ml index 049ad398..bda98cf7 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1307,7 +1307,7 @@ and conforms_to_n loosely spec actual = | _ -> true and conforms_to_o loosely spec actual = match (spec.order,actual.order,loosely) with - | (Ouvar _,_,true) | (Oinc,Oinc,_) | (Odec,Odec,_) | (_, Ouvar _,true) -> true + | (Ouvar _,_,true) | (Oinc,Oinc,_) | (Odec,Odec,_) | (_, Ouvar _,_) -> true | _ -> false and conforms_to_e loosely spec actual = match (spec.effect,actual.effect,loosely) with |