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

Merge branch 'cleanup/environment' into 'dev'

Browse Source 
some environment cleanup

See merge request ligolang/ligo!608
This commit is contained in:
Rémi Lesenechal 2020-05-07 15:53:09 +00:00
commit 19866476d7
24 changed files with 122 additions and 203 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/bin/expect_tests/contract_tests.ml
View File

@ -1425,7 +1425,7 @@ let%expect_test _ =
let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ;
[%expect {|
ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]]\n- E[]\tT[bool -> sum[false -> unit , true -> unit]]]"}
ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]\nbool -> sum[false -> unit , true -> unit]]"}
If you're not sure how to fix this error, you can
@ -1465,7 +1465,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ;
[%expect {|
ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"no suggestion"}
ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[bool -> sum[false -> unit , true -> unit]]","did_you_mean":"no suggestion"}
If you're not sure how to fix this error, you can

2
src/bin/expect_tests/typer_error_tests.ml
View File

@ -119,7 +119,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"bool"}
ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[bool -> sum[false -> unit , true -> unit]]","did_you_mean":"bool"}
If you're not sure how to fix this error, you can

12
src/environment/environment.ml
View File

@ -1,11 +1 @@
open Ast_typed
let merge e1 e2 =
let e1 = List.Ne.to_list e1 in
let e2 = List.Ne.to_list e2 in
List.Ne.of_list @@ e1 @ e2
let default = Environment.full_empty
let default = merge default Bool.environment
let default = Bool.environment

2
src/main/compile/of_core.ml
View File

@ -13,7 +13,7 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * As
| Env -> ok applied in
ok @@ (applied', state)
let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression)
let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression)
: (Ast_typed.expression * Ast_typed.typer_state) result =
let%bind (ae_typed,state) = Typer.type_expression_subst env state e in
let () = Typer.Solver.discard_state state in

4
src/passes/10-transpiler/untranspiler.ml
View File

@ -48,13 +48,13 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (e_bool b Environment.full_empty)
return (e_bool b Environment.empty)
)
| t when (compare t (t_bool ()).type_content) = 0-> (
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (e_bool b Environment.full_empty)
return (e_bool b Environment.empty)
)
| T_constant type_constant -> (
match type_constant with

6
src/passes/8-typer-new/errors.ml
View File

@ -10,7 +10,7 @@ let unbound_type_variable (e:environment) (tv:I.type_variable) (loc:Location.t)
let data = [
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
("in" , fun () -> Format.asprintf "%a" Environment.PP.environment e)
] in
error ~data title message ()
@ -20,7 +20,7 @@ let unbound_variable (e:environment) (n:I.expression_variable) (loc:Location.t)
let message () = "" in
let data = [
("variable" , name) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
@ -60,7 +60,7 @@ let unbound_constructor (e:environment) (c:I.constructor') (loc:Location.t) () =
let message () = "" in
let data = [
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()

4
src/passes/8-typer-new/typer.ml
View File

@ -28,7 +28,7 @@ let rec type_declaration env state : I.declaration -> (environment * O.typer_sta
let%bind (expr , state') =
trace (constant_declaration_error binder expression tv'_opt) @@
type_expression env state expression in
let post_env = Environment.add_ez_ae binder expr env in
let post_env = Environment.add_ez_declaration binder expr env in
ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline ; post_env} ))
)
@ -286,7 +286,7 @@ and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression
let content () =
Format.asprintf "%a in:\n%a\n"
Stage_common.PP.constructor constructor
O.Environment.PP.full_environment e
O.Environment.PP.environment e
in
error title content in
trace_option error @@

12
src/passes/8-typer-old/typer.ml
View File

@ -40,7 +40,7 @@ module Errors = struct
let data = [
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("in" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
("did_you_mean" , fun () -> suggestion)
] in
error ~data title message ()
@ -51,7 +51,7 @@ module Errors = struct
let message () = "" in
let data = [
("variable" , name) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
@ -91,7 +91,7 @@ module Errors = struct
let message () = "" in
let data = [
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c);
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
@ -101,7 +101,7 @@ module Errors = struct
let message () = "" in
let data = [
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c);
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ;
] in
error ~data title message ()
@ -514,7 +514,7 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) :
let%bind expr =
trace (constant_declaration_error binder expression tv'_opt) @@
type_expression' ?tv_opt:tv'_opt env expression in
let post_env = Environment.add_ez_ae 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 ; post_env}))
)
@ -766,7 +766,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
let content () =
Format.asprintf "%a in:\n%a\n"
Stage_common.PP.constructor constructor
O.Environment.PP.full_environment e
O.Environment.PP.environment e
in
error title content in
trace_option error @@

