balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

remove annotations from ast_simplified; make annotation expression explicit; locally very limited propagation of constraints in binding cases

Browse Source
This commit is contained in:
Galfour 2019-05-23 06:22:58 +00:00
parent 9d873c382b
commit c085dae123
14 changed files with 459 additions and 549 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

73
src/ast_simplified/PP.ml
View File

@ -33,48 +33,55 @@ let literal ppf (l:literal) = match l with
let rec expression ppf (e:expression) = match e with
| E_literal l -> literal ppf l
| E_variable name -> fprintf ppf "%s" name
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" annotated_expression f annotated_expression arg
| E_constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae
| E_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d annotated_expression) lst
| E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d annotated_expression) lst
| E_accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
| E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m
| E_list lst -> fprintf ppf "list[%a]" (list_sep_d annotated_expression) lst
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
| E_constructor (name, ae) -> fprintf ppf "%s(%a)" name expression ae
| E_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d expression) lst
| E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d expression) lst
| E_accessor (ae, p) -> fprintf ppf "%a.%a" expression ae access_path p
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d expression) m
| E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_expression) m
| E_list lst -> fprintf ppf "list[%a]" (list_sep_d expression) lst
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" expression ds expression ind
| E_lambda {binder;input_type;output_type;result} ->
fprintf ppf "lambda (%s:%a) : %a return %a"
binder (PP_helpers.option type_expression) input_type (PP_helpers.option type_expression) output_type
annotated_expression result
fprintf ppf "lambda (%a:%a) : %a return %a"
option_type_name binder
(PP_helpers.option type_expression) input_type (PP_helpers.option type_expression) output_type
expression result
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
fprintf ppf "match %a with %a" expression ae (matching expression) m
| E_failwith ae ->
fprintf ppf "failwith %a" annotated_expression ae
fprintf ppf "failwith %a" expression ae
| E_sequence (a , b) ->
fprintf ppf "%a ; %a"
annotated_expression a
annotated_expression b
expression a
expression b
| E_loop (expr , body) ->
fprintf ppf "%a ; %a"
annotated_expression expr
annotated_expression body
expression expr
expression body
| E_assign (name , path , expr) ->
fprintf ppf "%s.%a := %a"
name
PP_helpers.(list_sep access (const ".")) path
annotated_expression expr
expression expr
| E_let_in { binder ; rhs ; result } ->
fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
fprintf ppf "let %a = %a in %a" option_type_name binder expression rhs expression result
| E_skip -> fprintf ppf "skip"
| E_annotation (expr , ty) -> fprintf ppf "%a : %a" expression expr type_expression ty
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and option_type_name ppf ((name , ty_opt) : string * type_expression option) =
match ty_opt with
| None -> fprintf ppf "%s" name
| Some ty -> fprintf ppf "%s : %a" name type_expression ty
and assoc_expression ppf : (expr * expr) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" expression a expression b
and access ppf (a:access) =
match a with
| Access_tuple n -> fprintf ppf "%d" n
| Access_record s -> fprintf ppf "%s" s
| Access_map s -> fprintf ppf "(%a)" annotated_expression s
| Access_map s -> fprintf ppf "(%a)" expression s
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep access (const ".")) p
@ -83,17 +90,11 @@ and type_annotation ppf (ta:type_expression option) = match ta with
| None -> fprintf ppf ""
| Some t -> type_expression ppf t
and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotation with
| None -> fprintf ppf "%a" expression ae.expression
| Some t -> fprintf ppf "(%a) : %a" expression ae.expression type_expression t
and single_record_patch ppf ((p, expr) : string * expr) =
fprintf ppf "%s <- %a" p expression expr
and value : _ -> value -> unit = fun x -> annotated_expression x
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and single_tuple_patch ppf ((p, ae) : int * ae) =
fprintf ppf "%d <- %a" p annotated_expression ae
and single_tuple_patch ppf ((p, expr) : int * expr) =
fprintf ppf "%d <- %a" p expression expr
and matching_variant_case : type a . (_ -> a -> unit) -> _ -> (constructor_name * name) * a -> unit =
fun f ppf ((c,n),a) ->
@ -113,10 +114,10 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> u
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
let declaration ppf (d:declaration) = match d with
| Declaration_type {type_name ; type_expression = te} ->
| Declaration_type (type_name , te) ->
fprintf ppf "type %s = %a" type_name type_expression te
| Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
| Declaration_constant (name , ty_opt , expr) ->
fprintf ppf "const %a = %a" option_type_name (name , ty_opt) expression expr
let program ppf (p:program) =
fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) (List.map Location.unwrap p)

114
src/ast_simplified/combinators.ml
View File

