diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 42 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 20 |
2 files changed, 37 insertions, 25 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 7a43ca6c..993cc4f5 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -279,9 +279,8 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) = let insttys = List.map (fun x -> let (insts,tys) = List.split x in List.concat insts, Typ_aux (Typ_tup tys,l)) (cross' tys) in (kidset_bigunion vars, insttys) - | Typ_app (Id_aux (Id "vector",_), - [A_aux (A_nexp sz,_); - _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + | Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp sz,_);_]) -> (KidSet.of_list (size_nvars_nexp sz), [[],typ]) | Typ_app (_, tas) -> (KidSet.empty,[[],typ]) (* We only support sizes for bitvectors mentioned explicitly, not any buried @@ -695,7 +694,7 @@ let split_defs target all_errors splits env defs = [L_zero; L_one] | _ -> cannot ("don't know about type " ^ string_of_id id)) - | Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp len,_);_;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + | Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp len,_);_]) -> (match len with | Nexp_aux (Nexp_constant sz,_) when Big_int.greater_equal sz Big_int.zero -> let sz = Big_int.to_int sz in @@ -1211,9 +1210,8 @@ let rec sizes_of_typ (Typ_aux (t,l)) = | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs) | Typ_exist (kopts,_,typ) -> List.fold_left (fun s k -> KidSet.remove (kopt_kid k) s) (sizes_of_typ typ) kopts - | Typ_app (Id_aux (Id "vector",_), - [A_aux (A_nexp size,_); - _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + | Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp size,_);_]) -> KidSet.of_list (size_nvars_nexp size) | Typ_app (_,tas) -> kidset_bigunion (List.map sizes_of_typarg tas) @@ -1355,7 +1353,7 @@ in *) match destruct_tannot tannot with | Some (env,typ,_) -> begin match Env.base_typ_of env typ with - | Typ_aux (Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp size,_);_;_]),_) + | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) when not (is_nexp_constant size) -> begin match NexpMap.find size nexp_map with @@ -1917,12 +1915,12 @@ let mk_subrange_pattern vannot vstart vend = manage P_wild in the middle of a P_vector_concat *) let pat = P_aux (P_typ (typ_of_pat pat, pat),(Generated (pat_loc pat),empty_tannot)) in let pats = if Big_int.greater end_len Big_int.zero then - [pat;P_aux (P_typ (vector_typ (nconstant end_len) ord typ, + [pat;P_aux (P_typ (bitvector_typ (nconstant end_len) ord, P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot))] else [pat] in let pats = if Big_int.greater vstart Big_int.zero then - (P_aux (P_typ (vector_typ (nconstant vstart) ord typ, + (P_aux (P_typ (bitvector_typ (nconstant vstart) ord, P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot)))::pats else pats in @@ -2764,7 +2762,7 @@ let rec rewrite_app env typ (id,args) = match size with | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp) | _ -> match solve_unique env size with - | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp) + | Some c -> E_cast (bitvector_typ (nconstant c) order, exp) | None -> e in let rewrap e = E_aux (e, (Unknown, empty_tannot)) in @@ -2785,7 +2783,7 @@ let rec rewrite_app env typ (id,args) = let midsize = nminus size size1 in begin match solve_unique env midsize with | Some c -> - let midtyp = vector_typ (nconstant c) order bittyp in + let midtyp = bitvector_typ (nconstant c) order in E_app (append, [e1; E_aux (E_cast (midtyp, @@ -2813,7 +2811,7 @@ let rec rewrite_app env typ (id,args) = let midsize = nminus size size1 in begin match solve_unique env midsize with | Some c -> - let midtyp = vector_typ (nconstant c) order bittyp in + let midtyp = bitvector_typ (nconstant c) order in E_app (append, [e1; E_aux (E_cast (midtyp, @@ -2882,7 +2880,7 @@ let rec rewrite_app env typ (id,args) = let midsize = nminus size size1 in begin match solve_unique env midsize with | Some c -> - let midtyp = vector_typ (nconstant c) order bittyp in + let midtyp = bitvector_typ (nconstant c) order in try_cast_to_typ (E_aux (E_app (mk_id "append", [e1; @@ -2907,7 +2905,7 @@ let rec rewrite_app env typ (id,args) = let (size1,order,bittyp) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let (size2,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e2)) in let size12 = nexp_simp (nsum size1 size2) in - let tannot12 = mk_tannot env (vector_typ size12 order bittyp) no_effect in + let tannot12 = mk_tannot env (bitvector_typ size12 order) no_effect in E_app (id, [E_aux (E_app (append1, [e1; e2]), (Unknown, tannot12)); e3]) | _ -> E_app (id,args) @@ -3192,16 +3190,14 @@ let make_bitvector_cast_fns cast_name top_env env quant_kids src_typ target_typ let ps,es = List.split (List.map2 aux typs typs') in P_aux (P_typ (src_typ, P_aux (P_tup ps,(Generated src_l, src_ann))),(Generated src_l, src_ann)), E_aux (E_tuple es,(Generated tar_l, tar_ann)) - | Typ_app (Id_aux (Id "vector",_), - [A_aux (A_nexp size,_); _; - A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]), - Typ_app (Id_aux (Id "vector",_) as t_id, - [A_aux (A_nexp size',l_size'); t_ord; - A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_) as t_bit]) -> begin + | Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp size,_); _]), + Typ_app (Id_aux (Id "bitvector",_) as t_id, + [A_aux (A_nexp size',l_size'); t_ord]) -> begin match simplify_size_nexp env quant_kids size, simplify_size_nexp top_env quant_kids size' with | Some size, Some size' when Nexp.compare size size' <> 0 -> let var = fresh () in - let tar_typ' = Typ_aux (Typ_app (t_id, [A_aux (A_nexp size',l_size');t_ord;t_bit]), + let tar_typ' = Typ_aux (Typ_app (t_id, [A_aux (A_nexp size',l_size');t_ord]), tar_l) in let () = at_least_one := Some tar_typ' in P_aux (P_id var,(Generated src_l,src_ann)), @@ -3532,7 +3528,7 @@ let add_bitvector_casts (Defs defs) = let Defs cast_specs,_ = (* TODO: use default/relevant order *) let kid = mk_kid "n" in - let bitsn = vector_typ (nvar kid) dec_ord bit_typ in + let bitsn = bitvector_typ (nvar kid) dec_ord in let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) (function_typ [bitsn] bitsn no_effect) in let mkfn name = diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 836c4fbc..fe241ee7 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -364,6 +364,21 @@ let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = let replace_typ_size ctxt env (Typ_aux (t,a)) = match t with + | Typ_app (Id_aux (Id "bitvector",_) as id, [A_aux (A_nexp size,_);ord]) -> + begin + let mk_typ nexp = + Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord]),a)) + in + match Type_check.solve_unique env size with + | Some n -> mk_typ (nconstant n) + | None -> + let is_equal nexp = + prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> None + end + (* | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) -> begin let mk_typ nexp = @@ -378,6 +393,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = | nexp -> mk_typ nexp | exception Not_found -> None end + *) | _ -> None let make_printable_type ctxt env typ = @@ -454,7 +470,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) = | Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) | Typ_app (Id_aux (Id "bitvector",_), - [A_aux (A_nexp size_nexp,_)]) + [A_aux (A_nexp size_nexp,_); _]) | Typ_app (Id_aux (Id "itself",_), [A_aux (A_nexp size_nexp,_)]) -> let size_nexp = nexp_simp size_nexp in @@ -1467,7 +1483,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = (* TODO Assumes normalised, decreasing bitvector slices; however, since start indices or indexing order do not appear in Lem type annotations, this does not matter. *) - let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in + let ftyp = bitvector_typ (nconstant fsize) dec_ord in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (A_typ (mk_id_typ (mk_id tname))); |