2
src/passes/9-self_ast_typed/michelson_layout.ml
View File

@ -25,7 +25,7 @@ let match_var (t:type_expression) =
{ expression_content = E_variable (Var.of_name "x") ;
location = Location.generated ;
type_expression = t ;
environment = Environment.add_ez_binder (Var.of_name "x") t Environment.full_empty}
environment = Environment.add_ez_binder (Var.of_name "x") t Environment.empty}
let matching (e:expression) matchee cases =
{ expression_content = E_matching {matchee ; cases};

8
src/stages/1-ast_imperative/types.ml
View File

@ -189,17 +189,15 @@ and free_variables = expression_variable list
and environment_element =
{ type_value: type_expression
; source_environment: full_environment
; source_environment: environment
; definition: environment_element_definition }
and environment = (expression_variable * environment_element) list
and expr_environment = (expression_variable * environment_element) list
and type_environment = (type_variable * type_expression) list
(* SUBST ??? *)
and small_environment = environment * type_environment
and full_environment = small_environment List.Ne.t
and environment = expr_environment * type_environment
and expr = expression

8
src/stages/2-ast_sugar/types.ml
View File

@ -147,17 +147,15 @@ and free_variables = expression_variable list
and environment_element =
{ type_value: type_expression
; source_environment: full_environment
; source_environment: environment
; definition: environment_element_definition }
and environment = (expression_variable * environment_element) list
and expr_environment = (expression_variable * environment_element) list
and type_environment = (type_variable * type_expression) list
(* SUBST ??? *)
and small_environment = environment * type_environment
and full_environment = small_environment List.Ne.t
and environment = expr_environment * type_environment
and expr = expression

8
src/stages/3-ast_core/types.ml
View File

@ -92,17 +92,15 @@ and free_variables = expression_variable list
and environment_element =
{ type_value: type_expression
; source_environment: full_environment
; source_environment: environment
; definition: environment_element_definition }
and environment = (expression_variable * environment_element) list
and expr_environment = (expression_variable * environment_element) list
and type_environment = (type_variable * type_expression) list
(* SUBST ??? *)
and small_environment = environment * type_environment
and full_environment = small_environment List.Ne.t
and environment = expr_environment * type_environment
and expr = expression

5
src/stages/4-ast_typed/PP_generic.ml
View File

@ -27,7 +27,6 @@ let needs_parens = {
label_map = (fun _ _ _ _ -> false) ;
list = (fun _ _ _ _ -> false) ;
location_wrap = (fun _ _ _ _ -> false) ;
list_ne = (fun _ _ _ _ -> false) ;
option = (fun _visitor _continue _state o ->
match o with None -> false | Some _ -> true) ;
poly_unionfind = (fun _ _ _ _ -> false) ;
@ -80,10 +79,10 @@ let op ppf = {
location_wrap = (fun _visitor continue () lwrap ->
let ({ wrap_content; location } : _ Location.wrap) = lwrap in
fprintf ppf "{ wrap_content = %a ; location = %a }" (fun _ppf -> continue ()) wrap_content Location.pp location);
list_ne = (fun _visitor continue () (first, lst) ->
(* list_ne = (fun _visitor continue () (first, lst) ->
let aux ppf elt =
fprintf ppf "%a" (fun _ppf -> continue ()) elt in
fprintf ppf "[@,@[<hv 2> %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) (first::lst));
fprintf ppf "[@,@[<hv 2> %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) (first::lst)); *)
option = (fun _visitor continue () o ->
match o with
| None -> fprintf ppf "None"

38
src/stages/4-ast_typed/combinators.mli
View File

@ -3,7 +3,7 @@ open Types
val make_n_t : type_variable -> type_expression -> named_type_content
val make_t : ?loc:Location.t -> type_content -> S.type_expression option -> type_expression
val make_e : ?location:Location.t -> expression_content -> type_expression -> full_environment -> expression
val make_e : ?location:Location.t -> expression_content -> type_expression -> environment -> expression
val t_bool : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
val t_string : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
@ -38,7 +38,7 @@ val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.t
val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
val get_type_expression : expression -> type_expression
val get_type' : type_expression -> type_content
val get_environment : expression -> full_environment
val get_environment : expression -> environment
val get_expression : expression -> expression_content
val get_lambda : expression -> lambda result
val get_lambda_with_type : expression -> (lambda * ( type_expression * type_expression) ) result
@ -115,7 +115,7 @@ val e_unit : unit -> expression_content
val e_int : Z.t -> expression_content
val e_nat : Z.t -> expression_content
val e_mutez : Z.t -> expression_content
val e_bool : bool -> full_environment -> expression_content
val e_bool : bool -> environment -> expression_content
val e_string : string -> expression_content
val e_bytes : bytes -> expression_content
val e_timestamp : Z.t -> expression_content
@ -131,22 +131,22 @@ val e_application : expression -> expression -> expression_content
val e_variable : expression_variable -> expression_content
val e_let_in : expression_variable -> inline -> expression -> expression -> expression_content
val e_a_unit : full_environment -> expression
val e_a_int : Z.t -> full_environment -> expression
val e_a_nat : Z.t -> full_environment -> expression
val e_a_mutez : Z.t -> full_environment -> expression
val e_a_bool : bool -> full_environment -> expression
val e_a_string : string -> full_environment -> expression
val e_a_address : string -> full_environment -> expression
val e_a_pair : expression -> expression -> full_environment -> expression
val e_a_some : expression -> full_environment -> expression
val e_a_lambda : lambda -> type_expression -> type_expression -> full_environment -> expression
val e_a_none : type_expression -> full_environment -> expression
val e_a_record : expression label_map -> full_environment -> expression
val e_a_application : expression -> expression -> full_environment -> expression
val e_a_variable : expression_variable -> type_expression -> full_environment -> expression
val ez_e_a_record : ( label * expression ) list -> full_environment -> expression
val e_a_let_in : expression_variable -> bool -> expression -> expression -> full_environment -> expression
val e_a_unit : environment -> expression
val e_a_int : Z.t -> environment -> expression
val e_a_nat : Z.t -> environment -> expression
val e_a_mutez : Z.t -> environment -> expression
val e_a_bool : bool -> environment -> expression
val e_a_string : string -> environment -> expression
val e_a_address : string -> environment -> expression
val e_a_pair : expression -> expression -> environment -> expression
val e_a_some : expression -> environment -> expression
val e_a_lambda : lambda -> type_expression -> type_expression -> environment -> expression
val e_a_none : type_expression -> environment -> expression
val e_a_record : expression label_map -> environment -> expression
val e_a_application : expression -> expression -> environment -> expression
val e_a_variable : expression_variable -> type_expression -> environment -> expression
val ez_e_a_record : ( label * expression ) list -> environment -> expression
val e_a_let_in : expression_variable -> bool -> expression -> expression -> environment -> expression
val get_a_int : expression -> Z.t result
val get_a_unit : expression -> unit result

30
src/stages/4-ast_typed/combinators_environment.ml
View File

@ -1,25 +1,25 @@
open Types
open Combinators
let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.full_empty
let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.empty
let e_a_empty_unit = e_a_unit Environment.full_empty
let e_a_empty_int n = e_a_int n Environment.full_empty
let e_a_empty_nat n = e_a_nat n Environment.full_empty
let e_a_empty_mutez n = e_a_mutez n Environment.full_empty
let e_a_empty_bool b = e_a_bool b Environment.full_empty
let e_a_empty_string s = e_a_string s Environment.full_empty
let e_a_empty_address s = e_a_address s Environment.full_empty
let e_a_empty_pair a b = e_a_pair a b Environment.full_empty
let e_a_empty_some s = e_a_some s Environment.full_empty
let e_a_empty_none t = e_a_none t Environment.full_empty
let e_a_empty_record r = e_a_record r Environment.full_empty
let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty
let e_a_empty_lambda l i o = e_a_lambda l i o Environment.full_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 = full_empty)
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

2
src/stages/4-ast_typed/combinators_environment.mli
View File

@ -16,4 +16,4 @@ 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:full_environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> full_environment
val env_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> environment

65
src/stages/4-ast_typed/environment.ml
View File

@ -1,52 +1,46 @@
open Types
open Combinators
type t = environment
type element = environment_element
let make_element : type_expression -> full_environment -> environment_element_definition -> element =
let make_element : type_expression -> environment -> environment_element_definition -> element =
fun type_value source_environment definition -> {type_value ; source_environment ; definition}
let make_element_binder = fun t s -> make_element t s ED_binder
let make_element_declaration = fun s (expr : expression) ->
let free_variables = Misc.Free_variables.(expression empty expr) in
make_element (get_type_expression expr) s (ED_declaration {expr ; free_variables})
module Small = struct
type t = small_environment
let empty : t = { expression_environment = [] ; type_environment = [] }
(* TODO: generate *)
let get_environment : t -> environment = fun { expression_environment ; type_environment=_ } -> expression_environment
let get_expr_environment : t -> expression_environment = fun { expression_environment ; type_environment=_ } -> expression_environment
(* TODO: generate *)
let get_type_environment : t -> type_environment = fun { expression_environment=_ ; type_environment } -> type_environment
(* TODO: generate *)
let map_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment = f expression_environment ; type_environment }
let map_expr_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment = f expression_environment ; type_environment }
let map_type_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment ; type_environment = f type_environment }
let add : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_environment (fun x -> {expr_var ; env_elt} :: x)
let add_expr : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_expr_environment (fun x -> {expr_var ; env_elt} :: x)
let add_type : type_variable -> type_expression -> t -> t = fun type_variable type_ -> map_type_environment (fun x -> { type_variable ; type_ } :: x)
(* TODO: generate : these are now messy, clean them up. *)
let get_opt : expression_variable -> t -> element option = fun k x -> Option.bind (fun {expr_var=_ ; env_elt} -> Some env_elt) @@ List.find_opt (fun {expr_var ; env_elt=_} -> Var.equal expr_var k) (get_environment x)
let get_type_opt : type_variable -> t -> type_expression option = fun k x -> Option.bind (fun {type_variable=_ ; type_} -> Some type_) @@ List.find_opt (fun {type_variable ; type_=_} -> Var.equal type_variable k) (get_type_environment x)
end
let get_opt : expression_variable -> t -> element option = fun k x ->
Option.bind (fun {expr_var=_ ; env_elt} -> Some env_elt) @@
List.find_opt (fun {expr_var ; env_elt=_} -> Var.equal expr_var k) (get_expr_environment x)
let get_type_opt : type_variable -> t -> type_expression option = fun k x ->
Option.bind (fun {type_variable=_ ; type_} -> Some type_) @@
List.find_opt (fun {type_variable ; type_=_} -> Var.equal type_variable k) (get_type_environment x)
type t = full_environment
let empty : environment = Small.(get_environment empty)
let full_empty : t = List.Ne.singleton Small.empty
let add : expression_variable -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v)
let add_ez_binder : expression_variable -> type_expression -> t -> t = fun k v e ->
List.Ne.hd_map (Small.add k (make_element_binder v e)) e
add_expr k (make_element_binder v e) e
let add_ez_declaration : expression_variable -> expression -> t -> t = fun k ae e ->
List.Ne.hd_map (Small.add k (make_element_declaration e ae)) e
let add_ez_ae = add_ez_declaration
let add_type : type_variable -> type_expression -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v)
let get_opt : expression_variable -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x
let get_type_opt : type_variable -> t -> type_expression option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x
add_expr k (make_element_declaration e ae) e
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 aux = fun x ->
let aux = fun {type_variable=_ ; type_} ->
match type_.type_content with
| T_sum m ->
@ -55,8 +49,7 @@ let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expr
| None -> None)
| _ -> None
in
List.find_map aux (Small.get_type_environment x) in
List.Ne.find_map aux x
List.find_map aux (get_type_environment x)
module PP = struct
@ -72,27 +65,15 @@ module PP = struct
let type_environment_element = fun ppf {type_variable ; type_} ->
fprintf ppf "%a -> %a" PP.type_variable type_variable PP.type_expression type_
let environment : _ -> environment -> unit = fun ppf lst ->
fprintf ppf "E[%a]" (list_sep environment_element (const " , ")) lst
let expr_environment : _ -> expression_environment -> unit = fun ppf lst ->
fprintf ppf "E[%a]" (list_sep environment_element (tag "@,")) lst
let type_environment = fun ppf lst ->
fprintf ppf "T[%a]" (list_sep type_environment_element (const " , ")) lst
fprintf ppf "T[%a]" (list_sep type_environment_element (tag "@,")) lst
let small_environment : _ -> small_environment -> unit = fun ppf e ->
let environment : _ -> environment -> unit = fun ppf e ->
fprintf ppf "- %a\t%a"
environment (Small.get_environment e)
type_environment (Small.get_type_environment e)
expr_environment (get_expr_environment e)
type_environment (get_type_environment e)
let full_environment : _ -> full_environment -> unit = fun ppf e ->
fprintf ppf "@[%a]"
(ne_list_sep small_environment (tag "@;")) e
end
open Trace
let get_trace : expression_variable -> t -> element result = fun s env ->
let error =
let title () = "missing var not in env" in
let content () = Format.asprintf "\nvar: %a\nenv: %a\n" PP. expression_variable s PP.full_environment env in
error title content in
trace_option error @@ get_opt s env

