From 66974949b2282e40158d1210a0c0f16bb2a1ab49 Mon Sep 17 00:00:00 2001 From: Galfour Date: Thu, 21 Mar 2019 21:37:44 +0000 Subject: [PATCH] first working example of the whole pipeline --- .gitignore | 2 +- src/ligo/ast_simplified.ml | 218 +++++++++++++++++++++++++++++++-- src/ligo/ast_typed.ml | 58 +++++++-- src/ligo/contracts/toto.ligo | 8 ++ src/ligo/dune | 7 ++ src/ligo/ligo-helpers/PP.ml | 12 ++ src/ligo/ligo-helpers/trace.ml | 8 +- src/ligo/ligo.ml | 4 +- src/ligo/test/test.ml | 166 ++++--------------------- src/ligo/transpiler.ml | 5 + src/ligo/typer.ml | 55 ++++++++- 11 files changed, 369 insertions(+), 174 deletions(-) create mode 100644 src/ligo/contracts/toto.ligo create mode 100644 src/ligo/ligo-helpers/PP.ml diff --git a/.gitignore b/.gitignore index ed56e0546..0bdd47e8a 100644 --- a/.gitignore +++ b/.gitignore @@ -6,7 +6,7 @@ __pycache__ *.pyc /_build -*/_build +**/_build /_opam /_docker_build /docs/_build diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 4af3fab57..587a0ed3c 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -81,6 +81,7 @@ and instruction = | Loop of ae * b | Skip | Fail of ae + | Record_patch of ae * (string * ae) list and matching = | Match_bool of { @@ -106,22 +107,38 @@ module Simplify = struct let nseq_to_list (hd, tl) = hd :: tl let npseq_to_list (hd, tl) = hd :: (List.map snd tl) + let npseq_to_nelist (hd, tl) = hd, (List.map snd tl) + let pseq_to_list = function + | None -> [] + | Some lst -> npseq_to_list lst + + let type_constants = [ + ("nat", 0) ; + ("int", 0) ; + ] let rec simpl_type_expression (t:Raw.type_expr) : type_expression result = match t with | TPar x -> simpl_type_expression x.value.inside - | TAlias v -> ok @@ Type_variable v.value + | TAlias v -> ( + match List.assoc_opt v.value type_constants with + | Some 0 -> ok @@ Type_constant (v.value, []) + | Some _ -> simple_fail "type constructor with wrong number of args" + | None -> ok @@ Type_variable v.value + ) | TApp x -> let (name, tuple) = x.value in - let%bind lst = bind_list - @@ List.map simpl_type_expression - @@ npseq_to_list tuple.value.inside in - ok @@ Type_constant (name.value, lst) + let lst = npseq_to_list tuple.value.inside in + let%bind _ = match List.assoc_opt name.value type_constants with + | Some n when n = List.length lst -> ok () + | Some _ -> simple_fail "type constructor with wrong number of args" + | None -> simple_fail "unrecognized type constants" in + let%bind lst' = bind_list @@ List.map simpl_type_expression lst in + ok @@ Type_constant (name.value, lst') | TProd p -> - let%bind lst = bind_list - @@ List.map simpl_type_expression + let%bind tpl = simpl_list_type_expression @@ npseq_to_list p.value in - ok @@ Type_tuple lst + ok tpl | TRecord r -> let aux = fun (x, y) -> let%bind y = simpl_type_expression y in ok (x, y) in let%bind lst = bind_list @@ -161,16 +178,32 @@ module Simplify = struct ok @@ ae @@ Application (ae @@ Variable f, arg) | EPar x -> simpl_expression x.value.inside | EUnit _ -> ok @@ ae @@ Literal Unit - | EBytes x -> ok @@ ae @@ Literal (Bytes (fst x.value)) + | EBytes x -> ok @@ ae @@ Literal (Bytes (Bytes.of_string @@ fst x.value)) | ETuple tpl -> simpl_list_expression @@ npseq_to_list tpl.value.inside + | ERecord (RecordInj r) -> + let%bind fields = bind_list + @@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v)) + @@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr)) + @@ npseq_to_list r.value.fields in + let aux prev (k, v) = SMap.add k v prev in + ok @@ ae @@ Record (List.fold_left aux SMap.empty fields) + | ERecord (RecordProj p) -> + let record = p.value.record_name.value in + let lst = List.map (fun (x:_ Raw.reg) -> x.value) @@ npseq_to_list p.value.field_path in + let aux prev cur = + ae @@ Record_accessor (prev, cur) + in + let init = ae @@ Variable record in + ok @@ List.fold_left aux init lst | EConstr (ConstrApp c) -> let (c, args) = c.value in let%bind arg = simpl_list_expression @@ npseq_to_list args.value.inside in ok @@ ae @@ Constructor (c.value, arg) + | EConstr _ -> simple_fail "econstr: not supported yet" | EArith (Add c) -> let%bind (a, b) = simpl_binop c.value in ok @@ ae @@ Constant ("ADD", [a;b]) @@ -181,7 +214,15 @@ module Simplify = struct | EString (String s) -> ok @@ ae @@ Literal (String s.value) | EString _ -> simple_fail "string: not supported yet" - | _ -> simple_fail "todo" + | ELogic (BoolExpr (False _)) -> + ok @@ ae @@ Literal (Bool false) + | ELogic (BoolExpr (True _)) -> + ok @@ ae @@ Literal (Bool true) + | ELogic _ -> simple_fail "logic: not supported yet" + | EList _ -> simple_fail "list: not supported yet" + | ESet _ -> simple_fail "set: not supported yet" + | EMap _ -> simple_fail "map: not supported yet" + and simpl_binop (t:_ Raw.bin_op) : (ae * ae) result = let%bind a = simpl_expression t.arg1 in @@ -196,7 +237,36 @@ module Simplify = struct let%bind lst = bind_list @@ List.map simpl_expression lst in ok @@ ae @@ Tuple lst - and simpl_lambda (t:Raw.lambda_decl) : lambda result = simple_fail "todo" + and simpl_local_declaration (t:Raw.local_decl) : instruction result = + match t with + | LocalVar x -> + let x = x.value in + let name = x.name.value in + let%bind t = simpl_type_expression x.var_type in + let type_annotation = Some t in + let%bind expression = simpl_expression x.init in + ok @@ Assignment {name;annotated_expression={expression with type_annotation}} + | LocalConst x -> + let x = x.value in + let name = x.name.value in + let%bind t = simpl_type_expression x.const_type in + let type_annotation = Some t in + let%bind expression = simpl_expression x.init in + ok @@ Assignment {name;annotated_expression={expression with type_annotation}} + | _ -> simple_fail "todo" + + and simpl_param (t:Raw.param_decl) : named_type_expression result = + match t with + | ParamConst c -> + let c = c.value in + let type_name = c.var.value in + let%bind type_expression = simpl_type_expression c.param_type in + ok { type_name ; type_expression } + | ParamVar v -> + let c = v.value in + let type_name = c.var.value in + let%bind type_expression = simpl_type_expression c.param_type in + ok { type_name ; type_expression } and simpl_declaration (t:Raw.declaration) : declaration result = let open! Raw in @@ -213,8 +283,130 @@ module Simplify = struct ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}} | LambdaDecl (FunDecl x) -> let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in - simple_fail "todo" - | _ -> simple_fail "todo" + let%bind param = match npseq_to_list param.value.inside with + | [a] -> ok a + | _ -> simple_fail "only one param allowed" in + let%bind input = simpl_param param in + let name = name.value in + let binder = input.type_name in + let input_type = input.type_expression in + let%bind local_declarations = bind_list @@ List.map simpl_local_declaration local_decls in + let%bind instructions = bind_list + @@ List.map simpl_instruction + @@ npseq_to_list block.value.instr in + 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 = Lambda {binder ; input_type ; output_type ; result ; body } in + let type_annotation = Some (Type_function (input_type, output_type)) in + ok @@ Constant_declaration {name;annotated_expression = {expression;type_annotation}} + | LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet" + | LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet" + + + and simpl_single_instruction (t:Raw.single_instr) : instruction result = + match t with + | ProcCall _ -> simple_fail "no proc call" + | Fail e -> + let%bind expr = simpl_expression e.value.fail_expr in + ok @@ Fail expr + | Skip _ -> ok @@ Skip + | Loop (While l) -> + let l = l.value in + let%bind cond = simpl_expression l.cond in + let%bind body = simpl_block l.block.value in + ok @@ Loop (cond, body) + | Loop (For _) -> + simple_fail "no for yet" + | Cond c -> + let c = c.value in + let%bind expr = simpl_expression c.test in + let%bind match_true = simpl_instruction_block c.ifso in + let%bind match_false = simpl_instruction_block c.ifnot in + ok @@ Matching (expr, (Match_bool {match_true; match_false})) + | Assign a -> + let a = a.value in + let%bind name = match a.lhs with + | Path (Name v) -> ok v.value + | _ -> simple_fail "no complex assignments yet" + in + let%bind annotated_expression = match a.rhs with + | Expr e -> simpl_expression e + | _ -> simple_fail "no weird assignments yet" + in + ok @@ Assignment {name ; annotated_expression} + | Case c -> + let c = c.value in + let%bind expr = simpl_expression c.expr in + let%bind cases = bind_list + @@ List.map (fun (x:Raw.case) -> let%bind i = simpl_instruction_block x.instr in ok (x.pattern, i)) + @@ List.map (fun (x:_ Raw.reg) -> x.value) + @@ npseq_to_list c.cases.value in + let%bind m = simpl_cases cases in + ok @@ Matching (expr, m) + | RecordPatch r -> + let r = r.value in + let%bind record = match r.path with + | Name v -> ok v.value + | _ -> simple_fail "no complex assignments yet" + in + let%bind inj = bind_list + @@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e)) + @@ List.map (fun (x:_ Raw.reg) -> x.value) + @@ npseq_to_list r.record_inj.value.fields in + ok @@ Record_patch ({expression=Variable record;type_annotation=None}, inj) + | MapPatch _ -> simple_fail "no map patch yet" + + and simpl_cases (t:(Raw.pattern * block) list) : matching result = + let open Raw in + let get_var (t:Raw.pattern) = match t with + | PVar v -> ok v.value + | _ -> simple_fail "not a var" + in + match t with + | [(PFalse _, f) ; (PTrue _, t)] + | [(PTrue _, f) ; (PFalse _, t)] -> ok @@ Match_bool {match_true = t ; match_false = f} + | [(PSome v, some) ; (PNone _, none)] + | [(PNone _, none) ; (PSome v, some)] -> ( + let (_, v) = v.value in + let%bind v = match v.value.inside with + | PVar v -> ok v.value + | _ -> simple_fail "complex patterns not supported yet" in + ok @@ Match_option {match_none = none ; match_some = (v, some) } + ) + | [(PCons c, cons) ; (PList n, nil)] + | [(PList n, nil) ; (PCons c, cons)] -> + let%bind _ = match n with + | Sugar c -> ( + match pseq_to_list c.value.inside with + | [] -> ok () + | _ -> simple_fail "complex patterns not supported yet" + ) + | Raw _ -> simple_fail "complex patterns not supported yet" + in + let%bind (a, b) = + match c.value with + | a, [(_, b)] -> + let%bind a = get_var a in + let%bind b = get_var b in + ok (a, b) + | _ -> simple_fail "complex patterns not supported yet" + in + ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil} + | _ -> simple_fail "complex patterns not supported yet" + + and simpl_instruction_block (t:Raw.instruction) : block result = + match t with + | Single s -> let%bind i = simpl_single_instruction s in ok [ i ] + | Block b -> simpl_block b.value + + and simpl_instruction (t:Raw.instruction) : instruction result = + match t with + | Single s -> simpl_single_instruction s + | Block _ -> simple_fail "no block instruction yet" + + and simpl_block (t:Raw.block) : block result = + bind_list @@ List.map simpl_instruction (npseq_to_list t.instr) let simpl_program (t:Raw.ast) : program result = bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index 5a5397c56..84dd88845 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -42,6 +42,7 @@ and expression = | Literal of literal | Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *) | Variable of name + | Application of ae * ae | Lambda of { binder: name ; input_type: tv ; @@ -60,6 +61,7 @@ and expression = and literal = + | Unit | Bool of bool | Int of int | Nat of int @@ -91,22 +93,59 @@ and matching = } | Match_tuple of (name * b) list +module PP = struct + open Format + open Ligo_helpers.PP + + let rec type_value ppf (tv:type_value) : unit = + match tv with + | Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst + | Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m + | Type_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m + | Type_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b + | Type_constant (c, []) -> fprintf ppf "%s" c + | Type_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n +end + open Ligo_helpers.Trace +module Errors = struct + let different_kinds a b = + let title = "different kinds" in + let full = Format.asprintf "(%a) VS (%a)" PP.type_value a PP.type_value b in + error title full + + let different_constants a b = + let title = "different constants" in + let full = Format.asprintf "%s VS %s" a b in + error title full + + let different_size_constants a b = + let title = "constants have different sizes" in + let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in + error title full + + let different_size_tuples a b = + let title = "tuple have different sizes" in + let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in + error title full +end +open Errors + let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab with - | Type_tuple a, Type_tuple b -> ( + | Type_tuple a as ta, (Type_tuple b as tb) -> ( let%bind _ = - Assert.assert_true ~msg:"tuples with different sizes" - @@ List.(length a = length b) in + trace_strong (different_size_tuples ta tb) + @@ Assert.assert_true List.(length a = length b) in bind_list_iter type_value_eq (List.combine a b) ) - | Type_constant (a, a'), Type_constant (b, b') -> ( + | Type_constant (a, a') as ca, (Type_constant (b, b') as cb) -> ( let%bind _ = - Assert.assert_true ~msg:"constants with different sizes" - @@ List.(length a' = length b') in + trace_strong (different_size_constants ca cb) + @@ Assert.assert_true List.(length a' = length b') in let%bind _ = - Assert.assert_true ~msg:"constants with different names" - @@ (a = b) in + trace_strong (different_constants a b) + @@ Assert.assert_true (a = b) in trace (simple_error "constant sub-expression") @@ bind_list_iter type_value_eq (List.combine a' b') ) @@ -136,7 +175,7 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w @@ bind_list_iter aux (List.combine a' b') ) - | _ -> simple_fail "Different kinds of types" + | a, b -> fail @@ different_kinds a b let merge_annotation (a:type_value option) (b:type_value option) : type_value result = match a, b with @@ -151,6 +190,7 @@ let t_bool : type_value = Type_constant ("bool", []) let t_string : type_value = Type_constant ("string", []) let t_bytes : type_value = Type_constant ("bytes", []) let t_int : type_value = Type_constant ("int", []) +let t_unit : type_value = Type_constant ("unit", []) let get_annotation (x:annotated_expression) = x.type_annotation diff --git a/src/ligo/contracts/toto.ligo b/src/ligo/contracts/toto.ligo new file mode 100644 index 000000000..84b965857 --- /dev/null +++ b/src/ligo/contracts/toto.ligo @@ -0,0 +1,8 @@ +type toto is record + a : nat ; + b : nat +end + +const foo : int = 3 + + diff --git a/src/ligo/dune b/src/ligo/dune index e96ee8c92..df889af1b 100644 --- a/src/ligo/dune +++ b/src/ligo/dune @@ -13,3 +13,10 @@ ) (flags (:standard -w +1..62-4-9-44-40-42-48@39@33 )) ) + +(alias + (name runtest) + (action (run test/test.exe)) + (deps (glob_files contracts/*)) + +) diff --git a/src/ligo/ligo-helpers/PP.ml b/src/ligo/ligo-helpers/PP.ml new file mode 100644 index 000000000..15252672a --- /dev/null +++ b/src/ligo/ligo-helpers/PP.ml @@ -0,0 +1,12 @@ +open Format +module SMap = X_map.String + +let const s ppf () = pp_print_string ppf s + +let list_sep pp = pp_print_list ~pp_sep:(const " ; ") pp +let pair_sep pp ppf (a, b) = fprintf ppf "(%a, %a)" pp a pp b +let smap_sep pp ppf m = + let aux k v prev = (k, v) :: prev in + let new_pp ppf (k, v) = fprintf ppf "%s -> %a" k pp v in + let lst = List.rev @@ SMap.fold aux m [] in + fprintf ppf "%a" (list_sep new_pp) lst diff --git a/src/ligo/ligo-helpers/trace.ml b/src/ligo/ligo-helpers/trace.ml index 8fefe7910..47485c223 100644 --- a/src/ligo/ligo-helpers/trace.ml +++ b/src/ligo/ligo-helpers/trace.ml @@ -34,6 +34,10 @@ module Let_syntax = struct let bind m ~f = m >>? f end +let trace_strong err = function + | Ok _ as o -> o + | Errors _ -> Errors [err] + let trace err = function | Ok _ as o -> o | Errors errs -> Errors (err :: errs) @@ -151,9 +155,9 @@ let pp_to_string pp () x = let errors_to_string = pp_to_string errors_pp module Assert = struct - let assert_true ~msg = function + let assert_true ?msg = function | true -> ok () - | false -> simple_fail msg + | false -> simple_fail @@ Option.unopt ~default:"not true" msg let assert_equal_int ?msg a b = let msg = Option.unopt ~default:"not equal int" msg in diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml index 385b61c52..91186eac6 100644 --- a/src/ligo/ligo.ml +++ b/src/ligo/ligo.ml @@ -48,8 +48,8 @@ let parse (s:string) : AST_Raw.t result = ok program_cst -let abstract (p:AST_Raw.t) : AST_Simplified.program result = AST_Simplified.Simplify.program p +let simplify (p:AST_Raw.t) : Ast_simplified.program result = AST_Simplified.Simplify.simpl_program p -let annotate_types (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p +let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p let transpile (p:AST_Typed.program) : Mini_c.program result = Transpiler.translate_program p diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml index 48a0304bb..dd5da1b13 100644 --- a/src/ligo/test/test.ml +++ b/src/ligo/test/test.ml @@ -11,159 +11,43 @@ let test name f = Format.printf "Errors : {\n%a}\n%!" errors_pp errs ; raise Alcotest.Test_error -open Mini_c -open Combinators - -module Mini_c = struct - - let simple_int_program body : program = [ - Fun("main", function_int body) - ] - - let run_int program n = - Run.run program (`Int n) >>? function - | `Int n -> ok n - | _ -> simple_fail "run_int : output not int" - - let neg () = - let program : program = simple_int_program [ - assign_variable "output" @@ neg_int (var_int "input") ; - assign_variable "output" @@ neg_int (var_int "output") ; - assign_variable "output" @@ neg_int (var_int "output") ; - ] in - run_int program 42 >>? fun output -> - Assert.assert_equal_int (-42) output >>? fun () -> - ok () - - let multiple_variables () = - let program = simple_int_program [ - assign_variable "a" @@ neg_int (var_int "input") ; - assign_variable "b" @@ neg_int (var_int "a") ; - assign_variable "c" @@ neg_int (var_int "b") ; - assign_variable "d" @@ neg_int (var_int "c") ; - assign_variable "output" @@ neg_int (var_int "d") ; - ] in - run_int program 42 >>? fun output -> - Assert.assert_equal_int (-42) output >>? fun () -> - ok () - - let arithmetic () = - let expression = add_int (var_int "input") (neg_int (var_int "input")) in - let program = simple_int_program [ - Assignment (Variable ("a", expression)) ; - Assignment (Variable ("b", var_int "a")) ; - Assignment (Variable ("output", var_int "b")) ; - ] in - let test n = - run_int program n >>? fun output -> - Assert.assert_equal_int 0 output >>? fun () -> - ok () - in - let%bind _assert = bind_list @@ List.map test [42 ; 150 ; 0 ; -42] in - ok () - - let quote_ () = - let program = simple_int_program [ - assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "input") (int 42)] ; - assign_function "g" @@ function_int [assign_variable "output" @@ neg_int (var_int "input")] ; - assign_variable "output" @@ apply_int (type_f_int @@ var "g") @@ apply_int (type_f_int @@ var "f") (var_int "input") ; - ] in - let%bind output = run_int program 42 in - let%bind _ = Assert.assert_equal_int (-84) output in - ok () - - let function_ () = - let program = simple_int_program [ - assign_variable "a" @@ int 42 ; - assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "input") (var_int "a")] ; - let env = Environment.Small.of_list ["a", t_int] in - assign_variable "output" @@ apply_int (type_closure_int env @@ var "f") (var_int "input") ; - ] in - let%bind output = run_int program 100 in - let%bind _ = Assert.assert_equal_int 142 output in - ok () - - let functions_ () = - let program = simple_int_program [ - assign_variable "a" @@ int 42 ; - assign_variable "b" @@ int 144 ; - assign_function "f" @@ function_int [ - assign_variable "output" @@ add_int (var_int "input") (var_int "a") - ] ; - assign_function "g" @@ function_int [ - assign_variable "output" @@ add_int (var_int "input") (var_int "b") - ] ; - let env_f = Environment.Small.of_list ["a", t_int] in - let env_g = Environment.Small.of_list ["b", t_int] in - assign_variable "output" @@ add_int - (apply_int (type_closure_int env_f @@ var "f") (var_int "input")) - (apply_int (type_closure_int env_g @@ var "g") (var_int "input")) - ] in - let%bind output = run_int program 100 in - let%bind _ = Assert.assert_equal_int 386 output in - ok () - - let rich_function () = - let program = simple_int_program [ - assign_variable "a" @@ int 42 ; - assign_variable "b" @@ int 144 ; - assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "a") (var_int "b")] ; - let env = Environment.Small.of_list [("a", t_int) ; ("b", t_int)] in - assign_variable "output" @@ apply_int (type_closure_int env @@ var "f") (var_int "input") ; - ] in - let test n = - let%bind output = run_int program n in - let%bind _ = Assert.assert_equal_int 186 output in - ok () in - let%bind _assert = bind_list @@ List.map test [42 ; 150 ; 0 ; -42] in - ok () - - let main = "Mini_c", [ - test "basic.neg" neg ; - test "basic.variables" multiple_variables ; - test "basic.arithmetic" arithmetic ; - test "basic.quote" quote_ ; - test "basic.function" function_ ; - test "basic.functions" functions_ ; - test "basic.rich_function" rich_function ; - ] -end - module Ligo = struct - let run (source:string) (input:Ligo.Typed.O.value) : Ligo.Typed.Value.value result = - parse_file source >>? fun program_ast -> - Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program -> - Ligo.Run.run typed_program input >>? fun output -> - ok output - - let assert_value_int : Ligo.Typed.Value.value -> int result = function - | `Constant (`Int n) -> ok n - | _ -> simple_fail "not an int" + let pass (source:string) : unit result = + let%bind raw = + trace (simple_error "parsing") @@ + parse_file source in + let%bind simplified = + trace (simple_error "simplifying") @@ + simplify raw in + let%bind typed = + trace (simple_error "typing") @@ + type_ simplified in + let%bind _mini_c = + trace (simple_error "transpiling") @@ + transpile typed in + ok () let basic () : unit result = - run "./contracts/toto.ligo" (Ligo.Typed.Value.int 42) >>? fun output -> - assert_value_int output >>? fun output -> - Assert.assert_equal_int 42 output >>? fun () -> - ok () + Format.printf "basic test" ; + pass "./contracts/toto.ligo" - let display_basic () : unit result = - parse_file "./contracts/toto.ligo" >>? fun program_ast -> - Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program -> - Ligo.Transpile.program_to_michelson typed_program >>? fun node -> - let node = Tezos_utils.Cast.flatten_node node in - let str = Tezos_utils.Cast.node_to_string node in - Format.printf "Program:\n%s\n%!" str ; - ok () + (* let display_basic () : unit result = + * parse_file "./contracts/toto.ligo" >>? fun program_ast -> + * Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program -> + * Ligo.Transpile.program_to_michelson typed_program >>? fun node -> + * let node = Tezos_utils.Cast.flatten_node node in + * let str = Tezos_utils.Cast.node_to_string node in + * Format.printf "Program:\n%s\n%!" str ; + * ok () *) let main = "Ligo", [ test "basic" basic ; - test "basic.display" display_basic ; ] end let () = (* Printexc.record_backtrace true ; *) Alcotest.run "LIGO" [ - main ; + Ligo.main ; ] ; () diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index a73aa7698..33f427066 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -66,7 +66,12 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express | Literal (Nat n) -> ok (Literal (`Nat n), tv, env) | Literal (Bytes s) -> ok (Literal (`Bytes s), tv, env) | Literal (String s) -> ok (Literal (`String s), tv, env) + | Literal Unit -> ok (Literal `Unit, tv, env) | Variable name -> ok (Var name, tv, env) + | Application (a, b) -> + let%bind a = translate_annotated_expression env a in + let%bind b = translate_annotated_expression env b in + ok (Apply (a, b), tv, env) | Constructor (m, param) -> let%bind (param'_expr, param'_tv, _) = translate_annotated_expression env ae in let%bind map_tv = AST.get_t_sum ae.type_annotation in diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 496b8941e..af3700759 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -32,10 +32,39 @@ module Environment = struct List.assoc_opt s e.type_environment let add_type (e:t) (s:string) (tv:ele) : t = {e with type_environment = (s, tv) :: e.type_environment} + + module PP = struct + open Format + open Ligo_helpers.PP + + let value ppf (e:t) = + let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in + fprintf ppf "ValueEnv[%a]" (list_sep pp) e.environment + + let type_ ppf e = + let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in + fprintf ppf "TypeEnv[%a]" (list_sep pp) e.type_environment + + let full ppf e = + fprintf ppf "%a\n%a" value e type_ e + end end type environment = Environment.t +module Errors = struct + let unbound_type_variable (e:environment) (n:string) = + let title = "unbound type variable" in + let full = Format.asprintf "%s in %a" n Environment.PP.type_ e in + error title full + + let unrecognized_constant (n:string) = + let title = "unrecognized constant" in + let full = n in + error title full +end +open Errors + let rec type_program (p:I.program) : O.program result = let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) = let%bind (e', d') = type_declaration e d in @@ -99,6 +128,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc let%bind m' = type_match e m in let%bind ex' = type_annotated_expression e ex in ok (e, O.Matching (ex', m')) + | Record_patch _ -> simple_fail "no record_patch yet" and type_match (e:environment) : I.matching -> O.matching result = function | Match_bool {match_true ; match_false} -> @@ -148,7 +178,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f ok (O.Type_record m) | Type_variable name -> let%bind tv = - trace_option (simple_error "unbound type variable") + trace_option (unbound_type_variable e name) @@ Environment.get_type e name in ok tv | Type_constant (cst, lst) -> @@ -171,6 +201,9 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | Literal (Bool b) -> let%bind type_annotation = check O.t_bool in ok O.{expression = Literal (Bool b) ; type_annotation } + | Literal Unit -> + let%bind type_annotation = check O.t_unit in + ok O.{expression = Literal (Unit) ; type_annotation } | Literal (String s) -> let%bind type_annotation = check O.t_string in ok O.{expression = Literal (String s) ; type_annotation } @@ -241,13 +274,23 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let%bind (name', tv) = type_constant name tv_lst in let%bind type_annotation = check tv in ok O.{expression = O.Constant (name', lst') ; type_annotation} + | Application (f, arg) -> + let%bind f = type_annotated_expression e f in + let%bind arg = type_annotated_expression e arg in + let%bind type_annotation = match f.type_annotation with + | Type_function (param, result) -> + let%bind _ = O.type_value_eq (param, arg.type_annotation) in + ok result + | _ -> simple_fail "applying to not-a-function" + in + ok O.{expression = Application (f, arg) ; type_annotation} and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value) result = (* Constant poorman's polymorphism *) let open O in match (name, lst) with - | "add", [a ; b] when a = t_int && b = t_int -> ok ("add_int", t_int) - | "add", [a ; b] when a = t_string && b = t_string -> ok ("concat_string", t_string) - | "add", [_ ; _] -> simple_fail "bad types to add" - | "add", _ -> simple_fail "bad number of params to add" - | _ -> simple_fail "unrecognized constant" + | "ADD", [a ; b] when a = t_int && b = t_int -> ok ("ADD_INT", t_int) + | "ADD", [a ; b] when a = t_string && b = t_string -> ok ("CONCAT", t_string) + | "ADD", [_ ; _] -> simple_fail "bad types to add" + | "ADD", _ -> simple_fail "bad number of params to add" + | name, _ -> fail @@ unrecognized_constant name