This commit is contained in:
Pierre-Emmanuel Wulfman 2020-05-28 10:53:54 +02:00
parent 294e048aff
commit e661416056
13 changed files with 20 additions and 72 deletions

View File

@ -1,4 +1,8 @@
open Ast_typed open Ast_typed
open Stage_common.Constant open Stage_common.Constant
let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1})] let environment = Ast_typed.Environment.add_ez_sum_type ~type_name:t_bool @@
[
(Constructor "true" ,{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});
(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1});
]

View File

@ -374,9 +374,6 @@ let rec transpile_literal : AST.literal -> value = fun l -> match l with
| Literal_unit -> D_unit | Literal_unit -> D_unit
| Literal_void -> D_none | Literal_void -> D_none
(* 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 -> and tree_of_sum : AST.type_expression -> (AST.constructor' * AST.type_expression) Append_tree.t result = fun t ->
let%bind map_tv = get_t_sum t in let%bind map_tv = get_t_sum t in
let kt_list = List.map (fun (k,({ctor_type;_}:AST.ctor_content)) -> (k,ctor_type)) (kv_list_of_cmap map_tv) in let kt_list = List.map (fun (k,({ctor_type;_}:AST.ctor_content)) -> (k,ctor_type)) (kv_list_of_cmap map_tv) in
@ -397,10 +394,6 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
return (E_let_in ((let_binder, rhs'.type_expression), 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_literal l -> return @@ E_literal (transpile_literal l)
| E_variable name -> ( | E_variable name -> (
(* let%bind ele =
* trace_option (corner_case ~loc:__LOC__ "name not in environment") @@
* AST.Environment.get_opt name ae.environment in
* let%bind tv = transpile_environment_element_type tv in *)
return @@ E_variable (name) return @@ E_variable (name)
) )
| E_application {lamb; args} -> | E_application {lamb; args} ->
@ -441,7 +434,6 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
return ~tv ae return ~tv ae
) )
| E_record m -> ( | E_record m -> (
(*list_of_lmap to record_to_list*)
let node = Append_tree.of_list @@ Ast_typed.Helpers.list_of_record_or_tuple m in let node = Append_tree.of_list @@ Ast_typed.Helpers.list_of_record_or_tuple m in
let aux a b : expression result = let aux a b : expression result =
let%bind a = a in let%bind a = a in
@ -779,7 +771,9 @@ let transpile_program (lst : AST.program) : program result =
ok statements ok statements
(* check whether the storage contains a big_map, if yes, check that (* check whether the storage contains a big_map, if yes, check that
it appears on the left hand side of a pair *) it appears on the left hand side of a pair
TODO : checking should appears in check_pass.
*)
let check_storage f ty loc : (anon_function * _) result = let check_storage f ty loc : (anon_function * _) result =
let rec aux (t:type_expression) on_big_map = let rec aux (t:type_expression) on_big_map =
match t.type_content with match t.type_content with

View File

@ -494,27 +494,25 @@ let rec type_program (p:I.program) : (O.program * O.typer_state) result =
let%bind ed' = (bind_map_location (type_declaration e (Solver.placeholder_for_state_of_new_typer ()))) d in let%bind ed' = (bind_map_location (type_declaration e (Solver.placeholder_for_state_of_new_typer ()))) d in
let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
let (e', _placeholder_for_state_of_new_typer , d') = Location.unwrap ed' in let (e', _placeholder_for_state_of_new_typer , d') = Location.unwrap ed' in
match d' with ok (e', loc ed' d' :: acc)
| None -> ok (e', acc)
| Some d' -> ok (e', loc ed' d' :: acc)
in in
let%bind (_, lst) = let%bind (_, lst) =
trace (fun () -> program_error p ()) @@ trace (fun () -> program_error p ()) @@
bind_fold_list aux (DEnv.default, []) p in bind_fold_list aux (DEnv.default, []) p in
ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ())) ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ()))
and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration option) result = function and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration) result = function
| Declaration_type (type_binder , type_expr) -> | Declaration_type (type_binder , type_expr) ->
let%bind tv = evaluate_type env type_expr in let%bind tv = evaluate_type env type_expr in
let env' = Environment.add_type (type_binder) tv env in let env' = Environment.add_type (type_binder) tv env in
ok (env', (Solver.placeholder_for_state_of_new_typer ()) , Some (O.Declaration_type { type_binder ; type_expr = tv } )) ok (env', (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_type { type_binder ; type_expr = tv } ))
| Declaration_constant (binder , tv_opt , inline, expression) -> ( | Declaration_constant (binder , tv_opt , inline, expression) -> (
let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
let%bind expr = let%bind expr =
trace (constant_declaration_error binder expression tv'_opt) @@ trace (constant_declaration_error binder expression tv'_opt) @@
type_expression' ?tv_opt:tv'_opt env expression in type_expression' ?tv_opt:tv'_opt env expression in
let post_env = Environment.add_ez_declaration binder expr env in let post_env = Environment.add_ez_declaration binder expr env in
ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , Some (O.Declaration_constant { binder ; expr ; inline})) ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_constant { binder ; expr ; inline}))
) )
and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result = and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result =

