diff options
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 91 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 208 | ||||
| -rw-r--r-- | src/type_internal.ml | 319 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
5 files changed, 451 insertions, 172 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 60419886..49d8cbfe 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -302,7 +302,7 @@ let initial_instruction_state top_level main args = Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv (Interp.emem "istate top level") Interp.Top -type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal +type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis type interp_value_return = | Ivh_value of Interp.value | Ivh_value_after_exn of Interp.value @@ -311,6 +311,7 @@ type interp_value_return = let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk = let errk_str = match ivh_mode with | Ivh_translate -> "translate" + | Ivh_analysis -> "analysis" | Ivh_decode -> "decode" | Ivh_unsupported -> "supported_instructions" | Ivh_illegal -> "illegal instruction" end in @@ -323,15 +324,16 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev else (match ivh_mode with | Ivh_translate -> (Ivh_value value, events_out) + | Ivh_analysis -> (Ivh_value value, events_out) | _ -> (match value with | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ -> - (match ivh_mode with - | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out) - | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out) - | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out) - | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end) + (match (ivh_mode,arg) with + | (Ivh_decode, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out) + | (Ivh_illegal, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out) + | (Ivh_unsupported, _) -> (Ivh_error (Unsupported_instruction_error instr), events_out) + | _ -> Assert_extra.failwith "Reached unreachable pattern" end) | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end) | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out) | (Interp.Action (Interp.Return value) stack,_,_) -> @@ -413,7 +415,7 @@ let translate_address top_level end_flag thunk_name registers address = let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in let (address_error,events) = - interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction + interp_to_value_helper (Just (Opcode bytes)) Ivh_translate val_str ("",[],[]) internal_direction registers [] false (fun _ -> Interp.resume int_mode @@ -433,6 +435,77 @@ let translate_address top_level end_flag thunk_name registers address = | _ -> Assert_extra.failwith "Not an internal error either" end end +let value_of_instruction_param direction (name,typ,v) = + let vec = intern_ifield_value direction v in + let v = match vec with + | Interp.V_vector start dir bits -> + match typ with + | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end + | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec + | Enum _ _ -> Interp_lib.to_num Interp_lib.Unsigned vec + | _ -> vec + end + | _ -> Assert_extra.failwith "intern_ifield did not return vector" + end in v + +let intern_instruction direction (name,parms,_) = + Interp.V_ctor (Interp.id_of_string name) (T_id "ast") Interp.C_Union + (Interp.V_tuple (List.map (value_of_instruction_param direction) parms)) + +let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction = + let mode = make_mode true false end_flag in + let int_mode = mode.internal_mode in + let (Context top_env direction _ _ _ _ _ _) = top_level in + let intern_val = intern_instruction direction instruction in + let val_str = Interp.string_of_value intern_val in + let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in + let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let (analysis_or_error,events) = + interp_to_value_helper Nothing Ivh_analysis val_str ("",[],[]) internal_direction + registers [] false + (fun _ -> Interp.resume + int_mode + (Interp.Thunk_frame + (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) + (Interp_ast.Unknown, Nothing)) + top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in + match (analysis_or_error) with + | Ivh_value regs -> + (match regs with + | Interp.V_tuple [Interp.V_list regs1; Interp.V_list regs2; Interp.V_list regs3] -> + let reg_to_reg_name v = match v with + | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) -> + let (start,length,direction,_) = regn_to_reg_details n Nothing in + Reg n start length direction + | Interp.V_ctor (Id_aux (Id "RSlice") _) _ _ + (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); + Interp.V_lit (L_aux (L_num s1) _); + Interp.V_lit (L_aux (L_num s2) _);]) -> + let (start,length,direction,_) = regn_to_reg_details n Nothing in + Reg_slice n start direction (natFromInteger s1, natFromInteger s2) + (*Note, this may need to change order depending on the direction*) + | Interp.V_ctor (Id_aux (Id "RSliceBit") _) _ _ + (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); + Interp.V_lit (L_aux (L_num s) _);]) -> + let (start,length,direction,_) = regn_to_reg_details n Nothing in + Reg_slice n start direction (natFromInteger s,natFromInteger s) + | Interp.V_ctor (Id_aux (Id "RField") _) _ _ + (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); + Interp.V_lit (L_aux (L_string f) _);]) -> + let (start,length,direction,span) = regn_to_reg_details n (Just f) in + Reg_field n start direction f span + | _ -> Assert_extra.failwith "Analysis did not return an element of the specified type" end + in + let (regs1,regs2,regs3) = + (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3) in + (Just (regs1,regs2,regs3), events) + | _ -> Assert_extra.failwith "Analysis did not return a three-tuple of lists" end) + | Ivh_value_after_exn _ -> + (Nothing, events) + | Ivh_error err -> match err with + | Internal_error msg -> Assert_extra.failwith msg + | _ -> Assert_extra.failwith "Not an internal error either" end +end let rec find_instruction i = function | [] -> Nothing @@ -460,7 +533,7 @@ let decode_to_istate top_level registers value = let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in let (instr_decoded_error,events) = - interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction registers [] false + interp_to_value_helper (Just value) Ivh_decode val_str ("",[],[]) internal_direction registers [] false (fun _ -> Interp.resume mode (Interp.Thunk_frame @@ -488,7 +561,7 @@ let decode_to_istate top_level registers value = | _ -> Assert_extra.failwith "decoded instruction not a constructor" end in let (arg,_) = Interp.to_exp mode Interp.eenv instr in let (instr_decoded_error,events) = - interp_to_value_helper value Ivh_unsupported val_str instr_external internal_direction + interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction registers [] false (fun _ -> Interp.resume mode diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 99b4daf6..2da9e060 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -1154,6 +1154,10 @@ val translate_address : context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe (list event) +val instruction_analysis : + context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) + -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name) + val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = let mv = if endian = E_big_endian then mv else List.reverse mv in diff --git a/src/type_check.ml b/src/type_check.ml index 9a99cc36..eed53609 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -472,6 +472,199 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let t = {t = Tapp("list",[TA_typ u])} in (P_aux(P_list(pats'),(l,cons_tag_annot t emp_tag cs)), env,constraints@cs,bounds,t) +let rec check_pattern_after_constraint_res envs concrete_length_req expect_t (P_aux(p,(l,annot))) : t = + let check_pat = check_pattern_after_constraint_res envs in + let (Env(d_env,t_env,b_env,tp_env)) = envs in + (*let _ = Printf.eprintf "checking pattern after constraints with expected type %s\n" (t_to_string expect_t) in*) + let expect_t,_ = get_abbrev d_env expect_t in + (*let _ = Printf.eprintf "check pattern after constraints expect_t after abbrev %s\n" (t_to_string expect_t) in*) + let expect_actual = match expect_t.t with | Tabbrev(_,t) -> t | _ -> expect_t in + let t_inferred = match annot with + | Base((_,t),tag,cs,_,_,_) -> t + | _ -> failwith "Inference pass did not annotate a pattern with Base annot" in + match p with + | P_lit (L_aux(lit,l')) -> + let t_from_lit = (match lit with + | L_unit -> unit_t + | L_zero | L_one | L_true | L_false -> bit_t + | L_num i -> + (match expect_actual.t with + | Tid "bit" -> if i = 0 || i = 1 then bit_t else typ_error l' "Given number but expected bit" + | _ -> {t = Tapp("atom", [TA_nexp (mk_c_int i)])}) + | L_hex s -> + let size = big_int_of_int ((String.length s) * 4) in + let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in + mk_vector bit_t d_env.default_o (if is_inc then n_zero else mk_c (sub_big_int size one)) (mk_c size) + | L_bin s -> + let size = big_int_of_int (String.length s) in + let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in + mk_vector bit_t d_env.default_o (if is_inc then n_zero else mk_c(sub_big_int size one)) (mk_c size) + | L_string s -> string_t + | L_undef -> typ_error l' "Cannot pattern match on undefined") in + let t_c,_ = type_consistent (Patt l) d_env Require true t_from_lit t_inferred in + let t,_ = type_consistent (Patt l) d_env Require true t_c expect_t in + t + | P_wild -> + let t,_ = type_consistent (Patt l) d_env Require true t_inferred expect_t in t + | P_as(pat,id) -> check_pat concrete_length_req expect_t pat + | P_typ(typ,pat) -> + let tdec = typ_to_t envs false false typ in + let tdec = typ_subst tp_env false tdec in + let default _ = let tdec = check_pat false tdec pat in + let t,_ = type_consistent (Patt l) d_env Guarantee false tdec t_inferred in + let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in + t + in + (match tdec.t, concrete_length_req with + | Tapp ("vector", [_;TA_nexp {nexp = Nconst _};_;_]), true -> default () + | Tapp ("vector",_), true -> + (try (let tdec = check_pat true tdec pat in + let t,_ = type_consistent (Patt l) d_env Guarantee false tdec t_inferred in + let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in t) with + | Reporting_basic.Fatal_error(Reporting_basic.Err_type _) -> + typ_error l "Type annotation does not provide a concrete vector length and one cannot be inferred") + | _ -> default ()) + | P_id id -> + let i = id_to_string id in + let default t = + let t,_ = type_consistent (Patt l) d_env Guarantee false t t_inferred in + let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in t in + (match Envmap.apply t_env i with + | Some(Base((params,t),Constructor n,cs,efl,efr,bounds)) -> + let t,cs,ef,_ = subst params false false t cs efl in + (match t.t with + | Tfn({t = Tid "unit"},t',IP_none,ef) -> + if conforms_to_t d_env false false t' expect_t then default t' else default t + | Tfn(t1,t',IP_none,e) -> + if conforms_to_t d_env false false t' expect_t + then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none") + else default t' + | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type")) + | Some(Base((params,t),Enum max,cs,efl,efr,bounds)) -> + let t,cs,ef,_ = subst params false false t cs efl in default t + | _ -> (match t_inferred.t, concrete_length_req with + | Tapp ("vector", [_;TA_nexp {nexp = Nconst _};_;_]), true -> default t_inferred + | Tapp ("vector", _), true -> + typ_error l ("Unable to infer a vector length for paramter " ^ i ^ ", a type annotation may be required.") + | _ -> default t_inferred)) + | P_app(id,pats) -> + let i = id_to_string id in + (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*) + (match Envmap.apply t_env i with + | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") + | Some(Base((params,t),Constructor n,constraints,efl,efr,bounds)) -> + let t,dec_cs,_,_ = subst params false false t constraints efl in + (match t.t with + | Tid id -> if pats = [] + then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in t' + else typ_error l ("Constructor " ^ i ^ " does not expect arguments") + | Tfn(t1,t2,IP_none,ef) -> + let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in + (match pats with + | [] -> let _ = type_consistent (Patt l) d_env Guarantee false unit_t t1 in t' + | [p] -> check_pat concrete_length_req t1 p + | pats -> check_pat concrete_length_req t1 (P_aux(P_tup(pats),(l,annot)))) + | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor")) + | Some(Base((params,t),tag,constraints,efl,efr,bounds)) -> + typ_error l ("Identifier " ^ i ^ " used in pattern is not a union constructor")) + | P_record(fpats,_) -> + (match (fields_to_rec fpats d_env.rec_env) with + | None -> typ_error l ("No struct exists with the listed fields") + | Some(id,tannot,typ_pats) -> + (match tannot with + | (Base((vs,t),tag,cs,eft,_,bounds)) -> + let (ft_subst,cs,_,_) = subst vs false false t cs pure_e in + let subst_rtyp,subst_typs = + match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups + | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in + let _ = + List.map2 (fun (_,id,l,pat) styp -> check_pat concrete_length_req styp pat) typ_pats subst_typs in + let t',cs' = type_consistent (Patt l) d_env Guarantee false ft_subst expect_t in t' + | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot"))) + | P_vector pats -> + let (item_t, base, rise, ord) = match expect_actual.t with + | Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o) + | Tuvar _ -> (new_t (),new_n (),new_n(), d_env.default_o) + | _ -> typ_error l ("Expected a " ^ t_to_string expect_actual ^ " but found a vector") in + let ts = List.map (check_pat false item_t) pats in + let (u,cs) = List.fold_right (fun u (t,cs) -> + let t',cs = type_consistent (Patt l) d_env Require true u t in t',cs) ts (item_t,[]) in + let len = List.length ts in + let t = + match (ord.order,d_env.default_o.order) with + | (Oinc,_) | (Ovar _, Oinc) | (Ouvar _,Oinc) -> + {t = Tapp("vector",[TA_nexp n_zero; + TA_nexp (mk_c_int len); + TA_ord{order=Oinc}; + TA_typ u])} + | (Odec,_) | (Ovar _, Odec) | (Ouvar _,Odec) -> + {t= Tapp("vector", [TA_nexp (mk_c (if len = 0 then zero else (big_int_of_int (len -1)))); + TA_nexp (mk_c_int len); + TA_ord{order=Odec}; + TA_typ u;])} + | _ -> raise (Reporting_basic.err_unreachable l "Default order not set") in + let _,_ = type_consistent (Patt l) d_env Guarantee true t expect_t in t + | P_vector_indexed(ipats) -> + let item_t = match expect_actual.t with + | Tapp("vector",[b;r;o;TA_typ i]) -> i + | Tuvar _ -> new_t () + | _ -> typ_error l ("Expected a vector by pattern form, but a " ^ t_to_string expect_actual ^ " by type") in + let (is,pats) = List.split ipats in + let (fst,lst) = (List.hd is),(List.hd (List.rev is)) in + let inc_or_dec = + if fst < lst then + (let _ = List.fold_left + (fun i1 i2 -> if i1 < i2 then i2 + else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in + true) + else if lst < fst then + (let _ = List.fold_left + (fun i1 i2 -> if i1 > i2 then i2 + else typ_error l "Indexed vector pattern was inconsistently decreasing") fst (List.tl is) in + false) + else typ_error l "Indexed vector cannot be determined as either increasing or decreasing" in + let base,rise = new_n (), new_n () in + let ts = List.map (fun (_,pat) -> check_pat concrete_length_req item_t pat) ipats in + let co = Patt l in + let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env Require true u t) ts (item_t,[]) in + {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise); + (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} + | P_tup(pats) -> + let item_ts = match expect_actual.t with + | Ttup ts -> + if (List.length ts) = (List.length pats) + then ts + else typ_error l ("Expected a pattern with a tuple with " ^ + (string_of_int (List.length ts)) ^ " elements, found one with " ^ + (string_of_int (List.length pats))) + | Tuvar _ -> List.map (fun _ -> new_t ()) pats + | _ -> typ_error l ("Expected a tuple by pattern form, but a " ^ (t_to_string expect_actual) ^ " by type") in + let ts = List.map (fun (pat,t) -> check_pat false t pat) (List.combine pats item_ts) in + {t = Ttup ts} + | P_vector_concat pats -> + let item_t,base,rise,order = + match expect_t.t with + | Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item]) + | Tabbrev(_,{t=Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])}) -> item,b,r,o + | _ -> new_t (),new_n (), new_n (), d_env.default_o in + let vec_ti _ = {t= Tapp("vector",[TA_nexp (new_n ());TA_nexp (new_n ());TA_ord order;TA_typ item_t])} in + let _ = + let rec walk = function + | [] -> [] + | [p] -> + [check_pat concrete_length_req (*use enclosing pattern status in case of nested concats*) (vec_ti ()) p] + | p::ps -> (check_pat true (vec_ti ()) p)::(walk ps) in + walk pats in + {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord order);(TA_typ item_t)])} + | P_list(pats) -> + let item_t = match expect_actual.t with + | Tapp("list",[TA_typ i]) -> i + | Tuvar _ -> new_t () + | _ -> typ_error l ("Expected a list here by pattern form, but expected a " ^ t_to_string expect_actual ^ " by type") in + let ts = List.map (check_pat false item_t) pats in + let u = List.fold_right (fun u t -> let t',_ = type_consistent (Patt l) d_env Require true u t in t') ts item_t in + {t = Tapp("list",[TA_typ u])} + let simp_exp e l t = E_aux(e,(l,simple_annot t)) (*widen lets outer expressions control whether inner expressions should widen in the presence of literals or not. @@ -2058,7 +2251,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let (ids,_,constraints) = typq_to_params envs typq in let t = typ_to_t envs false false typ in (*TODO add check that ids == typ_params when has_spec*) - let t,constraints,_,t_param_env = subst (if has_spec then typ_params else ids) true true t constraints pure_e in + let t,constraints,_,t_param_env = + subst (if has_spec then typ_params else ids) true true t constraints pure_e in let p_t = new_t () in let ef = new_e () in t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,pure_e,nob),t_param_env in @@ -2075,10 +2269,12 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, merge_bounds b_env b_env',tp_env)) imp_param true true ret_t ret_t exp in (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in - let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" + let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" (constraints_to_string cs_p) (constraints_to_string cs_e) in*) let cs = CondCons(Fun l,cond_kind,None,cs_p,cs_e) in (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,[cs],ef,pure_e,nob)))),(cs,ef))) funcls) in + let check_pattern_after_constraints (FCL_aux ((FCL_Funcl (_, pat, _)), _)) = + check_pattern_after_constraint_res (Env(d_env,t_env,b_env,tp_env)) false param_t pat in let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = let pat' = match pat with | P_lit (L_aux (L_unit,l')) -> P_aux(P_id (Id_aux (Id var, l')), t) @@ -2091,7 +2287,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (*let _ = Printf.eprintf "Function %s is in env\n" id in*) let u,constraints,eft,t_param_env = subst_with_env t_param_env true u constraints eft in let _,cs_decs = type_consistent (Specc l) d_env Require false t u in - (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) in*) + (*let _ = Printf.eprintf "valspec consistent with type for %s, %s ~< %s with %s deriveds and %s stated\n" + id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) + (constraints_to_string (constraints@c')) in*) let imp_param = match u.t with | Tfn(_,_,IP_user n,_) -> Some n | _ -> None in @@ -2104,8 +2302,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let tannot = check_tannot l (match map with | None -> tannot | Some m -> add_map_tannot m tannot) imp_param cs' ef in (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in - let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" + let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) + let _ = List.map check_pattern_after_constraints funcls in let funcls = match imp_param with | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls | _ -> funcls @@ -2126,6 +2325,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let tannot = check_tannot l (match map with | None -> tannot | Some m -> add_map_tannot m tannot) None cs' ef in + let _ = List.map check_pattern_after_constraints funcls in (*let _ = Printf.eprintf "done funcheck case2\n" in*) (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)),b_env,tp_env) diff --git a/src/type_internal.ml b/src/type_internal.ml index c7b47831..4f232ca6 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1931,11 +1931,12 @@ let mk_pure_imp arg ret var = {t = Tfn (arg,ret,IP_length (mk_nv var),pure_e)} let lib_tannot param_typs func cs = Base(param_typs, External func, cs, pure_e, pure_e, nob) +let mk_ovar s = {order = Ovar s} let mk_range n1 n2 = {t=Tapp("range",[TA_nexp n1;TA_nexp n2])} let mk_atom n1 = {t = Tapp("atom",[TA_nexp n1])} -let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp start; TA_nexp size; TA_ord {order}; TA_typ typ])} +let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp start; TA_nexp size; TA_ord order; TA_typ typ])} let mk_bitwise_op name symb arity = - let ovar = Ovar "o" in + let ovar = mk_ovar "o" in let vec_typ = mk_vector bit_t ovar (mk_nv "n") (mk_nv "m") in let single_bit_vec_typ = mk_vector bit_t ovar (mk_nv "n") n_one in let vec_args = Array.to_list (Array.make arity vec_typ) in @@ -1959,7 +1960,7 @@ let initial_typ_env = ("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)) + (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) bit_t)) None []); ("+",Overload( lib_tannot ((mk_typ_params ["a";"b";"c"]), @@ -1970,51 +1971,51 @@ let initial_typ_env = (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))) (Some "add") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")))) (Some "add_vec") []; lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))) (Some "add_vec_vec_range") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "add_vec_range") [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) (Some "add_overflow_vec") []; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "add_vec_range_range") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "add_range_vec") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_sub (mk_2n (mk_nv "m")) n_one))))) (Some "add_range_vec_range") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")))) (Some "add_vec_bit") []; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")))) (Some "add_bit_vec") []; ])); ("+_s",Overload( @@ -2026,55 +2027,55 @@ let initial_typ_env = (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))) (Some "add_signed") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")))) (Some "add_vec_signed") []; lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))) (Some "add_vec_vec_range_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "add_vec_range_signed") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) (Some "add_overflow_vec_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "add_vec_range_range_signed") [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "add_range_vec_signed") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "add_range_vec_range_signed") [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")))) (Some "add_vec_bit_signed") []; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) (Some "add_overflow_vec_bit_signed") []; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")))) (Some "add_bit_vec_signed") []; ])); ("-_s",Overload( @@ -2086,38 +2087,38 @@ let initial_typ_env = (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))) (Some "minus") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")))) (Some "minus_vec_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "minus_vec_range_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "minus_vec_range_range_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "minus_range_vec_signed") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "minus_range_vec_range_signed") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) (Some "minus_overflow_vec_signed") []; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) (Some "minus_overflow_vec_bit_signed") []; ])); ("-",Overload( @@ -2129,42 +2130,42 @@ let initial_typ_env = (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))) (Some "minus") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")))) (Some "minus_vec") []; lib_tannot ((mk_nat_params ["m";"n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_atom (mk_nv "m")))) (Some "minus_vec_vec_range") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "minus_vec_range") []; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "minus_vec_range_range") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) (Some "minus_range_vec") []; lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) (Some "minus_range_vec_range") []; lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) (Some "minus_overflow_vec") []; lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) (Some "minus_overflow_vec_bit") []; ])); ("*",Overload( @@ -2177,19 +2178,19 @@ let initial_typ_env = (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))) (Some "multiply") []; Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "n") (mk_nv "n"))))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "n") (mk_nv "n"))))), (External (Some "multiply_vec")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), (External (Some "mult_range_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), (External (Some "mult_vec_range")),[],pure_e,pure_e,nob); ])); ("*_s",Overload( @@ -2202,24 +2203,24 @@ let initial_typ_env = (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))), (External (Some "multiply_signed")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))))), (External (Some "multiply_vec_signed")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), (External (Some "mult_range_vec_signed")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), (External (Some "mult_vec_range_signed")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))); bit_t;bit_t]))), (External (Some "mult_overflow_vec_signed")), [],pure_e,pure_e,nob); ])); @@ -2240,15 +2241,15 @@ let initial_typ_env = (External (Some "modulo")), [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_range n_one (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_vec_range")), [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_vec")),[],pure_e,pure_e,nob)])); ("mod_s", Overload( @@ -2262,15 +2263,15 @@ let initial_typ_env = (External (Some "mod_signed")), [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_range n_one (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_signed_vec_range")), [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_signed_vec")),[],pure_e,pure_e,nob)])); ("div", Base(((mk_nat_params["n";"m";"o";]), @@ -2296,15 +2297,15 @@ let initial_typ_env = (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))], pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "quot_vec")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), (External (Some "quot_overflow_vec")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], pure_e,pure_e,nob)])); @@ -2321,26 +2322,26 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")], pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")]) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "quot_vec_signed")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")]) + (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), (External (Some "quot_overflow_vec_signed")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob); ])); ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]), - (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m")) + (mk_pure_fun (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_atom (mk_nv "m")))), (External (Some "length")),[],pure_e,pure_e,nob)); (* incorrect types for typechecking processed sail code; do we care? *) ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]), - (mk_pure_imp (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m")) - (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "p") (mk_nv "o")) "o")), + (mk_pure_imp (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) + (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "p") (mk_nv "o")) "o")), (External (Some "mask")), [GtEq(Specc(Parse_ast.Int("mask",None)),Guarantee, (mk_nv "m"), (mk_nv "o"))],pure_e,pure_e,nob)); (*TODO These should be IP_start *) @@ -2364,12 +2365,12 @@ let initial_typ_env = (* == : bit['n] * [:'o:] -> bit_t *) Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), (External (Some "eq_range_vec")),[],pure_e,pure_e,nob); (* == : [:'o:] * bit['n] -> bit_t *) Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), (External (Some "eq_vec_range")),[],pure_e,pure_e,nob); @@ -2390,11 +2391,11 @@ let initial_typ_env = GtEq(Specc(Parse_ast.Int("<",None)),Guarantee, mk_nv "n", mk_nv "m"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "lt_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o"]@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), (External (Some "lt_vec_range")), [], pure_e,pure_e, nob); ])); @@ -2411,8 +2412,8 @@ let initial_typ_env = GtEq(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_nv "n", mk_nv "m"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "lt_vec_signed")),[],pure_e,pure_e,nob); ])); ("<_u", @@ -2428,8 +2429,8 @@ let initial_typ_env = GtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_nv "n", mk_nv "m"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "lt_vec_unsigned")),[],pure_e,pure_e,nob); ])); (">", @@ -2445,11 +2446,11 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "n", mk_nv "m"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "gt_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), (External (Some "gt_vec_range")), [], pure_e,pure_e, nob); ])); @@ -2466,8 +2467,8 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_nv "m"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "gt_vec_signed")),[],pure_e,pure_e,nob); ])); (">_u", @@ -2483,8 +2484,8 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int(">_u",None)),Guarantee, mk_nv "n", mk_nv "n"))], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "gt_vec_unsigned")),[],pure_e,pure_e,nob); ])); ("<=", @@ -2500,16 +2501,16 @@ let initial_typ_env = Gt(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "m"))], pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), (External (Some "lteq_vec_range")), [], pure_e,pure_e, nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), (External (Some "lteq_range_vec")), [], pure_e,pure_e, nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "lteq_vec")),[],pure_e,pure_e,nob); ])); ("<=_s", @@ -2524,8 +2525,8 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "m",mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "lteq_vec_signed")),[],pure_e,pure_e,nob); ])); (">=", @@ -2540,16 +2541,16 @@ let initial_typ_env = GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "m", mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "gteq_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), (External (Some "gteq_vec_range")), [], pure_e,pure_e, nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), + mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), (External (Some "gteq_range_vec")), [], pure_e,pure_e, nob); ])); (">=_s", @@ -2564,13 +2565,13 @@ let initial_typ_env = GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "m", mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), + (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), (External (Some "gteq_vec_signed")),[],pure_e,pure_e,nob); ])); ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),(External (Some "is_one")),[],pure_e,pure_e,nob)); ("signed",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})], - (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")) + (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_atom (mk_nv "o")))), External (Some "signed"), [(GtEq(Specc(Parse_ast.Int("signed",None)),Guarantee, @@ -2578,7 +2579,7 @@ let initial_typ_env = (LtEq(Specc(Parse_ast.Int("signed",None)),Guarantee, mk_nv "o", mk_sub (mk_2n (mk_nv "m")) n_one));],pure_e,pure_e,nob)); ("unsigned",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})], - (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")) + (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_atom (mk_nv "o")))), External (Some "unsigned"), [(GtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee, @@ -2595,40 +2596,40 @@ let initial_typ_env = Overload( Base((mk_nat_params["n";"o";"p"]@[("a",{k=K_Typ})], (mk_pure_fun (mk_tup [{t=Tvar "a"}; mk_atom (mk_nv "n")]) - (mk_vector bit_t Oinc (mk_nv "o") (mk_nv "p")))), + (mk_vector bit_t {order = Oinc} (mk_nv "o") (mk_nv "p")))), External (Some "duplicate"), [], pure_e, pure_e, nob), false, [Base((mk_nat_params ["n"], (mk_pure_fun (mk_tup [bit_t;mk_atom (mk_nv "n")]) - (mk_vector bit_t Oinc (mk_c zero) (mk_nv "n")))), + (mk_vector bit_t {order=Oinc} (mk_c zero) (mk_nv "n")))), External (Some "duplicate"),[],pure_e,pure_e,nob); Base((mk_nat_params ["n";"m";"o"]@mk_ord_params["or"], - mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_nv "m"); + mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "or") (mk_nv "o") (mk_nv "m"); mk_atom (mk_nv "n")]) - (mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_mult (mk_nv "m") (mk_nv "n")))), + (mk_vector bit_t (mk_ovar "or") (mk_nv "o") (mk_mult (mk_nv "m") (mk_nv "n")))), External (Some "duplicate_bits"),[],pure_e,pure_e,nob);])); ("<<",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); + (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); (mk_range n_zero (mk_nv "m"))]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), External (Some "bitwise_leftshift"),[],pure_e,pure_e,nob)); (">>",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); + (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); (mk_range n_zero (mk_nv "m"))]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), External (Some "bitwise_rightshift"),[],pure_e,pure_e,nob)); ("<<<",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]), - (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); + (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); (mk_range n_zero (mk_nv "m"))]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))), External (Some "bitwise_rotate"),[],pure_e,pure_e,nob)); ("EXTS",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) - (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + (mk_pure_imp (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), External (Some "exts"),[],pure_e,pure_e,nob)); ("EXTZ",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), - (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) - (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + (mk_pure_imp (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), External (Some "extz"),[],pure_e,pure_e,nob)); ("abs",Base(((mk_nat_params ["n";"m";]), (mk_pure_fun (mk_atom (mk_nv "n")) (mk_range n_zero (mk_nv "m")))), @@ -4171,7 +4172,7 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt = | Some _, None, None, None | None, Some _ , None, None | None, None, Some _ , None | None, None, None, Some _ | Some _, Some _,None,None | None,None,Some _,Some _ (*earlier check should ensure these*) -> () - | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> () (* + | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> if tri_to_bl (nexp_ge rlt glt) (*Can we guarantee the up is less than the required up*) then if tri_to_bl (nexp_ge rlt ggt) (*Can we guarantee the lw is less than the required up*) then if tri_to_bl (nexp_ge glt rgt) (*Can we guarantee the up is greater than the required lw*) @@ -4181,7 +4182,7 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt = ^ (n_to_string rgt) ^ " but best guarantee is " ^ (n_to_string ggt)) else multi_constraint_error cglt crgt ("Constraints arising from these locations guarantees a number no greather than " ^ (n_to_string glt) ^ " but requires a number greater than " ^ (n_to_string rgt)) else multi_constraint_error crlt cggt ("Constraints arising from these locations guarantees a number that is less than " ^ (n_to_string rlt) ^ " but best guarantee is " ^ (n_to_string ggt)) - else multi_constraint_error crlt cglt ("Constraints arising from these locations require no more than " ^ (n_to_string rlt) ^ " but guarantee indicates it may be above " ^ (n_to_string glt)) *) + else multi_constraint_error crlt cglt ("Constraints arising from these locations require no more than " ^ (n_to_string rlt) ^ " but guarantee indicates it may be above " ^ (n_to_string glt)) | _ -> (*let _ = Printf.eprintf "check_range_consistent is in the partial case\n" in*) () diff --git a/src/type_internal.mli b/src/type_internal.mli index 3ce674dd..b55418fe 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -150,6 +150,7 @@ val set_imp_param : nexp -> unit val mk_atom : nexp -> t val mk_tup : t list -> t +val mk_vector : t -> order -> nexp -> nexp -> t type variable_range = | VR_eq of string * nexp |