add deep closures
This commit is contained in:
parent
2dc6b4a263
commit
76163aa855
@ -86,10 +86,18 @@ module Append = struct
|
|||||||
| Leaf x -> leaf x
|
| Leaf x -> leaf x
|
||||||
| Node {a;b} -> node (fold' leaf node a) (fold' leaf node b)
|
| Node {a;b} -> node (fold' leaf node a) (fold' leaf node b)
|
||||||
|
|
||||||
|
let rec fold_s' : type a b . a -> (a -> b -> a) -> b t' -> a = fun init leaf -> function
|
||||||
|
| Leaf x -> leaf init x
|
||||||
|
| Node {a;b} -> fold_s' (fold_s' init leaf a) leaf b
|
||||||
|
|
||||||
let fold_ne leaf node = function
|
let fold_ne leaf node = function
|
||||||
| Empty -> raise (Failure "Tree.Append.fold_ne")
|
| Empty -> raise (Failure "Tree.Append.fold_ne")
|
||||||
| Full x -> fold' leaf node x
|
| Full x -> fold' leaf node x
|
||||||
|
|
||||||
|
let fold_s_ne : type a b . a -> (a -> b -> a) -> b t -> a = fun init leaf -> function
|
||||||
|
| Empty -> raise (Failure "Tree.Append.fold_s_ne")
|
||||||
|
| Full x -> fold_s' init leaf x
|
||||||
|
|
||||||
let fold empty leaf node = function
|
let fold empty leaf node = function
|
||||||
| Empty -> empty
|
| Empty -> empty
|
||||||
| Full x -> fold' leaf node x
|
| Full x -> fold' leaf node x
|
||||||
|
@ -1,8 +1,12 @@
|
|||||||
include Types
|
|
||||||
include Misc
|
|
||||||
|
|
||||||
module Types = Types
|
module Types = Types
|
||||||
module Environment = Environment
|
module Environment = Environment
|
||||||
module PP = PP
|
module PP = PP
|
||||||
module Combinators = Combinators
|
module Combinators = struct
|
||||||
|
include Combinators
|
||||||
|
include Combinators_environment
|
||||||
|
end
|
||||||
module Misc = Misc
|
module Misc = Misc
|
||||||
|
|
||||||
|
include Types
|
||||||
|
include Misc
|
||||||
|
include Combinators
|
||||||
|
@ -3,7 +3,6 @@ open Types
|
|||||||
|
|
||||||
let make_t type_value' simplified = { type_value' ; simplified }
|
let make_t type_value' simplified = { type_value' ; simplified }
|
||||||
let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment }
|
let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment }
|
||||||
let make_a_e_empty expression type_annotation = make_a_e expression type_annotation Environment.full_empty
|
|
||||||
let make_n_e name a_e = { name ; annotated_expression = a_e }
|
let make_n_e name a_e = { name ; annotated_expression = a_e }
|
||||||
|
|
||||||
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
|
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
|
||||||
@ -43,6 +42,8 @@ let t_function param result ?s () : type_value = make_t (T_function (param, resu
|
|||||||
let t_shallow_closure param result ?s () : type_value = make_t (T_function (param, result)) s
|
let t_shallow_closure param result ?s () : type_value = make_t (T_function (param, result)) s
|
||||||
|
|
||||||
let get_type_annotation (x:annotated_expression) = x.type_annotation
|
let get_type_annotation (x:annotated_expression) = x.type_annotation
|
||||||
|
let get_environment (x:annotated_expression) = x.environment
|
||||||
|
let get_expression (x:annotated_expression) = x.expression
|
||||||
|
|
||||||
let get_t_bool (t:type_value) : unit result = match t.type_value' with
|
let get_t_bool (t:type_value) : unit result = match t.type_value' with
|
||||||
| T_constant ("bool", []) -> ok ()
|
| T_constant ("bool", []) -> ok ()
|
||||||
@ -161,20 +162,6 @@ let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y
|
|||||||
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
|
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
|
||||||
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
|
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
|
||||||
|
|
||||||
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_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_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_tuple lst = e_a_tuple lst Environment.full_empty
|
|
||||||
let e_a_empty_record r = e_a_record r Environment.full_empty
|
|
||||||
let e_a_empty_map lst k v = e_a_map lst k v Environment.full_empty
|
|
||||||
let e_a_empty_list lst t = e_a_list lst t Environment.full_empty
|
|
||||||
let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty
|
|
||||||
|
|
||||||
let get_a_int (t:annotated_expression) =
|
let get_a_int (t:annotated_expression) =
|
||||||
match t.expression with
|
match t.expression with
|
||||||
| E_literal (Literal_int n) -> ok n
|
| E_literal (Literal_int n) -> ok n
|
||||||
@ -204,9 +191,3 @@ let get_declaration_by_name : program -> string -> declaration result = fun p na
|
|||||||
trace_option (simple_error "no declaration with given name") @@
|
trace_option (simple_error "no declaration with given name") @@
|
||||||
List.find_opt aux @@ List.map Location.unwrap p
|
List.find_opt aux @@ List.map Location.unwrap p
|
||||||
|
|
||||||
open Environment
|
|
||||||
let env_sum_type ?(env = full_empty)
|
|
||||||
?(name = "a_sum_type")
|
|
||||||
(lst : (string * type_value) list) =
|
|
||||||
add_type name (make_t_ez_sum lst) env
|
|
||||||
|
|
||||||
|
25
src/ligo/ast_typed/combinators_environment.ml
Normal file
25
src/ligo/ast_typed/combinators_environment.ml
Normal file
@ -0,0 +1,25 @@
|
|||||||
|
open Types
|
||||||
|
open Combinators
|
||||||
|
|
||||||
|
let make_a_e_empty expression type_annotation = make_a_e expression type_annotation Environment.full_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_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_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_tuple lst = e_a_tuple lst Environment.full_empty
|
||||||
|
let e_a_empty_record r = e_a_record r Environment.full_empty
|
||||||
|
let e_a_empty_map lst k v = e_a_map lst k v Environment.full_empty
|
||||||
|
let e_a_empty_list lst t = e_a_list lst t Environment.full_empty
|
||||||
|
let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty
|
||||||
|
|
||||||
|
open Environment
|
||||||
|
|
||||||
|
let env_sum_type ?(env = full_empty)
|
||||||
|
?(name = "a_sum_type")
|
||||||
|
(lst : (string * type_value) list) =
|
||||||
|
add_type name (make_t_ez_sum lst) env
|
@ -1,15 +1,18 @@
|
|||||||
open Types
|
open Types
|
||||||
|
open Combinators
|
||||||
|
|
||||||
type element = environment_element
|
type element = environment_element
|
||||||
let make_element : type_value -> full_environment -> element =
|
let make_element : type_value -> full_environment -> environment_element_definition -> element =
|
||||||
fun type_value source_environment -> {type_value ; source_environment}
|
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 t s d -> make_element t s (ED_declaration d)
|
||||||
|
|
||||||
module Small = struct
|
module Small = struct
|
||||||
type t = small_environment
|
type t = small_environment
|
||||||
|
|
||||||
let empty : t = ([] , [])
|
let empty : t = ([] , [])
|
||||||
|
|
||||||
|
|
||||||
let get_environment : t -> environment = fst
|
let get_environment : t -> environment = fst
|
||||||
let get_type_environment : t -> type_environment = snd
|
let get_type_environment : t -> type_environment = snd
|
||||||
let map_environment : _ -> t -> t = fun f (a , b) -> (f a , b)
|
let map_environment : _ -> t -> t = fun f (a , b) -> (f a , b)
|
||||||
@ -25,7 +28,12 @@ type t = full_environment
|
|||||||
let empty : environment = Small.(get_environment empty)
|
let empty : environment = Small.(get_environment empty)
|
||||||
let full_empty : t = List.Ne.singleton Small.empty
|
let full_empty : t = List.Ne.singleton Small.empty
|
||||||
let add : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v)
|
let add : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v)
|
||||||
let add_ez : string -> type_value -> t -> t = fun k v e -> List.Ne.hd_map (Small.add k (make_element v e)) e
|
let add_ez_binder : string -> type_value -> t -> t = fun k v e ->
|
||||||
|
List.Ne.hd_map (Small.add k (make_element_binder v e)) e
|
||||||
|
let add_ez_declaration : string -> type_value -> expression -> t -> t = fun k v expr e ->
|
||||||
|
List.Ne.hd_map (Small.add k (make_element_declaration v e expr)) e
|
||||||
|
let add_ez_ae : string -> annotated_expression -> t -> t = fun k ae e ->
|
||||||
|
add_ez_declaration k (get_type_annotation ae) (get_expression ae) e
|
||||||
let add_type : string -> type_value -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v)
|
let add_type : string -> type_value -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v)
|
||||||
let get_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x
|
let get_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x
|
||||||
let get_type_opt : string -> t -> type_value option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x
|
let get_type_opt : string -> t -> type_value option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x
|
||||||
|
@ -40,10 +40,7 @@ module Free_variables = struct
|
|||||||
let rec expression : bindings -> expression -> bindings = fun b e ->
|
let rec expression : bindings -> expression -> bindings = fun b 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 -> lambda b l
|
||||||
let b' = union (singleton l.binder) b in
|
|
||||||
let (b'', frees) = block' b' l.body in
|
|
||||||
union (annotated_expression b'' l.result) frees
|
|
||||||
| E_literal _ -> empty
|
| E_literal _ -> empty
|
||||||
| E_constant (_ , lst) -> unions @@ List.map self lst
|
| E_constant (_ , lst) -> unions @@ List.map self lst
|
||||||
| E_variable name -> (
|
| E_variable name -> (
|
||||||
@ -63,6 +60,11 @@ module Free_variables = struct
|
|||||||
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
|
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
|
||||||
| E_failwith a -> self a
|
| E_failwith a -> self a
|
||||||
|
|
||||||
|
and lambda : bindings -> lambda -> bindings = fun b l ->
|
||||||
|
let b' = union (singleton l.binder) b in
|
||||||
|
let (b'', frees) = block' b' l.body in
|
||||||
|
union (annotated_expression b'' l.result) frees
|
||||||
|
|
||||||
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
|
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
|
||||||
expression b ae.expression
|
expression b ae.expression
|
||||||
|
|
||||||
@ -103,6 +105,84 @@ module Free_variables = struct
|
|||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
(* module Dependencies = struct
|
||||||
|
*
|
||||||
|
* type bindings = string list
|
||||||
|
* let mem : string -> bindings -> bool = List.mem
|
||||||
|
* let singleton : string -> bindings = fun s -> [ s ]
|
||||||
|
* let union : bindings -> bindings -> bindings = (@)
|
||||||
|
* let unions : bindings list -> bindings = List.concat
|
||||||
|
* 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 self = annotated_expression b in
|
||||||
|
* match e with
|
||||||
|
* | E_lambda l ->
|
||||||
|
* let b' = union (singleton l.binder) b in
|
||||||
|
* let (b'', frees) = block' b' l.body in
|
||||||
|
* union (annotated_expression b'' l.result) frees
|
||||||
|
* | E_literal _ -> empty
|
||||||
|
* | E_constant (_ , lst) -> unions @@ List.map self lst
|
||||||
|
* | E_variable name -> (
|
||||||
|
* match mem name b with
|
||||||
|
* | true -> empty
|
||||||
|
* | false -> singleton name
|
||||||
|
* )
|
||||||
|
* | E_application (a, b) -> unions @@ List.map self [ a ; b ]
|
||||||
|
* | E_tuple lst -> unions @@ List.map self lst
|
||||||
|
* | E_constructor (_ , a) -> self a
|
||||||
|
* | E_record m -> unions @@ List.map self @@ Map.String.to_list m
|
||||||
|
* | E_record_accessor (a, _) -> self a
|
||||||
|
* | E_tuple_accessor (a, _) -> self a
|
||||||
|
* | E_list lst -> unions @@ List.map self lst
|
||||||
|
* | E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
|
||||||
|
* | E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
|
||||||
|
* | E_matching (a , cs) -> union (self a) (matching_expression b cs)
|
||||||
|
* | E_failwith a -> self a
|
||||||
|
*
|
||||||
|
* and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
|
||||||
|
* let open Combinators in
|
||||||
|
* expression b (get_environment ae) (get_expression ae)
|
||||||
|
*
|
||||||
|
* and instruction' : bindings -> instruction -> bindings * bindings = fun b i ->
|
||||||
|
* match i with
|
||||||
|
* | I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression)
|
||||||
|
* | I_assignment n -> b , (annotated_expression b n.annotated_expression)
|
||||||
|
* | I_skip -> b , empty
|
||||||
|
* | I_do e -> b , annotated_expression b e
|
||||||
|
* | I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl)
|
||||||
|
* | I_patch (_ , _ , a) -> b , annotated_expression b a
|
||||||
|
* | I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs)
|
||||||
|
*
|
||||||
|
* and block' : bindings -> block -> (bindings * bindings) = fun b bl ->
|
||||||
|
* let aux = fun (binds, frees) cur ->
|
||||||
|
* let (binds', frees') = instruction' binds cur in
|
||||||
|
* (binds', union frees frees') in
|
||||||
|
* List.fold_left aux (b , []) bl
|
||||||
|
*
|
||||||
|
* and block : bindings -> block -> bindings = fun b bl ->
|
||||||
|
* let (_ , frees) = block' b bl in
|
||||||
|
* frees
|
||||||
|
*
|
||||||
|
* and matching_variant_case : type a . (bindings -> a -> bindings) -> bindings -> ((constructor_name * name) * a) -> bindings = fun f b ((_,n),c) ->
|
||||||
|
* f (union (singleton n) b) c
|
||||||
|
*
|
||||||
|
* and matching : type a . (bindings -> a -> bindings) -> bindings -> a matching -> bindings = fun f b m ->
|
||||||
|
* match m with
|
||||||
|
* | Match_bool { match_true = t ; match_false = fa } -> union (f b t) (f b fa)
|
||||||
|
* | Match_list { match_nil = n ; match_cons = (hd, tl, c) } -> union (f b n) (f (union (of_list [hd ; tl]) b) c)
|
||||||
|
* | Match_option { match_none = n ; match_some = ((opt, _), s) } -> union (f b n) (f (union (singleton opt) b) s)
|
||||||
|
* | Match_tuple (lst , a) -> f (union (of_list lst) b) a
|
||||||
|
* | Match_variant (lst , _) -> unions @@ List.map (matching_variant_case f b) lst
|
||||||
|
*
|
||||||
|
* and matching_expression = fun x -> matching annotated_expression x
|
||||||
|
*
|
||||||
|
* and matching_block = fun x -> matching block x
|
||||||
|
*
|
||||||
|
* end *)
|
||||||
|
|
||||||
|
|
||||||
open Errors
|
open Errors
|
||||||
|
|
||||||
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
|
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
|
||||||
|
@ -17,9 +17,14 @@ and declaration =
|
|||||||
| Declaration_constant of (named_expression * full_environment)
|
| Declaration_constant of (named_expression * full_environment)
|
||||||
(* | Macro_declaration of macro_declaration *)
|
(* | Macro_declaration of macro_declaration *)
|
||||||
|
|
||||||
|
and environment_element_definition =
|
||||||
|
| ED_binder
|
||||||
|
| ED_declaration of expression
|
||||||
|
|
||||||
and environment_element = {
|
and environment_element = {
|
||||||
type_value : type_value ;
|
type_value : type_value ;
|
||||||
source_environment : full_environment ;
|
source_environment : full_environment ;
|
||||||
|
definition : environment_element_definition ;
|
||||||
}
|
}
|
||||||
and environment = (string * environment_element) list
|
and environment = (string * environment_element) list
|
||||||
and type_environment = (string * type_value) list
|
and type_environment = (string * type_value) list
|
||||||
|
@ -151,7 +151,31 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
|
|||||||
]
|
]
|
||||||
)
|
)
|
||||||
| T_deep_closure (_small_env, _, _) -> (
|
| T_deep_closure (_small_env, _, _) -> (
|
||||||
simple_fail "no compilation for deep closures app yet" ;
|
trace (simple_error "Compiling deep closure application") @@
|
||||||
|
let%bind f' = translate_expression ~first f in
|
||||||
|
let%bind arg' = translate_expression arg in
|
||||||
|
let error =
|
||||||
|
let error_title () = "michelson type-checking closure application" in
|
||||||
|
let error_content () =
|
||||||
|
Format.asprintf "Env : %a\nclosure : %a\narg : %a\n"
|
||||||
|
PP.environment env
|
||||||
|
PP.expression_with_type f
|
||||||
|
PP.expression_with_type arg
|
||||||
|
in
|
||||||
|
error error_title error_content
|
||||||
|
in
|
||||||
|
trace error @@
|
||||||
|
return @@ virtual_push @@ seq [
|
||||||
|
i_comment "(* unit :: env *)" ;
|
||||||
|
i_comment "compute arg" ;
|
||||||
|
arg' ; i_unpair ;
|
||||||
|
i_comment "(* (arg * unit) :: env *)" ;
|
||||||
|
i_comment "compute closure" ;
|
||||||
|
dip @@ seq [f' ; i_unpair ; i_unpair] ;
|
||||||
|
i_comment "(* arg :: capture :: f :: unit :: env *)" ;
|
||||||
|
i_pair ;
|
||||||
|
i_exec ; (* output :: stack :: env *)
|
||||||
|
]
|
||||||
)
|
)
|
||||||
| T_shallow_closure (_, _, _) -> (
|
| T_shallow_closure (_, _, _) -> (
|
||||||
trace (simple_error "Compiling shallow closure application") @@
|
trace (simple_error "Compiling shallow closure application") @@
|
||||||
@ -238,7 +262,49 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
|
|||||||
let%bind output_type = Compiler_type.type_ anon.output in
|
let%bind output_type = Compiler_type.type_ anon.output in
|
||||||
let code = virtual_push_first @@ i_lambda input_type output_type body in
|
let code = virtual_push_first @@ i_lambda input_type output_type body in
|
||||||
return code
|
return code
|
||||||
| Deep_capture _small_env -> simple_fail "no deep capture expression yet"
|
| Deep_capture small_env ->
|
||||||
|
(* Capture the sub environment. *)
|
||||||
|
let env_type = Compiler_environment.Small.to_mini_c_type small_env in
|
||||||
|
let%bind body = translate_closure_body anon env_type in
|
||||||
|
let%bind (_env , build_capture_code) =
|
||||||
|
let aux_leaf = fun prec (var_name , tv) ->
|
||||||
|
let%bind (small_env , code) = prec in
|
||||||
|
let small_env' = Environment.add (var_name , tv) small_env in
|
||||||
|
let%bind append_code = Compiler_environment.to_michelson_add (var_name , tv) small_env in
|
||||||
|
let%bind (get_code , _) = Compiler_environment.to_michelson_get env var_name in
|
||||||
|
let code' = seq [
|
||||||
|
code ;
|
||||||
|
i_comment ("deep closure get " ^ var_name) ;
|
||||||
|
dip (seq [ i_dup ; get_code ] ) ; i_swap ;
|
||||||
|
append_code ;
|
||||||
|
] in
|
||||||
|
ok (small_env' , code')
|
||||||
|
in
|
||||||
|
Append_tree.fold_s_ne (ok (Environment.empty , i_push_unit)) aux_leaf small_env
|
||||||
|
in
|
||||||
|
let%bind input_type =
|
||||||
|
let input_type = Combinators.t_pair anon.input env_type in
|
||||||
|
Compiler_type.type_ input_type in
|
||||||
|
let%bind output_type = Compiler_type.type_ anon.output in
|
||||||
|
let code = virtual_push_first @@ seq [ (* stack :: env *)
|
||||||
|
i_comment "env on top" ;
|
||||||
|
dip build_capture_code ; i_swap ; (* small_env :: stack :: env *)
|
||||||
|
i_comment "lambda" ;
|
||||||
|
i_lambda input_type output_type body ; (* lambda :: small_env :: stack :: env *)
|
||||||
|
i_comment "pair env + lambda" ;
|
||||||
|
i_piar ; (* (small_env * lambda) :: stack :: env *)
|
||||||
|
i_comment "new stack" ;
|
||||||
|
] in
|
||||||
|
let error =
|
||||||
|
let error_title () = "michelson type-checking trace" in
|
||||||
|
let error_content () =
|
||||||
|
Format.asprintf "Env : %a\n"
|
||||||
|
PP.environment_small small_env
|
||||||
|
in
|
||||||
|
error error_title error_content
|
||||||
|
in
|
||||||
|
trace error @@
|
||||||
|
return code
|
||||||
| Shallow_capture env ->
|
| Shallow_capture env ->
|
||||||
(* Capture the whole environment. *)
|
(* Capture the whole environment. *)
|
||||||
let env_type = Compiler_environment.to_mini_c_type env in
|
let env_type = Compiler_environment.to_mini_c_type env in
|
||||||
|
@ -119,6 +119,7 @@ let t_nat : type_value = T_base Base_nat
|
|||||||
|
|
||||||
let t_function x y : type_value = T_function ( x , y )
|
let t_function x y : type_value = T_function ( x , y )
|
||||||
let t_shallow_closure x y z : type_value = T_shallow_closure ( x , y , z )
|
let t_shallow_closure x y z : type_value = T_shallow_closure ( x , y , z )
|
||||||
|
let t_deep_closure x y z : type_value = T_deep_closure ( x , y , z )
|
||||||
let t_pair x y : type_value = T_pair ( x , y )
|
let t_pair x y : type_value = T_pair ( x , y )
|
||||||
let t_union x y : type_value = T_or ( x , y )
|
let t_union x y : type_value = T_or ( x , y )
|
||||||
|
|
||||||
|
@ -27,7 +27,6 @@ module Small = struct
|
|||||||
s PP.environment_small t in
|
s PP.environment_small t in
|
||||||
error title content
|
error title content
|
||||||
|
|
||||||
|
|
||||||
let has' s = exists' (fun ((x, _):element) -> x = s)
|
let has' s = exists' (fun ((x, _):element) -> x = s)
|
||||||
let has s = function
|
let has s = function
|
||||||
| Empty -> false
|
| Empty -> false
|
||||||
|
@ -422,9 +422,39 @@ and translate_lambda_shallow : Mini_c.Environment.t -> AST.lambda -> Mini_c.expr
|
|||||||
let new_env = Environment.add (binder, input_type') env' in
|
let new_env = Environment.add (binder, input_type') env' in
|
||||||
let%bind (_, e) as body = translate_block new_env body in
|
let%bind (_, e) as body = translate_block new_env body in
|
||||||
let%bind result = translate_annotated_expression e.post_environment result in
|
let%bind result = translate_annotated_expression e.post_environment result in
|
||||||
let capture_type = Shallow_capture env' in
|
|
||||||
let%bind output_type' = translate_type output_type in
|
let%bind output_type' = translate_type output_type in
|
||||||
let tv = Combinators.t_shallow_closure env input_type' output_type' in
|
let tv = Combinators.t_shallow_closure env input_type' output_type' in
|
||||||
|
let capture_type = Shallow_capture env' in
|
||||||
|
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in
|
||||||
|
ok @@ Combinators.Expression.make_tpl (E_function content, tv, env)
|
||||||
|
|
||||||
|
and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l ->
|
||||||
|
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
|
||||||
|
(* Deep capture. Capture the relevant part of the environment. Extend it with a new scope. Append it the input. *)
|
||||||
|
let%bind input_type' = translate_type input_type in
|
||||||
|
let%bind small_env =
|
||||||
|
let env' = Environment.extend env in
|
||||||
|
let new_env = Environment.add (binder, input_type') env' in
|
||||||
|
let free_variables = Ast_typed.Misc.Free_variables.lambda [] l in
|
||||||
|
let%bind elements =
|
||||||
|
let aux x =
|
||||||
|
let not_found_error =
|
||||||
|
let title () = "translate deep shallow (type checker didn't do its job)" in
|
||||||
|
let content () = Format.asprintf "%s in %a" x Mini_c.PP.environment new_env in
|
||||||
|
error title content in
|
||||||
|
trace_option not_found_error @@
|
||||||
|
Environment.get_opt new_env x in
|
||||||
|
bind_map_list aux free_variables in
|
||||||
|
let kvs = List.combine free_variables elements in
|
||||||
|
let small_env = Environment.Small.of_list kvs in
|
||||||
|
ok small_env
|
||||||
|
in
|
||||||
|
let new_env = Environment.(add (binder , input_type') @@ extend @@ of_small small_env) in
|
||||||
|
let%bind (_, e) as body = translate_block new_env body in
|
||||||
|
let%bind result = translate_annotated_expression e.post_environment result in
|
||||||
|
let%bind output_type' = translate_type output_type in
|
||||||
|
let tv = Combinators.t_deep_closure small_env input_type' output_type' in
|
||||||
|
let capture_type = Deep_capture small_env in
|
||||||
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in
|
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in
|
||||||
ok @@ Combinators.Expression.make_tpl (E_function content, tv, env)
|
ok @@ Combinators.Expression.make_tpl (E_function content, tv, env)
|
||||||
|
|
||||||
@ -452,8 +482,8 @@ and translate_lambda env l =
|
|||||||
ok @@ Combinators.Expression.make_tpl (E_literal (D_function {capture=None;content}), tv, env)
|
ok @@ Combinators.Expression.make_tpl (E_literal (D_function {capture=None;content}), tv, env)
|
||||||
)
|
)
|
||||||
| _ -> (
|
| _ -> (
|
||||||
trace (simple_error "translate lambda shallow") @@
|
trace (simple_error "translate lambda deep") @@
|
||||||
translate_lambda_shallow env l
|
translate_lambda_deep env l
|
||||||
)
|
)
|
||||||
|
|
||||||
let translate_declaration env (d:AST.declaration) : toplevel_statement result =
|
let translate_declaration env (d:AST.declaration) : toplevel_statement result =
|
||||||
|
@ -73,7 +73,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
|
|||||||
let%bind ae' =
|
let%bind ae' =
|
||||||
trace (constant_declaration_error name annotated_expression) @@
|
trace (constant_declaration_error name annotated_expression) @@
|
||||||
type_annotated_expression env annotated_expression in
|
type_annotated_expression env annotated_expression in
|
||||||
let env' = Environment.add_ez name ae'.type_annotation env in
|
let env' = Environment.add_ez_declaration name (O.get_type_annotation ae') (O.get_expression ae') env in
|
||||||
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , env')))
|
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , env')))
|
||||||
|
|
||||||
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
|
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
|
||||||
@ -109,7 +109,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
|
|||||||
| None, None -> simple_fail "Initial assignments need type annotation"
|
| None, None -> simple_fail "Initial assignments need type annotation"
|
||||||
| Some _, None ->
|
| Some _, None ->
|
||||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||||
let e' = Environment.add_ez name annotated_expression.type_annotation e in
|
let e' = Environment.add_ez_ae name annotated_expression e in
|
||||||
ok (e', [O.I_declaration (make_n_e name annotated_expression)])
|
ok (e', [O.I_declaration (make_n_e name annotated_expression)])
|
||||||
| None, Some prev ->
|
| None, Some prev ->
|
||||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||||
@ -120,7 +120,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
|
|||||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||||
let%bind _assert = trace (simple_error "Annotation doesn't match environment")
|
let%bind _assert = trace (simple_error "Annotation doesn't match environment")
|
||||||
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
|
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
|
||||||
let e' = Environment.add_ez name annotated_expression.type_annotation e in
|
let e' = Environment.add_ez_ae name annotated_expression e in
|
||||||
ok (e', [O.I_assignment (make_n_e name annotated_expression)])
|
ok (e', [O.I_assignment (make_n_e name annotated_expression)])
|
||||||
)
|
)
|
||||||
| I_matching (ex, m) ->
|
| I_matching (ex, m) ->
|
||||||
@ -168,7 +168,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
|||||||
let%bind match_none = f e match_none in
|
let%bind match_none = f e match_none in
|
||||||
let (n, b) = match_some in
|
let (n, b) = match_some in
|
||||||
let n' = n, t_opt in
|
let n' = n, t_opt in
|
||||||
let e' = Environment.add_ez n t_opt e in
|
let e' = Environment.add_ez_binder n t_opt e in
|
||||||
let%bind b' = f e' b in
|
let%bind b' = f e' b in
|
||||||
ok (O.Match_option {match_none ; match_some = (n', b')})
|
ok (O.Match_option {match_none ; match_some = (n', b')})
|
||||||
| Match_list {match_nil ; match_cons} ->
|
| Match_list {match_nil ; match_cons} ->
|
||||||
@ -177,8 +177,8 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
|||||||
@@ get_t_list t in
|
@@ get_t_list t in
|
||||||
let%bind match_nil = f e match_nil in
|
let%bind match_nil = f e match_nil in
|
||||||
let (hd, tl, b) = match_cons in
|
let (hd, tl, b) = match_cons in
|
||||||
let e' = Environment.add_ez hd t_list e in
|
let e' = Environment.add_ez_binder hd t_list e in
|
||||||
let e' = Environment.add_ez tl t e' in
|
let e' = Environment.add_ez_binder tl t e' in
|
||||||
let%bind b' = f e' b in
|
let%bind b' = f e' b in
|
||||||
ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
|
ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
|
||||||
| Match_tuple (lst, b) ->
|
| Match_tuple (lst, b) ->
|
||||||
@ -188,7 +188,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
|||||||
let%bind lst' =
|
let%bind lst' =
|
||||||
generic_try (simple_error "Matching tuple of different size")
|
generic_try (simple_error "Matching tuple of different size")
|
||||||
@@ (fun () -> List.combine lst t_tuple) in
|
@@ (fun () -> List.combine lst t_tuple) in
|
||||||
let aux prev (name, tv) = Environment.add_ez name tv prev in
|
let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
|
||||||
let e' = List.fold_left aux e lst' in
|
let e' = List.fold_left aux e lst' in
|
||||||
let%bind b' = f e' b in
|
let%bind b' = f e' b in
|
||||||
ok (O.Match_tuple (lst, b'))
|
ok (O.Match_tuple (lst, b'))
|
||||||
@ -230,7 +230,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
|||||||
let%bind (constructor , _) =
|
let%bind (constructor , _) =
|
||||||
trace_option (simple_error "bad constructor??") @@
|
trace_option (simple_error "bad constructor??") @@
|
||||||
Environment.get_constructor constructor_name e in
|
Environment.get_constructor constructor_name e in
|
||||||
let e' = Environment.add_ez name constructor e in
|
let e' = Environment.add_ez_binder name constructor e in
|
||||||
let%bind b' = f e' b in
|
let%bind b' = f e' b in
|
||||||
ok ((constructor_name , name) , b')
|
ok ((constructor_name , name) , b')
|
||||||
in
|
in
|
||||||
@ -414,7 +414,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
|
|||||||
} ->
|
} ->
|
||||||
let%bind input_type = evaluate_type e input_type in
|
let%bind input_type = evaluate_type e input_type in
|
||||||
let%bind output_type = evaluate_type e output_type in
|
let%bind output_type = evaluate_type e output_type in
|
||||||
let e' = Environment.add_ez binder input_type e in
|
let e' = Environment.add_ez_binder binder input_type e in
|
||||||
let%bind (body, e'') = type_block_full e' body in
|
let%bind (body, e'') = type_block_full e' body in
|
||||||
let%bind result = type_annotated_expression e'' result in
|
let%bind result = type_annotated_expression e'' result in
|
||||||
return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ())
|
return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ())
|
||||||
|
Loading…
Reference in New Issue
Block a user