mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Typing the HandleDefault operator
This commit is contained in:
Louis Gesbert
parent
fd50e6186f
commit
bcf285913e
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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))
|
||||
|
||||
@ -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; }
|
||||
|
||||
@ -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))
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user