adding E_sequence in sugar

This commit is contained in:
Pierre-Emmanuel Wulfman 2020-03-18 17:27:27 +01:00
parent cb1bc95d59
commit 6cafb4026b
29 changed files with 167 additions and 115 deletions

View File

@ -1174,7 +1174,7 @@ let%expect_test _ =
let%expect_test _ = let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return let rhs#812 = #P in let p = rhs#812.0 in let s = rhs#812.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"} ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return let rhs#654 = #P in let p = rhs#654.0 in let s = rhs#654.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1187,7 +1187,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8,
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return let rhs#815 = #P in let p = rhs#815.0 in let s = rhs#815.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"} ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return let rhs#657 = #P in let p = rhs#657.0 in let s = rhs#657.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can

View File

@ -26,7 +26,7 @@ let apply (entry_point : string) (param : Ast_core.expression) : Ast_core.expres
{ expression_content = Ast_core.E_variable name ; { expression_content = Ast_core.E_variable name ;
location = Virtual "generated entry-point variable" } in location = Virtual "generated entry-point variable" } in
let applied : Ast_core.expression = let applied : Ast_core.expression =
{ expression_content = Ast_core.E_application {expr1=entry_point_var; expr2=param} ; { expression_content = Ast_core.E_application {lamb=entry_point_var; args=param} ;
location = Virtual "generated application" } in location = Virtual "generated application" } in
ok applied ok applied

View File

