Skip to content

Commit

Permalink
Fudge up things so they work with _borrowed.
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed Dec 24, 2021
1 parent 87e2b26 commit bb32e4f
Show file tree
Hide file tree
Showing 31 changed files with 140 additions and 155 deletions.
Binary file modified pdfs/felix.pdf
Binary file not shown.
30 changes: 21 additions & 9 deletions src/compiler/flx_bind/flx_bind_expression.ml
Original file line number Diff line number Diff line change
Expand Up @@ -210,15 +210,6 @@ print_endline ("Case number " ^ si index);
| `EXPR_cond (sr,(c,t,f)) ->
bexpr_cond (be c) (be t) (be f)

| `EXPR_loan (sr,e) ->
let e,t = be e in
begin match t with
| BTYP_uniq t ->
bexpr_coerce ((e,t), btyp_borrowed t)
| BTYP_borrowed _ -> e,t
| t -> bexpr_coerce ((e,t), btyp_borrowed t)
end

| `EXPR_label (sr,label) ->
let maybe_index = lookup_label_in_env state bsym_table env sr label in
begin match maybe_index with
Expand Down Expand Up @@ -1394,6 +1385,27 @@ print_endline ("CLASS NEW " ^sbt bsym_table cls);
| `EXPR_map (sr,f,a) ->
handle_map sr (be f) (be a)

(* generic loan routine *)
| `EXPR_apply (sr,(`EXPR_name (_,"loan",[]), e)) ->
let _,t as x = be e in
begin match t with
| BTYP_uniq t ->
bexpr_coerce (x, btyp_borrowed t)
| BTYP_borrowed _ -> x
| t -> bexpr_coerce (x, btyp_borrowed t)
end

(* generic share routine *)
| `EXPR_apply (sr,(`EXPR_name (_,"share",[]), e)) ->
let _,t as x = be e in
begin match t with
| BTYP_uniq t ->
bexpr_coerce (x, t)
| BTYP_borrowed t -> bexpr_coerce (x, t)
| t -> x
end


(* generic str routine *)
| `EXPR_apply (sr,(`EXPR_name (_,"_strr",[]), a)) ->
let be rs e = bind_expr env rs e [] in
Expand Down
3 changes: 1 addition & 2 deletions src/compiler/flx_bind/flx_overload.ml
Original file line number Diff line number Diff line change
Expand Up @@ -203,13 +203,11 @@ if name = debugid then print_endline "Trying unification";
maybe_specialisation_with_dvars bsym_table counter eqns !dvars
else try Some (unification bsym_table counter eqns !dvars) with Not_found -> None
in
(*
if name = debugid then
begin match result with
| None -> print_endline "Does not unify"
| Some mgu -> print_endline ("UNIFIES with MGU = " ^ string_of_varlist bsym_table mgu)
end;
*)
result