View File

@ -39,7 +39,7 @@ module Errors : sig
end end
val type_program : I.program -> (O.program * O.typer_state) result val type_program : I.program -> (O.program * O.typer_state) result
val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration option) result val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration) result
(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *) (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
val evaluate_type : environment -> I.type_expression -> O.type_expression result val evaluate_type : environment -> I.type_expression -> O.type_expression result
val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result

View File

@ -13,7 +13,6 @@ let contract_passes = [
let all_program program = let all_program program =
let all_p = List.map Helpers.map_program all_passes in let all_p = List.map Helpers.map_program all_passes in
let%bind program' = bind_chain all_p program in let%bind program' = bind_chain all_p program in
(* let program'' = Recompute_environment.program Environment.default program' in *)
ok program' ok program'
let all_expression = let all_expression =

View File

@ -4,7 +4,6 @@ module PP = PP
module PP_generic = PP_generic module PP_generic = PP_generic
module Combinators = struct module Combinators = struct
include Combinators include Combinators
include Combinators_environment
end end
module Misc = struct module Misc = struct
include Misc include Misc

View File

@ -1,25 +0,0 @@
open Types
open Combinators
(* let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.empty *)
(* let e_a_empty_unit = e_a_unit Environment.empty
* let e_a_empty_int n = e_a_int n Environment.empty
* let e_a_empty_nat n = e_a_nat n Environment.empty
* let e_a_empty_mutez n = e_a_mutez n Environment.empty
* let e_a_empty_bool b = e_a_bool b Environment.empty
* let e_a_empty_string s = e_a_string s Environment.empty
* let e_a_empty_address s = e_a_address s Environment.empty
* let e_a_empty_pair a b = e_a_pair a b Environment.empty
* let e_a_empty_some s = e_a_some s Environment.empty
* let e_a_empty_none t = e_a_none t Environment.empty
* let e_a_empty_record r = e_a_record r Environment.empty
* let ez_e_a_empty_record r = ez_e_a_record r Environment.empty
* let e_a_empty_lambda l i o = e_a_lambda l i o Environment.empty *)
open Environment
let env_sum_type ?(env = empty)
?(type_name = Var.of_name "a_sum_type")
(lst : (constructor' * ctor_content) list) =
add_type type_name (make_t_ez_sum lst) env

View File

@ -1,19 +0,0 @@
open Types
(* val make_a_e_empty : expression_content -> type_expression -> expression
*
* val e_a_empty_unit : expression
* val e_a_empty_int : Z.t -> expression
* val e_a_empty_nat : Z.t -> expression
* val e_a_empty_mutez : Z.t -> expression
* val e_a_empty_bool : bool -> expression
* val e_a_empty_string : ligo_string -> expression
* val e_a_empty_address : string -> expression
* val e_a_empty_pair : expression -> expression -> expression
* val e_a_empty_some : expression -> expression
* val e_a_empty_none : type_expression -> expression
* val e_a_empty_record : expression label_map -> expression
* val ez_e_a_empty_record : ( label * expression ) list -> expression
* val e_a_empty_lambda : lambda -> type_expression -> type_expression -> expression *)
val env_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> environment

View File

@ -38,6 +38,9 @@ let add_ez_binder : expression_variable -> type_expression -> t -> t = fun k v e
let add_ez_declaration : expression_variable -> expression -> t -> t = fun k ae e -> let add_ez_declaration : expression_variable -> expression -> t -> t = fun k ae e ->
add_expr k (make_element_declaration e ae) e add_expr k (make_element_declaration e ae) e
let add_ez_sum_type ?(env = empty) ?(type_name = Var.of_name "a_sum_type") (lst : (constructor' * ctor_content) list) =
add_type type_name (make_t_ez_sum lst) env
let convert_constructor' (S.Constructor c) = Constructor c let convert_constructor' (S.Constructor c) = Constructor c
let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option = fun k x -> (* Left is the constructor, right is the sum type *) let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option = fun k x -> (* Left is the constructor, right is the sum type *)
@ -76,4 +79,4 @@ module PP = struct
expr_environment (get_expr_environment e) expr_environment (get_expr_environment e)
type_environment (get_type_environment e) type_environment (get_type_environment e)
end end

View File

@ -11,6 +11,7 @@ val get_opt : expression_variable -> t -> element option
val get_type_opt : type_variable -> t -> type_expression option val get_type_opt : type_variable -> t -> type_expression option
val get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option val get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option
val add_ez_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> environment
module PP : sig module PP : sig
open Format open Format

View File

@ -522,11 +522,6 @@ let get_entry (lst : program) (name : string) : expression result =
in in
List.find_map aux lst List.find_map aux lst
(* let program_environment (program : program) : environment =
* let last_declaration = Location.unwrap List.(hd @@ rev program) in
* match last_declaration with
* | Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env *)
let equal_variables a b : bool = let equal_variables a b : bool =
match a.expression_content, b.expression_content with match a.expression_content, b.expression_content with
| E_variable a, E_variable b -> Var.equal a b | E_variable a, E_variable b -> Var.equal a b

View File

@ -70,7 +70,6 @@ val assert_literal_eq : ( literal * literal ) -> unit result
*) *)
val get_entry : program -> string -> expression result val get_entry : program -> string -> expression result
(* val program_environment : program -> environment *)
val p_constant : constant_tag -> p_ctor_args -> type_value val p_constant : constant_tag -> p_ctor_args -> type_value
val c_equation : type_value -> type_value -> string -> type_constraint val c_equation : type_value -> type_value -> string -> type_constraint

View File

@ -34,7 +34,7 @@ module TestExpressions = struct
module I = Simplified.Combinators module I = Simplified.Combinators
module O = Typed.Combinators module O = Typed.Combinators
module E = O module E = Typed.Environment
let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ()) let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ())
let int () : unit result = test_expression I.(e_int (Z.of_int 32)) O.(t_int ()) let int () : unit result = test_expression I.(e_int (Z.of_int 32)) O.(t_int ())
@ -59,7 +59,7 @@ module TestExpressions = struct
(Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None ; ctor_decl_pos = 0}); (Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None ; ctor_decl_pos = 0});
(Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None ; ctor_decl_pos = 1}) ] (Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None ; ctor_decl_pos = 1}) ]
in test_expression in test_expression
~env:(E.env_sum_type variant_foo_bar) ~env:(E.add_ez_sum_type variant_foo_bar)
I.(e_constructor "foo" (e_int (Z.of_int 32))) I.(e_constructor "foo" (e_int (Z.of_int 32)))
O.(make_t_ez_sum variant_foo_bar) O.(make_t_ez_sum variant_foo_bar)