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

Merge branch 'master' of gitlab.com:gabriel.alfour/ligo

Browse Source
This commit is contained in:
Christian Rinderknecht 2019-05-22 19:38:40 +02:00
commit 193febc83e
28 changed files with 396 additions and 1144 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/ast_simplified/PP.ml
View File

@ -42,10 +42,10 @@ let rec expression ppf (e:expression) = match e with
| 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_lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_expression input_type type_expression output_type
block body annotated_expression result
| 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
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
| E_failwith ae ->
@ -65,6 +65,7 @@ let rec expression ppf (e:expression) = match e with
annotated_expression expr
| E_let_in { binder; rhs; result } ->
fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
| E_skip -> fprintf ppf "skip"
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
@ -88,8 +89,6 @@ and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotatio
and value : _ -> value -> unit = fun x -> annotated_expression x
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
@ -113,17 +112,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> u
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_do ae -> fprintf ppf "do %a" annotated_expression ae
| I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
| I_tuple_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_tuple_patch) lst
| I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = match d with
| Declaration_type {type_name ; type_expression = te} ->
fprintf ppf "type %s = %a" type_name type_expression te

20
src/ast_simplified/combinators.ml
View File

@ -9,11 +9,18 @@ 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 i_assignment : _ -> instruction = fun x -> I_assignment x
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 () =
@ -79,6 +86,10 @@ let e_accessor a b = E_accessor (a , b)
let e_accessor_props a b = e_accessor a (List.map (fun x -> Access_record x) b)
let e_variable v = E_variable v
let e_failwith v = E_failwith v
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_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
@ -89,6 +100,7 @@ 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_a_record r =
let type_annotation = Option.(
@ -130,17 +142,15 @@ let e_a_typed_list lst t =
let e_a_map lst k v = make_e_a ~type_annotation:(t_map k v) (e_map lst)
let e_lambda (binder : string)
(input_type : type_expression)
(output_type : type_expression)
(input_type : type_expression option)
(output_type : type_expression option)
(result : expression)
(body : block)
: expression =
E_lambda {
binder = (make_name binder) ;
input_type = input_type ;
output_type = output_type ;
result = (make_e_a result) ;
body ;
}
let e_tuple (lst : ae list) : expression = E_tuple lst

24
src/ast_simplified/types.ml
View File

@ -47,11 +47,10 @@ and type_expression =
| T_constant of type_name * te list
and lambda = {
binder: name ;
input_type: type_expression;
output_type: type_expression;
result: ae ;
body: block ;
binder : name ;
input_type : type_expression option ;
output_type : type_expression option ;
result : ae ;
}
and let_in = {
@ -86,6 +85,7 @@ and expression =
| E_sequence of (ae * ae)
| E_loop of (ae * ae)
| E_assign of (name * access_path * ae)
| E_skip
and access =
| Access_tuple of int
@ -105,18 +105,6 @@ and literal =
| Literal_address of string
| Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
and block = instruction list
and b = block
and instruction =
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_skip
| I_do of ae
| I_record_patch of (name * access_path * (string * ae) list)
| I_tuple_patch of (name * access_path * (int * ae) list)
and 'a matching =
| Match_bool of {
match_true : 'a ;
@ -133,6 +121,4 @@ and 'a matching =
| Match_tuple of name list * 'a
| Match_variant of ((constructor_name * name) * 'a) list
and matching_instr = b matching
and matching_expr = annotated_expression matching

23
src/ast_typed/PP.ml
View File

@ -24,10 +24,10 @@ let rec annotated_expression ppf (ae:annotated_expression) : unit =
| _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
and lambda ppf l =
let {binder;input_type;output_type;result;body} = l in
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
let {binder;input_type;output_type;result} = l in
fprintf ppf "lambda (%s:%a) : %a return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
annotated_expression result
and expression ppf (e:expression) : unit =
match e with
@ -74,8 +74,6 @@ and literal ppf (l:literal) : unit =
| Literal_address s -> fprintf ppf "@%s" s
| Literal_operation _ -> fprintf ppf "Operation(...bytes)"
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((s, ae) : string * ae) =
fprintf ppf "%s <- %a" s annotated_expression ae
@ -100,21 +98,6 @@ and pre_access ppf (a:access) = match a with
| Access_tuple i -> fprintf ppf ".%d" i
| Access_map n -> fprintf ppf ".%a" annotated_expression n
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_do ae -> fprintf ppf "do %a" annotated_expression ae
| I_loop (cond, b) -> fprintf ppf "while (%a) {@; @[<v>%a@]@;}" annotated_expression cond block b
| I_declaration {name;annotated_expression = ae} ->
fprintf ppf "let %s = %a" name annotated_expression ae
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
| I_patch (s, p, e) ->
fprintf ppf "%s%a := %a"
s.type_name (fun ppf -> List.iter (pre_access ppf)) p
annotated_expression e
let declaration ppf (d:declaration) =
match d with
| Declaration_constant ({name ; annotated_expression = ae} , _) ->

4
src/ast_typed/combinators.ml
View File

@ -6,7 +6,6 @@ let make_a_e expression type_annotation environment = { expression ; type_annota
let make_n_e name a_e = { name ; annotated_expression = a_e }
let make_n_t type_name type_value = { type_name ; type_value }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
@ -22,7 +21,6 @@ let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
let t_pair a b ?s () = t_tuple [a ; b] ?s ()
let t_record m ?s () : type_value = make_t (T_record m) s
let make_t_ez_record (lst:(string * type_value) list) : type_value =
let aux prev (k, v) = SMap.add k v prev in
@ -164,6 +162,7 @@ let e_pair a b : expression = E_tuple [a; b]
let e_application a b : expression = E_application (a , b)
let e_variable v : expression = E_variable v
let e_list lst : expression = E_list lst
let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
let e_a_unit = make_a_e e_unit (t_unit ())
let e_a_int n = make_a_e (e_int n) (t_int ())
@ -183,6 +182,7 @@ let e_a_variable v ty = make_a_e (e_variable v) ty
let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_annotation) r) ())
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
let e_a_let_in binder expr body = make_a_e (e_let_in binder expr body) (get_type_annotation body)
let get_a_int (t:annotated_expression) =
match t.expression with

8
src/ast_typed/environment.ml
View File

@ -78,3 +78,11 @@ module PP = struct
(ne_list_sep small_environment (tag "@;")) e
end
open Trace
let get_trace : string -> t -> element result = fun s env ->
let error =
let title () = "missing var not in env" in
let content () = Format.asprintf "\nvar: %s\nenv: %a\n" s PP.full_environment env in
error title content in
trace_option error @@ get_opt s env

25
src/ast_typed/misc.ml
View File

@ -70,32 +70,11 @@ module Free_variables = struct
and lambda : bindings -> lambda -> bindings = fun b l ->
let b' = union (singleton l.binder) b in
let (b'', frees) = block' b' l.body in
union (annotated_expression b'' l.result) frees
annotated_expression b' l.result
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
expression b ae.expression
and instruction' : bindings -> instruction -> bindings * bindings = fun b i ->
match i with
| I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression)
| I_assignment n -> b , (annotated_expression b n.annotated_expression)
| I_skip -> b , empty
| I_do e -> b , annotated_expression b e
| I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl)
| I_patch (_ , _ , a) -> b , annotated_expression b a
| I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs)
and block' : bindings -> block -> (bindings * bindings) = fun b bl ->
let aux = fun (binds, frees) cur ->
let (binds', frees') = instruction' binds cur in
(binds', union frees frees') in
List.fold_left aux (b , []) bl
and block : bindings -> block -> bindings = fun b bl ->
let (_ , frees) = block' b bl in
frees
and matching_variant_case : type a . (bindings -> a -> bindings) -> bindings -> ((constructor_name * name) * a) -> bindings = fun f b ((_,n),c) ->
f (union (singleton n) b) c
@ -109,8 +88,6 @@ module Free_variables = struct
and matching_expression = fun x -> matching annotated_expression x
and matching_block = fun x -> matching block x
end

45
src/ast_typed/misc_smart.ml
View File

@ -19,15 +19,10 @@ let program_to_main : program -> string -> lambda result = fun p s ->
| _ -> simple_fail "program main isn't a function" in
ok (main , input_ty , output_ty)
in
let body =
let aux : declaration -> instruction = fun d ->
match d with
| Declaration_constant (d , _) -> I_declaration d in
List.map (Function.compose aux Location.unwrap) p in
let env =
let aux = fun _ d ->
match d with
| Declaration_constant (_ , env) -> env in
| Declaration_constant (_ , (_ , post_env)) -> post_env in
List.fold_left aux Environment.full_empty (List.map Location.unwrap p) in
let binder = "@contract_input" in
let result =
@ -38,7 +33,6 @@ let program_to_main : program -> string -> lambda result = fun p s ->
binder ;
input_type ;
output_type ;
body ;
result ;
}
@ -103,41 +97,6 @@ module Captured_variables = struct
let b' = union (singleton li.binder) b in
annotated_expression b' li.result
and instruction' : bindings -> instruction -> (bindings * bindings) result = fun b i ->
match i with
| I_declaration n ->
let bounds = union (singleton n.name) b in
let%bind frees = annotated_expression b n.annotated_expression in
ok (bounds , frees)
| I_assignment n ->
let%bind frees = annotated_expression b n.annotated_expression in
ok (b , frees)
| I_skip -> ok (b , empty)
| I_do e ->
let%bind frees = annotated_expression b e in
ok (b , frees)
| I_loop (a , bl) ->
let%bind ae_frees = annotated_expression b a in
let%bind bl_frees = block b bl in
ok (b , union ae_frees bl_frees)
| I_patch (_ , _ , a) ->
let%bind a' = annotated_expression b a in
ok (b , a')
| I_matching (a , cs) ->
let%bind ae' = annotated_expression b a in
let%bind bl' = matching_block b cs in
ok (b , union ae' bl')
and block' : bindings -> block -> (bindings * bindings) result = fun b bl ->
let aux = fun (binds, frees) cur ->
let%bind (binds', frees') = instruction' binds cur in
ok (binds', union frees frees') in
bind_fold_list aux (b , []) bl
and block : bindings -> block -> bindings result = fun b bl ->
let%bind (_ , frees) = block' b bl in
ok frees
and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor_name * name) * a) -> bindings result = fun f b ((_,n),c) ->
f (union (singleton n) b) c
@ -163,6 +122,4 @@ module Captured_variables = struct
and matching_expression = fun x -> matching annotated_expression x
and matching_block = fun x -> matching block x
end

17
src/ast_typed/types.ml
View File

