CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Improve translation of typing upon dcalc -> lcalc

Browse Source 
A little bit of effort enables us to propagate valid typing annotations, making
subsequent typing re-inference easier (and avoiding a traversal just to remove
type annotations)
This commit is contained in:
Louis Gesbert 2024-01-31 18:56:11 +01:00
parent 7a4ac4364b
commit e47a1fc220
8 changed files with 134 additions and 132 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/dcalc/from_scopelang.ml
View File

@ -689,7 +689,7 @@ let translate_rule
| Runtime.Reentrant, pos -> (
match Mark.remove tau with
| TArrow _ -> new_e
| _ -> Expr.thunk_term new_e (Expr.with_pos pos (Mark.get new_e)))
| _ -> Mark.map_mark (Expr.with_pos pos) (Expr.thunk_term new_e))
in
( (fun next ->
Bindlib.box_apply2

95
compiler/lcalc/compile_with_exceptions.ml
View File

@ -41,48 +41,61 @@ let rec translate_typ (tau : typ) : typ =
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2)
end
let translate_mark e = Expr.map_ty translate_typ (Mark.get e)
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
let 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 =
Expr.eappop ~op:Op.HandleDefault
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:
[
Expr.earray exceptions mark_default;
Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr cons) (Mark.get cons);
]
mark_default
List.map (fun except -> Expr.thunk_term (translate_expr except)) exceptions
in
exceptions
Expr.eappop ~op:Op.HandleDefault
~tys:
[
TArray (TArrow ([TLit TUnit, pos], (TAny, pos)), pos), pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], (TAny, pos)), pos;
]
~args:
[
Expr.earray exceptions
(Expr.map_ty
(fun ty -> TArray (TArrow ([TLit TUnit, pos], ty), pos), pos)
mark_default);
Expr.thunk_term (translate_expr just);
Expr.thunk_term (translate_expr cons);
]
mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
let m = Mark.get e in
let m = translate_mark e in
match Mark.remove e with
| EEmptyError -> Expr.eraise EmptyError m
| EErrorOnEmpty arg ->
Expr.ecatch (translate_expr arg) EmptyError
(Expr.eraise NoValueProvided m)
m
| EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e)
| EDefault { excepts; just; cons } -> translate_default excepts just cons m
| EPureDefault e -> translate_expr e
(* As we need to translate types as well as terms, we cannot simply use
[Expr.map] for terms that contains types. *)
| EAbs { binder; tys } ->
let tys = List.map translate_typ tys in
Expr.map ~f:translate_expr (EAbs { binder; tys }, m)
| EApp { f; args; tys } ->
let tys = List.map translate_typ tys in
Expr.map ~f:translate_expr (EApp { f; args; tys }, m)
| EAppOp { op; args; tys } ->
Expr.eappop ~op:(Operator.translate op)
~args:(List.map translate_expr args)
~tys m
| ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
~tys:(List.map translate_typ tys)
m
| ( ELit _ | EArray _ | EVar _ | EExternal _ | EIfThenElse _ | ETuple _
| ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _
| EMatch _ ) as e ->
Expr.map ~f:translate_expr (Mark.add m e)
| _ -> .
@ -125,24 +138,20 @@ let translate_code_items scopes =
in
Scope.map ~f ~varf:Var.translate scopes
let translate_program (prg : typed D.program) : untyped A.program =
Program.untype
@@ Bindlib.unbox
@@ Bindlib.box_apply
(fun code_items ->
let ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map translate_typ)
prg.decl_ctx.ctx_enums
in
let ctx_structs =
StructName.Map.map
(StructField.Map.map translate_typ)
prg.decl_ctx.ctx_structs
in
{
prg with
code_items;
decl_ctx = { prg.decl_ctx with ctx_enums; ctx_structs };
})
(translate_code_items prg.code_items)
let translate_program (prg : 'm D.program) : 'm A.program =
let code_items = Bindlib.unbox (translate_code_items prg.code_items) in
let ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map translate_typ)
prg.decl_ctx.ctx_enums
in
let ctx_structs =
StructName.Map.map
(StructField.Map.map translate_typ)
prg.decl_ctx.ctx_structs
in
{
prg with
code_items;
decl_ctx = { prg.decl_ctx with ctx_enums; ctx_structs };
}

3
compiler/lcalc/compile_with_exceptions.mli
View File

@ -17,5 +17,4 @@
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions to handle empty default terms. *)
val translate_program :
Shared_ast.typed Dcalc.Ast.program -> Shared_ast.untyped Ast.program
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

136
compiler/lcalc/compile_without_exceptions.ml
View File

