summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/lem_interp/interp.lem14
-rw-r--r--src/lem_interp/interp_lib.lem20
-rw-r--r--src/parser.mly4
-rw-r--r--src/pretty_print.ml2
-rw-r--r--src/test/power.sail6
-rw-r--r--src/test/test3.sail2
-rw-r--r--src/type_check.ml180
-rw-r--r--src/type_internal.ml58
-rw-r--r--src/type_internal.mli5
10 files changed, 180 insertions, 112 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 95578d9f..0cd58e02 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -359,6 +359,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
| Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
| Parse_ast.E_vector_update_subrange(vex,e1,e2,e3) -> E_vector_update_subrange(to_ast_exp k_env vex, to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
+ | Parse_ast.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env e1,to_ast_exp k_env e2)
| Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env) exps)
| Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env e1, to_ast_exp k_env e2)
| Parse_ast.E_record _ -> raise (Reporting_basic.err_unreachable l "parser generated an E_record")
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index f0770d4e..2960f048 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -986,6 +986,20 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) (l,annot))))
| _ -> (Error l "vector update requires number",lm,le) end)
(fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot))))
+ | E_vector_append e1 e2 ->
+ resolve_outcome (interp_main mode t_level l_env l_mem e1)
+ (fun v1 lm le ->
+ match v1 with
+ | V_vector m inc vals1 ->
+ (resolve_outcome (interp_main mode t_level l_env lm e2)
+ (fun v2 lm le ->
+ match v2 with
+ | V_vector _ _ vals2 -> (Value (V_vector m inc (vals1++vals2)) Tag_empty,lm,l_env)
+ | _ -> (Error l "vector concat requires vector",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame
+ (fun e -> E_aux (E_vector_append (to_exp v1) e) (l,annot)))))
+ | _ -> (Error l "vector concat requires vector",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux (E_vector_append e e2) (l,annot))))
| E_tuple(exps) ->
exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 753de883..e994fdfe 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -39,6 +39,11 @@ let bitwise_not (V_vector idx inc v) =
let apply x = bool_to_bit(not (bit_to_bool x)) in
V_vector idx inc (List.map apply v)
+let bitwise_not_bit (V_lit (L_aux l loc)) = match l with
+ | L_zero -> (V_lit (L_aux L_one loc))
+ | L_one -> (V_lit (L_aux L_zero loc))
+end;;
+
let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
(* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
@@ -74,14 +79,16 @@ let arith_op_vec op (V_tuple args) = match args with
else to_vec_dec (List.length cs) n
end ;;
let arith_op_range_vec op (V_tuple args) = match args with
- | [l1; (V_vector _ _ _ as l2)] ->
- let l2 = (to_num true l2) in
- arith_op op (V_tuple [l1;l2])
+ | [n; (V_vector _ ord cs as l2)] ->
+ if ord
+ then arith_op_vec op (V_tuple [(to_vec_inc (List.length cs) n);l2])
+ else arith_op_vec op (V_tuple [(to_vec_dec (List.length cs) n);l2])
end ;;
let arith_op_vec_range op (V_tuple args) = match args with
- | [(V_vector _ _ _ as l1);l2] ->
- let l1 = (to_num true l1) in
- arith_op op (V_tuple [l1;l2])
+ | [(V_vector _ ord cs as l1);n] ->
+ if ord
+ then arith_op_vec op (V_tuple [l1;(to_vec_inc (List.length cs) n)])
+ else arith_op_vec op (V_tuple [l1;(to_vec_dec (List.length cs) n)])
end ;;
let compare_op op (V_tuple args) = match args with
@@ -123,6 +130,7 @@ let function_map = [
("to_vec_inc", to_vec_inc 64);
("to_vec_dec", to_vec_dec 64);
("bitwise_not", bitwise_not);
+ ("bitwise_not_bit", bitwise_not_bit);
("bitwise_and", bitwise_binop (&&));
("bitwise_or", bitwise_binop (||));
("bitwise_xor", bitwise_binop xor);
diff --git a/src/parser.mly b/src/parser.mly
index 75cdcf7d..aa088994 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -726,7 +726,7 @@ cons_exp:
| shift_exp ColonColon cons_exp
{ eloc (E_cons($1,$3)) }
| shift_exp Colon cons_exp
- { eloc (E_app_infix($1,Id_aux(Id(":"), locn 2 2), $3)) }
+ { eloc (E_vector_append($1, $3)) }
cons_right_atomic_exp:
| shift_right_atomic_exp
@@ -734,7 +734,7 @@ cons_right_atomic_exp:
| shift_exp ColonColon cons_right_atomic_exp
{ eloc (E_cons($1,$3)) }
| shift_exp Colon cons_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id(":"), locn 2 2), $3)) }
+ { eloc (E_vector_append($1, $3)) }
at_exp:
| cons_exp
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 3d8b0e91..7ade113c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -348,6 +348,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
| E_vector_update_subrange(v,e1,e2,e3) ->
fprintf ppf "@[<0>(E_aux (%a %a %a %a %a) (%a, %a))@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot
+ | E_vector_append(v1,v2) ->
+ fprintf ppf "@[<0>(E_aux (E_vector_append %a %a) (%a, %a))@]" pp_lem_exp v1 pp_lem_exp v2 pp_lem_l l pp_annot annot
| E_list(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
| E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
| E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
diff --git a/src/test/power.sail b/src/test/power.sail
index 02b4555f..adcd0d9f 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -126,7 +126,7 @@ scattered function ast decode
function clause execute ( LoadWordandZero ( D, RA, RT ) ) =
{ (bit[64]) EA := 0; (bit[64]) b := 0; {
- if((bit) ( RA == 0 ) ) then b := 0 else b := (GPR[ RA ]) ;
+ if((bit) ( (nat) RA == 0 ) ) then b := 0 else b := (GPR[ RA ]) ;
EA := ( b + ( exts ( D )) ) ;
GPR[ RT ] := ( 0b00000000000000000000000000000000 : MEM( EA , 4 ) ) ;
} }
@@ -139,7 +139,7 @@ scattered function ast decode
function clause execute ( StoreWord ( D, RA, RS ) ) =
{ (bit[64]) EA := 0; (bit[64]) b := 0; {
- if((bit) ( RA == 0 ) ) then b := 0 else b := (GPR[ RA ]) ;
+ if((bit) ( (nat) RA == 0 ) ) then b := 0 else b := (GPR[ RA ]) ;
EA := ( b + ( exts ( D )) ) ;
MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ;
} }
@@ -165,7 +165,7 @@ scattered function ast decode
function clause execute ( AddImmediate ( RA, RT, SI ) ) =
{ {
- if((bit) ( RA == 0 ) ) then GPR[ RT ] := ( exts ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( exts ( SI )) ) ;
+ if((bit) ( (nat) RA == 0 ) ) then GPR[ RT ] := (bit[64]) ( exts ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( exts ( SI )) ) ;
} }
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 06086dd7..3a806f41 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -48,7 +48,7 @@ function nat main _ = {
dummy_reg := (deinfix +)(5, 37);
(* casts and external calls *)
dummy_reg := 0b01 + 0b01;
- dummy_reg2 := dummy_reg; (* cast from [|256|] to bit[8] *)
+ dummy_reg2 := 0b00000001;
dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *)
dummy_reg2; (* cast again and return 4 *)
}
diff --git a/src/type_check.ml b/src/type_check.ml
index 073b36a7..5311b0b6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -14,6 +14,11 @@ let id_to_string (Id_aux(id,l)) =
| Id(s) -> s
| DeIid(s) -> s
+let get_e_typ (E_aux(_,(_,a))) =
+ match a with
+ | Base((_,t),_,_,_) -> t
+ | _ -> new_t ()
+
let typ_error l msg =
raise (Reporting_basic.err_typ
l
@@ -330,6 +335,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent (Patt l) d_env u t in t',cs@cs') ts (item_t,[]) in
let t = {t = Tapp("list",[TA_typ u])} in
(P_aux(P_list(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
+
+let simp_exp e l t = E_aux(e,(l,Base(([],t),Emp_local,[],pure_e)))
let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp * t * tannot emap * nexp_range list * effect) =
let Env(d_env,t_env) = envs in
@@ -345,14 +352,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let t,cs,ef = subst params t cs ef in
(match t.t with
| Tfn({t = Tid "unit"},t',ef) ->
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Base(([],{t=Tfn(unit_t,t',ef)}),Constructor,cs,ef))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild (Base(([],{t=Tfn(unit_t,t',ef)}),Constructor,cs,ef))) expect_t in
(e',t',t_env,cs@cs',ef)
| Tfn(t1,t',e) ->
typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
| _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
| Some(Base((params,t),Enum,cs,ef)) ->
let t',cs,_ = subst params t cs ef in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Base(([],t'),Enum,cs,pure_e))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild (Base(([],t'),Enum,cs,pure_e))) expect_t in
(e',t',t_env,cs@cs',pure_e)
| Some(Base(tp,Default,cs,ef)) | Some(Base(tp,Spec,cs,ef)) ->
typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
@@ -369,72 +376,74 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| 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')]) ->
let tannot = Base(([],t),Emp_local,cs,ef) in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_t' in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_t' in
(e',t,t_env,cs@cs',ef)
| Tapp("register",[TA_typ(t')]),Tuvar _ ->
let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
let tannot = Base(([],t),External (Some i),cs,ef') in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_actual in
(e',t,t_env,cs@cs',ef)
| Tapp("register",[TA_typ(t')]),_ ->
let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
let tannot = Base(([],t),External (Some i),cs,ef') in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_actual in
(e',t',t_env,cs@cs',ef)
| Tapp("reg",[TA_typ(t')]),_ ->
let tannot = Base(([],t),Emp_local,cs,pure_e) in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual in
+ let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_actual in
(e',t',t_env,cs@cs',pure_e)
| _ ->
- let t',cs',e' = type_coerce (Expr l) d_env t (rebuild (Base(([],t),tag,cs,pure_e))) expect_t in
- (e',t,t_env,cs@cs',pure_e)
+ let t',cs',e' = type_coerce (Expr l) d_env false t (rebuild (Base(([],t),tag,cs,pure_e))) expect_t in
+ (e',t',t_env,cs@cs',pure_e)
)
| Some NoTyp | Some Overload _ | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
| E_lit (L_aux(lit,l')) ->
- let t,lit',effect = (match lit with
- | L_unit -> unit_t,lit,pure_e
+ let e,cs,effect = (match lit with
+ | L_unit -> (rebuild (Base (([],unit_t), Emp_local,[],pure_e))),[],pure_e
| L_zero ->
(match expect_t.t with
- | Tid "bool" -> bool_t,L_false,pure_e
- | _ -> bit_t,lit,pure_e)
+ | Tid "bool" -> simp_exp (E_lit(L_aux(L_false,l'))) l bool_t,[],pure_e
+ | _ -> simp_exp e l bit_t,[],pure_e)
| L_one ->
(match expect_t.t with
- | Tid "bool" -> bool_t,L_true,pure_e
- | _ -> bit_t,lit,pure_e)
- | L_true -> bool_t,lit,pure_e
- | L_false -> bool_t,lit,pure_e
+ | Tid "bool" -> simp_exp (E_lit(L_aux(L_true,l'))) l bool_t,[],pure_e
+ | _ -> simp_exp e l bit_t,[],pure_e)
+ | L_true -> simp_exp e l bool_t,[],pure_e
+ | L_false -> simp_exp e l bool_t,[],pure_e
| L_num i ->
(match expect_t.t with
| Tid "bit" ->
- if i = 0 then bit_t,L_zero,pure_e
- else
- if i = 1 then bit_t,L_one,pure_e
- else typ_error l "Expected bit, found a number that cannot be used as a bit"
+ if i = 0 then simp_exp (E_lit(L_aux(L_zero,l'))) l bit_t,[],pure_e
+ else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t,[],pure_e
+ else typ_error l ("Expected a bit, found " ^ string_of_int i)
| Tid "bool" ->
- if i = 0 then bool_t, L_false,pure_e
- else
- if i = 1 then bool_t,L_true,pure_e
- else typ_error l "Expected bool, found a number that cannot be used as a bit and converted to bool"
- | _ -> {t = Tapp("range",
- [TA_nexp{nexp = Nconst (big_int_of_int i)};TA_nexp{nexp= Nconst zero};])},lit,pure_e)
- | L_hex s -> {t = Tapp("vector",
- [TA_nexp{nexp = Nconst zero};
- TA_nexp{nexp = Nconst (big_int_of_int ((String.length s)*4))};
- TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])},lit,pure_e
- | L_bin s -> {t = Tapp("vector",
- [TA_nexp{nexp = Nconst zero};
- TA_nexp{nexp = Nconst (big_int_of_int (String.length s))};
- TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])},lit,pure_e
- | L_string s -> {t = Tid "string"},lit,pure_e
- | L_undef -> new_t (),lit,{effect=Eset[BE_aux(BE_undef,l)]}) in
- let t',cs',e' =
- type_coerce (Expr l) d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Base(([],t),Emp_local,[],effect))))) expect_t in
- (e',t',t_env,cs',effect)
+ if i = 0 then simp_exp (E_lit(L_aux(L_false,l'))) l bool_t,[],pure_e
+ else if i = 1 then simp_exp (E_lit(L_aux(L_true,l'))) l bool_t ,[],pure_e
+ else typ_error l ("Expected bool or a bit, found " ^ string_of_int i)
+ | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) ->
+ let n = {nexp = Nconst (big_int_of_int i) } in
+ 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
+ | _ -> 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};
+ TA_nexp{nexp = Nconst (big_int_of_int ((String.length s)*4))};
+ TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])},[],pure_e
+ | L_bin s -> simp_exp e l {t = Tapp("vector",
+ [TA_nexp{nexp = Nconst zero};
+ TA_nexp{nexp = Nconst (big_int_of_int (String.length s))};
+ TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])},[],pure_e
+ | L_string s -> simp_exp e l {t = Tid "string"},[],pure_e
+ | L_undef -> simp_exp e l (new_t ()),[],{effect=Eset[BE_aux(BE_undef,l)]}) in
+ let t',cs',e' = type_coerce (Expr l) d_env false (get_e_typ e) e expect_t in
+ (e',t',t_env,cs@cs',effect)
| E_cast(typ,e) ->
let t = typ_to_t typ in
let (e',u,t_env,cs,ef) = check_exp envs (new_t ()) e in
- let t',cs2,e' = type_coerce (Expr l) d_env u e' t in
- let t',cs3,e'' = type_coerce (Expr l) d_env t e' expect_t in
+ let t',cs2,e' = type_coerce (Expr l) d_env true u e' t in
+ let t',cs3,e'' = type_coerce (Expr l) d_env false t e' expect_t in
(e'',t',t_env,cs@cs2@cs3,ef)
| E_app(id,parms) ->
let i = id_to_string id in
@@ -450,15 +459,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(match parms with
| [] ->
let (p',cs') = type_consistent (Expr l) d_env unit_t arg in
- let (ret_t,cs_r,e') = type_coerce (Expr l) d_env ret (rebuild (Base(([],ret),tag,cs@cs',ef))) expect_t in
+ let (ret_t,cs_r,e') = type_coerce (Expr l) d_env false ret (rebuild (Base(([],ret),tag,cs@cs',ef))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r,ef)
| [parm] ->
let (parm',arg_t,t_env,cs',ef_p) = check_exp envs arg parm in
- let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id,[parm']),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
+ let (ret_t,cs_r',e') = type_coerce (Expr l) d_env false ret (E_aux(E_app(id,[parm']),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef')
| parms ->
let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,NoTyp))) in
- let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id, parms'),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
+ let (ret_t,cs_r',e') = type_coerce (Expr l) d_env false ret (E_aux(E_app(id, parms'),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef'))
| _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
| Some(Overload(Base((params,t),tag,cs,ef),variants)) ->
@@ -485,14 +494,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let args',arg_cs' =
(match args with
| [parm] ->
- let _,cs,parm' = type_coerce (Expr l) d_env arg_t parm arg in
+ let _,cs,parm' = type_coerce (Expr l) d_env false arg_t parm arg in
[parm'],cs
| parms ->
let (_,cs,(E_aux(E_tuple parms',tannot'))) =
- type_coerce (Expr l) d_env arg_t (E_aux(E_tuple parms,(l,NoTyp))) arg in
+ type_coerce (Expr l) d_env false arg_t (E_aux(E_tuple parms,(l,NoTyp))) arg in
parms',cs) in
let (ret_t,cs_r,e') =
- type_coerce (Expr l) d_env ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+ type_coerce (Expr l) d_env false ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
(e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef'))
| _ -> assert false))
| _ -> typ_error l ("Unbound function " ^ i))
@@ -508,7 +517,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(match t.t with
| Tfn(arg,ret,ef) ->
let (E_aux(E_tuple [lft';rht'],tannot'),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple [lft;rht],(l,NoTyp))) in
- let ret_t,cs_r',e' = type_coerce (Expr l) d_env ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+ let ret_t,cs_r',e' = type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef')
| _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
| Some(Overload(Base((params,t),tag,cs,ef),variants)) ->
@@ -519,18 +528,19 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let (E_aux(E_tuple [lft';rht'],tannot'),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple [lft;rht],(l,NoTyp))) in
(lft',rht',arg_t,cs',ef')
| _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+ (*let _ = Printf.printf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" i (t_to_string t_p) (t_to_string arg_t) in*)
(match (select_overload_variant d_env variants arg_t) with
| NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
| Base((params,t),tag,cs,ef) ->
- (*let _ = Printf.eprintf "Selected an overloaded function for %s, variant with function type %s\n" i (t_to_string t) in*)
+ (*let _ = Printf.eprintf "Selected an overloaded function for %s, variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
(match t.t with
| Tfn(arg,ret,ef') ->
(match arg.t,arg_t.t with
| Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
- let (_,cs_lft,lft') = type_coerce (Expr l) d_env tlft_t lft' tlft in
- let (_,cs_rght,rht') = type_coerce (Expr l) d_env trght_t rht' trght in
+ let (_,cs_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+ let (_,cs_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
let (ret_t,cs_r,e') =
- type_coerce (Expr l) d_env ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+ type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
(e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,union_effects ef_p (union_effects arg_ef ef'))
|_ -> assert false)
| _ -> assert false))
@@ -556,17 +566,29 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let (e',t,_,c,ef) = check_exp envs (new_t ()) e in ((e'::exps),(t::typs),c@consts,union_effects ef effect))
exps ([],[],[],pure_e) in
let t = { t=Ttup typs } in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_tuple(exps),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_tuple(exps),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,consts@cs',effect))
| E_if(cond,then_,else_) ->
let (cond',_,_,c1,ef1) = check_exp envs bool_t cond in
- let then',then_t,then_env,then_c,then_ef = check_exp envs expect_t then_ in
- let else',else_t,else_env,else_c,else_ef = check_exp envs expect_t else_ in
- let t_cs = CondCons((Expr l),c1,then_c) in
- let e_cs = CondCons((Expr l),[],else_c) in
- (E_aux(E_if(cond',then',else'),(l,Base(([],expect_t),Emp_local,[],pure_e))),
- expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,[t_cs;e_cs],
- union_effects ef1 (union_effects then_ef else_ef))
+ (match expect_t.t with
+ | Tuvar _ ->
+ let then',then_t,then_env,then_c,then_ef = check_exp envs (new_t ()) then_ in
+ let else',else_t,else_env,else_c,else_ef = check_exp envs (new_t ()) else_ in
+ let then_t',then_c' = type_consistent (Expr l) d_env then_t expect_t in
+ let else_t',else_c' = type_consistent (Expr l) d_env else_t then_t' in
+ let t_cs = CondCons((Expr l),c1,then_c@then_c') in
+ let e_cs = CondCons((Expr l),[],else_c@else_c') in
+ (E_aux(E_if(cond',then',else'),(l,Base(([],expect_t),Emp_local,[],pure_e))),
+ expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,[t_cs;e_cs],
+ union_effects ef1 (union_effects then_ef else_ef))
+ | _ ->
+ let then',then_t,then_env,then_c,then_ef = check_exp envs expect_t then_ in
+ let else',else_t,else_env,else_c,else_ef = check_exp envs expect_t else_ in
+ let t_cs = CondCons((Expr l),c1,then_c) in
+ let e_cs = CondCons((Expr l),[],else_c) in
+ (E_aux(E_if(cond',then',else'),(l,Base(([],expect_t),Emp_local,[],pure_e))),
+ expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,[t_cs;e_cs],
+ union_effects ef1 (union_effects then_ef else_ef)))
| E_for(id,from,to_,step,order,block) ->
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("range",[TA_nexp fb;TA_nexp fr])},
@@ -595,7 +617,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
(List.map (check_exp envs item_t) es) ([],[],pure_e)) in
let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst zero});TA_nexp({nexp=Nconst (big_int_of_int (List.length es))});TA_ord({order=Oinc});TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_vector_indexed(eis,default) ->
let item_t = match expect_t.t with
@@ -614,7 +636,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
eis) ([],[],pure_e,first)) in
let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst (big_int_of_int first)});TA_nexp({nexp=Nconst (big_int_of_int (List.length eis))});
TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_vector_access(vec,i) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -636,7 +658,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
in
(*let _ = Printf.eprintf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*)
- let t',cs',e'=type_coerce (Expr l) d_env item_t (E_aux(E_vector_access(vec',i'),(l,Base(([],item_t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e'=type_coerce (Expr l) d_env false item_t (E_aux(E_vector_access(vec',i'),(l,Base(([],item_t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i)
| E_vector_subrange(vec,i1,i2) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -666,7 +688,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in
let nt = {t=Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env false nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,(union_effects ef (union_effects ef_i1 ef_i2)))
| E_vector_update(vec,i,e) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -689,7 +711,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
in
let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_update(vec',i',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env false nt (E_aux(E_vector_update(vec',i',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,(union_effects ef (union_effects ef_i ef_e)))
| E_vector_update_subrange(vec,i1,i2,e) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -723,8 +745,24 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in
let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env false nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,(union_effects ef (union_effects ef_i1 (union_effects ef_i2 ef_e))))
+ | E_vector_append(v1,v2) ->
+ let item_t,ord = match expect_t.t with
+ | Tapp("vector",[_;_;TA_ord o;TA_typ i]) -> i,o
+ | Tapp("range",_) -> bit_t,new_o ()
+ | _ -> new_t (),new_o () in
+ let base1,rise1 = new_n(), new_n() in
+ let base2,rise2 = new_n(),new_n() in
+ let (v1',t1',_,cs_1,ef_1) = check_exp envs {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in
+ let (v2',t2',_,cs_2,ef_2) = check_exp envs {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in
+ let ti = {t=Tapp("vector",[TA_nexp base1;TA_nexp {nexp = Nadd(rise1,rise2)};TA_ord ord; TA_typ item_t])} in
+ let cs_loc = match ord.order with
+ | Odec -> [GtEq((Expr l),base1,{nexp = Nadd(rise1,rise2)})]
+ | _ -> [] in
+ let (t,cs_c,e') =
+ type_coerce (Expr l) d_env false ti (E_aux(E_vector_append(v1',v2'),(l,Base(([],ti),Emp_local,cs_loc,pure_e)))) expect_t in
+ (e',t,t_env,cs_loc@cs_1@cs_2,(union_effects ef_1 ef_2))
| E_list(es) ->
let item_t = match expect_t.t with
| Tapp("list",[TA_typ i]) -> i
@@ -733,7 +771,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(List.fold_right (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
(List.map (check_exp envs item_t) es) ([],[],pure_e)) in
let t = {t = Tapp("list",[TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_list es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_list es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_cons(ls,i) ->
let item_t = match expect_t.t with
@@ -742,7 +780,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let lt = {t=Tapp("list",[TA_typ item_t])} in
let (ls',t',_,cs,ef) = check_exp envs lt ls in
let (i', ti, _,cs_i,ef_i) = check_exp envs item_t i in
- let (t',cs',e') = type_coerce (Expr l) d_env lt (E_aux(E_cons(ls',i'),(l,Base(([],lt),Emp_local,[],pure_e)))) expect_t in
+ let (t',cs',e') = type_coerce (Expr l) d_env false lt (E_aux(E_cons(ls',i'),(l,Base(([],lt),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs'@cs_i,(union_effects ef ef_i))
| E_record(FES_aux(FES_Fexps(fexps,_),l')) ->
let u,_ = get_abbrev d_env expect_t in
@@ -848,7 +886,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
| Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(acc,et',t_env,cs@c',ef)))
| Tid i ->
(match lookup_record_typ i d_env.rec_env with
@@ -860,7 +898,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
| Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(acc,et',t_env,cs@c',ef)))
| Tuvar _ ->
let fi = id_to_string id in
@@ -873,7 +911,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field")
| Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(*TODO tHIS should be equate_t*)
t'.t <- Tid i;
(acc,et',t_env,cs@c',ef))
diff --git a/src/type_internal.ml b/src/type_internal.ml
index c9a702e3..0c3efcab 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -759,15 +759,24 @@ let initial_typ_env =
Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
(mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
mk_range (mk_nv "o") (mk_nv "p")])
- (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+ (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
External (Some "add_vec_range"),
[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
(mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
- (mk_range (mk_nv "o") {nexp = N2n (mk_nv "m",None)}))),
+ (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
External (Some "add_range_vec"),
- [],pure_e); ]));
+ [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
+ Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t])
+ (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
+ External (Some "add_vec_bit"), [], pure_e);
+ Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
+ (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")])
+ (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
+ External (Some "add_bit_vec"), [], pure_e);
+ ]));
("*",Base(((mk_nat_params ["n";"m";"o";"p"]),
(mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
(mk_range (mk_mult (mk_nv "n") (mk_nv "o")) (mk_mult (mk_nv "m") (mk_nv "p"))))),
@@ -788,15 +797,15 @@ let initial_typ_env =
Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
(mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
mk_range (mk_nv "o") (mk_nv "p")])
- (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+ (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
External (Some "minus_vec_range"),
[LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
(mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
- (mk_range (mk_nv "o") {nexp = N2n (mk_nv "m",None)}))),
+ (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
External (Some "minus_range_vec"),
- [],pure_e); ]));
+ [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); ]));
("mod",
Overload(Base(((mk_typ_params ["a";"b";"c"]),
(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
@@ -826,18 +835,13 @@ let initial_typ_env =
mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")])
(mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
External (Some "quot_vec"),[],pure_e)]));
- (":",Base(((mk_nat_params["n";"m";"o";"p"]@(mk_ord_params["ord"])@(mk_typ_params ["a"])),
- (mk_pure_fun (mk_tup [mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m");
- mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "o") (Nvar "p")])
- (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nadd((mk_nv "m"), (mk_nv "p")))))),
- External (Some "vec_concat"),[(*TODO:: This is incorrect when ord is dec, as then n >= m+p is needed *)],pure_e));
(* incorrect types, not pressing as the type checker puts in the correct types automatically on a first pass *)
("to_num_inc",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
("to_num_dec",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
("to_vec_inc",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
("to_vec_dec",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
("==",
- Overload( Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e),
+ Overload( Base((mk_typ_params ["a";"b"],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),External (Some "eq"),[],pure_e),
[Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
{t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "eq"),
[Eq(Specc(Parse_ast.Int("==",None)),
@@ -1211,23 +1215,23 @@ and type_arg_eq co d_env ta1 ta2 =
and type_consistent co d_env t1 t2 =
type_consistent_internal co d_env t1 [] t2 []
-let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
+let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
let l = get_c_loc co in
let t1,cs1' = get_abbrev d_env t1 in
let t2,cs2' = get_abbrev d_env t2 in
let cs1,cs2 = cs1@cs1',cs2@cs2' in
let csp = cs1@cs2 in
match t1.t,t2.t with
- | Tabbrev(_,t1),Tabbrev(_,t2) -> type_coerce_internal co d_env t1 cs1 e t2 cs2
- | Tabbrev(_,t1),_ -> type_coerce_internal co d_env t1 cs1 e t2 cs2
- | _,Tabbrev(_,t2) -> type_coerce_internal co d_env t1 cs1 e t2 cs2
+ | Tabbrev(_,t1),Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
+ | Tabbrev(_,t1),_ -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
+ | _,Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
| Ttup t1s, Ttup t2s ->
let tl1,tl2 = List.length t1s,List.length t2s in
if tl1=tl2 then
let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in
let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Base(([],t),Emp_local,[],pure_e)))) ids t1s in
let (coerced_ts,cs,coerced_vars) =
- List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce co d_env t1 v t2 in
+ List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce co d_env is_explicit t1 v t2 in
((t'::ts),c'@cs,(e'::es)))
vars (List.combine t1s t2s) ([],[],[]) in
if vars = coerced_vars then (t2,cs,e)
@@ -1242,8 +1246,8 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| Tapp(id1,args1),Tapp(id2,args2) ->
if id1=id2 && (id1 <> "vector")
then let t',cs' = type_consistent co d_env t1 t2 in (t',cs',e)
- else (match id1,id2 with
- | "vector","vector" ->
+ else (match id1,id2,is_explicit with
+ | "vector","vector",_ ->
(match args1,args2 with
| [TA_nexp b1;TA_nexp r1;TA_ord o1;TA_typ t1i],
[TA_nexp b2;TA_nexp r2;TA_ord o2;TA_typ t2i] ->
@@ -1258,7 +1262,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e))),e),(l,tannot)) in
(t2,cs@cs',e')
| _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
- | "vector","range" ->
+ | "vector","range",_ ->
(match args1,args2 with
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
@@ -1273,7 +1277,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ ->
eq_error l "Cannot convert non-bit vector into an range"
| _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
- | "range","vector" ->
+ | "range","vector",true ->
(match args2,args1 with
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
@@ -1288,17 +1292,17 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ ->
eq_error l "Cannot convert an range into a non-bit vector"
| _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
- | "register",_ ->
+ | "register",_,_ ->
(match args1 with
| [TA_typ t] ->
(*TODO Should this be an internal cast? Probably, make sure it doesn't interfere with the other internal cast and get removed *)
(*let _ = Printf.printf "Adding cast to remove register read\n" in*)
let new_e = E_aux(E_cast(t_to_typ unit_t,e),(l,Base(([],t),External None,[],(add_effect (BE_aux(BE_rreg, l)) pure_e)))) in
- type_coerce co d_env t new_e t2
+ type_coerce co d_env is_explicit t new_e t2
| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
- | _,_ ->
+ | _,_,_ ->
let t',cs' = type_consistent co d_env t1 t2 in (t',cs',e))
- | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
+ (*| Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
let cs = [Eq(co,r1,{nexp = Nconst one})] in
(*WARNING: shrinking i to an int; should add a check*)
let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst one};TA_ord o;TA_typ {t=Tid "bit"}])} in
@@ -1307,7 +1311,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
let cs = [Eq(co,r1,{nexp = Nconst one})] in
(t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num (int_of_big_int i),l)),
(l,Base(([],{t=Tapp("range",[TA_nexp b1;TA_nexp {nexp=Nconst zero}])}),Emp_local,cs,pure_e)))))),
- (l,Base(([],t2),Emp_local,cs,pure_e))))
+ (l,Base(([],t2),Emp_local,cs,pure_e))))*)
| Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) ->
let t',cs'= type_consistent co d_env {t=Tapp("range",[TA_nexp{nexp=Nconst zero};TA_nexp{nexp=Nconst one}])} t2 in
(t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Base(([],t1),Emp_local,[],pure_e))),
@@ -1352,7 +1356,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
| _,_ -> let t',cs = type_consistent co d_env t1 t2 in (t',cs,e)
-and type_coerce co d_env t1 e t2 = type_coerce_internal co d_env t1 [] e t2 [];;
+and type_coerce co d_env is_explicit t1 e t2 = type_coerce_internal co d_env is_explicit t1 [] e t2 [];;
let rec conforms_to_t spec actual =
(*let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in*)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 30c0db15..2aff6db3 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -161,8 +161,9 @@ val nexp_eq : nexp -> nexp -> bool
*)
val type_consistent : constraint_origin -> def_envs -> t -> t -> t * nexp_range list
-(* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second and is inconsistent *)
-val type_coerce : constraint_origin -> def_envs -> t -> exp -> t -> t * nexp_range list * exp
+(* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second and is inconsistent,
+ bool specifices whether this has arisen from an implicit or explicit type coercion request *)
+val type_coerce : constraint_origin -> def_envs -> bool -> t -> exp -> t -> t * nexp_range list * exp
(* Merge tannots when intersection or unioning two environments. In case of default types, defer to tannot on right *)
val tannot_merge : constraint_origin -> def_envs -> tannot -> tannot -> tannot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:37:15 +0000