summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem3
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
-rw-r--r--src/lem_interp/interp_lib.lem63
-rw-r--r--src/lem_interp/printing_functions.ml2
-rw-r--r--src/pretty_print.ml12
-rw-r--r--src/test/test1.sail2
-rw-r--r--src/type_check.ml66
-rw-r--r--src/type_internal.ml71
8 files changed, 154 insertions, 67 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 50e37cf2..085e2fe2 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -334,9 +334,10 @@ val list_length : forall 'a . list 'a -> integer
let list_length l = integerFromNat (List.length l)
val taint: value -> list reg_form -> value
-let taint value regs =
+let rec taint value regs =
match value with
| V_track value rs -> V_track value (regs ++ rs)
+ | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
| _ -> V_track value regs
end
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 58a92cef..90d162e7 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -58,7 +58,7 @@ end
let integer_of_byte_list bytes =
let intv = intern_value (Bytevector bytes) in
- match Interp_lib.to_num false intv with
+ match Interp_lib.to_num Interp_lib.Unsigned intv with
| Interp.V_lit (L_aux (L_num n) _) -> n
end
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 823e358b..6c0d5b31 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -115,6 +115,8 @@ let rec bitwise_binop op (V_tuple [v1;v2]) =
| (_,V_unknown) -> V_unknown
end ;;
+type signed = Unsigned | Signed
+
(* BitSeq expects LSB first.
* By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
* hence MSB first.
@@ -123,14 +125,9 @@ let rec to_num signed v =
match v with
| (V_vector idx inc l) ->
(* Word library in Lem expects bitseq with LSB first *)
-(*TODO: Kathy think more
- We thought a reverse was needed due to above comments only in inc case.
- However, we seem to be interpresting bit vectors such that reverse is always needed
- and despite numbering MSB is on the left.
-*)
- let l = (*if inc then reverse l else l*) reverse l in
+ let l = reverse l in
(* Make sure the last bit is a zero to force unsigned numbers *)
- let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
+ let l = match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
| V_unknown -> V_unknown
| V_track v r -> taint (to_num signed v) r
@@ -166,7 +163,7 @@ let to_vec ord len n =
let rec exts (V_tuple[v1;v]) = match v1 with
| V_lit(L_aux (L_num len) _) -> (match v with
- | V_vector _ inc _ -> to_vec inc (natFromInteger len) (to_num true v)
+ | V_vector _ inc _ -> to_vec inc (natFromInteger len) (to_num Signed v)
| V_unknown -> V_unknown
| V_track v r2 -> taint (exts (V_tuple[v1;v])) r2 end)
| V_unknown -> v1
@@ -176,8 +173,8 @@ end
let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
(* XXX interpret vectors as unsigned numbers for equality *)
-let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num false v; r]) ;;
-let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num false v]) ;;
+let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num Unsigned v; r]) ;;
+let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num Unsigned v]) ;;
let rec neg v = match v with
| V_lit (L_aux arg la) ->
@@ -202,7 +199,7 @@ let rec arith_op op (V_tuple args) = match args with
end ;;
let rec arith_op_vec op size (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
- let (l1',l2') = (to_num false l1,to_num false l2) in
+ let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
let n = arith_op op (V_tuple [l1';l2']) in
to_vec ord ((List.length cs) * size) n
| [V_track v1 r1;V_track v2 r2] ->
@@ -214,6 +211,36 @@ let rec arith_op_vec op size (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
+let rec arith_op_vec_vec_range op (V_tuple args) = match args with
+ | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
+ let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+ arith_op op (V_tuple [l1';l2'])
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1;v2] ->
+ taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
+end ;;
+let rec arith_op_overflow_vec op size (V_tuple args) = match args with
+ | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
+ let (l1',l2') = (to_num Signed l1,to_num Signed l2) in
+ let n = arith_op op (V_tuple [l1';l2']) in
+ let correct_size_num = to_vec ord ((List.length cs) * size) n in
+ let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
+ let overflow = neq (V_tuple [correct_size_num;one_larger]) in
+ V_tuple [correct_size_num;overflow]
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1;v2] ->
+ taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_tuple [V_unknown;V_unknown]
+ | [_;V_unknown] -> V_tuple [V_unknown;V_unknown]
+end ;;
let rec arith_op_range_vec op size (V_tuple args) = match args with
| [V_track v1 r1;V_track v2 r2] ->
taint (arith_op_range_vec op size (V_tuple [v1;v2])) (r1++r2)
@@ -248,7 +275,7 @@ let rec arith_op_range_vec_range op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [n;(V_vector _ ord _ as l2)] ->
- arith_op op (V_tuple [n;(to_num false l2)])
+ arith_op op (V_tuple [n;(to_num Unsigned l2)])
end ;;
let rec arith_op_vec_range_range op (V_tuple args) = match args with
| [V_track v1 r1;V_track v2 r2] ->
@@ -260,7 +287,7 @@ let rec arith_op_vec_range_range op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [(V_vector _ ord _ as l1);n] ->
- arith_op op (V_tuple [(to_num false l1);n])
+ arith_op op (V_tuple [(to_num Unsigned l1);n])
end ;;
let rec compare_op op (V_tuple args) = match args with
@@ -287,7 +314,7 @@ let rec compare_op_vec op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
- let (l1',l2') = (to_num true l1, to_num true l2) in
+ let (l1',l2') = (to_num Signed l1, to_num Signed l2) in
compare_op op (V_tuple[l1';l2'])
end ;;
@@ -330,16 +357,20 @@ let function_map = [
("add_vec_range_range", arith_op_vec_range_range (+));
("add_range_vec", arith_op_range_vec (+) 1);
("add_range_vec_range", arith_op_range_vec_range (+));
+ ("add_vec_vec_range", arith_op_vec_vec_range (+));
+ ("add_overload_vec", arith_op_overflow_vec (+) 1);
("minus", arith_op (-));
("minus_vec", arith_op_vec (-) 1);
("minus_vec_range", arith_op_vec_range (-) 1);
("minus_range_vec", arith_op_range_vec (-) 1);
("minus_vec_range_range", arith_op_vec_range_range (-));
("minus_range_vec_range", arith_op_range_vec_range (-));
+ ("minus_overload_vec", arith_op_overflow_vec (-) 1);
("multiply", arith_op ( * ));
("multiply_vec", arith_op_vec ( * ) 2);
("mult_range_vec", arith_op_range_vec ( * ) 2);
("mult_vec_range", arith_op_vec_range ( * ) 2);
+ ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
("mod", arith_op (mod));
("mod_vec", arith_op_vec (mod) 1);
("mod_vec_range", arith_op_vec_range (mod) 1);
@@ -349,8 +380,8 @@ let function_map = [
("neq", neq);
("vec_concat", vec_concat);
("is_one", is_one);
- ("to_num_inc", to_num false);
- ("to_num_dec", to_num false);
+ ("to_num_inc", to_num Unsigned);
+ ("to_num_dec", to_num Unsigned);
("EXTS", exts);
("to_vec_inc", to_vec_inc);
("to_vec_dec", to_vec_dec);
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index d47a87b4..99b1f974 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -259,7 +259,7 @@ let instr_parm_to_string (name, typ, value) =
| Other,_ -> "Unrepresentable external value"
| _, Unknown0 -> "Unknown"
| _, v -> let intern_v = (Interp_inter_imp.intern_value value) in
- match Interp_lib.to_num false intern_v with
+ match Interp_lib.to_num Interp_lib.Unsigned intern_v with
| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
| _ -> val_to_string value
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 98b6f0d8..48855e64 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -241,8 +241,8 @@ let rec pp_format_t t =
| Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
| Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ args ^ "]))"
| Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
- | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
- | Toptions _ -> "(T_var \"fresh_v\" Unknown)"
+ | Tuvar(_) -> "(T_var \"fresh_v\")"
+ | Toptions _ -> "(T_var \"fresh_v\")"
and pp_format_targ = function
| TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
| TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
@@ -291,7 +291,7 @@ let pp_format_tag = function
let rec pp_format_nes nes =
"[" ^
- (*(list_format "; "
+ (list_format "; "
(fun ne -> match ne with
| LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
| Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
@@ -305,7 +305,7 @@ let rec pp_format_nes nes =
| BranchCons(_,nes_b) ->
"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"
)
- nes) ^*) "]"
+ nes) ^ "]"
let pp_format_annot = function
| NoTyp -> "Nothing"
@@ -986,11 +986,11 @@ let doc_exp, doc_let =
| LB_val_explicit(ts,pat,e) ->
prefix 2 1
(separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
- (exp e)
+ (atomic_exp e)
| LB_val_implicit(pat,e) ->
prefix 2 1
(separate space [string "let"; doc_atomic_pat pat; equals])
- (exp e)
+ (atomic_exp e)
and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e)
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 8ae00d78..8143bf5d 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -45,7 +45,7 @@ typedef colors = enumerate { red; green; blue }
let (colors) rgb = red
-function bit enu (red) = 0
+function bit enu ((colors) red) = let (one, two) = (1,2) in 0
function bit main _ = {ignore(sw(0)); ignore((nat) v2); ignore(enu(0)); v1[0] }
diff --git a/src/type_check.ml b/src/type_check.ml
index 884e90c6..0d9a245d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -558,7 +558,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
in
let coerce_parms arg_t parms expect_arg_t =
(match parms with
- | [parm] -> let _,cs,ef,parm' = type_coerce (Expr l) d_env false arg_t parm expect_arg_t in [parm'],ef,cs
+ | [parm] ->
+ let _,cs,ef,parm' = type_coerce (Expr l) d_env false arg_t parm expect_arg_t in [parm'],ef,cs
| parms ->
(match type_coerce (Expr l) d_env false arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t with
| (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs)
@@ -571,6 +572,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*)
let internal_exp = match expect_t.t,ret.t with
| Tapp("vector",_),_ ->
+ (*let _ = Printf.printf "adding internal exp on expext_t: %s %s \n" (t_to_string expect_t) (t_to_string ret) in*)
E_aux (E_internal_exp (l,Base(([],expect_t),Emp_local,[],pure_e)), (l,Base(([],nat_t),Emp_local,[],pure_e)))
| _,Tapp("vector",_) ->
E_aux (E_internal_exp (l,Base(([],ret),Emp_local,[],pure_e)), (l,Base(([],nat_t),Emp_local,[],pure_e)))
@@ -619,9 +621,13 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let args,arg_t,arg_cs,arg_ef =
(match t_p.t with
| Tfn(arg,ret,_,ef') -> check_parms arg parms
- | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+ | _ ->
+ typ_error l ("Expected a function or constructor, found identifier " ^ i
+ ^ " bound to type " ^ (t_to_string t))) in
(match (select_overload_variant d_env true overload_return variants arg_t) with
- | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+ | [] -> typ_error l
+ ("No matching function found with name " ^ i ^ " that expects parameters " ^
+ (t_to_string arg_t))
| [Base((params,t),tag,cs,ef)] ->
(match t.t with
| Tfn(arg,ret,imp,ef') ->
@@ -632,7 +638,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
| _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
| variants' ->
(match select_overload_variant d_env false true variants' expect_t with
- | [] -> typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
+ | [] ->
+ typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
| [Base((params,t),tag,cs,ef)] ->
(match t.t with
|Tfn(arg,ret,imp,ef') ->
@@ -679,36 +686,47 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let lft',rht',arg_t,arg_cs,arg_ef =
(match t_p.t with
| Tfn(arg,ret,_,ef') -> check_parms arg lft rht
- | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+ | _ -> 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 true overload_return variants arg_t) with
- | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+ | [] ->
+ 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.printf "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*)
+ (*let _ = Printf.printf "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,imp,ef') ->
(match arg.t,arg_t.t with
| Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
- let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
- let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
+ let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
+ (*let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+ let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in*)
let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
- (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,
- union_effects ef_r (union_effects ef_p (union_effects (union_effects (union_effects ef_lft ef_rght) arg_ef) ef')))
+ (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,
+ union_effects ef_r (union_effects ef_p (union_effects arg_ef ef')))
|_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type"))
| _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function"))
| variants ->
+ (*let _ = Printf.printf "Number of variants found before looking at return value %i\n%!" (List.length variants) in*)
(match (select_overload_variant d_env false true variants expect_t) with
- | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t))
+ | [] ->
+ typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^
+ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t))
| [Base((params,t),tag,cs,ef)] ->
+ (*let _ = Printf.printf "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,imp,ef') ->
(match arg.t,arg_t.t with
| Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
- let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+ let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
+ (*let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
- let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
- (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,
- union_effects ef_r (union_effects ef_p (union_effects (union_effects (union_effects ef_lft ef_rght) arg_ef) ef')))
+ *)let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
+ (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,
+ union_effects ef_r (union_effects ef_p (union_effects arg_ef ef')))
|_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type"))
| _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function"))
| _ ->
@@ -1444,17 +1462,23 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
let t,cs,ef = subst params t cs ef in
let (pat',env,cs1,u) = check_pattern envs emp_tag t pat in
let (e,t,_,cs2,ef2) = check_exp envs imp_param t e in
- let cs = resolve_constraints cs@cs1@cs2 in
+ let cs = if is_top_level then resolve_constraints cs@cs1@cs2 else cs@cs1@cs2 in
let ef = union_effects ef ef2 in
- let tannot = check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in
+ let tannot = if is_top_level
+ then check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*)
+ else (Base ((params,t),tag,cs,ef))
+ in
(LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,ef)
| NoTyp | Overload _ -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Base"))
| LB_val_implicit(pat,e) ->
let t = new_t () in
let (pat',env,cs1,u) = check_pattern envs emp_tag (new_t ()) pat in
let (e,t',_,cs2,ef) = check_exp envs imp_param u e in
- let cs = resolve_constraints cs1@cs2 in
- let tannot = check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *) in
+ let cs = if is_top_level then resolve_constraints cs1@cs2 else cs1@cs2 in
+ let tannot =
+ if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *)
+ else (Base (([],t'),emp_tag,cs,ef))
+ in
(LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,ef)
(*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
@@ -1613,7 +1637,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
List.split
(List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
- (*let _ = Printf.printf "about to check that %s and %s are consistent\n!" (t_to_string t') (t_to_string param_t) in*)
+ (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
let exp',_,_,cs_e,ef =
check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) imp_param ret_t exp in
(*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 0b0a2646..83d40e64 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -143,7 +143,7 @@ let co_to_string = function
let rec t_to_string t =
match t.t with
| Tid i -> i
- | Tvar i -> "'" ^ i
+ | Tvar i -> i
| Tfn(t1,t2,_,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e
| Ttup(tups) -> "(" ^ string_of_list ", " t_to_string tups ^ ")"
| Tapp(i,args) -> i ^ "<" ^ string_of_list ", " targ_to_string args ^ ">"
@@ -866,13 +866,25 @@ let initial_typ_env =
Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
(mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
- (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))), External (Some "add_vec"),[],pure_e);
+ (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))),
+ External (Some "add_vec"),[],pure_e);
+ Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+ mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+ (mk_range (mk_nv "q") {nexp = N2n (mk_nv "n",None)}))),
+ External (Some "add_vec_vec_range"),[],pure_e);
+
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_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";"o";"p"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+ mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+ (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")); bit_t]))),
+ External (Some "add_overload_vec"),[],pure_e);
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")])
@@ -1102,10 +1114,11 @@ let rec t_subst s_env t =
match t.t with
| Tvar i -> (match Envmap.apply s_env i with
| Some(TA_typ t1) -> t1
- | _ -> t)
+ | _ -> { t = Tvar i})
| Tuvar _ -> new_t()
- | Tid _ -> t
- | Tfn(t1,t2,imp,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(ip_subst s_env imp),(e_subst s_env e)) }
+ | Tid i -> { t = Tid i}
+ | Tfn(t1,t2,imp,e) ->
+ {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(ip_subst s_env imp),(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)}
| Tabbrev(ti,ta) -> {t = Tabbrev(t_subst s_env ti,t_subst s_env ta) }
@@ -1125,7 +1138,7 @@ and n_subst s_env n =
match n.nexp with
| Nvar i -> (match Envmap.apply s_env i with
| Some(TA_nexp n1) -> n1
- | _ -> n)
+ | _ -> { nexp = Nvar i })
| Nuvar _ -> new_n()
| Nconst _ | Npos_inf | Nneg_inf -> n
| N2n(n1,i) -> { nexp = N2n (n_subst s_env n1,i) }
@@ -1137,14 +1150,14 @@ and o_subst s_env o =
match o.order with
| Ovar i -> (match Envmap.apply s_env i with
| Some(TA_ord o1) -> o1
- | _ -> o)
+ | _ -> { order = Ovar i })
| 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)
+ | _ -> {effect = Evar i})
| Euvar _ -> new_e ()
| _ -> e
@@ -1179,9 +1192,13 @@ let subst k_env t cs e =
let rec t_remove_unifications s_env t =
match t.t with
| Tvar _ | Tid _-> s_env
- | Tuvar _ -> (match fresh_tvar s_env t with
- | Some ks -> Envmap.insert s_env ks
- | None -> s_env)
+ | Tuvar tu ->
+ (match tu.subst with
+ | None ->
+ (match fresh_tvar s_env t with
+ | Some ks -> Envmap.insert s_env ks
+ | None -> s_env)
+ | _ -> resolve_tsubst t; s_env)
| Tfn(t1,t2,_,e) -> e_remove_unifications (t_remove_unifications (t_remove_unifications s_env t1) t2) e
| Ttup(ts) -> List.fold_right (fun t s_env -> t_remove_unifications s_env t) ts s_env
| Tapp(i,args) -> List.fold_right (fun t s_env -> ta_remove_unifications s_env t) args s_env
@@ -1196,9 +1213,16 @@ and ta_remove_unifications s_env ta =
and n_remove_unifications s_env n =
match n.nexp with
| Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env
- | Nuvar _ -> (match fresh_nvar s_env n with
- | Some ks -> Envmap.insert s_env ks
- | None -> s_env)
+ | Nuvar nu ->
+ let n' = match nu.nsubst with
+ | None -> n
+ | _ -> resolve_nsubst n; n in
+ (match n.nexp with
+ | Nuvar _ ->
+ (match fresh_nvar s_env n with
+ | Some ks -> Envmap.insert s_env ks
+ | None -> s_env)
+ | _ -> s_env)
| N2n(n1,_) | Npow(n1,_) | Nneg n1 -> (n_remove_unifications s_env n1)
| Nadd(n1,n2) | Nmult(n1,n2) -> (n_remove_unifications (n_remove_unifications s_env n1) n2)
and o_remove_unifications s_env o =
@@ -1479,7 +1503,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 =
let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in
equate_t t2 t2';
(t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)])
- | t,Tuvar _ -> equate_t t2 t1; (t1,csp)
+ | t,Tuvar _ -> equate_t t2 t1; (t2,csp)
| _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2))
and type_arg_eq co d_env ta1 ta2 =
@@ -1546,6 +1570,10 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
| Oinc,Ouvar _ | Odec,Ouvar _ -> equate_o o2 o1;
| Ouvar _,Oinc | Ouvar _, Odec -> equate_o o1 o2;
| _,_ -> equate_o o1 o2);
+ (*(match r1.nexp,r2.nexp with
+ | Nuvar _,_ -> ignore(resolve_nsubst(r1)); equate_n r1 r2;
+ | _,Nuvar _ -> ignore(resolve_nsubst(r2)); equate_n r2 r1;
+ | _ -> ());*)
let cs = csp@[Eq(co,r1,r2)] in
let t',cs' = type_consistent co d_env t1i t2i in
let tannot = Base(([],t2),Emp_local,cs@cs',pure_e) in
@@ -1659,18 +1687,21 @@ and type_coerce co d_env is_explicit t1 e t2 = type_coerce_internal co d_env is_
let rec select_overload_variant d_env params_check get_all variants actual_type =
match variants with
| [] -> []
- | NoTyp::variants | Overload _::variants -> select_overload_variant d_env params_check get_all variants actual_type
- | Base((parms,t),tag,cs,ef)::variants ->
- let t,cs,ef = subst parms t cs ef in
+ | NoTyp::variants | Overload _::variants ->
+ select_overload_variant d_env params_check get_all variants actual_type
+ | Base((parms,t_orig),tag,cs,ef)::variants ->
+ (*let _ = Printf.printf "About to check a variant %s\n" (t_to_string t_orig) in*)
+ let t,cs,ef = if parms=[] then t_orig,cs,ef else subst parms t_orig cs ef in
+ (*let _ = Printf.printf "And after substitution %s\n" (t_to_string t) in*)
let t,cs' = get_abbrev d_env t in
let recur _ = select_overload_variant d_env params_check get_all variants actual_type in
(match t.t with
| Tfn(a,r,_,e) ->
- (*let _ = Printf.printf "About to check a variant\n" in*)
let is_matching =
if params_check then conforms_to_t d_env true false a actual_type
else match actual_type.t with
- | Toptions(at1,Some at2) -> (conforms_to_t d_env false true at1 r || conforms_to_t d_env false true at2 r)
+ | Toptions(at1,Some at2) ->
+ (conforms_to_t d_env false true at1 r || conforms_to_t d_env false true at2 r)
| Toptions(at1,None) -> conforms_to_t d_env false true at1 r
| _ -> conforms_to_t d_env true true actual_type r in
(*let _ = Printf.printf "Checked a variant, matching? %b\n" is_matching in*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:46:43 +0000