prepare lifting transpilation environments
This commit is contained in:
parent
c2ac9ab361
commit
7a2bd3d73d
@ -135,6 +135,10 @@ let rec bind_list = function
|
|||||||
bind_list tl >>? fun tl ->
|
bind_list tl >>? fun tl ->
|
||||||
ok @@ hd :: tl
|
ok @@ hd :: tl
|
||||||
)
|
)
|
||||||
|
let bind_ne_list = fun (hd , tl) ->
|
||||||
|
hd >>? fun hd ->
|
||||||
|
bind_list tl >>? fun tl ->
|
||||||
|
ok @@ (hd , tl)
|
||||||
|
|
||||||
let bind_smap (s:_ X_map.String.t) =
|
let bind_smap (s:_ X_map.String.t) =
|
||||||
let open X_map.String in
|
let open X_map.String in
|
||||||
@ -154,6 +158,7 @@ let bind_fold_smap f init (smap : _ X_map.String.t) =
|
|||||||
let bind_map_smap f smap = bind_smap (X_map.String.map f smap)
|
let bind_map_smap f smap = bind_smap (X_map.String.map f smap)
|
||||||
|
|
||||||
let bind_map_list f lst = bind_list (List.map f lst)
|
let bind_map_list f lst = bind_list (List.map f lst)
|
||||||
|
let bind_map_ne_list : _ -> 'a X_list.Ne.t -> 'b X_list.Ne.t result = fun f lst -> bind_ne_list (X_list.Ne.map f lst)
|
||||||
|
|
||||||
let bind_location (x:_ Location.wrap) =
|
let bind_location (x:_ Location.wrap) =
|
||||||
x.wrap_content >>? fun wrap_content ->
|
x.wrap_content >>? fun wrap_content ->
|
||||||
@ -168,6 +173,13 @@ let bind_fold_list f init lst =
|
|||||||
in
|
in
|
||||||
List.fold_left aux (ok init) lst
|
List.fold_left aux (ok init) lst
|
||||||
|
|
||||||
|
let bind_fold_right_list f init lst =
|
||||||
|
let aux x y =
|
||||||
|
x >>? fun x ->
|
||||||
|
f x y
|
||||||
|
in
|
||||||
|
X_list.fold_right' aux (ok init) lst
|
||||||
|
|
||||||
let bind_find_map_list error f lst =
|
let bind_find_map_list error f lst =
|
||||||
let rec aux lst =
|
let rec aux lst =
|
||||||
match lst with
|
match lst with
|
||||||
|
@ -149,6 +149,6 @@ let get_a_bool (t:annotated_expression) =
|
|||||||
open Environment
|
open Environment
|
||||||
let env_sum_type ?(env = full_empty)
|
let env_sum_type ?(env = full_empty)
|
||||||
?(name = "a_sum_type")
|
?(name = "a_sum_type")
|
||||||
(lst : (string * element) list) =
|
(lst : (string * type_value) list) =
|
||||||
add_type name (make_t_ez_sum lst) env
|
add_type name (make_t_ez_sum lst) env
|
||||||
|
|
||||||
|
@ -1,32 +1,36 @@
|
|||||||
open Types
|
open Types
|
||||||
|
|
||||||
type element = type_value
|
type element = environment_element
|
||||||
|
let make_element : type_value -> full_environment -> element =
|
||||||
|
fun type_value source_environment -> {type_value ; source_environment}
|
||||||
|
|
||||||
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)
|
||||||
let map_type_environment : _ -> t -> t = fun f (a , b) -> (a , f b)
|
let map_type_environment : _ -> t -> t = fun f (a , b) -> (a , f b)
|
||||||
|
|
||||||
let add : string -> element -> t -> t = fun k v -> map_environment (fun x -> (k , v) :: x)
|
let add : string -> element -> t -> t = fun k v -> map_environment (fun x -> (k , v) :: x)
|
||||||
let add_type : string -> element -> t -> t = fun k v -> map_type_environment (fun x -> (k , v) :: x)
|
let add_type : string -> type_value -> t -> t = fun k v -> map_type_environment (fun x -> (k , v) :: x)
|
||||||
let get_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_environment x)
|
let get_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_environment x)
|
||||||
let get_type_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_type_environment x)
|
let get_type_opt : string -> t -> type_value option = fun k x -> List.assoc_opt k (get_type_environment x)
|
||||||
end
|
end
|
||||||
|
|
||||||
type t = full_environment
|
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_type : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type 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_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 -> element 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
|
||||||
|
|
||||||
let get_constructor : string -> t -> (element * element) option = fun k x -> (* Left is the constructor, right is the sum type *)
|
let get_constructor : string -> t -> (type_value * type_value) option = fun k x -> (* Left is the constructor, right is the sum type *)
|
||||||
let aux = fun x ->
|
let aux = fun x ->
|
||||||
let aux = fun (_type_name , x) ->
|
let aux = fun (_type_name , x) ->
|
||||||
match x.type_value' with
|
match x.type_value' with
|
||||||
@ -43,14 +47,17 @@ module PP = struct
|
|||||||
|
|
||||||
let list_sep_scope x = list_sep x (const " | ")
|
let list_sep_scope x = list_sep x (const " | ")
|
||||||
|
|
||||||
let assoc = fun ppf (k , tv) ->
|
let environment_element = fun ppf (k , (ele : environment_element)) ->
|
||||||
|
fprintf ppf "%s -> %a" k PP.type_value ele.type_value
|
||||||
|
|
||||||
|
let type_environment_element = fun ppf (k , tv) ->
|
||||||
fprintf ppf "%s -> %a" k PP.type_value tv
|
fprintf ppf "%s -> %a" k PP.type_value tv
|
||||||
|
|
||||||
let environment : _ -> environment -> unit = fun ppf lst ->
|
let environment : _ -> environment -> unit = fun ppf lst ->
|
||||||
fprintf ppf "E[%a]" (list_sep assoc (const " , ")) lst
|
fprintf ppf "E[%a]" (list_sep environment_element (const " , ")) lst
|
||||||
|
|
||||||
let type_environment = fun ppf lst ->
|
let type_environment = fun ppf lst ->
|
||||||
fprintf ppf "T[%a]" (list_sep assoc (const " , ")) lst
|
fprintf ppf "T[%a]" (list_sep type_environment_element (const " , ")) lst
|
||||||
|
|
||||||
let small_environment : _ -> small_environment -> unit = fun ppf e ->
|
let small_environment : _ -> small_environment -> unit = fun ppf e ->
|
||||||
fprintf ppf "- %a\t%a"
|
fprintf ppf "- %a\t%a"
|
||||||
|
@ -16,7 +16,11 @@ and declaration =
|
|||||||
| Declaration_constant of named_expression
|
| Declaration_constant of named_expression
|
||||||
(* | Macro_declaration of macro_declaration *)
|
(* | Macro_declaration of macro_declaration *)
|
||||||
|
|
||||||
and environment = (string * type_value) list
|
and environment_element = {
|
||||||
|
type_value : type_value ;
|
||||||
|
source_environment : full_environment ;
|
||||||
|
}
|
||||||
|
and environment = (string * environment_element) list
|
||||||
and type_environment = (string * type_value) list
|
and type_environment = (string * type_value) list
|
||||||
and small_environment = (environment * type_environment)
|
and small_environment = (environment * type_environment)
|
||||||
and full_environment = small_environment List.Ne.t
|
and full_environment = small_environment List.Ne.t
|
||||||
|
@ -85,7 +85,6 @@ module Ty = struct
|
|||||||
let%bind (Ex_ty t') = type_ t in
|
let%bind (Ex_ty t') = type_ t in
|
||||||
ok @@ Ex_ty Contract_types.(option t')
|
ok @@ Ex_ty Contract_types.(option t')
|
||||||
|
|
||||||
|
|
||||||
and environment_small' = let open Append_tree in function
|
and environment_small' = let open Append_tree in function
|
||||||
| Leaf (_, x) -> type_ x
|
| Leaf (_, x) -> type_ x
|
||||||
| Node {a;b} ->
|
| Node {a;b} ->
|
||||||
@ -98,7 +97,7 @@ module Ty = struct
|
|||||||
| Full x -> environment_small' x
|
| Full x -> environment_small' x
|
||||||
|
|
||||||
and environment = function
|
and environment = function
|
||||||
| [] | [Empty] -> simple_fail "Schema.Big.to_ty"
|
| [] | [Empty] -> ok @@ Ex_ty Contract_types.unit
|
||||||
| [a] -> environment_small a
|
| [a] -> environment_small a
|
||||||
| Empty :: b -> environment b
|
| Empty :: b -> environment b
|
||||||
| a::b ->
|
| a::b ->
|
||||||
|
@ -182,9 +182,24 @@ and translate_literal : AST.literal -> value = fun l -> match l with
|
|||||||
| Literal_string s -> D_string s
|
| Literal_string s -> D_string s
|
||||||
| Literal_unit -> D_unit
|
| Literal_unit -> D_unit
|
||||||
|
|
||||||
|
and transpile_small_environment : AST.small_environment -> Environment.Small.t result = fun x ->
|
||||||
|
let x' = AST.Environment.Small.get_environment x in
|
||||||
|
let aux prec (name , (ele : AST.environment_element)) =
|
||||||
|
let%bind tv' = translate_type ele.type_value in
|
||||||
|
ok @@ Environment.Small.append (name , tv') prec
|
||||||
|
in
|
||||||
|
trace (simple_error "transpiling small environment") @@
|
||||||
|
bind_fold_right_list aux Append_tree.Empty x'
|
||||||
|
|
||||||
|
and transpile_environment : AST.full_environment -> Environment.t result = fun x ->
|
||||||
|
let%bind nlst = bind_map_ne_list transpile_small_environment x in
|
||||||
|
ok @@ List.Ne.to_list nlst
|
||||||
|
|
||||||
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
|
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
|
||||||
let%bind tv = translate_type ae.type_annotation in
|
let%bind tv = translate_type ae.type_annotation in
|
||||||
let return ?(tv = tv) expr = ok @@ Combinators.Expression.make_tpl (expr, tv, env) in
|
let return ?(tv = tv) expr =
|
||||||
|
(* let%bind env' = transpile_environment ae.environment in *)
|
||||||
|
ok @@ Combinators.Expression.make_tpl (expr, tv, env) in
|
||||||
let f = translate_annotated_expression env in
|
let f = translate_annotated_expression env in
|
||||||
match ae.expression with
|
match ae.expression with
|
||||||
| E_literal l -> return @@ E_literal (translate_literal l)
|
| E_literal l -> return @@ E_literal (translate_literal l)
|
||||||
@ -486,7 +501,6 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
|
|||||||
in
|
in
|
||||||
aux (tree, v)
|
aux (tree, v)
|
||||||
|
|
||||||
|
|
||||||
let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result =
|
let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result =
|
||||||
let open! AST in
|
let open! AST in
|
||||||
let return e = ok (make_a_e_empty e t) in
|
let return e = ok (make_a_e_empty e t) in
|
||||||
|
@ -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 name ae'.type_annotation env in
|
let env' = Environment.add_ez name ae'.type_annotation env in
|
||||||
ok (env', Some (O.Declaration_constant (make_n_e name ae')))
|
ok (env', Some (O.Declaration_constant (make_n_e name ae')))
|
||||||
|
|
||||||
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 =
|
||||||
@ -106,18 +106,18 @@ 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 name annotated_expression.type_annotation e in
|
let e' = Environment.add_ez name annotated_expression.type_annotation 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
|
||||||
let%bind _ =
|
let%bind _ =
|
||||||
O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
|
O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
|
||||||
ok (e, [O.I_assignment (make_n_e name annotated_expression)])
|
ok (e, [O.I_assignment (make_n_e name annotated_expression)])
|
||||||
| Some _, Some prev ->
|
| Some _, Some prev ->
|
||||||
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) in
|
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in
|
||||||
let e' = Environment.add name annotated_expression.type_annotation e in
|
let e' = Environment.add_ez name annotated_expression.type_annotation 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) ->
|
||||||
@ -130,7 +130,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
|
|||||||
let%bind ty =
|
let%bind ty =
|
||||||
trace_option (simple_error "unbound variable in record_patch") @@
|
trace_option (simple_error "unbound variable in record_patch") @@
|
||||||
Environment.get_opt r e in
|
Environment.get_opt r e in
|
||||||
let tv = O.{type_name = r ; type_value = ty} in
|
let tv = O.{type_name = r ; type_value = ty.type_value} in
|
||||||
let aux ty access =
|
let aux ty access =
|
||||||
match access with
|
match access with
|
||||||
| I.Access_record s ->
|
| I.Access_record s ->
|
||||||
@ -142,7 +142,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
|
|||||||
generic_try (simple_error "unbound tuple access in record_patch") @@
|
generic_try (simple_error "unbound tuple access in record_patch") @@
|
||||||
(fun () -> List.nth t i)
|
(fun () -> List.nth t i)
|
||||||
in
|
in
|
||||||
let%bind _assert = bind_fold_list aux ty (path @ [Access_record s]) in
|
let%bind _assert = bind_fold_list aux ty.type_value (path @ [Access_record s]) in
|
||||||
ok @@ O.I_patch (tv, path @ [Access_record s], ae')
|
ok @@ O.I_patch (tv, path @ [Access_record s], ae')
|
||||||
in
|
in
|
||||||
let%bind lst' = bind_map_list aux lst in
|
let%bind lst' = bind_map_list aux lst in
|
||||||
@ -165,7 +165,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 n t_opt e in
|
let e' = Environment.add_ez 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} ->
|
||||||
@ -174,8 +174,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 hd t_list e in
|
let e' = Environment.add_ez hd t_list e in
|
||||||
let e' = Environment.add tl t e' in
|
let e' = Environment.add_ez 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) ->
|
||||||
@ -185,7 +185,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 name tv prev in
|
let aux prev (name, tv) = Environment.add_ez 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'))
|
||||||
@ -239,7 +239,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
|
|||||||
let%bind tv' =
|
let%bind tv' =
|
||||||
trace_option (unbound_variable e name)
|
trace_option (unbound_variable e name)
|
||||||
@@ Environment.get_opt name e in
|
@@ Environment.get_opt name e in
|
||||||
return (E_variable name) tv'
|
return (E_variable name) tv'.type_value
|
||||||
| E_literal (Literal_bool b) ->
|
| E_literal (Literal_bool b) ->
|
||||||
return (E_literal (Literal_bool b)) (t_bool ())
|
return (E_literal (Literal_bool b)) (t_bool ())
|
||||||
| E_literal Literal_unit ->
|
| E_literal Literal_unit ->
|
||||||
@ -359,7 +359,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 binder input_type e in
|
let e' = Environment.add_ez 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