From c773fe61cef9edc973007159384ecb2b562987fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 17 May 2019 19:00:08 +0200 Subject: [PATCH] revert let_in as lambda and add let_in --- src/ast_simplified/PP.ml | 4 +++- src/ast_simplified/combinators.ml | 4 ++-- src/ast_simplified/types.ml | 12 ++++++++++-- src/ast_typed/PP.ml | 2 ++ src/ast_typed/misc.ml | 6 ++++++ src/ast_typed/misc_smart.ml | 1 + src/ast_typed/types.ml | 7 +++++++ src/simplify/camligo.ml | 4 ++-- src/simplify/pascaligo.ml | 8 ++++---- src/transpiler/transpiler.ml | 6 ++---- src/typer/typer.ml | 23 ++++++++++++----------- 11 files changed, 51 insertions(+), 26 deletions(-) diff --git a/src/ast_simplified/PP.ml b/src/ast_simplified/PP.ml index cd7f81d61..9193de818 100644 --- a/src/ast_simplified/PP.ml +++ b/src/ast_simplified/PP.ml @@ -44,12 +44,14 @@ let rec expression ppf (e:expression) = match e with | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind | E_lambda {binder;input_type;output_type;result;body} -> fprintf ppf "lambda (%s:%a) : %a {@; @[%a@]@;} return %a" - binder type_annotation input_type type_annotation output_type + binder type_expression input_type type_expression output_type block body annotated_expression result | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m | E_failwith ae -> fprintf ppf "failwith %a" annotated_expression ae + | E_let_in { binder; rhs; result } -> + fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" annotated_expression a annotated_expression b diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml index c17b457c9..6744722a6 100644 --- a/src/ast_simplified/combinators.ml +++ b/src/ast_simplified/combinators.ml @@ -137,8 +137,8 @@ let e_lambda (binder : string) : expression = E_lambda { binder = (make_name binder) ; - input_type = Some input_type ; - output_type = Some output_type ; + input_type = input_type ; + output_type = output_type ; result = (make_e_a result) ; body ; } diff --git a/src/ast_simplified/types.ml b/src/ast_simplified/types.ml index e09d12e59..f83af618f 100644 --- a/src/ast_simplified/types.ml +++ b/src/ast_simplified/types.ml @@ -1,3 +1,4 @@ +[@@@warning "-30"] module Map = Simple_utils.Map module Location = Simple_utils.Location @@ -47,12 +48,18 @@ and type_expression = and lambda = { binder: name ; - input_type: type_expression option; - output_type: type_expression option; + input_type: type_expression; + output_type: type_expression; result: ae ; body: block ; } +and let_in = { + binder : name; + rhs : ae; + result : ae; +} + and expression = (* Base *) | E_literal of literal @@ -60,6 +67,7 @@ and expression = | E_variable of name | E_lambda of lambda | E_application of (ae * ae) + | E_let_in of let_in (* E_Tuple *) | E_tuple of ae list (* Sum *) diff --git a/src/ast_typed/PP.ml b/src/ast_typed/PP.ml index 35bc1101e..6cc211c93 100644 --- a/src/ast_typed/PP.ml +++ b/src/ast_typed/PP.ml @@ -47,6 +47,8 @@ and expression ppf (e:expression) : unit = | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m | E_failwith ae -> fprintf ppf "failwith %a" annotated_expression ae + | E_let_in { binder; rhs; result } -> + fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result and value ppf v = annotated_expression ppf v diff --git a/src/ast_typed/misc.ml b/src/ast_typed/misc.ml index cb03a38b0..a42f73e0b 100644 --- a/src/ast_typed/misc.ml +++ b/src/ast_typed/misc.ml @@ -59,6 +59,12 @@ module Free_variables = struct | E_look_up (a , b) -> unions @@ List.map self [ a ; b ] | E_matching (a , cs) -> union (self a) (matching_expression b cs) | E_failwith a -> self a + | E_let_in { binder; rhs; result } -> + let b' = union (singleton binder) b in + union + (annotated_expression b' result) + (annotated_expression b' rhs) (* TODO: what about frees ??? *) + and lambda : bindings -> lambda -> bindings = fun b l -> let b' = union (singleton l.binder) b in diff --git a/src/ast_typed/misc_smart.ml b/src/ast_typed/misc_smart.ml index d333705fe..c47440f89 100644 --- a/src/ast_typed/misc_smart.ml +++ b/src/ast_typed/misc_smart.ml @@ -94,6 +94,7 @@ module Captured_variables = struct let%bind cs' = matching_expression b cs in ok @@ union a' cs' | E_failwith a -> self a + | E_let_in { binder; rhs; result } -> ignore (binder, rhs, result); (failwith "TODO") and instruction' : bindings -> instruction -> (bindings * bindings) result = fun b i -> match i with diff --git a/src/ast_typed/types.ml b/src/ast_typed/types.ml index c82abd1c6..cff3c92d4 100644 --- a/src/ast_typed/types.ml +++ b/src/ast_typed/types.ml @@ -75,6 +75,12 @@ and lambda = { body: block ; } +and let_in = { + binder: name; + rhs: ae; + result: ae; +} + and expression = (* Base *) | E_literal of literal @@ -82,6 +88,7 @@ and expression = | E_variable of name | E_application of (ae * ae) | E_lambda of lambda + | E_let_in of let_in (* Tuple *) | E_tuple of ae list | E_tuple_accessor of (ae * int) (* Access n'th tuple's element *) diff --git a/src/simplify/camligo.ml b/src/simplify/camligo.ml index bba10ebc1..7a99abcb4 100644 --- a/src/simplify/camligo.ml +++ b/src/simplify/camligo.ml @@ -461,8 +461,8 @@ let let_entry : _ -> _ result = fun l -> let lambda = O.{ binder = input_nty.type_name ; - input_type = Some input_type'; - output_type = Some output_type'; + input_type = input_type'; + output_type = output_type'; result ; body = tpl_declarations @ body' ; } in diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index ad686959f..be8526b19 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -350,8 +350,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> let%bind result = simpl_expression return in let%bind output_type = simpl_type_expression ret_type in let body = local_declarations @ instructions in - let expression = E_lambda {binder ; input_type = Some input_type; - output_type = Some output_type; result ; body } in + let expression = E_lambda {binder ; input_type = input_type; + output_type = output_type; result ; body } in let type_annotation = Some (T_function (input_type, output_type)) in ok {name;annotated_expression = {expression;type_annotation}} ) @@ -390,8 +390,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> let body = tpl_declarations @ local_declarations @ instructions in let%bind result = simpl_expression return in - let expression = E_lambda {binder ; input_type = Some input_type; - output_type = Some output_type; result ; body } in + let expression = E_lambda {binder ; input_type = input_type; + output_type = output_type; result ; body } in let type_annotation = Some (T_function (input_type, output_type)) in ok {name = name.value;annotated_expression = {expression;type_annotation}} ) diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index 83f3c2772..5396430e8 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -247,12 +247,10 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re let f = translate_annotated_expression in match ae.expression with (* Optimise immediate application as a let-in *) - | E_application ({expression = E_lambda {binder; input_type; output_type=_; body=[]; result}; _}, - rhs) -> - let%bind ty' = translate_type input_type in + | E_let_in {binder; rhs; result} -> let%bind rhs' = translate_annotated_expression rhs in let%bind result' = translate_annotated_expression result in - return (E_let_in ((binder, ty'), rhs', result')) + return (E_let_in ((binder, rhs'.type_value), rhs', result')) | E_failwith ae -> ( let%bind ae' = translate_annotated_expression ae in return @@ E_constant ("FAILWITH" , [ae']) diff --git a/src/typer/typer.ml b/src/typer/typer.ml index 10a146afd..68445bbd8 100644 --- a/src/typer/typer.ml +++ b/src/typer/typer.ml @@ -490,16 +490,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot result ; body ; } -> ( - let%bind input_type = - let%bind input_type = - trace_option (simple_error "missing annotation on input type") - input_type in - evaluate_type e input_type in - let%bind output_type = - let%bind output_type = - trace_option (simple_error "missing annotation of output type") - output_type in - evaluate_type e output_type in + let%bind input_type = evaluate_type e input_type in + let%bind output_type = evaluate_type e output_type in let e' = Environment.add_ez_binder binder input_type e in let%bind (body, e'') = type_block_full e' body in let%bind result = type_annotated_expression e'' result in @@ -571,6 +563,11 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot return (O.E_matching (ex', m')) tv ) ) + | E_let_in {binder; rhs; result} -> + let%bind rhs = type_annotated_expression e rhs in + let e' = Environment.add_ez_binder binder rhs.type_annotation e in + let%bind result = type_annotated_expression e' result in + return (E_let_in {binder; rhs; result}) result.type_annotation and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result = (* Constant poorman's polymorphism *) @@ -645,7 +642,7 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex let%bind output_type = untype_type_value output_type in let%bind result = untype_annotated_expression result in let%bind body = untype_block body in - return (E_lambda {binder;input_type = Some input_type;output_type = Some output_type;body;result}) + return (E_lambda {binder;input_type = input_type;output_type = output_type;body;result}) | E_tuple lst -> let%bind lst' = bind_list @@ List.map untype_annotated_expression lst in @@ -679,6 +676,10 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex | E_failwith ae -> let%bind ae' = untype_annotated_expression ae in return (E_failwith ae') + | E_let_in {binder;rhs;result} -> + let%bind rhs = untype_annotated_expression rhs in + let%bind result = untype_annotated_expression result in + return (E_let_in {binder;rhs;result}) and untype_block (b:O.block) : (I.block) result = bind_list @@ List.map untype_instruction b