From b8e5203d6517c92a53f1c1808978abe277ce8be8 Mon Sep 17 00:00:00 2001 From: Galfour Date: Thu, 2 May 2019 11:10:16 +0000 Subject: [PATCH] start coase; start simplify --- src/ligo/TODO.txt | 2 ++ src/ligo/contracts/coase.ligo | 57 ++++++++++++++++++++++++++++++ src/ligo/simplify/pascaligo.ml | 28 ++++++++++----- src/ligo/test/coase_tests.ml | 64 ++++++++++++++++++++++++++++++++++ src/ligo/test/test.ml | 1 + src/ligo/typer/typer.ml | 27 ++++++++++++-- 6 files changed, 168 insertions(+), 11 deletions(-) create mode 100644 src/ligo/TODO.txt create mode 100644 src/ligo/contracts/coase.ligo create mode 100644 src/ligo/test/coase_tests.ml diff --git a/src/ligo/TODO.txt b/src/ligo/TODO.txt new file mode 100644 index 000000000..ea687b9ba --- /dev/null +++ b/src/ligo/TODO.txt @@ -0,0 +1,2 @@ +- Unify gets in Ast_simplified +- Unify assignments in Ast_simplified diff --git a/src/ligo/contracts/coase.ligo b/src/ligo/contracts/coase.ligo new file mode 100644 index 000000000..56f1ee4ce --- /dev/null +++ b/src/ligo/contracts/coase.ligo @@ -0,0 +1,57 @@ +// Copyright Coase, Inc 2019 + +type card_pattern_id is nat +type card_pattern is record [ + coefficient : tez ; + quantity : nat ; + last_id : nat ; +] + +type card_patterns is map(card_pattern_id , card_pattern) + +type card_id is nat +type card is record [ + card_owner : address +] +type cards is map(card_id , card) + +type storage_type is record [ + cards : cards ; + card_patterns : card_patterns ; +] + +type action_buy_single is record [ + card_to_buy : card_pattern_id ; +] +type action_sell_single is record [ + card_to_sell : card_id ; +] +type action_transfer is record [ + card_to_transfer : card_id ; + destination : address ; +] + +type action is +| Buy_single of action_buy_single +// | Sell of action_sell +// | Transfer of action_transfer + +function buy_single(const action : action_buy_single ; const s : storage_type) : (list(operation) * storage_type) is + begin + const pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ; + const price : tez = card_pattern.coefficient * (card_pattern.quantity + 1n) ; + if (price > amount) then fail "Not enough money" else skip ; + const operations : list(operation) = nil ; + pattern.quantity := pattern.quantity + 1n ; + const card_patterns : card_patterns = s.card_patterns ; + card_patterns[action.card_to_buy] := pattern ; + s.card_patterns := card_patterns ; + end with (operations , s) + +function main(const action : action ; const s : storage_type) : (list(operation) * storage_type) is + block {skip} with + case action of + | Buy_single abs -> buy_single (abs , s) + // | Sell as -> sell_single (as , s) + // | Transfer at -> transfer (at , s) + end diff --git a/src/ligo/simplify/pascaligo.ml b/src/ligo/simplify/pascaligo.ml index 62d95b596..9727a927a 100644 --- a/src/ligo/simplify/pascaligo.ml +++ b/src/ligo/simplify/pascaligo.ml @@ -90,6 +90,7 @@ let rec simpl_expression (t:Raw.expr) : ae result = | Component index -> Access_tuple (Z.to_int (snd index.value)) in List.map aux @@ npseq_to_list path in + ok @@ make_e_a @@ E_accessor (var, path') in match t with @@ -457,18 +458,12 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> ok @@ I_matching (expr, m) | RecordPatch r -> ( let r = r.value in - let%bind record = match r.path with - | Name v -> ok v.value - | path -> ( - let err_content () = Format.asprintf "%a" (PP_helpers.printer Parser.Pascaligo.ParserLog.print_path) path in - fail @@ (fun () -> error (thunk "no complex record patch yet") err_content ()) - ) - in + let (name , access_path) = simpl_path r.path 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 @@ I_record_patch (record, [], inj) + ok @@ I_record_patch (name, access_path, inj) ) | MapPatch _ -> simple_fail "no map patch yet" | SetPatch _ -> simple_fail "no set patch yet" @@ -483,6 +478,23 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> ok @@ I_assignment {name = map ; annotated_expression = make_e_a expr} | SetRemove _ -> simple_fail "no set remove yet" +and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p -> + match p with + | Raw.Name v -> (v.value , []) + | Raw.Path p -> ( + let p' = p.value in + let var = p'.struct_name.value in + let path = p'.field_path in + let path' = + let aux (s:Raw.selection) = + match s with + | FieldName property -> Access_record property.value + | Component index -> Access_tuple (Z.to_int (snd index.value)) + in + List.map aux @@ npseq_to_list path in + (var , path') + ) + and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -> let open Raw in let get_var (t:Raw.pattern) = match t with diff --git a/src/ligo/test/coase_tests.ml b/src/ligo/test/coase_tests.ml new file mode 100644 index 000000000..7e02496b4 --- /dev/null +++ b/src/ligo/test/coase_tests.ml @@ -0,0 +1,64 @@ +(* Copyright Coase, Inc 2019 *) + +open Trace +open Ligo +open Test_helpers + +let get_program = + let s = ref None in + fun () -> match !s with + | Some s -> ok s + | None -> ( + let%bind program = type_file "./contracts/coase.ligo" in + s := Some program ; + ok program + ) + +let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) = + let open AST_Typed.Combinators in + let content = + let aux = fun (x, y) -> e_a_empty_nat x, y in + List.map aux content in + let value_type = match value_type, content with + | None, hd :: _ -> (snd hd).type_annotation + | Some s, _ -> s + | _ -> raise (Failure "no value type and heap empty when building heap") in + e_a_empty_map content (t_nat ()) value_type + +let ez lst = + let open AST_Typed.Combinators in + let value_type = t_pair + (t_int ()) + (t_string ()) + () + in + let lst' = + let aux (i, (j, s)) = + (i, e_a_empty_pair (e_a_empty_int j) (e_a_empty_string s)) in + List.map aux lst in + a_heap_ez ~value_type lst' + +let dummy n = + ez List.( + map (fun n -> (n, (n, string_of_int n))) + @@ tl + @@ range (n + 1) + ) + +let buy () = + let%bind program = get_program () in + let aux n = + let open AST_Typed.Combinators in + let input = dummy n in + let%bind result = easy_run_typed "is_empty" program input in + let expected = e_a_empty_bool (n = 0) in + AST_Typed.assert_value_eq (expected, result) + in + let%bind _ = bind_list + @@ List.map aux + @@ [0 ; 2 ; 7 ; 12] in + ok () + +let main = "Coase (End to End)", [ + test "buy" buy ; + ] diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml index 6d1965d27..3dbd250cb 100644 --- a/src/ligo/test/test.ml +++ b/src/ligo/test/test.ml @@ -9,5 +9,6 @@ let () = Transpiler_tests.main ; Typer_tests.main ; Heap_tests.main ; + (* Coase_tests.main ; *) ] ; () diff --git a/src/ligo/typer/typer.ml b/src/ligo/typer/typer.ml index c6157380f..f396b1b0e 100644 --- a/src/ligo/typer/typer.ml +++ b/src/ligo/typer/typer.ml @@ -123,10 +123,31 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc let e' = Environment.add_ez_ae name annotated_expression e in ok (e', [O.I_assignment (make_n_e name annotated_expression)]) ) - | I_matching (ex, m) -> + | I_matching (ex, m) -> ( let%bind ex' = type_annotated_expression e ex in - let%bind m' = type_match type_block e ex'.type_annotation m in - return @@ O.I_matching (ex', m') + match m with + (* Special case for assert-like failwiths. TODO: CLEAN THIS. *) + | I.Match_bool { match_false ; match_true = [ I_do { expression = E_failwith fw } ] } -> ( + let%bind fw' = type_annotated_expression e fw in + let%bind mf' = type_block e match_false in + let%bind () = + trace_strong (simple_error "Matching bool on not-a-bool") + @@ assert_t_bool (get_type_annotation ex') in + let mt' = [ O.I_do ( + make_a_e + (E_failwith fw') + (t_unit ()) + e + ) ] + in + let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in + return (O.I_matching (ex' , m')) + ) + | _ -> ( + let%bind m' = type_match type_block e ex'.type_annotation m in + return @@ O.I_matching (ex', m') + ) + ) | I_record_patch (r, path, lst) -> let aux (s, ae) = let%bind ae' = type_annotated_expression e ae in