@ -270,7 +270,7 @@ and eval_literal : Ast_typed.literal -> value result = function
and eval : Ast_typed.expression -> env -> value result and eval : Ast_typed.expression -> env -> value result
= fun term env -> = fun term env ->
match term.expression_content with match term.expression_content with
| E_application ({expr1 = f; expr2 = args}) -> ( | E_application ({lamb = f; args}) -> (
let%bind f' = eval f env in let%bind f' = eval f env in
let%bind args' = eval args env in let%bind args' = eval args env in
match f' with match f' with

View File

@ -253,9 +253,9 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
let%bind tv = transpile_environment_element_type ele in let%bind tv = transpile_environment_element_type ele in
return ~tv @@ E_variable (name) return ~tv @@ E_variable (name)
) )
| E_application {expr1;expr2} -> | E_application {lamb; args} ->
let%bind a = transpile_annotated_expression expr1 in let%bind a = transpile_annotated_expression lamb in
let%bind b = transpile_annotated_expression expr2 in let%bind b = transpile_annotated_expression args in
return @@ E_application (a, b) return @@ E_application (a, b)
| E_constructor {constructor;element} -> ( | E_constructor {constructor;element} -> (
let%bind param' = transpile_annotated_expression element in let%bind param' = transpile_annotated_expression element in
@ -550,10 +550,10 @@ and transpile_recursive {fun_name; fun_type; lambda} =
E_matching m -> E_matching m ->
let%bind ty = transpile_type e.type_expression in let%bind ty = transpile_type e.type_expression in
matching fun_name loop_type shadowed m ty | matching fun_name loop_type shadowed m ty |
E_application {expr1;expr2} -> ( E_application {lamb;args} -> (
match expr1.expression_content,shadowed with match lamb.expression_content,shadowed with
E_variable name, false when Var.equal fun_name name -> E_variable name, false when Var.equal fun_name name ->
let%bind expr = transpile_annotated_expression expr2 in let%bind expr = transpile_annotated_expression args in
ok @@ Expression.make (E_constant {cons_name=C_LOOP_CONTINUE;arguments=[expr]}) loop_type | ok @@ Expression.make (E_constant {cons_name=C_LOOP_CONTINUE;arguments=[expr]}) loop_type |
_ -> _ ->
let%bind expr = transpile_annotated_expression e in let%bind expr = transpile_annotated_expression e in

View File

@ -19,8 +19,8 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
| E_look_up ab -> | E_look_up ab ->
let%bind res = bind_fold_pair self init' ab in let%bind res = bind_fold_pair self init' ab in
ok res ok res
| E_application {expr1;expr2} -> ( | E_application {lamb;args} -> (
let ab = (expr1,expr2) in let ab = (lamb,args) in
let%bind res = bind_fold_pair self init' ab in let%bind res = bind_fold_pair self init' ab in
ok res ok res
) )
@ -59,6 +59,11 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
| E_recursive { lambda={result=e;_}; _} -> | E_recursive { lambda={result=e;_}; _} ->
let%bind res = self init' e in let%bind res = self init' e in
ok res ok res
| E_sequence {expr1;expr2} ->
let ab = (expr1,expr2) in
let%bind res = bind_fold_pair self init' ab in
ok res
and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m ->
match m with match m with
@ -145,10 +150,10 @@ let rec map_expression : exp_mapper -> expression -> expression result = fun f e
let%bind e' = self c.element in let%bind e' = self c.element in
return @@ E_constructor {c with element = e'} return @@ E_constructor {c with element = e'}
) )
| E_application {expr1;expr2} -> ( | E_application {lamb;args} -> (
let ab = (expr1,expr2) in let ab = (lamb,args) in
let%bind (a,b) = bind_map_pair self ab in let%bind (lamb,args) = bind_map_pair self ab in
return @@ E_application {expr1=a;expr2=b} return @@ E_application {lamb;args}
) )
| E_let_in { let_binder ; mut; rhs ; let_result; inline } -> ( | E_let_in { let_binder ; mut; rhs ; let_result; inline } -> (
let%bind rhs = self rhs in let%bind rhs = self rhs in
@ -167,6 +172,10 @@ let rec map_expression : exp_mapper -> expression -> expression result = fun f e
let%bind args = bind_map_list self c.arguments in let%bind args = bind_map_list self c.arguments in
return @@ E_constant {c with arguments=args} return @@ E_constant {c with arguments=args}
) )
| E_sequence {expr1;expr2} -> (
let%bind (expr1,expr2) = bind_map_pair self (expr1,expr2) in
return @@ E_sequence {expr1;expr2}
)
| E_literal _ | E_variable _ | E_skip as e' -> return e' | E_literal _ | E_variable _ | E_skip as e' -> return e'
and map_type_expression : ty_exp_mapper -> type_expression -> type_expression result = fun f te -> and map_type_expression : ty_exp_mapper -> type_expression -> type_expression result = fun f te ->
@ -288,10 +297,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
let%bind (res,e') = self init' c.element in let%bind (res,e') = self init' c.element in
ok (res, return @@ E_constructor {c with element = e'}) ok (res, return @@ E_constructor {c with element = e'})
) )
| E_application {expr1;expr2} -> ( | E_application {lamb;args} -> (
let ab = (expr1,expr2) in let ab = (lamb,args) in
let%bind (res,(a,b)) = bind_fold_map_pair self init' ab in let%bind (res,(a,b)) = bind_fold_map_pair self init' ab in
ok (res, return @@ E_application {expr1=a;expr2=b}) ok (res, return @@ E_application {lamb=a;args=b})
) )
| E_let_in { let_binder ; mut; rhs ; let_result; inline } -> ( | E_let_in { let_binder ; mut; rhs ; let_result; inline } -> (
let%bind (res,rhs) = self init' rhs in let%bind (res,rhs) = self init' rhs in
@ -310,6 +319,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
let%bind (res,args) = bind_fold_map_list self init' c.arguments in let%bind (res,args) = bind_fold_map_list self init' c.arguments in
ok (res, return @@ E_constant {c with arguments=args}) ok (res, return @@ E_constant {c with arguments=args})
) )
| E_sequence {expr1;expr2} -> (
let%bind (res,(expr1,expr2)) = bind_fold_map_pair self init' (expr1,expr2) in
ok (res, return @@ E_sequence {expr1;expr2})
)
| E_literal _ | E_variable _ | E_skip as e' -> ok (init', return e') | E_literal _ | E_variable _ | E_skip as e' -> ok (init', return e')
and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m -> and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m ->

View File

@ -68,10 +68,10 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind arguments = bind_map_list compile_expression arguments in let%bind arguments = bind_map_list compile_expression arguments in
return @@ O.E_constant {cons_name;arguments} return @@ O.E_constant {cons_name;arguments}
| I.E_variable name -> return @@ O.E_variable name | I.E_variable name -> return @@ O.E_variable name
| I.E_application {expr1;expr2} -> | I.E_application {lamb;args} ->
let%bind expr1 = compile_expression expr1 in let%bind lamb = compile_expression lamb in
let%bind expr2 = compile_expression expr2 in let%bind args = compile_expression args in
return @@ O.E_application {expr1; expr2} return @@ O.E_application {lamb;args}
| I.E_lambda lambda -> | I.E_lambda lambda ->
let%bind lambda = compile_lambda lambda in let%bind lambda = compile_lambda lambda in
return @@ O.E_lambda lambda return @@ O.E_lambda lambda
@ -85,7 +85,6 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind rhs = compile_expression rhs in let%bind rhs = compile_expression rhs in
let%bind let_result = compile_expression let_result in let%bind let_result = compile_expression let_result in
return @@ O.E_let_in {let_binder=(binder,ty_opt);inline;rhs;let_result} return @@ O.E_let_in {let_binder=(binder,ty_opt);inline;rhs;let_result}
| I.E_skip -> return @@ O.E_skip
| I.E_constructor {constructor;element} -> | I.E_constructor {constructor;element} ->
let%bind element = compile_expression element in let%bind element = compile_expression element in
return @@ O.E_constructor {constructor;element} return @@ O.E_constructor {constructor;element}
@ -134,6 +133,11 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind anno_expr = compile_expression anno_expr in let%bind anno_expr = compile_expression anno_expr in
let%bind type_annotation = compile_type_expression type_annotation in let%bind type_annotation = compile_type_expression type_annotation in
return @@ O.E_ascription {anno_expr; type_annotation} return @@ O.E_ascription {anno_expr; type_annotation}
| I.E_sequence {expr1; expr2} ->
let%bind expr1 = compile_expression expr1 in
let%bind expr2 = compile_expression expr2 in
return @@ O.E_sequence {expr1; expr2}
| I.E_skip -> return @@ O.E_skip
and compile_lambda : I.lambda -> O.lambda result = and compile_lambda : I.lambda -> O.lambda result =
fun {binder;input_type;output_type;result}-> fun {binder;input_type;output_type;result}->
let%bind input_type = bind_map_option compile_type_expression input_type in let%bind input_type = bind_map_option compile_type_expression input_type in
@ -252,10 +256,10 @@ let rec uncompile_expression : O.expression -> I.expression result =
let%bind arguments = bind_map_list uncompile_expression arguments in let%bind arguments = bind_map_list uncompile_expression arguments in
return @@ I.E_constant {cons_name;arguments} return @@ I.E_constant {cons_name;arguments}
| O.E_variable name -> return @@ I.E_variable name | O.E_variable name -> return @@ I.E_variable name
| O.E_application {expr1;expr2} -> | O.E_application {lamb; args} ->
let%bind expr1 = uncompile_expression expr1 in let%bind lamb = uncompile_expression lamb in
let%bind expr2 = uncompile_expression expr2 in let%bind args = uncompile_expression args in
return @@ I.E_application {expr1; expr2} return @@ I.E_application {lamb; args}
| O.E_lambda lambda -> | O.E_lambda lambda ->
let%bind lambda = uncompile_lambda lambda in let%bind lambda = uncompile_lambda lambda in
return @@ I.E_lambda lambda return @@ I.E_lambda lambda
@ -269,7 +273,6 @@ let rec uncompile_expression : O.expression -> I.expression result =
let%bind rhs = uncompile_expression rhs in let%bind rhs = uncompile_expression rhs in
let%bind let_result = uncompile_expression let_result in let%bind let_result = uncompile_expression let_result in
return @@ I.E_let_in {let_binder=(binder,ty_opt);mut=false;inline;rhs;let_result} return @@ I.E_let_in {let_binder=(binder,ty_opt);mut=false;inline;rhs;let_result}
| O.E_skip -> return @@ I.E_skip
| O.E_constructor {constructor;element} -> | O.E_constructor {constructor;element} ->
let%bind element = uncompile_expression element in let%bind element = uncompile_expression element in
return @@ I.E_constructor {constructor;element} return @@ I.E_constructor {constructor;element}
@ -318,6 +321,11 @@ let rec uncompile_expression : O.expression -> I.expression result =
let%bind anno_expr = uncompile_expression anno_expr in let%bind anno_expr = uncompile_expression anno_expr in
let%bind type_annotation = uncompile_type_expression type_annotation in let%bind type_annotation = uncompile_type_expression type_annotation in
return @@ I.E_ascription {anno_expr; type_annotation} return @@ I.E_ascription {anno_expr; type_annotation}
| O.E_sequence {expr1; expr2} ->
let%bind expr1 = uncompile_expression expr1 in
let%bind expr2 = uncompile_expression expr2 in
return @@ I.E_sequence {expr1; expr2}
| O.E_skip -> return @@ I.E_skip
and uncompile_lambda : O.lambda -> I.lambda result = and uncompile_lambda : O.lambda -> I.lambda result =
fun {binder;input_type;output_type;result}-> fun {binder;input_type;output_type;result}->

View File

@ -68,10 +68,10 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind arguments = bind_map_list compile_expression arguments in let%bind arguments = bind_map_list compile_expression arguments in
return @@ O.E_constant {cons_name;arguments} return @@ O.E_constant {cons_name;arguments}
| I.E_variable name -> return @@ O.E_variable name | I.E_variable name -> return @@ O.E_variable name
| I.E_application {expr1;expr2} -> | I.E_application {lamb;args} ->
let%bind expr1 = compile_expression expr1 in let%bind lamb = compile_expression lamb in
let%bind expr2 = compile_expression expr2 in let%bind args = compile_expression args in
return @@ O.E_application {expr1; expr2} return @@ O.E_application {lamb; args}
| I.E_lambda lambda -> | I.E_lambda lambda ->
let%bind lambda = compile_lambda lambda in let%bind lambda = compile_lambda lambda in
return @@ O.E_lambda lambda return @@ O.E_lambda lambda
@ -85,7 +85,6 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind rhs = compile_expression rhs in let%bind rhs = compile_expression rhs in
let%bind let_result = compile_expression let_result in let%bind let_result = compile_expression let_result in
return @@ O.E_let_in {let_binder=(binder,ty_opt);inline;rhs;let_result} return @@ O.E_let_in {let_binder=(binder,ty_opt);inline;rhs;let_result}
| I.E_skip -> ok @@ O.e_unit ~loc:e.location ()
| I.E_constructor {constructor;element} -> | I.E_constructor {constructor;element} ->
let%bind element = compile_expression element in let%bind element = compile_expression element in
return @@ O.E_constructor {constructor;element} return @@ O.E_constructor {constructor;element}
@ -134,6 +133,11 @@ let rec compile_expression : I.expression -> O.expression result =
let%bind anno_expr = compile_expression anno_expr in let%bind anno_expr = compile_expression anno_expr in
let%bind type_annotation = idle_type_expression type_annotation in let%bind type_annotation = idle_type_expression type_annotation in
return @@ O.E_ascription {anno_expr; type_annotation} return @@ O.E_ascription {anno_expr; type_annotation}
| I.E_sequence {expr1; expr2} ->
let%bind expr1 = compile_expression expr1 in
let%bind expr2 = compile_expression expr2 in
return @@ O.E_let_in {let_binder=(Var.of_name "_", Some O.t_unit); rhs=expr1;let_result=expr2; inline=false}
| I.E_skip -> ok @@ O.e_unit ~loc:e.location ()
and compile_lambda : I.lambda -> O.lambda result = and compile_lambda : I.lambda -> O.lambda result =
fun {binder;input_type;output_type;result}-> fun {binder;input_type;output_type;result}->
@ -253,10 +257,10 @@ let rec uncompile_expression : O.expression -> I.expression result =
let%bind arguments = bind_map_list uncompile_expression arguments in let%bind arguments = bind_map_list uncompile_expression arguments in
return @@ I.E_constant {cons_name;arguments} return @@ I.E_constant {cons_name;arguments}
| O.E_variable name -> return @@ I.E_variable name | O.E_variable name -> return @@ I.E_variable name
| O.E_application {expr1;expr2} -> | O.E_application {lamb; args} ->
let%bind expr1 = uncompile_expression expr1 in let%bind lamb = uncompile_expression lamb in
let%bind expr2 = uncompile_expression expr2 in let%bind args = uncompile_expression args in
return @@ I.E_application {expr1; expr2} return @@ I.E_application {lamb; args}
| O.E_lambda lambda -> | O.E_lambda lambda ->
let%bind lambda = uncompile_lambda lambda in let%bind lambda = uncompile_lambda lambda in
return @@ I.E_lambda lambda return @@ I.E_lambda lambda
@ -264,6 +268,10 @@ let rec uncompile_expression : O.expression -> I.expression result =
let%bind fun_type = uncompile_type_expression fun_type in let%bind fun_type = uncompile_type_expression fun_type in
let%bind lambda = uncompile_lambda lambda in let%bind lambda = uncompile_lambda lambda in
return @@ I.E_recursive {fun_name;fun_type;lambda} return @@ I.E_recursive {fun_name;fun_type;lambda}
| O.E_let_in {let_binder;inline=false;rhs=expr1;let_result=expr2} when let_binder = (Var.of_name "_", Some O.t_unit) ->
let%bind expr1 = uncompile_expression expr1 in
let%bind expr2 = uncompile_expression expr2 in
return @@ I.E_sequence {expr1;expr2}
| O.E_let_in {let_binder;inline;rhs;let_result} -> | O.E_let_in {let_binder;inline;rhs;let_result} ->
let (binder,ty_opt) = let_binder in let (binder,ty_opt) = let_binder in
let%bind ty_opt = bind_map_option uncompile_type_expression ty_opt in let%bind ty_opt = bind_map_option uncompile_type_expression ty_opt in

View File

@ -679,11 +679,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
* let%bind (name', tv) = * let%bind (name', tv) =
* type_constant name tv_lst tv_opt ae.location in * type_constant name tv_lst tv_opt ae.location in
* return (E_constant (name' , lst')) tv *) * return (E_constant (name' , lst')) tv *)
| E_application {expr1;expr2} -> | E_application {lamb;args} ->
let%bind (f' , state') = type_expression e state expr1 in let%bind (f' , state') = type_expression e state lamb in
let%bind (arg , state'') = type_expression e state' expr2 in let%bind (args , state'') = type_expression e state' args in
let wrapped = Wrap.application f'.type_expression arg.type_expression in let wrapped = Wrap.application f'.type_expression args.type_expression in
return_wrapped (E_application {expr1=f';expr2=arg}) state'' wrapped return_wrapped (E_application {lamb=f';args}) state'' wrapped
(* | E_look_up dsi -> (* | E_look_up dsi ->
* let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in * let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
@ -1037,9 +1037,9 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
return (e_constant cons_name lst') return (e_constant cons_name lst')
| E_variable (n) -> | E_variable (n) ->
return (e_variable (n)) return (e_variable (n))
| E_application {expr1;expr2} -> | E_application {lamb;args} ->
let%bind f' = untype_expression expr1 in let%bind f' = untype_expression lamb in
let%bind arg' = untype_expression expr2 in let%bind arg' = untype_expression args in
return (e_application f' arg') return (e_application f' arg')
| E_lambda lambda -> | E_lambda lambda ->
let%bind lambda = untype_lambda e.type_expression lambda in let%bind lambda = untype_lambda e.type_expression lambda in

View File

@ -688,21 +688,21 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
let%bind (name', tv) = let%bind (name', tv) =
type_constant cons_name tv_lst tv_opt in type_constant cons_name tv_lst tv_opt in
return (E_constant {cons_name=name';arguments=lst'}) tv return (E_constant {cons_name=name';arguments=lst'}) tv
| E_application {expr1;expr2} -> | E_application {lamb; args} ->
let%bind expr1' = type_expression' e expr1 in let%bind lamb' = type_expression' e lamb in
let%bind expr2 = type_expression' e expr2 in let%bind args' = type_expression' e args in
let%bind tv = match expr1'.type_expression.type_content with let%bind tv = match lamb'.type_expression.type_content with
| T_arrow {type1;type2} -> | T_arrow {type1;type2} ->
let%bind _ = O.assert_type_expression_eq (type1, expr2.type_expression) in let%bind _ = O.assert_type_expression_eq (type1, args'.type_expression) in
ok type2 ok type2
| _ -> | _ ->
fail @@ type_error_approximate fail @@ type_error_approximate
~expected:"should be a function type" ~expected:"should be a function type"
~expression:expr1 ~expression:lamb
~actual:expr1'.type_expression ~actual:lamb'.type_expression
expr1'.location lamb'.location
in in
return (E_application {expr1=expr1';expr2}) tv return (E_application {lamb=lamb'; args=args'}) tv
| E_look_up dsi -> | E_look_up dsi ->
let%bind (ds, ind) = bind_map_pair (type_expression' e) dsi in 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_expression in let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_expression in
@ -841,9 +841,9 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
return (e_constant cons_name lst') return (e_constant cons_name lst')
| E_variable n -> | E_variable n ->
return (e_variable (n)) return (e_variable (n))
| E_application {expr1;expr2} -> | E_application {lamb;args} ->
let%bind f' = untype_expression expr1 in let%bind f' = untype_expression lamb in
let%bind arg' = untype_expression expr2 in let%bind arg' = untype_expression args in
return (e_application f' arg') return (e_application f' arg')
| E_lambda {binder ; result} -> ( | E_lambda {binder ; result} -> (
let%bind io = get_t_function ty in let%bind io = get_t_function ty in

View File

@ -19,8 +19,8 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
| E_look_up ab -> | E_look_up ab ->
let%bind res = bind_fold_pair self init' ab in let%bind res = bind_fold_pair self init' ab in
ok res ok res
| E_application {expr1;expr2} -> ( | E_application {lamb; args} -> (
let ab = (expr1,expr2) in let ab = (lamb, args) in
let%bind res = bind_fold_pair self init' ab in let%bind res = bind_fold_pair self init' ab in
ok res ok res
) )
@ -135,10 +135,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
let%bind e' = self c.element in let%bind e' = self c.element in
return @@ E_constructor {c with element = e'} return @@ E_constructor {c with element = e'}
) )
| E_application {expr1;expr2} -> ( | E_application {lamb; args} -> (
let ab = (expr1,expr2) in let ab = (lamb, args) in
let%bind (a,b) = bind_map_pair self ab in let%bind (a,b) = bind_map_pair self ab in
return @@ E_application {expr1=a;expr2=b} return @@ E_application {lamb=a;args=b}
) )
| E_let_in { let_binder ; rhs ; let_result; inline } -> ( | E_let_in { let_binder ; rhs ; let_result; inline } -> (
let%bind rhs = self rhs in let%bind rhs = self rhs in
@ -251,10 +251,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
let%bind (res,e') = self init' c.element in let%bind (res,e') = self init' c.element in
ok (res, return @@ E_constructor {c with element = e'}) ok (res, return @@ E_constructor {c with element = e'})
) )
| E_application {expr1;expr2} -> ( | E_application {lamb;args} -> (
let ab = (expr1,expr2) in let ab = (lamb, args) in
let%bind (res,(a,b)) = bind_fold_map_pair self init' ab in let%bind (res,(a,b)) = bind_fold_map_pair self init' ab in
ok (res, return @@ E_application {expr1=a;expr2=b}) ok (res, return @@ E_application {lamb=a;args=b})
) )
| E_let_in { let_binder ; rhs ; let_result; inline } -> ( | E_let_in { let_binder ; rhs ; let_result; inline } -> (
let%bind (res,rhs) = self init' rhs in let%bind (res,rhs) = self init' rhs in

View File

@ -24,9 +24,9 @@ let rec check_recursive_call : expression_variable -> bool -> expression -> unit
Assert.assert_true (final_path || n <> v) in Assert.assert_true (final_path || n <> v) in
ok () ok ()
) )
| E_application {expr1;expr2} -> | E_application {lamb;args} ->
let%bind _ = check_recursive_call n final_path expr1 in let%bind _ = check_recursive_call n final_path lamb in
let%bind _ = check_recursive_call n false expr2 in let%bind _ = check_recursive_call n false args in
ok () ok ()
| E_lambda {result;_} -> | E_lambda {result;_} ->
let%bind _ = check_recursive_call n final_path result in let%bind _ = check_recursive_call n final_path result in

View File

@ -18,8 +18,8 @@ and expression_content ppf (ec : expression_content) =
literal ppf l literal ppf l
| E_variable n -> | E_variable n ->
fprintf ppf "%a" expression_variable n fprintf ppf "%a" expression_variable n
| E_application app -> | E_application {lamb;args} ->
fprintf ppf "(%a)@(%a)" expression app.expr1 expression app.expr2 fprintf ppf "(%a)@(%a)" expression lamb expression args
| E_constructor c -> | E_constructor c ->
fprintf ppf "%a(%a)" constructor c.constructor expression c.element fprintf ppf "%a(%a)" constructor c.constructor expression c.element
| E_constant c -> | E_constant c ->
@ -59,11 +59,13 @@ and expression_content ppf (ec : expression_content) =
expression_content (E_lambda lambda) expression_content (E_lambda lambda)
| E_let_in { let_binder ; mut; rhs ; let_result; inline } -> | E_let_in { let_binder ; mut; rhs ; let_result; inline } ->
fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result
| E_skip ->
fprintf ppf "skip"
| E_ascription {anno_expr; type_annotation} -> | E_ascription {anno_expr; type_annotation} ->
fprintf ppf "%a : %a" expression anno_expr type_expression fprintf ppf "%a : %a" expression anno_expr type_expression
type_annotation type_annotation
| E_sequence {expr1;expr2} ->
fprintf ppf "%a;\n%a" expression expr1 expression expr2
| E_skip ->
fprintf ppf "skip"
and option_type_name ppf and option_type_name ppf
((n, ty_opt) : expression_variable * type_expression option) = ((n, ty_opt) : expression_variable * type_expression option) =

View File

@ -125,11 +125,11 @@ let e_skip ?loc () = make_expr ?loc @@ E_skip
let e_let_in ?loc (binder, ascr) mut inline rhs let_result = let e_let_in ?loc (binder, ascr) mut inline rhs let_result =
make_expr ?loc @@ E_let_in { let_binder = (binder, ascr) ; mut; rhs ; let_result; inline } make_expr ?loc @@ E_let_in { let_binder = (binder, ascr) ; mut; rhs ; let_result; inline }
let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty} let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty}
let e_application ?loc a b = make_expr ?loc @@ E_application {expr1=a ; expr2=b} let e_application ?loc a b = make_expr ?loc @@ E_application {lamb=a ; args=b}
let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]} let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]}
let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst} let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst}
let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y) let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y)
let e_sequence ?loc expr1 expr2 = e_let_in ?loc (Var.fresh (), Some t_unit) false false expr1 expr2 let e_sequence ?loc expr1 expr2 = make_expr ?loc @@ E_sequence {expr1; expr2}
let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false}) let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false})
(* (*
let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*) let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*)