46
src/stages/4-ast_typed/environment.mli
View File

@ -1,62 +1,20 @@
open Types
open Trace
type t = full_environment
type t = environment
type element = environment_element
val get_trace : expression_variable -> t -> element result
val empty : environment
val full_empty : t
val add : expression_variable -> element -> t -> t
val empty : t
val add_ez_binder : expression_variable -> type_expression -> t -> t
val add_ez_declaration : expression_variable -> expression -> t -> t
val add_ez_ae : expression_variable -> expression -> t -> t
val add_type : type_variable -> type_expression -> t -> t
val get_opt : expression_variable -> t -> element option
val get_type_opt : type_variable -> t -> type_expression option
val get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option
module Small : sig
type t = small_environment
val get_environment : t -> environment
(*
val empty : t
val get_type_environment : t -> type_environment
val map_environment : ( environment -> environment ) -> t -> t
val map_type_environment : ( type_environment -> type_environment ) -> t -> t
val add : string -> element -> t -> t
val add_type : string -> type_expression -> t -> t
val get_opt : string -> t -> element option
val get_type_opt : string -> t -> type_expression option
*)
end
(*
val make_element : type_expression -> full_environment -> environment_element_definition -> element
val make_element_binder : type_expression -> full_environment -> element
val make_element_declaration : full_environment -> expression -> element
*)
module PP : sig
open Format
val list_sep_scope : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val full_environment : formatter -> full_environment -> unit
(*
val environment_element : formatter -> ( string * environment_element ) -> unit
val type_environment_element : formatter -> ( string * type_expression ) -> unit
val environment : formatter -> environment -> unit
val type_environment : formatter -> type_environment -> unit
val small_environment : formatter -> small_environment -> unit
*)
end

