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

bugfix: new typer did not check a lambda's result' type against its annotation.

Browse Source
This commit is contained in:
Suzanne Dupéron 2020-05-26 00:18:55 +01:00
parent 2633d732a3
commit 4cb34a1d7e
2 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/passes/8-typer-new/typer.ml
View File

@ -420,8 +420,7 @@ and type_lambda e state {
let e' = Environment.add_ez_binder (binder) fresh e in
let%bind (result , state') = type_expression e' state result in
let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' result.type_expression in
ok (({binder;result}:O.lambda),state',wrapped)
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =

15
src/passes/8-typer-new/wrap.ml
View File

@ -339,23 +339,26 @@ let lambda
: T.type_expression ->
T.type_expression option ->
T.type_expression option ->
T.type_expression ->
(constraints * T.type_variable) =
fun fresh arg body ->
fun fresh arg output result ->
let whole_expr = Core.fresh_type_variable () in
let unification_arg = T.{ tsrc = "wrap: lambda: arg" ; t = P_variable (Core.fresh_type_variable ()) } in
let unification_body = T.{ tsrc = "wrap: lambda: whole" ; t = P_variable (Core.fresh_type_variable ()) } in
let unification_output = T.{ tsrc = "wrap: lambda: whole" ; t = P_variable (Core.fresh_type_variable ()) } in
let result' = type_expression_to_type_value result in
let arg' = match arg with
None -> []
| Some arg -> [c_equation unification_arg (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
let body' = match body with
let output' = match output with
None -> []
| Some body -> [c_equation unification_body (type_expression_to_type_value body) "wrap: lambda: body annot"]
| Some output -> [c_equation unification_output (type_expression_to_type_value output) "wrap: lambda: output annot"]
in [
c_equation unification_output result' "wrap: lambda: result" ;
c_equation (type_expression_to_type_value fresh) unification_arg "wrap: lambda: arg" ;
c_equation ({ tsrc = "wrap: lambda: whole" ; t = P_variable whole_expr })
(p_constant C_arrow ([unification_arg ; unification_body]))
(p_constant C_arrow ([unification_arg ; unification_output]))
"wrap: lambda: arrow (whole)"
] @ arg' @ body' , whole_expr
] @ arg' @ output' , whole_expr
(* This is pretty much a wrapper for an n-ary function. *)
let constant : O.type_value -> T.type_expression list -> (constraints * T.type_variable) =