some environment cleanup
This commit is contained in:
parent
e93e3ccbdd
commit
9eeac11628
@ -1425,7 +1425,7 @@ let%expect_test _ =
|
|||||||
let%expect_test _ =
|
let%expect_test _ =
|
||||||
run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ;
|
run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ;
|
||||||
[%expect {|
|
[%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
|
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" ] ;
|
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ;
|
||||||
[%expect {|
|
[%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
|
If you're not sure how to fix this error, you can
|
||||||
|
@ -119,7 +119,7 @@ let%expect_test _ =
|
|||||||
|
|
||||||
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ;
|
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ;
|
||||||
[%expect {|
|
[%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
|
If you're not sure how to fix this error, you can
|
||||||
|
@ -1,11 +1 @@
|
|||||||
open Ast_typed
|
let default = Bool.environment
|
||||||
|
|
||||||
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
|
|
@ -13,7 +13,7 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * As
|
|||||||
| Env -> ok applied in
|
| Env -> ok applied in
|
||||||
ok @@ (applied', state)
|
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 =
|
: (Ast_typed.expression * Ast_typed.typer_state) result =
|
||||||
let%bind (ae_typed,state) = Typer.type_expression_subst env state e in
|
let%bind (ae_typed,state) = Typer.type_expression_subst env state e in
|
||||||
let () = Typer.Solver.discard_state state in
|
let () = Typer.Solver.discard_state state in
|
||||||
|
@ -48,13 +48,13 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
|
|||||||
let%bind b =
|
let%bind b =
|
||||||
trace_strong (wrong_mini_c_value "bool" v) @@
|
trace_strong (wrong_mini_c_value "bool" v) @@
|
||||||
get_bool v in
|
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-> (
|
| t when (compare t (t_bool ()).type_content) = 0-> (
|
||||||
let%bind b =
|
let%bind b =
|
||||||
trace_strong (wrong_mini_c_value "bool" v) @@
|
trace_strong (wrong_mini_c_value "bool" v) @@
|
||||||
get_bool v in
|
get_bool v in
|
||||||
return (e_bool b Environment.full_empty)
|
return (e_bool b Environment.empty)
|
||||||
)
|
)
|
||||||
| T_constant type_constant -> (
|
| T_constant type_constant -> (
|
||||||
match type_constant with
|
match type_constant with
|
||||||
|
@ -10,7 +10,7 @@ let unbound_type_variable (e:environment) (tv:I.type_variable) (loc:Location.t)
|
|||||||
let data = [
|
let data = [
|
||||||
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
|
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
|
||||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
|
("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
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
|
|
||||||
@ -20,7 +20,7 @@ let unbound_variable (e:environment) (n:I.expression_variable) (loc:Location.t)
|
|||||||
let message () = "" in
|
let message () = "" in
|
||||||
let data = [
|
let data = [
|
||||||
("variable" , name) ;
|
("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)
|
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||||
] in
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
@ -60,7 +60,7 @@ let unbound_constructor (e:environment) (c:I.constructor') (loc:Location.t) () =
|
|||||||
let message () = "" in
|
let message () = "" in
|
||||||
let data = [
|
let data = [
|
||||||
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c) ;
|
("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)
|
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||||
] in
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
|
@ -28,7 +28,7 @@ let rec type_declaration env state : I.declaration -> (environment * O.typer_sta
|
|||||||
let%bind (expr , state') =
|
let%bind (expr , state') =
|
||||||
trace (constant_declaration_error binder expression tv'_opt) @@
|
trace (constant_declaration_error binder expression tv'_opt) @@
|
||||||
type_expression env state expression in
|
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} ))
|
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 () =
|
let content () =
|
||||||
Format.asprintf "%a in:\n%a\n"
|
Format.asprintf "%a in:\n%a\n"
|
||||||
Stage_common.PP.constructor constructor
|
Stage_common.PP.constructor constructor
|
||||||
O.Environment.PP.full_environment e
|
O.Environment.PP.environment e
|
||||||
in
|
in
|
||||||
error title content in
|
error title content in
|
||||||
trace_option error @@
|
trace_option error @@
|
||||||
|
@ -40,7 +40,7 @@ module Errors = struct
|
|||||||
let data = [
|
let data = [
|
||||||
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
|
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
|
||||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
|
("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)
|
("did_you_mean" , fun () -> suggestion)
|
||||||
] in
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
@ -51,7 +51,7 @@ module Errors = struct
|
|||||||
let message () = "" in
|
let message () = "" in
|
||||||
let data = [
|
let data = [
|
||||||
("variable" , name) ;
|
("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)
|
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||||
] in
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
@ -91,7 +91,7 @@ module Errors = struct
|
|||||||
let message () = "" in
|
let message () = "" in
|
||||||
let data = [
|
let data = [
|
||||||
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c);
|
("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)
|
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||||
] in
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
@ -101,7 +101,7 @@ module Errors = struct
|
|||||||
let message () = "" in
|
let message () = "" in
|
||||||
let data = [
|
let data = [
|
||||||
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c);
|
("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
|
] in
|
||||||
error ~data title message ()
|
error ~data title message ()
|
||||||
|
|
||||||
@ -514,7 +514,7 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) :
|
|||||||
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_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}))
|
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 () =
|
let content () =
|
||||||
Format.asprintf "%a in:\n%a\n"
|
Format.asprintf "%a in:\n%a\n"
|
||||||
Stage_common.PP.constructor constructor
|
Stage_common.PP.constructor constructor
|
||||||
O.Environment.PP.full_environment e
|
O.Environment.PP.environment e
|
||||||
in
|
in
|
||||||
error title content in
|
error title content in
|
||||||
trace_option error @@
|
trace_option error @@
|
||||||
|
@ -25,7 +25,7 @@ let match_var (t:type_expression) =
|
|||||||
{ expression_content = E_variable (Var.of_name "x") ;
|
{ expression_content = E_variable (Var.of_name "x") ;
|
||||||
location = Location.generated ;
|
location = Location.generated ;
|
||||||
type_expression = t ;
|
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 =
|
let matching (e:expression) matchee cases =
|
||||||
{ expression_content = E_matching {matchee ; cases};
|
{ expression_content = E_matching {matchee ; cases};
|
||||||
|
@ -189,17 +189,15 @@ and free_variables = expression_variable list
|
|||||||
|
|
||||||
and environment_element =
|
and environment_element =
|
||||||
{ type_value: type_expression
|
{ type_value: type_expression
|
||||||
; source_environment: full_environment
|
; source_environment: environment
|
||||||
; definition: environment_element_definition }
|
; 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
|
and type_environment = (type_variable * type_expression) list
|
||||||
|
|
||||||
(* SUBST ??? *)
|
(* SUBST ??? *)
|
||||||
and small_environment = environment * type_environment
|
and environment = expr_environment * type_environment
|
||||||
|
|
||||||
and full_environment = small_environment List.Ne.t
|
|
||||||
|
|
||||||
and expr = expression
|
and expr = expression
|
||||||
|
|
||||||
|
@ -147,17 +147,15 @@ and free_variables = expression_variable list
|
|||||||
|
|
||||||
and environment_element =
|
and environment_element =
|
||||||
{ type_value: type_expression
|
{ type_value: type_expression
|
||||||
; source_environment: full_environment
|
; source_environment: environment
|
||||||
; definition: environment_element_definition }
|
; 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
|
and type_environment = (type_variable * type_expression) list
|
||||||
|
|
||||||
(* SUBST ??? *)
|
(* SUBST ??? *)
|
||||||
and small_environment = environment * type_environment
|
and environment = expr_environment * type_environment
|
||||||
|
|
||||||
and full_environment = small_environment List.Ne.t
|
|
||||||
|
|
||||||
and expr = expression
|
and expr = expression
|
||||||
|
|
||||||
|
@ -92,17 +92,15 @@ and free_variables = expression_variable list
|
|||||||
|
|
||||||
and environment_element =
|
and environment_element =
|
||||||
{ type_value: type_expression
|
{ type_value: type_expression
|
||||||
; source_environment: full_environment
|
; source_environment: environment
|
||||||
; definition: environment_element_definition }
|
; 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
|
and type_environment = (type_variable * type_expression) list
|
||||||
|
|
||||||
(* SUBST ??? *)
|
(* SUBST ??? *)
|
||||||
and small_environment = environment * type_environment
|
and environment = expr_environment * type_environment
|
||||||
|
|
||||||
and full_environment = small_environment List.Ne.t
|
|
||||||
|
|
||||||
and expr = expression
|
and expr = expression
|
||||||
|
|
||||||
|
@ -27,7 +27,6 @@ let needs_parens = {
|
|||||||
label_map = (fun _ _ _ _ -> false) ;
|
label_map = (fun _ _ _ _ -> false) ;
|
||||||
list = (fun _ _ _ _ -> false) ;
|
list = (fun _ _ _ _ -> false) ;
|
||||||
location_wrap = (fun _ _ _ _ -> false) ;
|
location_wrap = (fun _ _ _ _ -> false) ;
|
||||||
list_ne = (fun _ _ _ _ -> false) ;
|
|
||||||
option = (fun _visitor _continue _state o ->
|
option = (fun _visitor _continue _state o ->
|
||||||
match o with None -> false | Some _ -> true) ;
|
match o with None -> false | Some _ -> true) ;
|
||||||
poly_unionfind = (fun _ _ _ _ -> false) ;
|
poly_unionfind = (fun _ _ _ _ -> false) ;
|
||||||
@ -80,10 +79,10 @@ let op ppf = {
|
|||||||
location_wrap = (fun _visitor continue () lwrap ->
|
location_wrap = (fun _visitor continue () lwrap ->
|
||||||
let ({ wrap_content; location } : _ Location.wrap) = lwrap in
|
let ({ wrap_content; location } : _ Location.wrap) = lwrap in
|
||||||
fprintf ppf "{ wrap_content = %a ; location = %a }" (fun _ppf -> continue ()) wrap_content Location.pp location);
|
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 =
|
let aux ppf elt =
|
||||||
fprintf ppf "%a" (fun _ppf -> continue ()) elt in
|
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 ->
|
option = (fun _visitor continue () o ->
|
||||||
match o with
|
match o with
|
||||||
| None -> fprintf ppf "None"
|
| None -> fprintf ppf "None"
|
||||||
|
@ -3,7 +3,7 @@ open Types
|
|||||||
|
|
||||||
val make_n_t : type_variable -> type_expression -> named_type_content
|
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_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_bool : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
|
||||||
val t_string : ?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 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_expression : expression -> type_expression
|
||||||
val get_type' : type_expression -> type_content
|
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_expression : expression -> expression_content
|
||||||
val get_lambda : expression -> lambda result
|
val get_lambda : expression -> lambda result
|
||||||
val get_lambda_with_type : expression -> (lambda * ( type_expression * type_expression) ) 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_int : Z.t -> expression_content
|
||||||
val e_nat : Z.t -> expression_content
|
val e_nat : Z.t -> expression_content
|
||||||
val e_mutez : 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_string : string -> expression_content
|
||||||
val e_bytes : bytes -> expression_content
|
val e_bytes : bytes -> expression_content
|
||||||
val e_timestamp : Z.t -> 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_variable : expression_variable -> expression_content
|
||||||
val e_let_in : expression_variable -> inline -> expression -> expression -> expression_content
|
val e_let_in : expression_variable -> inline -> expression -> expression -> expression_content
|
||||||
|
|
||||||
val e_a_unit : full_environment -> expression
|
val e_a_unit : environment -> expression
|
||||||
val e_a_int : Z.t -> full_environment -> expression
|
val e_a_int : Z.t -> environment -> expression
|
||||||
val e_a_nat : Z.t -> full_environment -> expression
|
val e_a_nat : Z.t -> environment -> expression
|
||||||
val e_a_mutez : Z.t -> full_environment -> expression
|
val e_a_mutez : Z.t -> environment -> expression
|
||||||
val e_a_bool : bool -> full_environment -> expression
|
val e_a_bool : bool -> environment -> expression
|
||||||
val e_a_string : string -> full_environment -> expression
|
val e_a_string : string -> environment -> expression
|
||||||
val e_a_address : string -> full_environment -> expression
|
val e_a_address : string -> environment -> expression
|
||||||
val e_a_pair : expression -> expression -> full_environment -> expression
|
val e_a_pair : expression -> expression -> environment -> expression
|
||||||
val e_a_some : expression -> full_environment -> expression
|
val e_a_some : expression -> environment -> expression
|
||||||
val e_a_lambda : lambda -> type_expression -> type_expression -> full_environment -> expression
|
val e_a_lambda : lambda -> type_expression -> type_expression -> environment -> expression
|
||||||
val e_a_none : type_expression -> full_environment -> expression
|
val e_a_none : type_expression -> environment -> expression
|
||||||
val e_a_record : expression label_map -> full_environment -> expression
|
val e_a_record : expression label_map -> environment -> expression
|
||||||
val e_a_application : expression -> expression -> full_environment -> expression
|
val e_a_application : expression -> expression -> environment -> expression
|
||||||
val e_a_variable : expression_variable -> type_expression -> full_environment -> expression
|
val e_a_variable : expression_variable -> type_expression -> environment -> expression
|
||||||
val ez_e_a_record : ( label * expression ) list -> full_environment -> expression
|
val ez_e_a_record : ( label * expression ) list -> environment -> expression
|
||||||
val e_a_let_in : expression_variable -> bool -> expression -> expression -> full_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_int : expression -> Z.t result
|
||||||
val get_a_unit : expression -> unit result
|
val get_a_unit : expression -> unit result
|
||||||
|
@ -1,25 +1,25 @@
|
|||||||
open Types
|
open Types
|
||||||
open Combinators
|
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_unit = e_a_unit Environment.empty
|
||||||
let e_a_empty_int n = e_a_int n Environment.full_empty
|
let e_a_empty_int n = e_a_int n Environment.empty
|
||||||
let e_a_empty_nat n = e_a_nat n Environment.full_empty
|
let e_a_empty_nat n = e_a_nat n Environment.empty
|
||||||
let e_a_empty_mutez n = e_a_mutez n Environment.full_empty
|
let e_a_empty_mutez n = e_a_mutez n Environment.empty
|
||||||
let e_a_empty_bool b = e_a_bool b Environment.full_empty
|
let e_a_empty_bool b = e_a_bool b Environment.empty
|
||||||
let e_a_empty_string s = e_a_string s Environment.full_empty
|
let e_a_empty_string s = e_a_string s Environment.empty
|
||||||
let e_a_empty_address s = e_a_address s Environment.full_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.full_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.full_empty
|
let e_a_empty_some s = e_a_some s Environment.empty
|
||||||
let e_a_empty_none t = e_a_none t Environment.full_empty
|
let e_a_empty_none t = e_a_none t Environment.empty
|
||||||
let e_a_empty_record r = e_a_record r Environment.full_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.full_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.full_empty
|
let e_a_empty_lambda l i o = e_a_lambda l i o Environment.empty
|
||||||
|
|
||||||
open Environment
|
open Environment
|
||||||
|
|
||||||
let env_sum_type ?(env = full_empty)
|
let env_sum_type ?(env = empty)
|
||||||
?(type_name = Var.of_name "a_sum_type")
|
?(type_name = Var.of_name "a_sum_type")
|
||||||
(lst : (constructor' * ctor_content) list) =
|
(lst : (constructor' * ctor_content) list) =
|
||||||
add_type type_name (make_t_ez_sum lst) env
|
add_type type_name (make_t_ez_sum lst) env
|
||||||
|
@ -16,4 +16,4 @@ val e_a_empty_record : expression label_map -> expression
|
|||||||
val ez_e_a_empty_record : ( label * expression ) list -> expression
|
val ez_e_a_empty_record : ( label * expression ) list -> expression
|
||||||
val e_a_empty_lambda : lambda -> type_expression -> type_expression -> 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
|
||||||
|
@ -1,52 +1,46 @@
|
|||||||
open Types
|
open Types
|
||||||
open Combinators
|
open Combinators
|
||||||
|
|
||||||
|
type t = environment
|
||||||
type element = environment_element
|
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}
|
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_binder = fun t s -> make_element t s ED_binder
|
||||||
|
|
||||||
let make_element_declaration = fun s (expr : expression) ->
|
let make_element_declaration = fun s (expr : expression) ->
|
||||||
let free_variables = Misc.Free_variables.(expression empty expr) in
|
let free_variables = Misc.Free_variables.(expression empty expr) in
|
||||||
make_element (get_type_expression expr) s (ED_declaration {expr ; free_variables})
|
make_element (get_type_expression expr) s (ED_declaration {expr ; free_variables})
|
||||||
|
|
||||||
module Small = struct
|
let empty : t = { expression_environment = [] ; type_environment = [] }
|
||||||
type t = small_environment
|
|
||||||
|
|
||||||
let empty : t = { expression_environment = [] ; type_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_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 }
|
||||||
|
|
||||||
(* TODO: generate *)
|
let add_expr : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_expr_environment (fun x -> {expr_var ; env_elt} :: x)
|
||||||
let get_environment : t -> environment = fun { expression_environment ; type_environment=_ } -> expression_environment
|
let add_type : type_variable -> type_expression -> t -> t = fun type_variable type_ -> map_type_environment (fun x -> { type_variable ; type_ } :: x)
|
||||||
(* TODO: generate *)
|
(* TODO: generate : these are now messy, clean them up. *)
|
||||||
let get_type_environment : t -> type_environment = fun { expression_environment=_ ; type_environment } -> type_environment
|
let get_opt : expression_variable -> t -> element option = fun k x ->
|
||||||
(* TODO: generate *)
|
Option.bind (fun {expr_var=_ ; env_elt} -> Some env_elt) @@
|
||||||
let map_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment = f expression_environment ; type_environment }
|
List.find_opt (fun {expr_var ; env_elt=_} -> Var.equal expr_var k) (get_expr_environment x)
|
||||||
let map_type_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment ; type_environment = f type_environment }
|
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)
|
||||||
|
|
||||||
let add : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_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
|
|
||||||
|
|
||||||
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 ->
|
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 ->
|
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
|
add_expr 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
|
|
||||||
|
|
||||||
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 *)
|
||||||
let aux = fun x ->
|
|
||||||
let aux = fun {type_variable=_ ; type_} ->
|
let aux = fun {type_variable=_ ; type_} ->
|
||||||
match type_.type_content with
|
match type_.type_content with
|
||||||
| T_sum m ->
|
| T_sum m ->
|
||||||
@ -55,8 +49,7 @@ let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expr
|
|||||||
| None -> None)
|
| None -> None)
|
||||||
| _ -> None
|
| _ -> None
|
||||||
in
|
in
|
||||||
List.find_map aux (Small.get_type_environment x) in
|
List.find_map aux (get_type_environment x)
|
||||||
List.Ne.find_map aux x
|
|
||||||
|
|
||||||
|
|
||||||
module PP = struct
|
module PP = struct
|
||||||
@ -72,27 +65,15 @@ module PP = struct
|
|||||||
let type_environment_element = fun ppf {type_variable ; type_} ->
|
let type_environment_element = fun ppf {type_variable ; type_} ->
|
||||||
fprintf ppf "%a -> %a" PP.type_variable type_variable PP.type_expression type_
|
fprintf ppf "%a -> %a" PP.type_variable type_variable PP.type_expression type_
|
||||||
|
|
||||||
let environment : _ -> environment -> unit = fun ppf lst ->
|
let expr_environment : _ -> expression_environment -> unit = fun ppf lst ->
|
||||||
fprintf ppf "E[%a]" (list_sep environment_element (const " , ")) lst
|
fprintf ppf "E[%a]" (list_sep environment_element (tag "@,")) lst
|
||||||
|
|
||||||
let type_environment = fun ppf 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"
|
fprintf ppf "- %a\t%a"
|
||||||
environment (Small.get_environment e)
|
expr_environment (get_expr_environment e)
|
||||||
type_environment (Small.get_type_environment e)
|
type_environment (get_type_environment e)
|
||||||
|
|
||||||
let full_environment : _ -> full_environment -> unit = fun ppf e ->
|
end
|
||||||
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
|
|
@ -1,62 +1,20 @@
|
|||||||
open Types
|
open Types
|
||||||
open Trace
|
|
||||||
|
|
||||||
type t = full_environment
|
type t = environment
|
||||||
type element = environment_element
|
type element = environment_element
|
||||||
|
|
||||||
val get_trace : expression_variable -> t -> element result
|
val empty : t
|
||||||
val empty : environment
|
|
||||||
val full_empty : t
|
|
||||||
val add : expression_variable -> element -> t -> t
|
|
||||||
val add_ez_binder : expression_variable -> type_expression -> t -> t
|
val add_ez_binder : expression_variable -> type_expression -> t -> t
|
||||||
val add_ez_declaration : expression_variable -> 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 add_type : type_variable -> type_expression -> t -> t
|
||||||
val get_opt : expression_variable -> t -> element option
|
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
|
||||||
|
|
||||||
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
|
module PP : sig
|
||||||
open Format
|
open Format
|
||||||
|
|
||||||
val list_sep_scope : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
|
val list_sep_scope : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
|
||||||
val full_environment : formatter -> full_environment -> unit
|
val environment : formatter -> 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
|
end
|
||||||
|
@ -255,7 +255,7 @@ end
|
|||||||
* let empty : bindings = []
|
* let empty : bindings = []
|
||||||
* let of_list : string list -> bindings = fun x -> x
|
* 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
|
* let self = annotated_expression b in
|
||||||
* match e with
|
* match e with
|
||||||
* | E_lambda l ->
|
* | E_lambda l ->
|
||||||
@ -519,7 +519,7 @@ 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) : full_environment =
|
let program_environment (program : program) : environment =
|
||||||
let last_declaration = Location.unwrap List.(hd @@ rev program) in
|
let last_declaration = Location.unwrap List.(hd @@ rev program) in
|
||||||
match last_declaration with
|
match last_declaration with
|
||||||
| Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env
|
| Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env
|
||||||
|
@ -70,7 +70,7 @@ 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 -> full_environment
|
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
|
||||||
|
@ -24,7 +24,7 @@ let program_to_main : program -> string -> lambda result = fun p s ->
|
|||||||
let aux = fun _ d ->
|
let aux = fun _ d ->
|
||||||
match d with
|
match d with
|
||||||
| Declaration_constant {binder=_ ; expr= _ ; inline=_ ; post_env } -> post_env in
|
| 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 binder = Var.of_name "@contract_input" in
|
||||||
let result =
|
let result =
|
||||||
let input_expr = e_a_variable binder input_type env in
|
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 ->
|
let rec expression : bindings -> expression -> bindings result = fun b e ->
|
||||||
expression_content b e.environment e.expression_content
|
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
|
let self = expression b in
|
||||||
match ec with
|
match ec with
|
||||||
| E_lambda l -> ok @@ Free_variables.lambda empty l
|
| E_lambda l -> ok @@ Free_variables.lambda empty l
|
||||||
|
@ -269,7 +269,7 @@ and declaration_constant = {
|
|||||||
binder : expression_variable ;
|
binder : expression_variable ;
|
||||||
expr : expression ;
|
expr : expression ;
|
||||||
inline : bool ;
|
inline : bool ;
|
||||||
post_env : full_environment ;
|
post_env : environment ;
|
||||||
}
|
}
|
||||||
|
|
||||||
and declaration =
|
and declaration =
|
||||||
@ -281,7 +281,7 @@ and declaration =
|
|||||||
| Declaration_constant of declaration_constant
|
| Declaration_constant of declaration_constant
|
||||||
(*
|
(*
|
||||||
| Declaration_type of (type_variable * type_expression)
|
| 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 *)
|
(* | Macro_declaration of macro_declaration *)
|
||||||
|
|
||||||
@ -289,7 +289,7 @@ and expression = {
|
|||||||
expression_content: expression_content ;
|
expression_content: expression_content ;
|
||||||
location: location ;
|
location: location ;
|
||||||
type_expression: type_expression ;
|
type_expression: type_expression ;
|
||||||
environment: full_environment ;
|
environment: environment ;
|
||||||
}
|
}
|
||||||
|
|
||||||
and map_kv = {
|
and map_kv = {
|
||||||
@ -392,11 +392,11 @@ and free_variables = expression_variable list
|
|||||||
|
|
||||||
and environment_element = {
|
and environment_element = {
|
||||||
type_value: type_expression ;
|
type_value: type_expression ;
|
||||||
source_environment: full_environment ;
|
source_environment: environment ;
|
||||||
definition: environment_element_definition ;
|
definition: environment_element_definition ;
|
||||||
}
|
}
|
||||||
|
|
||||||
and environment = environment_binding list
|
and expression_environment = environment_binding list
|
||||||
|
|
||||||
and environment_binding = {
|
and environment_binding = {
|
||||||
expr_var: expression_variable ;
|
expr_var: expression_variable ;
|
||||||
@ -410,14 +410,11 @@ and type_environment_binding = {
|
|||||||
type_: type_expression ;
|
type_: type_expression ;
|
||||||
}
|
}
|
||||||
|
|
||||||
(* SUBST ??? *)
|
and environment = {
|
||||||
and small_environment = {
|
expression_environment: expression_environment ;
|
||||||
expression_environment: environment ;
|
|
||||||
type_environment: type_environment ;
|
type_environment: type_environment ;
|
||||||
}
|
}
|
||||||
|
|
||||||
and full_environment = small_environment list_ne
|
|
||||||
|
|
||||||
and named_type_content = {
|
and named_type_content = {
|
||||||
type_name : type_variable;
|
type_name : type_variable;
|
||||||
type_value : type_expression;
|
type_value : type_expression;
|
||||||
|
@ -21,10 +21,10 @@ module Substitution = struct
|
|||||||
let%bind expr = s_expression ~substs expr in
|
let%bind expr = s_expression ~substs expr in
|
||||||
let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
|
let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
|
||||||
ok @@ T.ED_declaration {expr ; free_variables}
|
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 }} ->
|
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 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
|
let%bind definition = s_environment_element_definition ~substs definition in
|
||||||
ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env
|
ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env
|
||||||
and s_type_environment : T.type_environment w = fun ~substs tenv ->
|
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_variable = s_type_variable ~substs type_variable in
|
||||||
let%bind type_ = s_type_expression ~substs type_ in
|
let%bind type_ = s_type_expression ~substs type_ in
|
||||||
ok @@ T.{type_variable ; type_}) tenv
|
ok @@ T.{type_variable ; type_}) tenv
|
||||||
and s_small_environment : T.small_environment w = fun ~substs T.{expression_environment ; type_environment} ->
|
and s_environment : T.environment w = fun ~substs T.{expression_environment ; type_environment} ->
|
||||||
let%bind expression_environment = s_environment ~substs expression_environment in
|
let%bind expression_environment = s_expr_environment ~substs expression_environment in
|
||||||
let%bind type_environment = s_type_environment ~substs type_environment in
|
let%bind type_environment = s_type_environment ~substs type_environment in
|
||||||
ok @@ T.{ expression_environment ; type_environment }
|
ok @@ T.{ expression_environment ; type_environment }
|
||||||
and s_full_environment : T.full_environment w = fun ~substs (a , b) ->
|
(* and s_environment : T.environment w = fun ~substs (a , b) ->
|
||||||
let%bind a = s_small_environment ~substs a in
|
let%bind a = s_environment ~substs a in
|
||||||
let%bind b = bind_map_list (s_small_environment ~substs) b in
|
let%bind b = bind_map_list (s_environment ~substs) b in
|
||||||
ok (a , b)
|
ok (a , b) *)
|
||||||
|
|
||||||
and s_variable : T.expression_variable w = fun ~substs var ->
|
and s_variable : T.expression_variable w = fun ~substs var ->
|
||||||
let () = ignore @@ substs in
|
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 } ->
|
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 expression_content = s_expression_content ~substs expression_content in
|
||||||
let%bind type_expr = s_type_expression ~substs type_expression 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
|
let location = location in
|
||||||
ok T.{ expression_content;type_expression=type_expr; environment; location }
|
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} ->
|
Ast_typed.Declaration_constant {binder ; expr ; inline ; post_env} ->
|
||||||
let%bind binder = s_variable ~substs binder in
|
let%bind binder = s_variable ~substs binder in
|
||||||
let%bind expr = s_expression ~substs expr 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}
|
ok @@ Ast_typed.Declaration_constant {binder; expr; inline; post_env}
|
||||||
|
|
||||||
and s_declaration_wrap :T.declaration Location.wrap w = fun ~substs d ->
|
and s_declaration_wrap :T.declaration Location.wrap w = fun ~substs d ->
|
||||||
|
@ -10,7 +10,7 @@ let int () : unit result =
|
|||||||
let open Combinators in
|
let open Combinators in
|
||||||
let pre = e_int (Z.of_int 32) in
|
let pre = e_int (Z.of_int 32) in
|
||||||
let open Typer in
|
let open Typer in
|
||||||
let e = Environment.full_empty in
|
let e = Environment.empty in
|
||||||
let state = Typer.Solver.initial_state in
|
let state = Typer.Solver.initial_state in
|
||||||
let%bind (post , new_state) = type_expression_subst e state pre in
|
let%bind (post , new_state) = type_expression_subst e state pre in
|
||||||
let () = Typer.Solver.discard_state new_state in
|
let () = Typer.Solver.discard_state new_state in
|
||||||
|
Loading…
Reference in New Issue
Block a user