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

Merge branch 'refactoring_mini-c_type' into 'dev'

Browse Source 
Refactor Mini-c types for conformity with the other stage

See merge request ligolang/ligo!598
This commit is contained in:
Pierre-Emmanuel Wulfman 2020-05-13 11:01:20 +00:00
commit 7bcf46d3bc
18 changed files with 192 additions and 178 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/main/compile/of_mini_c.ml
View File

@ -4,17 +4,17 @@ open Trace
let compile_contract : expression -> Compiler.compiled_expression result = fun e ->
let%bind e = Self_mini_c.contract_check e in
let%bind (input_ty , _) = get_t_function e.type_value in
let%bind (input_ty , _) = get_t_function e.type_expression in
let%bind body = get_function e in
let%bind body = Compiler.Program.translate_function_body body [] input_ty in
let expr = Self_michelson.optimize body in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_expression in
ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
let compile_expression : expression -> Compiler.compiled_expression result = fun e ->
let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in
let expr = Self_michelson.optimize expr in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_expression in
ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
let aggregate_and_compile = fun program form ->

100
src/passes/10-transpiler/transpiler.ml
View File

@ -233,51 +233,53 @@ let transpile_constant' : AST.constant' -> constant' = function
| C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
| C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB
let rec transpile_type (t:AST.type_expression) : type_value result =
let rec transpile_type (t:AST.type_expression) : type_expression result =
let return tc = ok @@ Expression.make_t @@ tc in
match t.type_content with
| T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> ok (T_base TB_bool)
| t when (compare t (t_bool ()).type_content) = 0-> ok (T_base TB_bool)
| T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> return (T_base TB_bool)
| t when (compare t (t_bool ()).type_content) = 0-> return (T_base TB_bool)
| T_variable (name) -> fail @@ no_type_variable @@ name
| T_constant (TC_int) -> ok (T_base TB_int)
| T_constant (TC_nat) -> ok (T_base TB_nat)
| T_constant (TC_mutez) -> ok (T_base TB_mutez)
| T_constant (TC_string) -> ok (T_base TB_string)
| T_constant (TC_bytes) -> ok (T_base TB_bytes)
| T_constant (TC_address) -> ok (T_base TB_address)
| T_constant (TC_timestamp) -> ok (T_base TB_timestamp)
| T_constant (TC_unit) -> ok (T_base TB_unit)
| T_constant (TC_operation) -> ok (T_base TB_operation)
| T_constant (TC_signature) -> ok (T_base TB_signature)
| T_constant (TC_key) -> ok (T_base TB_key)
| T_constant (TC_key_hash) -> ok (T_base TB_key_hash)
| T_constant (TC_chain_id) -> ok (T_base TB_chain_id)
| T_constant (TC_void) -> ok (T_base TB_void)
| T_constant (TC_int) -> return (T_base TB_int)
| T_constant (TC_nat) -> return (T_base TB_nat)
| T_constant (TC_mutez) -> return (T_base TB_mutez)
| T_constant (TC_string) -> return (T_base TB_string)
| T_constant (TC_bytes) -> return (T_base TB_bytes)
| T_constant (TC_address) -> return (T_base TB_address)
| T_constant (TC_timestamp) -> return (T_base TB_timestamp)
| T_constant (TC_unit) -> return (T_base TB_unit)
| T_constant (TC_operation) -> return (T_base TB_operation)
| T_constant (TC_signature) -> return (T_base TB_signature)
| T_constant (TC_key) -> return (T_base TB_key)
| T_constant (TC_key_hash) -> return (T_base TB_key_hash)
| T_constant (TC_chain_id) -> return (T_base TB_chain_id)
| T_constant (TC_void) -> return (T_base TB_void)
| T_operator (TC_contract x) ->
let%bind x' = transpile_type x in
ok (T_contract x')
return (T_contract x')
| T_operator (TC_map {k;v}) ->
let%bind kv' = bind_map_pair transpile_type (k, v) in
ok (T_map kv')
return (T_map kv')
| T_operator (TC_big_map {k;v}) ->
let%bind kv' = bind_map_pair transpile_type (k, v) in
ok (T_big_map kv')
return (T_big_map kv')
| T_operator (TC_map_or_big_map _) ->
fail @@ corner_case ~loc:"transpiler" "TC_map_or_big_map should have been resolved before transpilation"
| T_operator (TC_list t) ->
let%bind t' = transpile_type t in
ok (T_list t')
return (T_list t')
| T_operator (TC_set t) ->
let%bind t' = transpile_type t in
ok (T_set t')
return (T_set t')
| T_operator (TC_option o) ->
let%bind o' = transpile_type o in
ok (T_option o')
return (T_option o')
| T_sum m when Ast_typed.Helpers.is_michelson_or m ->
let node = Append_tree.of_list @@ kv_list_of_cmap m in
let aux a b : type_value annotated result =
let aux a b : type_expression annotated result =
let%bind a = a in
let%bind b = b in
ok (None, T_or (a, b))
let%bind t = return @@ T_or (a,b) in
ok (None, t)
in
let%bind m' = Append_tree.fold_ne
(fun (_, ({ctor_type ; michelson_annotation}: AST.ctor_content)) ->
@ -287,10 +289,11 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
ok @@ snd m'
| T_sum m ->
let node = Append_tree.of_list @@ kv_list_of_cmap m in
let aux a b : type_value annotated result =
let aux a b : type_expression annotated result =
let%bind a = a in
let%bind b = b in
ok (None, T_or (a, b))
let%bind t = return @@ T_or (a,b) in
ok (None, t)
in
let%bind m' = Append_tree.fold_ne
(fun (Ast_typed.Types.Constructor ann, ({ctor_type ; _}: AST.ctor_content)) ->
@ -300,10 +303,11 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
ok @@ snd m'
| T_record m when Ast_typed.Helpers.is_michelson_pair m ->
let node = Append_tree.of_list @@ Ast_typed.Helpers.tuple_of_record m in
let aux a b : type_value annotated result =
let aux a b : type_expression annotated result =
let%bind a = a in
let%bind b = b in
ok (None, T_pair (a, b))
let%bind t = return @@ T_pair (a, b) in
ok (None, t)
in
let%bind m' = Append_tree.fold_ne
(fun (_, ({field_type ; michelson_annotation} : AST.field_content)) ->
@ -320,10 +324,11 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
List.rev @@ Ast_typed.Types.LMap.to_kv_list m
)
in
let aux a b : type_value annotated result =
let aux a b : type_expression annotated result =
let%bind a = a in
let%bind b = b in
ok (None, T_pair (a, b))
let%bind t = return @@ T_pair (a, b) in
ok (None, t)
in
let%bind m' = Append_tree.fold_ne
(fun (Ast_typed.Types.Label ann, ({field_type;_}: AST.field_content)) ->
@ -339,10 +344,10 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
| T_arrow {type1;type2} -> (
let%bind param' = transpile_type type1 in
let%bind result' = transpile_type type2 in
ok (T_function (param',result'))
return @@ (T_function (param',result'))
)
let record_access_to_lr : type_value -> type_value AST.label_map -> AST.label -> (type_value * [`Left | `Right]) list result = fun ty tym ind ->
let record_access_to_lr : type_expression -> type_expression AST.label_map -> AST.label -> (type_expression * [`Left | `Right]) list result = fun ty tym ind ->
let tys = Ast_typed.Helpers.kv_list_of_record_or_tuple tym in
let node_tv = Append_tree.of_list tys in
let%bind path =
@ -377,7 +382,7 @@ let rec transpile_literal : AST.literal -> value = fun l -> match l with
| Literal_unit -> D_unit
| Literal_void -> D_none
and transpile_environment_element_type : AST.environment_element -> type_value result = fun ele ->
and transpile_environment_element_type : AST.environment_element -> type_expression result = fun ele ->
transpile_type ele.type_value
and tree_of_sum : AST.type_expression -> (AST.constructor' * AST.type_expression) Append_tree.t result = fun t ->
@ -397,7 +402,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
| E_let_in {let_binder; rhs; let_result; inline} ->
let%bind rhs' = transpile_annotated_expression rhs in
let%bind result' = transpile_annotated_expression let_result in
return (E_let_in ((let_binder, rhs'.type_value), inline, rhs', result'))
return (E_let_in ((let_binder, rhs'.type_expression), inline, rhs', result'))
| E_literal l -> return @@ E_literal (transpile_literal l)
| E_variable name -> (
let%bind ele =
@ -418,7 +423,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
let%bind node_tv =
trace_strong (corner_case ~loc:__LOC__ "getting lr tree") @@
tree_of_sum ae.type_expression in
let leaf (k, tv) : (expression' option * type_value) result =
let leaf (k, tv) : (expression_content option * type_expression) result =
if k = constructor then (
let%bind _ =
trace_strong (corner_case ~loc:__LOC__ "wrong type for constructor parameter")
@ -428,14 +433,14 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
let%bind tv = transpile_type tv in
ok (None, tv)
) in
let node a b : (expression' option * type_value) result =
let node a b : (expression_content option * type_expression) result =
let%bind a = a in
let%bind b = b in
match (a, b) with
| (None, a), (None, b) -> ok (None, T_or ((None, a), (None, b)))
| (None, a), (None, b) -> ok (None, Expression.make_t @@ T_or ((None, a), (None, b)))
| (Some _, _), (Some _, _) -> fail @@ corner_case ~loc:__LOC__ "multiple identical constructors in the same variant"
| (Some v, a), (None, b) -> ok (Some (E_constant {cons_name=C_LEFT ;arguments= [Combinators.Expression.make_tpl (v, a)]}), T_or ((None, a), (None, b)))
| (None, a), (Some v, b) -> ok (Some (E_constant {cons_name=C_RIGHT;arguments= [Combinators.Expression.make_tpl (v, b)]}), T_or ((None, a), (None, b)))
| (Some v, a), (None, b) -> ok (Some (E_constant {cons_name=C_LEFT ;arguments= [Combinators.Expression.make_tpl (v, a)]}), Expression.make_t @@ T_or ((None, a), (None, b)))
| (None, a), (Some v, b) -> ok (Some (E_constant {cons_name=C_RIGHT;arguments= [Combinators.Expression.make_tpl (v, b)]}), Expression.make_t @@ T_or ((None, a), (None, b)))
in
let%bind (ae_opt, tv) = Append_tree.fold_ne leaf node node_tv in
let%bind ae =
@ -451,7 +456,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
let%bind b = b in
let a_ty = Combinators.Expression.get_type a in
let b_ty = Combinators.Expression.get_type b in
let tv = T_pair ((None, a_ty) , (None, b_ty)) in
let tv = Combinators.Expression.make_t @@ T_pair ((None, a_ty) , (None, b_ty)) in
return ~tv @@ E_constant {cons_name=C_PAIR;arguments=[a; b]}
in
trace_strong (corner_case ~loc:__LOC__ "record build") @@
@ -652,7 +657,7 @@ and transpile_lambda l (input_type , output_type) =
ok @@ Combinators.Expression.make_tpl (closure , tv)
and transpile_recursive {fun_name; fun_type; lambda} =
let rec map_lambda : AST.expression_variable -> type_value -> AST.expression -> (expression * expression_variable list) result = fun fun_name loop_type e ->
let rec map_lambda : AST.expression_variable -> type_expression -> AST.expression -> (expression * expression_variable list) result = fun fun_name loop_type e ->
match e.expression_content with
E_lambda {binder;result} ->
let%bind (body,l) = map_lambda fun_name loop_type result in
@ -661,7 +666,7 @@ and transpile_recursive {fun_name; fun_type; lambda} =
let%bind res = replace_callback fun_name loop_type false e in
ok @@ (res, [])
and replace_callback : AST.expression_variable -> type_value -> bool -> AST.expression -> expression result = fun fun_name loop_type shadowed e ->
and replace_callback : AST.expression_variable -> type_expression -> bool -> AST.expression -> expression result = fun fun_name loop_type shadowed e ->
match e.expression_content with
E_let_in li ->
let shadowed = shadowed || Var.equal li.let_binder fun_name in
@ -684,7 +689,8 @@ and transpile_recursive {fun_name; fun_type; lambda} =
_ ->
let%bind expr = transpile_annotated_expression e in
ok @@ Expression.make (E_constant {cons_name=C_LOOP_STOP;arguments=[expr]}) loop_type
and matching : AST.expression_variable -> type_value -> bool -> AST.matching -> type_value -> expression result = fun fun_name loop_type shadowed m ty ->
and matching : AST.expression_variable -> type_expression -> bool -> AST.matching -> type_expression -> expression result = fun fun_name loop_type shadowed m ty ->
let return ret = ok @@ Expression.make ret @@ ty in
let%bind expr = transpile_annotated_expression m.matchee in
match m.cases with
@ -793,8 +799,8 @@ let transpile_program (lst : AST.program) : program result =
(* check whether the storage contains a big_map, if yes, check that
it appears on the left hand side of a pair *)
let check_storage f ty loc : (anon_function * _) result =
let rec aux (t:type_value) on_big_map =
match t with
let rec aux (t:type_expression) on_big_map =
match t.type_content with
| T_big_map _ -> on_big_map
| T_pair (a , b) -> (aux (snd a) true) && (aux (snd b) false)
| T_or (a,b) -> (aux (snd a) false) && (aux (snd b) false)
@ -806,7 +812,7 @@ let check_storage f ty loc : (anon_function * _) result =
| T_option a -> (aux a false)
| _ -> true
in
match f.body.type_value with
match f.body.type_expression.type_content with
| T_pair (_, storage) ->
if aux (snd storage) false then ok (f, ty) else fail @@ bad_big_map loc
| _ -> ok (f, ty)

4
src/passes/11-self_mini_c/helpers.ml
View File

@ -1,10 +1,10 @@
open Mini_c
open Trace
let rec fold_type_value : ('a -> type_value -> 'a result) -> 'a -> type_value -> 'a result = fun f init t ->
let rec fold_type_value : ('a -> type_expression -> 'a result) -> 'a -> type_expression -> 'a result = fun f init t ->
let self = fold_type_value f in
let%bind init' = f init t in
match t with
match t.type_content with
| T_pair ((_, a), (_, b))
| T_or ((_, a), (_, b))
| T_function (a, b)

8
src/passes/11-self_mini_c/self_mini_c.ml
View File

@ -147,12 +147,12 @@ let inline_lets : bool ref -> expression -> expression =
let beta : bool ref -> expression -> expression =
fun changed e ->
match e.content with
| E_application ({ content = E_closure { binder = x ; body = e1 } ; type_value = T_function (xtv, tv) }, e2) ->
| E_application ({ content = E_closure { binder = x ; body = e1 } ; type_expression = {type_content = T_function (xtv, tv);_ }}, e2) ->
(changed := true ;
Expression.make (E_let_in ((x, xtv), false, e2, e1)) tv)
(* also do CAR (PAIR x y) ↦ x, or CDR (PAIR x y) ↦ y, only if x and y are pure *)
| E_constant {cons_name = C_CAR| C_CDR as const; arguments = [ { content = E_constant {cons_name = C_PAIR; arguments = [ e1 ; e2 ]} ; type_value = _ } ]} ->
| E_constant {cons_name = C_CAR| C_CDR as const; arguments = [ { content = E_constant {cons_name = C_PAIR; arguments = [ e1 ; e2 ]} ; type_expression = _ } ]} ->
if is_pure e1 && is_pure e2
then (changed := true ;
match const with
@ -169,8 +169,8 @@ let betas : bool ref -> expression -> expression =
let eta : bool ref -> expression -> expression =
fun changed e ->
match e.content with
| E_constant {cons_name = C_PAIR; arguments = [ { content = E_constant {cons_name = C_CAR; arguments = [ e1 ]} ; type_value = _ } ;
{ content = E_constant {cons_name = C_CDR; arguments = [ e2 ]} ; type_value = _ }]} ->
| E_constant {cons_name = C_PAIR; arguments = [ { content = E_constant {cons_name = C_CAR; arguments = [ e1 ]} ; type_expression = _ } ;
{ content = E_constant {cons_name = C_CDR; arguments = [ e2 ]} ; type_expression = _ }]} ->
(match (e1.content, e2.content) with
| E_variable x1, E_variable x2 ->
if Var.equal x1 x2

13
src/passes/11-self_mini_c/subst.ml
View File

@ -117,12 +117,11 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
(* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons:
intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *)
let subst_binder2 y z expr' =
let dummy = T_base TB_unit in
let hack = { content = E_closure { binder = z ; body = expr' } ;
type_value = dummy } in
let dummy = Expression.make_t @@ T_base TB_unit in
let hack = Expression.make (E_closure { binder = z ; body = expr' }) dummy in
match subst_binder y hack with
| (y', { content = E_closure { binder = z' ; body = body } ; type_value = _dummy }) ->
(y', z', { body with type_value = expr'.type_value })
| (y', { content = E_closure { binder = z' ; body = body } ; type_expression = _dummy }) ->
(y', z', { body with type_expression = expr'.type_expression })
| _ -> assert false in
let return content = {body with content} in
let return_id = body in
@ -199,8 +198,8 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
)
let%expect_test _ =
let dummy_type = T_base TB_unit in
let wrap e = { content = e ; type_value = dummy_type } in
let dummy_type = Expression.make_t @@ T_base TB_unit in
let wrap e = Expression.make e dummy_type in
let show_subst ~body ~x ~expr =
Format.printf "(%a)[%a := %a] =@ %a"

20
src/passes/12-compiler/compiler_program.ml
View File

@ -27,14 +27,14 @@ end
open Errors
(* This does not makes sense to me *)
let rec get_operator : constant' -> type_value -> expression list -> predicate result = fun s ty lst ->
let rec get_operator : constant' -> type_expression -> expression list -> predicate result = fun s ty lst ->
match Operators.Compiler.get_operators s with
| Ok (x,_) -> ok x
| Error _ -> (
match s with
| C_SELF -> (
let%bind entrypoint_as_string = match lst with
| [{ content = E_literal (D_string s); type_value = _ }] -> (
| [{ content = E_literal (D_string s); type_expression = _ }] -> (
match String.split_on_char '%' s with
| ["" ; s] -> ok @@ String.concat "" ["%" ; (String.uncapitalize_ascii s)]
| _ -> fail @@ corner_case ~loc:__LOC__ "mini_c . SELF"
@ -128,7 +128,7 @@ let rec get_operator : constant' -> type_value -> expression list -> predicate r
let%bind r = get_t_contract ty in
let%bind r_ty = Compiler_type.type_ r in
let%bind entry = match lst with
| [ { content = E_literal (D_string entry); type_value = _ } ; _addr ] -> ok entry
| [ { content = E_literal (D_string entry); type_expression = _ } ; _addr ] -> ok entry
| [ _entry ; _addr ] ->
fail @@ contract_entrypoint_must_be_literal ~loc:__LOC__
| _ ->
@ -143,7 +143,7 @@ let rec get_operator : constant' -> type_value -> expression list -> predicate r
let%bind r = get_t_contract tc in
let%bind r_ty = Compiler_type.type_ r in
let%bind entry = match lst with
| [ { content = E_literal (D_string entry); type_value = _ } ; _addr ] -> ok entry
| [ { content = E_literal (D_string entry); type_expression = _ } ; _addr ] -> ok entry
| [ _entry ; _addr ] ->
fail @@ contract_entrypoint_must_be_literal ~loc:__LOC__
| _ ->
@ -154,7 +154,7 @@ let rec get_operator : constant' -> type_value -> expression list -> predicate r
]
| C_CREATE_CONTRACT ->
let%bind ch = match lst with
| { content= E_closure {body;binder} ; type_value = T_function (T_pair ((_,p),(_,s)) as tin,_)} :: _ ->
| { content= E_closure {body;binder} ; type_expression = {type_content=T_function ({type_content=T_pair ((_,p),(_,s));_} as tin,_);_}} :: _ ->
let%bind closure = translate_function_body {body;binder} [] tin in
let%bind (p',s') = bind_map_pair Compiler_type.type_ (p,s) in
ok @@ contract p' s' closure
@ -244,14 +244,14 @@ and translate_expression (expr:expression) (env:environment) : michelson result
let%bind t = Compiler_type.type_ ty in
return @@ i_push t v
| E_closure anon -> (
match ty with
match ty.type_content with
| T_function (input_ty , output_ty) ->
translate_function anon env input_ty output_ty
| _ -> simple_fail "expected function type"
)
| E_application (f , arg) -> (
trace (simple_error "Compiling quote application") @@
let%bind f = translate_expression f (Environment.add (Var.fresh (), arg.type_value) env) in
let%bind f = translate_expression f (Environment.add (Var.fresh (), arg.type_expression) env) in
let%bind arg = translate_expression arg env in
return @@ seq [
arg ;
@ -281,7 +281,7 @@ and translate_expression (expr:expression) (env:environment) : michelson result
PP.expression expr
Michelson.pp expr_code
PP.environment env ;
let env = Environment.add (Var.fresh (), expr.type_value) env in
let env = Environment.add (Var.fresh (), expr.type_expression) env in
let code = code @ [expr_code] in
ok (code, env) in
bind_fold_right_list aux ([], env) lst in
@ -433,7 +433,7 @@ and translate_expression (expr:expression) (env:environment) : michelson result
let%bind collection' =
translate_expression
collection
(Environment.add (Var.fresh (), initial.type_value) env) in
(Environment.add (Var.fresh (), initial.type_expression) env) in
let%bind initial' = translate_expression initial env in
let%bind body' = translate_expression body (Environment.add v env) in
let code = seq [
@ -450,7 +450,7 @@ and translate_expression (expr:expression) (env:environment) : michelson result
let%bind record' = translate_expression record env in
let record_var = Var.fresh () in
let env' = Environment.add (record_var, record.type_value) env in
let env' = Environment.add (record_var, record.type_expression) env in
let%bind expr' = translate_expression expr env' in
let modify_code =
let aux acc step = match step with

6
src/passes/12-compiler/compiler_program.mli
View File

@ -14,10 +14,10 @@ type compiled_expression = {
expr : michelson ;
}
val get_operator : constant' -> type_value -> expression list -> predicate result
val get_operator : constant' -> type_expression -> expression list -> predicate result
val translate_expression : expression -> environment -> michelson result
val translate_function_body : anon_function -> environment_element list -> type_value -> michelson result
val translate_value : value -> type_value -> michelson result
val translate_function_body : anon_function -> environment_element list -> type_expression -> michelson result
val translate_value : value -> type_expression -> michelson result
(*

16
src/passes/12-compiler/compiler_type.ml
View File

@ -92,8 +92,8 @@ module Ty = struct
| Timestamp_key annot -> ok (Timestamp_key annot)
| Address_key annot -> ok (Address_key annot)
let rec comparable_type : type_value -> ex_comparable_ty result = fun tv ->
match tv with
let rec comparable_type : type_expression -> ex_comparable_ty result = fun tv ->
match tv.type_content with
| T_base b -> comparable_type_base b
| T_function _ -> fail (not_comparable "function")
| T_or _ -> fail (not_comparable "or")
@ -128,8 +128,8 @@ module Ty = struct
| TB_key_hash -> return key_hash
| TB_chain_id -> return chain_id
let rec type_ : type_value -> ex_ty result =
function
let rec type_ : type_expression -> ex_ty result =
fun te -> match te.type_content with
| T_base b -> base_type b
| T_pair (t, t') -> (
annotated t >>? fun (ann, Ex_ty t) ->
@ -167,7 +167,7 @@ module Ty = struct
let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty (contract t')
and annotated : type_value annotated -> ex_ty annotated result =
and annotated : type_expression annotated -> ex_ty annotated result =
fun (ann, a) -> let%bind a = type_ a in
ok @@ (ann, a)
@ -213,8 +213,8 @@ let base_type : type_base -> O.michelson result =
| TB_key_hash -> ok @@ O.prim T_key_hash
| TB_chain_id -> ok @@ O.prim T_chain_id
let rec type_ : type_value -> O.michelson result =
function
let rec type_ : type_expression -> O.michelson result =
fun te -> match te.type_content with
| T_base b -> base_type b
| T_pair (t, t') -> (
annotated t >>? fun t ->
@ -249,7 +249,7 @@ let rec type_ : type_value -> O.michelson result =
let%bind ret = type_ ret in
ok @@ O.prim ~children:[arg;ret] T_lambda
and annotated : type_value annotated -> O.michelson result =
and annotated : type_expression annotated -> O.michelson result =
function
| (Some ann, o) ->
let%bind o' = type_ o in

10
src/passes/12-compiler/compiler_type.mli
View File

@ -63,7 +63,7 @@ module Ty : sig
val comparable_type : type_value -> ex_comparable_ty result
val base_type : type_base -> ex_ty result
*)
val type_ : type_value -> ex_ty result
val type_ : type_expression -> ex_ty result
val environment_representation : environment -> ex_ty result
@ -81,12 +81,12 @@ module Ty : sig
*)
end
val type_ : type_value -> O.t result
val type_ : type_expression -> O.t result
val environment_element : string * type_value -> (int, O.prim) Tezos_micheline.Micheline.node result
val environment_element : string * type_expression -> (int, O.prim) Tezos_micheline.Micheline.node result
val environment : ( 'a * type_value ) list -> O.t list result
val lambda_closure : environment * type_value * type_value -> (int, O.prim) Tezos_micheline.Micheline.node result
val environment : ( 'a * type_expression ) list -> O.t list result
val lambda_closure : environment * type_expression * type_expression -> (int, O.prim) Tezos_micheline.Micheline.node result
val environment_closure : environment -> (int , O.prim ) Tezos_micheline.Micheline.node result
(*

18
src/stages/5-mini_c/PP.ml
View File

@ -7,7 +7,7 @@ let list_sep_d x = list_sep x (tag " ,@ ")
let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R"
let rec type_variable ppf : type_value -> _ = function
let rec type_variable ppf : type_expression -> _ = fun te -> match te.type_content with
| T_or(a, b) -> fprintf ppf "@[(%a) |@ (%a)@]" annotated a annotated b
| T_pair(a, b) -> fprintf ppf "@[(%a) &@ (%a)@]" annotated a annotated b
| T_base b -> type_constant ppf b
@ -19,7 +19,7 @@ let rec type_variable ppf : type_value -> _ = function
| T_option(o) -> fprintf ppf "@[<7>option(%a)@]" type_variable o
| T_contract(t) -> fprintf ppf "@[<9>contract(%a)@]" type_variable t
and annotated ppf : type_value annotated -> _ = function
and annotated ppf : type_expression annotated -> _ = function
| (Some ann, a) -> fprintf ppf "(%a %%%s)" type_variable a ann
| (None, a) -> type_variable ppf a
@ -74,9 +74,9 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" value a value b
and expression ppf (e:expression) =
fprintf ppf "%a" expression' e.content
fprintf ppf "%a" expression_content e.content
and expression' ppf (e:expression') = match e with
and expression_content ppf (e:expression_content) = match e with
| E_skip -> fprintf ppf "skip"
| E_closure x -> function_ ppf x
| E_variable v -> fprintf ppf "%a" Var.pp v
@ -113,8 +113,8 @@ and expression' ppf (e:expression') = match e with
and expression_with_type : _ -> expression -> _ = fun ppf e ->
fprintf ppf "%a : %a"
expression' e.content
type_variable e.type_value
expression_content e.content
type_variable e.type_expression
and function_ ppf ({binder ; body}:anon_function) =
fprintf ppf "@[fun %a ->@ (%a)@]"
@ -258,9 +258,9 @@ let%expect_test _ =
[%expect{| 0x666f6f |}]
let%expect_test _ =
let pp = expression' Format.std_formatter in
let dummy_type = T_base TB_unit in
let wrap e = { content = e ; type_value = dummy_type } in
let pp = expression_content Format.std_formatter in
let dummy_type = {type_content=T_base TB_unit} in
let wrap e = { content = e ; type_expression = dummy_type} in
pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ;
[%expect{|
fun y -> (y)

4
src/stages/5-mini_c/PP.mli
View File

@ -8,7 +8,7 @@ val lr : formatter -> [< `Left ] -> unit
val type_base : formatter -> type_base -> unit
*)
val type_variable : formatter -> type_value -> unit
val type_variable : formatter -> type_expression -> unit
val environment_element : formatter -> environment_element -> unit
val environment : formatter -> environment -> unit
val value : formatter -> value -> unit
@ -16,7 +16,7 @@ val value : formatter -> value -> unit
(*
val value_assoc : formatter -> (value * value) -> unit
*)
val expression' : formatter -> expression' -> unit
val expression_content : formatter -> expression_content -> unit
val expression : formatter -> expression -> unit
val expression_with_type : formatter -> expression -> unit

58
src/stages/5-mini_c/combinators.ml
View File

@ -2,20 +2,24 @@ open Trace
open Types
module Expression = struct
type t' = expression'
type t' = expression_content
type t = expression
let get_content : t -> t' = fun e -> e.content
let get_type : t -> type_value = fun e -> e.type_value
let get_type : t -> type_expression = fun e -> e.type_expression
let make_t = fun tc -> {
type_content = tc;
}
let make = fun e' t -> {
content = e' ;
type_value = t ;
type_expression = t ;
}
let make_tpl = fun (e' , t) -> {
content = e' ;
type_value = t ;
type_expression = t ;
}
let pair : t -> t -> t' = fun a b -> E_constant { cons_name = C_PAIR; arguments = [ a ; b ]}
@ -76,7 +80,7 @@ let get_set (v:value) = match v with
| _ -> simple_fail "not a set"
let get_function_with_ty (e : expression) =
match (e.content , e.type_value) with
match (e.content , e.type_expression.type_content) with
| E_closure f , T_function ty -> ok (f , ty)
| _ -> simple_fail "not a function with functional type"
@ -85,11 +89,11 @@ let get_function (e : expression) =
| E_closure f -> ok f
| _ -> simple_fail "not a function"
let get_t_function tv = match tv with
let get_t_function tv = match tv.type_content with
| T_function ty -> ok ty
| _ -> simple_fail "not a function"
let get_t_option (v:type_value) = match v with
let get_t_option (v:type_expression) = match v.type_content with
| T_option t -> ok t
| _ -> simple_fail "not an option"
@ -97,27 +101,27 @@ let get_pair (v:value) = match v with
| D_pair (a, b) -> ok (a, b)
| _ -> simple_fail "not a pair"
let get_t_pair (t:type_value) = match t with
let get_t_pair (t:type_expression) = match t.type_content with
| T_pair ((_, a), (_, b)) -> ok (a, b)
| _ -> simple_fail "not a type pair"
let get_t_or (t:type_value) = match t with
let get_t_or (t:type_expression) = match t.type_content with
| T_or ((_, a), (_, b)) -> ok (a, b)
| _ -> simple_fail "not a type or"
let get_t_map (t:type_value) = match t with
let get_t_map (t:type_expression) = match t.type_content with
| T_map kv -> ok kv
| _ -> simple_fail "not a type map"
let get_t_big_map (t:type_value) = match t with
let get_t_big_map (t:type_expression) = match t.type_content with
| T_big_map kv -> ok kv
| _ -> simple_fail "not a type big_map"
let get_t_list (t:type_value) = match t with
let get_t_list (t:type_expression) = match t.type_content with
| T_list t -> ok t
| _ -> simple_fail "not a type list"
let get_t_set (t:type_value) = match t with
let get_t_set (t:type_expression) = match t.type_content with
| T_set t -> ok t
| _ -> simple_fail "not a type set"
@ -139,19 +143,19 @@ let wrong_type name t =
let content () = Format.asprintf "%a" PP.type_variable t in
error title content
let get_t_left t = match t with
let get_t_left t = match t.type_content with
| T_or ((_, a) , _) -> ok a
| _ -> fail @@ wrong_type "union" t
let get_t_right t = match t with
let get_t_right t = match t.type_content with
| T_or (_ , (_, b)) -> ok b
| _ -> fail @@ wrong_type "union" t
let get_t_contract t = match t with
let get_t_contract t = match t.type_content with
| T_contract x -> ok x
| _ -> fail @@ wrong_type "contract" t
let get_t_operation t = match t with
let get_t_operation t = match t.type_content with
| T_base TB_operation -> ok t
| _ -> fail @@ wrong_type "operation" t
@ -160,24 +164,24 @@ let get_operation (v:value) = match v with
| _ -> simple_fail "not an operation"
let t_int : type_value = T_base TB_int
let t_unit : type_value = T_base TB_unit
let t_nat : type_value = T_base TB_nat
let t_int () : type_expression = Expression.make_t @@ T_base TB_int
let t_unit () : type_expression = Expression.make_t @@ T_base TB_unit
let t_nat () : type_expression = Expression.make_t @@ T_base TB_nat
let t_function x y : type_value = T_function ( x , y )
let t_pair x y : type_value = T_pair ( x , y )
let t_union x y : type_value = T_or ( x , y )
let t_function x y : type_expression = Expression.make_t @@ T_function ( x , y )
let t_pair x y : type_expression = Expression.make_t @@ T_pair ( x , y )
let t_union x y : type_expression = Expression.make_t @@ T_or ( x , y )
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_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_in v tv inline expr body : expression = Expression.(make_tpl (
E_let_in ((v , tv) , inline, 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_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl (a , t_unit ()) , b) , get_type b))
let d_unit : value = D_unit

49
src/stages/5-mini_c/combinators.mli
View File

@ -2,16 +2,17 @@ open Trace
open Types
module Expression : sig
type t' = expression'
type t' = expression_content
type t = expression
val get_content : t -> t'
val get_type : t -> type_value
val get_type : t -> type_expression
(*
val is_toplevel : t -> bool
*)
val make : t' -> type_value -> t
val make_tpl : t' * type_value -> t
val make_t : type_content -> type_expression
val make : t' -> type_expression -> t
val make_tpl : t' * type_expression -> t
val pair : t -> t -> t'
end
@ -29,35 +30,35 @@ val get_map : value -> ( value * value ) list result
val get_big_map : value -> ( value * value ) list result
val get_list : value -> value list result
val get_set : value -> value list result
val get_function_with_ty : expression -> ( anon_function * ( type_value * type_value) ) result
val get_function_with_ty : expression -> ( anon_function * ( type_expression * type_expression) ) result
val get_function : expression -> anon_function result
val get_t_function : type_value -> ( type_value * type_value ) result
val get_t_option : type_value -> type_value result
val get_t_function : type_expression -> ( type_expression * type_expression ) result
val get_t_option : type_expression -> type_expression result
val get_pair : value -> ( value * value ) result
val get_t_pair : type_value -> ( type_value * type_value ) result
val get_t_or : type_value -> ( type_value * type_value ) result
val get_t_map : type_value -> ( type_value * type_value ) result
val get_t_big_map : type_value -> ( type_value * type_value ) result
val get_t_list : type_value -> type_value result
val get_t_set : type_value -> type_value result
val get_t_pair : type_expression -> ( type_expression * type_expression ) result
val get_t_or : type_expression -> ( type_expression * type_expression ) result
val get_t_map : type_expression -> ( type_expression * type_expression ) result
val get_t_big_map : type_expression -> ( type_expression * type_expression ) result
val get_t_list : type_expression -> type_expression result
val get_t_set : type_expression -> type_expression result
val get_left : value -> value result
val get_right : value -> value result
val get_or : value -> ( bool * value ) result
(*
val wrong_type : string -> type_value -> unit -> error
*)
val get_t_left : type_value -> type_value result
val get_t_right : type_value -> type_value result
val get_t_contract : type_value -> type_value result
val get_t_operation : type_value -> type_value result
val get_t_left : type_expression -> type_expression result
val get_t_right : type_expression -> type_expression result
val get_t_contract : type_expression -> type_expression result
val get_t_operation : type_expression -> type_expression result
val get_operation : value -> Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation result
val t_int : type_value
val t_unit : type_value
val t_nat : type_value
val t_function : type_value -> type_value -> type_value
val t_pair : type_value annotated -> type_value annotated -> type_value
val t_union : type_value annotated -> type_value annotated -> type_value
val t_int : unit -> type_expression
val t_unit : unit -> type_expression
val t_nat : unit -> type_expression
val t_function : type_expression -> type_expression -> type_expression
val t_pair : type_expression annotated -> type_expression annotated -> type_expression
val t_union : type_expression annotated -> type_expression annotated -> type_expression
(*
val quote : string -> type_value -> type_value -> Expression.t -> anon_function
@ -67,7 +68,7 @@ val e_int : Expression.t' -> Expression.t
val e_unit : Expression.t
val e_skip : Expression.t
val e_var_int : expression_variable -> Expression.t
val e_let_in : expression_variable -> type_value -> inline -> Expression.t -> Expression.t -> Expression.t
val e_let_in : expression_variable -> type_expression -> inline -> Expression.t -> Expression.t -> Expression.t
val ez_e_sequence : Expression.t' -> Expression.t -> expression
(*

2
src/stages/5-mini_c/combinators_smart.ml
View File

@ -3,4 +3,4 @@ open Combinators
let basic_int_quote_env : environment =
let e = Environment.empty in
Environment.add (Var.of_name "input", t_int) e
Environment.add (Var.of_name "input", t_int ()) e

4
src/stages/5-mini_c/environment.ml
View File

@ -21,12 +21,12 @@ module Environment (* : ENVIRONMENT *) = struct
let empty : t = []
let add : element -> t -> t = List.cons
let concat : t list -> t = List.concat
let get_opt : expression_variable -> t -> type_value option = List.assoc_opt ~compare:Var.compare
let get_opt : expression_variable -> t -> type_expression option = List.assoc_opt ~compare:Var.compare
let has : expression_variable -> t -> bool = fun s t ->
match get_opt s t with
| None -> false
| Some _ -> true
let get_i : expression_variable -> t -> (type_value * int) = List.assoc_i ~compare:Var.compare
let get_i : expression_variable -> t -> (type_expression * int) = List.assoc_i ~compare:Var.compare
let of_list : element list -> t = fun x -> x
let to_list : t -> element list = fun x -> x
let get_names : t -> expression_variable list = List.map fst

2
src/stages/5-mini_c/environment.mli
View File

@ -14,7 +14,7 @@ module Environment : sig
val get_opt : Var.t -> t -> type_value option
val has : Var.t -> t -> bool
*)
val get_i : expression_variable -> t -> (type_value * int)
val get_i : expression_variable -> t -> (type_expression * int)
val of_list : element list -> t
val to_list : t -> element list
val get_names : t -> expression_variable list

4
src/stages/5-mini_c/misc.ml
View File

@ -143,7 +143,7 @@ let aggregate_entry (lst : program) (form : form_t) : expression result =
let wrapper =
let aux prec cur =
let (((name , inline, expr) , _)) = cur in
e_let_in name expr.type_value inline expr prec
e_let_in name expr.type_expression inline expr prec
in
fun expr -> List.fold_right' aux expr lst
in
@ -154,7 +154,7 @@ let aggregate_entry (lst : program) (form : form_t) : expression result =
let l' = { l with body = wrapper l.body } in
let e' = {
content = E_closure l' ;
type_value = entry_expression.type_value ;
type_expression = entry_expression.type_expression ;
} in
ok e'
)

46
src/stages/5-mini_c/types.ml
View File

@ -2,17 +2,21 @@ include Stage_common.Types
type 'a annotated = string option * 'a
type type_value =
| T_pair of (type_value annotated * type_value annotated)
| T_or of (type_value annotated * type_value annotated)
| T_function of (type_value * type_value)
type type_content =
| T_pair of (type_expression annotated * type_expression annotated)
| T_or of (type_expression annotated * type_expression annotated)
| T_function of (type_expression * type_expression)
| T_base of type_base
| T_map of (type_value * type_value)
| T_big_map of (type_value * type_value)
| T_list of type_value
| T_set of type_value
| T_contract of type_value
| T_option of type_value
| T_map of (type_expression * type_expression)
| T_big_map of (type_expression * type_expression)
| T_list of type_expression
| T_set of type_expression
| T_contract of type_expression
| T_option of type_expression
and type_expression = {
type_content : type_content;
}
and type_base =
| TB_unit
@ -31,7 +35,7 @@ and type_base =
| TB_timestamp
| TB_void
and environment_element = expression_variable * type_value
and environment_element = expression_variable * type_expression
and environment = environment_element list
@ -68,28 +72,28 @@ type value =
and selector = var_name list
and expression' =
and expression_content =
| E_literal of value
| E_closure of anon_function
| E_skip
| E_constant of constant
| E_application of (expression * expression)
| E_variable of var_name
| E_make_none of type_value
| E_iterator of constant' * ((var_name * type_value) * expression) * expression
| E_fold of (((var_name * type_value) * expression) * expression * expression)
| E_make_none of type_expression
| E_iterator of constant' * ((var_name * type_expression) * expression) * expression
| E_fold of (((var_name * type_expression) * expression) * expression * expression)
| E_if_bool of (expression * expression * expression)
| E_if_none of expression * expression * ((var_name * type_value) * expression)
| E_if_cons of (expression * expression * (((var_name * type_value) * (var_name * type_value)) * expression))
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
| E_let_in of ((var_name * type_value) * inline * expression * expression)
| E_if_none of expression * expression * ((var_name * type_expression) * expression)
| E_if_cons of (expression * expression * (((var_name * type_expression) * (var_name * type_expression)) * expression))
| E_if_left of expression * ((var_name * type_expression) * expression) * ((var_name * type_expression) * expression)
| E_let_in of ((var_name * type_expression) * inline * expression * expression)
| E_sequence of (expression * expression)
| E_record_update of (expression * [`Left | `Right] list * expression)
| E_while of (expression * expression)
and expression = {
content : expression' ;
type_value : type_value ;
content : expression_content ;
type_expression : type_expression ;
}
and constant = {