View File

@ -184,7 +184,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
| (E_application _, _) | (E_let_in _, _) | (E_application _, _) | (E_let_in _, _)
| (E_recursive _,_) | (E_record_accessor _, _) | (E_recursive _,_) | (E_record_accessor _, _)
| (E_look_up _, _) | (E_matching _, _) | (E_look_up _, _) | (E_matching _, _)
| (E_skip, _) -> simple_fail "comparing not a value" | (E_sequence _, _) | (E_skip, _) -> simple_fail "comparing not a value"
let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b) let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)

View File

@ -36,7 +36,6 @@ and expression_content =
| E_lambda of lambda | E_lambda of lambda
| E_recursive of recursive | E_recursive of recursive
| E_let_in of let_in | E_let_in of let_in
| E_skip
(* Variant *) (* Variant *)
| E_constructor of constructor (* For user defined constructors *) | E_constructor of constructor (* For user defined constructors *)
| E_matching of matching | E_matching of matching
@ -44,21 +43,26 @@ and expression_content =
| E_record of expression label_map | E_record of expression label_map
| E_record_accessor of accessor | E_record_accessor of accessor
| E_record_update of update | E_record_update of update
(* Advanced *)
| E_ascription of ascription
(* Sugar *)
| E_sequence of sequence
| E_skip
(* Data Structures *) (* Data Structures *)
(* TODO : move to constant*) | E_map of (expression * expression) list
| E_map of (expression * expression) list (*move to operator *) | E_big_map of (expression * expression) list
| E_big_map of (expression * expression) list (*move to operator *)
| E_list of expression list | E_list of expression list
| E_set of expression list | E_set of expression list
| E_look_up of (expression * expression) | E_look_up of (expression * expression)
(* Advanced *)
| E_ascription of ascription
and constant = and constant =
{ cons_name: constant' (* this is at the end because it is huge *) { cons_name: constant' (* this is at the end because it is huge *)
; arguments: expression list } ; arguments: expression list }
and application = {expr1: expression; expr2: expression} and application = {
lamb: expression ;
args: expression ;
}
and lambda = and lambda =
{ binder: expression_variable { binder: expression_variable
@ -92,6 +96,10 @@ and matching =
} }
and ascription = {anno_expr: expression; type_annotation: type_expression} and ascription = {anno_expr: expression; type_annotation: type_expression}
and sequence = {
expr1: expression ;
expr2: expression ;
}
and environment_element_definition = and environment_element_definition =
| ED_binder | ED_binder

