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

Nearly builds, only one small API change and integration errors left

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-10-10 03:52:43 -04:00
parent 4fa54dd2c1
commit acfbd7eb15
2 changed files with 42 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -286,30 +286,30 @@ module Wrap = struct
C_equation (result' , P_variable whole_expr)
] @ rhs_tv_opt', whole_expr
let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let assign : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun v e ->
let v' = type_expression_to_type_value_copypasted v in
let e' = type_expression_to_type_value_copypasted e in
let v' = type_expression_to_type_value v in
let e' = type_expression_to_type_value e in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (v' , e') ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
let annotation : T.type_value -> T.type_value -> (constraints * O.type_variable) =
fun e annot ->
let e' = type_expression_to_type_value_copypasted e in
let annot' = type_expression_to_type_value_copypasted annot in
let e' = type_expression_to_type_value e in
let annot' = type_expression_to_type_value annot in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (e' , annot') ;
C_equation (e' , P_variable whole_expr)
] , whole_expr
let matching : I.type_expression list -> (constraints * O.type_variable) =
let matching : T.type_value list -> (constraints * O.type_variable) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_values = (List.map type_expression_to_type_value_copypasted es) in
let type_values = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values
in cs, whole_expr
@ -317,9 +317,9 @@ module Wrap = struct
Core.fresh_type_variable ()
let lambda
: I.type_expression ->
I.type_expression option ->
I.type_expression option ->
: T.type_value ->
T.type_value option ->
T.type_value option ->
(constraints * O.type_variable) =
fun fresh arg body ->
let whole_expr = Core.fresh_type_variable () in
@ -327,12 +327,12 @@ module Wrap = struct
let unification_body = Core.fresh_type_variable () in
let arg' = match arg with
None -> []
| Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value_copypasted arg)] in
| Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in
let body' = match body with
None -> []
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value_copypasted body)]
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
in O.[
C_equation (type_expression_to_type_value_copypasted fresh , P_variable unification_arg) ;
C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
C_equation (P_variable whole_expr ,
P_constant (C_arrow , [P_variable unification_arg ;
P_variable unification_body]))

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

@ -793,7 +793,7 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
| Access_map _ ->
fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
in
bind_fold_list aux (typed_name.type_expression , []) path in
bind_fold_list aux (typed_name.type_value , []) path in
let%bind (expr' , state') = type_expression e state expr in
let wrapped = Wrap.assign assign_tv expr'.type_annotation in
return_wrapped (O.E_assign (typed_name , path' , expr')) state' wrapped
@ -814,7 +814,7 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
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_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
@ -867,14 +867,14 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
let%bind input_type' = bind_map_option (evaluate_type e) input_type in
let%bind output_type' = bind_map_option (evaluate_type e) output_type in
let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in
let fresh : O.type_value = t_variable (Wrap.fresh_binder ()) () in
let e' = Environment.add_ez_binder (fst binder) fresh e in
let%bind (result , state') = type_expression e' state result in
let output_type = result.type_annotation in
let wrapped = Wrap.lambda fresh input_type' output_type' in
return_wrapped
(E_lambda {binder = fst binder;input_type=fresh;output_type;result})
(E_lambda {binder = fst binder; input_type=fresh;output_type; body=result})
state' wrapped
)
@ -964,8 +964,27 @@ let type_program' : I.program -> O.program result = fun p ->
(*
Tranform a Ast_typed type_expression into an ast_simplified type_expression
*)
let untype_type_expression (t:O.type_expression) : (I.type_expression) result =
ok t
let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
(* TODO: or should we use t.simplified if present? *)
match t.type_value' with
| O.T_tuple x ->
let%bind x' = bind_map_list untype_type_expression x in
ok @@ I.T_tuple x'
| O.T_sum x ->
let%bind x' = bind_map_smap untype_type_expression x in
ok @@ I.T_sum x'
| O.T_record x ->
let%bind x' = bind_map_smap untype_type_expression x in
ok @@ I.T_record x'
| O.T_constant (tag, args) ->
let%bind args' = bind_map_list untype_type_expression args in
ok @@ I.T_constant (tag, args')
| O.T_variable name -> ok @@ I.T_variable name (* TODO: is this the right conversion? *)
| O.T_function (a , b) ->
let%bind a' = untype_type_expression a in
let%bind b' = untype_type_expression b in
ok @@ I.T_function (a' , b')
(* match t.simplified with *)
(* | Some s -> ok s *)
(* | _ -> fail @@ internal_assertion_failure "trying to untype generated type" *)
@ -1049,9 +1068,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
let%bind ae' = untype_expression ae in
let%bind m' = untype_matching untype_expression m in
return (e_matching ae' m')
| E_failwith ae ->
let%bind ae' = untype_expression ae in
return (e_failwith ae')
(* | E_failwith ae ->
* let%bind ae' = untype_expression ae in
* return (e_failwith ae') *)
| E_sequence _
| E_loop _
| E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression