From b044a4fbc54d1e355eeb3d3a70d58f56599b0bd3 Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Thu, 16 Apr 2020 17:12:10 +0200 Subject: [PATCH] wip: compiling code that doesn't typecheck --- src/passes/08-typer-old/typer.ml | 4 ++-- src/passes/10-transpiler/transpiler.ml | 6 +++--- src/passes/12-compiler/compiler_program.ml | 7 ++++++- src/stages/5-mini_c/PP.ml | 21 ++++++++++++++++--- src/stages/5-mini_c/PP.mli | 1 + src/stages/5-mini_c/types.ml | 2 +- src/test/contracts/michelson_insertion.mligo | 3 ++- src/test/contracts/michelson_insertion.religo | 2 +- 8 files changed, 34 insertions(+), 12 deletions(-) diff --git a/src/passes/08-typer-old/typer.ml b/src/passes/08-typer-old/typer.ml index c86afc037..43c2e8091 100644 --- a/src/passes/08-typer-old/typer.ml +++ b/src/passes/08-typer-old/typer.ml @@ -938,8 +938,8 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression | E_raw_code {language;code;type_anno} -> let%bind type_anno = evaluate_type e type_anno in - let%bind (_input_type,output_type) = get_t_function type_anno in - return (E_raw_code {language;code;type_anno}) output_type + let%bind (_input_type,_output_type) = get_t_function type_anno in + return (E_raw_code {language;code;type_anno}) type_anno | E_recursive {fun_name; fun_type; lambda} -> let%bind fun_type = evaluate_type e fun_type in let e' = Environment.add_ez_binder fun_name fun_type e in diff --git a/src/passes/10-transpiler/transpiler.ml b/src/passes/10-transpiler/transpiler.ml index 278d8df0a..d335b6914 100644 --- a/src/passes/10-transpiler/transpiler.ml +++ b/src/passes/10-transpiler/transpiler.ml @@ -616,13 +616,13 @@ and transpile_annotated_expression (ae:AST.expression) : expression result = aux expr' tree'' ) ) - | E_raw_code { language; code; _} -> + | E_raw_code { language; code; type_anno} -> let backend = "Michelson" in let%bind () = trace_strong (language_backend_mismatch language backend ae.location) @@ Assert.assert_true (String.equal language backend) in - let code = String.sub code 2 (String.length code - 4) in - return @@ E_raw_michelson code + let%bind type_anno' = transpile_type type_anno in + return @@ E_raw_michelson (code, type_anno') and transpile_lambda l (input_type , output_type) = let { binder ; result } : AST.lambda = l in diff --git a/src/passes/12-compiler/compiler_program.ml b/src/passes/12-compiler/compiler_program.ml index 90042c7b3..b3630bccb 100644 --- a/src/passes/12-compiler/compiler_program.ml +++ b/src/passes/12-compiler/compiler_program.ml @@ -483,7 +483,12 @@ and translate_expression (expr:expression) (env:environment) : michelson result i_push_unit ; ] ) - | E_raw_michelson code -> return @@ Michelson.string code + | E_raw_michelson (code, type_anno) -> + let (code, _e) = Michelson_parser.V1.parse_expression ~check:false code in + let code = Tezos_micheline.Micheline.root code.expanded in + let annot = Format.asprintf "(%a)" Mini_c.PP.type_value type_anno in + + return @@ Michelson.prim ~children:[code] ~annot:[annot] I_PUSH and translate_function_body ({body ; binder} : anon_function) lst input : michelson result = let pre_env = Environment.of_list lst in diff --git a/src/stages/5-mini_c/PP.ml b/src/stages/5-mini_c/PP.ml index 54f98371d..e9aa005f9 100644 --- a/src/stages/5-mini_c/PP.ml +++ b/src/stages/5-mini_c/PP.ml @@ -47,7 +47,7 @@ and type_constant ppf (tb:type_base) : unit = | TB_chain_id -> "chain_id" | TB_void -> "void" in - fprintf ppf "(TC %s)" s + fprintf ppf "%s" s let rec value ppf : value -> unit = function | D_bool b -> fprintf ppf "%b" b @@ -70,6 +70,21 @@ let rec value ppf : value -> unit = function | D_list lst -> fprintf ppf "List[%a]" (list_sep_d value) lst | D_set lst -> fprintf ppf "Set[%a]" (list_sep_d value) lst +and type_value_annotated ppf : type_value annotated -> unit = fun (_, tv) -> + type_value ppf tv + +and type_value ppf : type_value -> unit = function + | T_pair (a,b) -> fprintf ppf "pair %a %a" type_value_annotated a type_value_annotated b + | T_or (a,b) -> fprintf ppf "or %a %a" type_value_annotated a type_value_annotated b + | T_function (a, b) -> fprintf ppf "lambda (%a) %a" type_value a type_value b + | T_base tc -> fprintf ppf "%a" type_constant tc + | T_map (k,v) -> fprintf ppf "Map (%a,%a)" type_value k type_value v + | T_big_map (k,v) -> fprintf ppf "BigMap (%a,%a)" type_value k type_value v + | T_list e -> fprintf ppf "List (%a)" type_value e + | T_set e -> fprintf ppf "Set (%a)" type_value e + | T_contract c -> fprintf ppf "Contract (%a)" type_value c + | T_option c -> fprintf ppf "Option (%a)" type_value c + and value_assoc ppf : (value * value) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" value a value b @@ -110,8 +125,8 @@ and expression_content ppf (e:expression_content) = match e with fprintf ppf "@[{ %a@;<1 2>with@;<1 2>{ %a = %a } }@]" expression r (list_sep lr (const ".")) path expression update | E_while (e , b) -> fprintf ppf "@[while %a do %a@]" expression e expression b - | E_raw_michelson code -> - fprintf ppf "{%s}" code + | E_raw_michelson (code, _) -> + fprintf ppf "%s" code and expression_with_type : _ -> expression -> _ = fun ppf e -> fprintf ppf "%a : %a" diff --git a/src/stages/5-mini_c/PP.mli b/src/stages/5-mini_c/PP.mli index 43db6fb4c..d4510b271 100644 --- a/src/stages/5-mini_c/PP.mli +++ b/src/stages/5-mini_c/PP.mli @@ -12,6 +12,7 @@ val type_variable : formatter -> type_expression -> unit val environment_element : formatter -> environment_element -> unit val environment : formatter -> environment -> unit val value : formatter -> value -> unit +val type_value : formatter -> type_value -> unit (* val value_assoc : formatter -> (value * value) -> unit diff --git a/src/stages/5-mini_c/types.ml b/src/stages/5-mini_c/types.ml index 81c2186b4..a3a5b22bf 100644 --- a/src/stages/5-mini_c/types.ml +++ b/src/stages/5-mini_c/types.ml @@ -91,7 +91,7 @@ and expression_content = | E_sequence of (expression * expression) | E_record_update of (expression * [`Left | `Right] list * expression) | E_while of (expression * expression) - | E_raw_michelson of string + | E_raw_michelson of (string * type_value) and expression = { content : expression_content ; diff --git a/src/test/contracts/michelson_insertion.mligo b/src/test/contracts/michelson_insertion.mligo index 4ab073888..17ee7a64f 100644 --- a/src/test/contracts/michelson_insertion.mligo +++ b/src/test/contracts/michelson_insertion.mligo @@ -1,4 +1,5 @@ // Test michelson insertion in CameLIGO let michelson_add (n : nat) : nat = - [%Michelson {| DUP;ADD; PUSH "hello" |} : nat -> nat ] + let f : nat -> nat = [%Michelson {| DUP;ADD |}] in + f n diff --git a/src/test/contracts/michelson_insertion.religo b/src/test/contracts/michelson_insertion.religo index b397e1934..138b58a6d 100644 --- a/src/test/contracts/michelson_insertion.religo +++ b/src/test/contracts/michelson_insertion.religo @@ -1,4 +1,4 @@ // Test michelson insertion in ReasonLIGO let michelson_add = (n : nat) : nat => - [%Michelson {| DUP;ADD; PUSH "hello" |} : nat => nat ] + [%Michelson {| DUP;ADD |} : nat => nat ]