Skip to content

Commit

Permalink
Added variance to nominal type specifier.
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed Jul 31, 2022
1 parent 88116b6 commit 6337f24
Show file tree
Hide file tree
Showing 46 changed files with 158 additions and 132 deletions.
12 changes: 8 additions & 4 deletions src/compiler/flx_bind/flx_bbind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -246,10 +246,12 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
let vs = fst sym.Flx_sym.vs in
begin match sym.Flx_sym.symdef with
| SYMDEF_function (params,ret,effect,props,_) when List.mem `Subtype props ->
(*
if List.length vs <> 0 then
clierr sr (" Improper subtype, no type variables allowed, got " ^
string_of_int (List.length vs))
else
*)
let dom, cod =
let ps = fst params in
begin match ps with
Expand Down Expand Up @@ -281,20 +283,22 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
print_endline ("Type of function " ^ string_of_int i ^ " is " ^ sbt bsym_table ft);
*)
match ft with
| BTYP_function (BTYP_inst (`Nominal, dom,[],_),BTYP_inst (`Nominal, cod,[],_)) ->
| BTYP_function (BTYP_inst (`Nominal _, dom,_,_),BTYP_inst (`Nominal _, cod,_,_)) ->
(*
print_endline ("Domain index = " ^ string_of_int dom ^ " codomain index = " ^ string_of_int cod);
*)
Flx_bsym_table.add_supertype bsym_table ((cod,dom),i)

| _ -> clierr sr ("Subtype specification requires nonpolymorphic nominal typed function")
| _ -> clierr sr ("Subtype specification requires function from and to nominal type")
end

| SYMDEF_fun (props,ps,ret,_,_,_) when List.mem `Subtype props ->
(*
if List.length vs <> 0 then
print_endline (" Improper subtype, no type variables allowed, got " ^
string_of_int (List.length vs))
else
*)
let dom, cod =
begin match ps with
| [typ] -> typ,ret
Expand Down Expand Up @@ -325,12 +329,12 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
print_endline ("Type of function " ^ string_of_int i ^ " is " ^ sbt bsym_table ft);
*)
match ft with
| BTYP_function (BTYP_inst (`Nominal, dom,[],_),BTYP_inst (`Nominal, cod,[],_)) ->
| BTYP_function (BTYP_inst (`Nominal _, dom,_,_),BTYP_inst (`Nominal _, cod,_,_)) ->
(*
print_endline ("Domain index = " ^ string_of_int dom ^ " codomain index = " ^ string_of_int cod);
*)
Flx_bsym_table.add_supertype bsym_table ((cod,dom),i)
| _ -> clierr sr ("Subtype specification requires nonpolymorphic nominal typed function")
| _ -> clierr sr ("Subtype specification requires function from and to nominal types")
end
| _ -> ()
end (* symdef *)
Expand Down
10 changes: 5 additions & 5 deletions src/compiler/flx_bind/flx_bind_circuit.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ type device_descr_t = string * pin_descr_t list

