summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/l2.lem1
-rw-r--r--language/l2.ml21
-rw-r--r--language/l2.ott1
-rw-r--r--src/initial_check.ml4
-rw-r--r--src/lem_interp/interp.lem28
-rw-r--r--src/pretty_print.ml2
-rw-r--r--src/test/run_tests.ml1
-rw-r--r--src/test/test1.sail5
-rw-r--r--src/type_check.ml49
-rw-r--r--src/type_internal.ml8
10 files changed, 100 insertions, 20 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 4ba01310..32b6f1c7 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -247,6 +247,7 @@ and exp 'a =
and lexp_aux 'a = (* lvalue expression *)
| LEXP_id of id (* identifier *)
| LEXP_memory of id * list (exp 'a) (* memory write via function call *)
+ | LEXP_cast of typ * id
| LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
| LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
| LEXP_field of (lexp 'a) * id (* struct field *)
diff --git a/language/l2.ml b/language/l2.ml
index 4e58d63c..80c94b39 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -74,6 +74,12 @@ base_effect =
type
+effect_aux = (* effect set, of kind Effects *)
+ Effect_var of kid
+ | Effect_set of (base_effect) list (* effect set *)
+
+
+type
order_aux = (* vector order specifications, of kind Order *)
Ord_var of kid (* variable *)
| Ord_inc (* increasing (little-endian) *)
@@ -81,25 +87,19 @@ order_aux = (* vector order specifications, of kind Order *)
type
-effect_aux = (* effect set, of kind Effects *)
- Effect_var of kid
- | Effect_set of (base_effect) list (* effect set *)
-
-
-type
id_aux = (* Identifier *)
Id of x
| DeIid of x (* remove infix status *)
type
-order =
- Ord_aux of order_aux * l
+effect =
+ Effect_aux of effect_aux * l
type
-effect =
- Effect_aux of effect_aux * l
+order =
+ Ord_aux of order_aux * l
type
@@ -289,6 +289,7 @@ and 'a exp =
and 'a lexp_aux = (* lvalue expression *)
LEXP_id of id (* identifier *)
| LEXP_memory of id * ('a exp) list (* memory write via function call *)
+ | LEXP_cast of typ * id
| LEXP_vector of 'a lexp * 'a exp (* vector element *)
| LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
| LEXP_field of 'a lexp * id (* struct field *)
diff --git a/language/l2.ott b/language/l2.ott
index 6efabf62..8aa7417a 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -636,6 +636,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }}
{{ com identifier }}
| id ( exp1 , .. , expn ) :: :: memory {{ com memory write via function call }}
| id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }}
+ | ( typ ) id :: :: cast
| lexp [ exp ] :: :: vector {{ com vector element }}
| lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }}
% maybe comma-sep such lists too
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 83a2c5ab..2a80ff37 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -384,10 +384,12 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
| args -> LEXP_memory(to_ast_id f', args))
| _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
+ | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
+ LEXP_cast(to_ast_typ k_env typ, to_ast_id id)
| Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
| Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
| Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id)
- | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
+ | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
, (l,None))
and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp =
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index fe4568fb..75e6443e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1095,6 +1095,34 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
end)
| (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
| e -> (e,Nothing) end
+ | LEXP_cast typc id ->
+ match tag with
+ | Tag_empty ->
+ match in_env l_env id with
+ | Just (V_boxref n t) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+ else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+ | Just v ->
+ if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_cast typc id) (l,annot)))
+ | Nothing ->
+ if is_top_level
+ then begin
+ let (Mem c m) = l_mem in
+ let l_mem = (Mem (c+1) m) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+ end
+ else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+ end
+ | Tag_extern _ ->
+ let regf = Reg id typ in
+ let request = (Action (Write_reg regf Nothing value)
+ (Frame (Id_aux (Id "0") l)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
+ if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+ | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
+ end
| LEXP_vector lexp exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value i,lm,le) ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index a06d1fe5..7ee110d3 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -261,6 +261,7 @@ and pp_lexp ppf (LEXP_aux(lexp,_)) =
match lexp with
| LEXP_id(id) -> pp_id ppf id
| LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args
+ | LEXP_cast(typ,id) -> fprintf ppf "@[(%a) %a@]" pp_typ typ pp_id id
| LEXP_vector(v,exp) -> fprintf ppf "@[%a%a%a%a@]" pp_lexp v kwd "[" pp_exp exp kwd "]"
| LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a%a%a%a%a%a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]"
| LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id
@@ -681,6 +682,7 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
match lexp with
| LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
| LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id
| LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
| LEXP_vector_range(v,e1,e2) ->
fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index f614306b..d1a90f38 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -6,6 +6,7 @@ let tests = [
"test3", Test3.defs;
"pattern", Pattern.defs;
"vectors", Vectors.defs;
+ "regbits", Regbits.defs;
(*"power", Power.defs;*)
] ;;
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 3d69018d..0050a257 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,6 +14,9 @@ val forall Nat 'a, Nat 'b. bit['a:'b] sliced
let bit v = bitzero
let ( bit [ 32 ] ) v1 = 0b101
+val forall Type 'a. 'a -> 'a effect pure identity
+function forall Type 'a. 'a identity i = i
+
function unit ignore(x) = ()
(* scattered function definition and union definition *)
@@ -32,7 +35,7 @@ function clause f ( C (a) ) = C(a)
end ast
end f
-function unit a (bit) b = if b then () else ()
+function unit a (bit) b = if identity(b) then (identity()) else ()
function bit sw s = switch s { case 0 -> bitzero }
diff --git a/src/type_check.ml b/src/type_check.ml
index 6cf4ca9b..fda5c97c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -148,10 +148,13 @@ let typschm_to_tannot envs ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tann
let (ids,constraints) = typq_to_params envs tq in
Some((ids,t),tag,constraints,pure_e)
-let into_register (t : tannot) : tannot =
+let into_register d_env (t : tannot) : tannot =
match t with
| Some((ids,ty),tag,constraints,eft) ->
- (match ty.t with
+ let ty' = match get_abbrev d_env ty with
+ | Some(t,cs,e) -> t
+ | None -> ty in
+ (match ty'.t with
| Tapp("register",_)-> t
| _ -> Some((ids, {t= Tapp("register",[TA_typ ty])}),tag,constraints,eft))
| None -> None
@@ -375,6 +378,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
| Some(Some((params,t),tag,cs,ef)) ->
let t,cs,ef = subst params t cs ef in
+ let t,cs,ef = match get_abbrev d_env t with
+ | Some(t,cs1,ef1) -> t,cs@cs1,union_effects ef ef1
+ | None -> t,cs,ef in
(match t.t,expect_t.t with
| Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
| Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) ->
@@ -513,7 +519,6 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1,
union_effects ef1 (union_effects then_ef else_ef))
| E_for(id,from,to_,step,order,block) ->
- (* TODO::: This presently assumes increasing; this should be checked if that's the assumption we want *)
let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in
let ft,tt,st = {t=Tapp("enum",[TA_nexp fb;TA_nexp fr])},
{t=Tapp("enum",[TA_nexp tb;TA_nexp tr])},{t=Tapp("enum",[TA_nexp sb;TA_nexp sr])} in
@@ -922,6 +927,36 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
| _ -> typ_error l ("Memory assignments require functions with declared wmem effect"))
| _ -> typ_error l ("Memory assignments require functions, found " ^ i ^ " which has type " ^ (t_to_string t)))
| _ -> typ_error l ("Unbound identifier " ^ i))
+ | LEXP_cast(typ,id) ->
+ let i = id_to_string id in
+ let ty = typ_to_t typ in
+ (match Envmap.apply t_env i with
+ | Some(Some((parms,t),Default,_,_)) ->
+ typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
+ | Some(Some((parms,t),tag,cs,_)) ->
+ let t,cs,_ = subst parms t cs pure_e in
+ let t,cs = match get_abbrev d_env t with
+ | None -> t,cs
+ | Some(t,cs,e) -> t,cs in
+ (match t.t with
+ | Tapp("register",[TA_typ u]) ->
+ let t',cs = type_consistent l d_env ty u in
+ let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
+ (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),ty,Envmap.empty,External (Some "register"),[],ef)
+ | Tapp("reg",[TA_typ u]) ->
+ let t',cs = type_consistent l d_env ty u in
+ (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)
+ | Tuvar _ ->
+ let u' = {t=Tapp("reg",[TA_typ ty])} in
+ t.t <- u'.t;
+ (LEXP_aux(lexp,(l,(Some((([],u'),Emp,cs,pure_e))))),ty,Envmap.empty,Emp,[],pure_e)
+ | _ ->
+ typ_error l
+ ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t))
+ | _ ->
+ let t = {t=Tapp("reg",[TA_typ ty])} in
+ let tannot = (Some(([],t),Emp,[],pure_e)) in
+ (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp,[],pure_e))
| LEXP_vector(vec,acc) ->
let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
let item_t,cs = match get_abbrev d_env item_t with
@@ -936,6 +971,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
in
let (e,t',_,cs',ef_e) = check_exp envs acc_t acc in
(LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,cs@cs',union_effects ef ef_e))),t,env,tag,cs@cs',union_effects ef ef_e)
+ | Tuvar _ -> typ_error l "Assignment to one position expected a vector with a known order, found a polymorphic value, try adding a cast"
| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t)))
| LEXP_vector_range(vec,e1,e2)->
let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
@@ -965,6 +1001,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
let cs = cs_t@cs@cs1@cs2 in
let ef = union_effects ef (union_effects ef_e ef_e') in
(LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Some(([],item_t),tag,cs,ef))),res_t,env,tag,cs,ef)
+ | Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, found a polymorphic value, try addinga cast"
| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t)))
| LEXP_field(vec,id)->
let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
@@ -1070,7 +1107,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Oinc});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e)))
ranges
in
- let tannot = into_register (Some(([],ty),Emp,[],pure_e)) in
+ let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in
(TD_aux(td,(l,tannot)),
Env({d_env with rec_env = ((id',Register,franges)::d_env.rec_env);
abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1097,7 +1134,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e)))
ranges
in
- let tannot = into_register (Some(([],ty),Emp,[],pure_e)) in
+ let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in
(TD_aux(td,(l,tannot)),
Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env;
abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1192,7 +1229,7 @@ let check_def envs (DEF_aux(def,(l,annot))) =
| DEF_reg_dec(typ,id) ->
let t = (typ_to_t typ) in
let i = id_to_string id in
- let tannot = into_register (Some(([],t),External (Some i),[],pure_e)) in
+ let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
(DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 73bd5bc4..932c3057 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -215,7 +215,8 @@ let rec t_subst s_env t =
| Tvar i -> (match Envmap.apply s_env i with
| Some(TA_typ t1) -> t1
| _ -> t)
- | Tid _ | Tuvar _ -> t
+ | Tuvar _ -> new_t ()
+ | Tid _ -> t
| Tfn(t1,t2,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(e_subst s_env e)) }
| Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
| Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
@@ -230,7 +231,8 @@ and n_subst s_env n =
| Nvar i -> (match Envmap.apply s_env i with
| Some(TA_nexp n1) -> n1
| _ -> n)
- | Nconst _ | Nuvar _ -> n
+ | Nuvar _ -> new_n ()
+ | Nconst _ -> n
| N2n n1 -> { nexp = N2n (n_subst s_env n1) }
| Nneg n1 -> { nexp = Nneg (n_subst s_env n1) }
| Nadd(n1,n2) -> { nexp = Nadd(n_subst s_env n1,n_subst s_env n2) }
@@ -240,12 +242,14 @@ and o_subst s_env o =
| Ovar i -> (match Envmap.apply s_env i with
| Some(TA_ord o1) -> o1
| _ -> o)
+ | Ouvar _ -> new_o ()
| _ -> o
and e_subst s_env e =
match e.effect with
| Evar i -> (match Envmap.apply s_env i with
| Some(TA_eft e1) -> e1
| _ -> e)
+ | Euvar _ -> new_e ()
| _ -> e
let rec cs_subst t_env cs =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:31:05 +0000