View File

@ -18,8 +18,8 @@ and expression_content ppf (ec : expression_content) =
literal ppf l literal ppf l
| E_variable n -> | E_variable n ->
fprintf ppf "%a" expression_variable n fprintf ppf "%a" expression_variable n
| E_application app -> | E_application {lamb;args} ->
fprintf ppf "(%a)@(%a)" expression app.expr1 expression app.expr2 fprintf ppf "(%a)@(%a)" expression lamb expression args
| E_constructor c -> | E_constructor c ->
fprintf ppf "%a(%a)" constructor c.constructor expression c.element fprintf ppf "%a(%a)" constructor c.constructor expression c.element
| E_constant c -> | E_constant c ->
@ -58,11 +58,12 @@ and expression_content ppf (ec : expression_content) =
cases cases
| E_let_in { let_binder ; rhs ; let_result; inline } -> | E_let_in { let_binder ; rhs ; let_result; inline } ->
fprintf ppf "let %a = %a%a in %a" option_type_name let_binder expression rhs option_inline inline expression let_result fprintf ppf "let %a = %a%a in %a" option_type_name let_binder expression rhs option_inline inline expression let_result
| E_sequence {expr1;expr2} ->
fprintf ppf "%a;\n%a" expression expr1 expression expr2
| E_ascription {anno_expr; type_annotation} ->
fprintf ppf "%a : %a" expression anno_expr type_expression type_annotation
| E_skip -> | E_skip ->
fprintf ppf "skip" fprintf ppf "skip"
| E_ascription {anno_expr; type_annotation} ->
fprintf ppf "%a : %a" expression anno_expr type_expression
type_annotation
and option_type_name ppf and option_type_name ppf
((n, ty_opt) : expression_variable * type_expression option) = ((n, ty_opt) : expression_variable * type_expression option) =

