diff options
| author | Kathy Gray | 2015-06-30 00:01:36 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-06-30 00:01:36 +0100 |
| commit | a5377f57b107351b40f9cd3f303cff6688ccb467 (patch) | |
| tree | 787f24d08d5ed28eb26c5ada2adf5f08c143f2fa | |
| parent | 01100e146e5c6ca2ed2697ff792af42ec37b6cc9 (diff) | |
Fix updating dec vector start bugs
| -rw-r--r-- | src/lem_interp/interp.lem | 3 | ||||
| -rw-r--r-- | src/rewriter.ml | 7 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 |
3 files changed, 8 insertions, 6 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 6edd311b..d0899674 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1263,8 +1263,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | V_vector start dir vs -> if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le) | _ -> (Value v,lm,le) end - | Typ_app (Id_aux (Id "vector") _) - [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_var (Kid_aux (Var "length") _)) _)) _;_;_;_] -> + | (Typ_var (Kid_aux (Var "length") _))-> match (detaint v) with | V_vector start dir vs -> let i = (List.length vs) - 1 in diff --git a/src/rewriter.ml b/src/rewriter.ml index 7999c3b4..eccdcc28 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -70,7 +70,7 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) = | E_nondet exps -> rewrap (E_nondet (List.map rewrite_exp exps)) | E_id _ | E_lit _ -> rewrap exp | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_exp exp)) - | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite_exp exps)) + | E_app (((Id_aux ((Id name),_)) as id),exps) -> rewrap (E_app (id,List.map rewrite_exp exps)) | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite_exp el,id,rewrite_exp er)) | E_tuple exps -> rewrap (E_tuple (List.map rewrite_exp exps)) | E_if (c,t,e) -> rewrap (E_if (rewrite_exp c,rewrite_exp t, rewrite_exp e)) @@ -121,13 +121,14 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) = Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_]) -> (match n1.nexp with | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp)) - | Nadd _ | Nsub _ -> (match o1.order with + | _ -> (match o1.order with | Odec -> + (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) if nexp_one_more_than nw1 n1 then rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp)) else new_exp | _ -> new_exp) - | _ -> new_exp) + | _ -> new_exp) | _ -> new_exp) | _ -> new_exp) | E_internal_exp (l,impl) -> diff --git a/src/type_internal.ml b/src/type_internal.ml index 6f0f1575..e29aa64c 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -825,13 +825,15 @@ let nexp_eq n1 n2 = b let nexp_one_more_than n1 n2 = - let n1,n2 = normalize_nexp n1, normalize_nexp n2 in + let n1,n2 = (normalize_nexp (normalize_nexp n1)), (normalize_nexp (normalize_nexp n2)) in match n1.nexp,n2.nexp with | Nconst i, Nconst j -> (int_of_big_int i) = (int_of_big_int j)+1 | _, Nsub(n2',{nexp = Nconst i}) -> if (int_of_big_int i) = 1 then nexp_eq n1 n2' else false | _, Nadd(n2',{nexp = Nconst i}) -> if (int_of_big_int i) = -1 then nexp_eq n1 n2' else false + | Nadd(n1',{nexp = Nconst i}),_ -> + if (int_of_big_int i) = 1 then nexp_eq n1' n2 else false | _ -> false let equate_t (t_box : t) (t : t) : unit = |