Skip to content

Commit

Permalink
Add almost working type function code.
Browse files Browse the repository at this point in the history
The binding is reworked to strict phases.
Beta reduction is done on everything (supposedly) at the end.
All the tests pass except the GUI which all fail with what
appears to be an unreduced term. Unfortunately, the failure
is at an extremely low level and there are no tracking diagnostics.

So I will commit what I have since most of it works,
and it self-rebuilds ok. I have missed beta-reducing something.
  • Loading branch information
skaller committed Feb 5, 2022
1 parent d00cc9d commit 292ba28
Show file tree
Hide file tree
Showing 24 changed files with 210 additions and 89 deletions.
116 changes: 72 additions & 44 deletions src/compiler/flx_bind/flx_bbind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ open Flx_bbind_state

let debug = false

let showpasses =
try let _ = Sys.getenv "FLX_COMPILER_SHOW_BINDING_PASSES" in true
with Not_found -> false


let hfind msg h k =
try Flx_sym_table.find h k
with Not_found ->
Expand All @@ -43,9 +48,8 @@ let rec fix_typeofs state bsym_table t =


let bbind (state:Flx_bbind_state.bbind_state_t) start_counter ref_counter bsym_table =
(*
print_endline ("Flx_bbind.bbind *********************** ");
*)
if showpasses then
print_endline ("Flx_bbind.bbind *********************** " ^ string_of_int (Flx_bsym_table.length bsym_table));
(* loop through all counter values [HACK] to get the indices in sequence, AND,
* to ensure any instantiations will be bound, (since they're always using the
* current value of state.counter for an index. Note that in the process of
Expand All @@ -54,16 +58,11 @@ print_endline ("Flx_bbind.bbind *********************** ");
*)
(* PASS 0, TYPEDEFS ONLY *)

(*
print_endline ("\n====================\nSetting type aliases to nominal\n===============\n");
*)
if showpasses then
print_endline ("\n====================\nPASS 1 PLAIN BINDING: Setting type aliases to nominal\n===============\n");
let saved_env_cache = Hashtbl.copy state.lookup_state.Flx_lookup_state.env_cache in
let saved_visited = Hashtbl.copy state.visited in

(*
let bsym_table_dummy = Flx_bsym_table.create_fresh () in
*)
let bsym_table_dummy = bsym_table in
set_nominal_typedefs state;
let counter = ref start_counter in
while !counter < !ref_counter do
Expand Down Expand Up @@ -92,7 +91,7 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
(*
print_endline ("Binding typefun " ^ sym.Flx_sym.id ^ "<"^string_of_int i^"> = " ^ string_of_typecode t);
*)
begin try Flx_bind_symbol.bbind_symbol state bsym_table_dummy i parent sym
begin try Flx_bind_symbol.bbind_symbol state bsym_table i parent sym
with Not_found ->
try match hfind "bbind" state.sym_table i with { Flx_sym.id=id } ->
print_endline ("Binding error, Not_found thrown binding " ^ id ^ " index " ^
Expand All @@ -109,7 +108,7 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
(*
print_endline ("Binding typedef " ^ sym.Flx_sym.id ^ "<"^string_of_int i^"> = " ^ string_of_typecode t);
*)
begin try Flx_bind_symbol.bbind_symbol state bsym_table_dummy i parent sym
begin try Flx_bind_symbol.bbind_symbol state bsym_table i parent sym
with Not_found ->
try match hfind "bbind" state.sym_table i with { Flx_sym.id=id } ->
print_endline ("Binding error, Not_found thrown binding " ^ id ^ " index " ^
Expand All @@ -130,34 +129,47 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
Flx_bsym_table.iter (fun bid parent bsym ->
let bbdcl = Flx_bsym.bbdcl bsym in
match bbdcl with
| BBDCL_nominal_type_alias _ -> print_endline ("typedef " ^ string_of_int bid ^ " -> " ^
Flx_print.string_of_bbdcl bsym_table_dummy bbdcl bid)
| BBDCL_type_function _
| BBDCL_nominal_type_alias _ -> print_endline (bsym.id ^ " typedef " ^ string_of_int bid ^ " -> " ^
Flx_print.string_of_bbdcl bsym_table bbdcl bid)
| _ -> ()
) bsym_table_dummy;
) 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_dummy bid b
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_dummy;
) 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 ("typedef " ^ string_of_int bid ^ " -> " ^
Flx_print.string_of_bbdcl bsym_table_dummy bbdcl bid)
| 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_dummy;
) bsym_table;
*)
(*
print_endline ("\n=====================\n VAR CACHE (function codomains) \n=====================\n");
Expand All @@ -183,30 +195,16 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
state.visited <-saved_visited;
state.lookup_state.Flx_lookup_state.env_cache <- saved_env_cache;

(*
(* copy the typedefs into the main symbol table *)
Flx_bsym_table.iter (fun bid parent bsym ->
let bbdcl = Flx_bsym.bbdcl bsym in
match bbdcl with
| BBDCL_structural_type_alias _ ->
Flx_bsym_table.add bsym_table bid parent bsym;
Hashtbl.add state.visited bid ()
| _ ->
print_endline ("Copy typedefs: Not copying " ^ string_of_int bid);
assert false;
()
) bsym_table_dummy;
*)
if showpasses then
print_endline ("\n===================\nSetting type aliases to structural\n=======================\n");

(*
print_endline ("\n===================\nSetting type aliases to structura\n=======================\n");
*)
(* PASS 1, TYPE ONLY *)
set_structural_typedefs state;

(*
print_endline ("Fixing typeofs");
*)
if showpasses then
print_endline ("\n===================\nFixing typeofs \n=======================\n");


Flx_bsym_table.iter (fun bid parent bsym ->
let bbdcl = Flx_bsym.bbdcl bsym in
let sr = Flx_bsym.sr bsym in
Expand All @@ -215,12 +213,19 @@ print_endline ("Fixing typeofs");
let r = fix_typeofs state bsym_table 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) ->
let r = fix_typeofs state bsym_table t in
let b = bbdcl_type_function (bks, r) in
Flx_bsym_table.update_bbdcl bsym_table bid b

| _ -> ()
) bsym_table_dummy;
) bsym_table;
(*
print_endline ("Done fixing typeofs");
*)
if showpasses then
print_endline ("\n===================\nBinding nominal types \n=======================\n");
let counter = ref start_counter in
while !counter < !ref_counter do
let i = !counter in
Expand Down Expand Up @@ -257,6 +262,8 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
done
;