View File

@ -125,11 +125,11 @@ let e_skip ?loc () = make_expr ?loc @@ E_skip
let e_let_in ?loc (binder, ascr) inline rhs let_result = let e_let_in ?loc (binder, ascr) inline rhs let_result =
make_expr ?loc @@ E_let_in { let_binder = (binder, ascr) ; rhs ; let_result; inline } make_expr ?loc @@ E_let_in { let_binder = (binder, ascr) ; rhs ; let_result; inline }
let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty} let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty}
let e_application ?loc a b = make_expr ?loc @@ E_application {expr1=a ; expr2=b} let e_application ?loc a b = make_expr ?loc @@ E_application {lamb=a ; args=b}
let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]} let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]}
let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst} let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst}
let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y) let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y)
let e_sequence ?loc expr1 expr2 = e_let_in ?loc (Var.fresh (), Some t_unit) false expr1 expr2 let e_sequence ?loc expr1 expr2 = make_expr ?loc @@ E_sequence {expr1; expr2}
let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false}) let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false})
(* (*
let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*) let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*)

View File

@ -184,7 +184,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
| (E_application _, _) | (E_let_in _, _) | (E_application _, _) | (E_let_in _, _)
| (E_recursive _,_) | (E_record_accessor _, _) | (E_recursive _,_) | (E_record_accessor _, _)
| (E_look_up _, _) | (E_matching _, _) | (E_look_up _, _) | (E_matching _, _)
| (E_skip, _) -> simple_fail "comparing not a value" | (E_sequence _, _) | (E_skip, _) -> simple_fail "comparing not a value"
let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b) let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)

