summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem16
-rw-r--r--src/pretty_print.ml10
-rw-r--r--src/test/run_power.ml8
-rw-r--r--src/type_check.ml3
-rw-r--r--src/type_internal.ml9
5 files changed, 29 insertions, 17 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index a95f4c01..1f0f9cec 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -63,16 +63,16 @@ let to_num signed (V_vector idx inc l) =
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
-let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
- let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
+let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
+ let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
V_vector 0 true (map bool_to_bit (reverse l)) ;;
-let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
- let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
+let to_vec_dec (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
+ let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
V_vector 0 false (map bool_to_bit l) ;;
let to_vec ord len n =
if ord
- then to_vec_inc len n
- else to_vec_dec len n
+ then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
+ else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
;;
let exts len ((V_vector _ inc _) as v) =
@@ -162,8 +162,8 @@ let function_map = [
("to_num_dec", to_num false);
("exts", exts 64);
(* XXX the size of the target vector should be given by the interpreter *)
- ("to_vec_inc", to_vec_inc 64);
- ("to_vec_dec", to_vec_dec 64);
+ ("to_vec_inc", to_vec_inc);
+ ("to_vec_dec", to_vec_dec);
("bitwise_not", bitwise_not);
("bitwise_not_bit", bitwise_not_bit);
("bitwise_and", bitwise_binop (&&));
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 86772b80..10cd2b68 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -366,8 +366,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
| E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
| E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
- (* XXX missing cases *)
- | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false
+ | E_internal_exp (l, Base((_,t),_,_,_)) ->
+ (match t.t with
+ | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
+ match r.nexp with
+ | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]"
+ kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)))
+ (* Should be unreachable *)
+ | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false
in
print_e ppf e
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 61f60ef3..e1039b0b 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -20,15 +20,15 @@ let hex_to_big_int s = Big_int.big_int_of_int64 (Int64.of_string s) ;;
let big_int_to_vec b size =
(if big_endian then to_vec_inc else to_vec_dec)
- size
- (V_lit (L_aux (L_num b, Unknown)))
+ (V_tuple [(V_lit (L_aux (L_num size, Unknown)));
+ (V_lit (L_aux (L_num b, Unknown)))])
;;
let mem = ref Mem.empty ;;
let add_mem byte addr =
assert(byte >= 0 && byte < 256);
- let vector = big_int_to_vec (Big_int.big_int_of_int byte) 8 in
+ let vector = big_int_to_vec (Big_int.big_int_of_int byte) (Big_int.big_int_of_int 8) in
let key = Id_aux (Id "MEM", Unknown), addr in
mem := Mem.add key vector !mem
;;
@@ -65,7 +65,7 @@ let init_reg () =
V_vector(_, inc, v) ->
V_vector(Big_int.big_int_of_int (64 - size), inc, v)
| _ -> assert false in
- Id_aux(Id name, Unknown), offset (big_int_to_vec value size) in
+ Id_aux(Id name, Unknown), offset (big_int_to_vec value (Big_int.big_int_of_int size)) in
List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
(* XXX execute main() directly until we can handle the init phase *)
init "CIA" (hex_to_big_int !mainaddr) 64;
diff --git a/src/type_check.ml b/src/type_check.ml
index 87560fa1..bb588fc5 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -425,7 +425,8 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let t = {t=Tapp("range", [TA_nexp n;TA_nexp {nexp = Nconst zero};])} in
let cs = [LtEq(Expr l,n,{nexp = N2n(rise,None)})] in
let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" (*Change to follow a default?*) in
- E_aux(E_app((Id_aux((Id f),l)),[simp_exp e l t]),(l,Base(([],expect_t),External (Some f),cs,pure_e))),cs,pure_e
+ let tannot = (l,Base(([],expect_t),External (Some f),cs,pure_e)) in
+ E_aux(E_app((Id_aux((Id f),l)),[(E_aux (E_internal_exp tannot, tannot));simp_exp e l t]),tannot),cs,pure_e
| _ -> simp_exp e l {t = Tapp("range", [TA_nexp{nexp = Nconst (big_int_of_int i)};TA_nexp{nexp= Nconst zero};])},[],pure_e)
| L_hex s -> simp_exp e l {t = Tapp("vector",
[TA_nexp{nexp = Nconst zero};
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 9d222672..0d3f467b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1260,6 +1260,7 @@ let rec nexp_eq_check n1 n2 =
| N2n(n,Some i),N2n(n2,Some i2) -> eq_big_int i i2
| N2n(n,_),N2n(n2,_) -> nexp_eq_check n n2
| Nneg n,Nneg n2 -> nexp_eq_check n n2
+ | Npow(n1,i1),Npow(n2,i2) -> i1=i2 && nexp_eq_check n1 n2
| Nuvar {nindex =i1},Nuvar {nindex = i2} -> i1 = i2
| _,_ -> false
@@ -1445,11 +1446,15 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [LtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n(r1,None)})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
+ let tannot = (l,Base(([],t2),External None, cs,pure_e)) in
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),
+ [(E_aux(E_internal_exp tannot, tannot));e]),tannot))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [LtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n(r1,None)})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
+ let tannot = (l,Base(([],t2),External None,cs,pure_e)) in
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),
+ [(E_aux(E_internal_exp tannot, tannot)); e]),tannot))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ ->
eq_error l "Cannot convert a range to a vector without an order"
| [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 23:10:37 +0000