@ -50,67 +50,69 @@ let rec translate_typ (tau : typ) : typ =
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2)
end
let rec translate_default
(exceptions : typed D.expr list)
(just : typed D.expr)
(cons : typed D.expr)
(mark_default : typed mark) : typed A.expr boxed =
(* Since the program is well typed, all exceptions have as type [option 't] *)
let exceptions = List.map translate_expr exceptions in
let pos = Expr.mark_pos mark_default in
let exceptions_and_cons_ty =
match mark_default with Typed { ty; _ } -> translate_typ ty
in
let exceptions =
Expr.eappop ~op:Op.HandleDefaultOpt
~tys:
[
TArray exceptions_and_cons_ty, pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], exceptions_and_cons_ty), pos;
]
~args:
[
Expr.earray exceptions mark_default;
(* In call-by-value programming languages, as lcalc, arguments are
evalulated before calling the function. Since we don't want to
execute the justification and conclusion while before checking
every exceptions, we need to thunk them. *)
Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr cons) (Mark.get cons);
]
mark_default
in
exceptions
let translate_mark e = Expr.map_ty translate_typ (Mark.get e)
and translate_expr (e : typed D.expr) : typed A.expr boxed =
let mark = Mark.get e in
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
(* Since the program is well typed, all exceptions have as type [option 't] *)
let pos = Expr.mark_pos mark_default in
let exceptions = List.map translate_expr exceptions in
let exceptions_and_cons_ty = Expr.maybe_ty mark_default in
Expr.eappop ~op:Op.HandleDefaultOpt
~tys:
[
TArray exceptions_and_cons_ty, pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], exceptions_and_cons_ty), pos;
]
~args:
[
Expr.earray exceptions
(Expr.map_ty (fun ty -> TArray ty, pos) mark_default);
(* In call-by-value programming languages, as lcalc, arguments are
evalulated before calling the function. Since we don't want to
execute the justification and conclusion while before checking every
exceptions, we need to thunk them. *)
Expr.thunk_term (translate_expr just);
Expr.thunk_term (translate_expr cons);
]
mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
let mark = translate_mark e in
match Mark.remove e with
| EEmptyError ->
Expr.einj ~e:(Expr.elit LUnit mark) ~cons:Expr.none_constr
~name:Expr.option_enum mark
Expr.einj
~e:(Expr.elit LUnit (Expr.with_ty mark (TLit TUnit, Expr.mark_pos mark)))
~cons:Expr.none_constr ~name:Expr.option_enum mark
| EErrorOnEmpty arg ->
let pos = Expr.mark_pos mark in
let cases =
EnumConstructor.Map.of_list
[
( Expr.none_constr,
let x = Var.make "_" in
Expr.eabs
(Expr.bind [| x |] (Expr.eraise NoValueProvided mark))
[TAny, Expr.mark_pos mark]
mark );
Expr.make_abs [| x |]
(Expr.eraise NoValueProvided mark)
[TAny, pos]
(Expr.mark_pos mark) );
(* | None x -> raise NoValueProvided *)
Expr.some_constr, Expr.fun_id ~var_name:"arg" mark (* | Some x -> x*);
Expr.some_constr, Expr.fun_id ~var_name:"arg" mark (* | Some x -> x *);
]
in
Expr.ematch ~e:(translate_expr arg) ~name:Expr.option_enum ~cases mark
| EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e)
| EDefault { excepts; just; cons } -> translate_default excepts just cons mark
| EPureDefault e ->
Expr.einj ~e:(translate_expr e) ~cons:Expr.some_constr
~name:Expr.option_enum mark
(* As we need to translate types as well as terms, we cannot simply use
[Expr.map] for terms that contains types. *)
| EApp { f; args; tys } ->
let tys = List.map translate_typ tys in
Expr.map ~f:translate_expr (EApp { f; args; tys }, mark)
| EAppOp { op; tys; args } ->
Expr.eappop ~op:(Operator.translate op)
~tys:(List.map translate_typ tys)
@ -122,15 +124,15 @@ and translate_expr (e : typed D.expr) : typed A.expr boxed =
let binder = Expr.bind (Array.map Var.translate vars) body in
let tys = List.map translate_typ tys in
Expr.eabs binder tys mark
| ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
| ( ELit _ | EArray _ | EVar _ | EExternal _ | EIfThenElse _ | ETuple _
| ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _
| EMatch _ ) as e ->
Expr.map ~f:translate_expr (Mark.add mark e)
| _ -> .
let translate_scope_body_expr
(scope_body_expr : (dcalc, typed) gexpr scope_body_expr) :
(lcalc, typed) gexpr scope_body_expr Bindlib.box =
(scope_body_expr : (dcalc, 'm) gexpr scope_body_expr) :
(lcalc, 'm) gexpr scope_body_expr Bindlib.box =
Scope.fold_right_lets
~f:(fun scope_let var_next acc ->
Bindlib.box_apply2
@ -168,24 +170,20 @@ let translate_code_items scopes =
in
Scope.map ~f ~varf:Var.translate scopes
let translate_program (prg : typed D.program) : untyped A.program =
Program.untype
@@ Bindlib.unbox
@@ Bindlib.box_apply
(fun code_items ->
let ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map translate_typ)
prg.decl_ctx.ctx_enums
in
let ctx_structs =
StructName.Map.map
(StructField.Map.map translate_typ)
prg.decl_ctx.ctx_structs
in
{
prg with
code_items;
decl_ctx = { prg.decl_ctx with ctx_enums; ctx_structs };
})
(translate_code_items prg.code_items)
let translate_program (prg : 'm D.program) : 'm A.program =
let code_items = Bindlib.unbox (translate_code_items prg.code_items) in
let ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map translate_typ)
prg.decl_ctx.ctx_enums
in
let ctx_structs =
StructName.Map.map
(StructField.Map.map translate_typ)
prg.decl_ctx.ctx_structs
in
{
prg with
code_items;
decl_ctx = { prg.decl_ctx with ctx_enums; ctx_structs };
}

4
compiler/lcalc/compile_without_exceptions.mli
View File

@ -19,6 +19,4 @@
transformation is one piece to permit to compile toward legacy languages
that does not contains exceptions. *)
open Shared_ast
val translate_program : typed Dcalc.Ast.program -> untyped Ast.program
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

7
compiler/lcalc/from_dcalc.mli
View File

@ -14,15 +14,12 @@
License for the specific language governing permissions and limitations under
the License. *)
open Shared_ast
val translate_program_with_exceptions :
typed Dcalc.Ast.program -> untyped Ast.program
val translate_program_with_exceptions : 'm Dcalc.Ast.program -> 'm Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions to handle empty default terms. *)
val translate_program_without_exceptions :
typed Dcalc.Ast.program -> untyped Ast.program
'm Dcalc.Ast.program -> 'm Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses an option monad to handle empty defaults terms. This
transformation is one piece to permit to compile toward legacy languages