View File

@ -36,7 +36,6 @@ and expression_content =
| E_lambda of lambda | E_lambda of lambda
| E_recursive of recursive | E_recursive of recursive
| E_let_in of let_in | E_let_in of let_in
| E_skip
(* Variant *) (* Variant *)
| E_constructor of constructor (* For user defined constructors *) | E_constructor of constructor (* For user defined constructors *)
| E_matching of matching | E_matching of matching
@ -44,21 +43,26 @@ and expression_content =
| E_record of expression label_map | E_record of expression label_map
| E_record_accessor of accessor | E_record_accessor of accessor
| E_record_update of update | E_record_update of update
(* Advanced *)
| E_ascription of ascription
(* Sugar *)
| E_sequence of sequence
| E_skip
(* Data Structures *) (* Data Structures *)
(* TODO : move to constant*) | E_map of (expression * expression) list
| E_map of (expression * expression) list (*move to operator *) | E_big_map of (expression * expression) list
| E_big_map of (expression * expression) list (*move to operator *)
| E_list of expression list | E_list of expression list
| E_set of expression list | E_set of expression list
| E_look_up of (expression * expression) | E_look_up of (expression * expression)
(* Advanced *)
| E_ascription of ascription
and constant = and constant =
{ cons_name: constant' (* this is at the end because it is huge *) { cons_name: constant' (* this is at the end because it is huge *)
; arguments: expression list } ; arguments: expression list }
and application = {expr1: expression; expr2: expression} and application = {
lamb: expression ;
args: expression ;
}
and lambda = and lambda =
{ binder: expression_variable { binder: expression_variable
@ -91,6 +95,10 @@ and matching =
} }
and ascription = {anno_expr: expression; type_annotation: type_expression} and ascription = {anno_expr: expression; type_annotation: type_expression}
and sequence = {
expr1: expression ;
expr2: expression ;
}
and environment_element_definition = and environment_element_definition =
| ED_binder | ED_binder