Expand Down Expand Up @@ -330,6 +328,7 @@ print_endline (" .. found tpattern .. analysing .. ");
type_of_tpattern counter t
| KND_generic (* overload treats this as a type variable in this routine *)
| KND_linear
| KND_borrowed
| KND_type
| KND_unitsum
| KND_compactlinear
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_bind/flx_tconstraint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^":
| KND_generic (* treated as ordinary type variable here *)
| KND_type
| KND_linear
| KND_borrowed
| KND_unitsum (* well this is wrong, it IS a constraint! *)
| KND_compactlinear
| KND_function _
Expand Down
3 changes: 1 addition & 2 deletions src/compiler/flx_core/flx_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ and suffixed_name_t =
* union, and the type ordinary procedure types return. There are no values
* of this type. *)
and kindcode_t =
| KND_borrowed (* borrowed type *)
| KND_type (* sharable (nonlinear) type *)
| KND_linear (* top level kind for types *)
| KND_unitsum
Expand Down Expand Up @@ -194,7 +195,6 @@ and expr_t = [
| `EXPR_ref of Flx_srcref.t * expr_t
| `EXPR_rref of Flx_srcref.t * expr_t
| `EXPR_wref of Flx_srcref.t * expr_t
| `EXPR_loan of Flx_srcref.t * expr_t
| `EXPR_likely of Flx_srcref.t * expr_t
| `EXPR_unlikely of Flx_srcref.t * expr_t
| `EXPR_new of Flx_srcref.t * expr_t
Expand Down Expand Up @@ -845,7 +845,6 @@ let src_of_expr (e : expr_t) = match e with
| `EXPR_ref (s,_)
| `EXPR_rref (s,_)
| `EXPR_wref (s,_)
| `EXPR_loan (s,_)
| `EXPR_likely (s,_)
| `EXPR_unlikely (s,_)
| `EXPR_literal (s,_)
Expand Down
1 change: 1 addition & 0 deletions src/compiler/flx_core/flx_btype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -902,6 +902,7 @@ let bbool v = BBOOL v
let rec bmt msg mt = match mt with
| Flx_ast.KND_type -> kind_type
| Flx_ast.KND_linear -> kind_linear
| Flx_ast.KND_borrowed -> kind_borrowed
| Flx_ast.KND_compactlinear-> kind_compactlinear
| Flx_ast.KND_unitsum -> kind_unitsum
| Flx_ast.KND_nat -> kind_nat
Expand Down
2 changes: 0 additions & 2 deletions src/compiler/flx_core/flx_maps.ml
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,6 @@ let full_map_expr fi ft fe (e:expr_t):expr_t = match e with
| `EXPR_coercion (sr, (x,t)) -> `EXPR_coercion (sr,(fe x, ft t))
| `EXPR_variant_subtype_match_coercion (sr, (x,t)) -> `EXPR_variant_subtype_match_coercion (sr,(fe x, ft t))
| `EXPR_suffix (sr,(qn,t)) -> `EXPR_suffix (sr,(qn, ft t))
| `EXPR_loan (sr,e) -> `EXPR_loan (sr, fe e)
| `EXPR_intersect (sr,es) -> `EXPR_intersect (sr, List.map fe es)
| `EXPR_union (sr,es) -> `EXPR_union(sr, List.map fe es)
| `EXPR_isin (sr,(a,b)) -> `EXPR_isin (sr, (fe a, fe b))
Expand Down Expand Up @@ -267,7 +266,6 @@ let iter_expr f (e:expr_t) =
| `EXPR_get_tuple_last (_,x)
| `EXPR_remove_fields (_,x,_)
| `EXPR_getall_field (_,x,_)
| `EXPR_loan (_,x)
-> f x

| `EXPR_letin (_,(_,a,b))
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,6 @@ and string_of_expr (e:expr_t) =
| `EXPR_ref (_,e) -> "&" ^ "(" ^ se e ^ ")"
| `EXPR_rref (_,e) -> "rref" ^ "(" ^ se e ^ ")"
| `EXPR_wref (_,e) -> "wref" ^ "(" ^ se e ^ ")"
| `EXPR_loan (_,e) -> "loan(" ^ se e ^ ")"

| `EXPR_likely (_,e) -> "likely" ^ "(" ^ se e ^ ")"
| `EXPR_unlikely (_,e) -> "unlikely" ^ "(" ^ se e ^ ")"
Expand Down Expand Up @@ -355,6 +354,7 @@ and str_of_kindcode k : string =
match k with
| KND_type -> "TYPE"
| KND_linear -> "LINEAR"
| KND_borrowed -> "BORROWED"
| KND_unitsum -> "UNITSUM"
| KND_compactlinear -> "COMPACTLINEAR"
| KND_bool -> "BOOL"
Expand Down
42 changes: 9 additions & 33 deletions src/compiler/flx_core/flx_unify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ let nominal_subtype bsym_table lhs rhs =

(* LHS ge RHS, parameter supertype of argument *)
let rec solve_subtypes nominal_subtype counter lhs rhs dvars (s:vassign_t option ref) (add_eq:reladd_t) (add_ge:reladd_t) =
(*
print_endline ("Solve subtypes " ^ Flx_btype.str_of_btype lhs ^ " >=? " ^ Flx_btype.str_of_btype rhs);
*)
try nominal_subtype lhs rhs
with Not_found ->

Expand All @@ -55,31 +58,13 @@ let rec solve_subtypes nominal_subtype counter lhs rhs dvars (s:vassign_t option
add_ge (t1,t2)


(* WARNING: HACK! SPECIAL RULES FOR UNIQUE TYPES.
We want a function accepting a T value to also accept
a uniq T; throwing away the uniq is safe!
We also want the same idea to work under pointers.
For values, we do that and also allow the usual value subtyping at
the same time.
For pointers, the read/write property subtypes, but
the pointed at value does not, except for uniq.
*)

| BTYP_ptr (`W,t1,[]), BTYP_ptr (`W,BTYP_uniq t2,[])
| BTYP_ptr (`W,t1,[]), BTYP_ptr (`RW,BTYP_uniq t2,[])
(*
| BTYP_rref t1, BTYP_rref (BTYP_uniq t2)
| BTYP_rref t1, BTYP_pointer (BTYP_uniq t2)
*)
-> add_eq (t1,t2)

(* here we throw away uniq part of argument type passing a value *)
| BTYP_borrowed t1, BTYP_uniq t2 -> add_ge (t1,t2)

| BTYP_type_var _, BTYP_uniq _ -> add_eq (lhs,rhs) (* hack to assign type variable *)
| t1, BTYP_uniq t2 -> add_ge (t1,t2)

| BTYP_borrowed _, BTYP_type_var _ -> add_eq (lhs, rhs) (* hack to assign type variable *)
| BTYP_borrowed t1, t2 -> add_ge (t1,t2)

(* argument type t must be a subtype of each type of the intersection parameter *)
Expand Down Expand Up @@ -188,16 +173,6 @@ let rec solve_subtypes nominal_subtype counter lhs rhs dvars (s:vassign_t option
add_eq (l,r);
add_eq (machl, machr);

(*
(* these special rules say a pointer &t is a subtype of a clt pointer <_,t> *)
| BTYP_cltpointer (lm,l), BTYP_pointer (t)
| BTYP_cltrref (lm,l), BTYP_pointer (t)
| BTYP_cltwref (lm,l), BTYP_pointer (t)
| BTYP_cltrref (lm,l), BTYP_rref (t)
| BTYP_cltwref (lm,l), BTYP_wref (t)
->
(* add_eq (lm,t); *) add_eq (l,t)
*)

| BTYP_function (dl,cl), BTYP_linearfunction (dr,cr)
| BTYP_linearfunction (dl,cl), BTYP_linearfunction (dr,cr)
Expand Down Expand Up @@ -678,7 +653,8 @@ let maybe_specialisation_with_dvars bsym_table counter eqns dvars =
let nominal_subtype lhs rhs = nominal_subtype bsym_table lhs rhs in
let eqns = List.map (fun x -> `Ge, x) eqns in
try Some (unif nominal_subtype counter eqns dvars)
with Not_found -> None
with Not_found ->
None

