From 941dadeb3ba67baf597b4bf9884aa13a1eed697b Mon Sep 17 00:00:00 2001 From: Galfour Date: Sat, 30 Mar 2019 00:52:40 +0000 Subject: [PATCH] added matching tests --- src/ligo/ast_simplified.ml | 424 +------------------------- src/ligo/ast_typed.ml | 21 +- src/ligo/contracts/map.ligo | 19 ++ src/ligo/contracts/match.ligo | 19 +- src/ligo/contracts/option.ligo | 4 + src/ligo/ligo.ml | 4 +- src/ligo/mini_c.ml | 139 +++++---- src/ligo/simplify.ml | 457 +++++++++++++++++++++++++++++ src/ligo/test/integration_tests.ml | 68 +++++ src/ligo/transpiler.ml | 51 +++- src/ligo/typer.ml | 27 +- 11 files changed, 741 insertions(+), 492 deletions(-) create mode 100644 src/ligo/contracts/map.ligo create mode 100644 src/ligo/contracts/option.ligo create mode 100644 src/ligo/simplify.ml diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 46091ce4a..3d5cbe2ef 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -65,6 +65,7 @@ and expression = | Accessor of ae * access_path (* Data Structures *) | Map of (ae * ae) list + | LookUp of (ae * ae) and access = | Tuple_access of int @@ -140,6 +141,7 @@ module PP = struct | Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m | Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m + | LookUp (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind | Lambda {binder;input_type;output_type;result;body} -> fprintf ppf "lambda (%s:%a) : %a {%a} return %a" binder type_expression input_type type_expression output_type @@ -310,433 +312,19 @@ module Rename = struct let%bind m' = bind_map_list (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in ok (Map m') + | LookUp m -> + let%bind m' = bind_map_pair (rename_annotated_expression r) m in + ok (LookUp m') end end -module Simplify = struct - module Raw = Ligo_parser.AST - - 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 = [ - ("unit", 0) ; - ("nat", 0) ; - ("int", 0) ; - ("bool", 0) ; - ("list", 1) ; - ("set", 1) ; - ("map", 2) ; - ] - - 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 -> ( - 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 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 tpl = simpl_list_type_expression - @@ npseq_to_list p.value in - 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 - @@ List.map aux - @@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type)) - @@ npseq_to_list r.value.field_decls in - let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in - ok @@ Type_record m - | TSum s -> - let aux (v:Raw.variant Raw.reg) = - let%bind te = simpl_list_type_expression - @@ npseq_to_list v.value.product.value in - ok (v.value.constr.value, te) - in - let%bind lst = bind_list - @@ List.map aux - @@ npseq_to_list s.value in - let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in - ok @@ Type_sum m - - and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result = - match lst with - | [] -> assert false - | [hd] -> simpl_type_expression hd - | lst -> - let%bind lst = bind_list @@ List.map simpl_type_expression lst in - ok @@ Type_tuple lst - - let rec simpl_expression (t:Raw.expr) : ae result = - match t with - | EVar c -> - if c.value = "unit" - then ok @@ ae @@ Literal Unit - else ok @@ ae @@ Variable c.value - | ECall x -> - let (name, args) = x.value in - let f = name.value in - let%bind arg = simpl_list_expression - @@ npseq_to_list args.value.inside in - 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 (Bytes.of_string @@ fst x.value)) - | ETuple tpl -> - let (Raw.TupleInj tpl') = tpl in - 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) - | EProj p' -> ( - let p = p'.value in - let var = - let name = p.record_name.value in - ae @@ Variable name in - let path = p.field_path in - let path' = - let aux (s:Raw.selection) = - match s with - | FieldName property -> Record_access property.value - | Component index -> Tuple_access (Z.to_int (snd index.value)) - in - List.map aux @@ npseq_to_list path in - ok @@ ae @@ Accessor (var, path') - ) - | 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) -> - simpl_binop "ADD" c.value - | EArith (Int n) -> - let n = Z.to_int @@ snd @@ n.value in - ok @@ ae @@ Literal (Number n) - | EArith _ -> simple_fail "arith: not supported yet" - | EString (String s) -> - ok @@ ae @@ Literal (String s.value) - | EString _ -> simple_fail "string: not supported yet" - | ELogic l -> simpl_logic_expression l - | EList _ -> simple_fail "list: not supported yet" - | ESet _ -> simple_fail "set: not supported yet" - | EMap _ -> simple_fail "map: not supported yet" - - and simpl_logic_expression (t:Raw.logic_expr) : ae result = - match t with - | BoolExpr (False _) -> - ok @@ ae @@ Literal (Bool false) - | BoolExpr (True _) -> - ok @@ ae @@ Literal (Bool true) - | BoolExpr (Or b) -> - simpl_binop "OR" b.value - | BoolExpr (And b) -> - simpl_binop "AND" b.value - | BoolExpr (Not b) -> - simpl_unop "NOT" b.value - | CompExpr (Lt c) -> - simpl_binop "LT" c.value - | CompExpr (Gt c) -> - simpl_binop "GT" c.value - | CompExpr (Leq c) -> - simpl_binop "LE" c.value - | CompExpr (Geq c) -> - simpl_binop "GE" c.value - | CompExpr (Equal c) -> - simpl_binop "EQ" c.value - | CompExpr (Neq c) -> - simpl_binop "NEQ" c.value - - and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result = - let%bind a = simpl_expression t.arg1 in - let%bind b = simpl_expression t.arg2 in - ok @@ ae @@ Constant (name, [a;b]) - - and simpl_unop (name:string) (t:_ Raw.un_op) : ae result = - let%bind a = simpl_expression t.arg in - ok @@ ae @@ Constant (name, [a]) - - and simpl_list_expression (lst:Raw.expr list) : ae result = - match lst with - | [] -> ok @@ ae @@ Literal Unit - | [hd] -> simpl_expression hd - | lst -> - let%bind lst = bind_list @@ List.map simpl_expression lst in - ok @@ ae @@ Tuple lst - - and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result = - match t with - | LocalData d -> simpl_data_declaration d - | LocalLam _ -> simple_fail "no local lambdas yet" - - and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result = - let return x = ok (Assignment x, x) in - 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 - return {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 - return {name;annotated_expression={expression with type_annotation}} - - - and simpl_param : Raw.param_decl -> named_type_expression result = fun t -> - 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 : Raw.declaration -> declaration result = fun t -> - let open! Raw in - match t with - | TypeDecl x -> - let {name;type_expr} : Raw.type_decl = x.value in - let%bind type_expression = simpl_type_expression type_expr in - ok @@ Type_declaration {type_name=name.value;type_expression} - | ConstDecl x -> - let {name;const_type;init} = x.value in - let%bind expression = simpl_expression init in - let%bind t = simpl_type_expression const_type in - let type_annotation = Some t in - 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 - (match npseq_to_list param.value.inside with - | [] -> simple_fail "function without parameters are not allowed" - | [a] -> ( - let%bind input = simpl_param a in - let name = name.value in - let binder = input.type_name in - let input_type = input.type_expression in - let%bind local_declarations = - let%bind tmp = bind_list - @@ List.map simpl_local_declaration local_decls in - ok (List.map fst tmp) in - let%bind instructions = bind_list - @@ List.map simpl_statement - @@ npseq_to_list block.value.statements 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 decl = - let expression = Lambda {binder ; input_type ; output_type ; result ; body } in - let type_annotation = Some (Type_function (input_type, output_type)) in - Constant_declaration {name;annotated_expression = {expression;type_annotation}} - in - ok decl - ) - | lst -> ( - let%bind params = bind_map_list simpl_param lst in - let input = - let type_expression = Type_record ( - SMap.of_list - @@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression) - params - ) in - { type_name = "arguments" ; type_expression } in - let binder = input.type_name in - let input_type = input.type_expression in - let%bind local_declarations = - let%bind typed = bind_map_list simpl_local_declaration local_decls in - ok (List.map fst typed) - in - let%bind output_type = simpl_type_expression ret_type in - let%bind instructions = bind_list - @@ List.map simpl_statement - @@ npseq_to_list block.value.statements in - let%bind (body, result) = - let renamings = - let aux ({type_name}:named_type_expression) : Rename.Value.renaming = - type_name, ("arguments", [Record_access type_name]) - in - List.map aux params - in - let%bind r = - let%bind tmp = simpl_expression return in - Rename.Value.rename_annotated_expression renamings tmp - in - let%bind b = - let tmp = local_declarations @ instructions in - Rename.Value.rename_block renamings tmp - in - ok (b, r) in - let decl = - let expression = Lambda {binder ; input_type ; output_type ; result ; body } in - let type_annotation = Some (Type_function (input_type, output_type)) in - Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}} - in - ok decl - ) - ) - | LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet" - | LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet" - - and simpl_statement : Raw.statement -> instruction result = fun s -> - match s with - | Instr i -> simpl_instruction i - | Data d -> let%bind (i, _) = simpl_data_declaration d in ok i - - and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> - 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 = match c.ifso with - | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] - | ClauseBlock b -> simpl_statements @@ fst b.value.inside in - let%bind match_false = match c.ifnot with - | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] - | ClauseBlock b -> simpl_statements @@ fst b.value.inside 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 = - let aux (x : Raw.case Raw.reg) = - let%bind i = simpl_instruction_block x.value.instr in - ok (x.value.pattern, i) in - bind_list - @@ List.map aux - @@ 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 (record, [], inj) - | MapPatch _ -> simple_fail "no map patch yet" - | SetPatch _ -> simple_fail "no set patch yet" - | MapRemove _ -> simple_fail "no map remove yet" - | SetRemove _ -> simple_fail "no set remove yet" - - and simpl_cases : (Raw.pattern * block) list -> matching result = fun t -> - 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 _, t) ; (PFalse _, f)] -> 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 (PNil _), nil)] - | [(PList (PNil _), nil) ; (PCons c, cons)] -> - 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 : Raw.instruction -> block result = fun t -> - match t with - | Single s -> let%bind i = simpl_single_instruction s in ok [ i ] - | Block b -> simpl_block b.value - - and simpl_instruction : Raw.instruction -> instruction result = fun t -> - match t with - | Single s -> simpl_single_instruction s - | Block _ -> simple_fail "no block instruction yet" - - and simpl_statements : Raw.statements -> block result = fun ss -> - let lst = npseq_to_list ss in - bind_map_list simpl_statement lst - - and simpl_block : Raw.block -> block result = fun t -> - simpl_statements t.statements - - let simpl_program : Raw.ast -> program result = fun t -> - bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl -end - module Combinators = struct let t_bool : type_expression = Type_constant ("bool", []) let t_string : type_expression = Type_constant ("string", []) let t_bytes : type_expression = Type_constant ("bytes", []) let t_int : type_expression = Type_constant ("int", []) let t_unit : type_expression = Type_constant ("unit", []) + let t_option o : type_expression = Type_constant ("option", [o]) let t_tuple lst : type_expression = Type_tuple lst let t_pair a b = t_tuple [a ; b] let t_record m : type_expression = (Type_record m) diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index df4b973ef..2e19cf379 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -66,6 +66,7 @@ and expression = | Record_accessor of ae * string (* Data Structures *) | Map of (ae * ae) list + | LookUp of (ae * ae) and value = annotated_expression (* todo (for refactoring) *) @@ -98,7 +99,7 @@ and matching = } | Match_option of { match_none : b ; - match_some : name * b ; + match_some : (name * type_value) * b ; } | Match_tuple of name list * b @@ -163,6 +164,7 @@ module PP = struct | Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m | Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m + | LookUp (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" annotated_expression a annotated_expression b @@ -189,7 +191,7 @@ module PP = struct | 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 + fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none (fst some) block match_some and instruction ppf (i:instruction) = match i with | Skip -> fprintf ppf "skip" @@ -381,8 +383,7 @@ let merge_annotation (a:type_value option) (b:type_value option) : type_value re let%bind _ = assert_type_value_eq (a, b) in match a.simplified, b.simplified with | _, None -> ok a - | None, Some _ -> ok b - | _ -> simple_fail "both have simplified ASTs" + | _, Some _ -> ok b module Combinators = struct @@ -406,6 +407,9 @@ module Combinators = struct let simplify_t_unit s = t_unit (Some s) let make_t_unit = t_unit None + let t_option o s : type_value = type_value (Type_constant ("option", [o])) s + let make_t_option o = t_option o None + let t_tuple lst s : type_value = type_value (Type_tuple lst) s let simplify_t_tuple lst s = t_tuple lst (Some s) let make_t_tuple lst = t_tuple lst None @@ -460,11 +464,18 @@ module Combinators = struct | Type_record m -> ok m | _ -> simple_fail "not a record" + let get_t_map (t:type_value) : (type_value * type_value) result = + match t.type_value with + | Type_constant ("map", [k;v]) -> ok (k, v) + | _ -> simple_fail "not a map" + let record map : expression = Record map let record_ez (lst : (string * ae) list) : expression = let aux prev (k, v) = SMap.add k v prev in let map = List.fold_left aux SMap.empty lst in record map + let some s : expression = Constant ("SOME", [s]) + let none : expression = Constant ("NONE", []) let map lst : expression = Map lst @@ -477,6 +488,8 @@ module Combinators = struct let a_int n = annotated_expression (int n) make_t_int let a_bool b = annotated_expression (bool b) make_t_bool let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation) + let a_some s = annotated_expression (some s) (make_t_option s.type_annotation) + let a_none t = annotated_expression none (make_t_option t) let a_tuple lst = annotated_expression (Tuple lst) (make_t_tuple (List.map get_type_annotation lst)) let a_record r = annotated_expression (record r) (make_t_record (SMap.map get_type_annotation r)) let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r)) diff --git a/src/ligo/contracts/map.ligo b/src/ligo/contracts/map.ligo new file mode 100644 index 000000000..896317631 --- /dev/null +++ b/src/ligo/contracts/map.ligo @@ -0,0 +1,19 @@ +type foobar is map(int, int) + +const fb : foobar = map + 23 -> 0 ; + 42 -> 0 ; +end + +function get (const m : foobar) : int is + begin + skip + end with m[42] + m[23] + +const bm : foobar = map + 144 -> 23 ; + 51 -> 23 ; + 42 -> 23 ; + 120 -> 23 ; + 421 -> 23 ; +end diff --git a/src/ligo/contracts/match.ligo b/src/ligo/contracts/match.ligo index 68c949640..6f3d3afd1 100644 --- a/src/ligo/contracts/match.ligo +++ b/src/ligo/contracts/match.ligo @@ -1,8 +1,17 @@ -function main (const i : int) : int is +function match_bool (const i : int) : int is var result : int := 23 ; begin - if i = 2 then - result := 42 - else - result := 0 + case i = 2 of + | True -> result := 42 + | False -> result := 0 + end + end with result + +function match_option (const o : option(int)) : int is + var result : int := 23 ; + begin + case o of + | None -> skip + | Some(s) -> result := s + end end with result diff --git a/src/ligo/contracts/option.ligo b/src/ligo/contracts/option.ligo new file mode 100644 index 000000000..85e3396e0 --- /dev/null +++ b/src/ligo/contracts/option.ligo @@ -0,0 +1,4 @@ +type foobar is option(int) + +const s : foobar = Some(42) +const n : foobar = None diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml index a8f1c8639..c2c198ee9 100644 --- a/src/ligo/ligo.ml +++ b/src/ligo/ligo.ml @@ -85,8 +85,8 @@ let parse_expression (s:string) : AST_Raw.expr result = ) >>? fun raw -> ok raw -let simplify (p:AST_Raw.t) : Ast_simplified.program result = AST_Simplified.Simplify.simpl_program p -let simplify_expr (e:AST_Raw.expr) : Ast_simplified.annotated_expression result = AST_Simplified.Simplify.simpl_expression e +let simplify (p:AST_Raw.t) : Ast_simplified.program result = Simplify.simpl_program p +let simplify_expr (e:AST_Raw.expr) : Ast_simplified.annotated_expression result = Simplify.simpl_expression e let unparse_simplified_expr (e:AST_Simplified.annotated_expression) : string result = ok @@ Format.asprintf "%a" AST_Simplified.PP.annotated_expression e diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 813fd106a..d38a95a9f 100644 --- a/src/ligo/mini_c.ml +++ b/src/ligo/mini_c.ml @@ -26,6 +26,7 @@ type type_value = [ | `Shallow_closure of environment * type_value * type_value | `Base of type_base | `Map of type_value * type_value + | `Option of type_value ] and environment_element = string * type_value @@ -54,6 +55,8 @@ type value = [ | `Pair of value * value | `Left of value | `Right of value + | `Some of value + | `None (* | `Macro of anon_macro ... The future. *) | `Function of anon_function ] @@ -64,6 +67,8 @@ and expression' = | Predicate of string * expression list | Apply of expression * expression | Var of var_name + | Empty_map of (type_value * type_value) + | Make_None of type_value and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *) @@ -72,6 +77,7 @@ and assignment = var_name * expression and statement' = | Assignment of assignment | Cond of expression * block * block + | If_None of expression * block * (var_name * block) | While of expression * block and statement = statement' * environment_wrap @@ -125,6 +131,7 @@ module PP = struct | `Base b -> type_base ppf b | `Function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b | `Map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v + | `Option(o) -> fprintf ppf "option(%a)" type_ o | `Shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b | `Deep_closure(c, arg, ret) -> fprintf ppf "[%a](%a)->(%a)" @@ -156,6 +163,8 @@ module PP = struct | `Left a -> fprintf ppf "L(%a)" value a | `Right b -> fprintf ppf "R(%a)" value b | `Function x -> function_ ppf x.content + | `None -> fprintf ppf "None" + | `Some s -> fprintf ppf "Some (%a)" value s and expression ppf ((e, _, _):expression) = match e with | Var v -> fprintf ppf "%s" v @@ -163,6 +172,8 @@ module PP = struct | Predicate(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst | Literal v -> fprintf ppf "%a" value v | Function_expression c -> function_ ppf c + | Empty_map _ -> fprintf ppf "map[]" + | Make_None _ -> fprintf ppf "none" and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) = fprintf ppf "fun (%s:%a) : %a %a return %a" @@ -177,6 +188,7 @@ module PP = struct and statement ppf ((s, _) : statement) = match s with | Assignment ass -> assignment ppf ass | Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e + | If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b and block ppf ((b, _):block) = @@ -188,46 +200,6 @@ module PP = struct fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p end -module Free_variables = struct - type free_variable = string - type free_variables = free_variable list - type t' = free_variable - type t = free_variables - - let append_wd (* without doubles *) double x t = - if List.mem x double - then t - else x :: t - - let append_bound x t = append_wd t x t - - let rec expression' (bound:t) : expression' -> t = function - | Literal _ -> [] - | Var x -> append_wd bound x [] - | Predicate(_, exprs) -> List.(concat @@ map (expression bound) exprs) - | Apply(a, b) -> List.(concat @@ map (expression bound) [a;b]) - | Function_expression {binder;body;result} -> block (binder :: bound) body @ expression (binder :: bound) result - - and expression bound (expr, _, _) = expression' bound expr - - and statement bound ((s, _) : statement) : (t * t) = match s with - | Assignment (n, e) -> append_bound n bound, expression bound e - | Cond (e, a, b) -> bound, (expression bound e) @ (block bound a) @ (block bound b) - | While (e, b) -> bound, (expression bound e) @ (block bound b) - - and block' bound (b:block') : t = match b with - | [] -> [] - | hd :: tl -> - let (bound, fv) = statement bound hd in - let fv' = block' bound tl in - fv @ fv' - - and block bound (b, _ : block) : t = block' bound b - - let function_ ({content = {body ; binder ; result}} : anon_function) : t = - block [binder] body @ expression [binder] result -end - module Translate_type = struct open Tezos_utils.Micheline.Michelson @@ -251,10 +223,11 @@ module Translate_type = struct | `Base b -> comparable_type_base b | `Deep_closure _ -> fail (not_comparable "deep closure") | `Shallow_closure _ -> fail (not_comparable "shallow closure") - | `Function _ -> fail (not_comparable "function closure") - | `Or _ -> fail (not_comparable "or closure") - | `Pair _ -> fail (not_comparable "pair closure") - | `Map _ -> fail (not_comparable "map closure") + | `Function _ -> fail (not_comparable "function") + | `Or _ -> fail (not_comparable "or") + | `Pair _ -> fail (not_comparable "pair") + | `Map _ -> fail (not_comparable "map") + | `Option _ -> fail (not_comparable "option") let base_type : type_base -> ex_ty result = fun b -> let open Types in @@ -299,6 +272,9 @@ module Translate_type = struct let%bind (Ex_comparable_ty k') = comparable_type k in let%bind (Ex_ty v') = type_ v in ok @@ Ex_ty Types.(map k' v') + | `Option t -> + let%bind (Ex_ty t') = type_ t in + ok @@ Ex_ty Types.(option t') and environment_small' = let open Append_tree in function @@ -347,6 +323,9 @@ module Translate_type = struct | `Map kv -> let%bind (k', v') = bind_map_pair type_ kv in ok @@ prim ~children:[k';v'] T_map + | `Option o -> + let%bind o' = type_ o in + ok @@ prim ~children:[o'] T_option | `Function (arg, ret) -> let%bind arg = type_ arg in let%bind ret = type_ ret in @@ -646,6 +625,10 @@ module Translate_program = struct | Binary of michelson | Ternary of michelson + let simple_constant c = Constant ( seq [ + c ; i_pair ; + ]) + let simple_unary c = Unary ( seq [ i_unpair ; c ; i_pair ; ]) @@ -654,6 +637,10 @@ module Translate_program = struct i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ; ]) + let simple_ternary c = Ternary ( seq [ + i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ; + ]) + let rec get_predicate : string -> predicate result = function | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD | "NEG" -> ok @@ simple_unary @@ prim I_NEG @@ -663,6 +650,8 @@ module Translate_program = struct | "CAR" -> ok @@ simple_unary @@ prim I_CAR | "CDR" -> ok @@ simple_unary @@ prim I_CDR | "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ] + | "UPDATE" -> ok @@ simple_ternary @@ prim I_UPDATE + | "SOME" -> ok @@ simple_unary @@ prim I_SOME | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist" and translate_value (v:value) : michelson result = match v with @@ -680,6 +669,10 @@ module Translate_program = struct | `Left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left | `Right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right | `Function anon -> translate_function anon + | `None -> ok @@ prim D_None + | `Some s -> + let%bind s' = translate_value s in + ok @@ prim ~children:[s'] D_Some and translate_function ({capture;content}:anon_function) : michelson result = let {capture_type } = content in @@ -766,6 +759,20 @@ module Translate_program = struct | _ -> simple_fail "bad arity" in ok code + | Empty_map sd -> + let%bind (src, dst) = bind_map_pair Translate_type.type_ sd in + let code = seq [ + prim ~children:[src;dst] I_EMPTY_MAP ; + i_pair ; + ] in + ok code + | Make_None o -> + let%bind o' = Translate_type.type_ o in + let code = seq [ + prim ~children:[o'] I_NONE ; + i_pair ; + ] in + ok code | Function_expression anon -> ( match ty with | `Function (_, _) -> @@ -861,12 +868,27 @@ module Translate_program = struct let%bind a = translate_regular_block a in let%bind b = translate_regular_block b in ok @@ (seq [ - prim ~children:[prim T_unit ; prim D_Unit] I_PUSH ; - expr ; - prim I_CAR ; - dip Environment.to_michelson_extend ; - prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ; - ]) + i_push_unit ; + expr ; + prim I_CAR ; + dip Environment.to_michelson_extend ; + prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ; + ]) + | If_None (expr, none, (_, some)) -> + let%bind expr = translate_expression expr in + let%bind none' = translate_regular_block none in + let%bind some' = translate_regular_block some in + let%bind add = + let env = Environment.extend w_env.pre_environment in + Environment.to_michelson_anonymous_add env in + ok @@ (seq [ + i_push_unit ; expr ; i_car ; + dip Environment.to_michelson_extend ; + prim ~children:[ + seq [none' ; Environment.to_michelson_restrict] ; + seq [add ; some' ; Environment.to_michelson_restrict] ; + ] I_IF_NONE + ]) | While ((_, _, _) as expr, block) -> let%bind expr = translate_expression expr in let%bind block = translate_regular_block block in @@ -984,6 +1006,11 @@ module Translate_ir = struct ok @@ `Bool b | (Unit_t _), () -> ok @@ `Unit + | (Option_t _), None -> + ok @@ `None + | (Option_t ((o_ty, _), _, _)), Some s -> + let%bind s' = translate_value @@ Ex_typed_value (o_ty, s) in + ok @@ `Some s' | _ -> simple_fail "this value can't be transpiled back yet" end @@ -1065,7 +1092,16 @@ module Combinators = struct let get_unit (v:value) = match v with | `Unit -> ok () - | _ -> simple_fail "not a bool" + | _ -> simple_fail "not a unit" + + let get_option (v:value) = match v with + | `None -> ok None + | `Some s -> ok (Some s) + | _ -> simple_fail "not an option" + + let get_t_option (v:type_value) = match v with + | `Option t -> ok t + | _ -> simple_fail "not an option" let get_pair (v:value) = match v with | `Pair (a, b) -> ok (a, b) @@ -1130,6 +1166,7 @@ module Combinators = struct let statement s' e : statement = match s' with | Cond _ -> s', id_environment_wrap e + | If_None _ -> s', id_environment_wrap e | While _ -> s', id_environment_wrap e | Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e) diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml new file mode 100644 index 000000000..c37b7ceff --- /dev/null +++ b/src/ligo/simplify.ml @@ -0,0 +1,457 @@ +open Ligo_helpers.Trace +open Ast_simplified +module Raw = Ligo_parser.AST + +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 get_value : 'a Raw.reg -> 'a = fun x -> x.value + +let type_constants = [ + ("unit", 0) ; + ("nat", 0) ; + ("int", 0) ; + ("bool", 0) ; + ("list", 1) ; + ("option", 1) ; + ("set", 1) ; + ("map", 2) ; +] + +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 -> ( + 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 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 tpl = simpl_list_type_expression + @@ npseq_to_list p.value in + 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 + @@ List.map aux + @@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type)) + @@ npseq_to_list r.value.field_decls in + let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in + ok @@ Type_record m + | TSum s -> + let aux (v:Raw.variant Raw.reg) = + let%bind te = simpl_list_type_expression + @@ npseq_to_list v.value.product.value in + ok (v.value.constr.value, te) + in + let%bind lst = bind_list + @@ List.map aux + @@ npseq_to_list s.value in + let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in + ok @@ Type_sum m + +and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result = + match lst with + | [] -> assert false + | [hd] -> simpl_type_expression hd + | lst -> + let%bind lst = bind_list @@ List.map simpl_type_expression lst in + ok @@ Type_tuple lst + +let rec simpl_expression (t:Raw.expr) : ae result = + let return x = ok @@ ae x in + let simpl_projection = fun (p:Raw.projection) -> + let var = + let name = p.record_name.value in + ae @@ Variable name in + let path = p.field_path in + let path' = + let aux (s:Raw.selection) = + match s with + | FieldName property -> Record_access property.value + | Component index -> Tuple_access (Z.to_int (snd index.value)) + in + List.map aux @@ npseq_to_list path in + ok @@ ae @@ Accessor (var, path') + in + match t with + | EVar c -> + if c.value = "unit" + then ok @@ ae @@ Literal Unit + else ok @@ ae @@ Variable c.value + | ECall x -> + let (name, args) = x.value in + let f = name.value in + let%bind arg = simpl_list_expression + @@ npseq_to_list args.value.inside in + 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 (Bytes.of_string @@ fst x.value)) + | ETuple tpl -> + let (Raw.TupleInj tpl') = tpl in + 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) + | EProj p' -> ( + let p = p'.value in + simpl_projection p + ) + | 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 (SomeApp a) -> + let (_, args) = a.value in + let%bind arg = + simpl_list_expression + @@ npseq_to_list args.value.inside in + ok @@ ae @@ Constant ("SOME", [arg]) + | EConstr (NoneExpr n) -> + let type_expr = n.value.inside.opt_type in + let%bind type_expr' = simpl_type_expression type_expr in + ok @@ annotated_expression (Constant ("NONE", [])) (Some (Combinators.t_option type_expr')) + | EArith (Add c) -> + simpl_binop "ADD" c.value + | EArith (Int n) -> + let n = Z.to_int @@ snd @@ n.value in + ok @@ ae @@ Literal (Number n) + | EArith _ -> simple_fail "arith: not supported yet" + | EString (String s) -> + ok @@ ae @@ Literal (String s.value) + | EString _ -> simple_fail "string: not supported yet" + | ELogic l -> simpl_logic_expression l + | EList _ -> simple_fail "list: not supported yet" + | ESet _ -> simple_fail "set: not supported yet" + | EMap (MapInj mi) -> + let%bind lst = + let lst = List.map get_value @@ pseq_to_list mi.value.elements in + let aux : Raw.binding -> (ae * ae) result = fun b -> + let%bind src = simpl_expression b.source in + let%bind dst = simpl_expression b.image in + ok (src, dst) in + bind_map_list aux lst in + return (Map lst) + | EMap (MapLookUp lu) -> + let%bind path = match lu.value.path with + | Name v -> return (Variable v.value) + | Path p -> simpl_projection p.value + in + let%bind index = simpl_expression lu.value.index.value.inside in + return (LookUp (path, index)) + +and simpl_logic_expression (t:Raw.logic_expr) : ae result = + match t with + | BoolExpr (False _) -> + ok @@ ae @@ Literal (Bool false) + | BoolExpr (True _) -> + ok @@ ae @@ Literal (Bool true) + | BoolExpr (Or b) -> + simpl_binop "OR" b.value + | BoolExpr (And b) -> + simpl_binop "AND" b.value + | BoolExpr (Not b) -> + simpl_unop "NOT" b.value + | CompExpr (Lt c) -> + simpl_binop "LT" c.value + | CompExpr (Gt c) -> + simpl_binop "GT" c.value + | CompExpr (Leq c) -> + simpl_binop "LE" c.value + | CompExpr (Geq c) -> + simpl_binop "GE" c.value + | CompExpr (Equal c) -> + simpl_binop "EQ" c.value + | CompExpr (Neq c) -> + simpl_binop "NEQ" c.value + +and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result = + let%bind a = simpl_expression t.arg1 in + let%bind b = simpl_expression t.arg2 in + ok @@ ae @@ Constant (name, [a;b]) + +and simpl_unop (name:string) (t:_ Raw.un_op) : ae result = + let%bind a = simpl_expression t.arg in + ok @@ ae @@ Constant (name, [a]) + +and simpl_list_expression (lst:Raw.expr list) : ae result = + match lst with + | [] -> ok @@ ae @@ Literal Unit + | [hd] -> simpl_expression hd + | lst -> + let%bind lst = bind_list @@ List.map simpl_expression lst in + ok @@ ae @@ Tuple lst + +and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result = + match t with + | LocalData d -> simpl_data_declaration d + | LocalLam _ -> simple_fail "no local lambdas yet" + +and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result = + let return x = ok (Assignment x, x) in + 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 + return {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 + return {name;annotated_expression={expression with type_annotation}} + + +and simpl_param : Raw.param_decl -> named_type_expression result = fun t -> + 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 : Raw.declaration -> declaration result = fun t -> + let open! Raw in + match t with + | TypeDecl x -> + let {name;type_expr} : Raw.type_decl = x.value in + let%bind type_expression = simpl_type_expression type_expr in + ok @@ Type_declaration {type_name=name.value;type_expression} + | ConstDecl x -> + let {name;const_type;init} = x.value in + let%bind expression = simpl_expression init in + let%bind t = simpl_type_expression const_type in + let type_annotation = Some t in + 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 + (match npseq_to_list param.value.inside with + | [] -> simple_fail "function without parameters are not allowed" + | [a] -> ( + let%bind input = simpl_param a in + let name = name.value in + let binder = input.type_name in + let input_type = input.type_expression in + let%bind local_declarations = + let%bind tmp = bind_list + @@ List.map simpl_local_declaration local_decls in + ok (List.map fst tmp) in + let%bind instructions = bind_list + @@ List.map simpl_statement + @@ npseq_to_list block.value.statements 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 decl = + let expression = Lambda {binder ; input_type ; output_type ; result ; body } in + let type_annotation = Some (Type_function (input_type, output_type)) in + Constant_declaration {name;annotated_expression = {expression;type_annotation}} + in + ok decl + ) + | lst -> ( + let%bind params = bind_map_list simpl_param lst in + let input = + let type_expression = Type_record ( + SMap.of_list + @@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression) + params + ) in + { type_name = "arguments" ; type_expression } in + let binder = input.type_name in + let input_type = input.type_expression in + let%bind local_declarations = + let%bind typed = bind_map_list simpl_local_declaration local_decls in + ok (List.map fst typed) + in + let%bind output_type = simpl_type_expression ret_type in + let%bind instructions = bind_list + @@ List.map simpl_statement + @@ npseq_to_list block.value.statements in + let%bind (body, result) = + let renamings = + let aux ({type_name}:named_type_expression) : Rename.Value.renaming = + type_name, ("arguments", [Record_access type_name]) + in + List.map aux params + in + let%bind r = + let%bind tmp = simpl_expression return in + Rename.Value.rename_annotated_expression renamings tmp + in + let%bind b = + let tmp = local_declarations @ instructions in + Rename.Value.rename_block renamings tmp + in + ok (b, r) in + let decl = + let expression = Lambda {binder ; input_type ; output_type ; result ; body } in + let type_annotation = Some (Type_function (input_type, output_type)) in + Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}} + in + ok decl + ) + ) + | LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet" + | LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet" + +and simpl_statement : Raw.statement -> instruction result = fun s -> + match s with + | Instr i -> simpl_instruction i + | Data d -> let%bind (i, _) = simpl_data_declaration d in ok i + +and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> + 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 = match c.ifso with + | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] + | ClauseBlock b -> simpl_statements @@ fst b.value.inside in + let%bind match_false = match c.ifnot with + | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] + | ClauseBlock b -> simpl_statements @@ fst b.value.inside 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 = + let aux (x : Raw.case Raw.reg) = + let%bind i = simpl_instruction_block x.value.instr in + ok (x.value.pattern, i) in + bind_list + @@ List.map aux + @@ 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 (record, [], inj) + | MapPatch _ -> simple_fail "no map patch yet" + | SetPatch _ -> simple_fail "no set patch yet" + | MapRemove _ -> simple_fail "no map remove yet" + | SetRemove _ -> simple_fail "no set remove yet" + +and simpl_cases : (Raw.pattern * block) list -> matching result = fun t -> + let open Raw in + let get_var (t:Raw.pattern) = match t with + | PVar v -> ok v.value + | _ -> simple_fail "not a var" + in + let%bind _assert = + trace_strong (simple_error "only pattern with two cases supported now") @@ + Assert.assert_equal_int 2 (List.length t) in + let ((pa, ba), (pb, bb)) = List.(hd t, hd @@ tl t) in + let uncons p = match p with + | PCons {value = (hd, _)} -> ok hd + | _ -> simple_fail "uncons fail" in + let%bind (pa, pb) = bind_map_pair uncons (pa, pb) in + match (pa, ba), (pb, bb) with + | (PFalse _, f), (PTrue _, t) + | (PTrue _, t), (PFalse _, f) -> 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 none patterns not supported yet" in + ok @@ Match_option {match_none = none ; match_some = (v, some) } + ) + | (PCons c, cons), (PList (PNil _), nil) + | (PList (PNil _), nil), (PCons c, cons) -> + 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 list patterns not supported yet" + in + ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil} + | _ -> + let error = simple_error "multi-level patterns not supported yet" in + fail error + +and simpl_instruction_block : Raw.instruction -> block result = fun t -> + match t with + | Single s -> let%bind i = simpl_single_instruction s in ok [ i ] + | Block b -> simpl_block b.value + +and simpl_instruction : Raw.instruction -> instruction result = fun t -> + match t with + | Single s -> simpl_single_instruction s + | Block _ -> simple_fail "no block instruction yet" + +and simpl_statements : Raw.statements -> block result = fun ss -> + let lst = npseq_to_list ss in + bind_map_list simpl_statement lst + +and simpl_block : Raw.block -> block result = fun t -> + simpl_statements t.statements + +let simpl_program : Raw.ast -> program result = fun t -> + bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index fa27b8e35..39253dbf6 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -154,6 +154,35 @@ let tuple () : unit result = in ok () +let option () : unit result = + let%bind program = type_file "./contracts/option.ligo" in + let open AST_Typed.Combinators in + let%bind _some = trace (simple_error "some") @@ + let%bind result = easy_evaluate_typed "s" program in + let expect = a_some (a_int 42) in + AST_Typed.assert_value_eq (expect, result) + in + let%bind _none = trace (simple_error "none") @@ + let%bind result = easy_evaluate_typed "n" program in + let expect = a_none make_t_int in + AST_Typed.assert_value_eq (expect, result) + in + ok () + +let map () : unit result = + let%bind program = type_file "./contracts/map.ligo" in + let ez lst = + let open AST_Typed.Combinators in + let lst' = List.map (fun (x, y) -> a_int x, a_int y) lst in + a_map lst' make_t_int make_t_int + in + let%bind _foobar = trace (simple_error "foobar") @@ + let%bind result = easy_evaluate_typed "fb" program in + let expect = ez [(23, 0) ; (42, 0)] in + AST_Typed.assert_value_eq (expect, result) + in + ok () + let condition () : unit result = let%bind program = type_file "./contracts/condition.ligo" in let aux n = @@ -170,6 +199,42 @@ let condition () : unit result = @@ [0 ; 2 ; 42 ; 163 ; -1] in ok () +let matching () : unit result = + let%bind program = type_file "./contracts/match.ligo" in + let%bind _bool = + let aux n = + let open AST_Typed.Combinators in + let input = a_int n in + let%bind result = easy_run_typed "match_bool" program input in + let%bind result' = + trace (simple_error "bad result") @@ + get_a_int result in + Assert.assert_equal_int (if n = 2 then 42 else 0) result' + in + let%bind _ = bind_list + @@ List.map aux + @@ [0 ; 2 ; 42 ; 163 ; -1] in + ok () + in + let%bind _option = + let aux n = + let open AST_Typed.Combinators in + let input = match n with + | Some s -> a_some (a_int s) + | None -> a_none (make_t_int) in + let%bind result = easy_run_typed "match_option" program input in + let%bind result' = + trace (simple_error "bad result") @@ + get_a_int result in + Assert.assert_equal_int (match n with None -> 23 | Some s -> s) result' + in + let%bind _ = bind_list + @@ List.map aux + @@ [Some 0 ; Some 2 ; Some 42 ; Some 163 ; Some (-1) ; None] in + ok () + in + ok () + let declarations () : unit result = let%bind program = type_file "./contracts/declarations.ligo" in let aux n = @@ -226,8 +291,11 @@ let main = "Integration (End to End)", [ test "unit" unit_expression ; test "record" record ; test "tuple" tuple ; + test "option" option ; + (* test "map" map ; *) test "multiple parameters" multiple_parameters ; test "condition" condition ; + test "matching" matching ; test "declarations" declarations ; test "quote declaration" quote_declaration ; test "quote declarations" quote_declarations ; diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 5de9e809c..b5cec2734 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -17,6 +17,12 @@ let rec translate_type (t:AST.type_value) : type_value result = | Type_constant ("int", []) -> ok (`Base Int) | Type_constant ("string", []) -> ok (`Base String) | Type_constant ("unit", []) -> ok (`Base Unit) + | Type_constant ("map", [key;value]) -> + let%bind kv' = bind_map_pair translate_type (key, value) in + ok (`Map kv') + | Type_constant ("option", [o]) -> + let%bind o' = translate_type o in + ok (`Option o') | Type_constant (name, _) -> fail (error "unrecognized constant" name) | Type_sum m -> let node = Append_tree.of_list @@ list_of_map m in @@ -68,13 +74,25 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in let env' = Environment.add (name, t) env in return ~env' (Assignment (name, expression)) - | Matching (expr, Match_bool {match_true ; match_false}) -> + | Matching (expr, m) -> ( let%bind expr' = translate_annotated_expression env expr in let env' = Environment.extend env in - let%bind true_branch = translate_block env' match_true in - let%bind false_branch = translate_block env' match_false in - return (Cond (expr', true_branch, false_branch)) - | Matching _ -> simple_fail "todo : match" + match m with + | Match_bool {match_true ; match_false} -> ( + let%bind true_branch = translate_block env' match_true in + let%bind false_branch = translate_block env' match_false in + return (Cond (expr', true_branch, false_branch)) + ) + | Match_option {match_none ; match_some = ((name, t), sm)} -> ( + let%bind none_branch = translate_block env' match_none in + let%bind some_branch = + let%bind t' = translate_type t in + let env' = Environment.add (name, t') env' in + translate_block env' sm in + return (If_None (expr', none_branch, (name, some_branch))) + ) + | _ -> simple_fail "todo : match" + ) | Loop (expr, body) -> let%bind expr' = translate_annotated_expression env expr in let%bind body' = translate_block env body in @@ -85,6 +103,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result = let%bind tv = translate_type ae.type_annotation in let return (expr, tv) = ok (expr, tv, env) in + let f = translate_annotated_expression env in match ae.expression with | Literal (Bool b) -> ok (Literal (`Bool b), tv, env) | Literal (Int n) -> ok (Literal (`Int n), tv, env) @@ -194,17 +213,26 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express Append_tree.fold_ne leaf node node_tv in ok expr | Constant (name, lst) -> - let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in - ok (Predicate (name, lst'), tv, env) + let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in ( + match name, lst with + | "NONE", [] -> + let%bind o = Mini_c.Combinators.get_t_option tv in + ok (Make_None o, tv, env) + | _ -> ok (Predicate (name, lst'), tv, env) + ) | Lambda l -> translate_lambda env l tv | Map m -> + let%bind (src, dst) = Mini_c.Combinators.get_t_map tv in let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev kv -> let%bind prev' = prev in let%bind (k', v') = bind_map_pair (translate_annotated_expression env) kv in return (Predicate ("UPDATE", [k' ; v' ; prev']), tv) in - let init = return (Predicate ("EMPTY", []), tv) in + let init = return (Empty_map (src, dst), tv) in List.fold_left aux init m + | LookUp dsi -> + let%bind (ds', i') = bind_map_pair f dsi in + return (Predicate ("GET", [ds' ; i']), tv) and translate_lambda_shallow env l tv = @@ -370,6 +398,13 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression | Type_constant ("string", []) -> let%bind n = get_string v in return (Literal (String n)) + | Type_constant ("option", [o]) -> ( + match%bind get_option v with + | None -> ok (a_none o) + | Some s -> + let%bind s' = untranspile s o in + ok (a_some s') + ) | Type_constant _ -> simple_fail "unknown type_constant" | Type_sum m -> diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 24a39f3c4..829943d4d 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -182,9 +182,10 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul @@ get_t_option t in let%bind match_none = type_block e match_none in let (n, b) = match_some in + let n' = n, t_opt in let e' = Environment.add e n t_opt in let%bind b' = type_block e' b in - ok (O.Match_option {match_none ; match_some = (n, b')}) + ok (O.Match_option {match_none ; match_some = (n', b')}) | Match_list {match_nil ; match_cons} -> let%bind t_list = trace_strong (simple_error "Matching list on not-an-list") @@ -362,7 +363,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | Constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in let tv_lst = List.map get_annotation lst' in - let%bind (name', tv) = type_constant name tv_lst in + let%bind (name', tv) = type_constant name tv_lst tv_opt in let%bind type_annotation = check tv in ok O.{expression = O.Constant (name', lst') ; type_annotation} | Application (f, arg) -> @@ -375,8 +376,15 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | _ -> simple_fail "applying to not-a-function" in ok O.{expression = Application (f, arg) ; type_annotation} + | LookUp dsi -> + let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in + let%bind (src, dst) = get_t_map ds.type_annotation in + let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in + let%bind type_annotation = check dst in + ok O.{expression = LookUp (ds, ind) ; type_annotation} -and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value) result = + +and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result = (* Constant poorman's polymorphism *) let open O in match (name, lst) with @@ -390,6 +398,14 @@ and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value | "OR", _ -> simple_fail "OR only defined over bool" | "AND", [a ; b] when type_value_eq (a, make_t_bool) && type_value_eq (b, make_t_bool) -> ok ("AND", make_t_bool) | "AND", _ -> simple_fail "AND only defined over bool" + | "NONE", [] -> ( + match tv_opt with + | Some t -> ok ("NONE", t) + | None -> simple_fail "untyped NONE" + ) + | "NONE", _ -> simple_fail "bad number of params to NONE" + | "SOME", [s] -> ok ("SOME", make_t_option s) + | "SOME", _ -> simple_fail "bad number of params to NONE" | name, _ -> fail @@ unrecognized_constant name let untype_type_value (t:O.type_value) : (I.type_expression) result = @@ -451,6 +467,9 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex | Map m -> let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in return (Map m') + | LookUp dsi -> + let%bind dsi' = bind_map_pair untype_annotated_expression dsi in + return (LookUp dsi') and untype_block (b:O.block) : (I.block) result = bind_list @@ List.map untype_instruction b @@ -487,7 +506,7 @@ and untype_matching (m:O.matching) : (I.matching) result = | Match_option {match_none ; match_some = (v, some)} -> let%bind match_none = untype_block match_none in let%bind some = untype_block some in - let match_some = v, some in + let match_some = fst v, some in ok @@ Match_option {match_none ; match_some} | Match_list {match_nil ; match_cons = (hd, tl, cons)} -> let%bind match_nil = untype_block match_nil in