Skip to content

Commit

Permalink
Add undiscriminated union type.
Browse files Browse the repository at this point in the history
Reduction for records and monotypes only.
Currently not supported at all in unification algo.
  • Loading branch information
skaller committed Jul 18, 2022
1 parent 2ddac46 commit 4e13dab
Show file tree
Hide file tree
Showing 19 changed files with 133 additions and 18 deletions.
1 change: 1 addition & 0 deletions src/compiler/flx_bind/flx_bind_type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,7 @@ print_endline ("Flx_bind_type. structural mode: TYP_typeof fixpoint metatype hac
| `TYP_compacttuple ts -> btyp_compacttuple (List.map bt ts)
| `TYP_tuple ts -> btyp_tuple (List.map bt ts)
| `TYP_intersect ts -> btyp_intersect (List.map bt ts)
| `TYP_union ts -> btyp_union (List.map bt ts)
| `TYP_tuple_cons (_,t1,t2) -> btyp_tuple_cons (bt t1) (bt t2)
| `TYP_tuple_snoc (_,t1,t2) -> btyp_tuple_snoc (bt t1) (bt t2)
| `TYP_unitsum k ->
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_bind/flx_guess_meta_type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,7 @@ print_endline (" ** BOUND mata type is " ^ Flx_kind.sk bmt);
| `TYP_callback _
| `TYP_patvar _
| `TYP_intersect _
| `TYP_union _
| `TYP_tuple _
| `TYP_sum _
| `TYP_compactsum _
Expand Down
7 changes: 4 additions & 3 deletions src/compiler/flx_core/flx_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -94,11 +94,12 @@ and typecode_t = [
| `TYP_patvar of Flx_srcref.t * Flx_id.t
| `TYP_patany of Flx_srcref.t
| `TYP_tuple of typecode_t list (** product type *)
| `TYP_intersect of typecode_t list (** intersection type *)
| `TYP_compacttuple of typecode_t list (** product type *)
| `TYP_intersect of typecode_t list (** intersection type *)
| `TYP_union of typecode_t list (** union type *)
| `TYP_compacttuple of typecode_t list (** product type *)
| `TYP_unitsum of int (** sum of units *)
| `TYP_sum of typecode_t list (** numbered sum type *)
| `TYP_compactsum of typecode_t list (** numbered sum type *)
| `TYP_compactsum of typecode_t list (** numbered sum type *)
| `TYP_record of (Flx_id.t * typecode_t) list
| `TYP_polyrecord of (Flx_id.t * typecode_t) list * Flx_id.t * typecode_t
| `TYP_variant of variant_item_t list (** anon sum *)
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_beta.ml
Original file line number Diff line number Diff line change
Expand Up @@ -396,6 +396,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
| BTYP_sum ls -> btyp_sum (List.map br ls)

| BTYP_intersect ls -> Flx_intersect.intersect bsym_table counter br ls
| BTYP_union ls -> Flx_intersect.union bsym_table counter br ls
| BTYP_record (ts) ->
let ss,ls = List.split ts in
btyp_record (List.combine ss (List.map br ls))
Expand Down
36 changes: 26 additions & 10 deletions src/compiler/flx_core/flx_btype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ and t =
| BTYP_finst of bid_t * kind list * kind * kind (* type function instance with kind args, domain, codomain kinds *)
| BTYP_vinst of bid_t * t list * Flx_kind.kind
| BTYP_intersect of t list
| BTYP_union of t list
| BTYP_tuple of t list
| BTYP_compacttuple of t list
| BTYP_array of t * t
Expand Down Expand Up @@ -132,6 +133,7 @@ let flat_iter
let unitrep = BTYP_tuple [] in
for i = 1 to k do f_btype unitrep done
| BTYP_intersect ts -> List.iter f_btype ts
| BTYP_union ts -> List.iter f_btype ts
| BTYP_inst (it, i,ts,mt) -> f_bid i; List.iter f_btype ts
| BTYP_finst (i,ks,dom, cod) -> f_bid i (* no iteration of kinds yet *)
| BTYP_vinst (i,ts,mt) -> f_bid i; List.iter f_btype ts
Expand Down Expand Up @@ -293,6 +295,7 @@ and str_of_btype typ =
| BTYP_vinst (i,ts,mt) -> "BTYP_vinst("^string_of_int i^"["^ss ts^"]:"^Flx_kind.sk mt^")"
| BTYP_tuple ts -> "BTYP_tuple(" ^ ss ts ^ ")"
| BTYP_intersect ts -> "BTYP_intersect(" ^ ss ts ^ ")"
| BTYP_union ts -> "BTYP_union(" ^ ss ts ^ ")"
| BTYP_compacttuple ts -> "BTYP_compacttuple(" ^ ss ts ^ ")"
| BTYP_array (b,x) -> "BTYP_array(" ^ s b ^"," ^s x^")"
| BTYP_compactarray (b,x) -> "BTYP_compactarray(" ^ s b ^"," ^s x^")"
Expand Down Expand Up @@ -513,14 +516,35 @@ let rec flatten_intersections (ts:t list): t list =
[]
ts

let rec flatten_unions (ts:t list): t list =
List.fold_left (fun acc t ->
match t with
| BTYP_union ts -> acc @ flatten_unions ts
| x -> acc @ [x]
)
[]
ts

let btyp_any () =
BTYP_fix (0, kind_type)

let contains_void ts = List.fold_left (fun acc t -> match t with | BTYP_void -> true | _ -> acc) false ts
let contains_any ts = List.fold_left (fun acc t -> match t with | BTYP_fix (0,_) -> true | _ -> acc) false ts

let btyp_union ts =
let ts = flatten_unions ts in
if contains_any ts then btyp_any () else
match ts with
| [] -> BTYP_void (* bottom type *)
| [x] -> x
| _ -> BTYP_union ts


(* pre-condition: no term contains a nested intersect
post-condition: an intersect of at least two non-unit non-intersect non-void terms
or a single non-intersect term
or void
*)

let btyp_intersect ts =
let ts = flatten_intersections ts in
if contains_void ts then BTYP_void else
Expand All @@ -547,9 +571,6 @@ let btyp_unit () =
let btyp_bool () =
BTYP_unitsum 2

let btyp_any () =
BTYP_fix (0, kind_type)

(** Construct a BTYP_unitsum type. *)
let btyp_unitsum n =
match n with
Expand Down Expand Up @@ -674,12 +695,6 @@ let btyp_tuple ts =
with Not_found ->
BTYP_tuple ts

(*
let btyp_tuple ts =
let tss = expand_list_with_intersections ts in
btyp_intersect (List.map btyp_tuple' tss)
*)

let btyp_compacttuple ts =
match ts with
| [] -> btyp_unit ()
Expand Down Expand Up @@ -1054,6 +1069,7 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) ?(f_kind=fun k->k) = funct
| BTYP_finst (i,ks,dom,cod) -> btyp_finst (f_bid i, List.map f_kind ks, f_kind dom, f_kind cod)
| BTYP_vinst (i,ts,mt) -> btyp_vinst (f_bid i, List.map f_btype ts,f_kind mt)
| BTYP_intersect ts -> btyp_intersect (List.map f_btype ts)
| BTYP_union ts -> btyp_union (List.map f_btype ts)
| BTYP_tuple ts -> btyp_tuple (List.map f_btype ts)
| BTYP_compacttuple ts -> btyp_compacttuple (List.map f_btype ts)
| BTYP_array (t1,t2) -> btyp_array (f_btype t1, f_btype t2)
Expand Down
2 changes: 2 additions & 0 deletions src/compiler/flx_core/flx_btype.mli
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ and t = private
| BTYP_finst of bid_t * kind list * kind * kind (* type function instance with kind args, domain, codomain kinds *)
| BTYP_vinst of bid_t * t list * Flx_kind.kind
| BTYP_intersect of t list
| BTYP_union of t list
| BTYP_tuple of t list
| BTYP_compacttuple of t list
| BTYP_array of t * t
Expand Down Expand Up @@ -139,6 +140,7 @@ val btyp_inst : instkind_t * bid_t * t list * kind -> t
val btyp_finst : bid_t * kind list * kind * kind -> t
val btyp_vinst : bid_t * t list * kind -> t
val btyp_intersect : t list -> t
val btyp_union : t list -> t
val btyp_tuple : t list -> t
val btyp_compacttuple : t list -> t
val btyp_rev : t -> t
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_btype_kind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,7 @@ print_endline ("Flx_btype_kind.metatype' case type_apply: " ^ Flx_btype.st typ);
| BTYP_label

| BTYP_intersect _
| BTYP_union _
| BTYP_polyrecord (_, _, _)
| BTYP_tuple_cons (_, _)
| BTYP_tuple_snoc (_, _)
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_btype_occurs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ let var_occurs bsym_table t =
| BTYP_vinst (_,ls,_)
| BTYP_compacttuple ls
| BTYP_intersect ls
| BTYP_union ls
| BTYP_tuple ls -> List.iter aux ls

| BTYP_record (ls) -> List.iter (fun (s,t) -> aux t) ls
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_btype_rec.ml
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ let fix i t =
| BTYP_vinst (k,ts,mt) -> btyp_vinst (k, List.map aux ts,mt)
| BTYP_tuple ts -> btyp_tuple (List.map aux ts)
| BTYP_intersect ts -> btyp_intersect (List.map aux ts)
| BTYP_union ts -> btyp_union (List.map aux ts)
| BTYP_compacttuple ts -> btyp_compacttuple (List.map aux ts)
| BTYP_sum ts -> btyp_sum (List.map aux ts)
| BTYP_compactsum ts -> btyp_compactsum (List.map aux ts)
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_fold.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ let fold (bsym_table: Flx_bsym_table.t) counter t =
| BTYP_compacttuple ls
| BTYP_tuple ls -> List.iter ax ls
| BTYP_intersect ls -> List.iter ax ls
| BTYP_union ls -> List.iter ax ls
| BTYP_record (ls) -> List.iter (fun (s,t) -> ax t) ls
| BTYP_polyrecord (ls,s,v) -> List.iter (fun (s,t) -> ax t) ls; ax v
| BTYP_variant ls -> List.iter (fun (s,t) -> ax t) ls
Expand Down
69 changes: 68 additions & 1 deletion src/compiler/flx_core/flx_intersect.ml
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,46 @@ let record_intersect bsym_table counter br ls =
in
btyp_record flds

(* only matching fields are output, and the type is
the union of both types
*)
let record_pair_union counter br ls rs =
let rec aux ls rs out =
match ls, rs with
| ls, [] -> List.rev out
| [] , rs -> List.rev out
| (s1,t1) :: tl1, (s2,t2) :: tl2 ->
if s1 = s2 then begin
let t = br (btyp_union [t1;t2]) in
aux tl1 tl2 ((s1, t)::out)
end
else if s1 < s2 then aux tl1 rs out
else aux ls tl2 out
in
let result = aux ls rs [] in
result

(* Note: void is the unit of a union, that is 0 \/ t = t
However an "empty" record has type unit. So if we find an
empty set of fields in a union, it's void and we need a special case
*)
let record_union bsym_table counter br ls =
let flds = List.fold_left (fun acc r ->
match r with
| BTYP_record rs ->
begin match acc with
| [] -> rs
| _ -> record_pair_union counter br acc rs
end
| t ->
print_endline ("Flx_intersect: Record union requires records, got " ^ Flx_btype.st t);
failwith ("Flx_intersect: Record iunion requires records, got " ^ Flx_btype.st t)
) [] ls
in
match flds with
| [] -> btyp_void ()
| _ -> btyp_record flds


let nominal_intersect bsym_table counter br ls =
let js = List.fold_left (fun acc elt ->
Expand All @@ -47,6 +87,23 @@ let nominal_intersect bsym_table counter br ls =
failwith ("Flx_intersect: No unique greatest subtype found")
| Some i -> btyp_inst (`Nominal, i, [], KIND_type)

let nominal_union bsym_table counter br ls =
let js = List.fold_left (fun acc elt ->
match elt with
| BTYP_inst (`Nominal, j, [], KIND_type) -> j :: acc
| t ->
print_endline ("Flx_intersect: Nominal type union requires monomorphic nominal type, got " ^ Flx_btype.st t);
failwith ("Flx_intersect: Nominal type union requires monomorphic nominal type, got " ^ Flx_btype.st t)
) [] ls
in
let maybe_join = Flx_bsym_table.least_supertype bsym_table js in
match maybe_join with
| None ->
print_endline ("Flx_intersect: No unique least supertype found: " ^ Flx_print.sbt bsym_table (btyp_intersect ls) );
failwith ("Flx_intersect: No unique least supertype found")
| Some i -> btyp_inst (`Nominal, i, [], KIND_type)



let intersect bsym_table counter br ls =
let ls = List.map br ls in
Expand All @@ -56,5 +113,15 @@ let intersect bsym_table counter br ls =
| BTYP_inst (`Nominal, _, [], KIND_type) :: _ -> nominal_intersect bsym_table counter br ls
| t :: tail ->
print_endline ("Flx_intersect: Intersection only defined for records and monomorphic nominal types, got " ^ Flx_btype.st t);
failwith ("Flx_intersect: Intersection only defined for records and monomorphic nominal types, got " ^ Flx_btype.st t);
failwith ("Flx_intersect: Intersection only defined for records and monomorphic nominal types, got " ^ Flx_btype.st t)

let union bsym_table counter br ls =
let ls = List.map br ls in
match ls with
| [] -> btyp_any ()
| BTYP_record _ :: _ -> record_union bsym_table counter br ls
| BTYP_inst (`Nominal, _, [], KIND_type) :: _ -> nominal_union bsym_table counter br ls
| t :: tail ->
print_endline ("Flx_intersect: Union only defined for records and monomorphic nominal types, got " ^ Flx_btype.st t);
failwith ("Flx_intersect: Union only defined for records and monomorphic nominal types, got " ^ Flx_btype.st t)

1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_maps.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ let map_type f (t:typecode_t):typecode_t = match t with
| `TYP_suffix (sr,(qn,t)) -> `TYP_suffix (sr, (qn, f t))
| `TYP_tuple ts -> `TYP_tuple (List.map f ts)
| `TYP_intersect ts -> `TYP_intersect (List.map f ts)
| `TYP_union ts -> `TYP_union (List.map f ts)
| `TYP_compacttuple ts -> `TYP_compacttuple (List.map f ts)
| `TYP_record ts -> `TYP_record (List.map (fun (s,t) -> s,f t) ts)
| `TYP_polyrecord (ts,s,v) -> `TYP_polyrecord (List.map (fun (s,t) -> s,f t) ts, s, f v)
Expand Down
17 changes: 14 additions & 3 deletions src/compiler/flx_core/flx_print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -476,11 +476,15 @@ and st prec tc : string =

| `TYP_intersect ls ->
begin match ls with
| [] -> 0,"unit"
| [] -> 0,"any"
| _ -> 4, cat " & " (map (st 4) ls)
end


| `TYP_union ls ->
begin match ls with
| [] -> 0,"void"
| _ -> 4, cat " | " (map (st 4) ls)
end

| `TYP_compacttuple ls ->
begin match ls with
Expand Down Expand Up @@ -766,11 +770,18 @@ and sb bsym_table depth fixlist counter prec tc =

| BTYP_intersect ls ->
begin match ls with
| [] -> 0,"unit"
| [] -> 0,"any"
| [x] -> failwith ("UNEXPECTED INTERSECTION OF ONE ARGUMENT " ^ sbt 9 x)
| _ -> 4,cat " & " (map (sbt 4) ls)
end

| BTYP_union ls ->
begin match ls with
| [] -> 0,"void"
| [x] -> failwith ("UNEXPECTED UNION OF ONE ARGUMENT " ^ sbt 9 x)
| _ -> 4,cat " | " (map (sbt 4) ls)
end


| BTYP_tuple ls ->
begin match ls with
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_typing2.ml
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ let string_of_type_name (t:typecode_t) = match t with
| `TYP_patany _ -> " `TYP_patany"
| `TYP_tuple _ -> "`TYP_tuple"
| `TYP_intersect _ -> "`TYP_intersect"
| `TYP_union _ -> "`TYP_union"
| `TYP_compacttuple _ -> "`TYP_compacttuple"
| `TYP_unitsum _ -> "`TYP_unitsum"
| `TYP_sum _ -> "`TYP_sum"
Expand Down
4 changes: 4 additions & 0 deletions src/compiler/flx_cpp_backend/flx_cal_type_offsets.ml
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,10 @@ let rec get_offsets' syms bsym_table typ : offset_kind_t list =
print_endline ("Flx_cal_type_offsets: HOT intersection type");
[`Ptr "0"]

| BTYP_union _ ->
print_endline ("Flx_cal_type_offsets: HOT union type");
[`Ptr "0"]

| BTYP_tuple args ->
let n = ref 0 in
let lst = ref [] in
Expand Down
2 changes: 2 additions & 0 deletions src/compiler/flx_cpp_backend/flx_name.ml
Original file line number Diff line number Diff line change
Expand Up @@ -283,6 +283,7 @@ print_endline ("Flx_tgen.cpp_type_classname " ^ sbt bsym_table t);
| BTYP_array _ -> "_at" ^ cid_of_bid (tix t)
| BTYP_tuple _ -> "_tt" ^ cid_of_bid (tix t)
| BTYP_intersect _ -> "_intersection" ^ cid_of_bid (tix t)
| BTYP_union _ -> "_union" ^ cid_of_bid (tix t)
| BTYP_tuple_cons _ -> "_tt" ^ cid_of_bid (tix t)
| BTYP_tuple_snoc _ -> "_tt" ^ cid_of_bid (tix t)
(* | BTYP_tuple ts -> "_tt"^string_of_int (List.length ts)^"<" ^ catmap "," tn ts ^ ">" *)
Expand Down Expand Up @@ -468,6 +469,7 @@ and cpp_structure_name syms bsym_table t =

(* will work with ObjC protocols, but probably should be a C union of the intersectees .. *)
| BTYP_intersect _ -> "void*"
| BTYP_union _ -> "void*"

| BTYP_variant _ -> "::flx::rtl::_uctor_"

Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_desugar/flx_sex2flx.ml
Original file line number Diff line number Diff line change
Expand Up @@ -238,6 +238,7 @@ print_endline ("sex2flx:type] " ^ Sex_print.string_of_sex x);
| Lst [Id "typ_compactarray"; t1; t2] -> `TYP_compactarray (ti t1, ti t2)
| Lst [Id "typ_tuple"; sr; Lst es] -> `TYP_tuple (map ti es)
| Lst [Id "typ_intersect"; sr; t1; t2] -> `TYP_intersect [ti t1; ti t2]
| Lst [Id "typ_union"; sr; t1; t2] -> `TYP_union [ti t1; ti t2]
| Lst [Id "typ_compacttuple"; sr; Lst es] -> `TYP_compacttuple (map ti es)
| Lst [Id "typ_sum"; sr; Lst es] -> `TYP_sum (map ti es)
| Lst [Id "typ_compactsum"; sr; Lst es] -> `TYP_compactsum (map ti es)
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_frontend/flx_treg.ml
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,7 @@ print_endline ("Array type " ^ sbt bsym_table t ^ " base type " ^ sbt bsym_table
| BTYP_compacttuple ps
| BTYP_tuple ps -> iter rr ps; rnr t
| BTYP_intersect ps -> iter rr ps; rnr t
| BTYP_union ps -> iter rr ps; rnr t

| BTYP_tuple_cons (t1,t2) -> assert false
| BTYP_tuple_snoc (t1,t2) -> assert false
Expand Down
3 changes: 2 additions & 1 deletion src/packages/grammar.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,8 @@ syntax types {
t[satomic_pri] := "false" =># "`(typ_false ,_sr)";

// this is the intersection combinator
t[sproduct_pri] := t[sproduct_pri] "&" t[>sproduct_pri] =># '`(typ_intersect ,_sr ,_1 ,_3)';
t[sproduct_pri] := t[sproduct_pri] "/\" t[>sproduct_pri] =># '`(typ_intersect ,_sr ,_1 ,_3)';
t[ssum_pri] := t[ssum_pri] "\/" t[>ssum_pri] =># '`(typ_union ,_sr ,_1 ,_3)';

//$ Ellipsis (for binding C varags functions).
t[satomic_pri] := "..." =># "`(typ_ellipsis ,_sr)";
Expand Down

0 comments on commit 4e13dab

Please sign in to comment.