start coase; start simplify

This commit is contained in:
Galfour 2019-05-02 11:10:16 +00:00
parent 76163aa855
commit b8e5203d65
6 changed files with 168 additions and 11 deletions

2
src/ligo/TODO.txt Normal file
View File

@ -0,0 +1,2 @@
- Unify gets in Ast_simplified
- Unify assignments in Ast_simplified

View File

@ -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

View File

@ -90,6 +90,7 @@ let rec simpl_expression (t:Raw.expr) : ae result =
| Component index -> Access_tuple (Z.to_int (snd index.value)) | Component index -> Access_tuple (Z.to_int (snd index.value))
in in
List.map aux @@ npseq_to_list path in List.map aux @@ npseq_to_list path in
ok @@ make_e_a @@ E_accessor (var, path') ok @@ make_e_a @@ E_accessor (var, path')
in in
match t with match t with
@ -457,18 +458,12 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
ok @@ I_matching (expr, m) ok @@ I_matching (expr, m)
| RecordPatch r -> ( | RecordPatch r -> (
let r = r.value in let r = r.value in
let%bind record = match r.path with let (name , access_path) = simpl_path r.path in
| 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%bind inj = bind_list 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.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) @@ List.map (fun (x:_ Raw.reg) -> x.value)
@@ npseq_to_list r.record_inj.value.fields in @@ 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" | MapPatch _ -> simple_fail "no map patch yet"
| SetPatch _ -> simple_fail "no set 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} ok @@ I_assignment {name = map ; annotated_expression = make_e_a expr}
| SetRemove _ -> simple_fail "no set remove yet" | 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 -> and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
let open Raw in let open Raw in
let get_var (t:Raw.pattern) = match t with let get_var (t:Raw.pattern) = match t with

View File

@ -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 ;
]

View File

@ -9,5 +9,6 @@ let () =
Transpiler_tests.main ; Transpiler_tests.main ;
Typer_tests.main ; Typer_tests.main ;
Heap_tests.main ; Heap_tests.main ;
(* Coase_tests.main ; *)
] ; ] ;
() ()

View File

@ -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 let e' = Environment.add_ez_ae name annotated_expression e in
ok (e', [O.I_assignment (make_n_e name annotated_expression)]) 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 ex' = type_annotated_expression e ex in
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 let%bind m' = type_match type_block e ex'.type_annotation m in
return @@ O.I_matching (ex', m') return @@ O.I_matching (ex', m')
)
)
| I_record_patch (r, path, lst) -> | I_record_patch (r, path, lst) ->
let aux (s, ae) = let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in let%bind ae' = type_annotated_expression e ae in