diff --git a/core/basicsettings.ml b/core/basicsettings.ml index e123b7daf..2fc3cc5e4 100644 --- a/core/basicsettings.ml +++ b/core/basicsettings.ml @@ -32,6 +32,17 @@ module Handlers = struct |> sync) end +(* control-flow linearity *) +module CTLinearity = struct + let enabled = + Settings.(flag "track_control_flow_linearity" + |> privilege `System + |> synopsis "Enables the control-flow linearity extension" + |> convert parse_bool + |> CLI.(add (long "track-control-flow-linearity")) + |> sync) +end + module Sessions = struct let exceptions_enabled = Settings.(flag "session_exceptions" diff --git a/core/commonTypes.ml b/core/commonTypes.ml index 3eed085f6..2d05b84f6 100644 --- a/core/commonTypes.ml +++ b/core/commonTypes.ml @@ -15,9 +15,9 @@ module Linearity = struct | Unl -> true | _ -> false - let to_string = function + let to_string ?(is_eff=false) = function | Any -> "Any" - | Unl -> "Unl" + | Unl -> if is_eff then "Lin" else "Unl" let min l r = match l, r with diff --git a/core/compilePatterns.ml b/core/compilePatterns.ml index c610ca4a2..4922eecf2 100644 --- a/core/compilePatterns.ml +++ b/core/compilePatterns.ml @@ -128,7 +128,7 @@ let rec desugar_pattern : Types.row -> Sugartypes.Pattern.with_pos -> Pattern.t | Variant (name, Some p) -> let p, env = desugar_pattern p in Pattern.Variant (name, p), env - | Operation (name, ps, k) -> + | Operation (name, ps, k, _) -> let ps, env = List.fold_right (fun p (ps, env) -> @@ -996,7 +996,7 @@ let compile_handle_cases fields in let rec extract t = match TypeUtils.concrete_type t with - | Types.Operation (domain, _) -> + | Types.Operation (domain, _, _) -> let (fields, _, _) = TypeUtils.extract_row domain |> TypeUtils.extract_row_parts in let arity = StringMap.size fields in if arity = 1 then diff --git a/core/desugarDatatypes.ml b/core/desugarDatatypes.ml index e6f774954..ed28f7011 100644 --- a/core/desugarDatatypes.ml +++ b/core/desugarDatatypes.ml @@ -113,8 +113,8 @@ module Desugar = struct | Record r -> Types.Record (row alias_env r t') | Variant r -> Types.Variant (row alias_env r t') | Effect r -> Types.Effect (row alias_env r t') - | Operation (f, t) -> Types.Operation ( Types.make_tuple_type (List.map datatype f) - , datatype t ) + | Operation (f, t, b) -> Types.Operation ( Types.make_tuple_type (List.map datatype f) + , datatype t, b) | Table (tmp, r, w, n) -> Types.Table (tmp, datatype r, datatype w, datatype n) | List k -> Types.Application (Types.list, [(PrimaryKind.Type, datatype k)]) | TypeApplication (tycon, ts) -> diff --git a/core/desugarEffects.ml b/core/desugarEffects.ml index 05023e9cb..704479058 100644 --- a/core/desugarEffects.ml +++ b/core/desugarEffects.ml @@ -128,10 +128,10 @@ let simplify_tycon_env (tycon_env : Types.tycon_environment) : simple_tycon_env in SEnv.fold simplify_tycon tycon_env SEnv.empty -let make_anon_point k sk freedom = +let make_anon_point ?(is_eff=true) k sk freedom = let var = Types.fresh_raw_variable () in Unionfind.fresh - (Types.Var (var, (k, DesugarTypeVariables.concrete_subkind sk), freedom)) + (Types.Var (var, (k, DesugarTypeVariables.concrete_subkind ~is_effect:is_eff sk), freedom)) (** A map with SugarTypeVar as keys, use for associating the former with information about what @@ -364,7 +364,8 @@ let cleanup_effects tycon_env = WithPos.make ~pos (match node with | Datatype.Operation _ -> node | Datatype.Forall (qs, dt) -> Datatype.Forall (qs, elaborate_op dt) - | _ -> Datatype.Operation ([], dt)) + | _ -> Datatype.Operation ([], dt, DeclaredLinearity.Unl)) + (* nullary operations without =@ are unlimited *) in let fields = List.map (function | name, Present dt when not (TypeUtils.is_builtin_effect name) -> @@ -379,18 +380,18 @@ let cleanup_effects tycon_env = if not (SugarTypeVar.is_resolved stv) then begin let gen_unresolved_eff () = - SugarTypeVar.mk_unresolved shared_effect_var_name None `Rigid + SugarTypeVar.mk_unresolved shared_effect_var_name ~is_eff:true None `Rigid in let to_unresolved_general sk fr = - SugarTypeVar.mk_unresolved "$" sk fr + SugarTypeVar.mk_unresolved "$" ~is_eff:true sk fr in let gen_resolved_flex () = SugarTypeVar.mk_resolved_row (let var = Types.fresh_raw_variable () in Unionfind.fresh - (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_effect)), `Flexible))) + (Types.Var (var, (PrimaryKind.Row, (default_effect_lin, res_effect)), `Flexible))) in - let name, sk, fr = gue stv in + let name, (_, sk), fr = gue stv in if has_effect_sugar then begin @@ -453,7 +454,7 @@ let gather_mutual_info (tycon_env : simple_tycon_env) = match eff_var with | Datatype.Open stv when (not (SugarTypeVar.is_resolved stv)) - && SugarTypeVar.get_unresolved_exn stv = ("$eff", None, `Rigid) + && SugarTypeVar.get_unresolved_exn stv = ("$eff", (true, None), `Rigid) -> self#with_implicit | _ -> self ) @@ -768,7 +769,7 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = let point = lazy (let var = Types.fresh_raw_variable () in - Unionfind.fresh (Types.Var (var, (PrimaryKind.Presence, default_subkind), `Rigid))) + Unionfind.fresh (Types.Var (var, (PrimaryKind.Presence, default_effect_subkind), `Rigid))) in StringMap.add op point m) v StringMap.empty), @@ -786,7 +787,7 @@ let preprocess_type (dt : Datatype.with_pos) tycon_env allow_fresh shared_effect lazy (let var = Types.fresh_raw_variable () in Unionfind.fresh - (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_any)), `Rigid))) + (Types.Var (var, (PrimaryKind.Row, default_effect_subkind), `Rigid))) in Some point | _ -> @@ -948,7 +949,7 @@ class main_traversal simple_tycon_env = (* Looking for this gives us the operations associcated with the $eff var. The kind and freedom info are ignored for the lookup *) let eff_sugar_var = - SugarTypeVar.mk_unresolved shared_effect_var_name None + SugarTypeVar.mk_unresolved shared_effect_var_name ~is_eff:true None `Rigid in @@ -1018,8 +1019,8 @@ class main_traversal simple_tycon_env = if not allow_implictly_bound_vars then raise (DesugarTypeVariables.free_type_variable dpos); - let _name, sk, freedom = SugarTypeVar.get_unresolved_exn stv in - let mtv = make_anon_point (PrimaryKind.Row) sk freedom in + let _name, (is_eff, sk), freedom = SugarTypeVar.get_unresolved_exn stv in + let mtv = make_anon_point ~is_eff:is_eff (PrimaryKind.Row) sk freedom in let rtv = SugarTypeVar.mk_resolved_row mtv in (o, D.Open rtv) | D.Open srv when not (SugarTypeVar.is_resolved srv) -> @@ -1177,7 +1178,7 @@ class main_traversal simple_tycon_env = ({ node = t, args, b; pos } as tn) = if StringMap.find t implicits then let var = Types.fresh_raw_variable () in - let q = (var, (PrimaryKind.Row, (lin_unl, res_effect))) in + let q = (var, (PrimaryKind.Row, (default_effect_lin, res_effect))) in (* Add the new quantifier to the argument list and rebind. *) (* let qs = List.map (snd ->- OptionUtils.val_of) args @ [q] in *) let args = args @ [ SugarQuantifier.mk_resolved q ] in @@ -1191,7 +1192,7 @@ class main_traversal simple_tycon_env = let tycon_env = SEnv.bind t (env_args, true, None) tycon_env in let shared_effect_var : Types.meta_row_var Lazy.t = lazy - (Unionfind.fresh (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_effect)), `Rigid))) + (Unionfind.fresh (Types.Var (var, (PrimaryKind.Row, (default_effect_lin, res_effect)), `Rigid))) in let shared_var_env = StringMap.add t (Some shared_effect_var) shared_var_env diff --git a/core/desugarSessionExceptions.ml b/core/desugarSessionExceptions.ml index f60f5846e..9ec30b735 100644 --- a/core/desugarSessionExceptions.ml +++ b/core/desugarSessionExceptions.ml @@ -87,7 +87,8 @@ object (o : 'self_type) let ty = Types.fresh_type_variable (CommonTypes.lin_any, CommonTypes.res_any) in let with_pos x = SourceCode.WithPos.make ~pos x in - let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type)) in + (* FIXME: WT: I don't know whether should it be lindo or not *) + let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type), DeclaredLinearity.Lin) in (o, with_pos (Switch (with_pos doOp, [], Some ty)), ty) | { node = TryInOtherwise (_, _, _, _, None); _} -> assert false | { node = TryInOtherwise (try_phr, pat, as_phr, otherwise_phr, (Some dt)); pos } @@ -122,7 +123,8 @@ object (o : 'self_type) (Utility.gensym ~prefix:"dsh" ()) in let otherwise_pat : Sugartypes.Pattern.with_pos = - with_dummy_pos (Pattern.Operation (failure_op_name, [], cont_pat)) in + (* FIXME: WT: I don't know whether should it be lincase or not *) + with_dummy_pos (Pattern.Operation (failure_op_name, [], cont_pat, DeclaredLinearity.Lin)) in let otherwise_clause = (otherwise_pat, otherwise_phr) in diff --git a/core/desugarTypeVariables.ml b/core/desugarTypeVariables.ml index b6035f01a..06ad2b40f 100644 --- a/core/desugarTypeVariables.ml +++ b/core/desugarTypeVariables.ml @@ -84,10 +84,10 @@ let free_type_variable ?var pos = "Unbound " ^ desc ^ " in position where no free type variables are allowed") -let concrete_subkind = +let concrete_subkind ?(is_effect=false) = function | Some subkind -> subkind - | None -> default_subkind + | None -> if is_effect then default_effect_subkind else default_subkind let default_kind : PrimaryKind.t = PrimaryKind.Type @@ -169,9 +169,9 @@ However, this is not the same as setting defaults. Instead, the info in the map takes precedence. *) -let make_opt_kinded_var k sk_opt freedom : Types.t = +let make_opt_kinded_var k ?(is_eff=false) sk_opt freedom : Types.t = let var = Types.fresh_raw_variable () in - let sk = concrete_subkind sk_opt in + let sk = concrete_subkind ~is_effect:is_eff sk_opt in Types.Var (var, (k, sk), freedom) let get_var_info (info : Types.t) = @@ -179,26 +179,26 @@ let get_var_info (info : Types.t) = | Types.Var (var, k, fd) -> (var, k, fd) | _ -> raise found_non_var_meta_var -let make_fresh_entry pk_opt sk_opt freedom : tyvar_map_entry = +let make_fresh_entry pk_opt ?(is_eff=false) sk_opt freedom : tyvar_map_entry = let open PrimaryKind in match pk_opt with | None -> TVUnkinded (sk_opt, freedom) | Some Type -> - let point = Unionfind.fresh (make_opt_kinded_var Type sk_opt freedom) in + let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Type sk_opt freedom) in TVType (sk_opt, point) | Some Row -> - let point = Unionfind.fresh (make_opt_kinded_var Row sk_opt freedom) in + let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Row sk_opt freedom) in TVRow (sk_opt, point) | Some Presence -> - let point = Unionfind.fresh (make_opt_kinded_var Presence sk_opt freedom) in + let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Presence sk_opt freedom) in TVPresence (sk_opt, point) (* does not do all sanity checks *) (* Note that this always reuses existing points! *) -let update_entry pk sk_opt freedom existing_entry : tyvar_map_entry = - let con_sk = concrete_subkind sk_opt in +let update_entry pk ?(is_eff=false) sk_opt freedom existing_entry : tyvar_map_entry = + let con_sk = concrete_subkind ~is_effect:is_eff sk_opt in let open PrimaryKind in match pk, existing_entry with | _, TVUnkinded _ -> @@ -290,7 +290,7 @@ object (o : 'self) (** Used for type/row/presence variables found along the way, including anonymous ones *) - method add ?pos name (pk : PrimaryKind.t) (sk : Subkind.t option) freedom : 'self * SugarTypeVar.t = + method add ?pos name (pk : PrimaryKind.t) ?(is_eff=false) (sk : Subkind.t option) freedom : 'self * SugarTypeVar.t = let anon = is_anonymous_name name in let pos = OptionUtils.from_option SourceCode.Position.dummy pos in if not anon && StringMap.mem name tyvar_map then @@ -314,7 +314,7 @@ object (o : 'self) the *existing* unionfind point carried inside the entry *) let entry = if pk' <> pk_union' || sk' <> sk_union' then - update_entry pk sk freedom existing_entry + update_entry pk ~is_eff:is_eff sk freedom existing_entry else existing_entry in @@ -332,7 +332,7 @@ object (o : 'self) Since at this point we know the primary kind, this will always result in the creation of a unionfind point. *) - let entry = make_fresh_entry (Some pk) sk freedom in + let entry = make_fresh_entry (Some pk) ~is_eff:is_eff sk freedom in let o = if anon then o else o#bind name entry in let resolved_var = resolved_var_of_entry entry in @@ -390,8 +390,8 @@ object (o : 'self) let open Datatype in function | TypeVar stv -> - let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn stv in - let o, resolved_tv = o#add name pk_type sk freedom in + let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn stv in + let o, resolved_tv = o#add name pk_type ~is_eff:is_eff sk freedom in (* let resolved_tv = resolved_var_of_entry entry in *) o, TypeVar resolved_tv | Forall (unresolved_qs, body) -> @@ -423,8 +423,8 @@ object (o : 'self) appear in contexts where implictly scoped variables are allowed. *) o, orig | Open srv -> - let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn srv in - let o, resolved_rv = o#add name pk_row sk freedom in + let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn srv in + let o, resolved_rv = o#add name pk_row ~is_eff:is_eff sk freedom in o, Datatype.Open resolved_rv | Recursive (stv, r) -> let original_o = o in @@ -446,8 +446,8 @@ object (o : 'self) let o, t = o#datatype t in o, Present t | Var utv -> - let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn utv in - let o, resolved_pv = o#add name pk_presence sk freedom in + let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn utv in + let o, resolved_pv = o#add name pk_presence ~is_eff:is_eff sk freedom in o, Var resolved_pv method! phrase p = diff --git a/core/desugarTypeVariables.mli b/core/desugarTypeVariables.mli index 407215f5f..1bd098d9a 100644 --- a/core/desugarTypeVariables.mli +++ b/core/desugarTypeVariables.mli @@ -1,6 +1,6 @@ val infer_kinds : bool Settings.setting -val concrete_subkind : CommonTypes.Subkind.t option -> CommonTypes.Subkind.t +val concrete_subkind : ?is_effect:bool -> CommonTypes.Subkind.t option -> CommonTypes.Subkind.t val free_type_variable : ?var:string -> SourceCode.Position.t -> exn diff --git a/core/generalise.ml b/core/generalise.ml index 7a3f0eba6..009732a6d 100644 --- a/core/generalise.ml +++ b/core/generalise.ml @@ -71,7 +71,7 @@ let rec get_type_args : gen_kind -> TypeVarSet.t -> datatype -> type_arg list = get_type_args kind (TypeVarSet.add_quantifiers qs bound_vars) t (* Effect *) | Effect row -> get_row_type_args kind bound_vars row - | Operation (f, t) -> + | Operation (f, t, _) -> let from_gens = gt f and to_gens = gt t in from_gens @ to_gens diff --git a/core/instantiate.ml b/core/instantiate.ml index dedd92e68..76226ae94 100644 --- a/core/instantiate.ml +++ b/core/instantiate.ml @@ -76,7 +76,7 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) * | Record row -> Record (instr row) | Variant row -> Variant (instr row) | Effect row -> Effect (instr row) - | Operation (f, t) -> Operation (inst f, inst t) + | Operation (f, t, b) -> Operation (inst f, inst t, b) | Table (tmp, f, d, r) -> Table (tmp, inst f, inst d, inst r) | ForAll (qs, t) -> let remove_shadowed_quantifier tmap q = diff --git a/core/irCheck.ml b/core/irCheck.ml index e68989795..f3f6df4de 100644 --- a/core/irCheck.ml +++ b/core/irCheck.ml @@ -350,11 +350,12 @@ let eq_types occurrence : type_eq_context -> (Types.datatype * Types.datatype) - | Effect r -> eq_rows (context, l, r) | _ -> false end - | Operation (lfrom, lto) -> + | Operation (lfrom, lto, llin) -> begin match t2 with - | Operation (rfrom, rto) -> + | Operation (rfrom, rto, rlin) -> eqt (context, lfrom, rfrom) && - eqt (context, lto , rto ) + eqt (context, lto , rto ) && + llin = rlin | _ -> false end (* Row *) diff --git a/core/lexer.mll b/core/lexer.mll index 47d3f92e4..2adfb1125 100644 --- a/core/lexer.mll +++ b/core/lexer.mll @@ -92,6 +92,7 @@ let keywords = [ "delete_left", DELETE_LEFT; "determined", DETERMINED; "do" , DOOP; + "lindo" , LINDOOP; "effectname", EFFECTNAME; "else" , ELSE; "escape" , ESCAPE; @@ -163,6 +164,8 @@ let keywords = [ "with" , WITH; (* SAND *) "tablekeys" , TABLEKEYS; + (* Control-flow linearity *) + "xlin" , LINFLAG ] exception LexicalError of (string * Lexing.position) @@ -212,6 +215,7 @@ rule lex ctxt nl = parse | "-@" { LOLLI } | "~@" { SQUIGLOLLI } | "=>" { FATRARROW } + | "=@" { FATLOLLI } | "-." { MINUSDOT } | '-' { MINUS } | '(' { LPAREN } diff --git a/core/lib.ml b/core/lib.ml index b40374545..556a987fd 100644 --- a/core/lib.ml +++ b/core/lib.ml @@ -356,7 +356,7 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ "Send", (p2 (fun _pid _msg -> assert(false)), (* Now handled in evalir.ml *) - datatype "forall a::Type(Any, Any), e::Row(Unl, Any), f::Row.(Process ({hear:a|e}), a) ~f~> ()", + datatype "forall a::Type(Any, Any), e::Row(Any, Any), f::Row(Any, Any).(Process ({hear:a|e}), a) ~f~> ()", IMPURE); "self", @@ -478,53 +478,53 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ "send", (`PFun (fun _ -> assert false), - datatype "forall a::Type(Any, Any), s::Type(Any, Session), e::Row.(a, !a.s) ~e~> s", + datatype "forall a::Type(Any, Any), s::Type(Any, Session), e::Row(Any, Any).(a, !a.s) ~e~> s", IMPURE); "receive", (`PFun (fun _ -> assert false), - datatype "forall a::Type(Any, Any), s::Type(Any, Session), e::Row. (?a.s) ~e~> (a, s)", + datatype "forall a::Type(Any, Any), s::Type(Any, Session), e::Row(Any, Any). (?a.s) ~e~> (a, s)", IMPURE); "link", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row(Unl, Any).(s, ~s) ~e~> ()", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).(s, ~s) ~e~> ()", IMPURE); (* access points *) "new", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.() ~e~> AP(s)", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).() ~e~> AP(s)", IMPURE); "newAP", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row. (Location) ~e~> AP(s)", + datatype "forall s::Type(Any, Session), e::Row(Any, Any). (Location) ~e~> AP(s)", IMPURE); "newClientAP", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.() ~e~> AP(s)", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).() ~e~> AP(s)", IMPURE); "newServerAP", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.() ~e~> AP(s)", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).() ~e~> AP(s)", IMPURE); "accept", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.(AP(s)) ~e~> s", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).(AP(s)) ~e~> s", IMPURE); "request", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.(AP(s)) ~e~> ~s", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).(AP(s)) ~e~> ~s", IMPURE); "cancel", (`PFun (fun _ -> assert false), - datatype "forall s::Type(Any, Session), e::Row.(s) ~e~> ()", + datatype "forall s::Type(Any, Session), e::Row(Any, Any).(s) ~e~> ()", IMPURE); "close", @@ -691,6 +691,7 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ "print", (p1 (fun msg -> print_string (Value.unbox_string msg); flush stdout; `Record []), + (* datatype "(String) ~> ()", *) datatype "(String) ~> ()", IMPURE); @@ -1750,6 +1751,7 @@ let typing_env = {Types.var_env = type_env; Types.rec_vars = StringSet.empty; tycon_env = alias_env; Types.effect_row = Types.closed_wild_row; + Types.cont_lin = -1; Types.desugared = false } let primitive_names = StringSet.elements (Env.String.domain type_env) diff --git a/core/parser.mly b/core/parser.mly index 97c44b167..60f0d16c9 100644 --- a/core/parser.mly +++ b/core/parser.mly @@ -55,6 +55,10 @@ open ParserConstructors let default_fixity = 9 +let lincont_enabled = Settings.get Basicsettings.CTLinearity.enabled + +let default_effect_lin = if lincont_enabled then lin_any else lin_unl + let primary_kind_of_string p = function | "Type" -> pk_type @@ -67,6 +71,7 @@ let linearity_of_string p = function | "Any" -> lin_any | "Unl" -> lin_unl + | "Lin" -> lin_unl (* for effect vars *) | lin -> raise (ConcreteSyntaxError (pos p, "Invalid kind linearity: " ^ lin)) @@ -111,6 +116,15 @@ let full_kind_of pos prim lin rest = let r = restriction_of_string pos rest in (Some p, Some (l, r)) +(* The Row(Lin) and Row(Any) syntactic sugars for linear effect vars. + Note that these two syntactic sugars should only be used for effect + row variables, not for value row variables. *) +let linrow_kind_of pos prim lin = + let p = primary_kind_of_string pos prim in + let l = if lincont_enabled then linearity_of_string pos lin else lin_unl in + let r = res_any in + (Some p, Some (l, r)) + let full_subkind_of pos lin rest = let l = linearity_of_string pos lin in let r = restriction_of_string pos rest in @@ -129,22 +143,23 @@ let kind_of p = function (* primary kind abbreviation *) | "Type" -> (Some pk_type, None) - | "Row" -> (Some pk_row, None) + | "Row" -> (Some pk_row, None) (* either a value row or an effect row *) | "Presence" -> (Some pk_presence, None) (* subkind of type abbreviations *) | "Any" -> (Some pk_type, Some (lin_any, res_any)) | "Base" -> (Some pk_type, Some (lin_unl, res_base)) | "Session" -> (Some pk_type, Some (lin_any, res_session)) - | "Eff" -> (Some pk_row , Some (lin_unl, res_effect)) + | "Eff" -> (Some pk_row , Some (default_effect_lin, res_effect)) | k -> raise (ConcreteSyntaxError (pos p, "Invalid kind: " ^ k)) let subkind_of p = function (* subkind abbreviations *) | "Any" -> Some (lin_any, res_any) + | "Lin" -> Some (lin_unl, res_any) (* for linear effect vars *) | "Base" -> Some (lin_unl, res_base) | "Session" -> Some (lin_any, res_session) - | "Eff" -> Some (lin_unl, res_effect) + | "Eff" -> Some (default_effect_lin, res_effect) | sk -> raise (ConcreteSyntaxError (pos p, "Invalid subkind: " ^ sk)) let named_quantifier name kind freedom = SugarQuantifier.mk_unresolved name kind freedom @@ -173,6 +188,17 @@ let attach_row_subkind (r, subkind) = | _ -> assert false in attach_subkind_helper update subkind +let attach_presence_subkind (t, subkind) = + let update sk = + match t with + | Datatype.Var stv -> + let (x, _, freedom) = SugarTypeVar.get_unresolved_exn stv in + let stv' = SugarTypeVar.mk_unresolved x sk freedom in + Datatype.Var stv' + | _ -> assert false + in attach_subkind_helper update subkind + + let alias p name args aliasbody = with_pos p (Aliases [with_pos p (name, args, aliasbody)]) @@ -191,15 +217,14 @@ let parseRegexFlags f = | _ -> assert false) (asList f 0 []) +let named_typevar ?(is_eff=false) name freedom : SugarTypeVar.t = + SugarTypeVar.mk_unresolved name ~is_eff:is_eff None freedom -let named_typevar name freedom : SugarTypeVar.t = - SugarTypeVar.mk_unresolved name None freedom - -let fresh_typevar freedom : SugarTypeVar.t = - named_typevar "$" freedom +let fresh_typevar ?(is_eff=false) freedom : SugarTypeVar.t = + named_typevar ~is_eff:is_eff "$" freedom let fresh_effects = - let stv = SugarTypeVar.mk_unresolved "$eff" None `Rigid in + let stv = SugarTypeVar.mk_unresolved ~is_eff:true "$eff" None `Rigid in ([], Datatype.Open stv) let make_effect_var : is_dot:bool -> ParserPosition.t -> Datatype.row_var @@ -213,13 +238,15 @@ let make_effect_var : is_dot:bool -> ParserPosition.t -> Datatype.row_var then begin if is_dot then Datatype.Closed - else Datatype.Open (SugarTypeVar.mk_unresolved "$eff" None `Rigid) + else Datatype.Open (SugarTypeVar.mk_unresolved "$eff" ~is_eff:true None `Rigid) end else begin if is_dot then raise (ConcreteSyntaxError (pos loc, "Dot syntax in effect row variables is only supported when effect_sugar and effect_sugar_policy.open_default are enabled.")) else Datatype.Closed end +let dummy_phrase pos = with_pos pos (Sugartypes.RecordLit ([], None)) + module MutualBindings = struct type mutual_bindings = @@ -303,7 +330,7 @@ let any = any_pat dp %token EOF %token EQ IN -%token FUN LINFUN FROZEN_FUN FROZEN_LINFUN RARROW LOLLI FATRARROW VAR OP +%token FUN LINFUN FROZEN_FUN FROZEN_LINFUN RARROW LOLLI FATRARROW FATLOLLI VAR OP %token SQUIGRARROW SQUIGLOLLI TILDE %token IF ELSE %token MINUS MINUSDOT @@ -311,7 +338,8 @@ let any = any_pat dp %token HANDLE SHALLOWHANDLE %token SPAWN SPAWNAT SPAWNANGELAT SPAWNCLIENT SPAWNANGEL SPAWNWAIT %token OFFER SELECT -%token DOOP +%token DOOP LINDOOP +%token LINFLAG %token LPAREN RPAREN %token LBRACE RBRACE LBRACEBAR BARRBRACE LQUOTE RQUOTE %token RBRACKET LBRACKET LBRACKETBAR BARRBRACKET @@ -526,6 +554,8 @@ typeargs_opt: kind: | COLONCOLON CONSTRUCTOR LPAREN CONSTRUCTOR COMMA CONSTRUCTOR RPAREN { full_kind_of $loc $2 $4 $6 } +| COLONCOLON CONSTRUCTOR LPAREN CONSTRUCTOR RPAREN + { linrow_kind_of $loc $2 $4 } | COLONCOLON CONSTRUCTOR { kind_of $loc($2) $2 } subkind: @@ -678,7 +708,8 @@ unary_expression: | MINUSDOT unary_expression { unary_appl ~ppos:$loc UnaryOp.FloatMinus $2 } | OPERATOR unary_expression { unary_appl ~ppos:$loc (UnaryOp.Name $1) $2 } | postfix_expression | constructor_expression { $1 } -| DOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None)) } +| DOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None, DeclaredLinearity.Unl)) } +| LINDOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None, DeclaredLinearity.Lin)) } infix_appl: | unary_expression { $1 } @@ -907,7 +938,13 @@ perhaps_db_driver: | atomic_expression perhaps_db_args { Some $1, $2 } | /* empty */ { None , None } +seq_expression: +// | LBRACKETBAR exp BARRBRACKET { with_pos $loc (Unlet $2) } +// | LEFTTRIANGLE exp RIGHTTRIANGLE { with_pos $loc (Linlet $2) } // deprecated +| LINFLAG { with_pos $loc (Linlet (dummy_phrase $loc)) } + exp: +| seq_expression | case_expression | conditional_expression | database_expression @@ -1033,18 +1070,18 @@ arrow_prefix: straight_arrow_prefix: | hear_arrow_prefix | arrow_prefix { $1 } -| MINUS nonrec_row_var | MINUS kinded_nonrec_row_var { ([], $2) } +| MINUS nonrec_eff_var | MINUS kinded_nonrec_row_var { ([], $2) } | MINUS effect_app { ([], $2) } squig_arrow_prefix: | hear_arrow_prefix | arrow_prefix { $1 } -| TILDE nonrec_row_var | TILDE kinded_nonrec_row_var { ([], $2) } +| TILDE nonrec_eff_var | TILDE kinded_nonrec_row_var { ([], $2) } | TILDE effect_app { ([], $2) } hear_arrow_prefix: | LBRACE COLON datatype COMMA efields RBRACE { hear_arrow_prefix $3 $5 } | LBRACE COLON datatype RBRACE { hear_arrow_prefix $3 ([], Datatype.Closed) } -| LBRACE COLON datatype VBAR nonrec_row_var RBRACE +| LBRACE COLON datatype VBAR nonrec_eff_var RBRACE | LBRACE COLON datatype VBAR kinded_nonrec_row_var RBRACE { hear_arrow_prefix $3 ([], $5) } straight_arrow: @@ -1064,7 +1101,9 @@ squiggly_arrow: | parenthesized_datatypes SQUIGLOLLI datatype { Datatype.Lolli ($1, row_with_wp fresh_effects, $3) } fat_arrow: -| parenthesized_datatypes FATRARROW datatype { Datatype.Operation ($1, $3) } +| parenthesized_datatypes FATRARROW datatype { Datatype.Operation ($1, $3, DeclaredLinearity.Unl) } +| parenthesized_datatypes FATLOLLI datatype { Datatype.Operation ($1, $3, + if lincont_enabled then DeclaredLinearity.Lin else DeclaredLinearity.Unl) } mu_datatype: | MU VARIABLE DOT mu_datatype { Datatype.Mu (named_typevar $2 `Rigid, with_pos $loc($4) $4) } @@ -1212,13 +1251,13 @@ vfield: efields: | efield { ([$1], make_effect_var ~is_dot:false $loc) } | soption(efield) VBAR DOT { ( $1 , make_effect_var ~is_dot:true $loc) } -| soption(efield) VBAR row_var { ( $1 , $3 ) } +| soption(efield) VBAR eff_var { ( $1 , $3 ) } | soption(efield) VBAR kinded_row_var { ( $1 , $3 ) } | soption(efield) VBAR effect_app { ( $1 , $3 ) } | efield COMMA efields { ( $1::fst $3, snd $3 ) } efield: -| effect_label fieldspec { ($1, $2) } +| effect_label efieldspec { ($1, $2) } effect_label: | CONSTRUCTOR { $1 } @@ -1241,6 +1280,30 @@ braced_fieldspec: | LBRACE UNDERSCORE RBRACE { Datatype.Var (fresh_typevar `Rigid) } | LBRACE PERCENT RBRACE { Datatype.Var (fresh_typevar `Flexible) } +efieldspec: +| ebraced_fieldspec { $1 } +| COLON datatype { Datatype.Present $2 } +| MINUS { Datatype.Absent } + +ebraced_fieldspec: +| LBRACE COLON datatype RBRACE { Datatype.Present $3 } +| LBRACE MINUS RBRACE { Datatype.Absent } +// | LBRACE VARIABLE RBRACE { Datatype.Var (named_typevar ~is_eff:true $2 `Rigid) } +// | LBRACE PERCENTVAR RBRACE { Datatype.Var (named_typevar ~is_eff:true $2 `Flexible) } +// | LBRACE UNDERSCORE RBRACE { Datatype.Var (fresh_typevar ~is_eff:true `Rigid) } +// | LBRACE PERCENT RBRACE { Datatype.Var (fresh_typevar ~is_eff:true `Flexible) } +| LBRACE nonrec_epresence_var RBRACE { $2 } +| LBRACE kinded_epresence_var RBRACE { $2 } + +kinded_epresence_var: +| nonrec_epresence_var subkind { attach_presence_subkind ($1, $2) } + +nonrec_epresence_var: +| VARIABLE { Datatype.Var (named_typevar ~is_eff:true $1 `Rigid ) } +| PERCENTVAR { Datatype.Var (named_typevar ~is_eff:true $1 `Flexible) } +| UNDERSCORE { Datatype.Var (fresh_typevar ~is_eff:true `Rigid) } +| PERCENT { Datatype.Var (fresh_typevar ~is_eff:true `Flexible) } + nonrec_row_var: | VARIABLE { Datatype.Open (named_typevar $1 `Rigid ) } | PERCENTVAR { Datatype.Open (named_typevar $1 `Flexible) } @@ -1257,6 +1320,15 @@ kinded_nonrec_row_var: kinded_row_var: | row_var subkind { attach_row_subkind ($1, $2) } +nonrec_eff_var: +| VARIABLE { Datatype.Open (named_typevar ~is_eff:true $1 `Rigid ) } +| PERCENTVAR { Datatype.Open (named_typevar ~is_eff:true $1 `Flexible) } +| UNDERSCORE { Datatype.Open (fresh_typevar ~is_eff:true `Rigid) } +| PERCENT { Datatype.Open (fresh_typevar ~is_eff:true `Flexible) } + +eff_var: +| nonrec_eff_var { $1 } +| LPAREN MU VARIABLE DOT fields RPAREN { Datatype.Recursive (named_typevar ~is_eff:true $3 `Rigid, $5) } vrow_var: /* This uses the usual nonrec_row_var, because a variant version would be exactly the same. */ @@ -1325,11 +1397,13 @@ typed_effect_pattern: resumable_operation_pattern: | operation_pattern FATRARROW pattern - { with_pos $loc (Pattern.Operation (fst $1, snd $1, $3)) } + { with_pos $loc (Pattern.Operation (fst $1, snd $1, $3, DeclaredLinearity.Unl)) } +| operation_pattern FATLOLLI pattern + { with_pos $loc (Pattern.Operation (fst $1, snd $1, $3, DeclaredLinearity.Lin)) } | operation_pattern RARROW pattern - { with_pos $loc (Pattern.Operation (fst $1, snd $1, $3)) } + { with_pos $loc (Pattern.Operation (fst $1, snd $1, $3, DeclaredLinearity.Unl)) } | operation_pattern - { with_pos $loc (Pattern.Operation (fst $1, snd $1, any)) } + { with_pos $loc (Pattern.Operation (fst $1, snd $1, any, DeclaredLinearity.Unl)) } operation_pattern: | CONSTRUCTOR { ($1, []) } diff --git a/core/sugarTraversals.ml b/core/sugarTraversals.ml index 0204f6d57..9f9e6868d 100644 --- a/core/sugarTraversals.ml +++ b/core/sugarTraversals.ml @@ -42,6 +42,9 @@ class map = method bool : bool -> bool = function | false -> false | true -> true + method linearity : DeclaredLinearity.t -> DeclaredLinearity.t = + DeclaredLinearity.(function | Lin -> Lin | Unl -> Unl) + method unary_op : UnaryOp.t -> UnaryOp.t = let open UnaryOp in function | Minus -> Minus @@ -82,11 +85,12 @@ class map = method type_variable : SugarTypeVar.t -> SugarTypeVar.t = let open SugarTypeVar in function - | TUnresolved (name, subkind_opt, freedom) -> + | TUnresolved (name, (is_eff, subkind_opt), freedom) -> let name' = o#name name in + let is_eff' = o#bool is_eff in let subkind_opt' = o#option (fun o -> o#subkind) subkind_opt in let freedom' = o#freedom freedom in - TUnresolved (name', subkind_opt', freedom') + TUnresolved (name', (is_eff', subkind_opt'), freedom') | v -> o#unknown v @@ -315,14 +319,18 @@ class map = let _x_i1 = o#option (fun o -> o#phrase) _x_i1 in let _x_i2 = o#option (fun o -> o#typ) _x_i2 in ConstructorLit ((_x, _x_i1, _x_i2)) - | DoOperation (op, ps, t) -> + | DoOperation (op, ps, t, b) -> let op = o#phrase op in let ps = o#list (fun o -> o#phrase) ps in let t = o#option (fun o -> o#typ) t in - DoOperation (op, ps, t) + DoOperation (op, ps, t, b) | Operation _x -> let _x = o#name _x in Operation _x + | Linlet _x -> + let _x = o#phrase _x in Linlet _x + | Unlet _x -> + let _x = o#phrase _x in Unlet _x | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let m = o#phrase sh_expr in let params = @@ -559,11 +567,12 @@ class map = let _x = o#name _x in let _x_i1 = o#option (fun o -> o#pattern) _x_i1 in Variant ((_x, _x_i1)) - | Operation (name, ps, k) -> + | Operation (name, ps, k, b) -> let name = o#name name in let ps = o#list (fun o -> o#pattern) ps in let k = o#pattern k in - Operation (name, ps, k) + let b = o#linearity b in + Operation (name, ps, k, b) | Negative _x -> let _x = o#list (fun o -> o#name) _x in Negative _x @@ -675,9 +684,10 @@ class map = | Record _x -> let _x = o#row _x in Record _x | Variant _x -> let _x = o#row _x in Variant _x | Effect r -> let r = o#row r in Effect r - | Operation (_x, _x_i1) -> + | Operation (_x, _x_i1, _x_i2) -> let _x = o#list (fun o -> o#datatype) _x in - let _x_i1 = o#datatype _x_i1 in Operation (_x, _x_i1) + let _x_i1 = o#datatype _x_i1 in + let _x_i2 = o#linearity _x_i2 in Operation (_x, _x_i1, _x_i2) | Table (_t, _x, _x_i1, _x_i2) -> let _x = o#datatype _x in let _x_i1 = o#datatype _x_i1 in @@ -904,6 +914,9 @@ class fold = method bool : bool -> 'self_type = function | false -> o | true -> o + method linearity : DeclaredLinearity.t -> 'self_type = + DeclaredLinearity.(function | Unl -> o | Lin -> o) + method unary_op : UnaryOp.t -> 'self_type = let open UnaryOp in function | Minus -> o @@ -940,8 +953,9 @@ class fold = method type_variable : SugarTypeVar.t -> 'self_type = let open SugarTypeVar in function - | TUnresolved (name, subkind_opt, freedom) -> + | TUnresolved (name, (is_eff, subkind_opt), freedom) -> let o = o#name name in + let o = o#bool is_eff in let o = o#option (fun o -> o#subkind) subkind_opt in let o = o#freedom freedom in o @@ -1132,12 +1146,17 @@ class fold = | ConstructorLit ((_x, _x_i1, _x_i2)) -> let o = o#name _x in let o = o#option (fun o -> o#phrase) _x_i1 in o - | DoOperation (op,ps,t) -> + | DoOperation (op,ps,t,b) -> let o = o#phrase op in let o = o#option (fun o -> o#unknown) t in - let o = o#list (fun o -> o#phrase) ps in o + let o = o#list (fun o -> o#phrase) ps in + let o = o#linearity b in o | Operation (_x) -> let o = o#name _x in o + | Linlet _x -> + let o = o#phrase _x in o + | Unlet _x -> + let o = o#phrase _x in o | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let o = o#phrase sh_expr in let o = @@ -1349,10 +1368,11 @@ class fold = | Variant ((_x, _x_i1)) -> let o = o#name _x in let o = o#option (fun o -> o#pattern) _x_i1 in o - | Operation (name, ps, k) -> + | Operation (name, ps, k, b) -> let o = o#name name in let o = o#list (fun o -> o#pattern) ps in let o = o#pattern k in + let o = o#linearity b in o | Negative _x -> let o = o#list (fun o -> o#name) _x in o @@ -1452,9 +1472,10 @@ class fold = | Record _x -> let o = o#row _x in o | Variant _x -> let o = o#row _x in o | Effect r -> let o = o#row r in o - | Operation (_x, _x_i1) -> + | Operation (_x, _x_i1, _x_i2) -> let o = o#list (fun o -> o#datatype) _x in - let o = o#datatype _x_i1 in o + let o = o#datatype _x_i1 in + let o = o#linearity _x_i2 in o | Table (_t, _x, _x_i1, _x_i2) -> let o = o#datatype _x in let o = o#datatype _x_i1 in @@ -1677,6 +1698,9 @@ class fold_map = method bool : bool -> ('self_type * bool) = function | false -> (o, false) | true -> (o, true) + method linearity : DeclaredLinearity.t -> ('self_type * DeclaredLinearity.t) = + DeclaredLinearity.(function | Unl -> (o, Unl) | Lin -> (o, Lin)) + method unary_op : UnaryOp.t -> ('self_type * UnaryOp.t) = let open UnaryOp in function | Minus -> (o, Minus) @@ -1712,11 +1736,12 @@ class fold_map = method type_variable : SugarTypeVar.t -> ('self_type * SugarTypeVar.t) = let open SugarTypeVar in function - | TUnresolved (name, subkind_opt, freedom) -> + | TUnresolved (name, (is_eff, subkind_opt), freedom) -> let o, name' = o#name name in + let o, is_eff' = o#bool is_eff in let o, subkind_opt' = o#option (fun o -> o#subkind) subkind_opt in let o, freedom' = o#freedom freedom in - o, TUnresolved (name', subkind_opt', freedom') + o, TUnresolved (name', (is_eff', subkind_opt'), freedom') | v -> o#unknown v @@ -1948,14 +1973,20 @@ class fold_map = let (o, _x_i1) = o#option (fun o -> o#phrase) _x_i1 in let o, _x_i2 = o#option (fun o -> o#typ) _x_i2 in (o, (ConstructorLit ((_x, _x_i1, _x_i2)))) - | DoOperation (op, ps, t) -> + | DoOperation (op, ps, t, b) -> let (o, op) = o#phrase op in let (o, t) = o#option (fun o -> o#typ) t in let (o, ps) = o#list (fun o -> o#phrase) ps in - (o, DoOperation (op, ps, t)) + (o, DoOperation (op, ps, t, b)) | Operation _x -> let (o, _x) = o#name _x in (o, Operation _x) + | Linlet _x -> + let (o, _x) = o#phrase _x in + (o, Linlet _x) + | Unlet _x -> + let (o, _x) = o#phrase _x in + (o, Unlet _x) | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let (o, m) = o#phrase sh_expr in let (o, params) = @@ -2234,11 +2265,12 @@ class fold_map = let (o, _x) = o#name _x in let (o, _x_i1) = o#option (fun o -> o#pattern) _x_i1 in (o, (Variant ((_x, _x_i1)))) - | Operation (name, ps, k) -> + | Operation (name, ps, k, b) -> let (o, name) = o#name name in let (o, ps) = o#list (fun o -> o#pattern) ps in let (o, k) = o#pattern k in - (o, Operation (name, ps, k)) + let (o, b) = o#linearity b in + (o, Operation (name, ps, k, b)) | Negative _x -> let (o, _x) = o#list (fun o -> o#name) _x in (o, (Negative _x)) | Record ((_x, _x_i1)) -> @@ -2369,9 +2401,11 @@ class fold_map = | Record _x -> let (o, _x) = o#row _x in (o, (Record _x)) | Variant _x -> let (o, _x) = o#row _x in (o, (Variant _x)) | Effect r -> let (o, r) = o#row r in (o, Effect r) - | Operation (_x, _x_i1) -> + | Operation (_x, _x_i1, _x_i2) -> let (o, _x) = o#list (fun o -> o#datatype) _x in - let (o, _x_i1) = o#datatype _x_i1 in (o, Operation (_x, _x_i1)) + let (o, _x_i1) = o#datatype _x_i1 in + let (o, _x_i2) = o#linearity _x_i2 in + (o, Operation (_x, _x_i1, _x_i2)) | Table (_t, _x, _x_i1, _x_i2) -> let (o, _x) = o#datatype _x in let (o, _x_i1) = o#datatype _x_i1 in diff --git a/core/sugarTraversals.mli b/core/sugarTraversals.mli index d3fb2a34d..943e4a310 100644 --- a/core/sugarTraversals.mli +++ b/core/sugarTraversals.mli @@ -25,6 +25,7 @@ class map : method float : float -> float method char : char -> char method bool : bool -> bool + method linearity : DeclaredLinearity.t -> DeclaredLinearity.t method timestamp : Timestamp.t -> Timestamp.t method unary_op : UnaryOp.t -> UnaryOp.t method tyunary_op : tyarg list * UnaryOp.t -> tyarg list * UnaryOp.t @@ -110,6 +111,7 @@ class fold : method char : char -> 'self method timestamp : Timestamp.t -> 'self method bool : bool -> 'self + method linearity : DeclaredLinearity.t -> 'self method unary_op : UnaryOp.t -> 'self method tyunary_op : tyarg list * UnaryOp.t -> 'self method binder : Binder.with_pos -> 'self @@ -187,6 +189,7 @@ object ('self) method binop : BinaryOp.t -> 'self * BinaryOp.t method tybinop : tyarg list * BinaryOp.t -> 'self * (tyarg list * BinaryOp.t) method bool : bool -> 'self * bool + method linearity : DeclaredLinearity.t -> 'self * DeclaredLinearity.t method char : char -> 'self * char method timestamp : Timestamp.t -> 'self * Timestamp.t method constant : Constant.t -> 'self * Constant.t diff --git a/core/sugartoir.ml b/core/sugartoir.ml index 6d2d8077c..c0cad95f3 100644 --- a/core/sugartoir.ml +++ b/core/sugartoir.ml @@ -982,7 +982,7 @@ struct cofv (I.inject (name, I.record ([], None), t)) | ConstructorLit (name, Some e, Some t) -> cofv (I.inject (name, ev e, t)) - | DoOperation (op, ps, Some t) -> + | DoOperation (op, ps, Some t, _) -> let name = let o = (object (o) inherit SugarTraversals.fold as super @@ -1001,6 +1001,10 @@ struct let vs = evs ps in I.do_operation (name, vs, t) | Operation _ -> assert false + (* FIXME: I don't know what's this. I suppose it is related to semantics, + but Unlet and Linlet do not influence semantics. *) + | Unlet _ -> assert false + | Linlet _ -> assert false | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> (* it happens that the ambient effects are the right ones for all of the patterns here (they match those of the diff --git a/core/sugartypes.ml b/core/sugartypes.ml index 86de77bfb..54ebb997f 100644 --- a/core/sugartypes.ml +++ b/core/sugartypes.ml @@ -68,13 +68,20 @@ type tyarg = Types.type_arg *) let default_subkind : Subkind.t = (lin_unl, res_any) -let default_effect_subkind : Subkind.t = (lin_unl, res_any) -type kind = PrimaryKind.t option * Subkind.t option - [@@deriving show] +(* NOTICE: `lin_any` here means this eff_row_var can be unified with + linear or unlimited row types *) + +let lincont_enabled = Settings.get Basicsettings.CTLinearity.enabled + +let default_effect_lin : Linearity.t = if lincont_enabled then lin_any else lin_unl +let default_effect_subkind : Subkind.t =(default_effect_lin, res_any) +type kind = PrimaryKind.t option * Subkind.t option + [@@deriving show] + module SugarTypeVar = struct @@ -82,7 +89,8 @@ struct about its primary kind. This is filled in when resolving the variable *) (* FIXME: the above comment may well be false now - check *) type t = - | TUnresolved of Name.t * Subkind.t option * Freedom.t + | TUnresolved of Name.t * (bool * Subkind.t option) * Freedom.t + (* true: is an effect var *) | TResolvedType of Types.meta_type_var | TResolvedRow of Types.meta_type_var | TResolvedPresence of Types.meta_type_var @@ -92,8 +100,8 @@ let is_resolved = function | TUnresolved _ -> false | _ -> true -let mk_unresolved name subkind_opt freedom_opt = - TUnresolved (name, subkind_opt, freedom_opt) +let mk_unresolved name ?(is_eff=false) subkind_opt freedom_opt = + TUnresolved (name, (is_eff, subkind_opt), freedom_opt) let mk_resolved_tye point : t = TResolvedType point @@ -106,8 +114,8 @@ let mk_resolved_presence point : t = let get_unresolved_exn = function - | TUnresolved (name, subkind, freedom) -> - name, subkind, freedom + | TUnresolved (name, (is_eff, subkind), freedom) -> + name, (is_eff, subkind), freedom | _ -> raise (internal_error @@ -195,7 +203,7 @@ module Datatype = struct | Record of row | Variant of row | Effect of row - | Operation of with_pos list * with_pos + | Operation of with_pos list * with_pos * DeclaredLinearity.t | Table of Temporality.t * with_pos * with_pos * with_pos | List of with_pos | TypeApplication of string * type_arg list @@ -245,7 +253,7 @@ module Pattern = struct | Variant of Name.t * with_pos option (* | Effect of Name.t * with_pos list * with_pos *) (* | Effect2 of with_pos list * with_pos option *) - | Operation of Label.t * with_pos list * with_pos + | Operation of Label.t * with_pos list * with_pos * DeclaredLinearity.t | Negative of Name.t list | Record of (Name.t * with_pos) list * with_pos option | Tuple of with_pos list @@ -474,9 +482,11 @@ and phrasenode = | Instantiate of phrase | Generalise of phrase | ConstructorLit of Name.t * phrase option * Types.datatype option - | DoOperation of phrase * phrase list * Types.datatype option + | DoOperation of phrase * phrase list * Types.datatype option * DeclaredLinearity.t | Operation of Name.t | Handle of handler + | Unlet of phrase + | Linlet of phrase | Switch of phrase * (Pattern.with_pos * phrase) list * Types.datatype option | Receive of (Pattern.with_pos * phrase) list * Types.datatype option @@ -640,7 +650,7 @@ struct | List ps -> union_map pattern ps | Cons (p1, p2) -> union (pattern p1) (pattern p2) | Variant (_, popt) -> option_map pattern popt - | Operation (_, ps, kopt) -> union (union_map pattern ps) (pattern kopt) + | Operation (_, ps, kopt, _) -> union (union_map pattern ps) (pattern kopt) | Record (fields, popt) -> union (option_map pattern popt) (union_map (snd ->- pattern) fields) @@ -792,12 +802,14 @@ struct diff (option_map phrase where) pat_bound; diff (union_map (snd ->- phrase) fields) pat_bound] | DBTemporalJoin (_, p, _) -> phrase p - | DoOperation (_, ps, _) -> union_map phrase ps + | DoOperation (_, ps, _, _) -> union_map phrase ps | Operation _ -> empty | QualifiedVar _ -> empty | TryInOtherwise (p1, pat, p2, p3, _ty) -> union (union_map phrase [p1; p2; p3]) (pattern pat) | Raise -> empty + | Unlet p -> phrase p + | Linlet p -> phrase p and binding (binding': binding) : StringSet.t (* vars bound in the pattern *) * StringSet.t (* free vars in the rhs *) = diff --git a/core/transformSugar.ml b/core/transformSugar.ml index 3b3d668a1..b0af370a4 100644 --- a/core/transformSugar.ml +++ b/core/transformSugar.ml @@ -491,9 +491,9 @@ class transform (env : Types.typing_environment) = let (o, e, _) = option o (fun o -> o#phrase) e in let (o, t) = o#datatype t in (o, ConstructorLit (name, e, Some t), t) - | DoOperation (name, ps, Some t) -> + | DoOperation (name, ps, Some t, b) -> let (o, ps, _) = list o (fun o -> o#phrase) ps in - (o, DoOperation (name, ps, Some t), t) + (o, DoOperation (name, ps, Some t, b), t) | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let (input_row, input_t, output_row, output_t) = sh_descr.shd_types in let (o, expr, _) = o#phrase sh_expr in @@ -726,10 +726,10 @@ class transform (env : Types.typing_environment) = | Variant (name, p) -> let (o, p) = optionu o (fun o -> o#pattern) p in (o, Variant (name, p)) - | Operation (name, ps, k) -> + | Operation (name, ps, k, b) -> let (o, ps) = listu o (fun o -> o#pattern) ps in let (o, k) = o#pattern k in - (o, Operation (name, ps, k)) + (o, Operation (name, ps, k, b)) | Negative name -> (o, Negative name) | Record (fields, rest) -> let (o, fields) = diff --git a/core/typeSugar.ml b/core/typeSugar.ml index a91b81c1b..e9d9fcaf8 100644 --- a/core/typeSugar.ml +++ b/core/typeSugar.ml @@ -93,6 +93,8 @@ struct | Upcast (p, _, _) | Instantiate p | Generalise p + | Linlet p + | Unlet p | Escape (_, p) -> is_pure p | ConstructorLit (_, p, _) -> opt_generalisable p | RecordLit (fields, p) -> @@ -178,7 +180,7 @@ struct | Tuple ps -> List.for_all is_safe_pattern ps | HasType (p, _) | As (_, p) -> is_safe_pattern p - | Operation (_, ps, k) -> + | Operation (_, ps, k, _) -> List.for_all is_safe_pattern ps && is_safe_pattern k and is_pure_regex = function (* don't check whether it can fail; just check whether it @@ -1642,6 +1644,7 @@ end end +(* Tag: context begin *) type context = Types.typing_environment = { (* mapping from variables to type schemes *) var_env : Types.environment; @@ -1659,16 +1662,23 @@ type context = Types.typing_environment = { (* the current effects *) effect_row : Types.row; + (* the current continuation linearity. + It will be mapped to a pair of bools, where + the first bool value indicates whether the current term is in a linear continuation currently + the second bool value indicates whether the current term is bound by a linlet *) + cont_lin : int; + (* Whether this is runs on desugared code, and so some non-user facing constructs are permitted. *) desugared : bool; } -let empty_context eff desugared = +let empty_context contlin eff desugared = { var_env = Env.empty; rec_vars = StringSet.empty; tycon_env = Env.empty; effect_row = eff; + cont_lin = contlin; desugared } let bind_var context (v, t) = {context with var_env = Env.bind v t context.var_env} @@ -1678,12 +1688,106 @@ let bind_effects context r = {context with effect_row = Types.flatten_r let lookup_effect context name = match context.effect_row with - | Types.Row (fields, _, _) -> begin match Utility.StringMap.find_opt name fields with + | Types.Row (fields, _, _) -> + begin match Utility.StringMap.find_opt name fields with | Some (Types.Present t) -> Some t | _ -> None end | _ -> raise (internal_error "Effect row in the context is not a row") + +module LinCont = struct + (* Some helper functions for control-flow linearity. *) + + let is_enabled = (Settings.get Basicsettings.CTLinearity.enabled) + + let enabled = fun f -> + if is_enabled then f () else () + (* + NOTE: The meaning of Any and Unl for effect row types is different from other types: + - An effect row type with kind `Any` means it can be linear or unlimited. + - An effect row type with kind `Unl` means it must be linear! + Moreover, for effect signatures, `=>` means linear signature which must have a linear + continuation, and `=@` means signature which may have any continuation. + This is just an implementation trick to reuse the previous mechanism of unification. + *) + + let make_operation_type : ?linear:bool -> Types.datatype list -> Types.datatype -> Types.datatype + = fun ?(linear=false) args range -> + let lin = if is_enabled then DeclaredLinearity.(if linear then Lin else Unl) + else DeclaredLinearity.Unl + in Types.Operation (Types.make_tuple_type args, range, lin) + + (* linear continuation(function) is still represented by `-@`, so we still use `islin` *) + let make_continuation_type = fun islin inp eff out -> + if is_enabled + then (Types.make_function_type ~linear:(islin) inp eff out) + else (Types.make_function_type ~linear:(false) inp eff out) + + + (* + `cont_lin` (continuation linearity) is represented by an + integer, which is mapped to a pair of bools by the global + `cont_lin_map`. + - `cont_lin.first = true` : the current term is in a linear + continuation. Nothing to do. + - `cont_lin.first = false` : the current term is in an unlimited + continuation. We need to guarantee it does not use linear + variables bound outside. + - `cont_lin.second = true` : the current term is bound by linlet + (i.e. has a linear continuation). If the current term is not + pure, we should guarantee that the current effect type + `effect_row` is linear. + - `cont_lin.second = false` : the current term is bound by let + (i.e. has an unlimited continuation). Nothing to do. + + We implement `cont_lin = (false, false)` by default because it + is more compatible with previous effect handlers. + + The reason to use a global map is that we want to make sure + sequenced terms (terms in the "same scope") have the same + `cont_lin`. The only places where `cont_lin` is updated to a new + one is where `effect_row` is updated to a new one. (I think + `effect_row` also uses some global mechanism for unification.) + *) + let count = ref 0 + + let default = (false, false) + + (* `-1` is the `cont_lin` of `empty_typing_environment`. It is + supposed to be used in the typing of default global bindings. *) + let linmap = ref (IntMap.add (-1) default IntMap.empty) + + let getnew () = + if is_enabled then ( + let newx = !count in + let () = count := newx + 1 in + let () = linmap := IntMap.add newx default !linmap in + newx ) + else -1 + + let is_in_linlet context = + if is_enabled then fst <| IntMap.find context.cont_lin !linmap + else false + + let is_bound_by_linlet context = + if is_enabled then snd <| IntMap.find context.cont_lin !linmap + else false + + let update_in_linlet context a = + enabled (fun () -> + let b = is_bound_by_linlet context in + linmap := IntMap.add context.cont_lin (a, b) !linmap + ) + + let update_bound_by_linlet context b = + enabled (fun () -> + let a = is_in_linlet context in + linmap := IntMap.add context.cont_lin (a, b) !linmap + ) +end + + (* TODO(dhil): I have extracted the Usage abstraction from my name hygiene/compilation unit patch. The below module is a compatibility module which will make it easier for me to merge my other branch @@ -1730,6 +1834,8 @@ module Usage: sig val filter : (Ident.t -> int -> bool) -> t -> t (* Iterates over entries in a given container. *) val iter : (Ident.t -> int -> unit) -> t -> unit + (* Folds over entries in a given container. *) + val fold : (Ident.t -> int -> 'b -> 'b) -> t -> 'b -> 'b (* Returns a usage container that does not contain any of the names in the given set. *) val restrict : t -> Ident.Set.t -> t @@ -1789,6 +1895,9 @@ end = struct let iter f usages = Ident.Map.iter f usages + let fold f usages = + Ident.Map.fold f usages + let restrict usages idents = filter (fun v _ -> not (Ident.Set.mem v idents)) usages @@ -1870,8 +1979,8 @@ let add_empty_usages (p, t) = (p, t, Usage.empty) let type_unary_op pos env = let datatype = datatype env.tycon_env in function - | UnaryOp.Minus -> add_empty_usages (datatype "(Int) -> Int") - | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) -> Float") + | UnaryOp.Minus -> add_empty_usages (datatype "(Int) { |_::Any}-> Int") + | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) { |_::Any}-> Float") | UnaryOp.Name n -> try add_usages (Utils.instantiate env.var_env n) (Usage.singleton n) @@ -2039,7 +2148,7 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty let unwrap_at : string -> Pattern.with_pos -> Pattern.with_pos list = fun name p -> let open Pattern in match p.node with - | Operation (name', ps, _) when name=name' -> ps + | Operation (name', ps, _, _) when name=name' -> ps | Operation _ -> [] | Variable _ | Any | As _ | HasType _ | Negative _ | Nil | Cons _ | List _ | Tuple _ | Record _ | Variant _ | Constant _ -> assert false in @@ -2210,7 +2319,7 @@ let check_for_duplicate_names : Position.t -> Pattern.with_pos list -> string li List.fold_right (fun p binderss -> gather binderss p) ps binderss | Variant (_, p) -> opt_app (fun p -> gather binderss p) binderss p - | Operation (_, ps, k) -> + | Operation (_, ps, k, _) -> let binderss' = List.fold_right (fun p binderss -> gather binderss p) ps binderss in @@ -2248,7 +2357,7 @@ let rec pattern_env : Pattern.with_pos -> Types.datatype Env.t = | HasType (p,_) -> pattern_env p | Variant (_, Some p) -> pattern_env p | Variant (_, None) -> Env.empty - | Operation (_, ps, k) -> + | Operation (_, ps, k, _) -> let env = List.fold_right (pattern_env ->- Env.extend) ps Env.empty in Env.extend env (pattern_env k) | Negative _ -> Env.empty @@ -2339,20 +2448,22 @@ let type_pattern ?(linear_vars=true) closed let p = tp p in let vtype typ = Types.Variant (make_singleton_row (name, Present (typ p))) in Pattern.Variant (name, Some (erase p)), (vtype ot, vtype it) - | Pattern.Operation (name, ps, k) -> + | Pattern.Operation (name, ps, k, linearity) -> + let is_lincase = linearity = DeclaredLinearity.Lin in (* Auxiliary machinery for typing effect patterns *) let rec type_resumption_pat (kpat : Pattern.with_pos) : Pattern.with_pos * (Types.datatype * Types.datatype) = let fresh_resumption_type () = let domain = fresh_var () in let codomain = fresh_var () in let effrow = Types.make_empty_open_row default_effect_subkind in - Types.make_function_type [domain] effrow codomain + LinCont.make_continuation_type is_lincase [domain] effrow codomain in let pos' = kpat.pos in let open Pattern in match kpat.node with | Any -> let t = fresh_resumption_type () in + if is_lincase && LinCont.is_enabled then Gripers.die pos' ("The linear continuation is not bound.") else (); kpat, (t, t) | Variable bndr -> let xtype = fresh_resumption_type () in @@ -2377,14 +2488,14 @@ let type_pattern ?(linear_vars=true) closed (* Construct operation type, i.e. op : A -> B or op : B *) match domain, codomain with | [], [] | _, [] -> assert false (* The continuation is at least unary *) - | [], [t] -> Types.Operation (Types.unit_type, t) - | [], ts -> Types.make_tuple_type ts + | [], [t] -> Types.Operation (Types.unit_type, t, linearity) + | [], ts -> Types.make_tuple_type ts (* FIXME: WT: I don't understand this case *) | ts, [t] -> - Types.make_operation_type ts t + LinCont.make_operation_type ~linear:is_lincase ts t | ts, ts' -> (* parameterised continuation *) let t = ListUtils.last ts' in - Types.make_operation_type ts t + LinCont.make_operation_type ~linear:is_lincase ts t in t in @@ -2397,7 +2508,7 @@ let type_pattern ?(linear_vars=true) closed | None -> (eff ot, eff it) in - Pattern.Operation (name, List.map erase ps, erase k), (ot, it) + Pattern.Operation (name, List.map erase ps, erase k, linearity), (ot, it) | Negative names -> let row_var = Types.fresh_row_variable (lin_any, res_any) in @@ -2510,7 +2621,7 @@ let make_ft_poly_curry declared_linearity ps effects return_type = | [p] -> [], make_ftcon declared_linearity (args p, effects, return_type) | p::ps -> let qs, t = ft ps in - let q, eff = Types.fresh_row_quantifier default_subkind in + let q, eff = Types.fresh_row_quantifier default_effect_subkind in q::qs, make_ftcon declared_linearity (args p, eff, t) | [] -> assert false in Types.for_all (ft ps) @@ -2635,6 +2746,90 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = end; in + (* Auxiliarty functions for control-flow linearity *) + (* check if an effect row type can be made linear *) + let _canlin_effrow = fun row -> + (* trick: for effect row types, Unl means Lin, Any means Any *) + Types.Unl.can_type_be row + in + let makelin_effrow = fun row -> + (* trick: for effect row types, Unl means Lin, Any means Any *) + if Types.Unl.can_type_be row then + Types.Unl.make_type row + else + Gripers.die pos ("Effect row type " ^ Types.string_of_datatype row + ^ " can not be made linear (represented by Unl).") + in + (* check if a term uses any linear variable *) + let _haslin_term = fun usages -> + (* trick: for effect row types, Unl means Lin, Any means Any *) + let env = context.var_env in + Usage.fold + (fun v _ b -> + let t = Env.find v env in + b || not (Types.Unl.can_type_be t)) + usages false + in + (* make all variables in a term unlimited *) + let makeunl_term = fun usages -> + let env = context.var_env in + Usage.iter + (fun v _ -> + let t = Env.find v env in + if Types.Unl.can_type_be t then + Types.Unl.make_type t + else + Gripers.die pos ("Variable " ^ v ^ " of linear type " ^ Types.string_of_datatype t + ^ " is used in a non-linear continuation.")) + usages + in + (* update control-flow linearity without automatically inserting xlin *) + let update_cflinearity p usages = + (LinCont.enabled (fun () -> + if (LinCont.is_bound_by_linlet context) + (* make `context.effect_row` linear if the current term is bound by a linlet *) + then makelin_effrow (context.effect_row) + else (); + if (not (LinCont.is_in_linlet context)) + (* make all vars in `p` unlimited if the current term is in the body of an unlet *) + then makeunl_term usages + else (); + (match p with + | Linlet _ -> LinCont.update_in_linlet context true + | Unlet _ -> LinCont.update_in_linlet context false + | DoOperation (_,_,_,lin) -> + if lin = DeclaredLinearity.Unl then LinCont.update_in_linlet context false + | _ -> ()) + )) + in + (* update control-flow linearity with automatically inserting xlin + This function isn't very useful as usually we don't know the + linearity of vars at the beginning until they are unified + (e.g., applied to functions). *) + (* let update_cflinearity_auto_xlin p usages = + (LinCont.enabled (fun () -> + if (LinCont.is_bound_by_linlet context) + (* make `context.effect_row` linear if the current term is bound by a linlet *) + then makelin_effrow (context.effect_row) + else (); + if (not (LinCont.is_in_linlet context)) + then + if haslin_term usages then ( + (* automatically insert a xlin if the term uses linear variables *) + LinCont.update_in_linlet context true; + makelin_effrow (context.effect_row) + ) + (* make all vars in `p` unlimited if the current term is in the body of an unlet *) + else makeunl_term usages + else (); + (match p with + | Linlet _ -> LinCont.update_in_linlet context true + | Unlet _ -> LinCont.update_in_linlet context false + | DoOperation (_,_,_,lin) -> + if lin = DeclaredLinearity.Unl then LinCont.update_in_linlet context false + | _ -> ()) + )) + in *) let find_opname phrase = let o = object (o) inherit SugarTraversals.fold as super @@ -2777,7 +2972,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = end | FunLit (argss_prev, lin, fnlit, location) -> let (pats, body) = Sugartypes.get_normal_funlit fnlit in - (* names of all variables in the parameter patterns *) + (* vs: names of all variables in the parameter patterns *) let vs = check_for_duplicate_names pos (List.flatten pats) in let (pats_init, pats_tail) = from_option ([], []) (unsnoc_opt pats) in let tpc' = if DeclaredLinearity.is_linear lin then tpc else tpcu in @@ -2792,8 +2987,10 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let effects = Types.make_empty_open_row default_effect_subkind in let body = type_check ({context with var_env = env'; - effect_row = effects}) body in + effect_row = effects; + cont_lin = LinCont.getnew ()}) body in + (* make types of parameters unlimited if they are not used exactly once *) let () = Env.iter (fun v t -> let uses = Usage.uses_of v (usages body) in @@ -2804,6 +3001,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = Gripers.non_linearity pos uses v t) pat_env in + (* make types of env vars unlimited if they are used in unlimited functions *) let () = if DeclaredLinearity.is_nonlinear lin then Usage.iter @@ -3409,7 +3607,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = if Settings.get Basicsettings.Sessions.exceptions_enabled && Settings.get Basicsettings.Sessions.expose_session_fail then - let ty = Types.make_operation_type [] (Types.empty_type) in + let ty = LinCont.make_operation_type [] (Types.empty_type) in Types.row_with (Value.session_exception_operation, T.Present ty) inner_effects else inner_effects in @@ -3505,6 +3703,8 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = in RangeLit (erase l, erase r), Types.make_list_type Types.int_type, Usage.combine (usages l) (usages r) + + (* Tag: FnAppl begin *) | FnAppl (f, ps) -> let f = tc f in let ps = List.map (tc) ps in @@ -3589,6 +3789,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = match Types.concrete_type ft with | T.Function _ -> unify ~handle:Gripers.fun_apply (term, funt) | T.Lolli _ -> unify ~handle:Gripers.fun_apply (term, lolt) + (* NOTE: non-linear function by default? why? *) | _ -> unify_or ~handle:Gripers.fun_apply ~pos (term, funt) (term, lolt) end; FnAppl (erase f, List.map erase ps), rettyp, Usage.combine_many (usages f :: List.map usages ps) @@ -3853,7 +4054,8 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = Conditional (erase i, erase t, erase e), (typ t), Usage.combine (usages i) (Usage.align [usages t; usages e]) | Block (bindings, e) -> let context', bindings, usage_builder = type_bindings context bindings in - let e = type_check (Types.extend_typing_environment context context') e in + let cur_context = (Types.extend_typing_environment context context') in + let e = type_check cur_context e in Block (bindings, erase e), typ e, usage_builder (usages e) | Regex r -> Regex (type_regex context r), @@ -3974,7 +4176,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = (* effect handlers *) | Handle { sh_expr = m; sh_value_cases = val_cases; sh_effect_cases = eff_cases; sh_descr = descr; } -> ignore - (if not (Settings.get Basicsettings.Handlers.enabled) + (if not (Settings.get Basicsettings.Handlers.enabled) then raise (Errors.disabled_extension ~pos ~setting:("enable_handlers", true) ~flag:"--enable-handlers" "Handlers")); @@ -4007,10 +4209,12 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = env ++ pattern_env p) henv (List.map fst typed_bindings) in - (param_env, typed_bindings, { descr with shd_params = Some { shp_bindings = List.map (fun (pat, body) -> erase_pat pat, erase body) typed_bindings; - shp_types = pat_types } }) + (param_env, typed_bindings, { descr with shd_params = + Some { shp_bindings = List.map (fun (pat, body) -> erase_pat pat, erase body) typed_bindings; + shp_types = pat_types } }) | None -> (henv, [], descr) in + (* Tag: Handle type_cases begin *) let type_cases val_cases eff_cases = let wild_row () = let fresh_row = Types.make_empty_open_row default_effect_subkind in @@ -4060,7 +4264,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = erase_ann pat in let effname, kpat = match pat.node with - | Pattern.Operation (name, _, k) -> name, k + | Pattern.Operation (name, _, k, _) -> name, k | _ -> assert false in let effrow = @@ -4068,9 +4272,9 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = not (Settings.get Basicsettings.Sessions.expose_session_fail) && String.equal effname Value.session_exception_operation then - Types.Effect (Types.make_empty_open_row (lin_any, res_any)) + Types.Effect (Types.make_empty_open_row default_effect_subkind) else - Types.Effect (Types.make_singleton_open_row (effname, Types.Present efftyp) (lin_any, res_any)) in + Types.Effect (Types.make_singleton_open_row (effname, Types.Present efftyp) default_effect_subkind) in unify ~handle:Gripers.handle_effect_patterns ((uexp_pos pat, effrow), no_pos (T.Effect inner_eff)); let pat, kpat = @@ -4247,13 +4451,15 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = (fun name p -> if TypeUtils.is_builtin_effect name then p - else Types.fresh_presence_variable (lin_unl, res_any)) (* It is questionable whether it is ever correct to + else Types.fresh_presence_variable default_effect_subkind) (* It is questionable whether it is ever correct to make absent operations polymorphic in their presence. *) operations in T.Row (operations', rho, dual) in - let m_context = { context with effect_row = Types.make_empty_open_row default_effect_subkind } in + let m_context = { context with + effect_row = Types.make_empty_open_row default_effect_subkind; + cont_lin = LinCont.getnew () } in let m = type_check m_context m in (* Type-check the input computation m under current context *) let m_effects = T.Effect m_context.effect_row in (* Most of the work is done by `type_cases'. *) @@ -4299,15 +4505,41 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = sh_effect_cases = erase_cases eff_cases; sh_value_cases = erase_cases val_cases; sh_descr = descr }, body_type, usages - | DoOperation (op, ps, _) -> - let op = tc op in + | DoOperation (op, ps, _, linearity) -> + let is_lindo = if LinCont.is_enabled then linearity = DeclaredLinearity.Lin else false in + let () = if is_lindo then () + else LinCont.update_bound_by_linlet context false + (* do is implicitly bound by an unlet *) + in + let op_linearity = if is_lindo then lin_unl else lin_any + (* lin_unl: linear operation; lin_any: unlimited operation *) + in + (* inline the type checking of Operation here to be able to + use is_lindo *) + let op = (match op.node with + | Operation name -> + if String.equal name Value.session_exception_operation then + if not context.desugared then + Gripers.die pos "The session failure effect SessionFail is not directly invocable (use `raise` instead)" + else + (Operation name, Types.empty_type, Usage.empty) + else + let t = + match lookup_effect context name with + | Some t -> t + | None -> Types.fresh_type_variable (op_linearity, res_any) + in + (Operation name, t, Usage.empty) + | _ -> Gripers.die pos "Do should take an operation label.") + in + let op = (let a,b,c = op in with_pos pos a,b,c) in let ps = List.map (tc) ps in let doop, rettyp, usage, opt = match Types.concrete_type (typ op) with | T.ForAll (_, (T.Operation _)) as t -> begin match Instantiate.typ t with - | tyargs, T.Operation (pts, rettyp) -> + | tyargs, T.Operation (pts, rettyp, _) -> (* quantifiers for the return type *) let rqs = (* the free type variables in the arguments (and effects) *) @@ -4327,31 +4559,33 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = in let rettyp = Types.for_all (rqs, rettyp) in - let opt = T.Operation (pts, rettyp) in + let opt = T.Operation (pts, rettyp, linearity) in let op' = erase op in let sugar_rqs = List.map SugarQuantifier.mk_resolved rqs in - let e = tabstr (sugar_rqs, DoOperation (with_dummy_pos (tappl (op'.node, tyargs)), List.map erase ps, Some rettyp)) in + let e = tabstr (sugar_rqs, DoOperation (with_dummy_pos (tappl (op'.node, tyargs)), List.map erase ps, Some rettyp, linearity)) in e, rettyp, Usage.combine_many (usages op :: List.map usages ps), opt | _ -> assert false end - | T.Operation (_, rettyp) as opt -> - DoOperation (erase op, List.map erase ps, Some rettyp), rettyp, Usage.combine_many (usages op :: List.map usages ps), opt + | T.Operation (pts, rettyp, _) -> + let opt = T.Operation (pts, rettyp, linearity) in + DoOperation (erase op, List.map erase ps, Some rettyp, linearity), rettyp, Usage.combine_many (usages op :: List.map usages ps), opt | opt -> + (* fresh variable case *) let rettyp = Types.fresh_type_variable (lin_unl, res_any) in - DoOperation (erase op, List.map erase ps, Some rettyp), rettyp, Usage.combine_many (usages op :: List.map usages ps), opt + DoOperation (erase op, List.map erase ps, Some rettyp, linearity), rettyp, Usage.combine_many (usages op :: List.map usages ps), opt in let opname = find_opname (erase op) in - let infer_opt = no_pos (Types.make_operation_type (List.map typ ps) rettyp) in + let infer_opt = no_pos (LinCont.make_operation_type ~linear:is_lindo (List.map typ ps) rettyp) in let term = (exp_pos op, opt) in let row = if Settings.get Basicsettings.Sessions.exceptions_enabled && not (Settings.get Basicsettings.Sessions.expose_session_fail) && String.equal opname Value.session_exception_operation then - Types.make_empty_open_row (lin_unl, res_effect) + Types.make_empty_open_row default_effect_subkind else - Types.make_singleton_open_row (opname, T.Present (typ op)) (lin_unl, res_effect) in + Types.make_singleton_open_row (opname, T.Present (typ op)) default_effect_subkind in let p = Position.resolve_expression pos in let () = unify ~handle:Gripers.do_operation @@ -4359,20 +4593,23 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = unify ~handle:Gripers.do_operation (no_pos (T.Effect context.effect_row), (p, T.Effect row)) in + (* postponed *) + (* let () = if is_lindo then () *) + (* else LinCont.update_in_linlet context false *) + (* in *) doop, rettyp, usage - | Operation name -> - if String.equal name Value.session_exception_operation then - if not context.desugared then - Gripers.die pos "The session failure effect SessionFail is not directly invocable (use `raise` instead)" - else - (Operation name, Types.empty_type, Usage.empty) - else - let t = - match lookup_effect context name with - | Some t -> t - | None -> Types.fresh_type_variable (lin_unl, res_any) - in - (Operation name, t, Usage.empty) + | Operation _ -> + Gripers.die pos "The operation label is used in invalid positions." + | Linlet p -> + let () = LinCont.update_bound_by_linlet context true in + let (p, t, usages) = type_check context p in + (* let () = LinCont.update_in_linlet context true in *) (* postponed *) + (WithPos.node p, t, usages) + | Unlet p -> + let () = LinCont.update_bound_by_linlet context false in + let (p, t, usages) = type_check context p in + (* let () = LinCont.update_in_linlet context false in *) (* postponed *) + (WithPos.node p, t, usages) | Switch (e, binders, _) -> let e = tc e in let binders, pattern_type, body_type = type_cases binders in @@ -4394,7 +4631,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let try_effects = if Settings.get Basicsettings.Sessions.expose_session_fail then Types.row_with - (Value.session_exception_operation, T.Present (Types.make_operation_type [] Types.empty_type)) + (Value.session_exception_operation, T.Present (LinCont.make_operation_type [] Types.empty_type)) (T.Row (StringMap.empty, rho, false)) else T.Row (StringMap.empty, rho, false) @@ -4479,7 +4716,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let effects = if Settings.get Basicsettings.Sessions.expose_session_fail then Types.make_singleton_open_row - (Value.session_exception_operation, T.Present (Types.make_operation_type [] Types.empty_type)) + (Value.session_exception_operation, T.Present (LinCont.make_operation_type [] Types.empty_type)) default_effect_subkind else Types.make_empty_open_row default_effect_subkind @@ -4487,7 +4724,10 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = unify ~handle:Gripers.raise_effect (no_pos (T.Effect context.effect_row), (Position.resolve_expression pos, T.Effect effects)); (Raise, Types.fresh_type_variable (lin_any, res_any), Usage.empty) - in with_pos pos e, t, usages + in + let p = with_pos pos e in + let () = update_cflinearity expr usages in + p, t, usages (* [type_binding] takes XXX YYY (FIXME) The input context is the environment in which to type the bindings. @@ -4520,7 +4760,7 @@ and type_binding : context -> binding -> binding * context * Usage.t = let exp_pos (p,_,_) = uexp_pos p in let pos_and_typ e = (exp_pos e, typ e) in - let empty_context = empty_context context.effect_row context.desugared in + let empty_context = empty_context context.cont_lin context.effect_row context.desugared in let module T = Types in let typed, ctxt, usage = match def with @@ -4584,7 +4824,6 @@ and type_binding : context -> binding -> binding * context * Usage.t = | None -> context, make_ft lin pats effects return_type, [] | Some ft -> - (* Debug.print ("t: " ^ Types.string_of_datatype ft); *) (* make sure the annotation has the right shape *) let shape = make_ft lin pats effects return_type in let quantifiers, ft_mono = TypeUtils.split_quantified_type ft in @@ -4607,7 +4846,10 @@ and type_binding : context -> binding -> binding * context * Usage.t = let fold_in_envs = List.fold_left (fun env pat' -> env ++ (pattern_env pat')) in let context_body = List.fold_left fold_in_envs context_body pats in - let body = type_check (bind_effects context_body effects) body in + (* the effects are flattened and a new cont_lin is generated before type checking the body *) + let new_body_context = {context_body with effect_row = Types.flatten_row effects; + cont_lin = LinCont.getnew () } in + let body = type_check new_body_context body in (* check that the body type matches the return type of any annotation *) let () = unify pos ~handle:Gripers.bind_fun_return (no_pos (typ body), no_pos return_type) in @@ -4723,7 +4965,6 @@ and type_binding : context -> binding -> binding * context * Usage.t = List.map (WithPos.map ~f:Renamer.rename_recursive_functionnode) defs in let fresh_tame () = Types.make_empty_open_row default_effect_subkind in - (* let fresh_wild () = Types.make_singleton_open_row ("wild", (Present Types.unit_type)) (lin_any, res_any) in *) let inner_rec_vars, inner_env, patss = List.fold_left @@ -4818,7 +5059,9 @@ and type_binding : context -> binding -> binding * context * Usage.t = in let body_context = {context with var_env = Env.extend body_env self_env} in let effects = fresh_tame () in - let body = type_check (bind_effects body_context effects) body in + let new_body_context = {body_context with effect_row = effects; + cont_lin = LinCont.getnew () } in + let body = type_check new_body_context body in let () = Env.iter (fun v t -> @@ -5005,14 +5248,15 @@ and type_regex typing_env : regex -> regex = in Splice (erase e) | Replace (r, Literal s) -> Replace (tr r, Literal s) | Replace (r, SpliceExpr e) -> Replace (tr r, SpliceExpr (erase (type_check typing_env e))) -and type_bindings (globals : context) bindings = +and type_bindings (globals : context) bindings = let tyenv, (bindings, uinf) = List.fold_left (fun (ctxt, (bindings, uinf)) (binding : binding) -> - let binding, ctxt', usage = type_binding (Types.extend_typing_environment globals ctxt) binding in + let cur_ctxt = (Types.extend_typing_environment globals ctxt) in + let binding, ctxt', usage = type_binding cur_ctxt binding in let result_ctxt = Types.extend_typing_environment ctxt ctxt' in result_ctxt, (binding::bindings, (binding.pos,ctxt'.var_env,usage)::uinf)) - (empty_context globals.effect_row globals.desugared, ([], [])) bindings in + (empty_context globals.cont_lin globals.effect_row globals.desugared, ([], [])) bindings in (* usage_builder checks the usage of variables from the bindings *) let usage_builder body_usage = List.fold_left @@ -5214,7 +5458,9 @@ struct match body with | None -> (bindings, None), Types.unit_type, tyenv' | Some body -> - let body, typ = type_check_general (Types.extend_typing_environment tyenv tyenv') body in + let context = (Types.extend_typing_environment tyenv tyenv') in + (* create a new cont_lin before typing the body *) + let body, typ = type_check_general {context with cont_lin = LinCont.getnew ()} body in let typ = Types.normalise_datatype typ in (bindings, Some body), typ, tyenv' in Debug.if_set show_post_sugar_typing diff --git a/core/typeUtils.ml b/core/typeUtils.ml index 91a31477d..a7c8d69e5 100644 --- a/core/typeUtils.ml +++ b/core/typeUtils.ml @@ -126,7 +126,7 @@ let rec return_type ?(overstep_quantifiers=true) t = match (concrete_type t, ove | (ForAll (_, t), true) -> return_type t | (Function (_, _, t), _) -> t | (Lolli (_, _, t), _) -> t - | (Operation (_, t), _) -> t + | (Operation (_, t, _), _) -> t | (t, _) -> error ("Attempt to take return type of non-function: " ^ string_of_datatype t) @@ -359,7 +359,7 @@ let check_type_wellformedness primary_kind t : unit = | Effect row -> irow row; pk_row - | Operation (f, t) -> + | Operation (f, t, _) -> idatatype f; idatatype t; pk_type (* Presence *) diff --git a/core/types.ml b/core/types.ml index 5011f2324..6449adac9 100644 --- a/core/types.ml +++ b/core/types.ml @@ -9,6 +9,9 @@ let internal_error message = let tag_expectation_mismatch = internal_error "Type tag expectation mismatch" + +let lincont_enabled = Settings.get Basicsettings.CTLinearity.enabled + module FieldEnv = Utility.StringMap type 'a stringmap = 'a Utility.stringmap [@@deriving show] type 'a field_env = 'a stringmap [@@deriving show] @@ -153,7 +156,7 @@ and typ = | ForAll of (Quantifier.t list * typ) (* Effect *) | Effect of row - | Operation of (typ * typ) + | Operation of (typ * typ * DeclaredLinearity.t) (* Row *) | Row of (field_spec_map * row_var * bool) | Closed @@ -384,10 +387,11 @@ struct | Effect row -> let (o, row') = o#row row in (o, Effect row') - | Operation (dom, cod) -> + | Operation (dom, cod, lin) -> let (o, dom') = o#typ dom in let (o, cod') = o#typ cod in - (o, Operation(dom', cod')) + (* let (o, lin') = o#bool lin in *) + (o, Operation(dom', cod', lin)) (* Row *) | Row (fsp, rv, d) -> let (o, fsp') = o#field_spec_map fsp in @@ -599,7 +603,7 @@ class virtual type_predicate = object(self) | Absent -> true | Present t -> self#type_satisfies vars t | Select r | Choice r -> self#row_satisfies vars r - | Input (a, b) | Output (a, b) | Operation (a, b) -> self#type_satisfies vars a && self#type_satisfies vars b + | Input (a, b) | Output (a, b) | Operation (a, b, _) -> self#type_satisfies vars a && self#type_satisfies vars b | Dual s -> self#type_satisfies vars s | End -> true @@ -662,7 +666,7 @@ class virtual type_iter = object(self) self#visit_type (rec_appl, rec_vars, TypeVarSet.add_quantifiers qs quant_vars) t (* Effect *) | Effect r -> self#visit_row vars r - | Operation (a, b) -> self#visit_type vars a; self#visit_type vars b + | Operation (a, b, _) -> self#visit_type vars a; self#visit_type vars b (* Row *) | Row (fields, row_var, _dual) -> self#visit_point self#visit_row vars row_var; @@ -810,7 +814,9 @@ module Unl : Constraint = struct | ForAll _ as t -> super#type_satisfies vars t (* Effect *) | Effect _ -> true - | Operation _ -> true + | Operation (_,_,b) -> + if lincont_enabled then DeclaredLinearity.(if b = Lin then true else false) + else true (* Row *) | Row _ as t -> super#type_satisfies vars t (* Presence *) @@ -818,6 +824,9 @@ module Unl : Constraint = struct | Present t -> o#type_satisfies vars t (* Session *) | Input _ | Output _ | Select _ | Choice _ | Dual _ | End -> false + + (* method! row_satisfies var = fun *) + (* | _ -> false *) end let type_satisfies, row_satisfies = @@ -1170,7 +1179,7 @@ let free_type_vars, free_row_type_vars, free_tyarg_vars = | Lolli (f, m, t) -> S.union_all [free_type_vars' rec_vars f; free_row_type_vars' rec_vars m; free_type_vars' rec_vars t] | Effect row | Record row | Variant row -> free_row_type_vars' rec_vars row - | Operation (f, t) -> + | Operation (f, t, _) -> S.union_all [free_type_vars' rec_vars f; free_type_vars' rec_vars t] | Table (_, r, w, n) -> S.union_all @@ -1369,7 +1378,7 @@ and subst_dual_type : var_map -> datatype -> datatype = | Record row -> Record (sdr row) | Variant row -> Variant (sdr row) | Effect row -> Effect (sdr row) - | Operation (f, t) -> Operation (sdt f, sdt t) + | Operation (f, t, b) -> Operation (sdt f, sdt t, b) | Table (t, r, w, n) -> Table (t, sdt r, sdt w, sdt n) | Lens _sort -> t (* TODO: we could do a check to see if we can preserve aliases here *) @@ -1575,7 +1584,7 @@ and normalise_datatype rec_names t = | Record row -> Record (nr row) | Variant row -> Variant (nr row) | Effect row -> Effect (nr row) - | Operation (f, t) -> Operation (nt f, nt t) + | Operation (f, t, b) -> Operation (nt f, nt t, b) | Table (t, r, w, n) -> Table (t, nt r, nt w, nt n) | Lens sort -> Lens sort | Alias (k, (name, qs, ts, is_dual), datatype) -> @@ -1883,7 +1892,7 @@ struct (List.rev vars) @ (free_bound_type_vars bound_vars body) (* Effect *) | Effect row -> free_bound_row_type_vars bound_vars row - | Operation (f, t) -> + | Operation (f, t, _) -> (fbtv f) @ (fbtv t) (* Row *) | Row (field_env, row_var, _) -> @@ -2649,7 +2658,7 @@ struct "forall "^ mapstrcat "," (quantifier p) tyvars ^"."^ datatype { context with bound_vars } p body (* Effect *) | Effect r -> "{" ^ row "," context p r ^ "}" - | Operation (f, t) -> sd f ^ " => " ^ sd t + | Operation (f, t, b) -> sd f ^ (if b=DeclaredLinearity.Lin then " =@ " else " => ") ^ sd t (* Row *) | Row _ as t -> "{" ^ row "," context p t ^ "}" (* Presence *) @@ -2785,7 +2794,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct | Variant | Effect | Row - | RowVar of [`Variant | `NonVariant] + | RowVar of [`Variant | `NonVariant | `Effect] | Binder | Type_arg [@@deriving show] @@ -2887,6 +2896,10 @@ module RoundtripPrinter : PRETTY_PRINTER = struct = fun { ambient ; _ } -> match ambient with | RowVar _ -> true | _ -> false + + let is_ambient_effvar : t -> bool + = fun { ambient ; _ } -> ambient = RowVar `Effect + let is_ambient_variant_rowvar : t -> bool = fun { ambient ; _ } -> match ambient with | RowVar `Variant -> true @@ -3124,11 +3137,15 @@ module RoundtripPrinter : PRETTY_PRINTER = struct method effect_row : row -> 'self_type * row_erasability * tid option = let maybe_contract : typ -> typ = function - | Operation (d,c) as tp when ES.contract_operation_arrows policy -> + | Operation (d,c,_) as tp when ES.contract_operation_arrows policy -> (* we are in an operation fieldspec and it's an arrow, and we want contractions: check if a contraction is possible here *) if d = unit_type then c else tp + (* FIXME: WT: I dont understand where this is + used. However, it seems dangerous that the + syntactic sugar discards the linearity + information. *) | tp -> tp in let decide_field : tid -> string -> field_spec -> 'self_type * field_spec_map -> 'self_type * field_spec_map @@ -3436,15 +3453,18 @@ module RoundtripPrinter : PRETTY_PRINTER = struct type 'a printer = 'a Printer.t + (* For correct printing of subkinds, need to know the subkind in advance: * see line (1): that has to be Empty so that the :: is not printed *) - let subkind_name : Policy.t -> Subkind.t -> unit printer - = fun policy (lin, res) -> + let subkind_name : ?is_eff:bool -> Policy.t -> Subkind.t -> unit printer + = fun ?(is_eff=false) policy (lin, res) -> let open Printer in let full_name : unit printer - = Printer (fun _ctx () buf -> + = let linname = + Linearity.to_string ~is_eff:is_eff lin + in Printer (fun _ctx () buf -> StringBuffer.write buf "("; - StringBuffer.write buf (Linearity.to_string lin); + StringBuffer.write buf linname; StringBuffer.write buf ","; StringBuffer.write buf (Restriction.to_string res); StringBuffer.write buf ")" @@ -3457,11 +3477,11 @@ module RoundtripPrinter : PRETTY_PRINTER = struct let module L = Linearity in let module R = Restriction in match (lin, res) with - | (L.Unl, R.Any) -> Empty (* (1) see above *) - | (L.Any, R.Any) -> constant "Any" + | (L.Unl, R.Any) -> if is_eff && lincont_enabled then constant "Lin" else Empty (* (1) see above *) + | (L.Any, R.Any) -> if is_eff && lincont_enabled then Empty else constant "Any" | (L.Unl, R.Base) -> constant @@ R.to_string res_base | (L.Any, R.Session) -> constant @@ R.to_string res_session - | (L.Unl, R.Effect) -> constant @@ R.to_string res_effect + | (L.Unl, R.Effect) -> constant @@ R.to_string res_effect (* control-flow-linearity may also need changing this *) | _ -> full_name @@ -3473,10 +3493,16 @@ module RoundtripPrinter : PRETTY_PRINTER = struct fun ctx ((primary, subknd) as knd) -> + let is_row = Kind.primary_kind knd = PrimaryKind.Row + || Context.is_ambient_rowvar ctx in + let is_presence = primary = PrimaryKind.Presence in + let is_eff = Context.is_ambient_effvar ctx + || (Context.is_ambient_effect ctx && (is_presence || is_row)) in + (* let in_binder = Context.is_ambient_binder ctx in *) let full_name : unit printer = Printer (fun ctxt () buf -> StringBuffer.write buf (P.to_string primary); - Printer.apply (subkind_name (Context.policy ctxt) subknd) ctxt () buf) + Printer.apply (subkind_name ~is_eff:is_eff (Context.policy ctxt) subknd) ctxt () buf) in let policy = Context.policy ctx in match Policy.kinds policy, knd with @@ -3499,7 +3525,15 @@ module RoundtripPrinter : PRETTY_PRINTER = struct | PrimaryKind.Row -> begin match subknd with | L.Unl, R.Any | L.Unl, R.Effect -> - StringBuffer.write buf (P.to_string pk_row) + if is_eff && lincont_enabled then StringBuffer.write buf (P.to_string pk_row ^ "(Lin)") + else StringBuffer.write buf (P.to_string pk_row) + | L.Any, R.Any | L.Any, R.Effect -> + (* NOTE: The first branch might not be entirely compatible with value rows. *) + if not lincont_enabled then StringBuffer.write buf (P.to_string pk_row) + else if is_eff then StringBuffer.write buf (P.to_string pk_row) + else + let ctx' = Context.(with_policy Policy.(set_kinds Full (policy ctx)) ctx) in + Printer.apply full_name ctx' () buf | _ -> let ctx' = Context.(with_policy Policy.(set_kinds Full (policy ctx)) ctx) in Printer.apply full_name ctx' () buf @@ -3508,6 +3542,11 @@ module RoundtripPrinter : PRETTY_PRINTER = struct match subknd with | L.Unl, R.Any -> StringBuffer.write buf (P.to_string pk_presence) + | L.Any, R.Effect -> + StringBuffer.write buf (P.to_string pk_row) + | L.Unl, R.Effect -> + (* explicit kinds for linear presence variables *) + StringBuffer.write buf (P.to_string pk_presence ^ "(Lin)") | _ -> let ctx' = Context.(with_policy Policy.(set_kinds Full (policy ctx)) ctx) in Printer.apply full_name ctx' () buf @@ -3553,13 +3592,13 @@ module RoundtripPrinter : PRETTY_PRINTER = struct * (or "{% ... }" if Flexible, but the % will be contributed by rule (3)) [is_presence] *) + let is_presence = (PrimaryKind.Presence = Kind.primary_kind knd) in + (if is_presence && not (Context.is_ambient_type_arg ctx) then StringBuffer.write buf "{"); let print_var : string printer = Printer (fun ctx var_name buf -> let anonymity = get_var_anonymity ctx vid in let show_flexible = (Policy.flavours Context.(policy ctx)) && flavour = `Flexible in - let is_presence = (PrimaryKind.Presence = Kind.primary_kind knd) in - (if is_presence && not (Context.is_ambient_type_arg ctx) then StringBuffer.write buf "{"); (if show_flexible then StringBuffer.write buf "%"); (match anonymity, show_flexible with | Anonymous, true -> () @@ -3568,12 +3607,18 @@ module RoundtripPrinter : PRETTY_PRINTER = struct if Policy.(EffectSugar.arrows_show_implicit (es_policy (Context.policy ctx))) then StringBuffer.write buf var_name else StringBuffer.write buf "_" - | _, _ -> StringBuffer.write buf var_name); - (if is_presence && not (Context.is_ambient_type_arg ctx) then StringBuffer.write buf "}")) + | _, _ -> StringBuffer.write buf var_name) + ) in + let is_row = Kind.primary_kind knd = PrimaryKind.Row + || Context.is_ambient_rowvar ctx in + let is_eff = Context.is_ambient_effvar ctx + || (Context.is_ambient_effect ctx && (is_presence || is_row)) in if not in_binder - then seq ~sep:"::" (print_var, subkind_name (Context.policy ctx) subknd) (var_name, ()) ctx buf - else seq ~sep:"::" (print_var, kind_name ctx knd) (var_name, ()) ctx buf) + then seq ~sep:"::" (print_var, subkind_name ~is_eff:is_eff (Context.policy ctx) subknd) (var_name, ()) ctx buf + else seq ~sep:"::" (print_var, kind_name ctx knd) (var_name, ()) ctx buf; + (if is_presence && not (Context.is_ambient_type_arg ctx) then StringBuffer.write buf "}") + ) and recursive : (tid * Kind.t * typ) printer = let open Printer in @@ -3666,6 +3711,8 @@ module RoundtripPrinter : PRETTY_PRINTER = struct else StringBuffer.write buf "|"; let ctx = Context.set_ambient (if Context.is_ambient_variant ctx then Context.RowVar `Variant + else if Context.is_ambient_effect ctx + then Context.RowVar `Effect else Context.RowVar `NonVariant) ctx in (if rdual then StringBuffer.write buf "~"); @@ -3812,8 +3859,10 @@ module RoundtripPrinter : PRETTY_PRINTER = struct | None | Some Absent | Some (Meta _) -> false | _ -> raise tag_expectation_mismatch in - let decide_skip ctx vid = + let decide_skip ctx vid subknd = let anonymity = get_var_anonymity ctx vid in + (* linear row variables should not be skipped *) + let is_linrow = if lincont_enabled then fst subknd = Linearity.Unl else false in if Context.implicit_shared_effect_exists ctx then begin let es_policy = Policy.es_policy (Context.policy ctx) in @@ -3824,12 +3873,13 @@ module RoundtripPrinter : PRETTY_PRINTER = struct match anonymity with | Visible -> false (* decided Visible, cannot skip *) - | Anonymous -> arrows_show_impl_shared || - (arrows_curried_hide_fresh && Context.is_ambient_arrow_curried ctx) - | ImplicitEffectVar -> not arrows_show_impl_shared + | Anonymous -> (arrows_show_impl_shared || + (arrows_curried_hide_fresh && Context.is_ambient_arrow_curried ctx)) && + not is_linrow + | ImplicitEffectVar -> not arrows_show_impl_shared && not is_linrow end else match anonymity with - | Anonymous -> true (* skip *) + | Anonymous -> not is_linrow (* skip *) | Visible -> false (* no skip *) | _ -> raise (internal_error "ImplicitEffectVar anonymity is not allowed when effect sugar is disabled") @@ -3846,10 +3896,8 @@ module RoundtripPrinter : PRETTY_PRINTER = struct | Empty -> false | _ -> true in - if visible_fields = 0 + if visible_fields = 0 && not row_var_exists then begin - if not row_var_exists - then begin let effect_sugar = Policy.effect_sugar (Context.policy ctx) in let es_policy = Policy.es_policy (Context.policy ctx) in if not ((Context.is_ambient_operation ctx) @@ -3864,36 +3912,44 @@ module RoundtripPrinter : PRETTY_PRINTER = struct StringBuffer.write buf "{ | .}" else StringBuffer.write buf "{}" - end - end - else (* empty open row use the abbreviated notation -a- or ~a~ unless - it's anonymous in which case we skip it entirely *) + end + end + else begin match Unionfind.find rvar with | Var (vid, knd, _) -> - if decide_skip ctx vid - then () (* skip printing it entirely *) - else begin - (if is_wild + let subknd = Kind.subkind knd in + let is_linrow = if lincont_enabled then fst subknd = Linearity.Unl else false in + (* empty unlimited open row use the abbreviated notation -a- or ~a~ unless + it's anonymous in which case we skip it entirely *) + if visible_fields = 0 && not is_linrow + then begin + if decide_skip ctx vid subknd + then () (* skip printing it entirely *) + else + begin + (if is_wild then StringBuffer.write buf "~" else StringBuffer.write buf "-"); - let ctx = - Context.(set_ambient Effect - (with_policy Policy.(set_kinds Hide (policy ctx)) ctx)) - in - Printer.apply var ctx (vid, knd) buf - end + let ctx = + Context.(set_ambient Effect + (with_policy Policy.(set_kinds Default (policy ctx)) ctx)) + in + Printer.apply var ctx (vid, knd) buf; + end + end + else begin + (* need the full effect row, but only construct the inside of it *) + StringBuffer.write buf "{"; + Printer.apply row_parts (Context.set_ambient Context.Effect ctx) r' buf; + StringBuffer.write buf "}"; + end | _ -> begin (* special case, construct row syntax, but only call the inside *) StringBuffer.write buf "{"; Printer.apply row_parts (Context.set_ambient Context.Effect ctx) r' buf; StringBuffer.write buf "}" end - end - else begin (* need the full effect row, but only construct the inside of it *) - StringBuffer.write buf "{"; - Printer.apply row_parts (Context.set_ambient Context.Effect ctx) r' buf; - StringBuffer.write buf "}"; - end; + end; (if is_wild then StringBuffer.write buf "~" else StringBuffer.write buf "-"); (* add the arrowhead/lollipop/oparrow *) (if is_lolli then StringBuffer.write buf "@" @@ -3924,12 +3980,12 @@ module RoundtripPrinter : PRETTY_PRINTER = struct Printer.apply datatype ctx range buf; ) - and op : (typ * typ) printer + and op : (typ * typ * DeclaredLinearity.t) printer = let open Printer in - Printer (fun ctx (domain, range) buf -> + Printer (fun ctx (domain, range, lin) buf -> (* build up the function type string: domain, arrow with effects, range *) Printer.apply row (Context.set_ambient Context.Tuple ctx) domain buf; (* function domain is always a Record *) - StringBuffer.write buf " => "; + StringBuffer.write buf (if lin=DeclaredLinearity.Lin then " =@ " else " => "); Printer.apply datatype ctx range buf; ) @@ -4226,6 +4282,7 @@ type typing_environment = { var_env : environment ; rec_vars : StringSet.t ; tycon_env : tycon_environment ; effect_row : row; + cont_lin : int; desugared : bool } [@@deriving show] @@ -4233,6 +4290,7 @@ let empty_typing_environment = { var_env = Env.empty; rec_vars = StringSet.empty; tycon_env = Env.empty; effect_row = make_empty_closed_row (); + cont_lin = -1; desugared = false } (* Which printer to use *) @@ -4358,12 +4416,13 @@ let normalise_typing_environment env = (* Functions on environments *) let extend_typing_environment - {var_env = l; rec_vars = lvars; tycon_env = al; effect_row = _; desugared = _; } - {var_env = r; rec_vars = rvars; tycon_env = ar; effect_row = er; desugared = dr } : typing_environment = + {var_env = l; rec_vars = lvars; tycon_env = al; effect_row = _; cont_lin = _; desugared = _; } + {var_env = r; rec_vars = rvars; tycon_env = ar; effect_row = er; cont_lin = xl; desugared = dr } : typing_environment = { var_env = Env.extend l r ; rec_vars = StringSet.union lvars rvars ; tycon_env = Env.extend al ar ; effect_row = er + ; cont_lin = xl ; desugared = dr } let string_of_environment env = show_environment (Env.map DecycleTypes.datatype env) @@ -4388,7 +4447,7 @@ let make_fresh_envs : datatype -> datatype IntMap.t * row IntMap.t * field_spec | Function (f, m, t) -> union [make_env boundvars f; make_env boundvars m; make_env boundvars t] | Lolli (f, m, t) -> union [make_env boundvars f; make_env boundvars m; make_env boundvars t] | Effect row | Record row | Variant row -> make_env boundvars row - | Operation (f, t) -> union [make_env boundvars f; make_env boundvars t] + | Operation (f, t, _) -> union [make_env boundvars f; make_env boundvars t] | Table (_, r, w, n) -> union [make_env boundvars r; make_env boundvars w; make_env boundvars n] | Lens _ -> empties | Alias (_, (_, _, ts, _), d) -> union (List.map (make_env_ta boundvars) ts @ [make_env boundvars d]) @@ -4696,12 +4755,8 @@ let make_function_type : ?linear:bool -> datatype list -> row -> datatype -> dat else Function (make_tuple_type args, effs, range) -let make_operation_type : datatype list -> datatype -> datatype - = fun args range -> - Operation (make_tuple_type args, range) - -let make_pure_function_type : datatype list -> datatype -> datatype - = fun domain range -> make_function_type domain (make_empty_closed_row ()) range +let make_pure_function_type : ?linear:bool -> datatype list -> datatype -> datatype + = fun ?(linear=false) domain range -> make_function_type ~linear domain (make_empty_closed_row ()) range let make_thunk_type : row -> datatype -> datatype = fun effs rtype -> diff --git a/core/types.mli b/core/types.mli index e308a6d5a..88c0fa19a 100644 --- a/core/types.mli +++ b/core/types.mli @@ -144,7 +144,7 @@ and typ = | ForAll of (Quantifier.t list * typ) (* Effect *) | Effect of row - | Operation of (typ * typ) + | Operation of (typ * typ * DeclaredLinearity.t) (* Row *) | Row of (field_spec_map * row_var * bool) | Closed @@ -221,7 +221,8 @@ type typing_environment = { var_env : environment ; rec_vars : Utility.StringSet.t ; tycon_env : tycon_environment ; effect_row : row ; - desugared : bool } + cont_lin : int ; + desugared : bool } val empty_typing_environment : typing_environment @@ -428,9 +429,8 @@ val add_tyvar_names : ('a -> Vars.vars_list) -> ('a list) -> unit (* Function type constructors *) -val make_pure_function_type : datatype list -> datatype -> datatype +val make_pure_function_type : ?linear:bool -> datatype list -> datatype -> datatype val make_function_type : ?linear:bool -> datatype list -> row -> datatype -> datatype -val make_operation_type : datatype list -> datatype -> datatype val make_thunk_type : row -> datatype -> datatype diff --git a/core/typevarcheck.ml b/core/typevarcheck.ml index cc4b35e54..ef4aec4d2 100644 --- a/core/typevarcheck.ml +++ b/core/typevarcheck.ml @@ -87,7 +87,7 @@ let rec is_guarded : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool = expanded_apps var t (* Effect *) | Effect row -> isgr row - | Operation (f, t) -> + | Operation (f, t, _) -> isg f && isg t (* Row *) | Row (fields, row_var, _dual) -> @@ -176,7 +176,7 @@ let rec is_negative : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool = expanded_apps var t (* Effect *) | Effect row -> isnr row - | Operation (f, t) -> + | Operation (f, t, _) -> isp f || isn t (* Row *) | Row (field_env, row_var, _dual) -> @@ -265,7 +265,7 @@ and is_positive : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool = expanded_apps var t (* Effect *) | Effect row -> ispr row - | Operation (f, t) -> + | Operation (f, t, _) -> isn f || isp t (* Row *) | Row (field_env, row_var, _dual) -> diff --git a/core/unify.ml b/core/unify.ml index c92c59848..4f234f6ff 100644 --- a/core/unify.ml +++ b/core/unify.ml @@ -160,11 +160,12 @@ let rec eq_types : (datatype * datatype) -> bool = | Effect r -> eq_rows (l, r) | _ -> false end - | Operation (lfrom, lto) -> + | Operation (lfrom, lto, llin) -> begin match unalias t2 with - | Operation (rfrom, rto) -> eq_types (lfrom, rfrom) - && eq_types (lto, rto) - | _ -> false + | Operation (rfrom, rto, rlin) -> eq_types (lfrom, rfrom) + && eq_types (lto, rto) + && llin = rlin + | _ -> false end (* Row *) | Row (lfield_env, lrow_var, ldual) -> @@ -687,9 +688,14 @@ let rec unify' : unify_env -> (datatype * datatype) -> unit = | (Present _ | Absent), (Present _ | Absent) -> unify_presence' rec_env (t1, t2) (* Effect *) | Effect (Row l), Effect (Row r) -> ur (l, r) - | Operation (lfrom, lto), Operation (rfrom, rto) -> + | Operation (lfrom, lto, llin), Operation (rfrom, rto, rlin) -> (ut (lfrom, rfrom); - ut (lto, rto)) + ut (lto, rto); + if llin = rlin then () else + raise (Failure + (`Msg ("Cannot unify two operations with different linearity '" ^ + string_of_datatype (Operation (lfrom, lto, llin)) ^ "' and '"^ + string_of_datatype (Operation (rfrom, rto, rlin)) ^"'")))) (* Session *) | Input (t, s), Input (t', s') | Output (t, s), Output (t', s') -> unify' rec_env (t, t'); ut (s, s') diff --git a/examples/handlers/pipes.links b/examples/handlers/pipes.links index 0127a26ed..b7af7e14d 100644 --- a/examples/handlers/pipes.links +++ b/examples/handlers/pipes.links @@ -71,11 +71,11 @@ module Deep { typename Consumer(e::Eff, s, a) = (s) ~e~> (Producer({ |e}, s, a)) ~e~> a; } - typename Pipe(e::Eff, s, a) = forall b::Presence, c::Presence. + typename Pipe(e::Eff, s, a) = forall b::Presence(Any), c::Presence(Any). (Comp({ Await: s, Yield{c} |e}, a)) { Await{b}, Yield{c} |e}~> (Producer({ Await{b}, Yield{c} |e}, s, a)) { Await{b}, Yield{c} |e}~> a; - typename Copipe(e::Eff, s, a) = forall b::Presence, c::Presence. + typename Copipe(e::Eff, s, a) = forall b::Presence(Any), c::Presence(Any). (Comp({ Await{b}, Yield: (s) => () |e}, a)) { Await{b}, Yield{c} |e}~> (Consumer({ Await{b}, Yield{c} |e}, s, a)) { Await{b}, Yield{c} |e}~> a; diff --git a/prelude.links b/prelude.links index f21f8ac36..de52f6234 100644 --- a/prelude.links +++ b/prelude.links @@ -1228,8 +1228,11 @@ fun sendSuspend(pagef) { typename Pid(a::Type) = Process({hear: a}); #### SESSION TYPING STUFF #### +# The SessionFail is defined to be a control-flow-linear operation. +# The effect row variable `e` can have kind `Row(Any)` because no linear +# resources is used in this function. #sig fork : forall s::Session,e::Row.((s) ~e~> ()) ~e~> ~s -sig fork : forall s::Session,e::Row.((s) {SessionFail:[||]}~> ()) ~e~> ~s +sig fork : forall s::Session,e::Row(Any).((s) {SessionFail:() =@ [||]}~> ()) ~e~> ~s fun fork(f) { var ap = new (); var _ = spawnAngel { @@ -1239,8 +1242,9 @@ fun fork(f) { } #sig linFork : forall s::Session,e::Row.((s) ~e~@ ()) ~e~> ~s -sig linFork : forall s::Session,e::Row.((s) {SessionFail:[||]}~@ ()) ~e~> ~s +sig linFork : forall s::Session,e::Row.((s) {SessionFail:() =@ [||]}~@ ()) ~e~> ~s fun linFork(f) { + xlin; var ap = new(); var _ = spawnAngel { f(accept(ap)) @@ -1249,8 +1253,9 @@ fun linFork(f) { } #sig reproduce : forall s::Session,e::Row.(AP(s), (s) ~e~> ()) ~e~> () -sig reproduce : forall s::Session,e::Row.(AP(s), (s) {SessionFail:[||]}~> ()) ~e~> () +sig reproduce : forall s::Session,e::Row.(AP(s), (s) {SessionFail:() =@ [||]}~> ()) ~e~> () fun reproduce(ap, f) { + xlin; var x = accept(ap); var _ = spawn {f(x)}; reproduce(ap, f) @@ -1266,8 +1271,9 @@ fun reproduce(ap, f) { # run even if the main process terminates.) #sig connect : forall s::Session,e::Row,a.((s) ~e~> (), (~s) ~e~> a) ~e~> a -sig connect : forall s::Session,e::Row,a.((s) {SessionFail:[||]}~> (), (~s) ~e~> a) ~e~> a +sig connect : forall s::Session,e::Row,a.((s) {SessionFail:() =@ [||]}~> (), (~s) ~e~> a) ~e~> a fun connect(f, g) { + xlin; var ap = new(); var done = new(); var _ = spawn { @@ -1284,19 +1290,22 @@ fun connect(f, g) { typename EndBang = !().End; typename EndQuery = ?().End; -sig wait : (EndQuery) ~> () +sig wait : forall e::Row . (EndQuery) { |e}~> () fun wait(s) { + xlin; var (_, s) = receive(s); close(s) } -sig closeBang : (EndBang) ~> () +sig closeBang : forall e::Row . (EndBang) { |e}~> () fun closeBang(s) { + xlin; close(send((), s)) } -sig makeEndBang : () ~> EndBang +sig makeEndBang : forall e::Row . () { |e}~> EndBang fun makeEndBang() { + xlin; var ap = new(); var _ = spawn { var c = accept(ap); @@ -1308,8 +1317,9 @@ fun makeEndBang() { # with split ends we synchronise on the termination of each spawned # child process #sig forkSync : forall s::Session,e::Row.((s) ~e~> EndBang) ~e~> ~s -sig forkSync : forall s::Session,e::Row.((s) {SessionFail:[||]}~> EndBang) ~e~> ~s +sig forkSync : forall s::Session,e::Row.((s) {SessionFail:() =@ [||]}~> EndBang) ~e~> ~s fun forkSync(f) { + xlin; var ap = new(); var _ = spawn { var c = accept(ap); @@ -1320,8 +1330,9 @@ fun forkSync(f) { } #sig linForkSync : forall s::Session,e::Row.((s) ~e~@ EndBang) ~e~> ~s -sig linForkSync : forall s::Session,e::Row.((s) {SessionFail:[||]}~@ EndBang) ~e~> ~s +sig linForkSync : forall s::Session,e::Row.((s) {SessionFail:() =@ [||]}~@ EndBang) ~e~> ~s fun linForkSync(f) { + xlin; var ap = new(); var _ = spawn { var c = accept(ap); @@ -1332,15 +1343,17 @@ fun linForkSync(f) { } #sig linkSync : forall s::Session,e::Row.(s, ~s) ~e~> EndBang -sig linkSync : forall s::Session,e::Row.(s, ~s) {SessionFail:[||] | e}~> EndBang +sig linkSync : forall s::Session,e::Row.(s, ~s) {SessionFail:() =@ [||] | e}~> EndBang fun linkSync(s, c) { + xlin; link(s, c); makeEndBang() } #sig runSync : ((!a.EndBang) ~e~> EndBang) ~e~> a -sig runSync : ((!a.EndBang) {SessionFail:[||]}~> EndBang) ~e~> a +sig runSync : forall a, e::Row . ((!a.EndBang) {SessionFail:() =@ [||]}~> EndBang) { |e}~> a fun runSync(f) { + xlin; var c = forkSync(f); var (v, c) = receive(c); wait(c); diff --git a/tests/control_flow_linearity.config b/tests/control_flow_linearity.config new file mode 100644 index 000000000..cd4799c98 --- /dev/null +++ b/tests/control_flow_linearity.config @@ -0,0 +1,2 @@ +enable_handlers=true +track_control_flow_linearity=true \ No newline at end of file diff --git a/tests/control_flow_linearity.tests b/tests/control_flow_linearity.tests new file mode 100644 index 000000000..5aea2354c --- /dev/null +++ b/tests/control_flow_linearity.tests @@ -0,0 +1,316 @@ +--- +config: tests/control_flow_linearity.config +--- + +# Usage of control-flow-linear/unlimited operations and linear resources + +Using linear variables in linear continuations (1) +fun(){xlin; var lf = linfun(x) {x}; lf(42)} +stdout : fun : () { |_::Lin}-> Int + +Using linear variables in linear continuations (2) +{ xlin; var lf = linfun(x) {x}; linfun(){xlin; lf(1)} } +stdout : fun : () { |_::Lin}-@ Int + +Using linear variables in unlimited continuations (1) +fun() {var lf = linfun(x) {x}; lf(1)} +exit : 1 +stderr : @.*Type error: Variable .* of linear type .* is used in a non-linear continuation.* + +Using linear variables in unlimited continuations (2) +{ xlin; var lf = linfun(x) {x}; linfun(){lf(1)} } +exit : 1 +stderr : @.*Type error: Variable .* of linear type .* is used in a non-linear continuation.* + +Using control-flow-linear operations in unlimited continuations +fun() {lindo Foo} +stdout : fun : () {Foo:() =@ a|_}-> a + +Using control-flow-linear operations in linear continuations +fun() {xlin; lindo Foo} +stdout : fun : () {Foo:() =@ a|_::Lin}-> a + +Using control-flow-linear operations and linear variables in linear continuations +fun(ch:End) {xlin; lindo L; close(ch)} +stdout : fun : (End) {L:() =@ ()|_::Lin}~> () + +Using control-flow-unlimited operations in unlimited continuations +fun() {do Foo} +stdout : fun : () {Foo:() => a|_}-> a + +Using control-flow-unlimited operations in linear continuations +fun() {xlin; do Foo} +exit : 1 +stderr : @.*Type error.* + +Mixing control-flow-linear and -unlimited operations in unlimited continuations +fun() {do U; lindo L} +stdout : fun : () {L:() =@ a,U:() => ()|_}-> a + + +# Handling control-flow-linear/unlimited operations + +Handling control-flow-linear operations (1) +handle (lindo Foo(20) + 1) {case -> xlin; k(i)} +stdout : 21 : Int + +Handling control-flow-linear operations (2) +{linfun f(x) {40+x} handle ({xlin; f(lindo Foo)}) {case -> xlin; k(2)}} +stdout : 42 : Int + +Handling control-flow-linear operations (3) +handle (lindo Foo(20) + 1) {case k> -> xlin; k(i)} +exit : 1 +stderr : @.*Type error.* + +Handling control-flow-unlimited operations (1) +handle (do Foo(20) + 1) {case k> -> k(i) + k(i)} +stdout : 42 : Int + +Handling control-flow-unlimited operations (2) +{linfun f(x) {x} handle (f(do Foo)) {case k> -> k(1)}} +exit : 1 +stderr : @.*Type error: Variable .* of linear type .* is used in a non-linear continuation.* + +Handling control-flow-unlimited operations (3) +handle (do Foo(20) + 1) {case -> k(i) + k(i)} +exit : 1 +stderr : @.*Type error.* + +Handling control-flow-unlimited operations (4) +fun(ch:End) { xlin; close(ch); handle ({if (do Choose) 40 else 2}) {case r> -> r(true) + r(false)} } +stdout : fun : (End) {Choose{_::Lin}|_::Lin}~> Int + + +# Kind annotations and operation annotations + +CFL kinds of explicit quantifiers in type signatures (1) +sig f:forall e::Row(Any). () {Foo:() => Int|e}-> Int fun f() {do Foo} f +stdout : fun : () {Foo:() => Int|_}-> Int + +CFL kinds of explicit quantifiers in type signatures (2) +sig f:forall e::Row. () {Foo:() => Int|e}-> Int fun f() {do Foo} f +stdout : fun : () {Foo:() => Int|_::Lin}-> Int + +Operation annotation +fun(m) { xlin; handle(m()) { case : ((Int) =@ Int) -> xlin; k (x) } } +stdout : fun : (() {Foo:(Int) =@ Int|a::Lin}~> b::Any) {Foo{_::Lin}|a::Lin}~> b::Any + + +# Usage of linear resources in handlers + +Using linear variables in deep handlers (1) +tests/control_flow_linearity/lin_deep1.links +filemode : true +exit : 1 +stderr : @.*Type error: Variable .* of linear type .* is used in a deep handler.* + +Using linear variables in deep handlers (2) +tests/control_flow_linearity/lin_deep2.links +filemode : true +exit : 1 +stderr : @.*Type error: Variable .* of linear type .* is used in a deep handler.* + +Using linear variables in deep handlers (3) +tests/control_flow_linearity/lin_deep3.links +filemode : true +stdout : 84 : Int + +Using linear variables in shallow handlers (1) +tests/control_flow_linearity/lin_shallow1.links +filemode : true +stdout : fun : () {Foo:() =@ Int|_::Lin}~> Int + +Using linear variables in shallow handlers (2) +tests/control_flow_linearity/lin_shallow2.links +filemode : true +exit : 1 +stderr : @.*Type error: Variable .* has linear type .* is used 2 times.* + +Using linear variables in shallow handlers (3) +tests/control_flow_linearity/lin_shallow3.links +filemode : true +exit : 1 +stderr : @.*Type error: Use of variable .* of linear type .* in unlimited function binding.* + +Using linear variables in shallow handlers (4) +tests/control_flow_linearity/lin_shallow4.links +filemode : true +stdout : 84 : Int + +Using linear variables in shallow handlers (5) +tests/control_flow_linearity/lin_shallow5.links +filemode : true +stdout : 84 : Int + + +# Previous examples with control-flow linearity + +Linear choice and unlimited choice +tests/control_flow_linearity/choose.links +filemode : true +stdout : [10, 10, 18, 12, 20] : [Int] + +Combining unlimited choice and unlimited state +tests/control_flow_linearity/choose_and_state.links +filemode : true +stdout : [3, 4, 9, 10, 3, 3, 3, 3] : [Int] + +Combining linear choice and unlimited state +tests/control_flow_linearity/choose_and_state2.links +filemode : true +stdout : 3 : Int + +Checking the first part of Issue 544 +tests/control_flow_linearity/issue544a.links +filemode : true +exit : 1 +stderr : @.*Type error: Effect row type .* can not be made linear .* + +Checking the second part of Issue 544 +tests/control_flow_linearity/issue544b.links +filemode : true +exit : 1 +stderr : @.*Type error: Effect row type .* can not be made linear .* + + +# Examples in the paper + +The original introduction program +tests/control_flow_linearity/popl24/intro.links +filemode : true +exit : 1 +stderr : @.*Type error.* + +The fixed version of the original introduction program +tests/control_flow_linearity/popl24/intro_fixed.links +filemode : true +stdout : 42well-typed() : () + + +## Examples in Section 4 + +The `faithfulSend` with CFL off +fun faithfulSend(c) { linfun (s) { var c = send(s, c); close(c) } } faithfulSend +stdout : fun : (!(a::Any).End) -> (a::Any) ~@ () +args : --set=track_control_flow_linearity=false + +The `faithfulSend` with CFL on +fun faithfulSend(c) { xlin; linfun (s) { xlin; var c = send(s, c); close(c) } } faithfulSend +stdout : fun : (!(a::Any).End) { |_::Lin}-> (a::Any) { |_::Lin}~@ () + +The `dubiousSend` with CFL on +fun dubiousSend(c) {xlin; var c = send(if (lindo Choose) "A" else "B", c); close(c)} dubiousSend +stdout : fun : (!(String).End) {Choose:() =@ Bool|_::Lin}~> () + +Handling `dubiousSend` with a linear handler +fun dubiousSend(c) {xlin; var c = send(if (lindo Choose) "A" else "B", c); close(c)} fun(c) {handle ({xlin; dubiousSend(c)}) {case -> xlin; r(true)} } +stdout : fun : (!(String).End) {Choose{_::Lin}|_::Lin}~> () + + +## Examples in Section 2 + +S2.1 Channel version of `faithfulWrite` (with CFL off) +fun faithfulSend(c) { linfun (s) { var c = send(s, c); close(c) } } faithfulSend +stdout : fun : (!(a::Any).End) -> (a::Any) ~@ () +args : --set=track_control_flow_linearity=false + +S2.1 Channel version of `faithfulWrite` (with CFL on) +fun faithfulSend(c) { xlin; linfun (s) { xlin; var c = send(s, c); close(c) } } faithfulSend +stdout : fun : (!(a::Any).End) { |_::Lin}-> (a::Any) { |_::Lin}~@ () + +S2.1 Subkinding of value linearity (with CFL off) (1) +fun id(x) {x} id(42) +stdout : 42 : Int +args : --set=track_control_flow_linearity=false + +S2.1 Subkinding of value linearity (with CFL off) (2) +fun id(x) {x} id(linfun(){42}) +stdout : fun : () -@ Int +args : --set=track_control_flow_linearity=false + +S2.1 Subkinding of value linearity (with CFL on) (1) +fun id(x) {xlin; x} id(42) +stdout : 42 : Int + +S2.1 Subkinding of value linearity (with CFL on) (2) +fun id(x) {xlin; x} id(linfun(){42}) +stdout : fun : () -@ Int + +S2.2 Channel version of `dubiousWrite` (with CFL off) +fun dubiousSend(c) {var c = send(if (do Choose) "A" else "B", c); close(c)} dubiousSend +stdout : fun : (!(String).End) {Choose:() => Bool|_}~> () +args : --set=track_control_flow_linearity=false + +S2.2 Channel version of `dubiousWrite` (with CFL on) +fun dubiousSend(c) {xlin; var c = send(if (lindo Choose) "A" else "B", c); close(c)} dubiousSend +stdout : fun : (!(String).End) {Choose:() =@ Bool|_::Lin}~> () + +S2.2 Handling `dubiousWrite` with an unlimited handler +fun dubiousSend(c) {xlin; var c = send(if (lindo Choose) "A" else "B", c); close(c)} fun(c) {handle ({xlin; dubiousSend(c)}) {case -> xlin; r(true); r(false)} } +exit : 1 +stderr : @.*Type error: Variable .* has linear type .* is used 2 times.* + +S2.2 Handling `dubiousWrite` with a linear handler +fun dubiousSend(c) {xlin; var c = send(if (lindo Choose) "A" else "B", c); close(c)} fun(c) {handle ({xlin; dubiousSend(c)}) {case -> xlin; r(true)} } +stdout : fun : (!(String).End) {Choose{_::Lin}|_::Lin}~> () + +S2.2 Subkinding of control-flow linearity (1) +fun tossCoin(g) {var b = g(); if (b) "heads" else "tails"} fun(){ tossCoin(fun(){do Choose}) } +stdout : fun : () {Choose:() => Bool|_}-> String + +S2.2 Subkinding of control-flow linearity (2) +fun tossCoin(g) {var b = g(); if (b) "heads" else "tails"} fun(){ tossCoin(fun(){lindo Choose}) } +stdout : fun : () {Choose:() =@ Bool|_}-> String + +S2.2 Subkinding of control-flow linearity (3) +fun tossCoin(g) {var b = g(); if (b) "heads" else "tails"} fun(){ tossCoin(fun(){xlin; lindo Choose}) } +stdout : fun : () {Choose:() =@ Bool|_::Lin}-> String + +S2.3 Different types of verboseId (1) +fun verboseId(x) {do Print("id is called"); x} verboseId +stdout : fun : (a) {Print:(String) => ()|_}-> a + +S2.3 Different types of verboseId (2) +fun verboseId(x) {lindo Print("id is called"); x} verboseId +stdout : fun : (a) {Print:(String) =@ ()|_}-> a + +S2.3 Different types of verboseId (3) +sig verboseId: (a) {Print:(String) => ()|_::Lin}-> a fun verboseId(x) {do Print("id is called"); x} verboseId +stdout : fun : (a) {Print:(String) => ()|_::Lin}-> a + +S2.3 Different types of verboseId (4) +sig verboseId: (a) {Print:(String) =@ ()|_::Lin}-> a fun verboseId(x) {lindo Print("id is called"); x} verboseId +stdout : fun : (a) {Print:(String) =@ ()|_::Lin}-> a + +S2.3 Different types of verboseId (5) +fun verboseId(x) {xlin; lindo Print("id is called"); x} verboseId +stdout : fun : (a::Any) {Print:(String) =@ ()|_::Lin}-> a::Any + +S2.3 Different types of verboseId (6) +linfun verboseId(x) {do Print("id is called"); x} {xlin; verboseId} +stdout : fun : (a) {Print:(String) => ()|_}-@ a + +S2.3 Different types of verboseId (7) +linfun verboseId(x) {lindo Print("id is called"); x} {xlin; verboseId} +stdout : fun : (a) {Print:(String) =@ ()|_}-@ a + +S2.3 Different types of verboseId (8) +sig verboseId: (a) {Print:(String) => ()|_::Lin}-@ a linfun verboseId(x) {do Print("id is called"); x} {xlin; verboseId} +stdout : fun : (a) {Print:(String) => ()|_::Lin}-@ a + +S2.3 Different types of verboseId (9) +sig verboseId: (a) {Print:(String) =@ ()|_::Lin}-@ a linfun verboseId(x) {lindo Print("id is called"); x} {xlin; verboseId} +stdout : fun : (a) {Print:(String) =@ ()|_::Lin}-@ a + +S2.3 Different types of verboseId (10) +linfun verboseId(x) {xlin; lindo Print("id is called"); x} {xlin; verboseId} +stdout : fun : (a::Any) {Print:(String) =@ ()|_::Lin}-@ a::Any + +S2.4 Restriction of row-based effect types (1) +fun verboseClose(c:End) {xlin; var s = lindo Get; close(c); lindo Print(s)} verboseClose +stdout : fun : (End) {Get:() =@ a,Print:(a) =@ b|_::Lin}~> b + +S2.4 Restriction of row-based effect types (2) +fun sandwichClose(g,f,h) {xlin; g(); close(f); h()} sandwichClose +stdout : fun : (() { |a::Lin}~> (), End, () { |a::Lin}~> b::Any) { |a::Lin}~> b::Any \ No newline at end of file diff --git a/tests/control_flow_linearity/choose.links b/tests/control_flow_linearity/choose.links new file mode 100644 index 000000000..2fb239550 --- /dev/null +++ b/tests/control_flow_linearity/choose.links @@ -0,0 +1,43 @@ +# Adapted from examples/handlers/choose.links + +# Choice example. + +# The choice computation +fun choice() { + var x = if (do Choose()) { 2 } + else { 4 }; + var y = if (do Choose()) { 8 } + else { 16 }; + x + y +} + +# Linear version of Choose +fun lin_choice() { + var x = if (lindo Choose()) { 2 } + else { 4 }; + var y = if (lindo Choose()) { 8 } + else { 16 }; + x + y +} + +# +# A few (closed) handlers +# + +# The "positive" handler +fun positive(m)() { + handle(m()) { + case x -> x + case -> xlin; k(true) + } +} + +# The "I'll-take-everything" handler +fun enumerate(m)() { + handle(m()) { + case x -> [x] + case k> -> k(true) ++ k(false) + } +} + +[positive(lin_choice)()] ++ enumerate(choice)() \ No newline at end of file diff --git a/tests/control_flow_linearity/choose_and_state.links b/tests/control_flow_linearity/choose_and_state.links new file mode 100644 index 000000000..dabc0428f --- /dev/null +++ b/tests/control_flow_linearity/choose_and_state.links @@ -0,0 +1,27 @@ +fun incr(x) {var y = do Get; do Put(x+y)} + +fun choice() { + var x = if (do Choose()) { incr(1); do Get } + else { incr(1); do Get }; + var y = if (do Choose()) { incr(1); do Get } + else { incr(1); do Get }; + x + y +} + +fun enumerate(m)() { + handle(m()) { + case x -> [x] + case k> -> k(true) ++ k(false) + } +} + + +fun evalState(st)(m)() { + (handle(m()) { + case x -> fun(_) { x } + case k> -> fun(st) { k(st)(st) } + case k> -> fun(_) { k(())(p) } + })(st) +} + +evalState(0)(enumerate(choice))() ++ enumerate(evalState(0)(choice))() \ No newline at end of file diff --git a/tests/control_flow_linearity/choose_and_state2.links b/tests/control_flow_linearity/choose_and_state2.links new file mode 100644 index 000000000..88459e5fc --- /dev/null +++ b/tests/control_flow_linearity/choose_and_state2.links @@ -0,0 +1,33 @@ +fun incr(x) {var y = do Get; do Put(x+y)} + +# this example shows that we can mix linear and unlimited operations +fun choice() { + var x = if (lindo Choose()) { incr(1); do Get } + else { incr(1); do Get }; + var y = if (lindo Choose()) { incr(1); do Get } + else { incr(1); do Get }; + x + y +} + +fun positive(m)() { + handle(m()) { + case x -> x + case -> xlin; k(true) + } +} + +fun evalState(st)(m)() { + (handle(m()) { + case x -> fun(_) { x } + case k> -> fun(st) { k(st)(st) } + case k> -> fun(_) { k(())(p) } + })(st) +} + +# First handling choose then handling state is ill-typed. This is +# because the continuation `k` in `positive` is linear, which excludes +# the usage of unlimited operations `Get` and `Put`. + +# evalState(0)(positive(choice))() + +positive(evalState(0)(choice))() \ No newline at end of file diff --git a/tests/control_flow_linearity/issue544a.links b/tests/control_flow_linearity/issue544a.links new file mode 100644 index 000000000..0a86313a9 --- /dev/null +++ b/tests/control_flow_linearity/issue544a.links @@ -0,0 +1,49 @@ +# issue 544a +# https://github.com/links-lang/links/issues/544 + +# Breaking session fidelity. +# Invoke the resumption twice to inadvertently perform two receives +# over a session-typed channel !Int.end. + +# A fixed version +fun deadlock_correct() { + var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) + }); + + handle({ + # Nondeterministic choice. + ignore(lindo Flip); + xlin; + var (i, ch) = receive(ch); + println("Int: " ^^ intToString(i)); + close(ch) + }) { + case _ -> () + case -> xlin; resume(true) + } +} + +# The original incorrect version +fun deadlock() { + var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) + }); + + handle({ + # Nondeterministic choice. + ignore(do Flip); + xlin; + var (i, ch) = receive(ch); + println("Int: " ^^ intToString(i)); + close(ch) + }) { + case _ -> () + case resume> -> + resume(true); resume(false) + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/issue544b.links b/tests/control_flow_linearity/issue544b.links new file mode 100644 index 000000000..c4674bfaf --- /dev/null +++ b/tests/control_flow_linearity/issue544b.links @@ -0,0 +1,62 @@ +# issue 544b +# https://github.com/links-lang/links/issues/544 + + +# Breaking type safety. +# Inadvertently send two integers over a session-typed channel +# !Int.!String.end by using multi-shot continuations and exceptions. + +# A fixed version +fun unsound_correct() { + var ch = fork(fun(ch) { + xlin; + var (i, ch) = receive(ch); + var (s, ch) = receive(ch); + println("Int: " ^^ intToString(i)); + println("String: " ^^ s); + close(ch) + }); + + handle({ + # Nondeterministic choice. + var msg = if (lindo Flip) 42 else 84; + xlin; + var ch = send(msg, ch); + # Throws an exception + lindo Fail; + var ch = send("foo", ch); + close(ch) + }) { + case _ -> () + case -> xlin; println("Failed"); resume(()) + case -> xlin; resume(true) + } +} + +# The original incorrect version +fun unsound() { + var ch = fork(fun(ch) { + xlin; + var (i, ch) = receive(ch); + var (s, ch) = receive(ch); + println("Int: " ^^ intToString(i)); + println("String: " ^^ s); + close(ch) + }); + + handle({ + # Nondeterministic choice. + var msg = if (do Flip) 42 else 84; + xlin; + var ch = send(msg, ch); + # Throws an exception + ignore(do Fail); + var ch = send("foo", ch); + close(ch) + }) { + case _ -> () + case -> () + case resume> -> + resume(true); resume(false) + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/lin_deep1.links b/tests/control_flow_linearity/lin_deep1.links new file mode 100644 index 000000000..01f5ae76c --- /dev/null +++ b/tests/control_flow_linearity/lin_deep1.links @@ -0,0 +1,19 @@ +# Using the linear variable `ch` in a deep handler is invalid + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +handle({ + xlin; + lindo Foo() + 42 +}) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + k(i) + } +} diff --git a/tests/control_flow_linearity/lin_deep2.links b/tests/control_flow_linearity/lin_deep2.links new file mode 100644 index 000000000..5a7bcb468 --- /dev/null +++ b/tests/control_flow_linearity/lin_deep2.links @@ -0,0 +1,23 @@ +# Using the linear variable `ch` in a deep handler is invalid + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +handle({ + xlin; + lindo Foo() + 42 +}) { + case _ -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + i + } + case -> { + xlin; + k(1) + } +} diff --git a/tests/control_flow_linearity/lin_deep3.links b/tests/control_flow_linearity/lin_deep3.links new file mode 100644 index 000000000..e8b2a892f --- /dev/null +++ b/tests/control_flow_linearity/lin_deep3.links @@ -0,0 +1,19 @@ +# Use the linear variable `ch` in a deep handler by passing it to the operation + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +handle({ + xlin; + lindo Foo(ch) + 42 +}) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + k(i) + } +} diff --git a/tests/control_flow_linearity/lin_shallow1.links b/tests/control_flow_linearity/lin_shallow1.links new file mode 100644 index 000000000..8209c3959 --- /dev/null +++ b/tests/control_flow_linearity/lin_shallow1.links @@ -0,0 +1,21 @@ +# Use the linear variable `ch` in a shallow handler + +fun() { + var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) + }); + + shallowhandle({ + xlin; + lindo Foo() + 42 + }) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + k(i) + } + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/lin_shallow2.links b/tests/control_flow_linearity/lin_shallow2.links new file mode 100644 index 000000000..4cecc72c9 --- /dev/null +++ b/tests/control_flow_linearity/lin_shallow2.links @@ -0,0 +1,13 @@ +# Using the linear variable `lf` twice (once inside the handler, once +# outside the handler) is invalid + +fun() { + var lf = linfun(x) {x}; + + shallowhandle({ + xlin; + lf(lindo Foo) + }) { + case -> xlin; k(lf(1)) + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/lin_shallow3.links b/tests/control_flow_linearity/lin_shallow3.links new file mode 100644 index 000000000..df550088d --- /dev/null +++ b/tests/control_flow_linearity/lin_shallow3.links @@ -0,0 +1,24 @@ +# Using the linear variable `ch` in a recursive function is invalid + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +sig h : (() {Foo:() =@ Int|a::Lin}~@ b) { |_::Lin}-> () {Foo{_::Lin}|a::Lin}~@ b +fun h(m) { + xlin; + linfun() { + shallowhandle({xlin; m()}) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + h(linfun(){xlin; k(i)})() + } + } + } +} + +h(linfun(){xlin; lindo Foo() + 42})() \ No newline at end of file diff --git a/tests/control_flow_linearity/lin_shallow4.links b/tests/control_flow_linearity/lin_shallow4.links new file mode 100644 index 000000000..d1f294108 --- /dev/null +++ b/tests/control_flow_linearity/lin_shallow4.links @@ -0,0 +1,32 @@ +# Use the linear variable `ch` in a shallow handler with an auxiliary +# recursive function + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +sig h : (() {Foo:() =@ Int|a::Lin}~@ b) { |_::Lin}-> () {Foo{_::Lin}|a::Lin}~@ b +fun h(m) { + xlin; + linfun() { + shallowhandle({xlin; m()}) { + case -> { + xlin; + h(linfun(){xlin; k(0)})() + } + } + } +} + +shallowhandle({ + lindo Foo() + 42 +}) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + h(linfun(){xlin; k(i)})() + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/lin_shallow5.links b/tests/control_flow_linearity/lin_shallow5.links new file mode 100644 index 000000000..cb407ffe9 --- /dev/null +++ b/tests/control_flow_linearity/lin_shallow5.links @@ -0,0 +1,21 @@ +# Use the linear variable `ch` in a shallow handler with an auxiliary +# deep handler + +var ch = fork(fun(ch) { + xlin; + var ch = send(42, ch); + close(ch) +}); + +shallowhandle({ + lindo Foo() + 42 +}) { + case -> { + xlin; + var (i, ch) = receive(ch); + close(ch); + handle ({xlin; k(i)}) { + case -> xlin; k(0) + } + } +} \ No newline at end of file diff --git a/tests/control_flow_linearity/popl24/intro.links b/tests/control_flow_linearity/popl24/intro.links new file mode 100644 index 000000000..04831c13d --- /dev/null +++ b/tests/control_flow_linearity/popl24/intro.links @@ -0,0 +1,24 @@ +sig outch : () ~> !Int.!String.End +fun outch() { + fork(fun(ic) { + var (i, ic) = receive(ic); # receive the integer + var (s, ic) = receive(ic); # receive the string + print(intToString(i) ^^ s); # convert, concat, and print + close(ic) # close the input channel + }) +} + +# sig unsound : () {}~> () +# fun unsound() { +handle({ + var oc = outch(); + var msg = if (do Flip) 42 else 84; # choose an integer message to send + var oc = send(msg, oc); + do Fail; # this is our exception + var oc = send("well-typed", oc); + close(oc) +}) { + case -> () + case resume> -> resume(true); resume(false) +} +# } diff --git a/tests/control_flow_linearity/popl24/intro_fixed.links b/tests/control_flow_linearity/popl24/intro_fixed.links new file mode 100644 index 000000000..d6eaaeb34 --- /dev/null +++ b/tests/control_flow_linearity/popl24/intro_fixed.links @@ -0,0 +1,24 @@ +sig outch : () { |_::Lin}~> !Int.!String.End +fun outch() { + xlin; + fork(fun(ic) { + xlin; + var (i, ic) = receive(ic); # receive the integer + var (s, ic) = receive(ic); # receive the string + print(intToString(i) ^^ s); # convert, concat, and print + close(ic) # close the input channel + }) +} + +handle({ + xlin; + var oc = outch(); + var msg = if (lindo Flip) 42 else 84; # choose an integer message to send + var oc = send(msg, oc); + lindo Fail; # this is our exception + var oc = send("well-typed", oc); + close(oc) +}) { + case -> xlin; resume(()) + case -> xlin; resume(true) +} \ No newline at end of file diff --git a/tests/examples_default_with_cfl_on.config b/tests/examples_default_with_cfl_on.config new file mode 100644 index 000000000..39e7e464f --- /dev/null +++ b/tests/examples_default_with_cfl_on.config @@ -0,0 +1,5 @@ +#typecheck_ir=true +typecheck_only=true +enable_handlers=true +track_control_flow_linearity=true +session_exceptions=false diff --git a/tests/freezeml.config b/tests/freezeml.config index 6e018ee9f..e6ab82e59 100644 --- a/tests/freezeml.config +++ b/tests/freezeml.config @@ -1,3 +1,3 @@ prelude=tests/freezeml_prelude.links show_quantifiers=true -hide_fresh_type_vars=false +hide_fresh_type_vars=false \ No newline at end of file diff --git a/tests/handler_linearity.tests b/tests/handler_linearity.tests deleted file mode 100644 index 1299b8117..000000000 --- a/tests/handler_linearity.tests +++ /dev/null @@ -1,48 +0,0 @@ -Use linear variables in deep handlers (1) -tests/handlers/lin_deep1.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* of linear type .* is used in a deep handler.* -args : --enable-handlers - -Use linear variables in deep handlers (2) -tests/handlers/lin_deep2.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* of linear type .* is used in a deep handler.* -args : --enable-handlers - -Use linear variables in deep handlers (3) -tests/handlers/lin_deep3.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* has linear type .* is used .* times.* -args : --enable-handlers - -Use linear variables in deep handlers (4) -tests/handlers/lin_deep4.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* of linear type .* is used in a deep handler.* -args : --enable-handlers - - -Use linear variables in shallow handlers (1) -tests/handlers/lin_shallow1.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* has linear type .* is used .* times.* -args : --enable-handlers - -Use linear variables in shallow handlers (2) -tests/handlers/lin_shallow2.links -filemode : true -exit : 1 -stderr : @.*Type error: Variable .* has linear type .* is used .* times.* -args : --enable-handlers - -Use linear variables in shallow handlers (3) -tests/handlers/lin_shallow3.links -filemode : true -stdout : 2 : Int -args : --enable-handlers \ No newline at end of file diff --git a/tests/handlers/lin_deep1.links b/tests/handlers/lin_deep1.links deleted file mode 100644 index 12ad79f70..000000000 --- a/tests/handlers/lin_deep1.links +++ /dev/null @@ -1,11 +0,0 @@ -var lf = linfun(x) {x}; - -handle({ - ignore(do Foo); - lf(2) -}) { - case resume> -> { - ignore(lf(3)); - resume(()) - } -} \ No newline at end of file diff --git a/tests/handlers/lin_deep2.links b/tests/handlers/lin_deep2.links deleted file mode 100644 index 6d09f67bc..000000000 --- a/tests/handlers/lin_deep2.links +++ /dev/null @@ -1,19 +0,0 @@ -var ch = fork(fun(ch) { - var ch = send(42, ch); - close(ch) -}); - -handle({ - ignore(do Foo); - var (i, ch) = receive(ch); - println("Int: " ^^ intToString(i)); - close(ch) -}) { - case _ -> () - case resume> -> { - var (i, ch) = receive(ch); - println("Int: " ^^ intToString(i)); - close(ch); - resume(()) - } -} \ No newline at end of file diff --git a/tests/handlers/lin_deep3.links b/tests/handlers/lin_deep3.links deleted file mode 100644 index d87361339..000000000 --- a/tests/handlers/lin_deep3.links +++ /dev/null @@ -1,18 +0,0 @@ -fun test() { - var ch = fork(fun(ch) { - var ch = send(42, ch); - close(ch) - }); - - handle({ - ignore(do Flip(ch)) - }) { - case _ -> () - case resume> -> { - ignore(do Flip(ch)); - var (i, ch) = receive(ch); - close(ch); - resume(true) - } - } -} diff --git a/tests/handlers/lin_deep4.links b/tests/handlers/lin_deep4.links deleted file mode 100644 index e9e44b6ef..000000000 --- a/tests/handlers/lin_deep4.links +++ /dev/null @@ -1,11 +0,0 @@ -var lf = linfun(x) {x}; - -handle({ - ignore(do Foo); - lf(2) -}) { - case _ -> lf(3) - case resume> -> { - resume(()) - } -} \ No newline at end of file diff --git a/tests/handlers/lin_shallow1.links b/tests/handlers/lin_shallow1.links deleted file mode 100644 index adfc0287e..000000000 --- a/tests/handlers/lin_shallow1.links +++ /dev/null @@ -1,12 +0,0 @@ -{ - var lf = linfun(x) {x}; - - shallowhandle({ - ignore(do Foo); - lf(1) - }) { - case _> -> { - lf(2) - } - } -} \ No newline at end of file diff --git a/tests/handlers/lin_shallow2.links b/tests/handlers/lin_shallow2.links deleted file mode 100644 index 07130aa02..000000000 --- a/tests/handlers/lin_shallow2.links +++ /dev/null @@ -1,11 +0,0 @@ -{ - var lf = linfun(x) {x}; - - shallowhandle({ - ignore(do Foo); - lf(1) - }) { - case _ -> lf(2) - case _> -> 3 - } -} \ No newline at end of file diff --git a/tests/handlers/lin_shallow3.links b/tests/handlers/lin_shallow3.links deleted file mode 100644 index 2eaf75ec2..000000000 --- a/tests/handlers/lin_shallow3.links +++ /dev/null @@ -1,12 +0,0 @@ -{ - var lf = linfun(x) {x}; - - shallowhandle({ - ignore(do Foo); - 1 - }) { - case _> -> { - lf(2) - } - } -} \ No newline at end of file diff --git a/tests/handlers_with_cfl_on.tests b/tests/handlers_with_cfl_on.tests new file mode 100644 index 000000000..998aab9e9 --- /dev/null +++ b/tests/handlers_with_cfl_on.tests @@ -0,0 +1,491 @@ +--- +config: tests/control_flow_linearity.config +--- + +Identity handler (1) +{ handle(42) {case x -> x} } +stdout : 42 : Int +args : --enable-handlers + +Identity handler (2) +handle(42) {case x -> x} +stdout : 42 : Int +args : --enable-handlers + +Listify handler (1) +{ handle(42) {case x -> [x]} } +stdout : [42] : [Int] +args : --enable-handlers + +Listify handler (2) +handle(42) {case x -> [x]} +stdout : [42] : [Int] +args : --enable-handlers + +Listify handler (3) +{ handle([42, 41, 40, 39]) {case x -> [x]} } +stdout : [[42, 41, 40, 39]] : [[Int]] +args : --enable-handlers + +Listify handler (4) +handle([42, 41, 40, 39]) {case x -> [x]} +stdout : [[42, 41, 40, 39]] : [[Int]] +args : --enable-handlers + +Top level operation invocation +{ do Foo } +stderr : @. +exit : 1 +args : --enable-handlers + +Operation invocation sugar (1) +{ fun() { do Foo } } +stdout : fun : () {Foo:() => a|_}-> a +args : --enable-handlers + +Operation invocation sugar (2) +{ fun() { do Foo() } } +stdout : fun : () {Foo:() => a|_}-> a +args : --enable-handlers + +Operation invocation sugar (3) +{ fun() { do Foo(()) } } +stdout : fun : () {Foo:(()) => a|_}-> a +args : --enable-handlers + +Operation invocation sugar (4) +fun() { do Foo } +stdout : fun : () {Foo:() => a|_}-> a +args : --enable-handlers + +Operation invocation sugar (5) +fun() { do Foo() } +stdout : fun : () {Foo:() => a|_}-> a +args : --enable-handlers + +Operation invocation sugar (6) +fun() { do Foo(()) } +stdout : fun : () {Foo:(()) => a|_}-> a +args : --enable-handlers + +Exception handling (1) +{ handle({do Fail; 42}) {case -> Nothing : Maybe(Int) case x -> Just(x) : Maybe(Int)} } +stdout : Nothing : Maybe (Int) +args : --enable-handlers + +Exception handling (2) +{ handle(42) {case -> Nothing : Maybe(Int) case x -> Just(x) : Maybe(Int)} } +stdout : Just(42) : Maybe (Int) +args : --enable-handlers + +Exception handling (3) +{ handle({var _ = do Fail : Zero; 42}) {case k> -> k(42) : Either(String,Int) case x -> Right(x) : Either(String, Int)} } +stderr : @. +exit : 1 +args : --enable-handlers + +Exception handling (4) +handle({do Fail; 42}) {case -> Nothing : Maybe(Int) case x -> Just(x) : Maybe(Int)} +stdout : Nothing : Maybe (Int) +args : --enable-handlers + +Exception handling (5) +handle(42) {case -> Nothing : Maybe(Int) case x -> Just(x) : Maybe(Int)} +stdout : Just(42) : Maybe (Int) +args : --enable-handlers + +Exception handling (6) +handle({var _ = do Fail : Zero; 42}) {case k> -> k(42) : Either(String,Int) case x -> Right(x) : Either(String, Int)} +stderr : @. +exit : 1 +args : --enable-handlers + +Binary choice handling (1) +{ handle({ var x = if (do Choose) 40 else 20; var y = if (do Choose) 2 else -20; x + y }) {case k> -> k(true) ++ k(false) case x -> [x]} } +stdout : [42, 20, 22, 0] : [Int] +args : --enable-handlers + +Binary choice handling (2) +handle({ var x = if (do Choose) 40 else 20; var y = if (do Choose) 2 else -20; x + y }) {case k> -> k(true) ++ k(false) case x -> [x]} +stdout : [42, 20, 22, 0] : [Int] +args : --enable-handlers + +Deep continuation escape (1) +{ fromJust(handle({ do Escape; print("Back in action"); do Escape}) { case k> -> Just(k) case _ -> Nothing })(()) } +stdout : @. +exit : 0 +args : --enable-handlers + +Deep continuation escape (2) +fromJust(handle({ do Escape; print("Back in action"); do Escape}) { case k> -> Just(k) case _ -> Nothing })(()) +stdout : @. +exit : 0 +args : --enable-handlers + +Type-and-effect signature for deep handler (1) +sig allChoices : (Comp(a, {Choose:Bool|e})) {Choose{_}|e}~> [a] fun allChoices(m) {handle(m()) {case x -> [x] case k> -> k(true) ++ k(false) }} +stdout : () : () +args : --enable-handlers + +Type-and-effect signature for deep handler (2) +sig allChoices : (Comp(a, {Choose:Bool|e})) -> Comp([a], {Choose{_}|e}) fun allChoices(m)() {handle(m()) {case x -> [x] case k> -> k(true) ++ k(false)}} +stdout : () : () +args : --enable-handlers + +Type-and-effect signature for deep handler (3) +sig allChoices : (Comp(a, {Choose:Bool|e})) -> Comp([a], {Choose- |e}) fun allChoices(m)() {handle(m()) {case x -> [x] case k> -> k(true) ++ k(false)}} +stdout : () : () +args : --enable-handlers + +Type-and-effect signature for shallow handler (1) +sig allChoices : (Comp(a, {Choose:Bool|e})) {Choose{_}|e}~> [a] fun allChoices(m) {shallowhandle(m()) {case x -> [x] case k> -> allChoices(fun() {k(true)}) ++ allChoices(fun(){k(false)}) }} +stdout : () : () +args : --enable-handlers + +Type-and-effect signature for shallow handler (2) +sig allChoices : (Comp(a, {Choose:Bool|e})) -> Comp([a], {Choose{_}|e}) fun allChoices(m)() {shallowhandle(m()) {case x -> [x] case k> -> allChoices(fun(){k(true)})() ++ allChoices(fun(){k(false)})()}} +stdout : () : () +args : --enable-handlers + +Type-and-effect signature for shallow handler (3) +sig allChoices : (Comp(a, {Choose:Bool|e})) -> Comp([a], {Choose- |e}) fun allChoices(m)() {shallowhandle(m()) {case x -> [x] case k> -> allChoices(fun(){k(true)})() ++ allChoices(fun(){k(false)})()}} +stdout : () : () +args : --enable-handlers + +Type inference for deep handler +fun() { handle({do A; do B}) { case k> -> k(()) case x -> x } } +stdout : fun : () {A{_},B:() => b|_}~> b +args : --enable-handlers + +Soundness +{fun mapk(m) { handle(m()) {case k> -> map(k,p) case x -> [x]} } } +stderr : @. +exit : 1 +args : --enable-handlers + +Deep state handling (1) +{fun state(m) { handle(m()) { case k> -> fun(s) { k(s)(s) } case k> -> fun(s) { k(())(p) } case x -> fun(s) { x } } } fun runState(s0, c) { var f = state(c); f(s0) } runState(2, fun() { var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get }) } +stdout : 6 : Int +args : --enable-handlers + +Deep state handling (2) +{fun state(m)(s) { handle(m())(s <- s) { case k> -> k(s,s) case k> -> k((),p) case x -> x } } fun runState(s0, c) { state(c)(s0) } runState(2, fun() { var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get }) } +stdout : 6 : Int +args : --enable-handlers + +Deep state handling (3) +handle({ var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get })(s <- 2) { case k> -> k(s,s) case k> -> k((),p) case x -> x } +stdout : 6 : Int +args : --enable-handlers + +Shallow state handling (1) +{fun state(m)(s) { shallowhandle(m()) { case k> -> state(fun(){k(s)})(s) case k> -> state(fun(){k(())})(p) case x -> x}} fun runState(s0, c) { var f = state(c); f(s0) } runState(2, fun() { var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get }) } +stdout : 6 : Int +args : --enable-handlers + +Shallow state handling (2) +{ fun simpleState(m)(s) { shallowhandle(m()) { case k> -> simpleState(fun() { k(s) })(s) case k> -> simpleState(fun() { k(()) })(s) case x -> x } } fun count() { var n = do Get; if (n == 0) {n} else {do Put(n-1); count() }} simpleState(count)(10) } +stdout : 0 : Int +args : --enable-handlers + +Shadowing handler parameter (1) +{ handle({ var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get })(s <- 0) { case k> -> k(s,s) case k> -> k((),s) case x -> x } } +stdout : 2 : Int +args : --enable-handlers + +Shadowing handler parameter (2) +{ handle({ var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get })(s <- 0) { case k> -> k(s,s) case k> -> k((),s) case x -> x } } +stdout : 2 : Int +args : --enable-handlers + +Shadowing handler parameter (3) +{ handle({ var s = do Get; do Put(s + 1); var s = do Get; do Put(s + s); do Get })(s <- 0) { case k> -> k(s,s) case k> -> k((),s) case x -> x } } +stdout : 2 : Int +args : --enable-handlers + +Operation parameter pattern-matching (1) +ignore(fun (m) { handle(m()) { case -> 1 case k> -> 2 case -> 3 case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (2) +ignore(fun(m) { handle(m()) { case k> -> k(q) case k> -> k(t) case -> d case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (3) +ignore(fun(m) { handle(m()) { case k> -> k(1) case k> -> k(s) case -> 3 case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (4) +ignore(fun(m) { handle(m()) { case k> -> k(1.0) case k> -> k(s) case -> 3.0 case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (5) +ignore(fun(m) { handle(m()) { case k> -> k(1) case k> -> k(s) case -> a case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (6) +ignore(fun(m) { handle(m()) { case k> -> k(y) case k> -> k(z) case -> a case x -> x } }) +stdout : () : () +args : --enable-handlers + +Operation parameter pattern-matching (7) +fun(m) { handle(m()) { case -> 'A' case -> 'B' case -> 'U' case x -> x } } +stdout : fun : (() {Move:([|Alice|Bob|_|]) => _::Any|c}~> Char) {Move{_}|c}~> Char +args : --enable-handlers + +Operation parameter pattern-matching (8) +handle(do Move(Alice)) { case -> 'A' case -> 'B' case -> 'U' case x -> x } +stdout : 'A' : Char +args : --enable-handlers + +Operation parameter pattern-matching (9) +handle(do Move(John)) { case -> 'A' case -> 'B' case -> 'U' case x -> x } +stdout : 'U' : Char +args : --enable-handlers + +Pattern-matching on continuation parameter (1) +ignore(fun(m) { handle(m()) { case -> 0 case x -> x } }) +stdout : () : () +args : --enable-handlers + +Pattern-matching on continuation parameter (2) +ignore(fun(m) { handle(m()) { case (k as f)> -> f(1) case x -> x } }) +stdout : () : () +args : --enable-handlers + +Pattern-matching on continuation parameter (3) +ignore(fun(m) { handle(m()) { case 2> -> f(1) case x -> x } }) +stderr : @. +exit : 1 +args : --enable-handlers + +Value parameter pattern-matching (1) +ignore(fun(m) { handle(m()) { case k> -> 1 case _ -> 0 } }) +stdout : () : () +args : --enable-handlers + +Value parameter pattern-matching (2) +ignore(fun(m) { handle(m()) { case k> -> 1 case x as y -> y } }) +stdout : () : () +args : --enable-handlers + +Value parameter pattern-matching (3) +ignore(fun(m) { handle(m()) { case k> -> 1 case 10 -> 10 } }) +stdout : () : () +args : --enable-handlers + +Value parameter pattern-matching (4) +ignore(fun(m) { handle(m()) { case k> -> 1 case 100.0 -> 0 } }) +stdout : () : () +args : --enable-handlers + +Value parameter pattern-matching (5) +ignore(fun(m) { handle(m()) { case k> -> 1 case Alice -> 0 } }) +stdout : () : () +args : --enable-handlers + +Value parameter pattern-matching (6) +ignore(fun(m) { handle(m()) { case k> -> 1 case (x,y) -> 0 } }) +stdout : () : () +args : --enable-handlers + +Pattern-matching on handler parameter (1) +handle(true)(_ <- 100) { case x -> x } +stdout : true : Bool +args : --enable-handlers + +Pattern-matching on handler parameter (2) +handle(true)(100 <- 100) { case x -> x} +stdout : true : Bool +args : --enable-handlers + +Pattern-matching on handler parameter (2) +handle(true)(99 <- 100) { case x -> x} +stderr : @. +exit : 1 +args : --enable-handlers + +Pattern-matching on handler parameter (3) +handle(true)(Foo(s) <- Foo(42)) { case _ -> s} +stdout : 42 : Int +args : --enable-handlers + +Pattern-matching on handler parameter (4) +handle(true)(Foo(s) <- Bar(42)) { case _ -> s} +stderr : @. +exit : 1 +args : --enable-handlers + +Pattern-matching on handler parameter (5) +handle(true)((x,y) <- (2,1)) { case _ -> x + y} +stdout : 3 : Int +args : --enable-handlers + +Pattern-matching on handler parameter (6) +handle(true)("Hello" <- "Hello") { case x -> x} +stdout : true : Bool +args : --enable-handlers + +Pattern-matching on handler parameter (7) +handle(true)((a=x, b=y) <- (a=44,b=(-2))) { case _ -> x + y} +stdout : 42 : Int +args : --enable-handlers + +Pattern-matching on handler parameter (8) +handle(true)(r <- (a=44,b=(-2))) { case _ -> r.a + r.b} +stdout : 42 : Int +args : --enable-handlers + +Deep Handler composition +fun h1(m)() { handle(m()) { case k> -> k(1) } } fun h2(m)() { handle(m()) { case k> -> k(2) } } fun h3(m)() { handle(m()) { case k> -> k(3) } } h1(h2(h3(fun() { do Op1 + do Op2 + do Op3 })))() +stdout : 6 : Int +args : --enable-handlers + +Type annotation on deep continuation parameter +fun h1(m) { handle(m()) { case (k : ((Int) {Op{_}|_}~> Int)) > -> k(1) } } +stdout : () : () +args : --enable-handlers + +Type annotation on shallow continuation parameter +fun h1(m) { shallowhandle(m()) { case (k : ((Int) {Op:Int|_}~> Int))> -> h1(fun() { k(1) }) } } +stdout : () : () +args : --enable-handlers + +Shallow addition with a single recursive handler +{ fun h1(m) { shallowhandle(m()) { case k> -> h1(fun() { k(1) }) case x -> x - 1 } } h1(fun() { do One + do One }) } +stdout : 1 : Int +args : --enable-handlers + +Shallow addition with two mutual recursive handlers +{ fun h1(m) { shallowhandle(m()) { case k> -> h1(fun() { k(1) }) } } fun h2(m) { shallowhandle(m()) { case k> -> h1(fun() { k(2) }) } } h2(fun() { do One + do One }) } +stdout : 3 : Int +args : --enable-handlers + +Shallow handler composition +{ fun h1(m)() { shallowhandle(m()) { case k> -> h1(fun() { k(1) })() } } fun h2(m)() { shallowhandle(m()) { case k> -> h2(fun() { k(2) })() } } h1(h2(fun() { do Op1 + do Op2 }))() } +stdout : 3 : Int +args : --enable-handlers + +Type ascription, parameterised handlers (1) +{ fun(a : Int)(b : Float)(c : String)(m)() { handle (m())(x <- a, y <- b, z <- c) { case k> -> k(c,42,p,"Foo") case _ -> x } } } +stdout : fun : (Int) -> (Float) -> (String) -> (() {Op:(Float) => String|d}~> _) -> () {Op{_}|d}~> Int +args : --enable-handlers + +Type ascription, parameterised handlers (2) +{ fun(a : Float, b : String, c : Int)(m)() { handle(m())(x <- a, y <- b, z <- c) { case k> -> k(x,p,"Bar",99) case _ -> y } } } +stdout : fun : (Float, String, Int) -> (() {Op:(Float) => Float|b}~> _) -> () {Op{_}|b}~> String +args : --enable-handlers + +Instantiate.ArityMismatch #132 (RESOLVED) +sig f : (() {Foo:Int|a}~> b) {Foo{_}|a}~> b fun f(m) { error("N/A") } fun g(m) { var x = f(m); x } +stdout : () : () +args : --enable-handlers + +Operation polymorphism (1) +sig catch : (() {Fail:forall a.a |e}~> b) {Fail{_} |e}~> Maybe(b) fun catch(m) { handle(m()) { case k> : (forall a. () => a) -> Nothing case x -> Just(x) } } catch(fun() { 42 }) +stdout : Just(42) : Maybe (Int) +args : --enable-handlers + +Operation polymorphism (2) +sig catch : (() {Fail:forall a.a |e}~> b) {Fail{_} |e}~> Maybe(b) fun catch(m) { handle(m()) { case k> : (forall a. () => a) -> Nothing case x -> Just(x) } } sig f : () {Fail:forall a.a}~> Int fun f () { if (do Fail) 42 else do Fail } catch (f) +stdout : Nothing : Maybe (Int) +args : --enable-handlers + +Operation polymorphism (3) +sig h : (() {Switch:forall a,b. (a,b) => (b,a) |e}~> c) {Switch{_} |e}~> c fun h(m) { handle(m()) { case k> : (forall a,b. (a,b) => (b,a)) -> k ((y,x)) } } sig f : () {Switch:forall a,b. (a,b) => (b,a)}~> Int fun f () { var (d,u) = do Switch(2,4) ; 10*d+u } h(f) +stdout : 42 : Int +args : --enable-handlers + +Generalise (1) +gen0(fun(m)() { handle(m()) { case k> -> 42 case x -> x } }(fun(){42})) +stdout : fun : Comp (Int,{ |_}) +args : --enable-handlers + +Generalise (2) +gen0(fun(m)() { handle(m()) { case (k : ((()) {Foo- |_}~> Int))> -> 42 case x -> x } }(fun(){42})) +stdout : fun : Comp (Int,{ |_}) +args : --enable-handlers + +Recursive nesting of deep handlers +{ fun h1(m,h) { handle(m()) { case k> -> h(fun() { k(()) },h1) case x -> x } } fun h2(m,h) { handle(m()) { case k> -> h(fun() { k(()) },h2) case x -> x } } h1(fun(){42},h2) } +stdout : 42 : Int +args : --enable-handlers + +Parameterised handler with multiple parameters (1) +handle({do A; do B; do C; do D})(a <- 0, b <- 1, c <- 2, d <- 3) { case k> -> k((),a+1,b,c,d) case k> -> k((),a,b+1,c,d) case k> -> k((),a,b,c+1,d) case k> -> k((),a,b,c,d+1) case _ -> (a,b,c,d) } +stdout : (1, 2, 3, 4) : (Int, Int, Int, Int) +args : --enable-handlers + +Parameterised handler with multiple parameters (2) +handle({do A; do B; do C; do D})(a <- 0, b <- false, (c0, c1) as c <- (true,0), d <- "Hello") { case k> -> k((),a+1,b,c,d) case k> -> k((),a,not(b),c,d) case k> -> k((),a,b,(not(c0), c1+1),d) case k> -> k((),a,b,c,d ^^ " World") case _ -> (a,b,c,d) } +stdout : (1, true, (false, 1), "Hello World") : (Int, Bool, (Bool, Int), String) +args : --enable-handlers + +Effect type sugar (1) +fun(g : (() {A:a,B:(a) => b|_}~> b)) { g }(fun(){error("N/A")}) +stdout : fun : () {A:() => a,B:(a) => b|_}~> b +args : --enable-handlers + +Effect type sugar (2) +fun(g : (() {:a|_}~> a)) { g }(fun(){error("N/A")}) +stdout : fun : () {:a|_}~> a +args : --enable-handlers + +Effect type sugar (3) +fun(g : (() {wild:()|_}-> a)) { g }(fun(){error("N/A")}) +stdout : fun : () ~> _ +args : --enable-handlers + +Implicit return case (1) +handle(42) { } +stdout : 42 : Int +args : --enable-handlers + +Implicit return case (2) +handle(do Op) { case resume> -> resume(true) } +stdout : true : Bool +args : --enable-handlers + +Omission of resumption for nullary operations (1) +handle(do Foo) { case -> 5 } +stdout : 5 : Int +args : --enable-handlers + +Omission of resumption for nullary operations (2) +handle(do Foo) { case _> -> 6 } +stdout : 6 : Int +args : --enable-handlers + +Omission of resumption for nullary operations (3) +fun(m) { handle(m()) { case -> 5 } } +stdout : fun : (() {Foo:() => _::Any|b}~> Int) {Foo{_}|b}~> Int +args : --enable-handlers + +Operation annotation (1) +fun(m) { handle(m()) { case k> : ((Int) => Int) -> k (x) } } +stdout : fun : (() {Foo:(Int) => Int|a}~> b) {Foo{_}|a}~> b +args : --enable-handlers +# NOTE: stdout is different from handlers.tests since the default printing behaiour is changed (the `Any` kind of row variables is omitted) + +Operation annotation (2) +fun(f)(m) { handle(m()) { case k> -> k (f (x)) } } +stdout : fun : ((Bool) {Foo{a}|b}~> c::Any) -> (() {Foo:(Bool) => c::Any|b}~> e) {Foo{a}|b}~> e +args : --enable-handlers +# NOTE: stdout is different from handlers.tests since the default printing behaiour is changed (the `Any` kind of row variables is omitted) + +Operation annotation (3) +fun(m) { handle(m()) { case k> : ((a) => (() {}-> (a,a))) -> k ( fun () { (x,x) } ) } } +stdout : fun : (() {Foo:(a) => () {}-> (a, a)|b}~> c) {Foo{_}|b}~> c +args : --enable-handlers +# NOTE: stdout is different from handlers.tests since the default printing behaiour is changed (the `Any` kind of row variables is omitted) + +Examples +./examples/handlers/tests.links +filemode : true +stdout : () : () +args : --enable-handlers --path=examples/handlers --set=effect_sugar=true --set=effect_sugar_policy=final_arrow diff --git a/tests/sessions_with_cfl_on.tests b/tests/sessions_with_cfl_on.tests new file mode 100644 index 000000000..4d313bb92 --- /dev/null +++ b/tests/sessions_with_cfl_on.tests @@ -0,0 +1,60 @@ +--- +config: tests/control_flow_linearity.config +--- + +# NOTE: The tests are slightly different from sessions.tests due to +# the tracking of control flow linearity. + +Access points +fun f(ap) {send(42, request(ap))} f +stdout : fun : (AP (?(Int).~a::Session)) ~> a::Session + +Linear function annotation +sig h : ((a::Any) -e-@ a::Any, a::Any) { |e::Lin}-> a::Any fun h(f, x) {xlin; f(x)} +stdout : () : () +exit : 0 + +Non-linear use of linear function +sig h : ((a::Any) -e-@ a::Any, a::Any) { |e::Lin}-> a::Any fun h(f, x) {xlin; f(f(x))} +stderr : @..* +exit : 1 + +Linear identity +fun (x) {xlin; x} +stdout : fun : (a::Any) { |_::Lin}-> a::Any +exit : 0 + +Non-linear dup +fun (x) {(x, x)} +stdout : fun : (a) -> (a, a) +exit : 0 + +Receive value +fun (c) {xlin; receive(c).1} +stdout : fun : (?(a::Any)._::(Unl,Session)) { |_::Lin}~> a::Any +exit : 0 + +Receive channel +fun (c) {xlin; receive(c).2} +stdout : fun : (?(_).b::Session) { |_::Lin}~> b::Session +exit : 0 + +Ignore send +fun (c) {xlin; ignore(send(42, c))} +stdout : fun : (!(Int)._::(Unl,Session)) { |_::Lin}~> () +exit : 0 + +Linear end +ignore(request((new(): AP(End)))) +stderr : @..* +exit : 1 + +Non-linear generalisation (1) +{var x = A; ()} +stdout : () : () +exit : 0 + +Non-linear generalisation (2) +fun (r) {var (x=42|q) = r; ()} +stdout : @fun..* +exit : 0 \ No newline at end of file diff --git a/tests/typecheck_examples_with_cfl_on.tests b/tests/typecheck_examples_with_cfl_on.tests new file mode 100644 index 000000000..753c58f9a --- /dev/null +++ b/tests/typecheck_examples_with_cfl_on.tests @@ -0,0 +1,155 @@ +--- +config: tests/examples_default_with_cfl_on.config +--- + +# Only include the files in examples/handlers + +Typecheck example file examples/handlers/alert.links +examples/handlers/alert.links +filemode : true + +Typecheck example file examples/handlers/aop.links +examples/handlers/aop.links +filemode : true + +Typecheck example file examples/handlers/aop2.links +examples/handlers/aop2.links +filemode : true + +Typecheck example file examples/handlers/coins_web.links +examples/handlers/coins_web.links +filemode : true + +Typecheck example file examples/handlers/choose.links +examples/handlers/choose.links +filemode : true +args : --set=enable_handlers=true + +Typecheck example file examples/handlers/coins.links +examples/handlers/coins.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/concurrency.links +examples/handlers/concurrency.links +filemode : true +args : --set=enable_handlers=true + +Typecheck example file examples/handlers/coop.links +examples/handlers/coop.links +filemode : true +args : --set=enable_handlers=true + +Typecheck example file examples/handlers/count_web.links +examples/handlers/count_web.links +filemode : true +ignore : broken example + +Typecheck example file examples/handlers/deep_state.links +examples/handlers/deep_state.links +filemode : true + +Typecheck example file examples/handlers/exceptions.links +examples/handlers/exceptions.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/fringe.links +examples/handlers/fringe.links +filemode : true +args : --set=effect_sugar=true --set=effect_sugar_policy=final_arrow + +Typecheck example file examples/handlers/identity.links +examples/handlers/identity.links +filemode : true + +Typecheck example file examples/handlers/lambda.links +examples/handlers/lambda.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/light_switch.links +examples/handlers/light_switch.links +filemode : true + +Typecheck example file examples/handlers/monadic_reflection.links +examples/handlers/monadic_reflection.links +filemode : true +args : --set=effect_sugar=true --set=effect_sugar_policy=final_arrow + +Typecheck example file examples/handlers/nim.links +examples/handlers/nim.links +filemode : true +args : --set=enable_handlers=true + +Typecheck example file examples/handlers/nim-webversion.links +examples/handlers/nim-webversion.links +filemode : true + +Typecheck example file examples/handlers/number_games.links +examples/handlers/number_games.links +filemode : true + +Typecheck example file examples/handlers/pi.links +examples/handlers/pi.links +filemode : true + +Typecheck example file examples/handlers/pipes.links +examples/handlers/pipes.links +filemode : true + +Typecheck example file examples/handlers/racing-lines.links +examples/handlers/racing-lines.links +filemode : true + +Typecheck example file examples/handlers/sat.links +examples/handlers/sat.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/shiftreset.links +examples/handlers/shiftreset.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/shallow_state.links +examples/handlers/shallow_state.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/sierpinski-triangle.links +examples/handlers/sierpinski-triangle.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/sudoku.links +examples/handlers/sudoku.links +filemode : true +args : --set=effect_sugar=true + +Typecheck example file examples/handlers/tests.links +examples/handlers/tests.links +filemode : true +ignore : broken example + +Typecheck example file examples/handlers/toggle.links +examples/handlers/toggle.links +filemode : true +ignore : broken example + +Typecheck example file examples/handlers/toggle_web.links +examples/handlers/toggle_web.links +filemode : true +ignore : broken example + +Typecheck example file examples/handlers/transaction.links +examples/handlers/transaction.links +filemode : true + +Typecheck example file examples/handlers/unhandled.links +examples/handlers/unhandled.links +filemode : true + +Typecheck example file examples/handlers/u2_puzzle.links +examples/handlers/u2_puzzle.links +filemode : true \ No newline at end of file