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

More progress on merging new typer and new dev

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-10-10 01:23:55 -04:00
parent 5de98259dc
commit 4fa54dd2c1
5 changed files with 230 additions and 167 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

85
src/passes/4-typer/solver.ml
View File

@ -112,8 +112,8 @@ module Wrap = struct
[C_equation (P_variable (type_name) , pattern)] , type_name
*)
let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys ->
let patterns = List.map type_expression_to_type_value_copypasted tys in
let tuple : T.type_value list -> (constraints * O.type_variable) = fun tys ->
let patterns = List.map type_expression_to_type_value tys in
let pattern = O.(P_constant (C_tuple , patterns)) in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
@ -143,7 +143,7 @@ module Wrap = struct
end
(* TODO: I think we should take an I.expression for the base+label *)
let access_label ~base ~label : (constraints * O.type_variable) =
let access_label ~(base : T.type_value) ~(label : O.label) : (constraints * O.type_variable) =
let base' = type_expression_to_type_value base in
let expr_type = Core.fresh_type_variable () in
[O.C_access_label (base' , label , expr_type)] , expr_type
@ -151,14 +151,14 @@ module Wrap = struct
let access_int ~base ~index = access_label ~base ~label:(L_int index)
let access_string ~base ~property = access_label ~base ~label:(L_string property)
let access_map : base:I.type_expression -> key:I.type_expression -> (constraints * O.type_variable) =
let access_map : base:T.type_value -> key:T.type_value -> (constraints * O.type_variable) =
let mk_map_type key_type element_type =
O.P_constant O.(C_map , [P_variable element_type; P_variable key_type]) in
fun ~base ~key ->
let key_type = Core.fresh_type_variable () in
let element_type = Core.fresh_type_variable () in
let base' = type_expression_to_type_value_copypasted base in
let key' = type_expression_to_type_value_copypasted key in
let base' = type_expression_to_type_value base in
let key' = type_expression_to_type_value key in
let base_expected = mk_map_type key_type element_type in
let expr_type = Core.fresh_type_variable () in
O.[C_equation (base' , base_expected);
@ -166,27 +166,27 @@ module Wrap = struct
C_equation (P_variable expr_type , P_variable element_type)] , expr_type
let constructor
: I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable)
: T.type_value -> T.type_value -> T.type_value -> (constraints * O.type_variable)
= fun t_arg c_arg sum ->
let t_arg = type_expression_to_type_value_copypasted t_arg in
let c_arg = type_expression_to_type_value_copypasted c_arg in
let sum = type_expression_to_type_value_copypasted sum in
let t_arg = type_expression_to_type_value t_arg in
let c_arg = type_expression_to_type_value c_arg in
let sum = type_expression_to_type_value sum in
let whole_expr = Core.fresh_type_variable () in
[
C_equation (P_variable (whole_expr) , sum) ;
C_equation (t_arg , c_arg)
] , whole_expr
let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields ->
let record_type = type_expression_to_type_value_copypasted (I.t_record fields) in
let record : T.type_value I.type_name_map -> (constraints * O.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () in
[C_equation (P_variable whole_expr , record_type)] , whole_expr
let collection : O.constant_tag -> I.type_expression list -> (constraints * O.type_variable) =
let collection : O.constant_tag -> T.type_value list -> (constraints * O.type_variable) =
fun ctor element_tys ->
let elttype = O.P_variable (Core.fresh_type_variable ()) in
let aux elt =
let elt' = type_expression_to_type_value_copypasted elt
let elt' = type_expression_to_type_value elt
in O.C_equation (elttype , elt') in
let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in
@ -197,15 +197,15 @@ module Wrap = struct
let list = collection O.C_list
let set = collection O.C_set
let map : (I.type_expression * I.type_expression) list -> (constraints * O.type_variable) =
let map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
fun kv_tys ->
let k_type = O.P_variable (Core.fresh_type_variable ()) in
let v_type = O.P_variable (Core.fresh_type_variable ()) in
let aux_k (k , _v) =
let k' = type_expression_to_type_value_copypasted k in
let k' = type_expression_to_type_value k in
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value_copypasted v in
let v' = type_expression_to_type_value v in
O.C_equation (v_type , v') in
let equations_k = List.map aux_k kv_tys in
let equations_v = List.map aux_v kv_tys in
@ -214,19 +214,38 @@ module Wrap = struct
C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let big_map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
fun kv_tys ->
let k_type = O.P_variable (Core.fresh_type_variable ()) in
let v_type = O.P_variable (Core.fresh_type_variable ()) in
let aux_k (k , _v) =
let k' = type_expression_to_type_value k in
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value v in
O.C_equation (v_type , v') in
let equations_k = List.map aux_k kv_tys in
let equations_v = List.map aux_v kv_tys in
let whole_expr = Core.fresh_type_variable () in
O.[
(* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *)
C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let application : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun f arg ->
let whole_expr = Core.fresh_type_variable () in
let f' = type_expression_to_type_value_copypasted f in
let arg' = type_expression_to_type_value_copypasted arg in
let f' = type_expression_to_type_value f in
let arg' = type_expression_to_type_value arg in
O.[
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
] , whole_expr
let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let look_up : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun ds ind ->
let ds' = type_expression_to_type_value_copypasted ds in
let ind' = type_expression_to_type_value_copypasted ind in
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in
O.[
@ -234,20 +253,20 @@ module Wrap = struct
C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
] , whole_expr
let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let sequence : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun a b ->
let a' = type_expression_to_type_value_copypasted a in
let b' = type_expression_to_type_value_copypasted b in
let a' = type_expression_to_type_value a in
let b' = type_expression_to_type_value b in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (a' , P_constant (C_unit , [])) ;
C_equation (b' , P_variable whole_expr)
] , whole_expr
let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let loop : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun expr body ->
let expr' = type_expression_to_type_value_copypasted expr in
let body' = type_expression_to_type_value_copypasted body in
let expr' = type_expression_to_type_value expr in
let body' = type_expression_to_type_value body in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (expr' , P_constant (C_bool , [])) ;
@ -255,13 +274,13 @@ module Wrap = struct
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) =
let let_in : T.type_value -> T.type_value option -> T.type_value -> (constraints * O.type_variable) =
fun rhs rhs_tv_opt result ->
let rhs' = type_expression_to_type_value_copypasted rhs in
let result' = type_expression_to_type_value_copypasted result in
let rhs' = type_expression_to_type_value rhs in
let result' = type_expression_to_type_value result in
let rhs_tv_opt' = match rhs_tv_opt with
None -> []
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value_copypasted annot)] in
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (result' , P_variable whole_expr)

293
src/passes/4-typer/typer.ml
View File

@ -474,39 +474,35 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
* | _ -> return (E_literal (Literal_string s)) (t_string ())
* ) *)
(* Tuple *)
| E_tuple lst ->
| E_tuple lst -> (
let aux state hd = type_expression e state hd >>? swap in
let%bind (state', lst') = bind_fold_map_list aux state lst in
let tv_lst = List.map get_type_annotation lst' in
return (E_tuple lst') (t_tuple tv_lst ())
| E_accessor (ae', path) ->
let%bind e' = type_expression e ae' in
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
match a with
| Access_tuple index -> (
let%bind tpl_tv = get_t_tuple prev.type_annotation in
let%bind tv =
generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
@@ (fun () -> List.nth tpl_tv index) in
return (E_tuple_accessor (prev , index)) tv
return_wrapped (e_tuple lst') state' @@ Wrap.tuple tv_lst
)
| Access_record property -> (
let%bind r_tv = get_t_record prev.type_annotation in
let%bind tv =
generic_try (bad_record_access property ae' prev.type_annotation ae.location)
@@ (fun () -> SMap.find property r_tv) in
return (E_record_accessor (prev , property)) tv
| E_accessor (base , [Access_tuple index]) -> (
let%bind (base' , state') = type_expression e state base in
let wrapped = Wrap.access_int ~base:base'.type_annotation ~index in
return_wrapped (E_tuple_accessor (base' , index)) state' wrapped
)
| Access_map ae' -> (
let%bind ae'' = type_expression e ae' in
let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in
let%bind () =
Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in
return (E_look_up (prev , ae'')) v
| E_accessor (base , [Access_record property]) -> (
let%bind (base' , state') = type_expression e state base in
let wrapped = Wrap.access_string ~base:base'.type_annotation ~property in
return_wrapped (E_record_accessor (base' , property)) state' wrapped
)
in
trace (simple_info "accessing") @@
bind_fold_list aux e' path
| E_accessor (base , [Access_map key_ae]) -> (
let%bind (base' , state') = type_expression e state base in
let%bind (key_ae' , state'') = type_expression e state' key_ae in
let xyz = get_type_annotation key_ae' in
let wrapped = Wrap.access_map ~base:base'.type_annotation ~key:xyz in
return_wrapped (E_look_up (base' , key_ae')) state'' wrapped
)
| E_accessor (_base , []) | E_accessor (_base , _ :: _ :: _) -> (
failwith
"The simplifier should produce E_accessor with only a single path element, not a list of path elements."
)
(* Sum *)
| E_constructor (c, expr) ->
let%bind (c_tv, sum_tv) =
@ -520,9 +516,10 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
trace_option error @@
Environment.get_constructor c e in
let%bind (expr' , state') = type_expression e state expr in
let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in
return_wrapped (E_constructor (c , expr')) state' wrapped
(* Record *)
| E_record m ->
let aux (acc, state) k expr =
@ -533,6 +530,8 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
let wrapped = Wrap.record (SMap.map get_type_annotation m') in
return_wrapped (E_record m') state' wrapped
(* Data-structure *)
(*
| E_list lst ->
let%bind lst' = bind_map_list (type_expression e) lst in
let%bind tv =
@ -605,112 +604,152 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
ok (t_map key_type value_type ())
in
return (E_map lst') tv
| E_big_map lst ->
let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
let%bind tv =
let aux opt c =
match opt with
| None -> ok (Some c)
| Some c' ->
let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
ok (Some c') in
let%bind key_type =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map fst lst' in
let%bind annot = bind_map_option get_t_big_map_key tv_opt in
trace (simple_info "empty map expression without a type annotation") @@
O.merge_annotation annot sub (needs_annotation ae "this map literal")
in
let%bind value_type =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map snd lst' in
let%bind annot = bind_map_option get_t_big_map_value tv_opt in
trace (simple_info "empty map expression without a type annotation") @@
O.merge_annotation annot sub (needs_annotation ae "this map literal")
in
ok (t_big_map key_type value_type ())
in
return (E_big_map lst') tv
| E_lambda {
binder ;
input_type ;
output_type ;
result ;
} -> (
let%bind input_type =
let%bind input_type =
(* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
let default_action e () = fail @@ (needs_annotation e "the returned value") in
match input_type with
| Some ty -> ok ty
| None -> (
match result.expression with
| I.E_let_in li -> (
match li.rhs.expression with
| I.E_variable name when name = (fst binder) -> (
match snd li.binder with
| Some ty -> ok ty
| None -> default_action li.rhs ()
)
| _ -> default_action li.rhs ()
)
| _ -> default_action result ()
)
in
evaluate_type e input_type in
let%bind output_type =
bind_map_option (evaluate_type e) output_type
in
let e' = Environment.add_ez_binder (fst binder) input_type e in
let%bind body = type_expression ?tv_opt:output_type e' result in
let output_type = body.type_annotation in
return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
)
| E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
let tv_lst = List.map get_type_annotation lst' in
let%bind (name', tv) =
type_constant name tv_lst tv_opt ae.location in
return (E_constant (name' , lst')) tv
*)
| E_list lst ->
let%bind (state', lst') =
bind_fold_map_list (fun state' elt -> type_expression e state' elt >>? swap) state lst in
let wrapped = Wrap.list (List.map (fun x -> O.(x.type_annotation)) lst') in
return_wrapped (E_list lst') state' wrapped
| E_set set ->
let aux = fun state' elt -> type_expression e state' elt >>? swap in
let%bind (state', set') =
bind_fold_map_list aux state set in
let wrapped = Wrap.set (List.map (fun x -> O.(x.type_annotation)) set') in
return_wrapped (E_set set') state' wrapped
| E_map map ->
let aux' state' elt = type_expression e state' elt >>? swap in
let aux = fun state' elt -> bind_fold_map_pair aux' state' elt in
let%bind (state', map') =
bind_fold_map_list aux state map in
let aux (x, y) = O.(x.type_annotation , y.type_annotation) in
let wrapped = Wrap.map (List.map aux map') in
return_wrapped (E_map map') state' wrapped
(* | E_big_map lst ->
* let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
* let%bind tv =
* let aux opt c =
* match opt with
* | None -> ok (Some c)
* | Some c' ->
* let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
* ok (Some c') in
* let%bind key_type =
* let%bind sub =
* bind_fold_list aux None
* @@ List.map get_type_annotation
* @@ List.map fst lst' in
* let%bind annot = bind_map_option get_t_big_map_key tv_opt in
* trace (simple_info "empty map expression without a type annotation") @@
* O.merge_annotation annot sub (needs_annotation ae "this map literal")
* in
* let%bind value_type =
* let%bind sub =
* bind_fold_list aux None
* @@ List.map get_type_annotation
* @@ List.map snd lst' in
* let%bind annot = bind_map_option get_t_big_map_value tv_opt in
* trace (simple_info "empty map expression without a type annotation") @@
* O.merge_annotation annot sub (needs_annotation ae "this map literal")
* in
* ok (t_big_map key_type value_type ())
* in
* return (E_big_map lst') tv *)
| E_big_map big_map ->
let aux' state' elt = type_expression e state' elt >>? swap in
let aux = fun state' elt -> bind_fold_map_pair aux' state' elt in
let%bind (state', big_map') =
bind_fold_map_list aux state big_map in
let aux (x, y) = O.(x.type_annotation , y.type_annotation) in
let wrapped = Wrap.big_map (List.map aux big_map') in
return_wrapped (E_big_map big_map') state' wrapped
(* | E_lambda {
* binder ;
* input_type ;
* output_type ;
* result ;
* } -> (
* let%bind input_type =
* let%bind input_type =
* (\* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *\)
* let default_action e () = fail @@ (needs_annotation e "the returned value") in
* match input_type with
* | Some ty -> ok ty
* | None -> (
* match result.expression with
* | I.E_let_in li -> (
* match li.rhs.expression with
* | I.E_variable name when name = (fst binder) -> (
* match snd li.binder with
* | Some ty -> ok ty
* | None -> default_action li.rhs ()
* )
* | _ -> default_action li.rhs ()
* )
* | _ -> default_action result ()
* )
* in
* evaluate_type e input_type in
* let%bind output_type =
* bind_map_option (evaluate_type e) output_type
* in
* let e' = Environment.add_ez_binder (fst binder) input_type e in
* let%bind body = type_expression ?tv_opt:output_type e' result in
* let output_type = body.type_annotation in
* return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
* ) *)
(* | E_constant (name, lst) ->
* let%bind lst' = bind_list @@ List.map (type_expression e) lst in
* let tv_lst = List.map get_type_annotation lst' in
* let%bind (name', tv) =
* type_constant name tv_lst tv_opt ae.location in
* return (E_constant (name' , lst')) tv *)
| E_application (f, arg) ->
let%bind (f' , state') = type_expression e state f in
let%bind (arg , state'') = type_expression e state' arg in
let wrapped = Wrap.application f'.type_annotation arg.type_annotation in
return_wrapped (E_application (f' , arg)) state'' wrapped
(* | E_look_up dsi ->
* let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
* let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
* let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
* return (E_look_up (ds , ind)) (t_option dst ()) *)
| E_look_up dsi ->
let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
return (E_look_up (ds , ind)) (t_option dst ())
let aux' state' elt = type_expression e state' elt >>? swap in
let%bind (state'' , (ds , ind)) = bind_fold_map_pair aux' state dsi in
let wrapped = Wrap.look_up ds.type_annotation ind.type_annotation in
return_wrapped (E_look_up (ds , ind)) state'' wrapped
(* Advanced *)
| E_matching (ex, m) -> (
let%bind ex' = type_expression e ex in
let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
let tvs =
let aux (cur:O.value O.matching) =
match cur with
| Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
| Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
| Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
| Match_tuple (_ , match_tuple) -> [ match_tuple ]
| Match_variant (lst , _) -> List.map snd lst in
List.map get_type_annotation @@ aux m' in
let aux prec cur =
let%bind () =
match prec with
| None -> ok ()
| Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
ok (Some cur) in
let%bind tv_opt = bind_fold_list aux None tvs in
let%bind tv =
trace_option (match_empty_variant m ae.location) @@
tv_opt in
return (O.E_matching (ex', m')) tv
)
(* | E_matching (ex, m) -> (
* let%bind ex' = type_expression e ex in
* let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
* let tvs =
* let aux (cur:O.value O.matching) =
* match cur with
* | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
* | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
* | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
* | Match_tuple (_ , match_tuple) -> [ match_tuple ]
* | Match_variant (lst , _) -> List.map snd lst in
* List.map get_type_annotation @@ aux m' in
* let aux prec cur =
* let%bind () =
* match prec with
* | None -> ok ()
* | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
* ok (Some cur) in
* let%bind tv_opt = bind_fold_list aux None tvs in
* let%bind tv =
* trace_option (match_empty_variant m ae.location) @@
* tv_opt in
* return (O.E_matching (ex', m')) tv
* ) *)
| E_sequence (a , b) ->
let%bind (a' , state') = type_expression e state a in
let%bind (b' , state'') = type_expression e state' b in

1
src/stages/ast_typed/combinators.ml
View File

@ -246,6 +246,7 @@ let e_application a b : expression = E_application (a , b)
let e_variable v : expression = E_variable v
let e_list lst : expression = E_list lst
let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
let e_tuple lst : expression = E_tuple lst
let e_a_unit = make_a_e e_unit (t_unit ())
let e_a_int n = make_a_e (e_int n) (t_int ())

1
src/stages/typesystem/core.ml
View File

@ -17,6 +17,7 @@
| C_record (* ( label , * ) … -> * *)
| C_variant (* ( label , * ) … -> * *)
| C_map (* * -> * -> * *)
| C_big_map (* * -> * -> * *)
| C_list (* * -> * *)
| C_set (* * -> * *)
| C_unit (* * *)

5
vendors/ligo-utils/simple-utils/trace.ml vendored
View File

@ -665,7 +665,10 @@ let bind_and (a, b) =
let bind_pair = bind_and
let bind_map_pair f (a, b) =
bind_pair (f a, f b)
let bind_fold_map_pair f acc (a, b) =
f acc a >>? fun (acc' , a') ->
f acc' b >>? fun (acc'' , b') ->
ok (acc'' , (a' , b'))
(**