@ -4,30 +4,6 @@ module Option = Simple_utils.Option
module SMap = Map.String
let get_name : named_expression -> string = fun x -> x.name
let get_type_name : named_type_expression -> string = fun x -> x.type_name
let get_type_annotation (x:annotated_expression) = x.type_annotation
let get_expression (x:annotated_expression) = x.expression
let named_expression name annotated_expression = { name ; annotated_expression }
let named_typed_expression name expression ty = { name ; annotated_expression = { expression ; type_annotation = Some ty } }
let typed_expression expression ty = { expression ; type_annotation = Some ty }
let untyped_expression expression = { expression ; type_annotation = None }
let merge_type_expression ae type_annotation = match ae.type_annotation with
| None -> ok { ae with type_annotation = Some type_annotation }
| Some _ -> simple_fail "merging already typed expression"
let merge_option_type_expression ae ta_opt = match (ae.type_annotation , ta_opt) with
| _ , None -> ok ae
| None , Some type_annotation -> ok { ae with type_annotation = Some type_annotation }
| _ -> simple_fail "merging already typed expression"
let get_untyped_expression : annotated_expression -> expression result = fun ae ->
let%bind () =
trace_strong (simple_error "expression is typed") @@
Assert.assert_none ae.type_annotation in
ok ae.expression
let t_bool : type_expression = T_constant ("bool", [])
let t_string : type_expression = T_constant ("string", [])
let t_bytes : type_expression = T_constant ("bytes", [])
@ -57,9 +33,6 @@ let ez_t_sum (lst:(string * type_expression) list) : type_expression =
let t_function param result : type_expression = T_function (param, result)
let t_map key value = (T_constant ("map", [key ; value]))
let make_e_a ?type_annotation expression = {expression ; type_annotation}
let make_e_a_full expression type_annotation = make_e_a ~type_annotation expression
let make_name (s : string) : name = s
let e_var (s : string) : expression = E_variable s
@ -76,6 +49,7 @@ let e_record map : expression = E_record map
let e_tuple lst : expression = E_tuple lst
let e_some s : expression = E_constant ("SOME", [s])
let e_none : expression = E_constant ("NONE", [])
let e_map_update k v old : expression = E_constant ("MAP_UPDATE" , [k ; v ; old])
let e_map lst : expression = E_map lst
let e_list lst : expression = E_list lst
let e_pair a b : expression = E_tuple [a; b]
@ -90,56 +64,24 @@ let e_skip = E_skip
let e_loop cond body = E_loop (cond , body)
let e_sequence a b = E_sequence (a , b)
let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
let e_annotation expr ty = E_annotation (expr , ty)
let e_application a b = E_application (a , b)
let e_a_unit : annotated_expression = make_e_a_full (e_unit ()) t_unit
let e_a_string s : annotated_expression = make_e_a_full (e_string s) t_string
let e_a_int n : annotated_expression = make_e_a_full (e_int n) t_int
let e_a_nat n : annotated_expression = make_e_a_full (e_nat n) t_nat
let e_a_bool b : annotated_expression = make_e_a_full (e_bool b) t_bool
let e_a_list lst : annotated_expression = make_e_a (e_list lst)
let e_a_constructor s a : annotated_expression = make_e_a (e_constructor s a)
let e_a_address x = make_e_a_full (e_address x) t_address
let e_a_tez x = make_e_a_full (e_tez x) t_tez
let e_a_sequence a b : annotated_expression = make_e_a (e_sequence a b)
let e_binop name a b = E_constant (name , [a ; b])
let e_a_record r =
let type_annotation = Option.(
map ~f:t_record (bind_map_smap get_type_annotation r)
) in
make_e_a ?type_annotation (e_record r)
let ez_e_a_record lst =
let ez_e_record lst =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
e_a_record map
e_record map
let e_a_tuple lst =
let type_annotation = Option.(
map ~f:t_tuple (bind_map_list get_type_annotation lst)
) in
make_e_a ?type_annotation (e_tuple lst)
let e_a_pair a b =
let type_annotation = Option.(
map ~f:t_pair
@@ bind_map_pair get_type_annotation (a , b)
) in
make_e_a ?type_annotation (e_pair a b)
let e_a_some opt =
let type_annotation = Option.(
map ~f:t_option (get_type_annotation opt)
) in
make_e_a ?type_annotation (e_some opt)
let e_a_typed_none t_opt =
let e_typed_none t_opt =
let type_annotation = t_option t_opt in
make_e_a ~type_annotation e_none
e_annotation e_none type_annotation
let e_a_typed_list lst t =
make_e_a ~type_annotation:(t_list t) (e_list lst)
let e_typed_list lst t =
e_annotation (e_list lst) (t_list t)
let e_a_map lst k v = make_e_a ~type_annotation:(t_map k v) (e_map lst)
let e_map lst k v = e_annotation (e_map lst) (t_map k v)
let e_lambda (binder : string)
(input_type : type_expression option)
@ -147,36 +89,24 @@ let e_lambda (binder : string)
(result : expression)
: expression =
E_lambda {
binder = (make_name binder) ;
binder = (make_name binder , input_type) ;
input_type = input_type ;
output_type = output_type ;
result = (make_e_a result) ;
result ;
}
let e_tuple (lst : ae list) : expression = E_tuple lst
let ez_e_tuple (lst : expression list) : expression =
e_tuple (List.map make_e_a lst)
let e_constructor (s : string) (e : ae) : expression = E_constructor (make_name s, e)
let e_record (lst : (string * ae) list) : expression =
let e_record (lst : (string * expr) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
E_record map
let ez_e_record (lst : (string * expression) list) : expression =
(* TODO: define a correct implementation of List.map
* (an implementation that does not fail with stack overflow) *)
e_record (List.map (fun (s,e) -> (s, make_e_a e)) lst)
let get_a_accessor = fun t ->
match t.expression with
let get_e_accessor = fun t ->
match t with
| E_accessor (a , b) -> ok (a , b)
| _ -> simple_fail "not an accessor"
let assert_a_accessor = fun t ->
let%bind _ = get_a_accessor t in
let assert_e_accessor = fun t ->
let%bind _ = get_e_accessor t in
ok ()
let get_access_record : access -> string result = fun a ->
@ -185,12 +115,12 @@ let get_access_record : access -> string result = fun a ->
| Access_map _ -> simple_fail "not an access record"
| Access_record s -> ok s
let get_a_pair = fun t ->
match t.expression with
let get_e_pair = fun t ->
match t with
| E_tuple [a ; b] -> ok (a , b)
| _ -> simple_fail "not a pair"
let get_a_list = fun t ->
match t.expression with
let get_e_list = fun t ->
match t with
| E_list lst -> ok lst
| _ -> simple_fail "not a pair"

21
src/ast_simplified/misc.ml
View File

@ -30,14 +30,16 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_operation _, _ -> simple_fail "operation vs non-operation"
let rec assert_value_eq (a, b: (value*value)) : unit result =
let rec assert_value_eq (a, b: (expression * expression )) : unit result =
let error_content () =
Format.asprintf "\n@[<v>- %a@;- %a]" PP.value a PP.value b
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
in
trace (fun () -> error (thunk "not equal") error_content ()) @@
match (a.expression, b.expression) with
match (a , b) with
| E_literal a , E_literal b ->
assert_literal_eq (a, b)
| E_literal _ , _ ->
simple_fail "comparing a literal with not a literal"
| E_constant (ca, lsta) , E_constant (cb, lstb) when ca = cb -> (
let%bind lst =
generic_try (simple_error "constants with different number of elements")
@ -50,8 +52,8 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
| E_constant _ , _ ->
let error_content () =
Format.asprintf "%a vs %a"
PP.annotated_expression a
PP.annotated_expression b
PP.expression a
PP.expression b
in
fail @@ (fun () -> error (thunk "comparing constant with other stuff") error_content ())
@ -111,8 +113,13 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
)
| E_list _, _ ->
simple_fail "comparing list with other stuff"
| _, _ -> simple_fail "comparing not a value"
| (E_annotation (a , _) , b) -> assert_value_eq (a , b)
| (a , E_annotation (b , _)) -> assert_value_eq (a , b)
| (E_variable _, _) | (E_lambda _, _)
| (E_application _, _) | (E_let_in _, _)
| (E_accessor _, _)
| (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _) | (E_sequence _, _)
| (E_loop _, _) | (E_assign _, _) | (E_skip, _) -> simple_fail "comparing not a value"
(* module Rename = struct

69
src/ast_simplified/types.ml
View File

@ -12,31 +12,14 @@ type 'a type_name_map = 'a Map.String.t
type program = declaration Location.wrap list
and declaration =
| Declaration_type of named_type_expression
| Declaration_constant of named_expression
| Declaration_type of (type_name * type_expression)
| Declaration_constant of (name * type_expression option * expression)
(* | Macro_declaration of macro_declaration *)
and value = annotated_expression
and annotated_expression = {
expression: expression ;
type_annotation: te option ;
}
and named_expression = {
name: name ;
annotated_expression: ae ;
}
and named_type_expression = {
type_name: type_name ;
type_expression: type_expression ;
}
and expr = expression
and te = type_expression
and ae = annotated_expression
and te_map = type_expression type_name_map
and ae_map = annotated_expression name_map
and expr_map = expression name_map
and type_expression =
| T_tuple of te list
@ -47,50 +30,52 @@ and type_expression =
| T_constant of type_name * te list
and lambda = {
binder : name ;
binder : (name * type_expression option) ;
input_type : type_expression option ;
output_type : type_expression option ;
result : ae ;
result : expr ;
}
and let_in = {
binder : name;
rhs : ae;
result : ae;
binder : (name * type_expression option) ;
rhs : expr ;
result : expr ;
}
and expression =
(* Base *)
| E_literal of literal
| E_constant of (name * ae list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_constant of (name * expr list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_variable of name
| E_lambda of lambda
| E_application of (ae * ae)
| E_application of (expr * expr)
| E_let_in of let_in
(* E_Tuple *)
| E_tuple of ae list
| E_tuple of expr list
(* Sum *)
| E_constructor of (name * ae) (* For user defined constructors *)
| E_constructor of (name * expr) (* For user defined constructors *)
(* E_record *)
| E_record of ae_map
| E_accessor of (ae * access_path)
| E_record of expr_map
| E_accessor of (expr * access_path)
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_look_up of (ae * ae)
| E_map of (expr * expr) list
| E_list of expr list
| E_look_up of (expr * expr)
(* Matching *)
| E_matching of (ae * matching_expr)
| E_failwith of ae
| E_matching of (expr * matching_expr)
| E_failwith of expr
(* Replace Statements *)
| E_sequence of (ae * ae)
| E_loop of (ae * ae)
| E_assign of (name * access_path * ae)
| E_sequence of (expr * expr)
| E_loop of (expr * expr)
| E_assign of (name * access_path * expr)
| E_skip
(* Annotate *)
| E_annotation of expr * type_expression
and access =
| Access_tuple of int
| Access_record of string
| Access_map of ae
| Access_map of expr
and access_path = access list
@ -121,4 +106,4 @@ and 'a matching =
| Match_tuple of name list * 'a
| Match_variant of ((constructor_name * name) * 'a) list
and matching_expr = annotated_expression matching
and matching_expr = expression matching

8
src/ast_typed/misc.ml
View File

@ -347,8 +347,12 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
)
| E_list _, _ ->
simple_fail "comparing list with other stuff"
| _, _ -> simple_fail "comparing not a value"
| (E_literal _, _) | (E_variable _, _) | (E_application _, _)
| (E_lambda _, _) | (E_let_in _, _) | (E_tuple_accessor _, _)
| (E_record_accessor _, _)
| (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _)
| (E_assign _ , _)
| (E_sequence _, _) | (E_loop _, _)-> simple_fail "comparing not a value"
let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
match a, b with

7
src/main/contract.ml
View File

@ -2,14 +2,13 @@ open Trace
include struct
open Ast_simplified
open Combinators
let assert_entry_point_defined : program -> string -> unit result =
fun program entry_point ->
let aux : declaration -> bool = fun declaration ->
match declaration with
| Declaration_type _ -> false
| Declaration_constant ne -> get_name ne = entry_point
| Declaration_constant (name , _ , _) -> name = entry_point
in
trace_strong (simple_error "no entry-point with given name") @@
Assert.assert_true @@ List.exists aux @@ List.map Location.unwrap program
@ -113,7 +112,7 @@ let compile_contract_parameter : string -> string -> string -> string result = f
| Declaration_constant (_ , (_ , post_env)) -> post_env
in
trace (simple_error "typing expression") @@
Typer.type_annotated_expression env simplified in
Typer.type_expression env simplified in
let%bind () =
trace (simple_error "expression type doesn't match type parameter") @@
Ast_typed.assert_type_value_eq (parameter_tv , typed.type_annotation) in
@ -161,7 +160,7 @@ let compile_contract_storage : string -> string -> string -> string result = fun
| Declaration_constant (_ , (_ , post_env)) -> post_env
in
trace (simple_error "typing expression") @@
Typer.type_annotated_expression env simplified in
Typer.type_expression env simplified in
let%bind () =
trace (simple_error "expression type doesn't match type storage") @@
Ast_typed.assert_type_value_eq (storage_tv , typed.type_annotation) in

16
src/main/main.ml
View File

@ -13,15 +13,15 @@ module Transpiler = Transpiler
let simplify (p:AST_Raw.t) : Ast_simplified.program result = Simplify.Pascaligo.simpl_program p
let simplify_expr (e:AST_Raw.expr) : Ast_simplified.annotated_expression result = Simplify.Pascaligo.simpl_expression e
let unparse_simplified_expr (e:AST_Simplified.annotated_expression) : string result =
ok @@ Format.asprintf "%a" AST_Simplified.PP.annotated_expression e
let simplify_expr (e:AST_Raw.expr) : Ast_simplified.expression result = Simplify.Pascaligo.simpl_expression e
let unparse_simplified_expr (e:AST_Simplified.expression) : string result =
ok @@ Format.asprintf "%a" AST_Simplified.PP.expression e
let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p
let type_expression ?(env:Typer.Environment.t = Typer.Environment.full_empty)
(e:AST_Simplified.annotated_expression) : AST_Typed.annotated_expression result =
Typer.type_annotated_expression env e
let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression result = Typer.untype_annotated_expression e
(e:AST_Simplified.expression) : AST_Typed.annotated_expression result =
Typer.type_expression env e
let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.expression result = Typer.untype_expression e
let transpile (p:AST_Typed.program) : Mini_c.program result = Transpiler.translate_program p
let transpile_entry (p:AST_Typed.program) (name:string) : Mini_c.anon_function result = Transpiler.translate_entry p name
@ -72,7 +72,7 @@ let easy_evaluate_typed (entry:string) (program:AST_Typed.program) : AST_Typed.a
untranspile_value result typed_main.type_annotation in
ok typed_result
let easy_evaluate_typed_simplified (entry:string) (program:AST_Typed.program) : Ast_simplified.annotated_expression result =
let easy_evaluate_typed_simplified (entry:string) (program:AST_Typed.program) : Ast_simplified.expression result =
let%bind result =
let%bind mini_c_main =
transpile_entry program entry in
@ -126,7 +126,7 @@ let easy_run_typed
let easy_run_typed_simplified
?(debug_mini_c = false) ?(debug_michelson = false) ?options (entry:string)
(program:AST_Typed.program) (input:Ast_simplified.annotated_expression) : Ast_simplified.annotated_expression result =
(program:AST_Typed.program) (input:Ast_simplified.expression) : Ast_simplified.expression result =
let%bind mini_c_main =
trace (simple_error "transpile mini_c entry") @@
transpile_entry program entry in

121
src/simplify/camligo.ml
View File

@ -180,21 +180,20 @@ let rec of_restricted_type_expression : I.restricted_type_expression -> I.type_e
let restricted_type_expression : I.restricted_type_expression -> O.type_expression result =
Function.compose type_expression of_restricted_type_expression
let rec expression : I.expression -> O.annotated_expression result = fun e ->
let rec expression : I.expression -> O.expression result = fun e ->
match e with
| I.E_sequence lst -> (
let%bind lst' = bind_map_list expression @@ List.map unwrap lst in
match lst' with
| [] -> simple_fail "empty sequence"
| hd :: tl -> ok @@ List.fold_right' (fun prec cur -> untyped_expression @@ e_sequence prec cur) hd tl
| hd :: tl -> ok @@ List.fold_right' (fun prec cur -> e_sequence prec cur) hd tl
)
| I.E_let_in (pattern , expr , body) -> (
let%bind (name , rte) = get_p_option_typed_variable @@ unwrap pattern in
let%bind type_expression' = bind_map_option (fun x -> restricted_type_expression @@ unwrap x) rte in
let%bind expr' = expression @@ unwrap expr in
let%bind expr'' = merge_option_type_expression expr' type_expression' in
let%bind body' = expression @@ unwrap body in
ok @@ untyped_expression @@ e_let_in (unwrap name) expr'' body'
ok @@ e_let_in (unwrap name , type_expression') expr' body'
)
| I.E_ifthenelse ite -> ifthenelse ite
| I.E_ifthen it -> ifthen it
@ -205,34 +204,31 @@ let rec expression : I.expression -> O.annotated_expression result = fun e ->
let name' = unwrap name in
let%bind type_expression' = restricted_type_expression (unwrap rte) in
let%bind expr' = expression (unwrap expr) in
ok @@ untyped_expression @@ E_lambda {
binder = name' ;
input_type = Some type_expression' ;
output_type = None ;
result = expr' ;
}
ok @@ e_lambda name'
(Some type_expression') None
expr'
)
| I.E_main m -> expression_main m
and ifthenelse
: (I.expression Location.wrap * I.expression Location.wrap * I.expression Location.wrap) -> O.annotated_expression result
: (I.expression Location.wrap * I.expression Location.wrap * I.expression Location.wrap) -> O.expression result
= fun ite ->
let (cond , branch_true , branch_false) = ite in
let%bind cond' = bind_map_location expression cond in
let%bind branch_true' = bind_map_location expression branch_true in
let%bind branch_false' = bind_map_location expression branch_false in
ok @@ O.(untyped_expression @@ e_match_bool (unwrap cond') (unwrap branch_true') (unwrap branch_false'))
ok @@ O.(e_match_bool (unwrap cond') (unwrap branch_true') (unwrap branch_false'))
and ifthen
: (I.expression Location.wrap * I.expression Location.wrap) -> O.annotated_expression result
: (I.expression Location.wrap * I.expression Location.wrap) -> O.expression result
= fun it ->
let (cond , branch_true) = it in
let%bind cond' = bind_map_location expression cond in
let%bind branch_true' = bind_map_location expression branch_true in
ok @@ O.(untyped_expression @@ e_match_bool (unwrap cond') (unwrap branch_true') e_a_unit)
ok @@ O.(e_match_bool (unwrap cond') (unwrap branch_true') (e_unit ()))
and match_
: I.expression Location.wrap * I.e_match_clause Location.wrap list -> O.annotated_expression result
: I.expression Location.wrap * I.e_match_clause Location.wrap list -> O.expression result
= fun m ->
let (expr , clauses) = m in
let%bind expr' = expression (unwrap expr) in
@ -246,7 +242,7 @@ and match_
ok (x' , y') in
bind_map_list aux clauses in
let%bind matching = match_clauses clauses' in
ok O.(untyped_expression @@ e_match expr' matching)
ok O.(e_match expr' matching)
and record
= fun r ->
@ -259,13 +255,13 @@ and record
in
let%bind r' = bind_map_list (bind_map_location aux) r in
let lst = List.map ((fun (x, y) -> unwrap x, unwrap y) >| unwrap) r' in
ok @@ O.(untyped_expression @@ e_record lst)
ok @@ O.(e_record lst)
and expression_main : I.expression_main Location.wrap -> O.annotated_expression result = fun em ->
let return x = ok @@ untyped_expression x in
and expression_main : I.expression_main Location.wrap -> O.expression result = fun em ->
let return x = ok @@ x in
let simple_binop name ab =
let%bind (a' , b') = bind_map_pair expression_main ab in
return @@ E_constant (name, [a' ; b']) in
return @@ e_binop name a' b' in
let error_main =
let title () = "simplifying main_expression" in
let content () = Format.asprintf "%a" I.pp_expression_main (unwrap em) in
@ -275,7 +271,7 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression
match (unwrap em) with
| Eh_tuple lst ->
let%bind lst' = bind_map_list expression_main lst in
return @@ E_tuple lst'
return @@ e_tuple lst'
| Eh_module_ident (lst , v) -> identifier_application (lst , v) None
| Eh_variable v -> identifier_application ([] , v) None
| Eh_application (f , arg) -> (
@ -285,15 +281,14 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression
| Eh_module_ident (lst , v) -> identifier_application (lst , v) (Some arg')
| _ -> (
let%bind f' = expression_main f in
return @@ E_application (f' , arg')
return @@ e_application f' arg'
)
)
| Eh_type_annotation (e, te) ->
let%bind e' =
| Eh_type_annotation (e, te) -> (
let%bind e' = expression_main e in
get_untyped_expression e' in
let%bind te' = bind_map_location restricted_type_expression te in
ok @@ typed_expression e' (unwrap te')
ok @@ e_annotation e' (unwrap te')
)
| Eh_lt ab ->
simple_binop "LT" ab
| Eh_gt ab ->
@ -315,20 +310,20 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression
| Eh_division ab ->
simple_binop "DIV" ab
| Eh_int n ->
return @@ E_literal (Literal_int (unwrap n))
return @@ e_int (unwrap n)
| Eh_string s ->
return @@ E_literal (Literal_string (unwrap s))
return @@ e_string (unwrap s)
| Eh_unit _ ->
return @@ E_literal Literal_unit
return @@ e_unit ()
| Eh_tz n ->
return @@ E_literal (Literal_tez (unwrap n))
return @@ e_tez (unwrap n)
| Eh_constructor _ ->
simple_fail "constructor without parameter"
| Eh_data_structure (kind , content) -> (
match unwrap kind with
| "list" -> (
let%bind lst = bind_map_list expression_main content in
ok @@ untyped_expression @@ E_list lst
ok @@ e_list lst
)
| kind' -> (
let error =
@ -343,30 +338,30 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression
| Eh_assign x ->
simple_binop "ASSIGN" x
| Eh_accessor (src , path) ->
ok @@ O.(untyped_expression @@ e_accessor_props (untyped_expression @@ e_variable (unwrap src)) (List.map unwrap path))
ok @@ O.(e_accessor_props (e_variable (unwrap src)) (List.map unwrap path))
| Eh_bottom e ->
expression (unwrap e)
and identifier_application : (string Location.wrap) list * string Location.wrap -> O.value option -> _ result = fun (lst , v) param_opt ->
and identifier_application : (string Location.wrap) list * string Location.wrap -> O.expression option -> _ result = fun (lst , v) param_opt ->
let constant_name = String.concat "." ((List.map unwrap lst) @ [unwrap v]) in
match List.assoc_opt constant_name constants , param_opt with
| Some 0 , None ->
ok O.(untyped_expression @@ E_constant (constant_name , []))
ok O.(E_constant (constant_name , []))
| Some _ , None ->
simple_fail "n-ary constant without parameter"
| Some 0 , Some _ -> simple_fail "applying to nullary constant"
| Some 1 , Some param -> (
ok O.(untyped_expression @@ E_constant (constant_name , [param]))
ok O.(E_constant (constant_name , [param]))
)
| Some n , Some param -> (
let params =
match get_expression param with
match param with
| E_tuple lst -> lst
| _ -> [ param ] in
let%bind () =
trace_strong (simple_error "bad constant arity") @@
Assert.assert_list_size params n in
ok O.(untyped_expression @@ E_constant (constant_name , params))
ok O.(E_constant (constant_name , params))
)
| None , param_opt -> (
let%bind () =
@ -376,10 +371,10 @@ and identifier_application : (string Location.wrap) list * string Location.wrap
error title content in
trace_strong error @@
Assert.assert_list_empty lst in
match constant_name , param_opt with
| "failwith" , Some param -> ok O.(untyped_expression @@ e_failwith param)
| _ , Some param -> ok O.(untyped_expression @@ E_application (untyped_expression @@ E_variable (unwrap v) , param))
| _ , None -> ok O.(untyped_expression @@ e_variable (unwrap v))
match (constant_name , param_opt) with
| "failwith" , Some param -> ok O.(e_failwith param)
| _ , Some param -> ok @@ e_application (e_variable (unwrap v)) param
| _ , None -> ok @@ e_variable (unwrap v)
)
let let_content : I.let_content -> _ result = fun l ->
@ -394,11 +389,8 @@ let let_content : I.let_content -> _ result = fun l ->
bind_map_location type_expression ty in
match args' with
| [] -> ( (* No arguments. Simplify as regular value. *)
let%bind e' =
let%bind e' = bind_map_location expression e in
bind_map_location O.Combinators.get_untyped_expression e' in
let ae = make_e_a_full (unwrap e') (unwrap ty') in
ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = ae}
ok @@ O.Declaration_constant (unwrap n , Some (unwrap ty') , unwrap e')
)
| [_param] ->
simple_fail "no syntactic sugar for functions yet param"
@ -423,35 +415,30 @@ let let_entry : _ -> _ result = fun l ->
ok (param_name' , param_ty') in
let%bind storage_name = get_untyped_variable_param (unwrap storage) in
let storage_ty = O.T_variable "storage" in
let input_nty =
let ty = O.T_tuple [param_ty ; storage_ty] in
let nty = O.{type_name = "arguments" ; type_expression = ty} in
let (arguments_name , input_ty) =
let ty = t_tuple [param_ty ; storage_ty] in
let nty = ("arguments" , ty) in
nty in
let input = O.Combinators.typed_expression (E_variable input_nty.type_name) input_nty.type_expression in
let tpl_declarations =
let aux = fun i (name , type_expression) expr ->
untyped_expression @@ e_let_in name (
make_e_a_full
(O.E_accessor (input , [ Access_tuple i ]))
type_expression
) expr
e_let_in
(name , Some type_expression)
(e_accessor (e_variable arguments_name) [ Access_tuple i ])
expr
in
let lst = List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)] in
fun expr -> List.fold_right' (fun prec cur -> cur prec) expr lst
in
let%bind result = expression (unwrap e) in
let result = tpl_declarations result in
let input_type' = input_nty.type_expression in
let input_type' = input_ty in
let output_type' = O.(t_pair (t_list t_operation , storage_ty)) in
let lambda =
O.{
binder = input_nty.type_name ;
input_type = Some input_type';
output_type = Some output_type';
result ;
} in
let lambda = e_lambda
arguments_name
(Some input_ty) (Some output_type')
result in
let type_annotation = Some (O.T_function (input_type', output_type')) in
ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = {expression = O.E_lambda lambda ; type_annotation}}
ok @@ O.Declaration_constant (unwrap n , type_annotation , lambda)
let let_init_storage : _ -> _ result = fun l ->
let (args , ty_opt , e) = l in
@ -462,11 +449,11 @@ let let_init_storage : _ -> _ result = fun l ->
trace (simple_error "storage init should have no parameter (address)") @@
Assert.assert_list_size args 0 in
let%bind content =
let%bind ae = bind_map_location expression e in
bind_map_location get_untyped_expression ae
let%bind expr = bind_map_location expression e in
ok expr
in
let type_annotation = O.t_variable "storage" in
ok @@ O.(Declaration_constant (named_typed_expression "storage" (unwrap content) type_annotation))
ok @@ O.(Declaration_constant ("storage" , Some type_annotation , (unwrap content)))
let let_init_content : I.let_content -> _ result = fun l ->
@ -482,7 +469,7 @@ let statement : I.statement -> O.declaration result = fun s ->
| Statement_entry_declaration x -> let_entry (unwrap x)
| Statement_type_declaration (n, te) ->
let%bind te' = bind_map_location type_expression te in
ok @@ O.Declaration_type {type_name = unwrap n ; type_expression = unwrap te'}
ok @@ O.Declaration_type (unwrap n , unwrap te')
let program : I.program -> O.program result = fun (Program lst) ->
bind_map_list (bind_map_location statement) lst

169
src/simplify/pascaligo.ml
View File

@ -18,15 +18,15 @@ let type_constants = Operators.Simplify.type_constants
let constants = Operators.Simplify.constants
let return expr = ok @@ fun expr'_opt ->
let expr = untyped_expression expr in
let expr = expr in
match expr'_opt with
| None -> ok @@ expr
| Some expr' -> ok @@ e_a_sequence expr expr'
| Some expr' -> ok @@ e_sequence expr expr'
let return_let_in binder rhs = ok @@ fun expr'_opt ->
match expr'_opt with
| None -> simple_fail "missing return" (* Hard to explain. Shouldn't happen in prod. *)
| Some expr' -> ok @@ untyped_expression @@ e_let_in binder rhs expr'
| Some expr' -> ok @@ e_let_in binder rhs expr'
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
match t with
@ -92,12 +92,12 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
let%bind lst = bind_list @@ List.map simpl_type_expression lst in
ok @@ T_tuple lst
let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
let rec simpl_expression (t:Raw.expr) : expr result =
let return x = ok x in
let simpl_projection = fun (p:Raw.projection) ->
let var =
let name = p.struct_name.value in
make_e_a @@ E_variable name in
e_variable name in
let path = p.field_path in
let path' =
let aux (s:Raw.selection) =
@ -111,13 +111,9 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
match t with
| EAnnot a -> (
let (expr , type_expr) = a.value in
match te_annot with
| None -> (
let%bind te_annot = simpl_type_expression type_expr in
let%bind expr' = simpl_expression ~te_annot expr in
ok expr'
)
| Some _ -> simple_fail "no double annotation"
let%bind expr' = simpl_expression expr in
let%bind type_expr' = simpl_type_expression type_expr in
return @@ e_annotation expr' type_expr'
)
| EVar c -> (
let c' = c.value in
@ -139,7 +135,7 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
match List.assoc_opt f constants with
| None ->
let%bind arg = simpl_tuple_expression args' in
return @@ E_application (make_e_a @@ E_variable f, arg)
return @@ E_application (e_variable f, arg)
| Some arity ->
let%bind _arity =
trace (simple_error "wrong arity for constants") @@
@ -147,12 +143,12 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
let%bind lst = bind_map_list simpl_expression args' in
return @@ E_constant (f, lst)
)
| EPar x -> simpl_expression ?te_annot x.value.inside
| EPar x -> simpl_expression x.value.inside
| EUnit _ -> return @@ E_literal Literal_unit
| EBytes x -> return @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
| ETuple tpl ->
let (Raw.TupleInj tpl') = tpl in
simpl_tuple_expression ?te_annot
simpl_tuple_expression
@@ npseq_to_list tpl'.value.inside
| ERecord r ->
let%bind fields = bind_list
@ -180,15 +176,15 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
| EConstr (NoneExpr _) ->
return @@ E_constant ("NONE" , [])
| EArith (Add c) ->
simpl_binop ?te_annot "ADD" c.value
simpl_binop "ADD" c.value
| EArith (Sub c) ->
simpl_binop ?te_annot "SUB" c.value
simpl_binop "SUB" c.value
| EArith (Mult c) ->
simpl_binop ?te_annot "TIMES" c.value
simpl_binop "TIMES" c.value
| EArith (Div c) ->
simpl_binop ?te_annot "DIV" c.value
simpl_binop "DIV" c.value
| EArith (Mod c) ->
simpl_binop ?te_annot "MOD" c.value
simpl_binop "MOD" c.value
| EArith (Int n) ->
let n = Z.to_int @@ snd @@ n.value in
return @@ E_literal (Literal_int n)
@ -206,8 +202,8 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
in
return @@ E_literal (Literal_string s')
| EString _ -> simple_fail "string: not supported yet"
| ELogic l -> simpl_logic_expression ?te_annot l
| EList l -> simpl_list_expression ?te_annot l
| ELogic l -> simpl_logic_expression l
| EList l -> simpl_list_expression l
| ESet _ -> simple_fail "set: not supported yet"
| ECase c ->
let%bind e = simpl_expression c.value.expr in
@ -224,7 +220,7 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
| EMap (MapInj mi) ->
let%bind lst =
let lst = List.map get_value @@ pseq_to_list mi.value.elements in
let aux : Raw.binding -> (annotated_expression * annotated_expression) result = fun b ->
let aux : Raw.binding -> (expression * expression) result = fun b ->
let%bind src = simpl_expression b.source in
let%bind dst = simpl_expression b.image in
ok (src, dst) in
@ -238,37 +234,37 @@ let rec simpl_expression ?te_annot (t:Raw.expr) : ae result =
let%bind index = simpl_expression lu.value.index.value.inside in
return (E_look_up (path, index))
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
and simpl_logic_expression (t:Raw.logic_expr) : expression result =
let return x = ok x in
match t with
| BoolExpr (False _) ->
return @@ E_literal (Literal_bool false)
| BoolExpr (True _) ->
return @@ E_literal (Literal_bool true)
| BoolExpr (Or b) ->
simpl_binop ?te_annot "OR" b.value
simpl_binop "OR" b.value
| BoolExpr (And b) ->
simpl_binop ?te_annot "AND" b.value
simpl_binop "AND" b.value
| BoolExpr (Not b) ->
simpl_unop ?te_annot "NOT" b.value
simpl_unop "NOT" b.value
| CompExpr (Lt c) ->
simpl_binop ?te_annot "LT" c.value
simpl_binop "LT" c.value
| CompExpr (Gt c) ->
simpl_binop ?te_annot "GT" c.value
simpl_binop "GT" c.value
| CompExpr (Leq c) ->
simpl_binop ?te_annot "LE" c.value
simpl_binop "LE" c.value
| CompExpr (Geq c) ->
simpl_binop ?te_annot "GE" c.value
simpl_binop "GE" c.value
| CompExpr (Equal c) ->
simpl_binop ?te_annot "EQ" c.value
simpl_binop "EQ" c.value
| CompExpr (Neq c) ->
simpl_binop ?te_annot "NEQ" c.value
simpl_binop "NEQ" c.value
and simpl_list_expression ?te_annot (t:Raw.list_expr) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
and simpl_list_expression (t:Raw.list_expr) : expression result =
let return x = ok x in
match t with
| Cons c ->
simpl_binop ?te_annot "CONS" c.value
simpl_binop "CONS" c.value
| List lst ->
let%bind lst' =
bind_map_list simpl_expression @@
@ -277,22 +273,22 @@ and simpl_list_expression ?te_annot (t:Raw.list_expr) : annotated_expression res
| Nil _ ->
return @@ E_list []
and simpl_binop ?te_annot (name:string) (t:_ Raw.bin_op) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
and simpl_binop (name:string) (t:_ Raw.bin_op) : expression result =
let return x = ok x in
let%bind a = simpl_expression t.arg1 in
let%bind b = simpl_expression t.arg2 in
return @@ E_constant (name, [a;b])
and simpl_unop ?te_annot (name:string) (t:_ Raw.un_op) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
and simpl_unop (name:string) (t:_ Raw.un_op) : expression result =
let return x = ok x in
let%bind a = simpl_expression t.arg in
return @@ E_constant (name, [a])
and simpl_tuple_expression ?te_annot (lst:Raw.expr list) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
and simpl_tuple_expression (lst:Raw.expr list) : expression result =
let return x = ok x in
match lst with
| [] -> return @@ E_literal Literal_unit
| [hd] -> simpl_expression ?te_annot hd
| [hd] -> simpl_expression hd
| lst ->
let%bind lst = bind_list @@ List.map simpl_expression lst in
return @@ E_tuple lst
@ -305,8 +301,8 @@ and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
and simpl_lambda_declaration : Raw.lambda_decl -> _ result = fun l ->
match l with
| FunDecl f ->
let%bind e = simpl_fun_declaration (f.value) in
return_let_in e.name e.annotated_expression
let%bind (name , e) = simpl_fun_declaration (f.value) in
return_let_in name e
| ProcDecl _ -> simple_fail "no local procedure yet"
| EntryDecl _ -> simple_fail "no local entry-point yet"
@ -316,29 +312,29 @@ and simpl_data_declaration : Raw.data_decl -> _ result = fun t ->
let x = x.value in
let name = x.name.value in
let%bind t = simpl_type_expression x.var_type in
let%bind annotated_expression = simpl_expression ~te_annot:t x.init in
return_let_in name annotated_expression
let%bind expression = simpl_expression x.init in
return_let_in (name , Some t) expression
| LocalConst x ->
let x = x.value in
let name = x.name.value in
let%bind t = simpl_type_expression x.const_type in
let%bind annotated_expression = simpl_expression ~te_annot:t x.init in
return_let_in name annotated_expression
let%bind expression = simpl_expression x.init in
return_let_in (name , Some t) expression
and simpl_param : Raw.param_decl -> named_type_expression result = fun t ->
and simpl_param : Raw.param_decl -> (type_name * 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 }
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 }
ok (type_name , type_expression)
and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * expression) result = fun x ->
let open! Raw in
let {name;param;ret_type;local_decls;block;return} : fun_decl = x in
(match npseq_to_list param.value.inside with
@ -346,8 +342,7 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
| [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 (binder , input_type) = input in
let%bind local_declarations =
bind_map_list simpl_local_declaration local_decls in
let%bind instructions = bind_list
@ -360,31 +355,25 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression = E_lambda {
binder ;
binder = (binder , Some input_type) ;
input_type = Some input_type ;
output_type = Some output_type ;
result
} in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name;annotated_expression = {expression;type_annotation}}
ok ((name , type_annotation) , expression)
)
| lst -> (
let arguments_name = "arguments" in
let%bind params = bind_map_list simpl_param lst in
let input =
let aux = fun x -> x.type_expression in
let type_expression = T_tuple (List.map aux params) in
{ type_name = arguments_name ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let (binder , input_type) =
let type_expression = T_tuple (List.map snd params) in
(arguments_name , type_expression) in
let%bind tpl_declarations =
let aux = fun i (x:named_type_expression) ->
let expr = E_accessor ({
expression = E_variable arguments_name ;
type_annotation = Some input.type_expression ;
} , [ Access_tuple i ]) in
let type_ = x.type_expression in
let ass = return_let_in x.type_name (make_e_a_full expr type_) in
let aux = fun i x ->
let expr = E_accessor (E_variable arguments_name , [ Access_tuple i ]) in
let type_ = Some (snd x) in
let ass = return_let_in (fst x , type_) expr in
ass
in
bind_list @@ List.mapi aux params in
@ -400,13 +389,13 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression = E_lambda {
binder ;
binder = (binder , Some input_type) ;
input_type = Some input_type ;
output_type = Some output_type ;
result
} in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name = name.value;annotated_expression = {expression;type_annotation}}
ok ((name.value , type_annotation) , expression)
)
)
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
@ -416,29 +405,29 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
| TypeDecl x ->
let {name;type_expr} : Raw.type_decl = x.value in
let%bind type_expression = simpl_type_expression type_expr in
ok @@ loc x @@ Declaration_type {type_name=name.value;type_expression}
ok @@ loc x @@ Declaration_type (name.value , type_expression)
| ConstDecl x ->
let simpl_const_decl = fun {name;const_type;init} ->
let%bind expression = simpl_expression init in
let%bind t = simpl_type_expression const_type in
let type_annotation = Some t in
ok @@ Declaration_constant {name=name.value;annotated_expression={expression with type_annotation}}
ok @@ Declaration_constant (name.value , type_annotation , expression)
in
bind_map_location simpl_const_decl (Location.lift_region x)
| LambdaDecl (FunDecl x) ->
let aux f x =
let%bind x' = f x in
ok @@ Declaration_constant x' in
let%bind ((name , ty_opt) , expr) = f x in
ok @@ Declaration_constant (name , ty_opt , expr) in
bind_map_location (aux simpl_fun_declaration) (Location.lift_region x)
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
and simpl_statement : Raw.statement -> (_ -> annotated_expression result) result = fun s ->
and simpl_statement : Raw.statement -> (_ -> expression result) result = fun s ->
match s with
| Instr i -> simpl_instruction i
| Data d -> simpl_data_declaration d
and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression result) result = fun t ->
and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) result = fun t ->
match t with
| ProcCall _ -> simple_fail "no proc call"
| Fail e -> (
@ -483,8 +472,8 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression re
| Name name -> ok name
| _ -> simple_fail "no complex map assignments yet" in
let%bind key_expr = simpl_expression v'.index.value.inside in
let old_expr = make_e_a @@ E_variable name.value in
let expr' = make_e_a @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in
let old_expr = e_variable name.value in
let expr' = e_map_update key_expr value_expr old_expr in
return @@ E_assign (name.value , [] , expr')
)
)
@ -517,7 +506,7 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression re
| [] -> simple_fail "empty record patch"
| hd :: tl -> (
let aux acc cur =
e_sequence (untyped_expression acc) (untyped_expression cur)
e_sequence (acc) (cur)
in
ok @@ List.fold_left aux hd tl
)
@ -533,8 +522,8 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression re
| Name v -> ok v.value
| _ -> simple_fail "no complex map remove yet" in
let%bind key' = simpl_expression key in
let expr = E_constant ("MAP_REMOVE", [key' ; make_e_a (E_variable map)]) in
return @@ E_assign (map , [] , make_e_a expr)
let expr = E_constant ("MAP_REMOVE", [key' ; e_variable map]) in
return @@ E_assign (map , [] , expr)
| SetRemove _ -> simple_fail "no set remove yet"
and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
@ -629,12 +618,12 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
bind_map_list aux lst in
ok @@ Match_variant constrs
and simpl_instruction_block : Raw.instruction -> (_ -> annotated_expression result) result = fun t ->
and simpl_instruction_block : Raw.instruction -> (_ -> expression result) result = fun t ->
match t with
| Single s -> simpl_single_instruction s
| Block b -> simpl_block b.value
and simpl_instruction : Raw.instruction -> (_ -> annotated_expression result) result = fun t ->
and simpl_instruction : Raw.instruction -> (_ -> expression result) result = fun t ->
let main_error =
let title () = "simplifiying instruction" in
let content () = Format.asprintf "%a" PP_helpers.(printer Parser.Pascaligo.ParserLog.print_instruction) t in
@ -644,17 +633,17 @@ and simpl_instruction : Raw.instruction -> (_ -> annotated_expression result) re
| Single s -> simpl_single_instruction s
| Block _ -> simple_fail "no block instruction yet"
and simpl_statements : Raw.statements -> (_ -> annotated_expression result) result = fun ss ->
and simpl_statements : Raw.statements -> (_ -> expression result) result = fun ss ->
let lst = npseq_to_list ss in
let%bind fs = bind_map_list simpl_statement lst in
let aux : _ -> (annotated_expression option -> annotated_expression result) -> _ = fun prec cur ->
let aux : _ -> (expression option -> expression result) -> _ = fun prec cur ->
let%bind res = cur prec in
ok @@ Some res in
ok @@ fun (expr' : _ option) ->
let%bind ret = bind_fold_right_list aux expr' fs in
ok @@ Option.unopt_exn ret
and simpl_block : Raw.block -> (_ -> annotated_expression result) result = fun t ->
and simpl_block : Raw.block -> (_ -> expression result) result = fun t ->
simpl_statements t.statements
let simpl_program : Raw.ast -> program result = fun t ->

74
src/test/coase_tests.ml
View File

@ -17,9 +17,9 @@ let get_program =
open Ast_simplified
let card owner =
ez_e_a_record [
ez_e_record [
("card_owner" , owner) ;
("card_pattern" , e_a_nat 0) ;
("card_pattern" , e_nat 0) ;
]
let card_ty = t_record_ez [
@ -27,14 +27,14 @@ let card_ty = t_record_ez [
("card_pattern" , t_nat) ;
]
let card_ez owner = card (e_a_address owner)
let card_ez owner = card (e_address owner)
let make_cards assoc_lst =
let card_id_ty = t_nat in
e_a_map assoc_lst card_id_ty card_ty
e_map assoc_lst card_id_ty card_ty
let card_pattern (coeff , qtt) =
ez_e_a_record [
ez_e_record [
("coefficient" , coeff) ;
("quantity" , qtt) ;
]
@ -46,25 +46,25 @@ let card_pattern_ty =
]
let card_pattern_ez (coeff , qtt) =
card_pattern (e_a_tez coeff , e_a_nat qtt)
card_pattern (e_tez coeff , e_nat qtt)
let make_card_patterns lst =
let card_pattern_id_ty = t_nat in
let assoc_lst = List.mapi (fun i x -> (e_a_nat i , x)) lst in
e_a_map assoc_lst card_pattern_id_ty card_pattern_ty
let assoc_lst = List.mapi (fun i x -> (e_nat i , x)) lst in
e_map assoc_lst card_pattern_id_ty card_pattern_ty
let storage cards_patterns cards next_id =
ez_e_a_record [
ez_e_record [
("cards" , cards) ;
("card_patterns" , cards_patterns) ;
("next_id" , next_id) ;
]
let storage_ez cps cs next_id =
storage (make_card_patterns cps) (make_cards cs) (e_a_nat next_id)
storage (make_card_patterns cps) (make_cards cs) (e_nat next_id)
let cards_ez owner n =
List.mapi (fun i x -> (e_a_nat i , x))
List.mapi (fun i x -> (e_nat i , x))
@@ List.map card_ez
@@ List.map (Function.constant owner)
@@ List.range n
@ -92,21 +92,21 @@ let buy () =
let%bind program = get_program () in
let%bind () =
let make_input = fun n ->
let buy_action = ez_e_a_record [
("card_to_buy" , e_a_nat 0) ;
let buy_action = ez_e_record [
("card_to_buy" , e_nat 0) ;
] in
let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
e_a_pair buy_action storage
e_pair buy_action storage
in
let make_expected = fun n ->
let ops = e_a_typed_list [] t_operation in
let ops = e_typed_list [] t_operation in
let storage =
let cards =
cards_ez first_owner n @
[(e_a_nat (2 * n) , card (e_a_address second_owner))]
[(e_nat (2 * n) , card (e_address second_owner))]
in
basic 101 1000 cards ((2 * n) + 1) in
e_a_pair ops storage
e_pair ops storage
in
let%bind () =
let%bind amount =
@ -130,22 +130,22 @@ let dispatch_buy () =
let%bind program = get_program () in
let%bind () =
let make_input = fun n ->
let buy_action = ez_e_a_record [
("card_to_buy" , e_a_nat 0) ;
let buy_action = ez_e_record [
("card_to_buy" , e_nat 0) ;
] in
let action = e_a_constructor "Buy_single" buy_action in
let action = e_constructor "Buy_single" buy_action in
let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
e_a_pair action storage
e_pair action storage
in
let make_expected = fun n ->
let ops = e_a_typed_list [] t_operation in
let ops = e_typed_list [] t_operation in
let storage =
let cards =
cards_ez first_owner n @
[(e_a_nat (2 * n) , card (e_a_address second_owner))]
[(e_nat (2 * n) , card (e_address second_owner))]
in
basic 101 1000 cards ((2 * n) + 1) in
e_a_pair ops storage
e_pair ops storage
in
let%bind () =
let%bind amount =
@ -169,23 +169,23 @@ let transfer () =
let%bind program = get_program () in
let%bind () =
let make_input = fun n ->
let transfer_action = ez_e_a_record [
("card_to_transfer" , e_a_nat 0) ;
("destination" , e_a_address second_owner) ;
let transfer_action = ez_e_record [
("card_to_transfer" , e_nat 0) ;
("destination" , e_address second_owner) ;
] in
let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
e_a_pair transfer_action storage
e_pair transfer_action storage
in
let make_expected = fun n ->
let ops = e_a_typed_list [] t_operation in
let ops = e_typed_list [] t_operation in
let storage =
let cards =
let new_card = card_ez second_owner in
let old_cards = cards_ez first_owner n in
(e_a_nat 0 , new_card) :: (List.tl old_cards)
(e_nat 0 , new_card) :: (List.tl old_cards)
in
basic 100 1000 cards (2 * n) in
e_a_pair ops storage
e_pair ops storage
in
let%bind () =
let amount = Memory_proto_alpha.Alpha_context.Tez.zero in
@ -200,17 +200,17 @@ let sell () =
let%bind program = get_program () in
let%bind () =
let make_input = fun n ->
let sell_action = ez_e_a_record [
("card_to_sell" , e_a_nat (n - 1)) ;
let sell_action = ez_e_record [
("card_to_sell" , e_nat (n - 1)) ;
] in
let cards = cards_ez first_owner n in
let storage = basic 100 1000 cards (2 * n) in
e_a_pair sell_action storage
e_pair sell_action storage
in
let make_expecter : int -> annotated_expression -> unit result = fun n result ->
let%bind (ops , storage) = get_a_pair result in
let make_expecter : int -> expression -> unit result = fun n result ->
let%bind (ops , storage) = get_e_pair result in
let%bind () =
let%bind lst = get_a_list ops in
let%bind lst = get_e_list ops in
Assert.assert_list_size lst 1 in
let expected_storage =
let cards = List.hds @@ cards_ez first_owner n in

160
src/test/integration_tests.ml
View File

@ -23,13 +23,13 @@ let assign () : unit result =
let annotation () : unit result =
let%bind program = type_file "./contracts/annotation.ligo" in
let%bind () =
expect_eq_evaluate program "lst" (e_a_list [])
expect_eq_evaluate program "lst" (e_list [])
in
let%bind () =
expect_eq_evaluate program "address" (e_a_address "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx")
expect_eq_evaluate program "address" (e_address "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx")
in
let%bind () =
expect_eq_evaluate program "address_2" (e_a_address "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx")
expect_eq_evaluate program "address_2" (e_address "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx")
in
ok ()
@ -41,25 +41,25 @@ let complex_function () : unit result =
let variant () : unit result =
let%bind program = type_file "./contracts/variant.ligo" in
let%bind () =
let expected = e_a_constructor "Foo" (e_a_int 42) in
let expected = e_constructor "Foo" (e_int 42) in
expect_eq_evaluate program "foo" expected in
let%bind () =
let expected = e_a_constructor "Bar" (e_a_bool true) in
let expected = e_constructor "Bar" (e_bool true) in
expect_eq_evaluate program "bar" expected in
let%bind () =
let expected = e_a_constructor "Kee" (e_a_nat 23) in
let expected = e_constructor "Kee" (e_nat 23) in
expect_eq_evaluate program "kee" expected in
ok ()
let variant_matching () : unit result =
let%bind program = type_file "./contracts/variant-matching.ligo" in
let%bind () =
let make_input = fun n -> e_a_constructor "Foo" (e_a_int n) in
let make_expected = e_a_int in
let make_input = fun n -> e_constructor "Foo" (e_int n) in
let make_expected = e_int in
expect_eq program "fb" (make_input 0) (make_expected 0) >>? fun () ->
expect_eq_n program "fb" make_input make_expected >>? fun () ->
expect_eq program "fb" (e_a_constructor "Kee" (e_a_nat 50)) (e_a_int 23) >>? fun () ->
expect_eq program "fb" (e_a_constructor "Bar" (e_a_bool true)) (e_a_int 42) >>? fun () ->
expect_eq program "fb" (e_constructor "Kee" (e_nat 50)) (e_int 23) >>? fun () ->
expect_eq program "fb" (e_constructor "Bar" (e_bool true)) (e_int 42) >>? fun () ->
ok ()
in
ok ()
@ -98,7 +98,7 @@ let shared_function () : unit result =
in
let%bind () =
let make_expect = fun n -> (2 * n + 3) in
expect_eq program "foo" (e_a_int 0) (e_a_int @@ make_expect 0)
expect_eq program "foo" (e_int 0) (e_int @@ make_expect 0)
in
let%bind () =
let make_expect = fun n -> (2 * n + 3) in
@ -128,30 +128,30 @@ let arithmetic () : unit result =
("times_op", fun n -> (n * 42)) ;
(* ("div_op", fun n -> (n / 2)) ; *)
] in
let%bind () = expect_eq_n_pos program "int_op" e_a_nat e_a_int in
let%bind () = expect_eq_n_pos program "mod_op" e_a_int (fun n -> e_a_nat (n mod 42)) in
let%bind () = expect_eq_n_pos program "div_op" e_a_int (fun n -> e_a_int (n / 2)) in
let%bind () = expect_eq_n_pos program "int_op" e_nat e_int in
let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in
let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in
ok ()
let unit_expression () : unit result =
let%bind program = type_file "./contracts/unit.ligo" in
expect_eq_evaluate program "u" e_a_unit
expect_eq_evaluate program "u" (e_unit ())
let string_expression () : unit result =
let%bind program = type_file "./contracts/string.ligo" in
expect_eq_evaluate program "s" (e_a_string "toto")
expect_eq_evaluate program "s" (e_string "toto")
let include_ () : unit result =
let%bind program = type_file "./contracts/includer.ligo" in
expect_eq_evaluate program "bar" (e_a_int 144)
expect_eq_evaluate program "bar" (e_int 144)
let record_ez_int names n =
ez_e_a_record @@ List.map (fun x -> x, e_a_int n) names
ez_e_record @@ List.map (fun x -> x, e_int n) names
let multiple_parameters () : unit result =
let%bind program = type_file "./contracts/multiple-parameters.ligo" in
let aux ((name : string) , make_input , make_output) =
let make_output' = fun n -> e_a_int @@ make_output n in
let make_output' = fun n -> e_int @@ make_output n in
expect_eq_n program name make_input make_output'
in
let%bind _ = bind_list @@ List.map aux [
@ -168,27 +168,27 @@ let record () : unit result =
expect_eq_evaluate program "fb" expected
in
let%bind () =
let%bind () = expect_eq_evaluate program "a" (e_a_int 42) in
let%bind () = expect_eq_evaluate program "b" (e_a_int 142) in
let%bind () = expect_eq_evaluate program "c" (e_a_int 242) in
let%bind () = expect_eq_evaluate program "a" (e_int 42) in
let%bind () = expect_eq_evaluate program "b" (e_int 142) in
let%bind () = expect_eq_evaluate program "c" (e_int 242) in
ok ()
in
let%bind () =
let make_input = record_ez_int ["foo" ; "bar"] in
let make_expected = fun n -> e_a_int (2 * n) in
let make_expected = fun n -> e_int (2 * n) in
expect_eq_n program "projection" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["foo" ; "bar"] in
let make_expected = fun n -> ez_e_a_record [("foo" , e_a_int 256) ; ("bar" , e_a_int n) ] in
let make_expected = fun n -> ez_e_record [("foo" , e_int 256) ; ("bar" , e_int n) ] in
expect_eq_n program "modify" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["a" ; "b" ; "c"] in
let make_expected = fun n -> ez_e_a_record [
("a" , e_a_int n) ;
("b" , e_a_int 2048) ;
("c" , e_a_int n)
let make_expected = fun n -> ez_e_record [
("a" , e_int n) ;
("b" , e_int 2048) ;
("c" , e_int n)
] in
expect_eq_n program "modify_abc" make_input make_expected
in
@ -201,19 +201,19 @@ let record () : unit result =
let tuple () : unit result =
let%bind program = type_file "./contracts/tuple.ligo" in
let ez n =
e_a_tuple (List.map e_a_int n) in
e_tuple (List.map e_int n) in
let%bind () =
let expected = ez [0 ; 0] in
expect_eq_evaluate program "fb" expected
in
let%bind () =
let make_input = fun n -> ez [n ; n] in
let make_expected = fun n -> e_a_int (2 * n) in
let make_expected = fun n -> e_int (2 * n) in
expect_eq_n program "projection" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [n ; 2 * n ; n] in
let make_expected = fun n -> e_a_int (2 * n) in
let make_expected = fun n -> e_int (2 * n) in
expect_eq_n program "projection_abc" make_input make_expected
in
let%bind () =
@ -235,11 +235,11 @@ let tuple () : unit result =
let option () : unit result =
let%bind program = type_file "./contracts/option.ligo" in
let%bind () =
let expected = e_a_some (e_a_int 42) in
let expected = e_some (e_int 42) in
expect_eq_evaluate program "s" expected
in
let%bind () =
let expected = e_a_typed_none t_int in
let expected = e_typed_none t_int in
expect_eq_evaluate program "n" expected
in
ok ()
@ -248,17 +248,17 @@ let map () : unit result =
let%bind program = type_file "./contracts/map.ligo" in
let ez lst =
let open Ast_simplified.Combinators in
let lst' = List.map (fun (x, y) -> e_a_int x, e_a_int y) lst in
e_a_map lst' t_int t_int
let lst' = List.map (fun (x, y) -> e_int x, e_int y) lst in
e_map lst' t_int t_int
in
let%bind () =
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
let make_expected = e_a_int in
let make_expected = e_int in
expect_eq_n program "gf" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez List.(map (fun x -> (x, x)) @@ range n) in
let make_expected = e_a_nat in
let make_expected = e_nat in
expect_eq_n_strict_pos_small program "size_" make_input make_expected
in
let%bind () =
@ -268,14 +268,14 @@ let map () : unit result =
let%bind () =
let make_input = fun n ->
let m = ez [(23 , 0) ; (42 , 0)] in
e_a_tuple [(e_a_int n) ; m]
e_tuple [(e_int n) ; m]
in
let make_expected = fun n -> ez [(23 , n) ; (42 , 0)] in
expect_eq_n_pos_small program "set_" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
let make_expected = fun _ -> e_a_some @@ e_a_int 4 in
let make_expected = fun _ -> e_some @@ e_int 4 in
expect_eq_n program "get" make_input make_expected
in
let%bind () =
@ -292,12 +292,12 @@ let map () : unit result =
let list () : unit result =
let%bind program = type_file "./contracts/list.ligo" in
let ez lst =
let lst' = List.map e_a_int lst in
e_a_typed_list lst' t_int
let lst' = List.map e_int lst in
e_typed_list lst' t_int
in
let%bind () =
let make_input = fun n -> (ez @@ List.range n) in
let make_expected = e_a_nat in
let make_expected = e_nat in
expect_eq_n_strict_pos_small program "size_" make_input make_expected
in
let%bind () =
@ -312,31 +312,31 @@ let list () : unit result =
let condition () : unit result =
let%bind program = type_file "./contracts/condition.ligo" in
let make_input = e_a_int in
let make_expected = fun n -> e_a_int (if n = 2 then 42 else 0) in
let make_input = e_int in
let make_expected = fun n -> e_int (if n = 2 then 42 else 0) in
expect_eq_n program "main" make_input make_expected
let condition_simple () : unit result =
let%bind program = type_file "./contracts/condition-simple.ligo" in
let make_input = e_a_int in
let make_expected = fun _ -> e_a_int 42 in
let make_input = e_int in
let make_expected = fun _ -> e_int 42 in
expect_eq_n program "main" make_input make_expected
let loop () : unit result =
let%bind program = type_file "./contracts/loop.ligo" in
let%bind () =
let make_input = e_a_nat in
let make_expected = e_a_nat in
let make_input = e_nat in
let make_expected = e_nat in
expect_eq_n_pos program "dummy" make_input make_expected
in
let%bind () =
let make_input = e_a_nat in
let make_expected = e_a_nat in
let make_input = e_nat in
let make_expected = e_nat in
expect_eq_n_pos_mid program "counter" make_input make_expected
in
let%bind () =
let make_input = e_a_nat in
let make_expected = fun n -> e_a_nat (n * (n + 1) / 2) in
let make_input = e_nat in
let make_expected = fun n -> e_nat (n * (n + 1) / 2) in
expect_eq_n_pos_mid program "sum" make_input make_expected
in
ok()
@ -345,21 +345,21 @@ let loop () : unit result =
let matching () : unit result =
let%bind program = type_file "./contracts/match.ligo" in
let%bind () =
let make_input = e_a_int in
let make_expected = fun n -> e_a_int (if n = 2 then 42 else 0) in
let make_input = e_int in
let make_expected = fun n -> e_int (if n = 2 then 42 else 0) in
expect_eq_n program "match_bool" make_input make_expected
in
let%bind () =
let make_input = e_a_int in
let make_expected = fun n-> e_a_int (if n = 2 then 42 else 0) in
let make_input = e_int in
let make_expected = fun n-> e_int (if n = 2 then 42 else 0) in
expect_eq_n program "match_expr_bool" make_input make_expected
in
let%bind () =
let aux n =
let input = match n with
| Some s -> e_a_some (e_a_int s)
| None -> e_a_typed_none t_int in
let expected = e_a_int (match n with
| Some s -> e_some (e_int s)
| None -> e_typed_none t_int in
let expected = e_int (match n with
| Some s -> s
| None -> 23) in
trace (simple_error (Format.asprintf "on input %a" PP_helpers.(option int) n)) @@
@ -371,9 +371,9 @@ let matching () : unit result =
let%bind () =
let aux n =
let input = match n with
| Some s -> e_a_some (e_a_int s)
| None -> e_a_typed_none t_int in
let expected = e_a_int (match n with
| Some s -> e_some (e_int s)
| None -> e_typed_none t_int in
let expected = e_int (match n with
| Some s -> s
| None -> 42) in
trace (simple_error (Format.asprintf "on input %a" PP_helpers.(option int) n)) @@
@ -386,53 +386,53 @@ let matching () : unit result =
let declarations () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" in
let make_input = e_a_int in
let make_expected = fun n -> e_a_int (42 + n) in
let make_input = e_int in
let make_expected = fun n -> e_int (42 + n) in
expect_eq program "main" (make_input 0) (make_expected 0) >>? fun () ->
expect_eq_n program "main" make_input make_expected
let declaration_local () : unit result =
let%bind program = type_file "./contracts/declaration-local.ligo" in
let make_input = e_a_int in
let make_expected = fun _ -> e_a_int 42 in
let make_input = e_int in
let make_expected = fun _ -> e_int 42 in
expect_eq_n program "main" make_input make_expected
let quote_declaration () : unit result =
let%bind program = type_file "./contracts/quote-declaration.ligo" in
let make_input = e_a_int in
let make_expected = fun n -> e_a_int (42 + 2 * n) in
let make_input = e_int in
let make_expected = fun n -> e_int (42 + 2 * n) in
expect_eq_n program "main" make_input make_expected
let quote_declarations () : unit result =
let%bind program = type_file "./contracts/quote-declarations.ligo" in
let make_input = e_a_int in
let make_expected = fun n -> e_a_int (74 + 2 * n) in
let make_input = e_int in
let make_expected = fun n -> e_int (74 + 2 * n) in
expect_eq_n program "main" make_input make_expected
let counter_contract () : unit result =
let%bind program = type_file "./contracts/counter.ligo" in
let make_input = fun n-> e_a_pair (e_a_int n) (e_a_int 42) in
let make_expected = fun n -> e_a_pair (e_a_typed_list [] t_operation) (e_a_int (42 + n)) in
let make_input = fun n-> e_pair (e_int n) (e_int 42) in
let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
expect_eq_n program "main" make_input make_expected
let super_counter_contract () : unit result =
let%bind program = type_file "./contracts/super-counter.ligo" in
let make_input = fun n ->
let action = if n mod 2 = 0 then "Increment" else "Decrement" in
e_a_pair (e_a_constructor action (e_a_int n)) (e_a_int 42) in
e_pair (e_constructor action (e_int n)) (e_int 42) in
let make_expected = fun n ->
let op = if n mod 2 = 0 then (+) else (-) in
e_a_pair (e_a_typed_list [] t_operation) (e_a_int (op 42 n)) in
e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
expect_eq_n program "main" make_input make_expected
let dispatch_counter_contract () : unit result =
let%bind program = type_file "./contracts/dispatch-counter.ligo" in
let make_input = fun n ->
let action = if n mod 2 = 0 then "Increment" else "Decrement" in
e_a_pair (e_a_constructor action (e_a_int n)) (e_a_int 42) in
e_pair (e_constructor action (e_int n)) (e_int 42) in
let make_expected = fun n ->
let op = if n mod 2 = 0 then (+) else (-) in
e_a_pair (e_a_typed_list [] t_operation) (e_a_int (op 42 n)) in
e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
expect_eq_n program "main" make_input make_expected
let basic_mligo () : unit result =
@ -442,14 +442,14 @@ let basic_mligo () : unit result =
let counter_mligo () : unit result =
let%bind program = mtype_file "./contracts/counter.mligo" in
let make_input = fun n-> e_a_pair (e_a_int n) (e_a_int 42) in
let make_expected = fun n -> e_a_pair (e_a_typed_list [] t_operation) (e_a_int (42 + n)) in
let make_input = fun n-> e_pair (e_int n) (e_int 42) in
let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
expect_eq_n program "main" make_input make_expected
let guess_the_hash_mligo () : unit result =
let%bind program = mtype_file "./contracts/new-syntax.mligo" in
let make_input = fun n-> e_a_pair (e_a_int n) (e_a_int 42) in
let make_expected = fun n -> e_a_pair (e_a_typed_list [] t_operation) (e_a_int (42 + n)) in
let make_input = fun n-> e_pair (e_int n) (e_int 42) in
let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
expect_eq_n program "main" make_input make_expected
let main = "Integration (End to End)", [

10
src/test/test_helpers.ml
View File

@ -28,8 +28,8 @@ let expect_eq ?options program entry_point input expected =
let expect_error =
let title () = "expect result" in
let content () = Format.asprintf "Expected %a, got %a"
Ast_simplified.PP.value expected
Ast_simplified.PP.value result in
Ast_simplified.PP.expression expected
Ast_simplified.PP.expression result in
error title content in
trace expect_error @@
Ast_simplified.assert_value_eq (expected , result) in
@ -83,7 +83,7 @@ let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]
let expect_eq_b program entry_point make_expected =
let aux b =
let input = e_a_bool b in
let input = e_bool b in
let expected = make_expected b in
expect_eq program entry_point input expected
in
@ -91,8 +91,8 @@ let expect_eq_b program entry_point make_expected =
ok ()
let expect_eq_n_int a b c =
expect_eq_n a b e_a_int (fun n -> e_a_int (c n))
expect_eq_n a b e_int (fun n -> e_int (c n))
let expect_eq_b_bool a b c =
let open Ast_simplified.Combinators in
expect_eq_b a b (fun bool -> e_a_bool (c bool))
expect_eq_b a b (fun bool -> e_bool (c bool))

12
src/test/typer_tests.ml
View File

@ -8,10 +8,10 @@ module Simplified = Ligo.AST_Simplified
let int () : unit result =
let open Combinators in
let pre = make_e_a @@ e_int 32 in
let pre = e_int 32 in
let open Typer in
let e = Environment.full_empty in
let%bind post = type_annotated_expression e pre in
let%bind post = type_expression e pre in
let open! Typed in
let open Combinators in
let%bind () = assert_type_value_eq (post.type_annotation, t_int ()) in
@ -21,10 +21,10 @@ module TestExpressions = struct
let test_expression ?(env = Typer.Environment.full_empty)
(expr : expression)
(test_expected_ty : Typed.tv) =
let pre = Combinators.make_e_a @@ expr in
let pre = expr in
let open Typer in
let open! Typed in
let%bind post = type_annotated_expression env pre in
let%bind post = type_expression env pre in
let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
ok ()
@ -45,7 +45,7 @@ module TestExpressions = struct
let tuple () : unit result =
test_expression
I.(ez_e_tuple [e_int 32; e_string "foo"])
I.(e_tuple [e_int 32; e_string "foo"])
O.(t_tuple [t_int (); t_string ()] ())
let constructor () : unit result =
@ -53,7 +53,7 @@ module TestExpressions = struct
O.[("foo", t_int ()); ("bar", t_string ())]
in test_expression
~env:(E.env_sum_type variant_foo_bar)
I.(e_constructor "foo" (make_e_a @@ e_int 32))
I.(e_constructor "foo" (e_int 32))
O.(make_t_ez_sum variant_foo_bar)
let record () : unit result =

140
src/typer/typer.ml
View File

@ -39,11 +39,11 @@ module Errors = struct
let full () = Format.asprintf "%a" I.PP.program p in
error title full ()
let constant_declaration_error (name:string) (ae:I.ae) () =
let constant_declaration_error (name:string) (ae:I.expr) () =
let title = (thunk "typing constant declaration") in
let full () =
Format.asprintf "%s = %a" name
I.PP.annotated_expression ae
I.PP.expression ae
in
error title full ()
end
@ -64,16 +64,18 @@ let rec type_program (p:I.program) : O.program result =
ok @@ List.rev lst
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
| Declaration_type {type_name;type_expression} ->
| Declaration_type (type_name , type_expression) ->
let%bind tv = evaluate_type env type_expression in
let env' = Environment.add_type type_name tv env in
ok (env', None)
| Declaration_constant {name;annotated_expression} ->
| Declaration_constant (name , tv_opt , expression) -> (
let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
let%bind ae' =
trace (constant_declaration_error name annotated_expression) @@
type_annotated_expression env annotated_expression in
trace (constant_declaration_error name expression) @@
type_expression ?tv_opt:tv'_opt env expression in
let env' = Environment.add_ez_ae name ae' env in
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
)
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =
fun f e t i -> match i with
@ -195,21 +197,20 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_constant(cst, lst'))
and type_annotated_expression : environment -> I.annotated_expression -> O.annotated_expression result = fun e ae ->
and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
let module L = Logger.Stateful() in
let%bind tv_opt = match ae.type_annotation with
| None -> ok None
| Some s -> let%bind r = evaluate_type e s in ok (Some r) in
let check tv = O.(merge_annotation tv_opt (Some tv)) in
let return expr tv =
let%bind type_annotation = check tv in
ok @@ make_a_e expr type_annotation e in
let%bind () =
match tv_opt with
| None -> ok ()
| Some tv' -> O.assert_type_value_eq (tv' , tv) in
ok @@ make_a_e expr tv e in
let main_error =
let title () = "typing annotated_expression" in
let content () = Format.asprintf "Expression: %a\nLog: %s\n" I.PP.annotated_expression ae (L.get()) in
let title () = "typing expression" in
let content () = Format.asprintf "Expression: %a\nLog: %s\n" I.PP.expression ae (L.get()) in
error title content in
trace main_error @@
match ae.expression with
match ae with
(* Basic *)
| E_failwith _ -> simple_fail "can't type failwith in isolation"
| E_variable name ->
@ -241,11 +242,11 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (e_operation op) (t_operation ())
(* Tuple *)
| E_tuple lst ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
let tv_lst = List.map get_type_annotation lst' in
return (E_tuple lst') (t_tuple tv_lst ())
| E_accessor (ae, path) ->
let%bind e' = type_annotated_expression e ae in
let%bind e' = type_expression e ae in
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
match a with
| Access_tuple index -> (
@ -263,7 +264,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (E_record_accessor (prev , property)) tv
)
| Access_map ae -> (
let%bind ae' = type_annotated_expression e ae in
let%bind ae' = type_expression e ae in
let%bind (k , v) = get_t_map prev.type_annotation in
let%bind () =
Ast_typed.assert_type_value_eq (k , get_type_annotation ae') in
@ -285,20 +286,20 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
error title content in
trace_option error @@
Environment.get_constructor c e in
let%bind expr' = type_annotated_expression e expr in
let%bind expr' = type_expression e expr in
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
return (E_constructor (c , expr')) sum_tv
(* Record *)
| E_record m ->
let aux prev k expr =
let%bind expr' = type_annotated_expression e expr in
let%bind expr' = type_expression e expr in
ok (SMap.add k expr' prev)
in
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
return (E_record m') (t_record (SMap.map get_type_annotation m') ())
(* Data-structure *)
| E_list lst ->
let%bind lst' = bind_map_list (type_annotated_expression e) lst in
let%bind lst' = bind_map_list (type_expression e) lst in
let%bind tv =
let aux opt c =
match opt with
@ -319,7 +320,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
in
return (E_list lst') tv
| E_map lst ->
let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in
let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
let%bind tv =
let aux opt c =
match opt with
@ -364,18 +365,18 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
trace_option (simple_error "no output type provided") @@
output_type in
evaluate_type e output_type in
let e' = Environment.add_ez_binder binder input_type e in
let%bind result = type_annotated_expression e' result in
return (E_lambda {binder;input_type;output_type;result}) (t_function input_type output_type ())
let e' = Environment.add_ez_binder (fst binder) input_type e in
let%bind result = type_expression ~tv_opt:output_type e' result in
return (E_lambda {binder = fst binder;input_type;output_type;result}) (t_function input_type output_type ())
)
| E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
let tv_lst = List.map get_type_annotation lst' in
let%bind (name', tv) = type_constant name tv_lst tv_opt in
return (E_constant (name' , lst')) tv
| E_application (f, arg) ->
let%bind f = type_annotated_expression e f in
let%bind arg = type_annotated_expression e arg in
let%bind f = type_expression e f in
let%bind arg = type_expression e arg in
let%bind tv = match f.type_annotation.type_value' with
| T_function (param, result) ->
let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
@ -384,18 +385,18 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
in
return (E_application (f , arg)) tv
| E_look_up dsi ->
let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in
let%bind (ds, ind) = bind_map_pair (type_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
return (E_look_up (ds , ind)) (t_option dst ())
(* Advanced *)
| E_matching (ex, m) -> (
let%bind ex' = type_annotated_expression e ex in
let%bind ex' = type_expression e ex in
match m with
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
| I.Match_bool { match_false ; match_true = { expression = E_failwith fw } } -> (
let%bind fw' = type_annotated_expression e fw in
let%bind mf' = type_annotated_expression e match_false in
| I.Match_bool { match_false ; match_true = E_failwith fw } -> (
let%bind fw' = type_expression e fw in
let%bind mf' = type_expression e match_false in
let%bind () =
trace_strong (simple_error "Matching bool on not-a-bool")
@@ assert_t_bool (get_type_annotation ex') in
@ -411,7 +412,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (O.E_matching (ex' , m')) (t_unit ())
)
| _ -> (
let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in
let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m in
let tvs =
let aux (cur:O.value O.matching) =
match cur with
@ -435,15 +436,15 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
)
)
| E_sequence (a , b) ->
let%bind a' = type_annotated_expression e a in
let%bind b' = type_annotated_expression e b in
let%bind a' = type_expression e a in
let%bind b' = type_expression e b in
let%bind () =
trace_strong (simple_error "first part of the sequence isn't of unit type") @@
Ast_typed.assert_type_value_eq (t_unit () , get_type_annotation a') in
return (O.E_sequence (a' , b')) (get_type_annotation b')
| E_loop (expr , body) ->
let%bind expr' = type_annotated_expression e expr in
let%bind body' = type_annotated_expression e body in
let%bind expr' = type_expression e expr in
let%bind body' = type_expression e body in
let%bind () =
trace_strong (simple_error "while condition isn't of type bool") @@
Ast_typed.assert_type_value_eq (t_bool () , get_type_annotation expr') in
@ -475,16 +476,23 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
| Access_map _ -> simple_fail "no assign expressions with maps yet"
in
bind_fold_list aux (typed_name.type_value , []) path in
let%bind expr' = type_annotated_expression e expr in
let%bind expr' = type_expression e expr in
let%bind () =
trace_strong (simple_error "assign type doesn't match left-hand-side") @@
Ast_typed.assert_type_value_eq (assign_tv , get_type_annotation expr') in
return (O.E_assign (typed_name , path' , expr')) (t_unit ())
| E_let_in {binder ; rhs ; result} ->
let%bind rhs = type_annotated_expression e rhs in
let e' = Environment.add_ez_declaration binder rhs e in
let%bind result = type_annotated_expression e' result in
return (E_let_in {binder; rhs; result}) result.type_annotation
let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in
let e' = Environment.add_ez_declaration (fst binder) rhs e in
let%bind result = type_expression e' result in
return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
| E_annotation (expr , te) ->
let%bind tv = evaluate_type e te in
let%bind expr' = type_expression ~tv_opt:tv e expr in
let%bind type_annotation = O.merge_annotation (Some tv) (Some expr'.type_annotation) in
ok {expr' with type_annotation}
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 *)
@ -536,69 +544,69 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_address s -> ok (Literal_address s)
| Literal_operation s -> ok (Literal_operation s)
let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
let open I in
let type_annotation = e.type_annotation.simplified in
let return e = ok @@ I.Combinators.make_e_a ?type_annotation e in
let return e = ok e in
match e.expression with
| E_literal l ->
let%bind l = untype_literal l in
return (E_literal l)
| E_constant (n, lst) ->
let%bind lst' = bind_list
@@ List.map untype_annotated_expression lst in
@@ List.map untype_expression lst in
return (E_constant (n, lst'))
| E_variable n ->
return (E_variable n)
| E_application (f, arg) ->
let%bind f' = untype_annotated_expression f in
let%bind arg' = untype_annotated_expression arg in
let%bind f' = untype_expression f in
let%bind arg' = untype_expression arg in
return (E_application (f', arg'))
| E_lambda {binder;input_type;output_type;result} ->
let%bind input_type = untype_type_value input_type in
let%bind output_type = untype_type_value output_type in
let%bind result = untype_annotated_expression result in
return (E_lambda {binder;input_type = Some input_type;output_type = Some output_type;result})
let%bind result = untype_expression result in
return (E_lambda {binder = (binder , Some input_type);input_type = Some input_type;output_type = Some output_type;result})
| E_tuple lst ->
let%bind lst' = bind_list
@@ List.map untype_annotated_expression lst in
@@ List.map untype_expression lst in
return (E_tuple lst')
| E_tuple_accessor (tpl, ind) ->
let%bind tpl' = untype_annotated_expression tpl in
let%bind tpl' = untype_expression tpl in
return (E_accessor (tpl', [Access_tuple ind]))
| E_constructor (n, p) ->
let%bind p' = untype_annotated_expression p in
let%bind p' = untype_expression p in
return (E_constructor (n, p'))
| E_record r ->
let%bind r' = bind_smap
@@ SMap.map untype_annotated_expression r in
@@ SMap.map untype_expression r in
return (E_record r')
| E_record_accessor (r, s) ->
let%bind r' = untype_annotated_expression r in
let%bind r' = untype_expression r in
return (E_accessor (r', [Access_record s]))
| E_map m ->
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
return (E_map m')
| E_list lst ->
let%bind lst' = bind_map_list untype_annotated_expression lst in
let%bind lst' = bind_map_list untype_expression lst in
return (E_list lst')
| E_look_up dsi ->
let%bind dsi' = bind_map_pair untype_annotated_expression dsi in
let%bind dsi' = bind_map_pair untype_expression dsi in
return (E_look_up dsi')
| E_matching (ae, m) ->
let%bind ae' = untype_annotated_expression ae in
let%bind m' = untype_matching untype_annotated_expression m in
let%bind ae' = untype_expression ae in
let%bind m' = untype_matching untype_expression m in
return (E_matching (ae', m'))
| E_failwith ae ->
let%bind ae' = untype_annotated_expression ae in
let%bind ae' = untype_expression ae in
return (E_failwith ae')
| E_sequence _
| E_loop _
| E_assign _ -> simple_fail "not possible to untranspile statements yet"
| E_let_in {binder;rhs;result} ->
let%bind rhs = untype_annotated_expression rhs in
let%bind result = untype_annotated_expression result in
return (E_let_in {binder;rhs;result})
let%bind tv = untype_type_value rhs.type_annotation in
let%bind rhs = untype_expression rhs in
let%bind result = untype_expression result in
return (E_let_in {binder = (binder , Some tv);rhs;result})
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in