Skip to content

Commit

Permalink
Expand polyvariants in beta.
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed Mar 4, 2024
1 parent a4bb09e commit 087fa8a
Show file tree
Hide file tree
Showing 8 changed files with 35 additions and 14 deletions.
9 changes: 9 additions & 0 deletions src/compiler/flx_core/flx_beta.ml
Original file line number Diff line number Diff line change
Expand Up @@ -421,10 +421,19 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
btyp_variant (List.combine ss (List.map br ls))

| BTYP_polyvariant ts ->
let ctors = List.fold_left (fun acc term -> match term with
| `Ctor (s,t) -> (s,br t)::acc
| `Base t -> match br t with
| BTYP_variant ts -> ts @ acc
| _ -> print_endline ("Reduction of polyvariant failed"); assert false
) [] ts
in btyp_variant ctors
(*
btyp_polyvariant (List.map (fun k -> match k with
| `Ctor (s,t) -> `Ctor (s, br t)
| `Base t -> `Base (br t)
) ts)
*)

| BTYP_type_set ls -> btyp_type_set (List.map br ls)

Expand Down
4 changes: 2 additions & 2 deletions src/compiler/flx_core/flx_btype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1172,8 +1172,8 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) ?(f_kind=fun k->k) = funct

| BTYP_fix (i,k) ->
let k' = f_kind k in
if k <> k' then print_endline ("Flx_btype.map changing metatype from " ^ Flx_kind.sk k ^ " to " ^ Flx_kind.sk k');
btyp_fix i (f_kind k')
(* if k <> k' then print_endline ("Flx_btype.map changing metatype from " ^ Flx_kind.sk k ^ " to " ^ Flx_kind.sk k'); *)
btyp_fix i k'

| BTYP_tuple_cons (a,b) -> btyp_tuple_cons (f_btype a) (f_btype b)
| BTYP_tuple_snoc (a,b) -> btyp_tuple_snoc (f_btype a) (f_btype b)
Expand Down
16 changes: 11 additions & 5 deletions src/compiler/flx_core/flx_type_fun.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,9 @@ open Flx_kind
let adjust bsym_table t = Flx_btype_rec.adjust_fixpoint t

let rec type_apply beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) f arg =
(*
print_endline ("Type apply " ^ Flx_btype.st f ^ " to " ^ Flx_btype.st arg);
*)
match f with

(* TYPEFUN REFERENCE *)
Expand Down Expand Up @@ -70,7 +73,7 @@ let rec type_apply beta_reduce' calltag counter bsym_table sr depth (termlist: (
begin match bbdcl with
| Flx_bbdcl.BBDCL_type_alias (bvs, alias) ->
let salias = Flx_btype_subst.tsubst sr bvs ts alias in
type_apply beta_reduce' calltag counter bsym_table sr depth termlist alias arg
type_apply beta_reduce' calltag counter bsym_table sr depth termlist salias arg
| _ -> assert false
end
with Not_found ->
Expand All @@ -80,14 +83,13 @@ let rec type_apply beta_reduce' calltag counter bsym_table sr depth (termlist: (

