From bcf285913e2432972c5b203270913a0df9be72b8 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 7 Nov 2023 17:13:16 +0100 Subject: [PATCH] Typing the HandleDefault operator --- compiler/lcalc/compile_with_exceptions.ml | 12 +- compiler/shared_ast/typing.ml | 18 +- .../good/closure_conversion.catala_en | 9 +- tests/test_func/good/closure_return.catala_en | 12 +- .../good/closure_through_scope.catala_en | 12 +- .../scope_call_func_struct_closure.catala_en | 206 ++++++++++-------- 6 files changed, 145 insertions(+), 124 deletions(-) diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index b0e5ad46..ea9aac90 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -19,12 +19,6 @@ open Shared_ast module D = Dcalc.Ast module A = Ast -let thunk_expr (type m) (e : m A.expr boxed) : m A.expr boxed = - let dummy_var = Var.make "_" in - let pos = Expr.pos e in - let arg_t = Mark.add pos (TLit TUnit) in - Expr.make_abs [| dummy_var |] e [arg_t] pos - let translate_var : 'm D.expr Var.t -> 'm A.expr Var.t = Var.translate let rec translate_default @@ -33,7 +27,7 @@ let rec translate_default (cons : 'm D.expr) (mark_default : 'm mark) : 'm A.expr boxed = let exceptions = - List.map (fun except -> thunk_expr (translate_expr except)) exceptions + List.map (fun except -> Expr.thunk_term (translate_expr except) (Mark.get except)) exceptions in let pos = Expr.mark_pos mark_default in let exceptions = @@ -43,8 +37,8 @@ let rec translate_default (Expr.no_mark mark_default)) [ Expr.earray exceptions mark_default; - thunk_expr (translate_expr just); - thunk_expr (translate_expr cons); + Expr.thunk_term (translate_expr just) (Mark.get just); + Expr.thunk_term (translate_expr cons) (Mark.get cons); ] pos in diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index 98bf340b..dbfc53a4 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -294,7 +294,8 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) : let it = lazy (UnionFind.make (TLit TInt, pos)) in let cet = lazy (UnionFind.make (TClosureEnv, pos)) in let array a = lazy (UnionFind.make (TArray (Lazy.force a), pos)) in - let option a = lazy (UnionFind.make (TOption (Lazy.force a), pos)) in + (* let option a = lazy (UnionFind.make (TOption (Lazy.force a), pos)) in *) + let default a = lazy (UnionFind.make (TDefault (Lazy.force a), pos)) in let ( @-> ) x y = lazy (UnionFind.make (TArrow (List.map Lazy.force x, Lazy.force y), pos)) in @@ -309,10 +310,13 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) : | Log (PosRecordIfTrueBool, _) -> [bt] @-> bt | Log _ -> [any] @-> any | Length -> [array any] @-> it - | HandleDefault -> [array ([ut] @-> any); [ut] @-> bt; [ut] @-> any] @-> any + | HandleDefault -> + [array ([ut] @-> default any); [ut] @-> bt; [ut] @-> any] @-> default any | HandleDefaultOpt -> - [array (option any); [ut] @-> option bt; [ut] @-> option any] - @-> option any + (* FIXME: when translating with avoid_exceptions, defaults morally become options everywhere. However, this is not reflected in the environment at the moment, so this operator may have to mix-and-match options and default terms ; since the typing of default is expected to guide a simplification of the avoid-exceptions backend anyway, this is left untyped at the moment *) + any + (* [array (option any); [ut] @-> option bt; [ut] @-> option any] + * @-> option any *) | ToClosureEnv -> [any] @-> cet | FromClosureEnv -> [cet] @-> any in @@ -710,7 +714,11 @@ and typecheck_expr_top_down : Expr.escopecall ~scope ~args:args' mark | A.ERaise ex -> Expr.eraise ex context_mark | A.ECatch { body; exn; handler } -> - let body' = typecheck_expr_top_down ~leave_unresolved ctx env tau body in + let body' = + typecheck_expr_top_down ~leave_unresolved ctx env + (unionfind (TDefault tau)) + body + in let handler' = typecheck_expr_top_down ~leave_unresolved ctx env tau handler in diff --git a/tests/test_func/good/closure_conversion.catala_en b/tests/test_func/good/closure_conversion.catala_en index c99aff8f..1303bf2d 100644 --- a/tests/test_func/good/closure_conversion.catala_en +++ b/tests/test_func/good/closure_conversion.catala_en @@ -19,7 +19,7 @@ type S_in = { x_in: eoption bool; } type S = { z: eoption integer; } -let topval closure_f : (closure_env, integer) → eoption integer = +let topval closure_f : (closure_env, integer) → eoption any = λ (env: closure_env) (y: integer) → ESome match @@ -35,8 +35,8 @@ let topval closure_f : (closure_env, integer) → eoption integer = | ESome f → f let scope S (S_in: S_in {x_in: eoption bool}): S {z: eoption integer} = let get x : eoption bool = S_in.x_in in - let set f : - eoption ((closure_env, integer) → eoption integer * closure_env) = + let set f : eoption ((closure_env, integer) → eoption any * closure_env) + = ESome (closure_f, to_closure_env (x)) in let set z : eoption integer = @@ -50,8 +50,7 @@ let scope S (S_in: S_in {x_in: eoption bool}): S {z: eoption integer} = | ENone _1 → ENone _1 | ESome f → let code_and_env : - ((closure_env, integer) → eoption integer * closure_env) - = + ((closure_env, integer) → eoption any * closure_env) = f in code_and_env.0 code_and_env.1 -1)) diff --git a/tests/test_func/good/closure_return.catala_en b/tests/test_func/good/closure_return.catala_en index 1d1c9ba4..d92f9f51 100644 --- a/tests/test_func/good/closure_return.catala_en +++ b/tests/test_func/good/closure_return.catala_en @@ -15,11 +15,9 @@ type eoption = | ENone of unit | ESome of any type S_in = { x_in: eoption bool; } -type S = { - f: eoption ((closure_env, integer) → eoption integer * closure_env); - } +type S = { f: eoption ((closure_env, integer) → eoption any * closure_env); } -let topval closure_f : (closure_env, integer) → eoption integer = +let topval closure_f : (closure_env, integer) → eoption any = λ (env: closure_env) (y: integer) → ESome match @@ -35,11 +33,11 @@ let topval closure_f : (closure_env, integer) → eoption integer = | ESome f → f let scope S (S_in: S_in {x_in: eoption bool}) - : S {f: eoption ((closure_env, integer) → eoption integer * closure_env)} + : S {f: eoption ((closure_env, integer) → eoption any * closure_env)} = let get x : eoption bool = S_in.x_in in - let set f : - eoption ((closure_env, integer) → eoption integer * closure_env) = + let set f : eoption ((closure_env, integer) → eoption any * closure_env) + = ESome (closure_f, to_closure_env (x)) in return { S f = f; } diff --git a/tests/test_func/good/closure_through_scope.catala_en b/tests/test_func/good/closure_through_scope.catala_en index f1f90055..b01fec0a 100644 --- a/tests/test_func/good/closure_through_scope.catala_en +++ b/tests/test_func/good/closure_through_scope.catala_en @@ -32,15 +32,12 @@ let scope T (T_in: T_in): T {y: eoption integer} = in let call result : eoption - S { - f: - eoption - ((closure_env, integer) → eoption integer * closure_env) - } = + S {f: eoption ((closure_env, integer) → eoption any * closure_env)} + = ESome S { S_in x_in = ESome s.x; } in let sub_get s.f : - eoption ((closure_env, integer) → eoption integer * closure_env) = + eoption ((closure_env, integer) → eoption any * closure_env) = match result with | ENone _ → ENone _ | ESome result → result.f @@ -56,8 +53,7 @@ let scope T (T_in: T_in): T {y: eoption integer} = | ENone _1 → ENone _1 | ESome s.f → let code_and_env : - ((closure_env, integer) → eoption integer * closure_env) - = + ((closure_env, integer) → eoption any * closure_env) = s.f in code_and_env.0 code_and_env.1 2)) diff --git a/tests/test_func/good/scope_call_func_struct_closure.catala_en b/tests/test_func/good/scope_call_func_struct_closure.catala_en index 3adc805c..23857aa3 100644 --- a/tests/test_func/good/scope_call_func_struct_closure.catala_en +++ b/tests/test_func/good/scope_call_func_struct_closure.catala_en @@ -45,7 +45,7 @@ $ catala Lcalc --avoid_exceptions -O --closure_conversion type eoption = | ENone of unit | ESome of any type Result = { - r: eoption ((closure_env, integer) → eoption integer * closure_env); + r: eoption ((closure_env, integer) → eoption any * closure_env); q: eoption integer; } @@ -53,27 +53,31 @@ type SubFoo1_in = { x_in: eoption integer; } type SubFoo1 = { x: eoption integer; - y: eoption ((closure_env, integer) → eoption integer * closure_env); + y: eoption ((closure_env, integer) → eoption any * closure_env); } type SubFoo2_in = { x1_in: eoption integer; x2_in: eoption integer; } type SubFoo2 = { x1: eoption integer; - y: eoption ((closure_env, integer) → eoption integer * closure_env); + y: eoption ((closure_env, integer) → eoption any * closure_env); } -type Foo_in = { b_in: eoption bool; } +type Foo_in = { b_in: eoption ⟨bool⟩; } type Foo = { z: eoption integer; } -let topval closure_y : (closure_env, integer) → eoption integer = +let topval closure_y : (closure_env, integer) → eoption any = λ (env: closure_env) (z: integer) → ESome match - (match (from_closure_env env).0 with - | ENone _ → ENone _ - | ESome x_0 → ESome (x_0 + z)) + (handle_default_opt + [ ] + (λ (_: unit) → ESome true) + (λ (_: unit) → + match (from_closure_env env).0 with + | ENone _1 → ENone _1 + | ESome x_0 → ESome (x_0 + z))) with | ENone _ → raise NoValueProvided | ESome y → y @@ -81,30 +85,34 @@ let scope SubFoo1 (SubFoo1_in: SubFoo1_in {x_in: eoption integer}) : SubFoo1 { x: eoption integer; - y: eoption ((closure_env, integer) → eoption integer * closure_env) + y: eoption ((closure_env, integer) → eoption any * closure_env) } = let get x : eoption integer = SubFoo1_in.x_in in - let set y : - eoption ((closure_env, integer) → eoption integer * closure_env) = + let set y : eoption ((closure_env, integer) → eoption any * closure_env) + = ESome (closure_y, to_closure_env (x)) in return { SubFoo1 x = x; y = y; } -let topval closure_y : (closure_env, integer) → eoption integer = +let topval closure_y : (closure_env, integer) → eoption any = λ (env: closure_env) (z: integer) → let env1 : (eoption integer * eoption integer) = from_closure_env env in ESome match - (match - (match env1.0 with - | ENone _ → ENone _ - | ESome x1_1 → - match env1.1 with - | ENone _ → ENone _ - | ESome x1_0 → ESome (x1_0 + x1_1)) - with - | ENone _ → ENone _ - | ESome y_0 → ESome (y_0 + z)) + (handle_default_opt + [ ] + (λ (_: unit) → ESome true) + (λ (_: unit) → + match + (match env1.0 with + | ENone _1 → ENone _1 + | ESome x1_1 → + match env1.1 with + | ENone _1 → ENone _1 + | ESome x1_0 → ESome (x1_0 + x1_1)) + with + | ENone _1 → ENone _1 + | ESome y_0 → ESome (y_0 + z))) with | ENone _ → raise NoValueProvided | ESome y → y @@ -112,48 +120,57 @@ let scope SubFoo2 (SubFoo2_in: SubFoo2_in {x1_in: eoption integer; x2_in: eoption integer}) : SubFoo2 { x1: eoption integer; - y: eoption ((closure_env, integer) → eoption integer * closure_env) + y: eoption ((closure_env, integer) → eoption any * closure_env) } = let get x1 : eoption integer = SubFoo2_in.x1_in in let get x2 : eoption integer = SubFoo2_in.x2_in in - let set y : - eoption ((closure_env, integer) → eoption integer * closure_env) = + let set y : eoption ((closure_env, integer) → eoption any * closure_env) + = ESome (closure_y, to_closure_env (x2, x1)) in return { SubFoo2 x1 = x1; y = y; } -let topval closure_r : (closure_env, integer) → eoption integer = +let topval closure_r : (closure_env, integer) → eoption any = λ (env: closure_env) (param0: integer) → match (SubFoo2 { SubFoo2_in x1_in = ESome 10; x2_in = ESome 10; }).y with | ENone _ → ENone _ | ESome result → - let code_and_env : - ((closure_env, integer) → eoption integer * closure_env) = + let code_and_env : ((closure_env, integer) → eoption any * closure_env) + = result in code_and_env.0 code_and_env.1 param0 -let topval closure_r : (closure_env, integer) → eoption integer = +let topval closure_r : (closure_env, integer) → eoption any = λ (env: closure_env) (param0: integer) → match (SubFoo1 { SubFoo1_in x_in = ESome 10; }).y with | ENone _ → ENone _ | ESome result → - let code_and_env : - ((closure_env, integer) → eoption integer * closure_env) = + let code_and_env : ((closure_env, integer) → eoption any * closure_env) + = result in code_and_env.0 code_and_env.1 param0 let scope Foo - (Foo_in: Foo_in {b_in: eoption bool}) + (Foo_in: Foo_in {b_in: eoption ⟨bool⟩}) : Foo {z: eoption integer} = - let get b : eoption bool = Foo_in.b_in in + let get b : eoption ⟨bool⟩ = Foo_in.b_in in let set b : eoption bool = ESome match (handle_default_opt [ b ] (λ (_: unit) → ESome true) - (λ (_: unit) → ESome true)) + (λ (_: unit) → + ESome + match + (handle_default_opt + [ ] + (λ (_1: unit) → ESome true) + (λ (_1: unit) → ESome true)) + with + | ENone _1 → raise NoValueProvided + | ESome b → b)) with | ENone _ → raise NoValueProvided | ESome b → b @@ -161,57 +178,62 @@ let scope Foo let set r : eoption Result { - r: - eoption - ((closure_env, integer) → eoption integer * closure_env); + r: eoption ((closure_env, integer) → eoption any * closure_env); q: eoption integer } = ESome match - (match b with - | ENone _ → ENone _ - | ESome b → - if b then - match - (match (SubFoo1 { SubFoo1_in x_in = ESome 10; }).x with - | ENone _ → ENone _ - | ESome result_0 → - ESome - { SubFoo1 - x = ESome result_0; - y = ESome (closure_r, to_closure_env ()); - }) - with - | ENone _ → ENone _ - | ESome f → - match f.x with - | ENone _ → ENone _ - | ESome f_1 → - match f.y with - | ENone _ → ENone _ - | ESome f_0 → ESome { Result r = ESome f_0; q = ESome f_1; } - else - match - (match - (SubFoo2 { SubFoo2_in x1_in = ESome 10; x2_in = ESome 10; }). - x1 + (handle_default_opt + [ ] + (λ (_: unit) → ESome true) + (λ (_: unit) → + match b with + | ENone _1 → ENone _1 + | ESome b → + if b then + match + (match (SubFoo1 { SubFoo1_in x_in = ESome 10; }).x with + | ENone _1 → ENone _1 + | ESome result_0 → + ESome + { SubFoo1 + x = ESome result_0; + y = ESome (closure_r, to_closure_env ()); + }) with - | ENone _ → ENone _ - | ESome result_0 → - ESome - { SubFoo2 - x1 = ESome result_0; - y = ESome (closure_r, to_closure_env ()); - }) - with - | ENone _ → ENone _ - | ESome f → - match f.x1 with - | ENone _ → ENone _ - | ESome f_1 → - match f.y with - | ENone _ → ENone _ - | ESome f_0 → ESome { Result r = ESome f_0; q = ESome f_1; }) + | ENone _1 → ENone _1 + | ESome f → + match f.x with + | ENone _1 → ENone _1 + | ESome f_1 → + match f.y with + | ENone _1 → ENone _1 + | ESome f_0 → + ESome { Result r = ESome f_0; q = ESome f_1; } + else + match + (match + (SubFoo2 + { SubFoo2_in x1_in = ESome 10; x2_in = ESome 10; }). + x1 + with + | ENone _1 → ENone _1 + | ESome result_0 → + ESome + { SubFoo2 + x1 = ESome result_0; + y = ESome (closure_r, to_closure_env ()); + }) + with + | ENone _1 → ENone _1 + | ESome f → + match f.x1 with + | ENone _1 → ENone _1 + | ESome f_1 → + match f.y with + | ENone _1 → ENone _1 + | ESome f_0 → + ESome { Result r = ESome f_0; q = ESome f_1; })) with | ENone _ → raise NoValueProvided | ESome r → r @@ -219,16 +241,20 @@ let scope Foo let set z : eoption integer = ESome match - (match (match r with - | ENone _ → ENone _ - | ESome r → r.r) with - | ENone _ → ENone _ - | ESome r → - let code_and_env : - ((closure_env, integer) → eoption integer * closure_env) = - r - in - code_and_env.0 code_and_env.1 1) + (handle_default_opt + [ ] + (λ (_: unit) → ESome true) + (λ (_: unit) → + match (match r with + | ENone _1 → ENone _1 + | ESome r → r.r) with + | ENone _1 → ENone _1 + | ESome r → + let code_and_env : + ((closure_env, integer) → eoption any * closure_env) = + r + in + code_and_env.0 code_and_env.1 1)) with | ENone _ → raise NoValueProvided | ESome z → z