From e47a1fc220f3eb773621008891401a43a676304d Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Wed, 31 Jan 2024 18:56:11 +0100 Subject: [PATCH] Improve translation of typing upon dcalc -> lcalc 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) --- compiler/dcalc/from_scopelang.ml | 2 +- compiler/lcalc/compile_with_exceptions.ml | 95 ++++++------ compiler/lcalc/compile_with_exceptions.mli | 3 +- compiler/lcalc/compile_without_exceptions.ml | 136 +++++++++--------- compiler/lcalc/compile_without_exceptions.mli | 4 +- compiler/lcalc/from_dcalc.mli | 7 +- compiler/shared_ast/expr.ml | 15 +- compiler/shared_ast/expr.mli | 4 +- 8 files changed, 134 insertions(+), 132 deletions(-) diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml index ccc26855..6ca82092 100644 --- a/compiler/dcalc/from_scopelang.ml +++ b/compiler/dcalc/from_scopelang.ml @@ -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 diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index f2c92361..24551600 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -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 }; + } diff --git a/compiler/lcalc/compile_with_exceptions.mli b/compiler/lcalc/compile_with_exceptions.mli index 428459c4..da0f4d78 100644 --- a/compiler/lcalc/compile_with_exceptions.mli +++ b/compiler/lcalc/compile_with_exceptions.mli @@ -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 diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 3df72bb8..25c35b11 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -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 }; + } diff --git a/compiler/lcalc/compile_without_exceptions.mli b/compiler/lcalc/compile_without_exceptions.mli index 15b21288..6bb2b18d 100644 --- a/compiler/lcalc/compile_without_exceptions.mli +++ b/compiler/lcalc/compile_without_exceptions.mli @@ -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 diff --git a/compiler/lcalc/from_dcalc.mli b/compiler/lcalc/from_dcalc.mli index 2a99ce1a..fb4ba11b 100644 --- a/compiler/lcalc/from_dcalc.mli +++ b/compiler/lcalc/from_dcalc.mli @@ -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 diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index 1009c1ea..4ca3b23b 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -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) diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 84ffe432..a4c80fd5 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -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 :