From dc29e187718075506dcddf043cede6d88b96379e Mon Sep 17 00:00:00 2001 From: kumber Date: Sun, 12 Apr 2026 16:36:50 +0200 Subject: [PATCH 1/3] to surface --- src/DblParser/Desugar.ml | 20 ++++++++++++++++---- src/DblParser/Raw.ml | 3 +++ src/DblParser/YaccParser.mly | 10 ++++++++++ src/TypeInference/Type.ml | 7 ++++++- 4 files changed, 35 insertions(+), 5 deletions(-) diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index e1f7dbd1..9aebd071 100644 --- a/src/DblParser/Desugar.ml +++ b/src/DblParser/Desugar.ml @@ -136,6 +136,18 @@ let rec tr_type_expr (tp : Raw.type_expr) = make (TEffect (List.map tr_type_expr tps)) | TApp(tp1, tp2) -> make (TApp(tr_type_expr tp1, tr_type_expr tp2)) + | THandler (effct_opt, cap_tp, in_comp, out_comp) -> + let cap_type = tr_type_expr cap_tp in + let effct = Option.value effct_opt ~default:"_" in + let in_eff_opt, in_type = tr_eff_type in_comp in + let in_eff = + Option.value in_eff_opt ~default:(make (TEffect [ make TWildcard ])) + in + let out_eff_opt, out_type = tr_eff_type out_comp in + let out_eff = + Option.value out_eff_opt ~default:(make (TEffect [ make TWildcard ])) + in + make (THandler { effct; cap_type; in_type; in_eff; out_type; out_eff }) | TRecord _ | TTypeLbl _ -> Error.fatal (Error.desugar_error tp.pos) @@ -178,7 +190,7 @@ and tr_scheme_expr (tp : Raw.type_expr) = Error.fatal (Error.impure_scheme pos) end - | TWildcard | TVar _ | TArrow _ | TEffect _ | TApp _ -> + | TWildcard | TVar _ | TArrow _ | TEffect _ | TApp _ | THandler _ -> { sch_pos = pos; sch_args = []; sch_body = tr_type_expr tp @@ -214,7 +226,7 @@ and tr_type_var (tp : Raw.type_expr) = let k = Option.value ka ~default:(make KWildcard) in (x, k) | TVar ({data = NPSel _; _}, _) | TWildcard | TArrow _ | TEffect _ | TApp _ - | TRecord _ | TTypeLbl _ -> + | THandler _ | TRecord _ | TTypeLbl _ -> Error.fatal (Error.desugar_error tp.pos) (** Translate a type expression as a type parameter *) @@ -240,7 +252,7 @@ let rec tr_named_type_arg (tp : Raw.type_expr) = | TTypeLbl tp -> make (TNAnon, tr_type_arg tp) | TWildcard -> make (TNAnon, make (TA_Wildcard)) | TVar ({data = NPSel _; _}, _) | TArrow _ | TEffect _ | TApp _ - | TRecord _ -> + | THandler _ | TRecord _ -> Error.fatal (Error.desugar_error tp.pos) (** Translate a left-hand-side of the type definition. The additional @@ -250,7 +262,7 @@ let rec tr_type_def (tp : Raw.type_expr) args = | TVar ({data = NPName x; _}, _) -> TD_Id(x, args) | TApp(tp1, tp2) -> tr_type_def tp1 (tp2 :: args) | TVar ({data = NPSel _; _}, _) | TWildcard | TParen _ | TArrow _ - | TEffect _ | TRecord _ | TTypeLbl _ -> + | TEffect _ | THandler _ | TRecord _ | TTypeLbl _ -> Error.fatal (Error.desugar_error tp.pos) let tr_ctor_decl (d : Raw.ctor_decl) = diff --git a/src/DblParser/Raw.ml b/src/DblParser/Raw.ml index 9b3f8c43..60704801 100644 --- a/src/DblParser/Raw.ml +++ b/src/DblParser/Raw.ml @@ -120,6 +120,9 @@ and type_expr_data = | TTypeLbl of type_expr (** Label of anonymous type parameter of ADT *) + | THandler of tvar option * type_expr * type_expr * type_expr + (** Handler type: effect binding, capability, input comp, output comp *) + (** Field of record-like type *) and ty_field = (type_expr, type_expr) field_data node diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly index 6cdf778d..d17f0753 100644 --- a/src/DblParser/YaccParser.mly +++ b/src/DblParser/YaccParser.mly @@ -168,8 +168,18 @@ ty_expr_simple | UNDERSCORE { make TWildcard } | SBR_OPN effct SBR_CLS { make ($2).data } | CBR_OPN ty_field_list CBR_CLS { make (TRecord $2) } +| KW_HANDLER effct_bind ty_expr KW_IN ty_expr ARROW2 ty_expr + { make (THandler ($2, $3, $5, $7)) } +| KW_HANDLER effct_bind ty_expr ARROW2 ty_expr + { make (THandler ($2, $3, $5, $5)) } ; +effct_bind +: CBR_OPN UID CBR_CLS { Some $2 } +| /* empty */ { None } +; + + /* ------------------------------------------------------------------------- */ type_annot diff --git a/src/TypeInference/Type.ml b/src/TypeInference/Type.ml index 5543f961..e2ab3c07 100644 --- a/src/TypeInference/Type.ml +++ b/src/TypeInference/Type.ml @@ -50,7 +50,12 @@ let rec infer_kind env (tp : S.type_expr) = | THandler { effct; cap_type; in_type; in_eff; out_type; out_eff } -> let (in_env, _) = Env.enter_scope env in - let (in_env, eff_var) = Env.add_tvar ~pos in_env effct T.Kind.k_effect in + let (in_env, eff_var) = + if String.equal effct "_" then + Env.add_anon_tvar ~pos ~name:"E" in_env T.Kind.k_effect + else + Env.add_tvar ~pos in_env effct T.Kind.k_effect + in let cap_type = tr_ttype in_env cap_type in let in_type = tr_ttype in_env in_type in let in_eff = tr_effect in_env in_eff in From 5e3cf74415f1fe6f8731763e0e6fd5db2934f7e8 Mon Sep 17 00:00:00 2001 From: kumber Date: Sun, 12 Apr 2026 22:37:05 +0200 Subject: [PATCH 2/3] Fix pretty printer, allow wildcard --- src/DblParser/YaccParser.mly | 1 + src/Lang/UnifCommon/Pretty.ml | 43 +++++++++++++++++++++++------------ 2 files changed, 29 insertions(+), 15 deletions(-) diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly index d17f0753..1f3b24a7 100644 --- a/src/DblParser/YaccParser.mly +++ b/src/DblParser/YaccParser.mly @@ -176,6 +176,7 @@ ty_expr_simple effct_bind : CBR_OPN UID CBR_CLS { Some $2 } +| CBR_OPN UNDERSCORE CBR_CLS { None } | /* empty */ { None } ; diff --git a/src/Lang/UnifCommon/Pretty.ml b/src/Lang/UnifCommon/Pretty.ml index 42e50d22..fdac0300 100644 --- a/src/Lang/UnifCommon/Pretty.ml +++ b/src/Lang/UnifCommon/Pretty.ml @@ -354,25 +354,38 @@ let rec print_type env (tp : type_tree) prec = | PP_THandler h -> paren env prec 0 (fun () -> - let name = gen_tvar_name (fun n -> fresh_for_type env n tp) "E" in + let name = + match Env.lookup_tvar env h.eff_var with + | Found name -> name + | Anon(name, _) -> name + | Unbound _ -> gen_tvar_name (fun n -> fresh_for_type env n tp) "E" + in let env1 = Env.add_tvar env name h.eff_var in Env.print_string env "handler "; + Env.print_string env "{"; Env.print_string env name; - Env.print_string env " of "; + Env.print_string env "} "; print_type env1 h.cap_tp 1; - Env.print_string env " with ["; - print_effect_body env1 h.in_eff; - Env.print_string env "] "; - print_type env1 h.in_tp 1; - begin match h.out_eff with - | [ PP_EffWildcard ] -> - Env.print_string env " ->> " - | effs -> - Env.print_string env " ->["; - print_effect_body env effs; - Env.print_string env "] " - end; - print_type env h.out_tp 1) + let print_comp env eff tp = + begin match eff with + | [ PP_EffWildcard ] -> () + | _ -> + Env.print_string env " ["; + print_effect_body env eff; + Env.print_string env "]" + end; + Env.print_string env " "; + print_type env tp 1 + in + if h.in_eff = h.out_eff && h.in_tp = h.out_tp then ( + Env.print_string env " =>"; + print_comp env h.out_eff h.out_tp + ) else ( + Env.print_string env " in"; + print_comp env1 h.in_eff h.in_tp; + Env.print_string env " =>"; + print_comp env h.out_eff h.out_tp + )) | PP_TEffect eff -> print_effect env eff prec From 10fff97e46b08c53af92630bfd320cd76f383797 Mon Sep 17 00:00:00 2001 From: kumber Date: Tue, 21 Apr 2026 21:22:48 +0200 Subject: [PATCH 3/3] Fix THandler type --- src/DblParser/Desugar.ml | 10 ++++++++-- src/Lang/Surface.ml | 2 +- src/TypeInference/Type.ml | 7 +++---- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index 9aebd071..ea542159 100644 --- a/src/DblParser/Desugar.ml +++ b/src/DblParser/Desugar.ml @@ -138,7 +138,6 @@ let rec tr_type_expr (tp : Raw.type_expr) = make (TApp(tr_type_expr tp1, tr_type_expr tp2)) | THandler (effct_opt, cap_tp, in_comp, out_comp) -> let cap_type = tr_type_expr cap_tp in - let effct = Option.value effct_opt ~default:"_" in let in_eff_opt, in_type = tr_eff_type in_comp in let in_eff = Option.value in_eff_opt ~default:(make (TEffect [ make TWildcard ])) @@ -147,7 +146,14 @@ let rec tr_type_expr (tp : Raw.type_expr) = let out_eff = Option.value out_eff_opt ~default:(make (TEffect [ make TWildcard ])) in - make (THandler { effct; cap_type; in_type; in_eff; out_type; out_eff }) + make (THandler { + effct = effct_opt; + cap_type; + in_type; + in_eff; + out_type; + out_eff; + }) | TRecord _ | TTypeLbl _ -> Error.fatal (Error.desugar_error tp.pos) diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml index 2b5abb3c..4d3413c0 100644 --- a/src/Lang/Surface.ml +++ b/src/Lang/Surface.ml @@ -92,7 +92,7 @@ and type_expr_data = (** Effectful function: the last parameter is an effect *) | THandler of (** First-class handler *) - { effct : tvar; + { effct : tvar option; (** Effect variable bound by this handler (it's bound in [cap_type], [in_type], and [in_eff] *) diff --git a/src/TypeInference/Type.ml b/src/TypeInference/Type.ml index e2ab3c07..8ddd92dc 100644 --- a/src/TypeInference/Type.ml +++ b/src/TypeInference/Type.ml @@ -51,10 +51,9 @@ let rec infer_kind env (tp : S.type_expr) = | THandler { effct; cap_type; in_type; in_eff; out_type; out_eff } -> let (in_env, _) = Env.enter_scope env in let (in_env, eff_var) = - if String.equal effct "_" then - Env.add_anon_tvar ~pos ~name:"E" in_env T.Kind.k_effect - else - Env.add_tvar ~pos in_env effct T.Kind.k_effect + match effct with + | Some effct -> Env.add_tvar ~pos in_env effct T.Kind.k_effect + | None -> Env.add_anon_tvar ~pos ~name:"E" in_env T.Kind.k_effect in let cap_type = tr_ttype in_env cap_type in let in_type = tr_ttype in_env in_type in