if showpasses then
print_endline ("\n===================\nHandling Subtyping Coercions\n=======================\n");
(* PASS 2, SUBTYPE COERCIONS ONLY *)
let counter = ref start_counter in
while !counter < !ref_counter do
Expand Down Expand Up @@ -367,6 +374,8 @@ print_endline ("[flx_bbind] bind_symbol " ^ sym.Flx_sym.id ^ "??");
done
;

if showpasses then
print_endline ("\n===================\nBinding non-deferred functions\n=======================\n");
(* PASS 3, NON DEFERRED FUNCTIONS *)
let defered = ref [] in
let counter = ref start_counter in
Expand Down Expand Up @@ -397,6 +406,8 @@ print_endline ("Binding symbol " ^ symdef.Flx_sym.id ^ "<" ^ si i ^ ">");
done
;

if showpasses then
print_endline ("\n===================\nBinding deferred functions\n=======================\n");
(* PASS 4 DEFERRED FUNCTIONS *)
if (List.length (!defered) <> 0) then begin
print_endline ("DEFERED PROCESSING STARTS");
Expand All @@ -421,6 +432,23 @@ print_endline ("[flx_bbind] DEFERED bind_symbol " ^ sym.Flx_sym.id ^ "?? calling
(!defered)
;
print_endline ("DEFERED PROCESSING ENDS");
end

end;

if showpasses then
print_endline ("\n===================\nBETA EVERYTHING \n=======================\n");

Flx_bsym_table.iter
(fun bid parent bsym ->
let f_btype t = Flx_beta.beta_reduce "Global beta reduction" state.counter bsym_table Flx_srcref.dummy_sr t in
let f_bexpr e = Flx_bexpr.map ~f_btype e in
let f_bexe exe = Flx_bexe.map ~f_btype exe in
let bbdcl = Flx_bbdcl.map ~f_btype ~f_bexe ~f_bexpr bsym.bbdcl in
let bsym = Flx_bsym.replace_bbdcl bsym bbdcl in
Flx_bsym_table.update bsym_table bid bsym
) bsym_table
;

if showpasses then
print_endline ("\n===================\nBINDING COMPLETE \n=======================\n")

4 changes: 3 additions & 1 deletion src/compiler/flx_bind/flx_bind_bexe.ml
Original file line number Diff line number Diff line change
Expand Up @@ -621,7 +621,9 @@ print_endline ("Flx_bind_bexe: UNIFIYING explicit ret=" ^ sbt bsym_table state.
if funame="insert_unique'3_mf_3732" then
print_endline ("Flx_bind_bexe: UNIFICATION DONE, result= " ^ string_of_bool uresult);
*)
state.ret_type <- varmap_subst (Flx_lookup_state.get_varmap state.lookup_state) state.ret_type;
let rt = varmap_subst (Flx_lookup_state.get_varmap state.lookup_state) state.ret_type in
let rt = Flx_beta.beta_reduce "flx_bind_bexe: EXE_fun_return" state.counter bsym_table sr rt in
state.ret_type <- rt;
if type_match bsym_table state.counter state.ret_type t' then
(*
if match maybe_matches bsym_table state.counter [state.ret_type, t'] with Some _ -> true | _ -> false then
Expand Down
8 changes: 7 additions & 1 deletion src/compiler/flx_bind/flx_bind_expression.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ let base_type_of_literal sr {Flx_literal.felix_type=t } = `TYP_name (sr,t,[])
let type_of_literal inner_bind_type state bsym_table env sr v =
let _,_,root,_,_ = List.hd (List.rev env) in
let t = base_type_of_literal sr v in
let bt = inner_bind_type state bsym_table env sr rsground t in
let bt = inner_bind_type "Flx_bind_expression:type_of_literal" state bsym_table env sr rsground t in
bt

let handle_map sr (f,ft) (a,at) =
Expand Down Expand Up @@ -126,7 +126,13 @@ let rec bind_expression'
let bt sr t =
(* we're really wanting to call bind type and propagate depth ? *)
let t = bind_type' state bsym_table env { rs with depth=rs.depth +1 } sr t [] mkenv in
(*
print_endline ("Flx_bind_expression will try to beta reduce " ^ sbt bsym_table t);
*)
let t = beta_reduce "flx_lookup: bind_expression'(1)" state.counter bsym_table sr t in
(*
print_endline ("Flx_bind_expression beta reduce result = " ^ sbt bsym_table t);
*)
t
in
let ti sr i ts =
Expand Down
27 changes: 23 additions & 4 deletions src/compiler/flx_bind/flx_bind_symbol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ let str_parent p = match p with | Some p -> string_of_int p | None -> "None"

let rec bbind_symbol state bsym_table symbol_index sym_parent sym =
(*
print_endline (" ^^^^ BBIND_SYMBOL (subroutine) : Binding symbol "^sym.Flx_sym.id^" index=" ^ string_of_int symbol_index);
print_endline (" ^^^^ BIND_SYMBOL (subroutine) : Binding symbol "^sym.Flx_sym.id^" index=" ^ string_of_int symbol_index);
*)
(* If we've already processed this bid, exit early. We do this so we can avoid
* any infinite loops in the symbols. *)
Expand Down Expand Up @@ -101,14 +101,14 @@ let rec bbind_symbol state bsym_table symbol_index sym_parent sym =
print_endline ("Parent " ^ str_parent sym_parent ^ " mapped to true parent " ^ str_parent true_parent);
*)
(* let env = Flx_lookup.build_env state.lookup_state state.sym_table parent in *)

let env = Flx_lookup.build_env
state.lookup_state
bsym_table
(Some symbol_index)
in

(*
print_endline "got ENVIRONMENT:";
print_env_short env;
*)

Expand Down Expand Up @@ -239,6 +239,7 @@ print_endline (" &&&&&& bind_type_uses calling BBIND_SYMBOL");
(* bind the type variables *)
let bvs = map (fun (s,i,tp) -> s,i, Flx_btype.bmt "Flx_bbind" tp) (fst ivs) in

(* DEFINE HOW TO BIND A TYPE CONSTRAINT: DOES NOT BETA REDUCE *)
let bind_type_constraint ivs =
let cons =
try
Expand All @@ -261,11 +262,29 @@ print_endline ("Binding type constraint: cons=" ^ sbt bsym_table cons);
(*
print_endline ("Binding type constraint: icons=" ^ sbt bsym_table icons);
*)
let cons = btyp_typeop "_staticbool_and" (btyp_type_tuple [cons; icons]) Flx_kind.KIND_bool in
(* Special cases to reduce debug output *)
let cons = match cons,icons with
| BBOOL true,x
| x, BBOOL true -> x
| _ -> btyp_typeop "_staticbool_and" (btyp_type_tuple [cons; icons]) Flx_kind.KIND_bool
in
(*
print_endline ("[Flx_bind_symbol] Binding type constraint: cons=" ^ sbt bsym_table cons);
*)
cons
in

(* NOW ACTUALLY BIND TYPE CONSTRAINT *)
let bcons = bind_type_constraint ivs in
let bcons = Flx_beta.beta_reduce "flx_bbind: constraint" state.counter bsym_table sym.Flx_sym.sr bcons in
let bcons =
if bcons = bbool true then bcons else
(*
let _ = print_endline ("[Flx_bind_symbol] Beta reducing type constraint : bcons=" ^ sbt bsym_table bcons) in
let bcons = Flx_beta.beta_reduce "flx_bbind: constraint" state.counter bsym_table sym.Flx_sym.sr bcons in
let _ = print_endline ("[Flx_bind_symbol] Beta reduced type constraint : bcons=" ^ sbt bsym_table bcons) in
*)
bcons
in
(*
print_endline ("[flx_bbind] bound type constraint bcons = " ^ sbt bsym_table bcons);
*)
Expand Down
7 changes: 3 additions & 4 deletions src/compiler/flx_bind/flx_bind_type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ open Flx_mtypes2
open Flx_typing
open Flx_typing2
open Flx_unify
open Flx_beta
open Flx_generic
open Flx_overload
open Flx_tpat
Expand Down Expand Up @@ -121,7 +120,7 @@ print_endline ("Bind type " ^ string_of_typecode t ^ " params = " ^
let bt t = btp t params in
let bi i ts = bind_type_index state bsym_table rs sr i ts mkenv in
let bisub i ts = bind_type_index state bsym_table {rs with depth= rs.depth+1} sr i ts mkenv in
let br t = Flx_beta.beta_reduce "flx_lookup: bind_type'" state.counter bsym_table sr t in
(* let br t = Flx_beta.beta_reduce "flx_lookup: bind_type'" state.counter bsym_table sr t in *)

let t =
match t with
Expand Down Expand Up @@ -245,7 +244,7 @@ print_endline ("Bound variant = " ^ Flx_btype.st t);
clierr sr ("Flx_bind_type.record extension: can't find nominal type, expected typedef .." ^ string_of_int i)
end

| _ -> clierrx "[flx_bind/flx_lookup.ml:802: E93] " sr ("Record extension requires bases be records too, got " ^
| _ -> clierrx "[flx_bind_type.ml:247: E93] " sr ("Record extension requires bases be records too, got " ^
Flx_btype.st t ^ "=" ^
sbt bsym_table t)
)
Expand Down Expand Up @@ -544,7 +543,7 @@ print_endline ("type _map datatype = " ^ sbt bsym_table bt2);
(*
print_endline ("Binding `TYP_apply " ^ string_of_typecode t);
*)
let x = br (btyp_type_apply (bt t1, bt t2)) in
let x = (* br *) (btyp_type_apply (bt t1, bt t2)) in
(*
print_endline (" ***** Bound `TYP_apply: " ^ Flx_btype.st x );
*)
Expand Down
4 changes: 2 additions & 2 deletions src/compiler/flx_bind/flx_bind_type_index.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ open Flx_mtypes2
open Flx_typing
open Flx_typing2
open Flx_unify
open Flx_beta
open Flx_generic
open Flx_overload
open Flx_tpat
Expand All @@ -23,6 +22,7 @@ open Flx_btype_occurs
open Flx_btype_subst
open Flx_bid

(* NOTE: THIS MODULE DOES NOT DIRECTLY DO BETA REDUCTION *)

(* This module produces a reference to either a nominal type, or a type alias,
of the form
Expand Down Expand Up @@ -77,7 +77,7 @@ let debug = false

let rec bind_type_index
bind_type'
inner_bind_type
inner_bind_type (* why is this here it isn't used *)
state (bsym_table:Flx_bsym_table.t) (rs:recstop) sr index ts mkenv
=
(* fixup the fixpoints *)
Expand Down
4 changes: 4 additions & 0 deletions src/compiler/flx_bind/flx_cal_apply.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ print_endline ("cal_apply', AFTER NORMALISE, fn = " ^ sbt bsym_table t1 ^ " arg=
end
;
*)

let t1 = Flx_beta.beta_reduce "Flx_cal_apply:cal_apply'" state.counter bsym_table sr t1 in
let t2 = Flx_beta.beta_reduce "Flx_cal_apply:cal_apply'" state.counter bsym_table sr t2 in

let result_type,reorder =
let argt = unfold "flx_cal_apply" t1 in
match argt with
Expand Down

0 comments on commit 292ba28

Please sign in to comment.