4
src/stages/4-ast_typed/misc.ml
View File

@ -255,7 +255,7 @@ end
* let empty : bindings = []
* let of_list : string list -> bindings = fun x -> x
*
* let rec expression : bindings -> full_environment -> expression -> bindings = fun b _env e ->
* let rec expression : bindings -> environment -> expression -> bindings = fun b _env e ->
* let self = annotated_expression b in
* match e with
* | E_lambda l ->
@ -519,7 +519,7 @@ let get_entry (lst : program) (name : string) : expression result =
in
List.find_map aux lst
let program_environment (program : program) : full_environment =
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

2
src/stages/4-ast_typed/misc.mli
View File

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

4
src/stages/4-ast_typed/misc_smart.ml
View File

@ -24,7 +24,7 @@ let program_to_main : program -> string -> lambda result = fun p s ->
let aux = fun _ d ->
match d with
| Declaration_constant {binder=_ ; expr= _ ; inline=_ ; post_env } -> post_env in
List.fold_left aux Environment.full_empty (List.map Location.unwrap p) in
List.fold_left aux Environment.empty (List.map Location.unwrap p) in
let binder = Var.of_name "@contract_input" in
let result =
let input_expr = e_a_variable binder input_type env in
@ -47,7 +47,7 @@ module Captured_variables = struct
let rec expression : bindings -> expression -> bindings result = fun b e ->
expression_content b e.environment e.expression_content
and expression_content : bindings -> full_environment -> expression_content -> bindings result = fun b env ec ->
and expression_content : bindings -> environment -> expression_content -> bindings result = fun b env ec ->
let self = expression b in
match ec with
| E_lambda l -> ok @@ Free_variables.lambda empty l