View File

@ -18,8 +18,8 @@ and expression_content ppf (ec : expression_content) =
literal ppf l literal ppf l
| E_variable n -> | E_variable n ->
fprintf ppf "%a" expression_variable n fprintf ppf "%a" expression_variable n
| E_application app -> | E_application {lamb;args} ->
fprintf ppf "(%a)@(%a)" expression app.expr1 expression app.expr2 fprintf ppf "(%a)@(%a)" expression lamb expression args
| E_constructor c -> | E_constructor c ->
fprintf ppf "%a(%a)" constructor c.constructor expression c.element fprintf ppf "%a(%a)" constructor c.constructor expression c.element
| E_constant c -> | E_constant c ->

View File

@ -124,11 +124,10 @@ let e_variable ?loc v = make_expr ?loc @@ E_variable v
let e_let_in ?loc (binder, ascr) inline rhs let_result = let e_let_in ?loc (binder, ascr) inline rhs let_result =
make_expr ?loc @@ E_let_in { let_binder = (binder,ascr) ; rhs ; let_result; inline } make_expr ?loc @@ E_let_in { let_binder = (binder,ascr) ; rhs ; let_result; inline }
let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty} let e_annotation ?loc anno_expr ty = make_expr ?loc @@ E_ascription {anno_expr; type_annotation = ty}
let e_application ?loc a b = make_expr ?loc @@ E_application {expr1=a ; expr2=b} let e_application ?loc a b = make_expr ?loc @@ E_application {lamb=a ; args=b}
let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]} let e_binop ?loc name a b = make_expr ?loc @@ E_constant {cons_name = name ; arguments = [a ; b]}
let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst} let e_constant ?loc name lst = make_expr ?loc @@ E_constant {cons_name=name ; arguments = lst}
let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y) let e_look_up ?loc x y = make_expr ?loc @@ E_look_up (x , y)
let e_sequence ?loc expr1 expr2 = e_let_in ?loc (Var.fresh (), Some t_unit) false expr1 expr2
let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false}) let e_cond ?loc expr match_true match_false = e_matching expr ?loc (Match_bool {match_true; match_false})
(* (*
let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*) let e_assign ?loc a b c = location_wrap ?loc @@ E_assign (Var.of_name a , b , c) (* TODO handlethat*)

View File

@ -83,7 +83,6 @@ val e_matching_bool : ?loc:Location.t -> expression -> expression -> expression
val e_accessor : ?loc:Location.t -> expression -> string -> expression val e_accessor : ?loc:Location.t -> expression -> string -> expression
val e_accessor_list : ?loc:Location.t -> expression -> string list -> expression val e_accessor_list : ?loc:Location.t -> expression -> string list -> expression
val e_variable : ?loc:Location.t -> expression_variable -> expression val e_variable : ?loc:Location.t -> expression_variable -> expression
val e_sequence : ?loc:Location.t -> expression -> expression -> expression
val e_cond: ?loc:Location.t -> expression -> expression -> expression -> expression val e_cond: ?loc:Location.t -> expression -> expression -> expression -> expression
val e_let_in : ?loc:Location.t -> ( expression_variable * type_expression option ) -> bool -> expression -> expression -> expression val e_let_in : ?loc:Location.t -> ( expression_variable * type_expression option ) -> bool -> expression -> expression -> expression
val e_annotation : ?loc:Location.t -> expression -> type_expression -> expression val e_annotation : ?loc:Location.t -> expression -> type_expression -> expression

View File

@ -57,7 +57,10 @@ and constant =
{ cons_name: constant' (* this is at the end because it is huge *) { cons_name: constant' (* this is at the end because it is huge *)
; arguments: expression list } ; arguments: expression list }
and application = {expr1: expression; expr2: expression} and application = {
lamb: expression ;
args: expression ;
}
and lambda = and lambda =
{ binder: expression_variable { binder: expression_variable

View File

@ -19,8 +19,8 @@ and expression_content ppf (ec: expression_content) =
literal ppf l literal ppf l
| E_variable n -> | E_variable n ->
fprintf ppf "%a" expression_variable n fprintf ppf "%a" expression_variable n
| E_application app -> | E_application {lamb;args} ->
fprintf ppf "(%a)@(%a)" expression app.expr1 expression app.expr2 fprintf ppf "(%a)@(%a)" expression lamb expression args
| E_constructor c -> | E_constructor c ->
fprintf ppf "%a(%a)" constructor c.constructor expression c.element fprintf ppf "%a(%a)" constructor c.constructor expression c.element
| E_constant c -> | E_constant c ->

View File

@ -294,7 +294,7 @@ let e_chain_id s : expression_content = E_literal (Literal_chain_id s)
let e_operation s : expression_content = E_literal (Literal_operation s) let e_operation s : expression_content = E_literal (Literal_operation s)
let e_lambda l : expression_content = E_lambda l let e_lambda l : expression_content = E_lambda l
let e_pair a b : expression_content = ez_e_record [(Label "0",a);(Label "1", b)] let e_pair a b : expression_content = ez_e_record [(Label "0",a);(Label "1", b)]
let e_application expr1 expr2 : expression_content = E_application {expr1;expr2} let e_application lamb args : expression_content = E_application {lamb;args}
let e_variable v : expression_content = E_variable v let e_variable v : expression_content = E_variable v
let e_list lst : expression_content = E_list lst let e_list lst : expression_content = E_list lst
let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; let_result; inline } let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; let_result; inline }