(* DERIVED *)
let maybe_specialisation bsym_table counter eqns =
Expand Down
4 changes: 0 additions & 4 deletions src/compiler/flx_desugar/flx_desugar_expr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -258,10 +258,6 @@ let rec rex rst_with_ret mkreqs map_reqs (state:desugar_state_t) name (e:expr_t)
let l1,x1 = rex e in
l1, `EXPR_ainj (sr,x1, t)

| `EXPR_loan (sr,e) ->
let l1,x1 = rex e in
l1, `EXPR_loan (sr,x1)

| `EXPR_not (sr,e) ->
let l1, x1 = rex e in
l1, `EXPR_not (sr,x1)
Expand Down
1 change: 0 additions & 1 deletion src/compiler/flx_desugar/flx_desugar_pat.ml
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,6 @@ let rec subst (vars:psym_table_t) (e:expr_t) mv : expr_t =
| `EXPR_union _
| `EXPR_isin _ (* only used in type constraints *)
| `EXPR_callback _
| `EXPR_loan _
->
let sr = src_of_expr e in
clierrx "[flx_desugar/flx_desugar_pat.ml:107: E341] " sr
Expand Down
1 change: 0 additions & 1 deletion src/compiler/flx_desugar/flx_macro.ml
Original file line number Diff line number Diff line change
Expand Up @@ -618,7 +618,6 @@ and expand_expr recursion_limit local_prefix seq (macros:macro_dfn_t list) (e:ex
| `EXPR_ref (sr, e1) -> `EXPR_ref (sr, me e1)
| `EXPR_rref (sr, e1) -> `EXPR_rref (sr, me e1)
| `EXPR_wref (sr, e1) -> `EXPR_wref (sr, me e1)
| `EXPR_loan (sr, e1) -> `EXPR_loan (sr, me e1)
| `EXPR_likely (sr, e1) -> `EXPR_likely (sr, me e1)
| `EXPR_unlikely (sr, e1) -> `EXPR_unlikely (sr, me e1)
| `EXPR_new (sr, e1) -> `EXPR_new (sr, me e1)
Expand Down
3 changes: 1 addition & 2 deletions src/compiler/flx_desugar/flx_sex2flx.ml
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ let rec xsr x : Flx_srcref.t =
and kind_of_sex sr x : kindcode_t =
let ki k = kind_of_sex sr k in
match x with
| Lst [Id "ast_name"; sr; Str "BORROWED"; Lst []] -> KND_borrowed
| Lst [Id "ast_name"; sr; Str "LINEAR"; Lst []] -> KND_linear
| Lst [Id "ast_name"; sr; Str "TYPE"; Lst []] -> KND_type
| Lst [Id "ast_name"; sr; Str "UNITSUM"; Lst []] -> KND_unitsum
Expand Down Expand Up @@ -441,8 +442,6 @@ print_endline ("Processing ast_name "^xid id^" in xexpr");
`EXPR_deref (xsr sr,ex e)
| Lst [Id "ast_ref"; sr; e] -> `EXPR_ref (xsr sr,ex e)

| Lst [Id "ast_loan"; sr; e] -> `EXPR_loan (xsr sr, ex e)