let cal_channel bsym_table (schannel,ischannel,oschannel) sr typ : int * string * Flx_btype.t =
match typ with
| BTYP_inst (`Nominal,i,[t],_) ->
| BTYP_inst (`Nominal _,i,[t],_) ->
let direction = match i with
| _ when i = schannel -> "io"
| _ when i = oschannel -> "output"
Expand Down Expand Up @@ -64,14 +64,14 @@ let bind_circuit bsym_table (state : Flx_bexe_state.bexe_state_t) sr be (cs:Flx_
print_endline ("Continuation starting function '_continuation_start' is " ^ Flx_print.sbe bsym_table start_continuation);
*)
let continuation_type_index = lun "cont" in
let continuation_type = Flx_btype.btyp_inst (`Nominal, continuation_type_index, [], Flx_kind.KIND_type) in
let continuation_type = Flx_btype.btyp_inst (`Nominal [], continuation_type_index, [], Flx_kind.KIND_type) in
let lmk name =
let signs = [continuation_type] in
let ts = [] in
luf name ts signs
in
let fthread_type_index = lun "fthread" in
let fthread_type = Flx_btype.btyp_inst (`Nominal, fthread_type_index, [], Flx_kind.KIND_type) in
let fthread_type = Flx_btype.btyp_inst (`Nominal [], fthread_type_index, [], Flx_kind.KIND_type) in
let mk_thread = lmk "mk_thread" in
(*
print_endline ("Fthread constructor function 'mk_thread' is " ^ Flx_print.sbe bsym_table mk_thread);
Expand Down Expand Up @@ -395,7 +395,7 @@ print_endline ("SPawn Fthread svc call '_svc_fthread' is " ^ Flx_print.sbe bsym_
vt,nw
in
let name = "pin_" ^ string_of_int index in
let stype = Flx_btype.btyp_inst (`Nominal, schannel, [vt], Flx_kind.KIND_type) in
let stype = Flx_btype.btyp_inst (`Nominal [], schannel, [vt], Flx_kind.KIND_type) in
let bbdcl = Flx_bbdcl.bbdcl_val (state.parent_vs,stype,`Val) in
let bsym = Flx_bsym.create ~sr name bbdcl in
Flx_bsym_table.add bsym_table index state.parent bsym;
Expand Down Expand Up @@ -449,7 +449,7 @@ print_endline ("SPawn Fthread svc call '_svc_fthread' is " ^ Flx_print.sbe bsym_
(* the type expected, ischannel,oschannel, or schannel, is NOT
the actual variable type which is always just schannel
*)
let ct = Flx_btype.btyp_inst (`Nominal, cast_schannelindex,[vt], Flx_kind.KIND_type) in
let ct = Flx_btype.btyp_inst (`Nominal [], cast_schannelindex,[vt], Flx_kind.KIND_type) in
let component = pin,(Flx_bexpr.bexpr_varname ct (vindex, parent_ts)) in
component::acc
)
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_bind/flx_bind_symbol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -757,7 +757,7 @@ print_endline ("Flx_bbind: Adding type of index " ^ si symbol_index ^ " to cache
| SYMDEF_union (cs,variance) ->
if state.print_flag then
print_endline ("//Binding union " ^ si symbol_index ^ " --> " ^ sym.Flx_sym.id);
let ut = btyp_inst ( `Nominal,
let ut = btyp_inst ( `Nominal variance,
symbol_index,
List.map (fun (s,i,k) -> btyp_type_var (i,k)) bvs,
Flx_kind.KIND_type)
Expand Down
10 changes: 5 additions & 5 deletions src/compiler/flx_bind/flx_bind_type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -509,15 +509,15 @@ print_endline ("Binding `TYP_name " ^s^ " via params to " ^ sbt bsym_table t);
syserr sr ("Synthetic name "^name ^ " not in symbol table!")
in
begin match sym.Flx_sym.symdef with
| SYMDEF_struct _
| SYMDEF_cstruct _
| SYMDEF_union _
| SYMDEF_abs _ ->
| SYMDEF_struct (_,variance)
| SYMDEF_cstruct (_,_,variance)
| SYMDEF_union (_,variance)
| SYMDEF_abs (_,_,_,variance) ->
let ts = List.map
(fun (s,i,mt) -> btyp_type_var (i, Flx_btype.bmt "Flx_bind_type1" mt))
(fst sym.Flx_sym.vs)
in
btyp_inst (`Nominal,index,ts,Flx_kind.KIND_type)
btyp_inst (`Nominal variance,index,ts,Flx_kind.KIND_type)
| SYMDEF_typevar _ ->
print_endline ("Synthetic name "^name ^ " is a typevar!");
syserr sr ("Synthetic name "^name ^ " is a typevar!")
Expand Down
23 changes: 11 additions & 12 deletions src/compiler/flx_bind/flx_bind_type_index.ml
Original file line number Diff line number Diff line change
Expand Up @@ -230,29 +230,28 @@ print_endline ("Flx_bind_type_index: btyp_inst, meta type calculated by guess_me
t
end

| SYMDEF_abs _ ->
btyp_inst (`Nominal, index,ts,Flx_kind.KIND_type)
| SYMDEF_abs (_,_,_,variance) ->
btyp_inst (`Nominal variance, index,ts,Flx_kind.KIND_type)

| SYMDEF_virtual_type ->
btyp_vinst (index,ts,Flx_kind.KIND_type)

| SYMDEF_newtype _
| SYMDEF_union _
| SYMDEF_struct _
| SYMDEF_cstruct _
| SYMDEF_newtype _ ->
btyp_inst (`Nominal [],index,ts,Flx_kind.KIND_type)

| SYMDEF_union (_,variance)
| SYMDEF_struct (_,variance)
| SYMDEF_cstruct (_,_,variance)
->
(*
print_endline ("bind type index, struct thing " ^ si index ^ " ts=" ^ catmap "," (sbt bsym_table) ts);
*)
btyp_inst (`Nominal,index,ts,Flx_kind.KIND_type)
btyp_inst (`Nominal variance,index,ts,Flx_kind.KIND_type)


(* allow binding to type constructors now too .. *)
| SYMDEF_const_ctor (uidx,ut,idx,vs') ->
btyp_inst (`Nominal, index,ts,Flx_kind.KIND_type)
btyp_inst (`Nominal [], index,ts,Flx_kind.KIND_type)

| SYMDEF_nonconst_ctor (uidx,ut,idx,vs',argt) ->
btyp_inst (`Nominal, index,ts,Flx_kind.KIND_type)
btyp_inst (`Nominal [], index,ts,Flx_kind.KIND_type)

| SYMDEF_typeclass
| SYMDEF_module
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_bind/flx_btype_of_bsym.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ print_endline ("btype of bsym struct " ^ Flx_bsym.id bsym ^ "<" ^ si bid ^ ">, #
ts
in
let t = btyp_tuple (List.map snd ls) in
let result = btyp_function (t, btyp_inst (`Nominal, bid, ts, Flx_kind.KIND_type)) in
let result = btyp_function (t, btyp_inst (`Nominal variance, bid, ts, Flx_kind.KIND_type)) in
(*
print_endline ("struct as function [btype_of_bsym] " ^ sbt bsym_table result);
*)
Expand Down
6 changes: 3 additions & 3 deletions src/compiler/flx_bind/flx_inner_type_of_index.ml
Original file line number Diff line number Diff line change
Expand Up @@ -190,8 +190,8 @@ print_endline ("** FINISH **** Calculating Function type for function " ^ sym.Fl
clierrx "[flx_bind/flx_lookup.ml:2048: E108] " sym.Flx_sym.sr ("Union " ^ sym.Flx_sym.id ^ " doesn't have a type")

(* struct as function *)
| SYMDEF_cstruct (ls,_,_)
| SYMDEF_struct (ls,_) ->
| SYMDEF_cstruct (ls,_,variance)
| SYMDEF_struct (ls,variance) ->
let _,vs,_ = find_split_vs state.sym_table bsym_table index in
let ts = List.map
(fun (s,i,_) -> `TYP_name (sym.Flx_sym.sr,s,[]))
Expand Down Expand Up @@ -219,7 +219,7 @@ print_endline ("** FINISH **** Calculating Function type for function " ^ sym.Fl
*)

let mt = Flx_kind.kind_type in
let result = btyp_function (bt sym.Flx_sym.sr t, btyp_inst (`Nominal,index, ts, mt)) in
let result = btyp_function (bt sym.Flx_sym.sr t, btyp_inst (`Nominal variance,index, ts, mt)) in
(*
print_endline ("struct as function [inner_type_of_index] " ^ sbt bsym_table result);
*)
Expand Down
4 changes: 2 additions & 2 deletions src/compiler/flx_bind/flx_lookup.ml
Original file line number Diff line number Diff line change
Expand Up @@ -841,7 +841,7 @@ and lookup_name_with_sig
print_endline ("projection of tuple cons not implemented yet"); assert false
*)

| [BTYP_inst (`Nominal,j,ts',_) as d] ->
| [BTYP_inst (`Nominal _,j,ts',_) as d] ->
let bsym = try Some (Flx_bsym_table.find bsym_table j) with Not_found -> None in
begin match bsym with
| Some bsym ->
Expand Down Expand Up @@ -891,7 +891,7 @@ and lookup_name_with_sig
end
end

| [BTYP_ptr (mode,BTYP_inst (`Nominal,j,ts',_) ,[]) as d] ->
| [BTYP_ptr (mode,BTYP_inst (`Nominal _,j,ts',_) ,[]) as d] ->
let bsym = try Some (Flx_bsym_table.find bsym_table j) with Not_found -> None in
begin match bsym with
| Some bsym ->
Expand Down
15 changes: 11 additions & 4 deletions src/compiler/flx_bind/flx_lookup_name_itdws.ml
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ if name = debugid then
(* if its a struct with a record argument we return it without checking if the record
matches ..
*)
| (SYMDEF_cstruct _ | SYMDEF_struct _ )
| (SYMDEF_struct (_,variance) | SYMDEF_cstruct (_,_,variance ) )
when
(match t2 with
| [BTYP_record _] -> true
Expand All @@ -229,7 +229,7 @@ if name = debugid then
print_endline ("lookup_name_in_table_dirs_with_sig finds struct constructor " ^ id);
print_endline ("Record Argument type is " ^ catmap "," (sbt bsym_table) t2);
end;
Some (bexpr_closure (btyp_inst (`Nominal, sye index,ts,Flx_kind.KIND_type)) (sye index,ts))
Some (bexpr_closure (btyp_inst (`Nominal variance, sye index,ts,Flx_kind.KIND_type)) (sye index,ts))
(*
failwith "NOT IMPLEMENTED YET"
*)
Expand Down Expand Up @@ -399,14 +399,21 @@ if name = debugid then
{ Flx_sym.id=id; sr=sr; vs=vs; symdef=entry }->
if id = debugid then print_endline ("FOUND " ^ id);
match entry with
| (SYMDEF_cstruct _ | SYMDEF_struct _ ) ->
| (SYMDEF_struct (_,variance) | SYMDEF_cstruct (_,_,variance) ) ->
(match t2 with
| [BTYP_record _] -> true
| _ -> false
)
| _ -> false
) ->
Some (bexpr_closure (btyp_inst (`Nominal, sye i,ts,Flx_kind.KIND_type)) (sye i,ts))
let variance =
match get_data state.sym_table (sye i) with
{ Flx_sym.id=id; sr=sr; vs=vs; symdef=entry }->
match entry with
| (SYMDEF_struct (_,variance) | SYMDEF_cstruct (_,_,variance) ) -> variance
| _ -> assert false
in
Some (bexpr_closure (btyp_inst (`Nominal variance, sye i,ts,Flx_kind.KIND_type)) (sye i,ts))

| _ ->
let fs =
Expand Down
19 changes: 11 additions & 8 deletions src/compiler/flx_bind/flx_lookup_type_name_itdws.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,12 @@ let handle_type
state bsym_table rs sra srn name ts index =
let sym = get_data state.sym_table index in
match sym.Flx_sym.symdef with
| SYMDEF_struct (_,variance)
| SYMDEF_cstruct (_,_,variance) -> btyp_inst (`Nominal [],index,ts,Flx_kind.KIND_type)
| SYMDEF_nonconst_ctor _
| SYMDEF_function _
| SYMDEF_fun _
| SYMDEF_struct _
| SYMDEF_cstruct _
| SYMDEF_nonconst_ctor _
| SYMDEF_callback _ -> btyp_inst (`Nominal,index,ts,Flx_kind.KIND_type)
| SYMDEF_callback _ -> btyp_inst (`Nominal [],index,ts,Flx_kind.KIND_type)
| SYMDEF_instance_type _ ->
(*
print_endline ("Lookup_type_name_in_table_dirs_with_sig: Handle type " ^ name ^ " ... binding type index " ^ string_of_int index);
Expand Down Expand Up @@ -158,11 +158,14 @@ let lookup_type_name_in_table_dirs_with_sig
print_endline "Found virtual type";
Some (btyp_vinst (sye index, ts, Flx_kind.KIND_type))

| SYMDEF_newtype _
| SYMDEF_abs _
| SYMDEF_union _ ->
(* FIXME when newtype gets variance! *)
| SYMDEF_newtype _ ->
Some (btyp_inst (`Nominal [],sye index, ts, Flx_kind.KIND_type))

| SYMDEF_abs (_,_,_,variance)
| SYMDEF_union (_,variance) ->
(* print_endline "Found abs,union,or newtype"; *)
Some (btyp_inst (`Nominal,sye index, ts, Flx_kind.KIND_type))
Some (btyp_inst (`Nominal variance,sye index, ts, Flx_kind.KIND_type))

(* an instance type is just like a type alias in phase 1 *)
| SYMDEF_instance_type t ->
Expand Down
4 changes: 4 additions & 0 deletions src/compiler/flx_bind/flx_subtypetable.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,12 @@ let report_subtypes syms =
(*
print_endline ("Felix Function: Symbol table " ^ string_of_int bid ^ " -> " ^ sym.id);
*)
(*
if List.length vs <> 0 then
print_endline (" Improper subtype, no type variables allowed, got " ^
string_of_int (List.length vs))
else
*)
let ps = fst params in
begin match ps with
| Satom (sr,kind,id,typ,initopt) -> ()
Expand All @@ -33,10 +35,12 @@ let report_subtypes syms =
(*
print_endline ("Extern Function: Symbol table " ^ string_of_int bid ^ " -> " ^ sym.id);
*)
(*
if List.length vs <> 0 then
print_endline (" Improper subtype, no type variables allowed, got " ^
string_of_int (List.length vs))
else
*)
begin match ps with
| [typ] -> ()
(*
Expand Down
5 changes: 5 additions & 0 deletions src/compiler/flx_core/flx_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,12 @@ type variance_t = [
]
type variance_list_t = variance_t list

let string_of_variance_list v =
String.concat "," (List.map (function | `covariant -> "+" | `invariant -> "!" | `contravariant -> "-") v)

type base_type_qual_t = [
| `Regular
| `Semiregular
| `Incomplete
| `Uncopyable
| `Pod
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_beta.ml
Original file line number Diff line number Diff line change
Expand Up @@ -361,7 +361,7 @@ print_endline ("processed ts = " ^ catmap "," Flx_btype.st ts);
with Not_found -> assert false
end

| BTYP_inst (`Nominal, i,ts,mt) -> btyp_inst (`Nominal,i, List.map br ts,mt)
| BTYP_inst (`Nominal v, i,ts,mt) -> btyp_inst (`Nominal v,i, List.map br ts,mt)
| BTYP_typeop (op,t,k) ->
(*
print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
Expand Down
6 changes: 3 additions & 3 deletions src/compiler/flx_core/flx_btype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,12 @@ let str_of_pmode = function
| `N -> "NULL"

type instkind_t = [
| `Nominal (* nominal type: primitive or user defined *)
| `Nominal of variance_list_t (* nominal type: primitive or user defined *)
| `Alias (* type alias, to be eliminated *)
]

let str_of_instkind = function
| `Nominal -> "Nominal"
| `Nominal v -> "Nominal["^string_of_variance_list v^"]"
| `Alias -> "Alias"

type btpattern_t = {
Expand Down Expand Up @@ -640,7 +640,7 @@ let btyp_vinst (bid, ts,mt) =
BTYP_vinst (bid, ts,mt)


let btyp_int () = btyp_inst (`Nominal,Flx_concordance.flx_int, [], Flx_kind.kind_type)
let btyp_int () = btyp_inst (`Nominal[],Flx_concordance.flx_int, [], Flx_kind.kind_type)

(** Construct a BTYP_array type. *)
let btyp_array (t, n) =
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_btype.mli
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ type pmode = [

val str_of_pmode: pmode -> string
type instkind_t = [
| `Nominal (* nominal type: primitive or user defined *)
| `Nominal of Flx_ast.variance_list_t (* nominal type: primitive or user defined *)
| `Alias (* type alias, to be eliminated *)
]

Expand Down

0 comments on commit 6337f24

Please sign in to comment.