View File

@ -206,7 +206,7 @@ module Free_variables = struct
| true -> empty | true -> empty
| false -> singleton name | false -> singleton name
) )
| E_application {expr1;expr2} -> unions @@ List.map self [ expr1 ; expr2 ] | E_application {lamb;args} -> unions @@ List.map self [ lamb ; args ]
| E_constructor {element;_} -> self element | E_constructor {element;_} -> self element
| E_record m -> unions @@ List.map self @@ LMap.to_list m | E_record m -> unions @@ List.map self @@ LMap.to_list m
| E_record_accessor {expr;_} -> self expr | E_record_accessor {expr;_} -> self expr

View File

@ -63,8 +63,8 @@ module Captured_variables = struct
| ED_binder -> ok empty | ED_binder -> ok empty
| ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo" | ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
) )
| E_application {expr1;expr2} -> | E_application {lamb;args} ->
let%bind lst' = bind_map_list self [ expr1 ; expr2 ] in let%bind lst' = bind_map_list self [ lamb ; args ] in
ok @@ unions lst' ok @@ unions lst'
| E_constructor {element;_} -> self element | E_constructor {element;_} -> self element
| E_record m -> | E_record m ->

View File

@ -61,7 +61,10 @@ and constant =
{ cons_name: constant' { cons_name: constant'
; arguments: expression list } ; arguments: expression list }
and application = {expr1: expression; expr2: expression} and application = {
lamb: expression ;
args: expression ;
}
and lambda = { and lambda = {
binder: expression_variable ; binder: expression_variable ;

View File

@ -151,10 +151,10 @@ module Substitution = struct
| T.E_variable tv -> | T.E_variable tv ->
let%bind tv = s_variable ~substs tv in let%bind tv = s_variable ~substs tv in
ok @@ T.E_variable tv ok @@ T.E_variable tv
| T.E_application {expr1;expr2} -> | T.E_application {lamb;args} ->
let%bind expr1 = s_expression ~substs expr1 in let%bind lamb = s_expression ~substs lamb in
let%bind expr2 = s_expression ~substs expr2 in let%bind args = s_expression ~substs args in
ok @@ T.E_application {expr1;expr2} ok @@ T.E_application {lamb;args}
| T.E_lambda { binder; result } -> | T.E_lambda { binder; result } ->
let%bind binder = s_variable ~substs binder in let%bind binder = s_variable ~substs binder in
let%bind result = s_expression ~substs result in let%bind result = s_expression ~substs result in