(* TYPE LAMBDA *)
| BTYP_type_function (ps,r,body) ->
(* print_endline ("TYPE LAMBDA body " ^ Flx_btype.st body); *)
(* Fixpoint handling here *)
let appl = Flx_btype.btyp_type_apply (f, arg) in
begin match Flx_type_list_index.type_list_index counter bsym_table termlist appl with
| Some j ->
let t = btyp_fix (j-depth) r in
(*
print_endline ("Flx_type_fun: installing fixpoint " ^ Flx_btype.st t);
*)
(* print_endline ("Flx_type_fun: installing fixpoint " ^ Flx_btype.st t); *)
t
| None ->
(* NOTE: the typefun term MUST be alpha converted here so the substitution does not lead to false captures in NESTED
Expand All @@ -114,7 +116,8 @@ if not (Flx_btype.complete_type arg) then print_endline ("Type lambda argument i
let params' =
match ps with
| [] -> []
| [i,_] -> [i,arg]
| [i,_] -> (* print_endline ("Variable " ^ string_of_int i ^ " to be replaced with arg= " ^ Flx_btype.st arg); *)
[i,arg]
| _ ->
match arg with
| BTYP_type_tuple ts ->
Expand All @@ -131,7 +134,10 @@ if not (Flx_btype.complete_type arg) then print_endline ("Type lambda argument i
in
if not (Flx_btype.complete_type body) then print_endline ("Type lambda body is not complete! \n" ^ Flx_btype.st body);
let t' = list_subst counter params' body in
(* print_endline ("** After Substitution = " ^ Flx_btype.st t'); *)
(* NOTE: we didn't adjust the fixpoint if there is one, but we HAVE to do that after beta-reduction! *)
let t' = beta_reduce' calltag counter bsym_table sr depth ((appl,depth)::termlist) t' in
(* print_endline ("** FINAL RESULT = " ^ Flx_btype.st t'); *)
t'
| _ -> assert false (* alpha convert can't fail here *)
end
Expand Down
10 changes: 8 additions & 2 deletions src/compiler/flx_opt/flx_tailit.ml
Original file line number Diff line number Diff line change
Expand Up @@ -492,8 +492,14 @@ print_endline ("tailit:asgn2 assign to projection");
aux tail (x::res)
end

| BEXE_fun_return (sr,(BEXPR_apply((BEXPR_closure (i,ts),_),a),_)) :: tail -> assert false

(* NOTE: this was previously considered a bug, probably because a general apply
of a closure should have reduced to a direct apply,
but somehow the reduction has not occured with the fixpoint operator on functions
.. it's clearly a sequencing issue, the fixpoint operation is happening AFTER
the reduction step? In any case the case does occur and can be handled so
I'm re-enabling it
*)
| BEXE_fun_return (sr,(BEXPR_apply((BEXPR_closure (i,ts),_),a),_)) :: tail (* -> assert false *)
| BEXE_fun_return (sr,(BEXPR_apply_direct(i,ts,a),_)) :: tail

when (i)=(this)
Expand Down
4 changes: 2 additions & 2 deletions src/web/tut/func_01.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,8 @@ fun f(x:int) = {
return g;
}
@
The function @{f} here has type {int -> (long -> long)}. This type is
the same as {int -> long -> long} since the arrow operator is right
The function @{f} here has type @{int -> (long -> long)}. This type is
the same as @{int -> long -> long} since the arrow operator is right
associative. There's a simpler way to write the function @{f}:
@felix
fun f(x:int) (y:long) => x.long + y;
Expand Down
2 changes: 1 addition & 1 deletion src/web/tut/polymorphism_01.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ C bindings can be polymorphic too:
type vector[T] = "::std::vector<?1>";
proc push_back[T]: vector[T] * T = "$1.push_back($2)";
@
In the C code {?1}, {?2} represent the
In the C code @{?1}, @{?2} represent the
first and second type variables.

@h2 Overloading
Expand Down
2 changes: 1 addition & 1 deletion src/web/tut/polymorphism_02.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ fun f: !integers * !integers -> int = "f($1, $2)" requires myf;

The reason this is <em>so</em> useful is that if we just lifted the
signature of @{f} from C, we'd be ignoring the fact that the C programmer
has automatic conversions and can call {f(42L, 23u)}, which would
has automatic conversions and can call @{f(42L, 23u)}, which would
fail in Felix because it has no automatic conversions. The user
would have to cast every argument to exactly the right type which is
not practical. By using constrained polymorphism, we can make
Expand Down
2 changes: 1 addition & 1 deletion src/web/tut/string_01.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ See <a href="/share/lib/std/strings/string.fdoc">string</a> module.

@h1 Concept.

Felix uses a binding to the C++ string datatype {::std::basic_string&lt;char&gt;}.
Felix uses a binding to the C++ string datatype @{::std::basic_string&lt;char&gt;}.



Expand Down

0 comments on commit 087fa8a

Please sign in to comment.