summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/constant_propagation.ml160
-rw-r--r--src/monomorphise.ml16
-rw-r--r--test/mono/pass/union-exist21
-rw-r--r--test/mono/union-exist2.sail31
4 files changed, 115 insertions, 93 deletions
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 51d079e9..608d25e1 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -110,7 +110,7 @@ let rec is_value (E_aux (e,(l,annot))) =
match e with
| E_id id -> is_constructor id
| E_lit _ -> true
- | E_tuple es -> List.for_all is_value es
+ | E_tuple es | E_vector es -> List.for_all is_value es
| E_record fes ->
List.for_all (fun (FE_aux (FE_Fexp (_, e), _)) -> is_value e) fes
| E_app (id,es) -> is_constructor id && List.for_all is_value es
@@ -655,9 +655,22 @@ let const_props defs ref_vars =
| _ -> exp
and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
- let rec check_exp_pat (E_aux (e,(l,annot))) (P_aux (p,(l',_))) =
- match e with
- | E_id id ->
+ let rec check_exp_pat (E_aux (e,(l,annot)) as exp) (P_aux (p,(l',_)) as pat) =
+ match e, p with
+ | _, P_wild -> DoesMatch ([],[])
+ | _, P_typ (_,p') -> check_exp_pat exp p'
+ | _, P_id id' when pat_id_is_variable env id' -> DoesMatch ([id',exp],[])
+ | E_tuple es, P_tup ps ->
+ let rec check = function
+ | DoesNotMatch -> fun _ -> DoesNotMatch
+ | GiveUp -> fun _ -> GiveUp
+ | DoesMatch (s,ns) ->
+ fun (e,p) ->
+ match check_exp_pat e p with
+ | DoesMatch (s',ns') -> DoesMatch (s@s', ns@ns')
+ | x -> x
+ in List.fold_left check (DoesMatch ([],[])) (List.combine es ps)
+ | E_id id, _ ->
(match Env.lookup_id id env with
| Enum _ -> begin
match p with
@@ -669,95 +682,76 @@ let const_props defs ref_vars =
"Unexpected kind of pattern for enumeration"; GiveUp)
end
| _ -> GiveUp)
- | E_lit (L_aux (lit_e, lit_l)) -> begin
- match p with
- | P_lit (L_aux (lit_p, _)) ->
- if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
- | P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) ->
- begin
- match lit_e with
- | L_num i ->
- DoesMatch ([id, E_aux (e,(l,annot))],
- [kid,Nexp_aux (Nexp_constant i,Unknown)])
- (* For undefined we fix the type-level size (because there's no good
- way to construct an undefined size), but leave the term as undefined
- to make the meaning clear. *)
- | L_undef ->
- let nexp = fabricate_nexp l annot in
- let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
- DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
- [kid,nexp])
- | _ ->
- (Reporting.print_err lit_l "Monomorphisation"
- "Unexpected kind of literal for var match"; GiveUp)
- end
- | _ ->
- (Reporting.print_err l' "Monomorphisation"
- "Unexpected kind of pattern for literal"; GiveUp)
- end
- | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> begin
- match p with
- | P_vector ps ->
- let matches = List.map2 (fun e p ->
- match e, p with
- | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) ->
- if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
- | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
- DoesMatch ([var, e],[])
- | _ -> GiveUp) es ps in
- let final = List.fold_left (fun acc m -> match acc, m with
- | _, GiveUp -> GiveUp
- | GiveUp, _ -> GiveUp
- | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub')
- | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
- (match final with
- | GiveUp ->
- (Reporting.print_err l "Monomorphisation"
- "Unexpected kind of pattern for vector literal"; GiveUp)
- | _ -> final)
- | _ ->
+ | E_lit (L_aux (lit_e, lit_l)), P_lit (L_aux (lit_p, _)) ->
+ if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
+ | E_lit (L_aux (lit_e, lit_l)),
+ P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) ->
+ begin
+ match lit_e with
+ | L_num i ->
+ DoesMatch ([id, E_aux (e,(l,annot))],
+ [kid,Nexp_aux (Nexp_constant i,Unknown)])
+ (* For undefined we fix the type-level size (because there's no good
+ way to construct an undefined size), but leave the term as undefined
+ to make the meaning clear. *)
+ | L_undef ->
+ let nexp = fabricate_nexp l annot in
+ let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
+ DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
+ [kid,nexp])
+ | _ ->
+ (Reporting.print_err lit_l "Monomorphisation"
+ "Unexpected kind of literal for var match"; GiveUp)
+ end
+ | E_lit _, _ ->
+ (Reporting.print_err l' "Monomorphisation"
+ "Unexpected kind of pattern for literal"; GiveUp)
+ | E_vector es, P_vector ps
+ when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
+ let matches = List.map2 (fun e p ->
+ match e, p with
+ | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) ->
+ if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
+ | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
+ DoesMatch ([var, e],[])
+ | _ -> GiveUp) es ps in
+ let final = List.fold_left (fun acc m -> match acc, m with
+ | _, GiveUp -> GiveUp
+ | GiveUp, _ -> GiveUp
+ | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub')
+ | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
+ (match final with
+ | GiveUp ->
(Reporting.print_err l "Monomorphisation"
"Unexpected kind of pattern for vector literal"; GiveUp)
- end
- | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) -> begin
- match p with
- | P_lit (L_aux (lit_p, _)) -> DoesNotMatch
- | P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) ->
- (* For undefined we fix the type-level size (because there's no good
- way to construct an undefined size), but leave the term as undefined
- to make the meaning clear. *)
- let nexp = fabricate_nexp l annot in
- let kids = equal_kids (env_of_annot p_id_annot) kid in
- let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
- let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in
- DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
- KBindings.bindings ksubst)
- | _ ->
+ | _ -> final)
+ | E_vector _, _ ->
+ (Reporting.print_err l "Monomorphisation"
+ "Unexpected kind of pattern for vector literal"; GiveUp)
+ | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)),
+ P_lit (L_aux (lit_p, _))
+ -> DoesNotMatch
+ | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)),
+ P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) ->
+ (* For undefined we fix the type-level size (because there's no good
+ way to construct an undefined size), but leave the term as undefined
+ to make the meaning clear. *)
+ let nexp = fabricate_nexp l annot in
+ let kids = equal_kids (env_of_annot p_id_annot) kid in
+ let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
+ let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in
+ DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
+ KBindings.bindings ksubst)
+ | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), _ ->
(Reporting.print_err l' "Monomorphisation"
"Unexpected kind of pattern for literal"; GiveUp)
- end
- | E_record _ | E_cast (_, E_aux (E_record _, _)) -> DoesNotMatch
+ | E_record _,_ | E_cast (_, E_aux (E_record _, _)),_ -> DoesNotMatch
| _ -> GiveUp
in
let check_pat = check_exp_pat exp0 in
let rec findpat_generic description assigns = function
| [] -> (Reporting.print_err l "Monomorphisation"
("Failed to find a case for " ^ description); None)
- | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
- | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
- findpat_generic description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl)
- | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx
- when pat_id_is_variable env id' ->
- Some (exp, [(id', exp0)], [])
- | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl
- when pat_id_is_variable env id' -> begin
- let substs = Bindings.add id' exp0 substs, ksubsts in
- let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in
- match guard with
- | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[])
- | E_lit (L_aux (L_false,_)) -> findpat_generic description assigns tl
- | _ -> None
- end
| (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin
match check_pat p with
| DoesNotMatch -> findpat_generic description assigns tl
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 03527ef3..0c63e020 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -165,13 +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) -> (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
@@ -196,11 +196,10 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
in insts, Typ_aux (Typ_app (id,ts),l)
| Typ_exist (kopts, nc, t) -> begin
let kid_insts, insts' = peel (kopts,insts) in
- let kopts', t' = apply_kid_insts kid_insts t in
- (* TODO: subst in nc *)
+ let kopts', nc', t' = apply_kid_insts kid_insts nc t in
match kopts' with
| [] -> insts', t'
- | _ -> insts', Typ_aux (Typ_exist (kopts', 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) =
@@ -299,7 +298,7 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
let (insts,nc') = List.fold_right find_insts kopts ([],nc) in
let insts = cross'' insts in
let ty_and_inst (inst0,ty) inst =
- let kopts, 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 kopts with
@@ -312,7 +311,6 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
(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) ->
@@ -323,9 +321,6 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
| tys ->
if contains_exist t then
cannot l "Only prenex types in unions are supported by monomorphisation" []
- else if List.length kids > 1 then
- cannot l
- "Only single-variable existential types in unions are currently supported by monomorphisation" []
else tys
end
| _ -> []
@@ -3212,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) ->
diff --git a/test/mono/pass/union-exist2 b/test/mono/pass/union-exist2
new file mode 100644
index 00000000..9852a125
--- /dev/null
+++ b/test/mono/pass/union-exist2
@@ -0,0 +1 @@
+union-exist2.sail -auto_mono
diff --git a/test/mono/union-exist2.sail b/test/mono/union-exist2.sail
new file mode 100644
index 00000000..aede3c0d
--- /dev/null
+++ b/test/mono/union-exist2.sail
@@ -0,0 +1,31 @@
+default Order dec
+$include <prelude.sail>
+
+union myunion = {
+ MyConstr : {'n 'm 'o, 'n in {8,16} & 'o in {8,16} & 'n <= 'm & 'm <= 'o. (int('n),bits('n),int('o),bits('o),int('m))}
+}
+
+val make : bits(2) -> myunion
+
+function make(v) =
+ let (n,v,m) : {'n 'm, 'n in {8,16} & 'm in {8,16} & 'n <= 'm. (int('n),bits('n),int('m))} = match v {
+ 0b00 => ( 8, 0x12, 8),
+ 0b01 => (16,0x1234,16),
+ 0b10 => ( 8, 0x56,16),
+ 0b11 => (16,0x5678,16)
+ } in
+ let w = sail_zero_extend(0x5,m) in
+ MyConstr(n,v,m,w,m)
+
+val use : myunion -> bits(32)
+
+function use(MyConstr(n,v,_,_,_)) = sail_zero_extend(v,32)
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ assert(use(make(0b00)) == 0x00000012);
+ assert(use(make(0b01)) == 0x00001234);
+ assert(use(make(0b10)) == 0x00000056);
+ assert(use(make(0b11)) == 0x00005678);
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:14:23 +0000