| Lst [Id "ast_rref"; sr; e] -> `EXPR_rref(xsr sr, ex e)
| Lst [Id "ast_wref"; sr; e] -> `EXPR_wref(xsr sr, ex e)

Expand Down
26 changes: 23 additions & 3 deletions src/compiler/flx_frontend/flx_getset.ml
Original file line number Diff line number Diff line change
Expand Up @@ -102,12 +102,32 @@ print_endline ("Find once for expresssion " ^ Flx_print.sbe bsym_table e ^ ", ty

(* This will ONLY work correctly if coercions on tuples have
been expanded ...
| BEXPR_coerce ((_,BTYP_uniq _) _), BTYP_borrowed _),_
*)
| BEXPR_coerce ((_,(*BTYP_uniq*) _), BTYP_borrowed _),_ ->
| BEXPR_coerce ((_,BTYP_uniq t1), BTYP_borrowed t2),_
when t1 = t2
->
(*
print_endline ("Skipping expression coerced to borrowed");
begin
if t1 = t2 then
print_endline ("Skipping expression type " ^Flx_print.sbt bsym_table t1 ^ " coerced to borrowed: " ^ Flx_print.sbe bsym_table e)
else
print_endline ("Skipping WEIRD expression coerced to borrowed or shared")
end;
*)
()
| BEXPR_coerce ((_,BTYP_uniq t1), t2),_
when t1 = t2
->
(*
begin
if t1 = t2 then
print_endline ("Skipping expression type uniq " ^Flx_print.sbt bsym_table t1 ^ " coerced to shared: " ^ Flx_print.sbe bsym_table e)
else
print_endline ("Skipping WEIRD expression coerced to borrowed or shared")
end;
*)
()
()

(*
| BEXPR_apply_prim (i,_,(_,argt)),_
Expand Down

0 comments on commit bb32e4f

Please sign in to comment.