15
compiler/shared_ast/expr.ml
View File

@ -188,11 +188,6 @@ let mark_pos (type m) (m : m mark) : Pos.t =
match m with Untyped { pos } | Typed { pos; _ } | Custom { pos; _ } -> pos
let pos (type m) (x : ('a, m) marked) : Pos.t = mark_pos (Mark.get x)
let fun_id ?(var_name : string = "x") mark : ('a any, 'm) boxed_gexpr =
let x = Var.make var_name in
eabs (bind [| x |] (evar x mark)) [TAny, mark_pos mark] mark
let ty (_, m) : typ = match m with Typed { ty; _ } -> ty
let set_ty (type m) (ty : typ) (x : ('a, m) marked) : ('a, typed) marked =
@ -985,12 +980,12 @@ let make_erroronempty e =
in
eerroronempty e mark
let thunk_term term mark =
let thunk_term term =
let silent = Var.make "_" in
let pos = mark_pos mark in
let pos = mark_pos (Mark.get term) in
make_abs [| silent |] term [TLit TUnit, pos] pos
let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark) mark
let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark)
let unthunk_term_nobox term mark =
Mark.add mark
@ -1012,3 +1007,7 @@ let make_puredefault e =
map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e)
in
epuredefault e mark
let fun_id ?(var_name : string = "x") mark : ('a any, 'm) boxed_gexpr =
let x = Var.make var_name in
make_abs [| x |] (evar x mark) [TAny, mark_pos mark] (mark_pos mark)

4
compiler/shared_ast/expr.mli
View File

@ -174,6 +174,8 @@ val ecustom :
(< custom : Definitions.yes ; .. >, 'm) boxed_gexpr
val fun_id : ?var_name:string -> 'm mark -> ('a any, 'm) boxed_gexpr
(** The type of the mark, if typed, is assumed to correspond to the argument
type, not the function type *)
(** {2 Manipulation of marks} *)
@ -342,7 +344,7 @@ val make_erroronempty :
val empty_thunked_term :
'm mark -> (< defaultTerms : yes ; .. >, 'm) boxed_gexpr
val thunk_term : ('a any, 'b) boxed_gexpr -> 'b mark -> ('a, 'b) boxed_gexpr
val thunk_term : ('a any, 'b) boxed_gexpr -> ('a, 'b) boxed_gexpr
val unthunk_term_nobox : ('a any, 'm) gexpr -> 'm mark -> ('a, 'm) gexpr
val make_let_in :