diff options
Diffstat (limited to 'src/monomorphise.ml')
| -rw-r--r-- | src/monomorphise.ml | 80 |
1 files changed, 54 insertions, 26 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4fa5d1d6..3ea156d0 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -54,8 +54,7 @@ open Ast_util module Big_int = Nat_big_num open Type_check -let size_set_limit = 8 -let vector_split_limit = 4 +let size_set_limit = 16 let optmap v f = match v with @@ -1316,14 +1315,10 @@ let split_defs continue_anyway splits defs = | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with | Nexp_aux (Nexp_constant sz,_) -> - if Big_int.to_int sz <= vector_split_limit then - let lits = make_vectors (Big_int.to_int sz) in - List.map (fun lit -> - P_aux (P_lit lit,(l,annot)), - [var,E_aux (E_lit lit,(new_l,annot))]) lits - else - cannot ("Refusing to split vector type of length " ^ Big_int.to_string sz ^ - " (above limit " ^ string_of_int vector_split_limit ^ ")") + let lits = make_vectors (Big_int.to_int sz) in + List.map (fun lit -> + P_aux (P_lit lit,(l,annot)), + [var,E_aux (E_lit lit,(new_l,annot))]) lits | _ -> cannot ("length not constant, " ^ string_of_nexp len) ) @@ -1494,6 +1489,19 @@ let split_defs continue_anyway splits defs = in p in + let check_split_size lst l = + let size = List.length lst in + if size > size_set_limit then + let open Reporting_basic in + let error = + Err_general (l, "Case split is too large (" ^ string_of_int size ^ + " > limit " ^ string_of_int size_set_limit ^ ")") + in if continue_anyway + then (print_error error; false) + else raise (Fatal_error error) + else true + in + let rec map_exp ((E_aux (e,annot)) as ea) = let re e = E_aux (e,annot) in match e with @@ -1556,13 +1564,16 @@ let split_defs continue_anyway splits defs = FE_aux (FE_Fexp (id,map_exp e),annot) and map_pexp = function | Pat_aux (Pat_exp (p,e),l) -> + let nosplit = [Pat_aux (Pat_exp (p,map_exp e),l)] in (match map_pat p with - | NoSplit -> [Pat_aux (Pat_exp (p,map_exp e),l)] + | NoSplit -> nosplit | VarSplit patsubsts -> - List.map (fun (pat',substs) -> - let exp' = subst_exp substs e in - Pat_aux (Pat_exp (pat', map_exp exp'),l)) - patsubsts + if check_split_size patsubsts (pat_loc p) then + List.map (fun (pat',substs) -> + let exp' = subst_exp substs e in + Pat_aux (Pat_exp (pat', map_exp exp'),l)) + patsubsts + else nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = nexp_subst_pat nsubst pat' in @@ -1570,14 +1581,17 @@ let split_defs continue_anyway splits defs = Pat_aux (Pat_exp (pat', map_exp exp'),l) ) patnsubsts) | Pat_aux (Pat_when (p,e1,e2),l) -> + let nosplit = [Pat_aux (Pat_when (p,map_exp e1,map_exp e2),l)] in (match map_pat p with - | NoSplit -> [Pat_aux (Pat_when (p,map_exp e1,map_exp e2),l)] + | NoSplit -> nosplit | VarSplit patsubsts -> - List.map (fun (pat',substs) -> - let exp1' = subst_exp substs e1 in - let exp2' = subst_exp substs e2 in - Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) - patsubsts + if check_split_size patsubsts (pat_loc p) then + List.map (fun (pat',substs) -> + let exp1' = subst_exp substs e1 in + let exp2' = subst_exp substs e2 in + Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) + patsubsts + else nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = nexp_subst_pat nsubst pat' in @@ -1770,6 +1784,10 @@ let rewrite_size_parameters env (Defs defs) = { (compute_exp_alg KidSet.empty KidSet.union) with e_aux = (fun ((s,e),annot) -> KidSet.union s (sizes_of_annot annot), E_aux (e,annot)); e_let = (fun ((sl,lb),(s2,e2)) -> KidSet.union sl (KidSet.diff s2 (tyvars_bound_in_lb lb)), E_let (lb,e2)); + e_for = (fun (id,(s1,e1),(s2,e2),(s3,e3),ord,(s4,e4)) -> + let kid = mk_kid ("loop_" ^ string_of_id id) in + KidSet.union s1 (KidSet.union s2 (KidSet.union s3 (KidSet.remove kid s4))), + E_for (id,e1,e2,e3,ord,e4)); pat_exp = (fun ((sp,pat),(s,e)) -> KidSet.diff s (tyvars_bound_in_pat pat), Pat_exp (pat,e))} pexp) in @@ -1786,7 +1804,7 @@ let rewrite_size_parameters env (Defs defs) = | P_aux (P_tup ps,_) -> ps | _ -> [pat] in - let to_change = List.map + let to_change = Util.map_filter (fun kid -> let check (P_aux (_,(_,Some (env,typ,_)))) = match Env.expand_synonyms env typ with @@ -1799,9 +1817,10 @@ let rewrite_size_parameters env (Defs defs) = if Kid.compare kid kid' = 0 then Some kid else None | _ -> None in match findi check parameters with - | None -> raise (Reporting_basic.err_general l - ("Unable to find an argument for " ^ string_of_kid kid)) - | Some i -> i) + | None -> (Reporting_basic.print_error (Reporting_basic.Err_general (l, + ("Unable to find an argument for " ^ string_of_kid kid))); + None) + | Some i -> Some i) (KidSet.elements expose_tyvars) in let ik_compare (i,k) (i',k') = @@ -1858,7 +1877,7 @@ let rewrite_size_parameters env (Defs defs) = let body = List.fold_left add_var_rebind body vars in let guard = match guard with | None -> None - | Some exp -> Some (List.fold_left add_var_rebind body vars) + | Some exp -> Some (List.fold_left add_var_rebind exp vars) in pat,guard,body | exception Not_found -> pat,guard,body @@ -2752,6 +2771,15 @@ let rewrite_app env typ (id,args) = | _ -> E_app (id,args) + else if is_id env (Id "UInt") id then + let is_slice = is_id env (Id "slice") in + match args with + | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] + when is_slice slice1 && not (is_constant length1) -> + E_app (mk_id "UInt_slice", [vector1; start1; length1]) + + | _ -> E_app (id,args) + else E_app (id,args) let rewrite_aux = function |