@ -14,7 +14,7 @@ type 'a type_name_map = 'a SMap.t
type program = declaration Location.wrap list
and declaration =
| Declaration_constant of (named_expression * full_environment)
| Declaration_constant of (named_expression * (full_environment * full_environment))
(* | Macro_declaration of macro_declaration *)
and environment_element_definition =
@ -72,7 +72,6 @@ and lambda = {
input_type: tv ;
output_type: tv ;
result: ae ;
body: block ;
}
and let_in = {
@ -122,18 +121,6 @@ and literal =
| Literal_address of string
| Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
and block = instruction list
and b = block
and instruction =
| I_declaration of named_expression
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_do of ae
| I_skip
| I_patch of named_type_value * access_path * ae
and access =
| Access_tuple of int
| Access_record of string
@ -157,8 +144,6 @@ and 'a matching =
| Match_tuple of (name list * 'a)
| Match_variant of (((constructor_name * name) * 'a) list * type_value)
and matching_instr = b matching
and matching_expr = ae matching
open Trace

20
src/compiler/compiler_environment.ml
View File

@ -135,11 +135,18 @@ let select : environment -> string list -> michelson result = fun e lst ->
ok code
let clear : environment -> michelson result = fun e -> select e []
let select_env : environment -> environment -> michelson result = fun source filter ->
let lst = Environment.get_names filter in
select source lst
let select_env : environment -> environment -> michelson result = fun e e' ->
let lst = Environment.get_names e' in
select e lst
let clear : environment -> (michelson * environment) result = fun e ->
let lst = Environment.get_names e in
let%bind first_name =
trace_option (simple_error "try to clear empty env") @@
List.nth_opt lst 0 in
let%bind code = select e [ first_name ] in
let e' = Environment.select [ first_name ] e in
ok (code , e')
let pack : environment -> michelson result = fun e ->
let%bind () =
@ -276,3 +283,8 @@ let add_packed_anon : environment -> type_value -> michelson result = fun e type
in
ok code
let pop : environment -> environment result = fun e ->
match e with
| [] -> simple_fail "pop empty env"
| _ :: tl -> ok tl

272
src/compiler/compiler_program.ml
View File

@ -87,6 +87,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
let error_message () =
Format.asprintf "\n- expr: %a\n- type: %a\n" PP.expression expr PP.type_ ty
in
let i_skip = i_push_unit in
let return ?prepend_env ?end_env code =
let%bind env' =
@ -123,6 +124,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
trace (error (thunk "compiling expression") error_message) @@
match expr' with
| E_skip -> return @@ i_skip
| E_environment_capture c ->
let%bind code = Compiler_environment.pack_select env c in
return @@ code
@ -130,14 +132,26 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
let%bind (expr' , _) = translate_expression expr env in
let%bind clear = Compiler_environment.select env [] in
let%bind unpack = Compiler_environment.unpack load_env in
return ~end_env:load_env @@ seq [
return ~prepend_env:load_env @@ seq [
expr' ;
dip clear ;
unpack ;
i_skip ;
]
| E_environment_select sub_env ->
let%bind code = Compiler_environment.select_env env sub_env in
return ~end_env:sub_env code
return ~prepend_env:sub_env @@ seq [
code ;
i_skip ;
]
| E_environment_return expr -> (
let%bind (expr' , env) = translate_expression expr env in
let%bind (code , cleared_env) = Compiler_environment.clear env in
return ~end_env:cleared_env @@ seq [
expr' ;
code ;
]
)
| E_literal v ->
let%bind v = translate_value v in
let%bind t = Compiler_type.type_ ty in
@ -195,11 +209,21 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
return code
| E_sequence (a , b) ->
let%bind (a' , env_a) = translate_expression a env in
let%bind (b' , env_b) = translate_expression b env_a in
return ~prepend_env:env_b @@ seq [
let%bind env_a' = Compiler_environment.pop env_a in
let%bind (b' , env_b) = translate_expression b env_a' in
return ~end_env:env_b @@ seq [
a' ;
i_drop ;
b' ;
]
(* | E_sequence_drop (a , b) ->
* let%bind (a' , env_a) = translate_expression a env in
* let%bind (b' , env_b) = translate_expression b env_a in
* return ~end_env:env_b @@ seq [
* a' ;
* i_drop ;
* b' ;
* ] *)
| E_constant(str, lst) ->
let module L = Logger.Stateful() in
let%bind lst' =
@ -250,8 +274,9 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
return @@ i_none o'
| E_if_bool (c, a, b) -> (
let%bind (c' , env') = translate_expression c env in
let%bind (a' , _) = translate_expression a env' in
let%bind (b' , _) = translate_expression b env' in
let%bind popped = Compiler_environment.pop env' in
let%bind (a' , _) = translate_expression a popped in
let%bind (b' , _) = translate_expression b popped in
let%bind code = ok (seq [
c' ;
i_if a' b' ;
@ -259,16 +284,18 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
return code
)
| E_if_none (c, n, (ntv , s)) -> (
let%bind (c' , _env') = translate_expression c env in
let%bind (n' , _) = translate_expression n env in
let s_env = Environment.add ntv env in
let%bind (s' , _) = translate_expression s s_env in
let%bind restrict_s = Compiler_environment.select_env s_env env in
let%bind (c' , env') = translate_expression c env in
let%bind popped = Compiler_environment.pop env' in
let%bind (n' , _) = translate_expression n popped in
let s_env = Environment.add ntv popped in
let%bind (s' , s_env') = translate_expression s s_env in
let%bind popped' = Compiler_environment.pop s_env' in
let%bind restrict_s = Compiler_environment.select_env popped' popped in
let%bind code = ok (seq [
c' ;
i_if_none n' (seq [
s' ;
restrict_s ;
dip restrict_s ;
])
;
]) in
@ -297,11 +324,15 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
]) in
return code
)
| E_let_in (v, expr , body) -> (
let%bind (expr' , _) = translate_expression expr env in
let env' = Environment.add v env in
let%bind (body' , _) = translate_expression body env' in
let%bind restrict = Compiler_environment.select_env env' env in
| E_let_in (v , expr , body) -> (
let%bind (expr' , expr_env) = translate_expression expr env in
let%bind env' =
let%bind popped = Compiler_environment.pop expr_env in
ok @@ Environment.add v popped in
let%bind (body' , body_env) = translate_expression body env' in
let%bind restrict =
let%bind popped = Compiler_environment.pop body_env in
Compiler_environment.select_env popped env in
let%bind code = ok (seq [
expr' ;
body' ;
@ -312,6 +343,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
)
| E_assignment (name , lrs , expr) -> (
let%bind (expr' , env') = translate_expression expr env in
(* Format.printf "\nass env':%a\n" PP.environment env' ; *)
let%bind get_code = Compiler_environment.get env' name in
let modify_code =
let aux acc step = match step with
@ -333,211 +365,42 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
in
error title content in
trace error @@
return ~end_env:env @@ seq [
return ~prepend_env:env @@ seq [
i_comment "assign: start # env" ;
expr' ;
i_comment "assign: compute rhs # rhs : env" ;
get_code ;
i_swap ; modify_code ;
i_comment "assign: get name # name : rhs : env" ;
i_swap ;
i_comment "assign: swap # rhs : name : env" ;
modify_code ;
i_comment "assign: modify code # name+rhs : env" ;
set_code ;
i_comment "assign: set new # new_env" ;
i_skip ;
]
)
| E_while (expr, block) -> (
let%bind (expr' , env') = translate_expression expr env in
let%bind (block' , env'') = translate_expression block env' in
let%bind restrict_block = Compiler_environment.select_env env'' env' in
let%bind popped = Compiler_environment.pop env' in
let%bind (block' , env'') = translate_expression block popped in
let%bind restrict_block = Compiler_environment.select_env env'' popped in
return @@ seq [
expr' ;
prim ~children:[seq [
block' ;
restrict_block ;
expr']] I_LOOP ;
i_skip ;
]
)
and translate_statement ((s', w_env) as s:statement) : michelson result =
let error_message () = Format.asprintf "%a" PP.statement s in
let return code =
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment w_env.pre_environment in
let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment w_env.post_environment in
let error_message () =
let%bind pre_env_michelson = Compiler_type.environment w_env.pre_environment in
let%bind post_env_michelson = Compiler_type.environment w_env.post_environment in
ok @@ Format.asprintf
"statement : %a\ncode : %a\npre type : %a\npost type : %a\n"
PP.statement s
Michelson.pp code
PP_helpers.(list_sep Michelson.pp (const " ; ")) pre_env_michelson
PP_helpers.(list_sep Michelson.pp (const " ; ")) post_env_michelson
in
let%bind _ =
Trace.trace_tzresult_lwt_r (fun () -> let%bind error_message = error_message () in
ok (fun () -> error (thunk "error parsing statement code")
(fun () -> error_message)
())) @@
Proto_alpha_utils.Memory_proto_alpha.parse_michelson_fail code
input_stack_ty output_stack_ty
in
ok code
in
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_add _ ->
simple_fail "add not ready yet"
| S_environment_select sub_env ->
let%bind code = Compiler_environment.select_env w_env.pre_environment sub_env in
return code
| S_environment_load (expr , env) ->
let%bind (expr' , _) = translate_expression expr w_env.pre_environment in
let%bind clear = Compiler_environment.select w_env.pre_environment [] in
let%bind unpack = Compiler_environment.unpack env in
return @@ seq [
expr' ;
dip clear ;
unpack ;
]
| S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in
let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind add = Compiler_environment.add w_env.pre_environment (s, tv) in
return @@ seq [
i_comment "declaration" ;
seq [
i_comment "expr" ;
expr ;
] ;
seq [
i_comment "env <- env . expr" ;
add ;
];
]
| S_assignment (s, expr) ->
let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind set = Compiler_environment.set w_env.pre_environment s in
return @@ seq [
i_comment "assignment" ;
seq [
i_comment "expr" ;
expr ;
] ;
seq [
i_comment "env <- env . expr" ;
set ;
];
]
| S_cond (expr, a, b) ->
let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in
return @@ seq [
expr ;
prim ~children:[seq [a'];seq [b']] I_IF ;
]
| S_do expr -> (
match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind (fw' , _) = translate_expression fw w_env.pre_environment in
return @@ seq [
fw' ;
i_failwith ;
]
)
| _ -> (
let%bind (expr' , _) = translate_expression expr w_env.pre_environment in
return @@ seq [
expr' ;
i_drop ;
]
)
)
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in
let%bind add =
let env' = w_env.pre_environment in
Compiler_environment.add env' (name, tv) in
let%bind restrict_s = Compiler_environment.select_env (snd some).post_environment w_env.pre_environment in
return @@ seq [
expr ;
prim ~children:[
seq [none'] ;
seq [add ; some' ; restrict_s] ;
] I_IF_NONE
]
| S_while (expr, block) ->
let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Compiler_environment.select_env (snd block).post_environment env_while in
return @@ seq [
expr ;
prim ~children:[seq [
block' ;
restrict_block ;
expr]] I_LOOP ;
]
| S_patch (name, lrs, expr) ->
let%bind (expr' , env') = translate_expression expr w_env.pre_environment in
let%bind get_code = Compiler_environment.get env' name in
let modify_code =
let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair]
| `Right -> seq [dip i_unpiar ; acc ; i_piar]
in
let init = dip i_drop in
List.fold_right' aux init lrs
in
let%bind set_code = Compiler_environment.set w_env.pre_environment name in
let error =
let title () = "michelson type-checking patch" in
let content () =
let aux ppf = function
| `Left -> Format.fprintf ppf "left"
| `Right -> Format.fprintf ppf "right" in
Format.asprintf "Sub path: %a\n"
PP_helpers.(list_sep aux (const " , ")) lrs
in
error title content in
trace error @@
return @@ seq [
expr' ;
get_code ;
i_swap ; modify_code ;
set_code ;
]
and translate_regular_block ((b, env):block) : michelson result =
let aux prev statement =
let%bind (lst : michelson list) = prev in
let%bind instruction = translate_statement statement in
ok (instruction :: lst)
in
let%bind codes =
let error_message () =
let%bind schema_michelsons = Compiler_type.environment env.pre_environment in
ok @@ Format.asprintf "\nblock : %a\nschema : %a\n"
PP.block (b, env)
PP_helpers.(list_sep Michelson.pp (const " ; ")) schema_michelsons
in
trace_r (fun () ->
let%bind error_message = error_message () in
ok (fun () -> error (thunk "compiling regular block")
(fun () -> error_message)
())) @@
List.fold_left aux (ok []) b in
let code = seq (List.rev codes) in
ok code
and translate_quote_body ({body;result} as f:anon_function) : michelson result =
let%bind body' = translate_regular_block body in
let%bind (expr , _) = translate_expression result (snd body).post_environment in
let%bind restrict = Compiler_environment.clear (snd body).post_environment in
and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result =
let env = Environment.(add (binder , input) empty) in
let%bind (expr , _) = translate_expression result env in
let code = seq [
i_comment "function body" ;
body' ;
i_comment "function result" ;
expr ;
dip restrict ;
] in
let%bind _assert_type =
@ -547,11 +410,10 @@ and translate_quote_body ({body;result} as f:anon_function) : michelson result =
let output_stack_ty = Stack.(output_ty @: nil) in
let error_message () =
Format.asprintf
"\ncode : %a\ninput : %a\noutput : %a\nenv : %a\n"
"\ncode : %a\ninput : %a\noutput : %a\n"
Michelson.pp code
PP.type_ f.input
PP.type_ f.output
PP.environment (snd body).post_environment
in
let%bind _ =
Trace.trace_tzresult_lwt (

4
src/contracts/assign.ligo Normal file
View File

@ -0,0 +1,4 @@
function main (const i : int) : int is
begin
i := i + 1 ;
end with i

8
src/contracts/condition-simple.ligo Normal file
View File

@ -0,0 +1,8 @@
function main (const i : int) : int is
begin
if 1 = 1 then
i := 42
else
i := 0
end with i

3
src/contracts/declaration-local.ligo Normal file
View File

@ -0,0 +1,3 @@
function main (const i : int) : int is block {
const j : int = 42 ;
} with j

4
src/main/contract.ml
View File

@ -110,7 +110,7 @@ let compile_contract_parameter : string -> string -> string -> string result = f
let env =
let last_declaration = Location.unwrap List.(hd @@ rev program) in
match last_declaration with
| Declaration_constant (_ , env) -> env
| Declaration_constant (_ , (_ , post_env)) -> post_env
in
trace (simple_error "typing expression") @@
Typer.type_annotated_expression env simplified in
@ -158,7 +158,7 @@ let compile_contract_storage : string -> string -> string -> string result = fun
let env =
let last_declaration = Location.unwrap List.(hd @@ rev program) in
match last_declaration with
| Declaration_constant (_ , env) -> env
| Declaration_constant (_ , (_ , post_env)) -> post_env
in
trace (simple_error "typing expression") @@
Typer.type_annotated_expression env simplified in

2
src/main/main.ml
View File

@ -138,7 +138,7 @@ let easy_run_typed_simplified
let env =
let last_declaration = Location.unwrap List.(hd @@ rev program) in
match last_declaration with
| Declaration_constant (_ , env) -> env
| Declaration_constant (_ , (_ , post_env)) -> post_env
in
type_expression ~env input in
let%bind mini_c_value = transpile_value typed_value in

28
src/mini_c/PP.ml
View File

@ -64,6 +64,8 @@ and expression' ppf (e:expression') = match e with
| E_environment_capture s -> fprintf ppf "capture(%a)" (list_sep string (const " ; ")) s
| E_environment_load (expr , env) -> fprintf ppf "load %a in %a" expression expr environment env
| E_environment_select env -> fprintf ppf "select %a" environment env
| E_environment_return expr -> fprintf ppf "return %a" expression expr
| E_skip -> fprintf ppf "skip"
| E_variable v -> fprintf ppf "%s" v
| E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
| E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
@ -76,8 +78,9 @@ and expression' ppf (e:expression') = match e with
| E_if_left (c, ((name_l, _) , l), ((name_r, _) , r)) ->
fprintf ppf "%a ?? %s -> %a : %s -> %a" expression c name_l expression l name_r expression r
| E_sequence (a , b) -> fprintf ppf "%a ; %a" expression a expression b
(* | E_sequence_drop (a , b) -> fprintf ppf "%a ;- %a" expression a expression b *)
| E_let_in ((name , _) , expr , body) ->
fprintf ppf "let %s = %a in %a" name expression expr expression body
fprintf ppf "let %s = %a in ( %a )" name expression expr expression body
| E_assignment (r , path , e) ->
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
| E_while (e , b) ->
@ -91,36 +94,17 @@ and expression_with_type : _ -> expression -> _ = fun ppf e ->
expression' e.content
type_ e.type_value
and function_ ppf ({binder ; input ; output ; body ; result}:anon_function) =
fprintf ppf "fun (%s:%a) : %a %a return %a"
and function_ ppf ({binder ; input ; output ; result}:anon_function) =
fprintf ppf "fun (%s:%a) : %a (%a)"
binder
type_ input
type_ output
block body
expression result
and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e
and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e
and statement ppf ((s, _) : statement) = match s with
| S_environment_load _ -> fprintf ppf "load env"
| S_environment_select _ -> fprintf ppf "select env"
| S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv
| S_declaration ass -> declaration ppf ass
| S_assignment ass -> assignment ppf ass
| S_do e -> fprintf ppf "do %a" expression e
| S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| S_patch (r, path, e) ->
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
| S_if_none (expr, none, ((name, _), some)) -> fprintf ppf "if_none (%a) %a %s->%a" expression expr block none name block some
| S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b
and block ppf ((b, _):block) =
match b with
| [] -> fprintf ppf "{}"
| b -> fprintf ppf "{@; @[<v>%a@]@;}" (pp_print_list ~pp_sep:(tag "@;") statement) b
let tl_statement ppf (ass, _) = assignment ppf ass
let program ppf (p:program) =

33
src/mini_c/combinators.ml
View File

@ -121,12 +121,6 @@ let get_operation (v:value) = match v with
| _ -> simple_fail "not an operation"
let get_last_statement ((b', _):block) : statement result =
let aux lst = match lst with
| [] -> simple_fail "get_last: empty list"
| lst -> ok List.(nth lst (length lst - 1)) in
aux b'
let t_int : type_value = T_base Base_int
let t_unit : type_value = T_base Base_unit
let t_nat : type_value = T_base Base_nat
@ -136,25 +130,34 @@ let t_deep_closure x y z : type_value = T_deep_closure ( x , y , z )
let t_pair x y : type_value = T_pair ( x , y )
let t_union x y : type_value = T_or ( x , y )
let quote binder input output body result : anon_function =
let quote binder input output result : anon_function =
{
binder ; input ; output ;
body ; result ;
result ;
}
let basic_quote i o b : anon_function result =
let%bind (_, _e) = get_last_statement b in
let r : expression = Expression.make_tpl (E_variable "output", o) in
ok @@ quote "input" i o b r
let basic_int_quote b : anon_function result =
basic_quote t_int t_int b
let e_int expr : expression = Expression.make_tpl (expr, t_int)
let e_unit : expression = Expression.make_tpl (E_literal D_unit, t_unit)
let e_skip : expression = Expression.make_tpl (E_skip, t_unit)
let e_var_int name : expression = e_int (E_variable name)
let e_let_int v tv expr body : expression = Expression.(make_tpl (
E_let_in ((v , tv) , expr , body) ,
get_type body
))
let ez_e_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl (a , t_unit) , b) , get_type b))
let ez_e_return e : expression = Expression.(make_tpl ((E_environment_return e) , get_type e))
let d_unit : value = D_unit
let basic_quote i o expr : anon_function result =
ok @@ quote "input" i o (ez_e_return expr)
let basic_int_quote expr : anon_function result =
basic_quote t_int t_int expr
let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
let id_environment_wrap e = environment_wrap e e

46
src/mini_c/combinators_smart.ml
View File

@ -1,52 +1,6 @@
open Trace
open Types
open Combinators
let basic_int_quote_env : environment =
let e = Environment.empty in
Environment.add ("input", t_int) e
let statement s' env : statement =
match s' with
| S_environment_load (_ , env') -> s', environment_wrap env env'
| S_environment_select env' -> s', environment_wrap env env'
| S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env)
| S_cond _ -> s' , id_environment_wrap env
| S_do _ -> s' , id_environment_wrap env
| S_if_none _ -> s' , id_environment_wrap env
| S_while _ -> s' , id_environment_wrap env
| S_patch _ -> s' , id_environment_wrap env
| S_declaration (name , e) -> s', environment_wrap env (Environment.add (name , (Expression.get_type e)) env)
| S_assignment (name , e) -> s', environment_wrap env (Environment.add (name , (Expression.get_type e)) env)
let block (statements:statement list) : block result =
match statements with
| [] -> simple_fail "no statements in block"
| lst ->
let first = List.hd lst in
let last = List.(nth lst (length lst - 1)) in
ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment)
let append_statement' : block -> statement' -> block = fun b s' ->
let b_wrap = snd b in
let s = statement s' b_wrap.post_environment in
let s_wrap = snd s in
let b_wrap' = { b_wrap with post_environment = s_wrap.post_environment } in
let b_content = fst b in
(b_content @ [s], b_wrap')
let prepend_statement : statement -> block -> block = fun s b ->
let s_wrap = snd s in
let b_wrap = snd b in
let b_wrap' = { b_wrap with pre_environment = s_wrap.pre_environment } in
let b_content = fst b in
(s :: b_content, b_wrap')
let statements (lst:(environment -> statement) list) e : statement list =
let rec aux lst e = match lst with
| [] -> []
| hd :: tl ->
let s = hd e in
s :: aux tl (snd s).post_environment
in
aux lst e

22
src/mini_c/types.ml
View File

@ -56,6 +56,8 @@ and expression' =
| E_environment_capture of selector
| E_environment_select of environment
| E_environment_load of (expression * environment)
| E_environment_return of expression
| E_skip
| E_constant of string * expression list
| E_application of expression * expression
| E_variable of var_name
@ -67,6 +69,7 @@ and expression' =
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
| E_let_in of ((var_name * type_value) * expression * expression)
| E_sequence of (expression * expression)
(* | E_sequence_drop of (expression * expression) *)
| E_assignment of (string * [`Left | `Right] list * expression)
| E_while of expression * expression
@ -78,32 +81,13 @@ and expression = {
and assignment = var_name * expression
and statement' =
| S_environment_select of environment
| S_environment_load of (expression * environment)
| S_environment_add of (var_name * type_value)
| S_declaration of assignment (* First assignment *)
| S_assignment of assignment
| S_do of expression
| S_cond of expression * block * block
| S_patch of string * [`Left | `Right] list * expression
| S_if_none of expression * block * ((var_name * type_value) * block)
| S_while of expression * block
and statement = statement' * environment_wrap
and toplevel_statement = assignment * environment_wrap
and anon_function = {
binder : string ;
input : type_value ;
output : type_value ;
body : block ;
result : expression ;
}
and block' = statement list
and block = block' * environment_wrap
and program = toplevel_statement list

110
src/simplify/camligo.ml
View File

@ -45,6 +45,15 @@ let get_p_variable : I.pattern -> string Location.wrap result = fun p ->
| I.P_variable v -> ok v
| _ -> simple_fail "not a pattern variable"
let get_p_option_typed_variable : I.pattern -> (string Location.wrap * I.restricted_type_expression Location.wrap option) result = fun p ->
match p with
| I.P_variable v -> ok (v , None)
| I.P_type_annotation (pat , rte) -> (
let%bind v = get_p_variable @@ unwrap pat in
ok (v , Some rte)
)
| _ -> simple_fail "not an optionally typed pattern variable"
let get_p_typed_variable : I.pattern -> (string Location.wrap * I.restricted_type_expression Location.wrap) result = fun p ->
let%bind (p' , rte) =
trace (simple_error "get_p_typed_variable") @@
@ -171,64 +180,40 @@ 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
type last_instruction_result = (O.block * O.annotated_expression)
type lir = last_instruction_result
let rec expression : I.expression -> O.annotated_expression result = fun e ->
let simple_error str =
let title () = Format.asprintf "No %s in inside expressions" str in
let content () = Format.asprintf "%a" I.pp_expression e in
error title content in
match e with
| I.E_sequence _ -> fail @@ simple_error "sequence"
| I.E_let_in _ -> fail @@ simple_error "letin"
| 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
)
| 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'
)
| I.E_ifthenelse ite -> ifthenelse ite
| I.E_ifthen it -> ifthen it
| I.E_match m -> match_ m
| I.E_record r -> record r
| I.E_fun _ -> fail @@ simple_error "fun"
| I.E_fun (pattern , expr) -> (
let%bind (name , rte) = get_p_typed_variable @@ unwrap pattern in
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' ;
}
)
| I.E_main m -> expression_main m
and expression_last_instruction : I.expression -> lir result = fun e ->
match e with
| I.E_let_in l -> let_in_last_instruction l
| I.E_sequence s -> sequence_last_instruction s
| I.E_fun _|I.E_record _|I.E_ifthenelse _
| I.E_ifthen _|I.E_match _|I.E_main _ -> (
let%bind result' = expression e in
ok ([] , result')
)
and expression_sequence : I.expression -> O.instruction result = fun e ->
match e with
| _ -> (
let%bind e' = expression e in
ok @@ O.I_do e'
)
and let_in_last_instruction :
I.pattern Location.wrap * I.expression Location.wrap * I.expression Location.wrap -> lir result
= fun l ->
let (pat , expr , body) = l in
let%bind (var , ty) = get_p_typed_variable (unwrap pat) in
let%bind ty' = type_expression @@ of_restricted_type_expression (unwrap ty) in
let%bind expr' = expression (unwrap expr) in
let%bind uexpr' =
trace_strong (simple_error "no annotation on let bodies") @@
get_untyped_expression expr' in
let%bind (body' , last') = expression_last_instruction (unwrap body) in
let assignment = O.(i_assignment @@ named_typed_expression (unwrap var) uexpr' ty') in
ok (assignment :: body' , last')
and sequence_last_instruction = fun s ->
let exprs = List.map unwrap s in
let%bind (hds , tl) =
trace_option (simple_error "at least 2 expressions in sequence") @@
List.rev_uncons_opt exprs in
let%bind instrs' = bind_map_list expression_sequence hds in
let%bind (body' , last') = expression_last_instruction tl in
ok (instrs' @ body' , last')
and ifthenelse
: (I.expression Location.wrap * I.expression Location.wrap * I.expression Location.wrap) -> O.annotated_expression result
= fun ite ->
@ -444,27 +429,26 @@ let let_entry : _ -> _ result = fun l ->
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) ->
O.I_assignment {
name ;
annotated_expression = {
expression = O.E_accessor (input , [ Access_tuple i ]) ;
type_annotation = Some type_expression ;
}
}
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
in
List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)]
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 (body' , result) = expression_last_instruction (unwrap e) in
let%bind result = expression (unwrap e) in
let result = tpl_declarations result in
let input_type' = input_nty.type_expression in
let output_type' = O.(t_pair (t_list t_operation , storage_ty)) in
let lambda =
O.{
binder = input_nty.type_name ;
input_type = input_type';
output_type = output_type';
input_type = Some input_type';
output_type = Some output_type';
result ;
body = tpl_declarations @ body' ;
} 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}}

151
src/simplify/pascaligo.ml
View File

@ -17,6 +17,17 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value
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
match expr'_opt with
| None -> ok @@ expr
| Some expr' -> ok @@ e_a_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'
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
match t with
| TPar x -> simpl_type_expression x.value.inside
@ -286,36 +297,33 @@ and simpl_tuple_expression ?te_annot (lst:Raw.expr list) : annotated_expression
let%bind lst = bind_list @@ List.map simpl_expression lst in
return @@ E_tuple lst
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
match t with
| LocalData d -> simpl_data_declaration d
| LocalLam l -> simpl_lambda_declaration l
and simpl_lambda_declaration : Raw.lambda_decl -> (instruction * named_expression) result =
fun l ->
and simpl_lambda_declaration : Raw.lambda_decl -> _ result = fun l ->
match l with
| FunDecl f ->
let%bind e = simpl_fun_declaration (f.value) in
ok (I_assignment e, e)
return_let_in e.name e.annotated_expression
| ProcDecl _ -> simple_fail "no local procedure yet"
| EntryDecl _ -> simple_fail "no local entry-point yet"
and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result =
let return x = ok (I_assignment x, x) in
and simpl_data_declaration : Raw.data_decl -> _ result = fun t ->
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%bind annotated_expression = simpl_expression ~te_annot:t x.init in
return {name;annotated_expression}
return_let_in name annotated_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 {name;annotated_expression}
return_let_in name annotated_expression
and simpl_param : Raw.param_decl -> named_type_expression result = fun t ->
match t with
@ -341,17 +349,22 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
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
bind_map_list simpl_local_declaration local_decls 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 expression = E_lambda {binder ; input_type = input_type;
output_type = output_type; result ; body } in
let%bind result =
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression = E_lambda {
binder ;
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}}
)
@ -364,34 +377,34 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
{ type_name = arguments_name ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let tpl_declarations =
let%bind tpl_declarations =
let aux = fun i (x:named_type_expression) ->
let ass = I_assignment {
name = x.type_name ;
annotated_expression = {
expression = E_accessor ({
let expr = E_accessor ({
expression = E_variable arguments_name ;
type_annotation = Some input.type_expression ;
} , [ Access_tuple i ] ) ;
type_annotation = Some (x.type_expression) ;
}
} in
} , [ 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
ass
in
List.mapi aux params in
bind_list @@ List.mapi aux params 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
bind_map_list simpl_local_declaration local_decls in
let%bind instructions = bind_list
@@ List.map simpl_statement
@@ npseq_to_list block.value.statements in
let body = tpl_declarations @ local_declarations @ instructions in
let%bind result = simpl_expression return in
let expression = E_lambda {binder ; input_type = input_type;
output_type = output_type; result ; body } in
let%bind output_type = simpl_type_expression ret_type in
let body = tpl_declarations @ local_declarations @ instructions in
let%bind result =
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression = E_lambda {
binder ;
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}}
)
@ -420,23 +433,25 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
| 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 ->
and simpl_statement : Raw.statement -> (_ -> annotated_expression result) result = fun s ->
match s with
| Instr i -> simpl_instruction i
| Data d -> let%bind (i, _) = simpl_data_declaration d in ok i
| Data d -> simpl_data_declaration d
and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression result) result = fun t ->
match t with
| ProcCall _ -> simple_fail "no proc call"
| Fail e ->
| Fail e -> (
let%bind expr = simpl_expression e.value.fail_expr in
ok @@ I_do (untyped_expression @@ E_failwith expr)
| Skip _ -> ok @@ I_skip
return @@ e_failwith expr
)
| Skip _ -> return @@ e_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 @@ I_loop (cond, body)
let%bind body = body None in
return @@ e_loop cond body
| Loop (For _) ->
simple_fail "no for yet"
| Cond c ->
@ -448,7 +463,9 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
let%bind match_false = match c.ifnot with
| ClauseInstr i -> simpl_instruction_block i
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
ok @@ I_matching (expr, (Match_bool {match_true; match_false}))
let%bind match_true = match_true None in
let%bind match_false = match_false None in
return @@ E_matching (expr, (Match_bool {match_true; match_false}))
| Assign a -> (
let a = a.value in
let%bind value_expr = match a.rhs with
@ -458,16 +475,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
match a.lhs with
| Path path -> (
let (name , path') = simpl_path path in
match List.rev_uncons_opt path' with
| None -> (
ok @@ I_assignment {name ; annotated_expression = value_expr}
)
| Some (hds , last) -> (
match last with
| Access_record property -> ok @@ I_record_patch (name , hds , [(property , value_expr)])
| Access_tuple index -> ok @@ I_tuple_patch (name , hds , [(index , value_expr)])
| _ -> simple_fail "no map assignment in this weird case yet"
)
return @@ E_assign (name , path' , value_expr)
)
| MapPath v -> (
let v' = v.value in
@ -477,21 +485,23 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
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
ok @@ I_assignment {name = name.value ; annotated_expression = expr'}
return @@ E_assign (name.value , [] , expr')
)
)
| CaseInstr c ->
| CaseInstr c -> (
let c = c.value in
let%bind expr = simpl_expression c.expr in
let%bind cases =
let aux (x : Raw.instruction Raw.case_clause Raw.reg) =
let%bind i = simpl_instruction_block x.value.rhs in
let%bind i = i None 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 @@ I_matching (expr, m)
return @@ E_matching (expr, m)
)
| RecordPatch r -> (
let r = r.value in
let (name , access_path) = simpl_path r.path in
@ -499,7 +509,20 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
@@ 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)
@@ pseq_to_list r.record_inj.value.elements in
ok @@ I_record_patch (name, access_path, inj)
let%bind expr =
let aux = fun (access , v) ->
E_assign (name , access_path @ [ Access_record access ] , v) in
let assigns = List.map aux inj in
match assigns with
| [] -> simple_fail "empty record patch"
| hd :: tl -> (
let aux acc cur =
e_sequence (untyped_expression acc) (untyped_expression cur)
in
ok @@ List.fold_left aux hd tl
)
in
return @@ expr
)
| MapPatch _ -> simple_fail "no map patch yet"
| SetPatch _ -> simple_fail "no set patch yet"
@ -511,7 +534,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| _ -> 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
ok @@ I_assignment {name = map ; annotated_expression = make_e_a expr}
return @@ E_assign (map , [] , make_e_a expr)
| SetRemove _ -> simple_fail "no set remove yet"
and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
@ -606,12 +629,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 -> block result = fun t ->
and simpl_instruction_block : Raw.instruction -> (_ -> annotated_expression result) result = fun t ->
match t with
| Single s -> let%bind i = simpl_single_instruction s in ok [ i ]
| Single s -> simpl_single_instruction s
| Block b -> simpl_block b.value
and simpl_instruction : Raw.instruction -> instruction result = fun t ->
and simpl_instruction : Raw.instruction -> (_ -> annotated_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
@ -621,11 +644,17 @@ and simpl_instruction : Raw.instruction -> instruction result = fun t ->
| Single s -> simpl_single_instruction s
| Block _ -> simple_fail "no block instruction yet"
and simpl_statements : Raw.statements -> block result = fun ss ->
and simpl_statements : Raw.statements -> (_ -> annotated_expression result) result = fun ss ->
let lst = npseq_to_list ss in
bind_map_list simpl_statement lst
let%bind fs = bind_map_list simpl_statement lst in
let aux : _ -> (annotated_expression option -> annotated_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 -> block result = fun t ->
and simpl_block : Raw.block -> (_ -> annotated_expression result) result = fun t ->
simpl_statements t.statements
let simpl_program : Raw.ast -> program result = fun t ->

26
src/test/compiler_tests.ml
View File

@ -11,29 +11,19 @@ let run_entry_int (e:anon_function) (n:int) : int result =
| _ -> simple_fail "result is not an int"
let identity () : unit result =
let e = basic_int_quote_env in
let s = statement (S_declaration ("output", e_var_int "input")) e in
let%bind b = block [s] in
let%bind f = basic_int_quote b in
let%bind f = basic_int_quote (e_var_int "input") in
let%bind result = run_entry_int f 42 in
let%bind _ = Assert.assert_equal_int ~msg:__LOC__ 42 result in
ok ()
let multiple_vars () : unit result =
let e = basic_int_quote_env in
(*
Statements can change the environment, and you don't want to pass the new environment manually.
[statements] deals with this and this is why those statements are parametrized over an environment.
Yes. One could do a monad. Feel free when we have the time.
*)
let ss = statements [
(fun e -> statement (S_declaration ("a", e_var_int "input")) e) ;
(fun e -> statement (S_declaration ("b", e_var_int "input")) e) ;
(fun e -> statement (S_declaration ("c", e_var_int "a")) e) ;
(fun e -> statement (S_declaration ("output", e_var_int "c")) e) ;
] e in
let%bind b = block ss in
let%bind f = basic_int_quote b in
let expr =
e_let_int "a" t_int (e_var_int "input") @@
e_let_int "b" t_int (e_var_int "input") @@
e_let_int "c" t_int (e_var_int "a") @@
e_let_int "output" t_int (e_var_int "c") @@
e_var_int "output" in
let%bind f = basic_int_quote expr in
let%bind result = run_entry_int f 42 in
let%bind _ = Assert.assert_equal_int ~msg:__LOC__ 42 result in
ok ()

21
src/test/integration_tests.ml
View File

@ -15,6 +15,11 @@ let function_ () : unit result =
let make_expect = fun n -> n in
expect_eq_n_int program "main" make_expect
let assign () : unit result =
let%bind program = type_file "./contracts/assign.ligo" in
let make_expect = fun n -> n + 1 in
expect_eq_n_int program "main" make_expect
let annotation () : unit result =
let%bind program = type_file "./contracts/annotation.ligo" in
let%bind () =
@ -311,6 +316,12 @@ let condition () : unit result =
let make_expected = fun n -> e_a_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
expect_eq_n program "main" make_input make_expected
let loop () : unit result =
let%bind program = type_file "./contracts/loop.ligo" in
let%bind () =
@ -377,6 +388,13 @@ 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
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
expect_eq_n program "main" make_input make_expected
let quote_declaration () : unit result =
@ -436,11 +454,14 @@ let guess_the_hash_mligo () : unit result =
let main = "Integration (End to End)", [
test "function" function_ ;
test "assign" assign ;
test "declaration local" declaration_local ;
test "complex function" complex_function ;
test "variant" variant ;
test "variant matching" variant_matching ;
test "tuple" tuple ;
test "record" record ;
test "condition simple" condition_simple ;
test "condition" condition ;
test "shadow" shadow ;
test "annotation" annotation ;

2
src/test/test_helpers.ml
View File

@ -20,7 +20,7 @@ let expect ?options program entry_point input expecter =
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in
trace run_error @@
Ligo.easy_run_typed_simplified ~debug_michelson:false ?options entry_point program input in
Ligo.easy_run_typed_simplified ~debug_michelson:true ?options entry_point program input in
expecter result
let expect_eq ?options program entry_point input expected =

2
src/test/typer_tests.ml
View File

@ -40,7 +40,7 @@ module TestExpressions = struct
let lambda () : unit result =
test_expression
I.(e_lambda "x" t_int t_int (e_var "x") [])
I.(e_lambda "x" (Some t_int) (Some t_int) (e_var "x"))
O.(t_function (t_int ()) (t_int ()) ())
let tuple () : unit result =

381
src/transpiler/transpiler.ml
View File

@ -119,298 +119,7 @@ let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -
bind_fold_list aux (ty , []) lr_path in
ok lst
(* let rec translate_block env (b:AST.block) : block result =
* let aux = fun (precs, env) instruction ->
* let%bind lst = translate_instruction env instruction in
* let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in (\* Get last environment *\)
* ok (precs @ lst, env') in
* let%bind (instructions, env') = bind_fold_list aux ([], env) b in
* ok (instructions, environment_wrap env env')
*
* and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result =
* let return ?(env' = env) x : statement list result = ok ([x, environment_wrap env env']) in
* match i with
* | I_declaration {name;annotated_expression} ->
* let%bind expression = translate_annotated_expression annotated_expression in
* let env' = Environment.add (name, (Combinators.Expression.get_type expression)) env in
* return ~env' (S_declaration (name, expression))
* | I_assignment {name;annotated_expression} ->
* let%bind expression = translate_annotated_expression annotated_expression in
* return (S_assignment (name, expression))
* | I_patch (r, s, v) -> (
* let ty = r.type_value in
* let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result =
* fun (prev, acc) cur ->
* let%bind ty' = translate_type prev in
* match cur with
* | Access_tuple ind ->
* let%bind ty_lst = AST.Combinators.get_t_tuple prev in
* let%bind ty'_lst = bind_map_list translate_type ty_lst in
* let%bind path = tuple_access_to_lr ty' ty'_lst ind in
* let path' = List.map snd path in
* ok (List.nth ty_lst ind, acc @ path')
* | Access_record prop ->
* let%bind ty_map =
* let error =
* let title () = "accessing property on not a record" in
* let content () = Format.asprintf "%s on %a in %a"
* prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in
* error title content
* in
* trace error @@
* AST.Combinators.get_t_record prev in
* let%bind ty'_map = bind_map_smap translate_type ty_map in
* let%bind path = record_access_to_lr ty' ty'_map prop in
* let path' = List.map snd path in
* ok (Map.String.find prop ty_map, acc @ path')
* | Access_map _k -> simple_fail "no patch for map yet"
* in
* let%bind (_, path) = bind_fold_right_list aux (ty, []) s in
* let%bind v' = translate_annotated_expression v in
* return (S_patch (r.type_name, path, v'))
* )
* | I_matching (expr, m) -> (
* let%bind expr' = translate_annotated_expression expr in
* let env' = env in
* let return s =
* ok [ (s, environment_wrap env env) ] in
* 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 @@ S_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 t' = translate_type t in
* let%bind some_branch =
* let env'' = Environment.add (name, t') env' in
* translate_block env'' sm
* in
* return @@ S_if_none (expr', none_branch, ((name, t'), some_branch))
* )
* | _ -> simple_fail "todo : match"
* )
* | I_loop (expr, body) ->
* let%bind expr' = translate_annotated_expression expr in
* let%bind body' = translate_block env body in
* return (S_while (expr', body'))
* | I_skip -> ok []
* | I_do ae -> (
* let%bind ae' = translate_annotated_expression ae in
* return @@ S_do ae'
* ) *)
let rec translate_block env (b:AST.block) : block result =
let aux = fun (precs, env) instruction ->
let%bind lst = translate_instruction env instruction in
let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in (* Get last environment *)
ok (precs @ lst, env') in
let%bind (instructions, env') = bind_fold_list aux ([], env) b in
ok (instructions, environment_wrap env env')
and translate_block' : expression option -> AST.block -> expression result = fun expr_opt block ->
let aux = fun expr_opt i ->
let%bind expr = translate_instruction' i expr_opt in
ok (Some expr) in
let%bind expr_opt = bind_fold_right_list aux expr_opt block in
let default = e_unit in
ok (Option.unopt ~default expr_opt)
and translate_instruction' : AST.instruction -> expression option -> expression result = fun i expr_opt ->
let expr =
let default = e_unit in
Option.unopt ~default expr_opt in
let return ?(tv = expr.type_value) expr' = ok @@ Combinators.Expression.make_tpl (expr' , tv) in
let skip = ok expr in
let return_seq ?(tv = expr.type_value) expr' =
let lhs = Expression.make_tpl (expr' , t_unit) in
let rhs = expr in
ok @@ Combinators.Expression.make_tpl (E_sequence ( lhs , rhs ) , tv) in
match i with
| I_declaration { name ; annotated_expression } ->
let%bind rhs = translate_annotated_expression annotated_expression in
return @@ E_let_in ((name , rhs.type_value) , rhs , expr)
| I_assignment { name ; annotated_expression } ->
let%bind rhs = translate_annotated_expression annotated_expression in
return_seq @@ E_assignment (name , [] , rhs)
| I_matching (matched , clauses) -> (
let%bind expr' = translate_annotated_expression matched in
match clauses with
| Match_bool {match_true ; match_false} ->
let%bind (t , f) = bind_map_pair (translate_block' None) (match_true, match_false) in
return_seq @@ E_if_bool (expr', t, f)
| Match_option { match_none; match_some = ((name, tv), s) } ->
let%bind n = translate_block' None match_none in
let%bind (tv' , s') =
let%bind tv' = translate_type tv in
let%bind s' = translate_block' None s in
ok (tv' , s') in
return_seq @@ E_if_none (expr' , n , ((name , tv') , s'))
| Match_variant (lst , variant) -> (
let%bind tree = tree_of_sum variant in
let%bind tree' = match tree with
| Empty -> simple_fail "match empty variant"
| Full x -> ok x in
let%bind tree'' =
let rec aux t =
match (t : _ Append_tree.t') with
| Leaf (name , tv) ->
let%bind tv' = translate_type tv in
ok (`Leaf name , tv')
| Node {a ; b} ->
let%bind a' = aux a in
let%bind b' = aux b in
let tv' = Mini_c.t_union (snd a') (snd b') in
ok (`Node (a' , b') , tv')
in aux tree'
in
let rec aux top t =
match t with
| ((`Leaf constructor_name) , tv) -> (
let%bind ((_ , name) , body) =
trace_option (simple_error "not supposed to happen here: missing match clause") @@
List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in
let%bind body' = translate_block' None body in
return @@ E_let_in ((name , tv) , top , body')
)
| ((`Node (a , b)) , tv) ->
let%bind a' =
let%bind a_ty = get_t_left tv in
let a_var = "left" , a_ty in
let%bind e = aux (((Expression.make (E_variable "left") a_ty))) a in
ok (a_var , e)
in
let%bind b' =
let%bind b_ty = get_t_right tv in
let b_var = "right" , b_ty in
let%bind e = aux (((Expression.make (E_variable "right") b_ty))) b in
ok (b_var , e)
in
return @@ E_if_left (top , a' , b')
in
aux expr' tree''
)
| AST.Match_list _ | AST.Match_tuple (_, _) ->
simple_fail "only match bool, option and variants are translated yet"
)
| I_loop (condition , body) ->
let%bind condition' = translate_annotated_expression condition in
let%bind body' = translate_block' None body in
return_seq @@ E_while (condition' , body')
| I_do action ->
let%bind action' = translate_annotated_expression action in
return_seq action'.content
| I_skip -> skip
| I_patch (typed_name , path , rhs) -> (
let ty = typed_name.type_value in
let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result =
fun (prev, acc) cur ->
let%bind ty' = translate_type prev in
match cur with
| Access_tuple ind ->
let%bind ty_lst = AST.Combinators.get_t_tuple prev in
let%bind ty'_lst = bind_map_list translate_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
let path' = List.map snd path in
ok (List.nth ty_lst ind, acc @ path')
| Access_record prop ->
let%bind ty_map =
let error =
let title () = "accessing property on not a record" in
let content () = Format.asprintf "%s on %a in %a"
prop Ast_typed.PP.type_value prev Ast_typed.PP.annotated_expression rhs in
error title content
in
trace error @@
AST.Combinators.get_t_record prev in
let%bind ty'_map = bind_map_smap translate_type ty_map in
let%bind path = record_access_to_lr ty' ty'_map prop in
let path' = List.map snd path in
ok (Map.String.find prop ty_map, acc @ path')
| Access_map _k -> simple_fail "no patch for map yet"
in
let%bind (_, path) = bind_fold_right_list aux (ty, []) path in
let%bind expr' = translate_annotated_expression rhs in
return_seq (E_assignment (typed_name.type_name, path, expr'))
)
and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result =
let return ?(env' = env) x : statement list result = ok ([x, environment_wrap env env']) in
match i with
| I_declaration {name;annotated_expression} ->
let%bind expression = translate_annotated_expression annotated_expression in
let env' = Environment.add (name, (Combinators.Expression.get_type expression)) env in
return ~env' (S_declaration (name, expression))
| I_assignment {name;annotated_expression} ->
let%bind expression = translate_annotated_expression annotated_expression in
return (S_assignment (name, expression))
| I_patch (r, s, v) -> (
let ty = r.type_value in
let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result =
fun (prev, acc) cur ->
let%bind ty' = translate_type prev in
match cur with
| Access_tuple ind ->
let%bind ty_lst = AST.Combinators.get_t_tuple prev in
let%bind ty'_lst = bind_map_list translate_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
let path' = List.map snd path in
ok (List.nth ty_lst ind, acc @ path')
| Access_record prop ->
let%bind ty_map =
let error =
let title () = "accessing property on not a record" in
let content () = Format.asprintf "%s on %a in %a"
prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in
error title content
in
trace error @@
AST.Combinators.get_t_record prev in
let%bind ty'_map = bind_map_smap translate_type ty_map in
let%bind path = record_access_to_lr ty' ty'_map prop in
let path' = List.map snd path in
ok (Map.String.find prop ty_map, acc @ path')
| Access_map _k -> simple_fail "no patch for map yet"
in
let%bind (_, path) = bind_fold_right_list aux (ty, []) s in
let%bind v' = translate_annotated_expression v in
return (S_patch (r.type_name, path, v'))
)
| I_matching (expr, m) -> (
let%bind expr' = translate_annotated_expression expr in
let env' = env in
let return s =
ok [ (s, environment_wrap env env) ] in
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 @@ S_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 t' = translate_type t in
let%bind some_branch =
let env'' = Environment.add (name, t') env' in
translate_block env'' sm
in
return @@ S_if_none (expr', none_branch, ((name, t'), some_branch))
)
| _ -> simple_fail "todo : match"
)
| I_loop (expr, body) ->
let%bind expr' = translate_annotated_expression expr in
let%bind body' = translate_block env body in
return (S_while (expr', body'))
| I_skip -> ok []
| I_do ae -> (
let%bind ae' = translate_annotated_expression ae in
return @@ S_do ae'
)
and translate_literal : AST.literal -> value = fun l -> match l with
let rec translate_literal : AST.literal -> value = fun l -> match l with
| Literal_bool b -> D_bool b
| Literal_int n -> D_int n
| Literal_nat n -> D_nat n
@ -689,7 +398,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
)
and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l ->
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
let { binder ; input_type ; output_type ; result } : AST.lambda = l in
(* Deep capture. Capture the relevant part of the environment. *)
let%bind (fv , c_env , c_tv) =
let free_variables = Ast_typed.Free_variables.lambda [] l in
@ -701,17 +410,12 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express
let init_env = Environment.(add (binder , raw_input) c_env) in
let input = Environment.closure_representation init_env in
let%bind output = translate_type output_type in
let%bind (statements , body_env) = translate_block init_env body in
let body =
let load_env = Environment.(add ("closure_arg" , input) empty) in
let load_expr = Expression.make_tpl (E_variable "closure_arg" , input) in
let load_st = Mini_c.statement (S_environment_load (load_expr , init_env)) load_env in
let statements' = load_st :: statements in
(statements' , body_env)
in
let%bind result = translate_annotated_expression result in
let result =
let load_expr = Expression.make_tpl (E_variable binder , input) in
ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) result in
let tv = Mini_c.t_function input output in
let f_literal = D_function { binder ; input ; output ; body ; result } in
let f_literal = D_function { binder ; input ; output ; result } in
let expr = Expression.make_tpl (E_literal f_literal , tv) in
ok (expr , raw_input , output) in
let%bind c_expr =
@ -721,26 +425,19 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express
ok @@ Expression.make_tpl (expr , tv)
and translate_lambda env l =
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
let { binder ; input_type ; output_type ; result } : AST.lambda = l in
(* Try to translate it in an empty env, if it succeeds, transpiles it as a quote value, else, as a closure expression. *)
let ((_body_bounds , body_fvs) , result_fvs) = AST.Free_variables.(
let bindings = singleton binder in
let ((body_bounds , _) as b) = block' bindings body in
b , annotated_expression body_bounds result
) in
let fvs = AST.Free_variables.(annotated_expression (singleton binder) result) in
let%bind result =
match (body_fvs, result_fvs) with
| [] , [] -> (
let%bind empty_env =
let%bind input = translate_type input_type in
ok Environment.(add (binder, input) empty) in
let%bind body' = translate_block empty_env body in
match fvs with
| [] -> (
let%bind result' = translate_annotated_expression result in
let result' = ez_e_return result' in
trace (simple_error "translate quote") @@
let%bind input = translate_type input_type in
let%bind output = translate_type output_type in
let tv = Combinators.t_function input output in
let content = D_function {binder;input;output;body=body';result=result'} in
let content = D_function {binder;input;output;result=result'} in
ok @@ Combinators.Expression.make_tpl (E_literal content, tv)
)
| _ -> (
@ -781,36 +478,36 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value =
input_type = Combinators.t_unit () ;
output_type = t ;
result = e ;
body = [I_skip]
}, Combinators.(t_function (t_unit ()) t ())
let translate_entry (lst:AST.program) (name:string) : anon_function result =
let%bind (lst', l, _) =
let rec aux acc (lst:AST.program) =
match lst with
| [] -> None
| hd :: tl -> (
let (AST.Declaration_constant (an , _)) = temp_unwrap_loc hd in
match an.name = name with
| true -> (
match an.annotated_expression.expression with
| E_lambda l -> Some (acc, l, an.annotated_expression.type_annotation)
| _ ->
let (a, b) = functionalize an.annotated_expression in
Some (acc, a, b)
)
| false -> aux (acc @ [AST.I_declaration an]) tl
)
in
let%bind (lst', l, tv) =
trace_option (simple_error "no entry-point with given name")
@@ aux [] lst in
ok (lst', l, tv) in
let l' = {l with body = lst' @ l.body} in
let r =
trace (simple_error "translating entry") @@
translate_main l' in
r
let rec aux acc (lst:AST.program) =
let%bind acc = acc in
match lst with
| [] -> simple_fail "no entry point with given name"
| hd :: tl -> (
let (AST.Declaration_constant (an , (pre_env , _))) = temp_unwrap_loc hd in
match an.name = name with
| false -> (
let next = fun expr ->
let cur = e_a_let_in an.name an.annotated_expression expr pre_env in
acc cur in
aux (ok next) tl
)
| true -> (
match an.annotated_expression.expression with
| E_lambda l ->
let l' = { l with result = acc l.result } in
translate_main l'
| _ ->
let (l , _) = functionalize an.annotated_expression in
let l' = { l with result = acc l.result } in
translate_main l'
)
)
in
let%bind l = aux (ok (fun x -> x)) lst in
ok l
open Combinators

217
src/typer/typer.ml
View File

@ -73,146 +73,11 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
trace (constant_declaration_error name annotated_expression) @@
type_annotated_expression env annotated_expression in
let env' = Environment.add_ez_ae name ae' env in
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , env')))
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
let%bind (e', i') = type_instruction e i in
ok (e', i' @ acc)
in
let%bind (e', lst) = bind_fold_list aux (e, []) b in
ok @@ (List.rev lst, e')
and type_block (e:environment) (b:I.block) : O.block result =
let%bind (block, _) = type_block_full e b in
ok block
and type_instruction (e:environment) : I.instruction -> (environment * O.instruction list) result = fun i ->
let return x = ok (e, [x]) in
match i with
| I_skip -> return O.I_skip
| I_do x ->
let%bind expression = type_annotated_expression e x in
let%bind () =
trace_strong (simple_error "do without unit") @@
Ast_typed.assert_type_value_eq (get_type_annotation expression , t_unit ()) in
return @@ O.I_do expression
| I_loop (cond, body) ->
let%bind cond = type_annotated_expression e cond in
let%bind _ =
O.assert_type_value_eq (cond.type_annotation, t_bool ()) in
let%bind body = type_block e body in
return @@ O.I_loop (cond, body)
| I_assignment {name;annotated_expression} -> (
match annotated_expression.type_annotation, Environment.get_opt name e with
| None, None -> simple_fail "Initial assignments need type annotation"
| Some _, None ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in
let e' = Environment.add_ez_ae name annotated_expression e in
ok (e', [O.I_declaration (make_n_e name annotated_expression)])
| None, Some prev ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in
let%bind _ =
O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
ok (e, [O.I_assignment (make_n_e name annotated_expression)])
| Some _, Some prev ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in
let%bind _assert = trace (simple_error "Annotation doesn't match environment")
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
let e' = Environment.add_ez_ae name annotated_expression e in
ok (e', [O.I_assignment (make_n_e name annotated_expression)])
)
| I_matching (ex, m) -> (
let%bind ex' = type_annotated_expression e ex in
match m with
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
| I.Match_bool { match_false = [] ; match_true = [ I_do { expression = E_failwith fw } ] }
| I.Match_bool { match_false = [ I_skip ] ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
let%bind fw' = type_annotated_expression e fw in
let%bind () =
trace_strong (simple_error "Matching bool on not-a-bool")
@@ assert_t_bool (get_type_annotation ex') in
let assert_ = make_a_e
(E_constant ("ASSERT" , [ex' ; fw']))
(t_unit ())
e
in
return (O.I_do assert_)
)
| _ -> (
let%bind m' = type_match type_block e ex'.type_annotation m in
return @@ O.I_matching (ex', m')
)
)
| I_record_patch (r, path, lst) ->
let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in record_patch") @@
Environment.get_opt r e in
let tv = O.{type_name = r ; type_value = ty.type_value} in
let aux ty access =
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
let%bind ty =
trace_option (simple_error "unbound record access in record_patch") @@
Map.String.find_opt s m in
ok (ty , O.Access_record s)
| I.Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
let%bind ty =
generic_try (simple_error "unbound tuple access in record_patch") @@
(fun () -> List.nth t i) in
ok (ty , O.Access_tuple i)
| I.Access_map ind ->
let%bind (k , v) = O.Combinators.get_t_map ty in
let%bind ind' = type_annotated_expression e ind in
let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in
ok (v , O.Access_map ind')
in
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_record s]) in
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
| I_tuple_patch (r, path, lst) ->
let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in tuple_patch") @@
Environment.get_opt r e in
let tv = O.{type_name = r ; type_value = ty.type_value} in
let aux ty access =
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
let%bind ty =
trace_option (simple_error "unbound record access in tuple_patch") @@
Map.String.find_opt s m in
ok (ty , O.Access_record s)
| I.Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
let%bind ty =
generic_try (simple_error "unbound tuple access in tuple_patch") @@
(fun () -> List.nth t i) in
ok (ty , O.Access_tuple i)
| I.Access_map ind ->
let%bind (k , v) = O.Combinators.get_t_map ty in
let%bind ind' = type_annotated_expression e ind in
let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in
ok (v , O.Access_map ind')
in
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_tuple s]) in
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
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
| Match_bool {match_true ; match_false} ->
| Match_bool {match_true ; match_false} ->
let%bind _ =
trace_strong (simple_error "Matching bool on not-a-bool")
@@ get_t_bool t in
@ -354,7 +219,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (E_variable name) tv'.type_value
| E_literal (Literal_bool b) ->
return (E_literal (Literal_bool b)) (t_bool ())
| E_literal Literal_unit ->
| E_literal Literal_unit | E_skip ->
return (E_literal (Literal_unit)) (t_unit ())
| E_literal (Literal_string s) -> (
L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_value) tv_opt) ;
@ -488,14 +353,20 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
input_type ;
output_type ;
result ;
body ;
} -> (
let%bind input_type = evaluate_type e input_type in
let%bind output_type = evaluate_type e output_type in
let%bind input_type =
let%bind input_type =
trace_option (simple_error "no input type provided") @@
input_type in
evaluate_type e input_type in
let%bind output_type =
let%bind output_type =
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 (body, e'') = type_block_full e' body in
let%bind result = type_annotated_expression e'' result in
return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ())
let%bind result = type_annotated_expression e' result in
return (E_lambda {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
@ -532,7 +403,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
trace_strong (simple_error "Matching not-unit on an assert")
@@ assert_t_unit (get_type_annotation mf') in
let mt' = make_a_e
(E_failwith fw')
(E_constant ("ASSERT" , [ex' ; fw']))
(t_unit ())
e
in
@ -582,9 +453,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (O.E_loop (expr' , body')) (t_unit ())
| E_assign (name , path , expr) ->
let%bind typed_name =
let%bind ele =
trace_option (simple_error "missing var in env") @@
Environment.get_opt name e in
let%bind ele = Environment.get_trace name e in
ok @@ make_n_t name ele.type_value in
let%bind (assign_tv , path') =
let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path ->
@ -613,7 +482,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
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_binder binder rhs.type_annotation e 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
@ -685,12 +554,11 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
let%bind f' = untype_annotated_expression f in
let%bind arg' = untype_annotated_expression arg in
return (E_application (f', arg'))
| E_lambda {binder;input_type;output_type;body;result} ->
| 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
let%bind body = untype_block body in
return (E_lambda {binder;input_type = input_type;output_type = output_type;body;result})
return (E_lambda {binder;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
@ -732,51 +600,6 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
let%bind result = untype_annotated_expression result in
return (E_let_in {binder;rhs;result})
and untype_block (b:O.block) : (I.block) result =
bind_list @@ List.map untype_instruction b
and untype_instruction (i:O.instruction) : (I.instruction) result =
let open I in
match i with
| I_skip -> ok I_skip
| I_do e ->
let%bind e' = untype_annotated_expression e in
ok (I_do e')
| I_loop (e, b) ->
let%bind e' = untype_annotated_expression e in
let%bind b' = untype_block b in
ok @@ I_loop (e', b')
| I_declaration a ->
let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
ok @@ I_assignment {name = a.name ; annotated_expression}
| I_assignment a ->
let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
ok @@ I_assignment {name = a.name ; annotated_expression}
| I_matching (e, m) ->
let%bind e' = untype_annotated_expression e in
let%bind m' = untype_matching untype_block m in
ok @@ I_matching (e', m')
| I_patch (s, p, e) ->
let%bind e' = untype_annotated_expression e in
let%bind (hds, tl) =
trace_option (simple_error "patch without path") @@
List.rev_uncons_opt p in
let%bind tl_name = match tl with
| Access_record n -> ok n
| Access_tuple _ -> simple_fail "last element of patch is tuple"
| Access_map _ -> simple_fail "last element of patch is map"
in
let%bind hds' = bind_map_list untype_access hds in
ok @@ I_record_patch (s.type_name, hds', [tl_name, e'])
and untype_access (a:O.access) : I.access result =
match a with
| Access_record n -> ok @@ I.Access_record n
| Access_tuple n -> ok @@ I.Access_tuple n
| Access_map n ->
let%bind n' = untype_annotated_expression n in
ok @@ I.Access_map n'
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in
match m with