diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 1 | ||||
| -rw-r--r-- | src/lexer.mll | 2 | ||||
| -rw-r--r-- | src/test/power.sail | 10 | ||||
| -rw-r--r-- | src/type_internal.ml | 8 |
4 files changed, 14 insertions, 7 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 9cdb1246..94c3e283 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1841,7 +1841,6 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun a -> update_stack a (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env)))) end -(*TODO The rebuilder function should take an environment and thread through as in to_exp and add_to_top_frame *) and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) = let (Env defs lets regs ctors subregs aliases) = t_level in let (typ,tag,ncs,ef) = match annot with diff --git a/src/lexer.mll b/src/lexer.mll index 5b18026b..1dfcfe12 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -121,7 +121,7 @@ let kw_table = ] -let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "uint8";"uint16";"uint32";"uint64";"implicit"] +let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int"; "uint8";"uint16";"uint32";"uint64";"implicit"] let custom_type_names : string list ref = ref [] } diff --git a/src/test/power.sail b/src/test/power.sail index fd2a87fc..75238732 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -27,14 +27,14 @@ val forall Nat 'n, Nat 'm, 0 <= 'n, 'n <= 'm, 'm <= 63 . MASK function (bit[64]) MASK(start, stop) = { - (bit[64]) mask := 0; + (bit[64]) mask_temp := 0; if(start > stop) then { - mask[start .. 63] := bitone ^^ (64 - start); - mask[0 .. stop] := bitone ^^ (stop + 1); + mask_temp[start .. 63] := bitone ^^ (64 - start); + mask_temp[0 .. stop] := bitone ^^ (stop + 1); } else { - mask[start .. stop ] := bitone ^^ (stop - start + 1); + mask_temp[start .. stop ] := bitone ^^ (stop - start + 1); }; - mask; + mask_temp; } val forall Nat 'n, 0 <= 'n, 'n <= 63 . diff --git a/src/type_internal.ml b/src/type_internal.ml index 79251d5b..d619b2e9 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -739,6 +739,7 @@ let rec fresh_evar bindings e = | _ -> None let nat_t = {t = Tapp("range",[TA_nexp{nexp= Nconst zero};TA_nexp{nexp = Npos_inf};])} +let int_t = {t = Tapp("range",[TA_nexp{nexp=Nneg_inf};TA_nexp{nexp = Npos_inf};])} let uint8_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 8)},Some (big_int_of_int 256))}])} let uint16_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 16)},Some (big_int_of_int 65536))}])} let uint32_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 32)},Some (big_int_of_int 4294967296))}])} @@ -761,6 +762,7 @@ let initial_kind_env = Envmap.from_list [ ("bool", {k = K_Typ}); ("nat", {k = K_Typ}); + ("int", {k = K_Typ}); ("uint8", {k = K_Typ}); ("uint16", {k= K_Typ}); ("uint32", {k=K_Typ}); @@ -778,6 +780,7 @@ let initial_kind_env = let initial_abbrev_env = Envmap.from_list [ ("nat",Base(([],nat_t),Emp_global,[],pure_e)); + ("int",Base(([],int_t),Emp_global,[],pure_e)); ("uint8",Base(([],uint8_t),Emp_global,[],pure_e)); ("uint16",Base(([],uint16_t),Emp_global,[],pure_e)); ("uint32",Base(([],uint32_t),Emp_global,[],pure_e)); @@ -957,6 +960,11 @@ let initial_typ_env = (* incorrect types for typechecking processed sail code; do we care? *) ("to_num_inc",Base(([("a",{k=K_Typ})],({t= Tfn ({t=Tvar "a"},nat_typ,IP_length,pure_e)})),External None,[],pure_e)); ("to_num_dec",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,IP_length,pure_e)}),External None,[],pure_e)); + ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]), + (mk_pure_imp (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m")) + (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "p") (Nvar "o")))), + External (Some "mask"), + [GtEq(Specc(Parse_ast.Int("mask",None)), (mk_nv "m"), (mk_nv "o"))],pure_e)); (*TODO These should be IP_start *) ("to_vec_inc",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},IP_none,pure_e)}),External None,[],pure_e)); ("to_vec_dec",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},IP_none,pure_e)}),External None,[],pure_e)); |