diff options
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 9 | ||||
| -rw-r--r-- | src/type_check.ml | 9 | ||||
| -rw-r--r-- | src/type_internal.ml | 20 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
4 files changed, 28 insertions, 11 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 674991a5..c1267fc6 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -125,6 +125,14 @@ let is_one v = | V_unknown -> v end ;; +let rec most_significant v = + retaint v + match detaint v with + | V_vector _ _ (v::vs) -> v + | V_vector_sparse _ _ _ _ _ -> most_significant (fill_in_sparse v) + | V_unknown -> V_unknown +end;; + let lt_range (V_tuple[v1;v2]) = let lr_helper v1 v2 = match (v1,v2) with | (V_lit (L_aux (L_num l1) lr),V_lit (L_aux (L_num l2) ll)) -> @@ -737,6 +745,7 @@ let library_functions direction = [ ("gtu", compare_op_vec_unsigned (>)); ("duplicate", duplicate direction); ("mask", mask direction); + ("most_significant", most_significant); ] ;; let eval_external name v = match List.lookup name (library_functions IInc) with diff --git a/src/type_check.ml b/src/type_check.ml index 0971bc29..b9fd37ff 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -525,9 +525,10 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux( let t',cs' = type_consistent (Expr l) d_env Require false t' expect_t' in (rebuild tannot,t,t_env,cs@cs',bounds,ef) | Tapp("register",[TA_typ(t')]),Tuvar _ -> - let ef' = add_effect (BE_aux(BE_rreg,l)) ef in - let tannot = Base(([],t),(if is_alias then tag else External (Some i)),cs,ef',ef',bounds) in - let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in + (*let ef' = add_effect (BE_aux(BE_rreg,l)) ef in + let tannot = Base(([],t),(if is_alias then tag else External (Some i)),cs,ef',ef',bounds) in*) + let tannot = Base(([],t),(if is_alias then tag else Emp_global),cs,pure_e,pure_e,bounds) in + let _,cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in (e',t,t_env,cs@cs',bounds,ef') | Tapp("register",[TA_typ(t')]),_ -> let ef' = add_effect (BE_aux(BE_rreg,l)) ef in @@ -683,7 +684,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux( type_coerce (Expr l) d_env Require false false b_env ret (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t | (IP_none,_) -> - (*let _ = Printf.printf "no implicit length or var required\n" in*) + (*let _ = Printf.eprintf "no implicit length or var required: ret %s and expect_t %s\n" (t_to_string ret) (t_to_string expect_t) in*) type_coerce (Expr l) d_env Require false false b_env ret (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t in diff --git a/src/type_internal.ml b/src/type_internal.ml index 22e79de8..9d43d99c 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1437,6 +1437,7 @@ let tag_annot_efr t tag efr = Base(([],t),tag,[],pure_e,efr,nob) let constrained_annot t cs = Base(([],t),Emp_local,cs,pure_e,pure_e,nob) let constrained_annot_efr t cs efr = Base(([],t),Emp_local,cs,pure_e,efr,nob) let cons_tag_annot t tag cs = Base(([],t),tag,cs,pure_e,pure_e,nob) +let cons_tag_annot_efr t tag cs efr = Base(([],t),tag,cs,pure_e,efr,nob) let cons_efl_annot t cs ef = Base(([],t),Emp_local,cs,ef,pure_e,nob) let cons_efs_annot t cs efl efr = Base(([],t),Emp_local,cs,efl,efr,nob) let efs_annot t efl efr = Base(([],t),Emp_local,[],efl,efr,nob) @@ -1483,7 +1484,7 @@ let mk_bitwise_op name symb arity = (symb, Overload(lib_tannot ((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}) (Some name) [], true, [lib_tannot ((mk_nat_params ["n";"m"]@mk_ord_params["o"]), mk_pure_fun varg vec_typ) (Some name) []; - lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg bit_t) (Some (name ^ "_range_bit")) []; + (*lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg single_bit_vec_typ) (Some name) [];*) lib_tannot ([],mk_pure_fun barg bit_t) (Some (name ^ "_bit")) []])) let initial_typ_env = @@ -1493,6 +1494,9 @@ let initial_typ_env = Constructor 2,[],pure_e,pure_e,nob)); ("None", Base((["a", {k=K_Typ}], mk_pure_fun unit_t {t=Tapp("option", [TA_typ {t=Tvar "a"}])}), Constructor 2,[],pure_e,pure_e,nob)); + ("most_significant", lib_tannot ((mk_nat_params ["n";"m"]@(mk_ord_params ["ord"])), + (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")) bit_t)) + None []); ("+",Overload( lib_tannot ((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) (Some "add") [], @@ -2591,8 +2595,8 @@ let merge_bounds b1 b2 = Bounds ((merge b1s b2s),merged_map) let rec conforms_to_t d_env loosely within_coercion spec actual = -(*let _ = Printf.printf "conforms_to_t called, evaluated loosely? %b, with %s and %s\n" - loosely (t_to_string spec) (t_to_string actual) in*) + (*let _ = Printf.eprintf "conforms_to_t called, evaluated loosely? %b & within_coercion? %b, with spec %s and actual %s\n" + within_coercion loosely (t_to_string spec) (t_to_string actual) in*) let spec,_ = get_abbrev d_env spec in let actual,_ = get_abbrev d_env actual in match (spec.t,actual.t,loosely) with @@ -2621,6 +2625,9 @@ let rec conforms_to_t d_env loosely within_coercion spec actual = (is = ia) (List.length tas = List.length taa) in*) (is = ia) && (List.length tas = List.length taa) && (List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas taa) + | (Tid "bit", Tapp("vector",[_;_;_;TA_typ ti]), _) -> + within_coercion && + conforms_to_t d_env loosely within_coercion spec ti | (Tabbrev(_,s),a,_) -> conforms_to_t d_env loosely within_coercion s actual | (s,Tabbrev(_,a),_) -> conforms_to_t d_env loosely within_coercion spec a | (_,_,_) -> false @@ -2891,11 +2898,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded")) | _,_,_ -> let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e)) - | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") -> + | Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") -> let cs = [Eq(co,r1,n_one)] in - (t2,cs,pure_e,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num (int_of_big_int i),l)), - (l,simple_annot {t=Tapp("atom",[TA_nexp b1])}))))), - (l,constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))))) + (t2,cs,pure_e,E_aux((E_app ((Id_aux (Id "most_significant", l)), [e])), + (l, cons_tag_annot_efr t2 (External (Some "most_significant")) cs (get_cummulative_effects (get_eannot e))))) | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) -> let t',cs'= type_consistent co d_env enforce false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in (t2,cs',pure_e, diff --git a/src/type_internal.mli b/src/type_internal.mli index 1748f0a7..23324ab5 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -219,6 +219,7 @@ val tag_annot_efr : t -> tag -> effect -> tannot val constrained_annot : t -> nexp_range list -> tannot val constrained_annot_efr : t -> nexp_range list -> effect -> tannot val cons_tag_annot : t -> tag -> nexp_range list -> tannot +val cons_tag_annot_efr : t -> tag -> nexp_range list -> effect -> tannot val cons_efl_annot : t -> nexp_range list -> effect -> tannot val cons_efs_annot : t -> nexp_range list -> effect -> effect -> tannot val efs_annot : t -> effect -> effect -> tannot |