17
src/stages/4-ast_typed/types.ml
View File

@ -269,7 +269,7 @@ and declaration_constant = {
binder : expression_variable ;
expr : expression ;
inline : bool ;
post_env : full_environment ;
post_env : environment ;
}
and declaration =
@ -281,7 +281,7 @@ and declaration =
| Declaration_constant of declaration_constant
(*
| Declaration_type of (type_variable * type_expression)
| Declaration_constant of (named_expression * (full_environment * full_environment))
| Declaration_constant of (named_expression * (environment * environment))
*)
(* | Macro_declaration of macro_declaration *)
@ -289,7 +289,7 @@ and expression = {
expression_content: expression_content ;
location: location ;
type_expression: type_expression ;
environment: full_environment ;
environment: environment ;
}
and map_kv = {
@ -392,11 +392,11 @@ and free_variables = expression_variable list
and environment_element = {
type_value: type_expression ;
source_environment: full_environment ;
source_environment: environment ;
definition: environment_element_definition ;
}
and environment = environment_binding list
and expression_environment = environment_binding list
and environment_binding = {
expr_var: expression_variable ;
@ -410,14 +410,11 @@ and type_environment_binding = {
type_: type_expression ;
}
(* SUBST ??? *)
and small_environment = {
expression_environment: environment ;
and environment = {
expression_environment: expression_environment ;
type_environment: type_environment ;
}
and full_environment = small_environment list_ne
and named_type_content = {
type_name : type_variable;
type_value : type_expression;

20
src/stages/typesystem/misc.ml
View File

@ -21,10 +21,10 @@ module Substitution = struct
let%bind expr = s_expression ~substs expr in
let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
ok @@ T.ED_declaration {expr ; free_variables}
and s_environment : T.environment w = fun ~substs env ->
and s_expr_environment : T.expression_environment w = fun ~substs env ->
bind_map_list (fun T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }} ->
let%bind type_value = s_type_expression ~substs type_value in
let%bind source_environment = s_full_environment ~substs source_environment in
let%bind source_environment = s_environment ~substs source_environment in
let%bind definition = s_environment_element_definition ~substs definition in
ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env
and s_type_environment : T.type_environment w = fun ~substs tenv ->
@ -32,14 +32,14 @@ module Substitution = struct
let%bind type_variable = s_type_variable ~substs type_variable in
let%bind type_ = s_type_expression ~substs type_ in
ok @@ T.{type_variable ; type_}) tenv
and s_small_environment : T.small_environment w = fun ~substs T.{expression_environment ; type_environment} ->
let%bind expression_environment = s_environment ~substs expression_environment in
and s_environment : T.environment w = fun ~substs T.{expression_environment ; type_environment} ->
let%bind expression_environment = s_expr_environment ~substs expression_environment in
let%bind type_environment = s_type_environment ~substs type_environment in
ok @@ T.{ expression_environment ; type_environment }
and s_full_environment : T.full_environment w = fun ~substs (a , b) ->
let%bind a = s_small_environment ~substs a in
let%bind b = bind_map_list (s_small_environment ~substs) b in
ok (a , b)
(* and s_environment : T.environment w = fun ~substs (a , b) ->
let%bind a = s_environment ~substs a in
let%bind b = bind_map_list (s_environment ~substs) b in
ok (a , b) *)
and s_variable : T.expression_variable w = fun ~substs var ->
let () = ignore @@ substs in
@ -198,7 +198,7 @@ module Substitution = struct
and s_expression : T.expression w = fun ~(substs:substs) { expression_content; type_expression; environment; location } ->
let%bind expression_content = s_expression_content ~substs expression_content in
let%bind type_expr = s_type_expression ~substs type_expression in
let%bind environment = s_full_environment ~substs environment in
let%bind environment = s_environment ~substs environment in
let location = location in
ok T.{ expression_content;type_expression=type_expr; environment; location }
@ -207,7 +207,7 @@ module Substitution = struct
Ast_typed.Declaration_constant {binder ; expr ; inline ; post_env} ->
let%bind binder = s_variable ~substs binder in
let%bind expr = s_expression ~substs expr in
let%bind post_env = s_full_environment ~substs post_env in
let%bind post_env = s_environment ~substs post_env in
ok @@ Ast_typed.Declaration_constant {binder; expr; inline; post_env}
and s_declaration_wrap :T.declaration Location.wrap w = fun ~substs d ->

2
src/test/typer_tests.ml
View File

@ -10,7 +10,7 @@ let int () : unit result =
let open Combinators in
let pre = e_int (Z.of_int 32) in
let open Typer in
let e = Environment.full_empty in
let e = Environment.empty in
let state = Typer.Solver.initial_state in
let%bind (post , new_state) = type_expression_subst e state pre in
let () = Typer.Solver.discard_state new_state in