From 28b098876f91c5c6857c95efc622a9095aefbcb1 Mon Sep 17 00:00:00 2001 From: skaller Date: Tue, 6 Feb 2024 13:03:52 +1100 Subject: [PATCH] View mode pointers. Aka propagating const. --- src/compiler/flx_bind/flx_bind_apply.ml | 29 ++++--- src/compiler/flx_bind/flx_bind_expression.ml | 12 +-- src/compiler/flx_bind/flx_bind_type.ml | 7 +- src/compiler/flx_bind/flx_bind_type_index.ml | 4 +- src/compiler/flx_bind/flx_cal_apply.ml | 19 +++-- src/compiler/flx_bind/flx_cal_ret_type.ml | 2 - src/compiler/flx_bind/flx_guess_meta_type.ml | 4 +- .../flx_bind/flx_inner_type_of_index.ml | 1 - src/compiler/flx_bind/flx_overload.ml | 1 + src/compiler/flx_bind/flx_resolve_overload.ml | 4 +- src/compiler/flx_bind/flx_tconstraint.ml | 1 + .../flx_bind/flx_typecode_of_btype.ml | 2 +- src/compiler/flx_bind/flx_typeset.ml | 2 +- src/compiler/flx_core/flx_alpha.ml | 4 +- src/compiler/flx_core/flx_ast.ml | 1 + src/compiler/flx_core/flx_beta.ml | 4 +- src/compiler/flx_core/flx_bexpr.ml | 2 +- src/compiler/flx_core/flx_btype.ml | 75 ++++++++++++++++--- src/compiler/flx_core/flx_btype.mli | 13 +++- src/compiler/flx_core/flx_btype_kind.ml | 36 +++++---- src/compiler/flx_core/flx_btype_occurs.ml | 6 +- src/compiler/flx_core/flx_btype_rec.ml | 2 +- src/compiler/flx_core/flx_btype_subst.ml | 23 ++++-- src/compiler/flx_core/flx_fold.ml | 3 +- src/compiler/flx_core/flx_kind.ml | 21 +++++- src/compiler/flx_core/flx_print.ml | 3 +- src/compiler/flx_core/flx_typeeq.ml | 5 +- src/compiler/flx_core/flx_unify.ml | 24 ++++-- src/compiler/flx_cpp_backend/flx_name.ml | 4 +- src/compiler/flx_cpp_backend/flx_tgen.ml | 2 +- src/compiler/flx_desugar/flx_sex2flx.ml | 3 + src/compiler/flx_frontend/flx_monoclass.ml | 9 +++ src/compiler/flx_frontend/flx_polyinst.ml | 9 +++ src/compiler/flx_frontend/flx_reparent.ml | 9 +++ src/compiler/flx_frontend/flx_treg.ml | 2 +- src/compiler/flx_frontend/flx_typeclass.ml | 4 +- src/packages/grammar.fdoc | 2 +- src/packages/pointers.fdoc | 16 ++-- src/packages/rtl.fdoc | 3 + 39 files changed, 271 insertions(+), 102 deletions(-) diff --git a/src/compiler/flx_bind/flx_bind_apply.ml b/src/compiler/flx_bind/flx_bind_apply.ml index 7c6ead539..e3ab9d7c9 100644 --- a/src/compiler/flx_bind/flx_bind_apply.ml +++ b/src/compiler/flx_bind/flx_bind_apply.ml @@ -129,7 +129,7 @@ let cal_bind_apply *) let (ea,ta as a) = be a' in (* - print_endline ("[bind_expression] GENERAL APPLY " ^ + print_endline ("[bind_apply] GENERAL APPLY " ^ Flx_print.string_of_expr f' ^ " to " ^ Flx_print.string_of_expr a' ^ ", type= " ^ Flx_print.sbt bsym_table ta ); *) @@ -143,6 +143,8 @@ let cal_bind_apply (* if not (complete_type ta) then print_endline ("*************>>>>>>>>> reduced Apply argument type is not complete!!" ^ sbt bsym_table ta); +*) +(* print_endline ("Bound argument " ^ Flx_print.sbe bsym_table a ^ " type=" ^ Flx_btype.st ta); *) (* ---------------------------------------------------------- *) @@ -180,22 +182,24 @@ let cal_bind_apply with Flx_exceptions.TryNext -> - (* - print_endline ("Can't interpret apply function "^string_of_expr f'^" as projection, trying as an actual function"); - *) +(* + print_endline ("Can't interpret apply function "^Flx_print.string_of_expr f'^" as projection, trying as an actual function"); +*) try begin (* as a function *) try let bt,tf as f = match Flx_typing2.qualified_name_of_expr f' with | Some name -> (* -print_endline ("Checking if " ^ Flx_print.string_of_qualified_name name ^ " is a function"); if match name with | `AST_name (_,"accumulate",_) -> true | _ -> false then begin print_endline "Trying to bind application of accumulate"; end; *) let srn = src_of_qualified_name name in begin +(* +print_endline ("Checking if " ^ Flx_print.string_of_qualified_name name ^ " is a function with lookup_qn_with_sig'"); +*) try let result = (lookup_qn_with_sig' state bsym_table sr srn env rs name (ta::sigs)) in (* @@ -205,14 +209,17 @@ print_endline (" WITH TYPE " ^ Flx_print.sbt bsym_table (snd result)); result with | Not_found -> failwith "lookup_qn_with_sig' threw Not_found" - | exn -> raise exn + | exn -> (* print_endline ("NOPE, lookup_qn_with_sig' barfed"); *) raise exn end | None -> begin +(* +print_endline ("Lookup qn with sig' failed to find a function, lets try bind expression directly in case the name is a variable of function type"); +*) try bind_expression' state bsym_table env rs f' (a :: args) with | Not_found -> failwith "bind_expression' XXX threw Not_found" - | exn -> raise exn + | exn -> (* print_endline ("Nope, bind expression also failed"); *) raise exn end in (* @@ -229,17 +236,15 @@ print_endline (" WITH TYPE " ^ Flx_print.sbt bsym_table (snd result)); -> begin try (* - print_endline (" ** Bound LHS of application as function!"); + print_endline (" ** Bound LHS of application as function! Calling cal_apply to bind it!"); *) let result = cal_apply state bsym_table sr rs f a in (* - print_endline (" ** application of function done!"); + print_endline (" ** (after cal_apply): application of function done!\n"); *) result with exn -> -(* - print_endline ("!!! cal_apply failed"); -*) + (* print_endline ("!!! cal_apply failed"); *) (* NOTE: this isn't necessarily an error if used in tentative binding *) raise exn end (* NOTE THIS CASE HASN'T BEEN CHECKED FOR POLYMORPHISM YET *) diff --git a/src/compiler/flx_bind/flx_bind_expression.ml b/src/compiler/flx_bind/flx_bind_expression.ml index 646035603..63d5b3586 100644 --- a/src/compiler/flx_bind/flx_bind_expression.ml +++ b/src/compiler/flx_bind/flx_bind_expression.ml @@ -584,7 +584,7 @@ assert false | `EXPR_case_index (sr,e) -> let (e',t) as e = be e in begin match t with - | BTYP_type_var (_,k) + | BTYP_type_var (_,_,k) | BTYP_inst (_,_,_,k) when Flx_kind.kind_ge2 Flx_kind.KIND_compactlinear k -> () @@ -669,7 +669,7 @@ print_endline ("Evaluating EXPPR_typed_case index=" ^ si v ^ " type=" ^ string_o *) bexpr_unitsum_case v k (* const ctor *) end - | BTYP_type_var (_,Flx_kind.KIND_unitsum) -> + | BTYP_type_var (_,_,Flx_kind.KIND_unitsum) -> bexpr_const_case (v, t) (* const ctor *) | BTYP_compactsum ls @@ -1338,14 +1338,14 @@ print_endline ("LOOKUP 9A: varname " ^ si i); end | `EXPR_deref (sr,e') -> -(* -print_endline ("Binding _deref .. " ^ string_of_expr e); -*) let e,t = be e' in begin match unfold "flx_lookup" t with | BTYP_ptr (`R,t',_) | BTYP_ptr (`RW,t',_) -> bexpr_deref t' (e,t) - | BTYP_ptr (`V,t',_) -> bexpr_deref t' (e,t) + | BTYP_ptr (`V,t',_) -> + (* print_endline ("deref of V mode pointer detected"); *) + let vt = Flx_btype.viewify_type t' in + bexpr_deref vt (e,t) | _ -> clierrx "[flx_bind/flx_lookup.ml:4856: E207] " sr ("[bind_expression'] Dereference non pointer, type " ^ sbt bsym_table t) diff --git a/src/compiler/flx_bind/flx_bind_type.ml b/src/compiler/flx_bind/flx_bind_type.ml index 25744a669..d630181cf 100644 --- a/src/compiler/flx_bind/flx_bind_type.ml +++ b/src/compiler/flx_bind/flx_bind_type.ml @@ -491,7 +491,12 @@ print_endline (" ***** Bound `TYP_apply: " ^ Flx_btype.st x ); | `TYP_name (sr,s,[]) when List.mem_assoc s rs.as_fixlist -> let level, kind = List.assoc s rs.as_fixlist in - btyp_fix (level - rs.depth) kind + let fx = btyp_fix (level - rs.depth) kind in +(* +print_endline ("######################## Flx_bind_type.TYP_name fixpoint from 'as' name `"^s^"`: " ^ Flx_btype.st fx); +*) + fx + | `TYP_name (sr,s,[]) when List.mem_assoc s params -> let t = List.assoc s params in diff --git a/src/compiler/flx_bind/flx_bind_type_index.ml b/src/compiler/flx_bind/flx_bind_type_index.ml index 62daee293..577a54b4d 100644 --- a/src/compiler/flx_bind/flx_bind_type_index.ml +++ b/src/compiler/flx_bind/flx_bind_type_index.ml @@ -116,7 +116,9 @@ print_endline ("Bind type index ts adjusted"); then begin let mt = Flx_guess_meta_type.guess_meta_type state bsym_table bt index in (* - print_endline ("Flx_bind_type_index: fixpoint, meta type calculated by guess_meta_type!"); + print_endline ("@@@@@@@@@@@@@ Flx_bind_type_index: fixpoint, meta type calculated by guess_meta_type!" ^ Flx_kind.sk mt); + let mt = Flx_kind.kind_max2 mt Flx_kind.kind_type in + (* A fix point has to at least be kind type! *) *) let fixated = btyp_fix ((List.assoc index rs.type_alias_fixlist)-rs.depth) mt in fixated diff --git a/src/compiler/flx_bind/flx_cal_apply.ml b/src/compiler/flx_bind/flx_cal_apply.ml index 2b6431956..46e56b098 100644 --- a/src/compiler/flx_bind/flx_cal_apply.ml +++ b/src/compiler/flx_bind/flx_cal_apply.ml @@ -30,20 +30,19 @@ let cal_apply' build_env state bsym_table be sr ((be1,t1) as tbe1) ((be2,t2) as tbe2) = let original_argument_type = t2 in + (* - if t1 <> t1' || t2 <> t2' then begin -print_endline ("cal_apply' BEFORE NORMALISE, fn = " ^ sbt bsym_table t1' ^ " arg=" ^ sbt bsym_table t2'); -print_endline ("cal_apply', AFTER NORMALISE, fn = " ^ sbt bsym_table t1 ^ " arg=" ^ sbt bsym_table t2); - end - ; +print_endline ("\n%%%%%%%%\nFlx_cal_apply: Function type \n" ^ Flx_btype.st t1 ^ "\nArgument type\n`" ^ Flx_btype.st t2 ^ "\n"); *) - 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 - + +(* +print_endline ("\n%%%%%%%%\nFlx_cal_apply AFTER BETA: Function type \n" ^ Flx_btype.st t1 ^ "\nArgument type\n`" ^ Flx_btype.st t2 ^ "\n"); +*) let result_type,reorder = - let argt = unfold "flx_cal_apply" t1 in - match argt with + let funt = (* unfold "flx_cal_apply" *) t1 in (* the UNFOLD IS BUGGED IT PUTS THE WRONG KIND ON THE FIXPOINT *) + match funt with | BTYP_lineareffector(paramt,_,result_type) | BTYP_linearfunction (paramt,result_type) | BTYP_effector(paramt,_,result_type) @@ -55,7 +54,7 @@ print_endline ("cal_apply', AFTER NORMALISE, fn = " ^ sbt bsym_table t1 ^ " arg= *) let rel = Flx_unify.compare_sigs bsym_table state.counter paramt t2 in (* - print_endline ("Function domain " ^ sbt bsym_table paramt ^ " " ^str_of_cmp rel ^ " argument type " ^ sbt bsym_table t2); + print_endline ("Function domain " ^ sbt bsym_table paramt ^ "\n " ^str_of_cmp rel ^ "\n argument type " ^ sbt bsym_table t2); *) match rel with | `Equal -> diff --git a/src/compiler/flx_bind/flx_cal_ret_type.ml b/src/compiler/flx_bind/flx_cal_ret_type.ml index f8febeec1..52ffc1ad5 100644 --- a/src/compiler/flx_bind/flx_cal_ret_type.ml +++ b/src/compiler/flx_bind/flx_cal_ret_type.ml @@ -45,8 +45,6 @@ print_endline ("+++++++++++++++++++++++++++++"); print_endline ("Cal ret type of " ^ id ^ "<" ^ string_of_int index ^ "> at " ^ Flx_srcref.short_string_of_src sr); print_endline ("+++++ UNBOUND return type is " ^ string_of_typecode rt'); begin match rt' with | `TYP_var j when j = index -> print_endline ("RETURN TYPE UNSPECIFIED") | _ -> () end; -*) -(* print_endline ("Trying to bind type .. if function index variable, we get a recurse?"); *) let declared_ret = not (index = (match rt' with `TYP_var k -> k | _ -> 0)) in diff --git a/src/compiler/flx_bind/flx_guess_meta_type.ml b/src/compiler/flx_bind/flx_guess_meta_type.ml index b96956a87..5fb9cdf75 100644 --- a/src/compiler/flx_bind/flx_guess_meta_type.ml +++ b/src/compiler/flx_bind/flx_guess_meta_type.ml @@ -183,6 +183,8 @@ let guess_meta_type state bsym_table bt index : kind = k | SYMDEF_type_alias t -> - guess_metatype sr t + let mt = guess_metatype sr t in + print_endline ("Guess meta type of " ^ Flx_print.string_of_typecode t ^ " as " ^ Flx_kind.sk mt); + mt | _ -> print_endline ("Dunno, assume a type " ^ string_of_symdef entry id vs); assert false diff --git a/src/compiler/flx_bind/flx_inner_type_of_index.ml b/src/compiler/flx_bind/flx_inner_type_of_index.ml index a5002bdf3..73da31307 100644 --- a/src/compiler/flx_bind/flx_inner_type_of_index.ml +++ b/src/compiler/flx_bind/flx_inner_type_of_index.ml @@ -49,7 +49,6 @@ if debug then if List.mem index rs.idx_fixlist then begin if debug then print_endline "inner_typeof+index returning fixpoint"; - (* btyp_fix (-rs.depth) (btyp_type 0) *) btyp_fix (-rs.depth) (Flx_kind.kind_type) end else diff --git a/src/compiler/flx_bind/flx_overload.ml b/src/compiler/flx_bind/flx_overload.ml index 577c69773..8ddca228d 100644 --- a/src/compiler/flx_bind/flx_overload.ml +++ b/src/compiler/flx_bind/flx_overload.ml @@ -329,6 +329,7 @@ print_endline (" .. found tpattern .. analysing .. " ^ string_of_typecode t); | KND_unitsum | KND_compactlinear | KND_function _ + | KND_view | KND_tuple _ -> `TYP_var j',[],[],[],[] | _ -> print_endline ("Flx_overload. Expected KND_tpattern, got " ^ str_of_kindcode tp); diff --git a/src/compiler/flx_bind/flx_resolve_overload.ml b/src/compiler/flx_bind/flx_resolve_overload.ml index 03393760d..a06b1acc7 100644 --- a/src/compiler/flx_bind/flx_resolve_overload.ml +++ b/src/compiler/flx_bind/flx_resolve_overload.ml @@ -257,7 +257,7 @@ end; Hashtbl.iter (fun i j -> print_endline (" Rebind index " ^ si i ^ " -> " ^ si j)) remap_table; *) let rec fbt t = match t with - | Flx_btype.BTYP_type_var (i,mt) -> + | Flx_btype.BTYP_type_var (i,tvm,mt) -> (* print_endline ("Examining bound type variable index " ^ si i); *) @@ -273,7 +273,7 @@ print_endline ("Replaced by vmap: " ^ sbt bsym_table r); (* print_endline ("Not found in vmap, remaping with index remapper: " ^ si j); *) - Flx_btype.btyp_type_var (j, mt) + Flx_btype.btyp_type_varm (j, tvm, mt) end | x -> Flx_btype.map ~f_bid:fi ~f_btype:fbt x in diff --git a/src/compiler/flx_bind/flx_tconstraint.ml b/src/compiler/flx_bind/flx_tconstraint.ml index 3d1bab366..88e06cfff 100644 --- a/src/compiler/flx_bind/flx_tconstraint.ml +++ b/src/compiler/flx_bind/flx_tconstraint.ml @@ -38,6 +38,7 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^": | KND_borrowed | KND_unitsum (* well this is wrong, it IS a constraint! *) | KND_compactlinear + | KND_view | KND_function _ | KND_tuple _ -> bbool true diff --git a/src/compiler/flx_bind/flx_typecode_of_btype.ml b/src/compiler/flx_bind/flx_typecode_of_btype.ml index af2d8fd09..1ef915037 100644 --- a/src/compiler/flx_bind/flx_typecode_of_btype.ml +++ b/src/compiler/flx_bind/flx_typecode_of_btype.ml @@ -36,7 +36,7 @@ let typecode_of_btype ?sym_table:(sym_table=None) bsym_table counter sr (t0:Flx_ let id = Flx_bsym_table.find_id bsym_table i in `TYP_name (sr,id, (List.map tc ts)) - | BTYP_type_var (i,_) -> `TYP_var i + | BTYP_type_var (i,_,_) -> `TYP_var i | BTYP_uniq t -> `TYP_uniq (tc t) (* begin match sym_table with diff --git a/src/compiler/flx_bind/flx_typeset.ml b/src/compiler/flx_bind/flx_typeset.ml index 82ff10dc3..86ca69869 100644 --- a/src/compiler/flx_bind/flx_typeset.ml +++ b/src/compiler/flx_bind/flx_typeset.ml @@ -13,7 +13,7 @@ let is_typeset tss1 = p1.assignments = [] && BidSet.cardinal p1.pattern_vars = 1 && match p1.pattern,v1 with - | BTYP_type_var (i,KIND_type), BTYP_void + | BTYP_type_var (i,_,KIND_type), BTYP_void when i = BidSet.choose p1.pattern_vars -> begin try List.iter (fun (p,v) -> match p,v with diff --git a/src/compiler/flx_core/flx_alpha.ml b/src/compiler/flx_core/flx_alpha.ml index 7f1edc4bf..8f8e1575a 100644 --- a/src/compiler/flx_core/flx_alpha.ml +++ b/src/compiler/flx_core/flx_alpha.ml @@ -6,8 +6,8 @@ let remap map i = try List.assoc i map with Not_found -> i let rec alpha counter map t = match t with - | BTYP_type_var (i, knd) -> - btyp_type_var (remap map i, knd) + | BTYP_type_var (i, m, knd) -> + btyp_type_varm (remap map i, m, knd) | BTYP_type_function (ps,r,b) -> let map = List.fold_left (fun acc (i,_) -> (i, fresh_bid counter)::acc) map ps in diff --git a/src/compiler/flx_core/flx_ast.ml b/src/compiler/flx_core/flx_ast.ml index aeffb133b..8408978dd 100644 --- a/src/compiler/flx_core/flx_ast.ml +++ b/src/compiler/flx_core/flx_ast.ml @@ -79,6 +79,7 @@ and kindcode_t = | KND_tpattern of typecode_t (* | KND_special of string *) | KND_var of string + | KND_view and sortcode_t = diff --git a/src/compiler/flx_core/flx_beta.ml b/src/compiler/flx_core/flx_beta.ml index 815bee5d3..9dda60940 100644 --- a/src/compiler/flx_core/flx_beta.ml +++ b/src/compiler/flx_core/flx_beta.ml @@ -158,7 +158,9 @@ and fixup counter ps body = && i + depth +1 = 0 (* looking inside application, one more level *) -> print_endline "SPECIAL REDUCTION"; (* HACK: meta type of fixpoint guessed *) +(* print_endline ("Flx_beta:fixup:aux: hacking meta type of fixpoint!"); +*) btyp_fix (i+2) (kind_type) (* elide application AND skip under lambda abstraction *) | BTYP_type_function (a,b,c) -> @@ -372,7 +374,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t); | BTYP_ellipsis -> btyp_ellipsis (* not a value type! *) | BTYP_none -> assert false | BTYP_fix _ -> (* print_endline "Returning fixpoint"; *) t - | BTYP_type_var (i,_) -> t + | BTYP_type_var (i,_,_) -> t | BBOOL _ -> t | BTYP_type_function (p,r,b) -> t diff --git a/src/compiler/flx_core/flx_bexpr.ml b/src/compiler/flx_core/flx_bexpr.ml index db3e23bd6..9dac093f0 100644 --- a/src/compiler/flx_core/flx_bexpr.ml +++ b/src/compiler/flx_core/flx_bexpr.ml @@ -178,7 +178,7 @@ let bexpr_deref t ((_,(pt:Flx_btype.t)) as e) : t = | _ -> match pt with | BTYP_ptr (mode,base,_) -> - if base <> t then + if base <> t && mode <> `V then print_endline ("Flx_bexpr: Warning deref of pointer to type " ^ Flx_btype.st base ^ "given type " ^ Flx_btype.st t) ; diff --git a/src/compiler/flx_core/flx_btype.ml b/src/compiler/flx_core/flx_btype.ml index bd3445ae5..dce6c8d9d 100644 --- a/src/compiler/flx_core/flx_btype.ml +++ b/src/compiler/flx_core/flx_btype.ml @@ -18,6 +18,18 @@ type pmode = [ | `V (* view only: propagating read *) ] +let viewify_mode = function + | `RW + | `R + | `V -> `V + | `N + | `W -> `N + +type tvmode = [ + | `N + | `V +] + let str_of_pmode = function | `RW -> "RW" | `R -> "R" @@ -25,6 +37,10 @@ let str_of_pmode = function | `N -> "NULL" | `V -> "V" +let str_of_tvmode = function + | `N -> "normal" + | `V -> "view" + type instkind_t = [ | `Nominal of variance_list_t (* nominal type: primitive or user defined *) | `Alias (* type alias, to be eliminated *) @@ -88,7 +104,7 @@ and t = | BTYP_type_tuple of t list | BTYP_type_function of (bid_t * kind) list * kind * t - | BTYP_type_var of bid_t * kind + | BTYP_type_var of bid_t * tvmode * kind | BTYP_type_apply of t * t (* type_map is NOT a map over a kind, the argument should @@ -174,7 +190,7 @@ let flat_iter (* The first argument of [its] is an index, not a bid. *) (* List.iter (fun (_,t) -> f_btype t) its; *) f_btype b - | BTYP_type_var (_,t) -> () + | BTYP_type_var (_,_,t) -> () (* The first argument of [BTYP_type_var] is just a unique integer, not a * bid. *) | BTYP_type_apply (a,b) -> f_btype a; f_btype b @@ -335,7 +351,7 @@ and str_of_btype typ = String.concat "," (List.map (fun (i,t)->string_of_int i^":"^sk t) ps)^"):"^ sk r^"=("^ s b ^"))" - | BTYP_type_var (i,t) -> "BTYP_type_var("^string_of_int i^":"^sk t^")" + | BTYP_type_var (i,m, t) -> "BTYP_type_var("^string_of_int i^ "-" ^ str_of_tvmode m ^ ":"^sk t^")" | BTYP_type_apply (f,x) -> "BTYP_type_apply("^s f^","^s x^ ")" | BTYP_type_match (v,pats) -> let sa (i,t) = string_of_int i ^ " <- " ^ s t in @@ -385,7 +401,7 @@ let rec islinear_type t = | BTYP_type_apply (BTYP_inst (_,_,_,KIND_function (_,k)),_) | BTYP_typeop (_,_,k) | BTYP_inst (_,_,_,k) - | BTYP_type_var (_,k) -> kind_ge2 KIND_compactlinear k + | BTYP_type_var (_,_,k) -> kind_ge2 KIND_compactlinear k | _ -> false @@ -395,7 +411,7 @@ let rec islinear_type t = let iscopyable_type t = let rec f t = match t with - | BTYP_type_var (_,k) -> + | BTYP_type_var (_,_,k) -> (* this rule says all kinds are copyable except run time values (LINEAR) which are not shareable (TYPE) @@ -638,7 +654,14 @@ let btyp_compactsum ts = let btyp_inst (it,bid, ts,mt) = - BTYP_inst (it,bid, ts,mt) + let t = BTYP_inst (it,bid, ts,mt) in +(* + begin match it,mt with + | _,KIND_type -> () + | _,_ -> print_endline ("Flx_btype:btyp_inst " ^ st t); + end; +*) + t let btyp_finst (bid, ks,dom, cod) = BTYP_finst (bid, ks,dom,cod) @@ -893,6 +916,13 @@ let btyp_cfunction (args, ret) = (** Construct a BTYP_fix type. *) let btyp_fix i mt = +(* + begin match mt with + | KIND_type -> () + | _ -> + print_endline ("$$$$$$$$$ Constructing fixpoint " ^ string_of_int i ^ " kind " ^ sk mt); + end; +*) BTYP_fix (i, mt) (** Construct a BTYP_type_tuple type. *) @@ -911,7 +941,15 @@ let btyp_type_var (bid, t) = if bid = 7141 then print_endline ("Flx_btype: Binding type variable " ^ string_of_int bid ^ ", kind=" ^ Flx_kind.sk t); *) - BTYP_type_var (bid, t) + BTYP_type_var (bid, `N, t) + +let btyp_type_varm (bid, m, t) = +(* +if bid = 7141 then print_endline ("Flx_btype: Binding type variable " ^ string_of_int bid ^ + ", kind=" ^ Flx_kind.sk t); +*) + BTYP_type_var (bid, m, t) + (** Construct a BTYP_type_apply type. *) let btyp_type_apply (f, a) = @@ -965,6 +1003,7 @@ let rec bmt msg mt = match mt with (* this is wrong, we actually need to examine the pattern to find the kind *) | Flx_ast.KND_tpattern t -> kind_type (* print_endline ("BMT tpattern fail " ^ msg); assert false *) | Flx_ast.KND_generic -> kind_type (* requied at least for GADTs to work *) + | Flx_ast.KND_view -> kind_view (* -------------------------------------------------------------------------- *) @@ -1109,19 +1148,24 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) ?(f_kind=fun k->k) = funct | BTYP_borrowed t -> btyp_borrowed (f_btype t) | BTYP_void as x -> x - | BTYP_fix (i,k) -> btyp_fix i (f_kind k) + + | 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') + | 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) | BTYP_type_tuple ts -> btyp_type_tuple (List.map f_btype ts) | BTYP_type_function (its, a, b) -> btyp_type_function (List.map (fun (i,k) -> f_bid i,f_kind k) its, f_kind a, f_btype b) - | BTYP_type_var (i,k) -> btyp_type_var (f_bid i,f_kind k) + | BTYP_type_var (i,m,k) -> btyp_type_varm (f_bid i,m, f_kind k) | BTYP_type_apply (a, b) -> btyp_type_apply (f_btype a, f_btype b) | BTYP_type_map (a, b) -> btyp_type_map (f_btype a, f_btype b) | BTYP_type_match (t,ps) -> let ps = List.map begin fun (tp, t) -> - { tp with + { (* tp with *) pattern = f_btype tp.pattern; pattern_vars = BidSet.map f_bid tp.pattern_vars; assignments = List.map (fun (i, t) -> f_bid i, f_btype t) tp.assignments @@ -1416,3 +1460,14 @@ let contains_alias t : bool = try contains_alias' t; false with | Not_found -> true +let rec viewify_type' t = + let f_btype t = viewify_type' t in + match t with + | BTYP_type_var (i,m,k) -> BTYP_type_var (i, `V, k) + | BTYP_ptr (pm, t, x) -> BTYP_ptr (viewify_mode pm,f_btype t, x) + | t -> map ~f_btype t + +let viewify_type t = + (* print_endline ("Viewify tyype " ^ st t); *) + viewify_type' t + diff --git a/src/compiler/flx_core/flx_btype.mli b/src/compiler/flx_core/flx_btype.mli index 195c75392..3d15ac157 100644 --- a/src/compiler/flx_core/flx_btype.mli +++ b/src/compiler/flx_core/flx_btype.mli @@ -10,7 +10,15 @@ type pmode = [ | `V (* pointer to unit : no read or write *) ] +type tvmode = [ + | `N + | `V +] + + val str_of_pmode: pmode -> string +val str_of_tvmode: tvmode -> string + type instkind_t = [ | `Nominal of Flx_ast.variance_list_t (* nominal type: primitive or user defined *) | `Alias (* type alias, to be eliminated *) @@ -63,7 +71,7 @@ and t = private | BTYP_borrowed of t | BTYP_type_tuple of t list | BTYP_type_function of (bid_t * kind) list * kind * t - | BTYP_type_var of bid_t * kind + | BTYP_type_var of bid_t * tvmode * kind | BTYP_type_apply of t * t | BTYP_type_map of t * t | BTYP_type_match of t * (btpattern_t * t) list @@ -179,6 +187,7 @@ val btyp_fix : int -> kind -> t val btyp_type_tuple : t list -> t val btyp_type_function : (bid_t * kind) list * kind * t -> t val btyp_type_var : bid_t * kind -> t +val btyp_type_varm : bid_t * tvmode * kind -> t val btyp_type_apply : t * t -> t val btyp_type_map : t * t -> t val btyp_type_match : t * (btpattern_t * t) list -> t @@ -229,3 +238,5 @@ val eval_typeop: t ) option ref +val viewify_type: t -> t + diff --git a/src/compiler/flx_core/flx_btype_kind.ml b/src/compiler/flx_core/flx_btype_kind.ml index f59460010..16c7ec67d 100644 --- a/src/compiler/flx_core/flx_btype_kind.ml +++ b/src/compiler/flx_core/flx_btype_kind.ml @@ -14,6 +14,11 @@ and metatype' sr typ : kind = let mt t = metatype' sr t in if not (Flx_btype.iscopyable_type typ) then kind_linear else match typ with + (* pointers that cannoot write *) + | BTYP_ptr (`V,v,_) when mt v = KIND_view -> KIND_view + | BTYP_ptr (`R,v,_) when mt v = KIND_view -> KIND_view + | BTYP_ptr (`N,v,_) when mt v = KIND_view -> KIND_view + | BBOOL _ -> KIND_bool | BTYP_in _ -> KIND_bool @@ -102,7 +107,7 @@ print_endline ("Flx_btype_kind.metatype' case type_apply: " ^ Flx_btype.st typ); ); KIND_type (* HACK *) end - | BTYP_type_var (i,k) -> k + | BTYP_type_var (i,m,k) -> k | BTYP_vinst (index,ts,k) -> k | BTYP_inst (_,index,ts,k) -> k | BTYP_finst (index,ks,dom,cod) -> kind_function (dom, cod) @@ -119,21 +124,24 @@ print_endline ("Flx_btype_kind.metatype' case type_apply: " ^ Flx_btype.st typ); (* Ordinary type expressions *) - | BTYP_tuple _ - | BTYP_array _ - | BTYP_sum _ - | BTYP_rptsum _ + | BTYP_sum ts + | BTYP_tuple ts -> kind_max (kind_type::(List.map mt ts)) + + | BTYP_array (base,index) -> kind_max [kind_type; (mt base); (mt index)] (* not clear index counts here *) + | BTYP_rptsum (rpt, base) -> kind_max [kind_type; (mt rpt); (mt base)] + + | BTYP_cfunction (d,c) + | BTYP_linearfunction (d,c) + | BTYP_lineareffector (d,_,c) + | BTYP_function (d,c) + | BTYP_effector (d,_,c) -> kind_type + + | BTYP_record vs + | BTYP_variant vs -> kind_type | BTYP_typeof _ - | BTYP_cfunction _ - | BTYP_function _ - | BTYP_effector _ - | BTYP_linearfunction _ - | BTYP_lineareffector _ - | BTYP_ptr _ - | BTYP_variant _ - | BTYP_polyvariant _ - | BTYP_record _ + | BTYP_ptr _ (* we already handled the read/write case *) + | BTYP_polyvariant _ (* Too hard lol *) | BTYP_rev _ | BTYP_label diff --git a/src/compiler/flx_core/flx_btype_occurs.ml b/src/compiler/flx_core/flx_btype_occurs.ml index 4059fc254..4fab30e90 100644 --- a/src/compiler/flx_core/flx_btype_occurs.ml +++ b/src/compiler/flx_core/flx_btype_occurs.ml @@ -6,7 +6,7 @@ open Flx_bid let var_i_occurs i t = let rec f_btype t = match t with - | BTYP_type_var (j,_) when i = j -> raise Not_found + | BTYP_type_var (j,_,_) when i = j -> raise Not_found | _ -> Flx_btype.flat_iter ~f_btype t in try @@ -19,7 +19,7 @@ let rec vars_in t = let add_var i = vs := BidSet.add i !vs in let rec f_btype t = match t with - | BTYP_type_var (i,_) -> add_var i + | BTYP_type_var (i,_,_) -> add_var i | _ -> Flx_btype.flat_iter ~f_btype t in f_btype t; @@ -79,7 +79,7 @@ let var_occurs bsym_table t = | BTYP_void | BTYP_fix _ -> () - | BTYP_type_var (k,_) -> if not (List.mem k excl) then raise Not_found + | BTYP_type_var (k,_,_) -> if not (List.mem k excl) then raise Not_found | BTYP_type_function (p,r,b) -> aux' (List.map fst p @ excl) b diff --git a/src/compiler/flx_core/flx_btype_rec.ml b/src/compiler/flx_core/flx_btype_rec.ml index e02160784..ef76fd086 100644 --- a/src/compiler/flx_core/flx_btype_rec.ml +++ b/src/compiler/flx_core/flx_btype_rec.ml @@ -32,7 +32,7 @@ let fix i t = | BTYP_tuple_snoc _ -> assert false | BTYP_none -> assert false | BTYP_ellipsis -> assert false - | BTYP_type_var (k,mt) -> + | BTYP_type_var (k,m,mt) -> if k = i then begin print_endline ("Flx_btype_rec: fixpoint inheriting metatype from type variabe"); btyp_fix n mt diff --git a/src/compiler/flx_core/flx_btype_subst.ml b/src/compiler/flx_core/flx_btype_subst.ml index 4603782b3..df109d68f 100644 --- a/src/compiler/flx_core/flx_btype_subst.ml +++ b/src/compiler/flx_core/flx_btype_subst.ml @@ -7,7 +7,7 @@ let si x = string_of_int x let var_subst t (i, j) = let rec f_btype t = match t with - | BTYP_type_var (k,t) when i = k -> btyp_type_var (j,t) + | BTYP_type_var (k,m,kind) when i = k -> btyp_type_varm (j,m,kind) | t -> Flx_btype.map ~f_btype t in f_btype t @@ -17,7 +17,10 @@ let vars_subst ls t = List.fold_left var_subst t ls let term_subst counter src i arg = let rec aux level t = match t with - | BTYP_type_var (k,_) when k = i -> widen_fixgap level arg + | BTYP_type_var (k,`N,_) when k = i -> widen_fixgap level arg + | BTYP_type_var (k,`V,_) when k = i -> +print_endline ("TERMS SUBST VIEW VARIABLE"); + widen_fixgap level (viewify_type arg) | BTYP_type_match (tt, pts) -> let tt = aux level tt in @@ -44,9 +47,13 @@ let list_subst counter ls t = let varmap0_subst varmap t = let rec f_btype t = match Flx_btype.map ~f_btype t with - | BTYP_type_var (i,_) as x -> + | BTYP_type_var (i,m,_) as x -> if Hashtbl.mem varmap i - then Hashtbl.find varmap i + then + let t = Hashtbl.find varmap i in + match m with + | `N -> t + | `V -> viewify_type t else x | x -> x in @@ -55,9 +62,13 @@ let varmap0_subst varmap t = let varmap_subst varmap t = let rec f_btype t = match Flx_btype.map ~f_btype t with - | BTYP_type_var (i,_) as x -> + | BTYP_type_var (i,m,_) as x -> if Hashtbl.mem varmap i - then Hashtbl.find varmap i + then + let t = Hashtbl.find varmap i in + match m with + | `N -> t + | `V -> viewify_type t else x | BTYP_type_function (p,r,b) -> let diff --git a/src/compiler/flx_core/flx_fold.ml b/src/compiler/flx_core/flx_fold.ml index f2ae0b8e2..e9675c384 100644 --- a/src/compiler/flx_core/flx_fold.ml +++ b/src/compiler/flx_core/flx_fold.ml @@ -80,7 +80,8 @@ let fold (bsym_table: Flx_bsym_table.t) counter t = | BBOOL _ -> () in try aux [] 0 t; t - with Found t -> t + with + | Found t -> t (* produces a unique minimal representation of a type by folding at every node *) diff --git a/src/compiler/flx_core/flx_kind.ml b/src/compiler/flx_core/flx_kind.ml index 474f18212..03066a57c 100644 --- a/src/compiler/flx_core/flx_kind.ml +++ b/src/compiler/flx_core/flx_kind.ml @@ -16,6 +16,7 @@ type kind = | KIND_tuple of kind list | KIND_function of kind * kind (* the kind of a type function from domain to codomain kinds *) | KIND_var of string + | KIND_view (* same as linear with write pointers removed *) let rec sk k = match k with @@ -30,6 +31,7 @@ let rec sk k = | KIND_tuple ks -> "(" ^ Flx_util.catmap ", " sk ks ^")" | KIND_function (d,c) -> sk d ^ " -> " ^ sk c | KIND_var s -> s + | KIND_view -> "VIEW" let map f (k:kind):kind = match k with @@ -69,6 +71,7 @@ let kind_typeset = KIND_typeset let kind_function (d, c) = KIND_function (d,c) let kind_tuple ks = KIND_tuple ks let kind_var s = KIND_var s +let kind_view = KIND_view (* this probably doesn't belong here .. *) type bv_t = string * Flx_bid.bid_t * kind @@ -84,6 +87,7 @@ type keqns_t = keqn_t list type kmgu_t = (string * kind) list +(* NOTE: here the rhs is a subtype of the lhs *) let ksolve_subtypes add_eqn lhs rhs (mgu:kmgu_t ref) = match lhs, rhs with | KIND_borrowed, KIND_borrowed @@ -110,6 +114,15 @@ let ksolve_subtypes add_eqn lhs rhs (mgu:kmgu_t ref) = | KIND_nat, KIND_nat | KIND_typeset, KIND_typeset | KIND_bool, KIND_bool + + (* A view is basically the types not allowing mutation *) + | KIND_view, KIND_view + | KIND_borrowed, KIND_view + | KIND_linear, KIND_view + | KIND_type, KIND_view + | KIND_view, KIND_compactlinear + | KIND_view, KIND_unitsum + -> () (* depth covariant *) @@ -192,22 +205,22 @@ let kind_eq2 a b = (* returns the most specialised kind *) (* FIXME: should throw exception which can be trapped by caller *) let kind_min2 a b = - if kind_ge [a, b] then b else if kind_ge [b, a] then a + if kind_ge2 a b then b else if kind_ge2 b a then a else failwith ("Flx_kind: kind_unify, " ^ sk a ^ " doesn't unify with " ^ sk b) (* returns most general kind *) let kind_max2 a b = - if kind_ge [a, b] then a else if kind_ge [b, a] then b + if kind_ge2 a b then a else if kind_ge2 b a then b else failwith ("Flx_kind: kind_unify, " ^ sk a ^ " doesn't unify with " ^ sk b) let kind_min ks = match ks with - | [] -> assert false (* should return BOTTOM *) + | [] -> assert false (* should return TOP *) | h::t -> List.fold_left kind_min2 h t let kind_max ks = match ks with | [] -> assert false (* should return BOTTOM *) - | h::t -> List.fold_left kind_min2 h t + | h::t -> List.fold_left kind_max2 h t diff --git a/src/compiler/flx_core/flx_print.ml b/src/compiler/flx_core/flx_print.ml index 8c05dcdaa..cf4c09c8d 100644 --- a/src/compiler/flx_core/flx_print.ml +++ b/src/compiler/flx_core/flx_print.ml @@ -382,6 +382,7 @@ and str_of_kindcode (k:kindcode_t) : string = (* | KND_special s -> s *) | KND_tpattern t -> "TPATTERN(" ^ st 0 t ^ ")" | KND_var s -> "kvar_" ^ s + | KND_view -> "VIEW" and st prec tc : string = @@ -739,7 +740,7 @@ and sb bsym_table depth fixlist counter prec tc = lab ) - | BTYP_type_var (i,mt) -> 0," 0,""" | _ -> ":"^Flx_kind.sk mt)^ ">" diff --git a/src/compiler/flx_core/flx_typeeq.ml b/src/compiler/flx_core/flx_typeeq.ml index 5db2f8e02..26d3eef49 100644 --- a/src/compiler/flx_core/flx_typeeq.ml +++ b/src/compiler/flx_core/flx_typeeq.ml @@ -202,7 +202,8 @@ let rec type_eq' sbt counter ltrail ldepth rtrail rdepth trail t1 t2 = | BTYP_void,BTYP_void -> true - | BTYP_type_var (i,_), BTYP_type_var (j,_) -> + (* NOTE: ignoring tvmode *) + | BTYP_type_var (i,_,_), BTYP_type_var (j,_,_) -> let result = i = j in (* print_endline ("Type variables compared " ^ (if result then "TRUE" else "FALSE")); @@ -220,7 +221,7 @@ let rec type_eq' sbt counter ltrail ldepth rtrail rdepth trail t1 t2 = print_endline ("Check fixpoint " ^ si i ^ " vs " ^ si j); *) if i = j then begin - if t1 <> t2 then print_endline "[type_eq] Fix points at same level have different metatypes"; + if t1 <> t2 then print_endline "[type_eq] WARNING: Fix points at same level have different metatypes, judging not equal!"; (* true *) diff --git a/src/compiler/flx_core/flx_unify.ml b/src/compiler/flx_core/flx_unify.ml index 00c584fc5..80f20e052 100644 --- a/src/compiler/flx_core/flx_unify.ml +++ b/src/compiler/flx_core/flx_unify.ml @@ -14,6 +14,7 @@ open Flx_bid let mode_supertype m1 m2 = match m1,m2 with | `V, `R + | `V, `RW | `R, `RW | `W, `RW | `N, _ -> () @@ -295,6 +296,11 @@ print_endline ("Adding inequality " ^ Flx_btype.st lhs ^ " > " ^ Flx_btype.st x) add_eq (l,r); add_eq (machl, machr); + | BTYP_fix (i,ml),BTYP_fix (j,mr) -> + if i <> j then raise Not_found; + (* is this right? because below, the reverse order is tested .. *) +print_endline ("Checking fixpoint kinds " ^ Flx_kind.sk ml ^ " >= " ^ Flx_kind.sk mr); + if not (Flx_kind.kind_ge2 ml mr) then raise Not_found | BTYP_function (dl,cl), BTYP_linearfunction (dr,cr) | BTYP_linearfunction (dl,cl), BTYP_linearfunction (dr,cr) @@ -358,11 +364,13 @@ and solve_subsumption bsym_table counter lhs rhs dvars (s:vassign_t option ref) In fact we need to extra the kind level MGU and return that too ...... *) - | (BTYP_type_var (i,mi) as ti), (BTYP_type_var (j,mj) as tj)-> + (* FIXME: ignore tvmode for the moment *) + | (BTYP_type_var (i,_,mi) as ti), (BTYP_type_var (j,_,mj) as tj)-> (* meta type have to agree *) if i <> j then if BidSet.mem i dvars then begin +(* isn't this backwards?? *) if not (Flx_kind.kind_ge [mi, mj]) then begin raise Not_found; @@ -381,8 +389,14 @@ and solve_subsumption bsym_table counter lhs rhs dvars (s:vassign_t option ref) else () (* same variable .. we should check kinds agree .. *) (* TO DO: calculate the smallest metatype of the type and do a kinding check *) - | BTYP_type_var (i,mt), t - | t,BTYP_type_var (i,mt) -> +(* +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *) + (* FIXME: ignore tvmode for the moment *) + (* What SHOULD happen: the assignment Some (i,t) should viewify t if the + tvmode is view and i is dependent. This means internal subtitutions + will be viewified and so will the MGU + *) + | BTYP_type_var (i,_,mt), t + | t,BTYP_type_var (i,_,mt) -> if not (BidSet.mem i dvars) then raise Not_found; if var_i_occurs i t then begin @@ -407,8 +421,8 @@ and solve_subsumption bsym_table counter lhs rhs dvars (s:vassign_t option ref) * therefore this operation cannot cause an infinite loop * note the laws rev(rev x) = x and rev x = y implies x = rev y *) - | BTYP_rev (BTYP_type_var (i,m) as tvar),t - | t,BTYP_rev (BTYP_type_var (i,m) as tvar) -> + | BTYP_rev (BTYP_type_var (i,_,m) as tvar),t + | t,BTYP_rev (BTYP_type_var (i,_,m) as tvar) -> add_eqn (tvar,btyp_rev t) | BTYP_uniq t1, BTYP_uniq t2 -> add_eqn (t1,t2) diff --git a/src/compiler/flx_cpp_backend/flx_name.ml b/src/compiler/flx_cpp_backend/flx_name.ml index c6e671c4e..8326f17a6 100644 --- a/src/compiler/flx_cpp_backend/flx_name.ml +++ b/src/compiler/flx_cpp_backend/flx_name.ml @@ -238,7 +238,7 @@ print_endline ("Flx_tgen.cpp_type_classname " ^ sbt bsym_table t); | BTYP_ptr (_,_,(_::_::_)) -> assert false | BTYP_ellipsis -> "..." - | BTYP_type_var (i,mt) -> + | BTYP_type_var (i,_,mt) -> failwith ("[cpp_type_classname] Can't name type variable " ^ string_of_bid i ^ ":"^ Flx_kind.sk mt) | BTYP_fix (i,_) -> "void" (* failwith "[cpp_type_classname] Can't name type fixpoint" *) @@ -431,7 +431,7 @@ and cpp_structure_name syms bsym_table t = let t = Flx_fold.fold bsym_table syms.counter t in let t' = unfold "flx_name: cpp_structure_name" t in try match t' with - | BTYP_type_var (i,mt) -> + | BTYP_type_var (i,_,mt) -> failwith ("[cpp_type_classname] Can't name type variable " ^ string_of_bid i ^ ":"^ Flx_kind.sk mt) | BTYP_fix (i,_) -> "_fix<"^string_of_int (-i)^">" (* failwith "[cpp_type_classname] Can't name type fixpoint" *) diff --git a/src/compiler/flx_cpp_backend/flx_tgen.ml b/src/compiler/flx_cpp_backend/flx_tgen.ml index ca5a67ef5..b802ff597 100644 --- a/src/compiler/flx_cpp_backend/flx_tgen.ml +++ b/src/compiler/flx_cpp_backend/flx_tgen.ml @@ -179,7 +179,7 @@ let rec gen_type_name syms bsym_table (index,typ) = "typedef ::flx::rtl::cl_t " ^ cntyp ^ ";\n" | BTYP_fix (i,_) -> "" - | BTYP_type_var (i,mt) -> failwith "[gen_type_name] Can't gen name of type variable" + | BTYP_type_var (i,_,mt) -> failwith "[gen_type_name] Can't gen name of type variable" | BTYP_ptr _ -> "" (* NEW *) diff --git a/src/compiler/flx_desugar/flx_sex2flx.ml b/src/compiler/flx_desugar/flx_sex2flx.ml index 3774ed3e3..68204e2d1 100644 --- a/src/compiler/flx_desugar/flx_sex2flx.ml +++ b/src/compiler/flx_desugar/flx_sex2flx.ml @@ -66,6 +66,7 @@ and kind_of_sex sr x : kindcode_t = | Lst [Id "knd_name"; Str "NAT"] -> KND_nat | Lst [Id "knd_name"; Str "TYPESET"] -> KND_typeset | Lst [Id "knd_name"; Str "COMPACTLINEAR"] -> KND_compactlinear + | Lst [Id "knd_name"; Str "VIEW"] -> KND_view (* Combinators *) | Lst [Id "knd_arrow"; Lst[dom; cod]] -> KND_function (ki dom, ki cod) @@ -477,6 +478,8 @@ print_endline ("sex2flx:expr] " ^ Sex_print.string_of_sex x); ) | Lst [Id "ast_deref"; sr; e] -> +(* print_endline ("Flx_sex2flx: ast_deref " ^ Flx_print.string_of_expr (ex e)); *) + `EXPR_deref (xsr sr,ex e) | Lst [Id "ast_ref"; sr; e] -> `EXPR_ref (xsr sr,ex e) diff --git a/src/compiler/flx_frontend/flx_monoclass.ml b/src/compiler/flx_frontend/flx_monoclass.ml index d1f717256..e7dff575d 100644 --- a/src/compiler/flx_frontend/flx_monoclass.ml +++ b/src/compiler/flx_frontend/flx_monoclass.ml @@ -40,6 +40,15 @@ let flat_typeclass_fixup_expr syms bsym_table virtualinst sr (e,t) = | BEXPR_ref (i,ts) -> let i,ts = virtualinst sr i ts in bexpr_ref t (i,ts) + | BEXPR_rref (i,ts) -> + let i,ts = virtualinst sr i ts in + bexpr_rref t (i,ts) + | BEXPR_wref (i,ts) -> + let i,ts = virtualinst sr i ts in + bexpr_wref t (i,ts) + | BEXPR_vref (i,ts) -> + let i,ts = virtualinst sr i ts in + bexpr_vref t (i,ts) | BEXPR_varname (i',ts') -> let i,ts = virtualinst sr i' ts' in diff --git a/src/compiler/flx_frontend/flx_polyinst.ml b/src/compiler/flx_frontend/flx_polyinst.ml index 78994d1c8..a2c9251e9 100644 --- a/src/compiler/flx_frontend/flx_polyinst.ml +++ b/src/compiler/flx_frontend/flx_polyinst.ml @@ -91,6 +91,15 @@ let flat_poly_fixup_expr syms bsym_table polyinst sr (e,t) = | BEXPR_ref (i,ts) -> let i,ts = polyinst sr i ts in bexpr_ref t (i,ts) + | BEXPR_rref (i,ts) -> + let i,ts = polyinst sr i ts in + bexpr_rref t (i,ts) + | BEXPR_wref (i,ts) -> + let i,ts = polyinst sr i ts in + bexpr_wref t (i,ts) + | BEXPR_vref (i,ts) -> + let i,ts = polyinst sr i ts in + bexpr_vref t (i,ts) | BEXPR_varname (i',ts') -> let i,ts = polyinst sr i' ts' in diff --git a/src/compiler/flx_frontend/flx_reparent.ml b/src/compiler/flx_frontend/flx_reparent.ml index 605cf06b8..bb9fdb9e2 100644 --- a/src/compiler/flx_frontend/flx_reparent.ml +++ b/src/compiler/flx_frontend/flx_reparent.ml @@ -78,6 +78,15 @@ let remap_expr | BEXPR_ref (i,ts) as x,t -> let i,ts = fixup i ts in bexpr_ref (t) (i,ts) + | BEXPR_rref (i,ts) as x,t -> + let i,ts = fixup i ts in + bexpr_rref (t) (i,ts) + | BEXPR_wref (i,ts) as x,t -> + let i,ts = fixup i ts in + bexpr_wref (t) (i,ts) + | BEXPR_vref (i,ts) as x,t -> + let i,ts = fixup i ts in + bexpr_vref (t) (i,ts) | BEXPR_closure (i,ts),t -> let i,ts = fixup i ts in diff --git a/src/compiler/flx_frontend/flx_treg.ml b/src/compiler/flx_frontend/flx_treg.ml index 2ab9d1529..03163b43a 100644 --- a/src/compiler/flx_frontend/flx_treg.ml +++ b/src/compiler/flx_frontend/flx_treg.ml @@ -163,7 +163,7 @@ then (* | BTYP_type_var (i,mt) -> clierrx "[flx_frontend/flx_treg.ml:126: E358] " sr ("Attempt to register type variable " ^ si i ^":"^sbt sym_table mt) *) - | BTYP_type_var (i,mt) -> + | BTYP_type_var (i,_,mt) -> (* print_endline ("Attempt to register type variable " ^ string_of_bid i ^ ":" ^ sbt bsym_table mt); diff --git a/src/compiler/flx_frontend/flx_typeclass.ml b/src/compiler/flx_frontend/flx_typeclass.ml index 0a72d21f5..6dfddac42 100644 --- a/src/compiler/flx_frontend/flx_typeclass.ml +++ b/src/compiler/flx_frontend/flx_typeclass.ml @@ -87,8 +87,8 @@ print_endline ("Inst " ^ string_of_int j ^" function: " ^ id ^ let assigns, rest = fold_left (fun (assigns,rest) (l,r) -> match l,r with - | BTYP_type_var (x,KIND_type), other - | other, BTYP_type_var (x,KIND_type) -> (x,other) :: assigns, rest + | BTYP_type_var (x,_,KIND_type), other + | other, BTYP_type_var (x,_,KIND_type) -> (x,other) :: assigns, rest | _ -> assigns, (l,r) :: rest ) diff --git a/src/packages/grammar.fdoc b/src/packages/grammar.fdoc index 0a2e4b5e1..f477f6d27 100644 --- a/src/packages/grammar.fdoc +++ b/src/packages/grammar.fdoc @@ -520,7 +520,7 @@ syntax expressions { x[srefr_pri] := "*" x[srefr_pri] =># "(prefix 'deref)"; //$ Deref primitive. - //x[srefr_pri] := "_deref" x[srefr_pri] =># "`(ast_deref ,_sr ,_2)"; + x[srefr_pri] := "_deref" x[srefr_pri] =># "`(ast_deref ,_sr ,_2)"; //$ Operator new. x[srefr_pri] := "new" x[srefr_pri] =># "`(ast_new ,_sr ,_2)"; diff --git a/src/packages/pointers.fdoc b/src/packages/pointers.fdoc index 2fb1071e4..6cbd6658c 100644 --- a/src/packages/pointers.fdoc +++ b/src/packages/pointers.fdoc @@ -32,10 +32,15 @@ open class MachinePointers proc storeat[T:LINEAR] ( p: &>T, v: T) = { _storeat (p,v); } //$ Dereference a Felx pointer. - fun _deref[T:LINEAR]: & T = "*$t"; - fun _deref[T:LINEAR]: &< T = "*$t"; - fun deref[T:LINEAR] (p:& _deref p; - fun deref[T:LINEAR] (p:&< _deref p; + //fun _deref[T:LINEAR]: & T = "*$t"; + //fun _deref[T:LINEAR]: &< T = "*$t"; + // NOTE: at present we need all these cases because overload resolution + // does not "rank" kinds .. hmm .. but even this doesn't work! + // adding the RW case changes the ambiguity from the view and read only case + // to the view and read/write case + // looks like a problem in unification not ranking the modes + fun deref[T:LINEAR] (p:& /* { println$ "deref R"; return */ _deref p; /* }(); */ + fun deref[T:LINEAR] (p:&< /* { println$ "deref V"; return */ _deref p; /* }(); */ } open class CompactLinearPointers @@ -44,7 +49,8 @@ open class CompactLinearPointers proc storeat[D,C] ( p:_wpclt< D, C >, v: C) = { _storeat (p,v); } // deref a pointer to compact linear component - fun _deref[mach,clv]: _rpclt -> clv = "::flx::rtl::clt_deref($t)"; + //fun _deref[mach,clv]: _rpclt -> clv = "::flx::rtl::clt_deref($t)"; + //fun _deref[mach,clv]: _rpclt -> clv = "*($t)"; // operator * added to C++ fun deref[mach,clv] (p: _rpclt) => _deref p; } diff --git a/src/packages/rtl.fdoc b/src/packages/rtl.fdoc index f160615c3..d60751c00 100644 --- a/src/packages/rtl.fdoc +++ b/src/packages/rtl.fdoc @@ -830,6 +830,9 @@ inline const_clptr_t applyprj (const_clptr_t cp, clprj_t d) { // dereference inline cl_t clt_deref(clptr_t q) { return *q.p / q.divisor % q.modulus; } inline cl_t clt_deref(const_clptr_t q) { return *q.p / q.divisor % q.modulus; } +inline cl_t operator*(clptr_t q) { return *q.p / q.divisor % q.modulus; } +inline cl_t operator*(const_clptr_t q) { return *q.p / q.divisor % q.modulus; } + // storeat // NOTE: not available for const version