diff options
Diffstat (limited to 'src/monomorphise.ml')
| -rw-r--r-- | src/monomorphise.ml | 187 |
1 files changed, 100 insertions, 87 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4d7119d7..0c63e020 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -165,11 +165,13 @@ let rec split_insts = function | (k,None)::t -> let l1,l2 = split_insts t in l1,k::l2 | (k,Some v)::t -> let l1,l2 = split_insts t in (k,v)::l1,l2 -let apply_kid_insts kid_insts t = +let apply_kid_insts kid_insts nc t = let kid_insts, kids' = split_insts kid_insts in - let kid_insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) kid_insts in + let kid_insts = List.map + (fun (v,i) -> (kopt_kid v,Nexp_aux (Nexp_constant i,Generated Unknown))) + kid_insts in let subst = kbindings_from_list kid_insts in - kids', subst_kids_typ subst t + kids', subst_kids_nc subst nc, subst_kids_typ subst t let rec inst_src_type insts (Typ_aux (ty,l) as typ) = match ty with @@ -193,14 +195,11 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) = args (insts,[]) in insts, Typ_aux (Typ_app (id,ts),l) | Typ_exist (kopts, nc, t) -> begin - (* TODO handle non-integer existentials *) - let kids = List.map kopt_kid kopts in - let kid_insts, insts' = peel (kids,insts) in - let kids', t' = apply_kid_insts kid_insts t in - (* TODO: subst in nc *) - match kids' with + let kid_insts, insts' = peel (kopts,insts) in + let kopts', nc', t' = apply_kid_insts kid_insts nc t in + match kopts' with | [] -> insts', t' - | _ -> insts', Typ_aux (Typ_exist (List.map (mk_kopt K_int) kids', nc, t'), l) + | _ -> insts', Typ_aux (Typ_exist (kopts', nc', t'), l) end | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) = @@ -249,19 +248,31 @@ let rec size_nvars_nexp (Nexp_aux (ne,_)) = (* Given a type for a constructor, work out which refinements we ought to produce *) (* TODO collision avoidance *) -let split_src_type id ty (TypQ_aux (q,ql)) = +let split_src_type all_errors env id ty (TypQ_aux (q,ql)) = + let cannot l msg default = + let open Reporting in + let error = Err_general (l, msg) in + match all_errors with + | None -> raise (Fatal_error error) + | Some flag -> begin + flag := false; + print_error error; + default + end + in let i = string_of_id id in (* This was originally written for the general case, but I cut it down to the more manageable prenex-form below *) - let rec size_nvars_ty (Typ_aux (ty,l) as typ) = + let rec size_nvars_ty typ = + let Typ_aux (ty,l) = Env.expand_synonyms env typ in match ty with | Typ_id _ | Typ_var _ -> (KidSet.empty,[[],typ]) | Typ_fn _ -> - raise (Reporting.err_general l ("Function type in constructor " ^ i)) + cannot l ("Function type in constructor " ^ i) (KidSet.empty,[[],typ]) | Typ_bidir _ -> - raise (Reporting.err_general l ("Mapping type in constructor " ^ i)) + cannot l ("Mapping type in constructor " ^ i) (KidSet.empty,[[],typ]) | Typ_tup ts -> let (vars,tys) = List.split (List.map size_nvars_ty ts) in let insttys = List.map (fun x -> let (insts,tys) = List.split x in @@ -275,54 +286,41 @@ let split_src_type id ty (TypQ_aux (q,ql)) = (KidSet.empty,[[],typ]) (* We only support sizes for bitvectors mentioned explicitly, not any buried inside another type *) | Typ_exist (kopts, nc, t) -> - (* TODO handle non integer existentials *) - let kids = List.map kopt_kid kopts in let (vars,tys) = size_nvars_ty t in let find_insts k (insts,nc) = let inst,nc' = - if KidSet.mem k vars then - let is,nc' = extract_set_nc l k nc in + if KidSet.mem (kopt_kid k) vars then + let is,nc' = extract_set_nc l (kopt_kid k) nc in Some is,nc' else None,nc in (k,inst)::insts,nc' in - let (insts,nc') = List.fold_right find_insts kids ([],nc) in + let (insts,nc') = List.fold_right find_insts kopts ([],nc) in let insts = cross'' insts in let ty_and_inst (inst0,ty) inst = - let kids, ty = apply_kid_insts inst ty in + let kopts, nc', ty = apply_kid_insts inst nc' ty in let ty = (* Typ_exist is not allowed an empty list of kids *) - match kids with + match kopts with | [] -> ty - | _ -> Typ_aux (Typ_exist (List.map (mk_kopt K_int) kids, nc', ty),l) + | _ -> Typ_aux (Typ_exist (kopts, nc', ty),l) in inst@inst0, ty in let tys = List.concat (List.map (fun instty -> List.map (ty_and_inst instty) insts) tys) in - let free = List.fold_left (fun vars k -> KidSet.remove k vars) vars kids in + let free = List.fold_left (fun vars k -> KidSet.remove (kopt_kid k) vars) vars kopts in (free,tys) | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" in - (* Only single-variable prenex-form for now *) let size_nvars_ty (Typ_aux (ty,l) as typ) = match ty with | Typ_exist (kids,_,t) -> begin match snd (size_nvars_ty typ) with | [] -> [] + | [[],_] -> [] | tys -> - (* One level of tuple type is stripped off by the type checker, so - add another here *) - let tys = - List.map (fun (x,ty) -> - x, match ty with - | Typ_aux (Typ_tup _,_) -> Typ_aux (Typ_tup [ty],Unknown) - | _ -> ty) tys in if contains_exist t then - raise (Reporting.err_general l - "Only prenex types in unions are supported by monomorphisation") - else if List.length kids > 1 then - raise (Reporting.err_general l - "Only single-variable existential types in unions are currently supported by monomorphisation") + cannot l "Only prenex types in unions are supported by monomorphisation" [] else tys end | _ -> [] @@ -331,19 +329,19 @@ let split_src_type id ty (TypQ_aux (q,ql)) = let variants = size_nvars_ty ty in match variants with | [] -> None - | sample::__ -> - let () = if List.length variants > size_set_limit then - raise (Reporting.err_general ql - (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^ - "bigger than limit " ^ string_of_int size_set_limit)) else () - in + | sample::_ -> + if List.length variants > size_set_limit then + cannot ql + (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^ + "bigger than limit " ^ string_of_int size_set_limit) None + else let wrap = match id with | Id_aux (Id i,l) -> (fun f -> Id_aux (Id (f i),Generated l)) | Id_aux (Operator i,l) -> (fun f -> Id_aux (Operator (f i),l)) in let name_seg = function | (_,None) -> "" - | (k,Some i) -> string_of_kid k ^ Big_int.to_string i + | (k,Some i) -> string_of_kid (kopt_kid k) ^ Big_int.to_string i in let name l i = String.concat "_" (i::(List.map name_seg l)) in Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants) @@ -385,7 +383,7 @@ let typ_of_args args = let refine_constructor refinements l env id args = match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with | (_,irefinements) -> begin - let (_,constr_ty) = Env.get_val_spec id env in + let (_,constr_ty) = Env.get_union_id id env in match constr_ty with (* A constructor should always have a single argument. *) | Typ_aux (Typ_fn ([constr_ty],_,_),_) -> begin @@ -393,11 +391,9 @@ let refine_constructor refinements l env id args = match Type_check.destruct_exist (Type_check.Env.expand_synonyms env constr_ty) with | None -> None | Some (kopts,nc,constr_ty) -> - (* TODO: Handle non-integer existentials *) - let kids = List.map kopt_kid kopts in let bindings = Type_check.unify l env (tyvars_of_typ constr_ty) constr_ty arg_ty in - let find_kid kid = try Some (KBindings.find kid bindings) with Not_found -> None in - let bindings = List.map find_kid kids in + let find_kopt kopt = try Some (KBindings.find (kopt_kid kopt) bindings) with Not_found -> None in + let bindings = List.map find_kopt kopts in let matches_refinement (mapping,_,_) = List.for_all2 (fun v (_,w) -> @@ -614,11 +610,12 @@ let apply_pat_choices choices = e_assert = rewrite_assert; e_case = rewrite_case } -let split_defs all_errors splits defs = +let split_defs all_errors splits env defs = let no_errors_happened = ref true in + let error_opt = if all_errors then Some no_errors_happened else None in let split_constructors (Defs defs) = let sc_type_union q (Tu_aux (Tu_ty_id (ty, id), l)) = - match split_src_type id ty q with + match split_src_type error_opt env id ty q with | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)]) | Some variants -> ([(id,variants)], @@ -897,12 +894,14 @@ let split_defs all_errors splits defs = begin match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with | (_,variants) -> +(* TODO: what changes to the pattern and what substitutions do we need in general? let kid,kid_annot = match args with | [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann | _ -> raise (Reporting.err_general l - "Pattern match not currently supported by monomorphisation") + ("Pattern match not currently supported by monomorphisation: " + ^ string_of_pat pat)) in let map_inst (insts,id',_) = let insts = @@ -920,6 +919,11 @@ let split_defs all_errors splits defs = P_aux (P_app (id',[P_aux (P_id (id_of_kid kid),kid_annot)]),(Generated l,tannot)), kbindings_from_list insts in +*) + let map_inst (insts,id',_) = + P_aux (P_app (id',args),(Generated l,tannot)), + KBindings.empty + in ConstrSplit (List.map map_inst variants) | exception Not_found -> NoSplit end @@ -980,7 +984,7 @@ let split_defs all_errors splits defs = | E_tuple es -> re (E_tuple (List.map map_exp es)) | E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3)) | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,map_exp e1,map_exp e2,map_exp e3,ord,map_exp e4)) - | E_loop (loop,e1,e2) -> re (E_loop (loop,map_exp e1,map_exp e2)) + | E_loop (loop,m,e1,e2) -> re (E_loop (loop,m,map_exp e1,map_exp e2)) | E_vector es -> re (E_vector (List.map map_exp es)) | E_vector_access (e1,e2) -> re (E_vector_access (map_exp e1,map_exp e2)) | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (map_exp e1,map_exp e2,map_exp e3)) @@ -1007,9 +1011,9 @@ let split_defs all_errors 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 + let nosplit = lazy [Pat_aux (Pat_exp (p,map_exp e),l)] in (match map_pat p with - | NoSplit -> nosplit + | NoSplit -> Lazy.force nosplit | VarSplit patsubsts -> if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> @@ -1020,7 +1024,7 @@ let split_defs all_errors splits defs = let exp' = stop_at_false_assertions exp' in Pat_aux (Pat_exp (pat', map_exp exp'),l)) patsubsts - else nosplit + else Lazy.force nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in @@ -1028,9 +1032,9 @@ let split_defs all_errors 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 + let nosplit = lazy [Pat_aux (Pat_when (p,map_exp e1,map_exp e2),l)] in (match map_pat p with - | NoSplit -> nosplit + | NoSplit -> Lazy.force nosplit | VarSplit patsubsts -> if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> @@ -1044,7 +1048,7 @@ let split_defs all_errors splits defs = let exp2' = stop_at_false_assertions exp2' in Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) patsubsts - else nosplit + else Lazy.force nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in @@ -1115,10 +1119,14 @@ let split_defs all_errors splits defs = | DEF_internal_mutrec _ -> [d] | DEF_fundef fd -> [DEF_fundef (map_fundef fd)] - | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now" + | DEF_mapdef (MD_aux (_, (l, _))) -> + Reporting.unreachable l __POS__ "mappings should be gone by now" | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)] + | DEF_loop_measures (id,_) -> + Reporting.unreachable (id_loc id) __POS__ + "Loop termination measures should have been rewritten before now" in Defs (List.concat (List.map map_def defs)) in @@ -2065,7 +2073,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let d3,a3,r3 = analyse_exp fn_id env assigns e3 in let assigns = add_dep_to_assigned d1 (dep_bindings_merge a2 a3) [e2;e3] in (dmerge d1 (dmerge d2 d3), assigns, merge r1 (merge r2 r3)) - | E_loop (_,e1,e2) -> + | E_loop (_,_,e1,e2) -> (* We remove all of the variables assigned in the loop, so we don't need to add control dependencies *) let assigns = remove_assigns [e1;e2] " assigned in a loop" in @@ -2207,30 +2215,34 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = (List.fold_left (fun tenv kopt -> Env.add_typ_var l kopt tenv) tenv kopts), typ in - if is_bitvector_typ typ then - let size,_,_ = vector_typ_args_of typ in - let Nexp_aux (size,_) as size_nexp = simplify_size_nexp env tenv size in - let is_tyvar_parameter v = - List.exists (fun k -> Kid.compare k v == 0) env.top_kids - in - match size with - | Nexp_constant _ -> r - | Nexp_var v when is_tyvar_parameter v -> - { r with kid_in_caller = CallerKidSet.add (fn_id,v) r.kid_in_caller } - | _ -> - match deps_of_nexp l env.kid_deps [] size_nexp with - | Have (args,extras) -> - { r with - split = ArgSplits.merge merge_detail r.split args; - extra_splits = merge_extras r.extra_splits extras - } - | Unknown (l,msg) -> - { r with - failures = - Failures.add l (StringSet.singleton ("Unable to monomorphise " ^ string_of_nexp size_nexp ^ ": " ^ msg)) - r.failures } - else - r + let rec check_typ typ = + if is_bitvector_typ typ then + let size,_,_ = vector_typ_args_of typ in + let Nexp_aux (size,_) as size_nexp = simplify_size_nexp env tenv size in + let is_tyvar_parameter v = + List.exists (fun k -> Kid.compare k v == 0) env.top_kids + in + match size with + | Nexp_constant _ -> r + | Nexp_var v when is_tyvar_parameter v -> + { r with kid_in_caller = CallerKidSet.add (fn_id,v) r.kid_in_caller } + | _ -> + match deps_of_nexp l env.kid_deps [] size_nexp with + | Have (args,extras) -> + { r with + split = ArgSplits.merge merge_detail r.split args; + extra_splits = merge_extras r.extra_splits extras + } + | Unknown (l,msg) -> + { r with + failures = + Failures.add l (StringSet.singleton ("Unable to monomorphise " ^ string_of_nexp size_nexp ^ ": " ^ msg)) + r.failures } + else match typ with + | Typ_aux (Typ_tup typs,_) -> + List.fold_left (fun r ty -> merge r (check_typ ty)) r typs + | _ -> r + in check_typ typ in (deps, assigns, r) @@ -3178,6 +3190,7 @@ let make_bitvector_env_casts env quant_kids (kid,i) exp = if mut = Immutable then mk_cast var typ exp else exp) locals exp let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = + if alpha_equivalent cast_env typ target_typ then exp else let infer_arg_typ env f l typ = let (typq, ctor_typ) = Env.get_union_id f env in let quants = quant_items typq in @@ -3194,6 +3207,7 @@ let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = in (* Push the cast down, including through constructors *) let rec aux exp (typ, target_typ) = + if alpha_equivalent cast_env typ target_typ then exp else let exp_env = env_of exp in match exp with | E_aux (E_let (lb,exp'),ann) -> @@ -3383,9 +3397,8 @@ let add_bitvector_casts (Defs defs) = let bitsn = vector_typ (nvar kid) dec_ord bit_typ in let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) (function_typ [bitsn] bitsn no_effect) in - let extfn _ = Some "zeroExtend" in let mkfn name = - mk_val_spec (VS_val_spec (ts,name,extfn,false)) + mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false)) in let defs = List.map mkfn (IdSet.elements !specs_required) in check Env.empty (Defs defs) @@ -3650,7 +3663,7 @@ let monomorphise opts splits defs = then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") in - let ok_split, defs = split_defs opts.all_split_errors splits defs in + let ok_split, defs = split_defs opts.all_split_errors splits env defs in let () = if (ok_analysis && ok_extras && ok_split) || opts.continue_anyway then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") |