From ccd4a17aaca92c9f9ae0348eb622c6b03fff1edb Mon Sep 17 00:00:00 2001 From: Galfour Date: Sat, 23 Mar 2019 13:47:18 +0000 Subject: [PATCH] pipeline works --- src/ligo/ast_typed.ml | 67 +++++++++++++++++++++++++++++++- src/ligo/contracts/function.ligo | 4 ++ src/ligo/contracts/toto.ligo | 2 - src/ligo/mini_c.ml | 8 ++-- src/ligo/test/test.ml | 11 +++++- src/ligo/transpiler.ml | 22 +++++++---- 6 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 src/ligo/contracts/function.ligo diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index f6319ace0..524df7e52 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -132,6 +132,61 @@ module PP = struct and type_value ppf (tv:type_value) : unit = type_value' ppf tv.type_value + + let rec annotated_expression ppf (ae:annotated_expression) : unit = + match ae.type_annotation.simplified with + | Some _ -> fprintf ppf "%a:%a" expression ae.expression type_value ae.type_annotation + | _ -> expression ppf ae.expression + + and expression ppf (e:expression) : unit = + match e with + | Literal l -> literal ppf l + | Constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep annotated_expression) lst + | Constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst + | Variable a -> fprintf ppf "%s" a + | Application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg + | Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst + | Lambda {binder;input_type;output_type;result;body} -> + fprintf ppf "lambda (%s:%a) : %a {%a} return %a" + binder type_value input_type type_value output_type + block body annotated_expression result + | Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i + | Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s + | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m + + and literal ppf (l:literal) : unit = + match l with + | Unit -> fprintf ppf "unit" + | Bool b -> fprintf ppf "%b" b + | Int n -> fprintf ppf "%d" n + | Nat n -> fprintf ppf "%d" n + | String s -> fprintf ppf "%s" s + | Bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b + + and block ppf (b:block) = (list_sep instruction) ppf b + + and single_record_patch ppf ((s, ae) : string * ae) = + fprintf ppf "%s <- %a" s annotated_expression ae + + and matching ppf (m:matching) = match m with + | Match_tuple (lst, b) -> + fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst block b + | Match_bool {match_true ; match_false} -> + fprintf ppf "| True -> %a @.| False -> %a" block match_true block match_false + | Match_list {match_nil ; match_cons = (hd, tl, match_cons)} -> + fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons + | Match_option {match_none ; match_some = (some, match_some)} -> + fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none some block match_some + + and instruction ppf (i:instruction) = match i with + | Skip -> fprintf ppf "skip" + | Fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae + | Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b + | Assignment {name;annotated_expression = ae} -> + fprintf ppf "%s := %a" name annotated_expression ae + | Matching (ae, m) -> + fprintf ppf "match %a with %a" annotated_expression ae matching m + end @@ -165,16 +220,18 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m @@ Assert.assert_true List.(length ta = length tb) in bind_list_iter assert_type_value_eq (List.combine ta tb) ) + | Type_tuple _, _ -> fail @@ different_kinds a b | Type_constant (ca, lsta), Type_constant (cb, lstb) -> ( let%bind _ = trace_strong (different_size_constants a b) @@ Assert.assert_true List.(length lsta = length lstb) in let%bind _ = trace_strong (different_constants ca cb) - @@ Assert.assert_true (a = b) in + @@ Assert.assert_true (ca = cb) in trace (simple_error "constant sub-expression") @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb) ) + | Type_constant _, _ -> fail @@ different_kinds a b | Type_sum a, Type_sum b -> ( let a' = list_of_smap a in let b' = list_of_smap b in @@ -188,6 +245,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m @@ bind_list_iter aux (List.combine a' b') ) + | Type_sum _, _ -> fail @@ different_kinds a b | Type_record a, Type_record b -> ( let a' = list_of_smap a in let b' = list_of_smap b in @@ -201,7 +259,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m @@ bind_list_iter aux (List.combine a' b') ) - | _ -> fail @@ different_kinds a b + | Type_record _, _ -> fail @@ different_kinds a b + | Type_function (param, result), Type_function (param', result') -> + let%bind _ = assert_type_value_eq (param, param') in + let%bind _ = assert_type_value_eq (result, result') in + ok () + | Type_function _, _ -> fail @@ different_kinds a b (* No information about what made it fail *) let type_value_eq ab = match assert_type_value_eq ab with diff --git a/src/ligo/contracts/function.ligo b/src/ligo/contracts/function.ligo new file mode 100644 index 000000000..8149b2e15 --- /dev/null +++ b/src/ligo/contracts/function.ligo @@ -0,0 +1,4 @@ +function main (const i : int) : int is + begin + skip + end with i diff --git a/src/ligo/contracts/toto.ligo b/src/ligo/contracts/toto.ligo index 84b965857..785655b4a 100644 --- a/src/ligo/contracts/toto.ligo +++ b/src/ligo/contracts/toto.ligo @@ -4,5 +4,3 @@ type toto is record end const foo : int = 3 - - diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 434e39f9f..de49de7c3 100644 --- a/src/ligo/mini_c.ml +++ b/src/ligo/mini_c.ml @@ -175,11 +175,13 @@ module PP = struct | Literal v -> fprintf ppf "%a" value v | Function_expression c -> function_ ppf c - and function_ ppf ({input ; output ; body}:anon_function_content) = - fprintf ppf "fun (%a) : %a %a" + and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) = + fprintf ppf "fun (%s:%a) : %a %a return %a" + binder type_ input type_ output block body + expression result and assignment ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e @@ -852,7 +854,7 @@ module Translate_program = struct let%bind expr = translate_expression result in let code = seq [ body ; - expr ; i_car ; + i_push_unit ; expr ; i_car ; dip i_drop ; ] in diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml index dd5da1b13..57a4b2ccf 100644 --- a/src/ligo/test/test.ml +++ b/src/ligo/test/test.ml @@ -22,15 +22,23 @@ module Ligo = struct let%bind typed = trace (simple_error "typing") @@ type_ simplified in - let%bind _mini_c = + let%bind mini_c = trace (simple_error "transpiling") @@ transpile typed in + Format.printf "mini_c code : %a" Mini_c.PP.program mini_c ; ok () let basic () : unit result = Format.printf "basic test" ; pass "./contracts/toto.ligo" + let function_ () : unit result = + Format.printf "function test" ; + let%bind _ = pass "./contracts/function.ligo" in + let%bind result = easy_run_main "./contracts/function.ligo" "2" in + Format.printf "result : %a" AST_Typed.PP.annotated_expression result ; + ok () + (* let display_basic () : unit result = * parse_file "./contracts/toto.ligo" >>? fun program_ast -> * Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program -> @@ -42,6 +50,7 @@ module Ligo = struct let main = "Ligo", [ test "basic" basic ; + test "function" function_ ; ] end diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 9b9186990..7450356bd 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -14,6 +14,7 @@ let rec translate_type (t:AST.type_value) : type_value result = | Type_constant ("bool", []) -> ok (`Base Bool) | Type_constant ("int", []) -> ok (`Base Int) | Type_constant ("string", []) -> ok (`Base String) + | Type_constant _ -> simple_fail "unrecognized constant" | Type_sum m -> let node = Append_tree.of_list @@ list_of_map m in let aux a b : type_value result = @@ -38,28 +39,35 @@ let rec translate_type (t:AST.type_value) : type_value result = ok (`Pair (a, b)) in Append_tree.fold_ne translate_type aux node - | _ -> simple_fail "todo" + | Type_function (param, result) -> + let%bind param' = translate_type param in + let%bind result' = translate_type result in + ok (`Function (param', result')) let rec translate_block env (b:AST.block) : block result = let env' = Environment.extend env in - let%bind instructions = bind_list @@ List.map (translate_instruction env) b in + let%bind instructionss = bind_list @@ List.map (translate_instruction env) b in + let instructions = List.concat instructionss in ok (instructions, env') -and translate_instruction (env:Environment.t) (i:AST.instruction) : statement result = +and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result = + let return x = ok [x] in match i with | Assignment {name;annotated_expression} -> let%bind expression = translate_annotated_expression env annotated_expression in - ok @@ (Assignment (name, expression), env) + return (Assignment (name, expression), env) | Matching (expr, Match_bool {match_true ; match_false}) -> let%bind expr' = translate_annotated_expression env expr in let%bind true_branch = translate_block env match_true in let%bind false_branch = translate_block env match_false in - ok @@ (Cond (expr', true_branch, false_branch), env) + return (Cond (expr', true_branch, false_branch), env) + | Matching _ -> simple_fail "todo : match" | Loop (expr, body) -> let%bind expr' = translate_annotated_expression env expr in let%bind body' = translate_block env body in - ok @@ (While (expr', body'), env) - | _ -> simple_fail "todo" + return (While (expr', body'), env) + | Skip -> ok [] + | Fail _ -> simple_fail "todo : fail" and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result = let%bind tv = translate_type ae.type_annotation in