Skip to content

Commit

Permalink
Add new type BTYP_in (elt,tset).
Browse files Browse the repository at this point in the history 
This term has kind BOOL and is used in constraints,
it checks if a type is a member of a typeset.

It is eliminated in beta-reduction, being replaced
by a typematch.
  • Loading branch information
@skaller
skaller committed May 21, 2022
1 parent 22d49ed commit b5f980d
Show file tree
Hide file tree
Showing 20 changed files with 123 additions and 320 deletions.
37 changes: 0 additions & 37 deletions src/compiler/flx_bind/flx_bbind.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,43 +135,6 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
| _ -> ()
) bsym_table;
print_endline ("\n==========================================\n");
*)
(* DOING EXPANSION NOW *)
(*
Flx_bsym_table.iter (fun bid parent bsym ->
let bbdcl = Flx_bsym.bbdcl bsym in
let sr = Flx_bsym.sr bsym in
match bbdcl with
| BBDCL_nominal_type_alias (bvs,t) ->
(*
print_endline ("******* EXPANDING TYPEDEF " ^ bsym.id);
*)
let r = Flx_expand_typedef.expand bsym_table state.counter sr t in
let b = bbdcl_structural_type_alias (bvs, r) in
Flx_bsym_table.update_bbdcl bsym_table bid b
| BBDCL_type_function (bks,t) ->
(*
print_endline ("******* EXPANDING TYPEFUNCTION " ^ bsym.id);
*)
let r = Flx_expand_typedef.expand bsym_table state.counter sr t in
let b = bbdcl_type_function (bks, r) in
Flx_bsym_table.update_bbdcl bsym_table bid b
| _ -> ()
) bsym_table;
*)
(*
print_endline ("\n=====================\n TYPEDEFS after expansion\n=====================\n");
Flx_bsym_table.iter (fun bid parent bsym ->
let bbdcl = Flx_bsym.bbdcl bsym in
match bbdcl with
| BBDCL_structural_type_alias _ -> print_endline (bsym.id ^ " typedef " ^ string_of_int bid ^ " -> " ^
Flx_print.string_of_bbdcl bsym_table bbdcl bid)
| BBDCL_type_function (bks, t) -> print_endline (bsym.id ^ " typefun " ^ string_of_int bid ^ " -> " ^
Flx_print.string_of_bbdcl bsym_table bbdcl bid)
| _ -> ()
) bsym_table;
*)
(*
print_endline ("\n=====================\n VAR CACHE (function codomains) \n=====================\n");
Expand Down
83 changes: 19 additions & 64 deletions src/compiler/flx_bind/flx_bind_type.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,63 +22,25 @@ open Flx_btype_occurs
open Flx_btype_subst
open Flx_bid

let debug = false

let rec expand_typeset t =
match t with
| BTYP_type_tuple ls
| BTYP_type_set ls
| BTYP_type_set_union ls -> List.fold_left (fun ls t -> expand_typeset t @ ls) [] ls
| x -> [x]

let handle_typeset state sr elt tset =
let ls = expand_typeset tset in
(* x isin { a,b,c } is the same as
typematch x with
| a => 1
| b => 1
| c => 1
| _ => 0
endmatch
** THIS CODE ONLY WORKS FOR BASIC TYPES **
This is because we don't know what to do with any
type variables in the terms of the set. The problem
is that 'bind type' just replaces them with bound
variables. We have to assume they're not pattern
variables at the moment, therefore they're variables
from the environment.
We should really allow for patterns, however bound
patterns aren't just types, but types with binders
indicating 'as' assignments and pattern variables.
Crudely -- typesets are a hack that we should get
rid of in the future, since a typematch is just
more general .. however we have no way to generalise
type match cases so they can be named at the moment.
This is why we have typesets.. so I need to fix them,
so the list of things in a typeset is actually
a sequence of type patterns, not types.
(* NEW RULES. bind_type MAY NOT
lookup in the bound symbol table
beta reduce anything
*)
let e = BidSet.empty in
let un = bbool true in
let lss = List.rev_map (fun t -> {pattern=t; pattern_vars=e; assignments=[]},un) ls in
let fresh = fresh_bid state.counter in
let dflt =
{
pattern = btyp_type_var (fresh,Flx_kind.KIND_type);
pattern_vars = BidSet.singleton fresh;
assignments=[]
},
bbool false
in
let lss = List.rev (dflt :: lss) in
btyp_type_match (elt, lss)
It is permitted ONLY to actually replace names with indices
by lookup in the unbound symbol table, and,
replace unbound terms with corresponding bound terms
In particular, it is used to bind typedefs and type functions
putting them in the bound symbol table, so that subsequent binding
of non-type terms eg variables and functions, can find bound types
in the bound symbol table: at THAT point only ALL the nominal types
typedefs, and type functions must be in the bound symbol table.
The types can then be beta-reduced.
*)

let debug = false

let rec bind_type'
bind_type_index
Expand Down Expand Up @@ -328,17 +290,10 @@ print_endline ("Calling Flx_beta.adjust, possibly incorrectly, type = " ^ sbt bs
| `TYP_none ->
failwith "Unexpected `TYP_none in bind type"

| `TYP_typeset ts
| `TYP_setunion ts ->
btyp_type_set (expand_typeset (btyp_type_set (List.map bt ts)))

| `TYP_typeset ts -> btyp_type_set (List.map bt ts)
| `TYP_setunion ts -> btyp_type_set_union (List.map bt ts)
| `TYP_setintersection ts -> btyp_type_set_intersection (List.map bt ts)


| `TYP_isin (elt,typeset) ->
let elt = bt elt in
let typeset = bt typeset in
handle_typeset state sr elt typeset
| `TYP_isin (elt,tset) -> btyp_in (bt elt, bt tset)

| `TYP_var i ->
(*
Expand Down
20 changes: 5 additions & 15 deletions src/compiler/flx_bind/flx_overload.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -322,10 +322,8 @@ print_endline ("Scanning type variable " ^ s ^ "<" ^ si j' ^ ">: " ^ str_of_kind
(* this is not really right, kinds do act as constraints *)
match tp with
| KND_tpattern t ->
(*
if id = debugid then
print_endline (" .. found tpattern .. analysing .. ");
*)
(* if id = debugid then *)
print_endline (" .. found tpattern .. analysing .. " ^ string_of_typecode t);
type_of_tpattern counter t
| KND_generic (* overload treats this as a type variable in this routine *)
| KND_linear
Expand Down Expand Up @@ -413,13 +411,13 @@ if i = 7123 then
print_endline ("Flx_overload, constraint FUDGE");
*)
(* let t1 = btyp_type_var (i, btyp_type 0) in *)
let t1 = btyp_type_var (i, kind_linear) in
let t1 = btyp_type_var (i, kind_type) in
(*
if k = 7123 then
print_endline ("Flx_overload, constraint FUDGE");
*)
(* let t2 = btyp_type_var (k, btyp_type 0) in *)
let t2 = btyp_type_var (k, kind_linear) in
let t2 = btyp_type_var (k, kind_type) in

print_endline ("Adding equation " ^ sbt bsym_table t1 ^ " = " ^
sbt bsym_table t2);
Expand Down Expand Up @@ -461,7 +459,7 @@ if i = 7123 then
print_endline ("Flx_overload, extra FUDGE");
*)
(* let t1 = btyp_type_var (i, btyp_type 0) in *)
let t1 = btyp_type_var (i, kind_linear) in
let t1 = btyp_type_var (i, kind_type) in
extra_eqns := (t1,t2) :: !extra_eqns
end eqns1;

Expand Down Expand Up @@ -621,14 +619,10 @@ if name = debugid then print_endline ("BUILDING TYPE CONSTRAINTS");
*)
let type_constraint = build_type_constraints counter bsym_table (bt sr) id sr base_vs in
if name = debugid then print_endline ("TYPE CONSTRAINTS BUILT");
(*
if name = debugid then
print_endline ("type constraint1(build_type_constraints) " ^ sbt bsym_table type_constraint);
*)
(*
if name = debugid then
print_endline ("type constraint2(con) " ^ sbt bsym_table con);
*)
(*
let con =
try btyp_typeop "_type_to_staticbool" con Flx_kind.KIND_bool
Expand All @@ -640,10 +634,8 @@ if name = debugid then
print_endline ("type constraint2(con) as staticbool: " ^ sbt bsym_table con);
*)
let type_constraint = btyp_typeop "_staticbool_and" (btyp_type_tuple [type_constraint; con]) Flx_kind.KIND_bool in
(*
if name = debugid then
print_endline ("type constraint(merged) " ^ sbt bsym_table type_constraint);
*)
(*
if name = debugid then
print_endline ("Raw type constraint " ^ sbt bsym_table type_constraint);
Expand Down Expand Up @@ -940,10 +932,8 @@ if name = debugid then
)
in
let env_traint = btyp_typeop "_staticbool_and" (btyp_type_tuple (filter_out_units ls)) kind_bool in
(*
if name = debugid then
print_endline ("ENVIRONMENT CONSTRAINT BUILT = " ^ sbt bsym_table env_traint);
*)
(* HACK for the moment *)
let aux i =
match
Expand Down
3 changes: 0 additions & 3 deletions src/compiler/flx_bind/flx_symtab.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1394,9 +1394,6 @@ print_endline (string_of_int symbol_index ^ " Adding virtual type " ^ id ^ " to

| DCL_fun (props, ts,t,c,reqs,prec) ->
(*
if id = "bind" then print_endline ("Adding fun bind index=" ^ string_of_int symbol_index);
*)
(*
print_endline ("Adding DCL_fun " ^ id ^ " to symbol table " ^ name);
*)
(* Add the function to the sym_table. *)
Expand Down
35 changes: 21 additions & 14 deletions src/compiler/flx_bind/flx_tconstraint.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ let debug = false
*)


let build_constraint_element counter bt sr i p1 =
let build_constraint_element counter bsym_table bt sr i p1 =
(*
print_endline ("Build type constraints for type variable " ^string_of_int i ^": " ^ str_of_kindcode p1);
*)
Expand All @@ -41,7 +41,7 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^":
| KND_function _
| KND_tuple _ -> bbool true

| KND_tpattern p1 ->
| KND_tpattern p1 -> assert false; (* I don't think this is used anymore *)
begin
(* special case, no constraint, represent by just 'true' (unit type) *)
match p1 with
Expand Down Expand Up @@ -89,26 +89,39 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^":
varset1 explicit_vars1
in
let un = bbool true in (* the 'true' value of the type system *)
let elt = btyp_type_var (i, Flx_kind.kind_linear) in
let elt = btyp_type_var (i, Flx_kind.kind_type) in
let p1 = bt p1 in
let rec fe t = match t with
| BTYP_type_set ls
| BTYP_type_set_union ls ->
uniq_list (concat (map fe ls))

| BTYP_inst (`Alias,index,ts,mt) ->
begin try
let bsym = Flx_bsym_table.find bsym_table index in
let bbdcl = Flx_bsym.bbdcl bsym in
begin match bbdcl with
| Flx_bbdcl.BBDCL_structural_type_alias (bvs, alias)
| Flx_bbdcl.BBDCL_nominal_type_alias (bvs, alias) ->
let alias = Flx_btype_subst.tsubst sr bvs ts alias in
let alias = Flx_beta.beta_reduce "Tconstraint" counter bsym_table bsym.Flx_bsym.sr alias in
fe alias
| _ -> assert false
end
with Not_found ->
print_endline ("Flx_tconstraint: Unable to find symbol " ^ string_of_int index ^ " in bound symbol table!");
assert false
end
| t -> [t]
in
let tyset ls =
(*
print_endline ("Generating type match for typeset " ^ Flx_util.catmap ", " Flx_btype.st ls);
*)
let e = BidSet.empty in
let un = bbool true in
let lss = rev_map (fun t -> {pattern=t; pattern_vars=e; assignments=[]},un) ls in
let fresh = fresh_bid counter in
let dflt =
{
pattern = btyp_type_var (fresh, Flx_kind.kind_linear);
pattern = btyp_type_var (fresh, Flx_kind.kind_type);
pattern_vars = BidSet.singleton fresh;
assignments=[]
},
Expand All @@ -124,15 +137,9 @@ print_endline ("Generating type match for typeset " ^ Flx_util.catmap ", " Flx_b
| _ -> assert false (* unexpected kind *)

let build_type_constraints counter bsym_table bt name sr vs =
(*
print_endline ("building type constraints for " ^ name);
*)
let type_constraints =
map (fun (s,i,tp) ->
(*
print_endline ("type variable " ^ s ^ " constraint = " ^ str_of_kindcode tp);
*)
let tp = build_constraint_element counter bt sr i tp in
let tp = build_constraint_element counter bsym_table bt sr i tp in
(*
if tp <> btyp_tuple [] then
print_endline (
Expand Down

0 comments on commit b5f980d

Please sign in to comment.