WIP: adding E_recursive in ast
This commit is contained in:
parent
734620a179
commit
b2f0e8bbc4
@ -56,6 +56,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
|
|||||||
let%bind res = self res let_result in
|
let%bind res = self res let_result in
|
||||||
ok res
|
ok res
|
||||||
)
|
)
|
||||||
|
| E_recursive { lambda={result=e;_}; _} ->
|
||||||
|
let%bind res = self init' e 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
|
||||||
@ -156,6 +159,10 @@ let rec map_expression : exp_mapper -> expression -> expression result = fun f e
|
|||||||
let%bind result = self result in
|
let%bind result = self result in
|
||||||
return @@ E_lambda { binder ; input_type ; output_type ; result }
|
return @@ E_lambda { binder ; input_type ; output_type ; result }
|
||||||
)
|
)
|
||||||
|
| E_recursive { fun_name; fun_type; lambda} ->
|
||||||
|
let%bind result = self lambda.result in
|
||||||
|
let lambda = {lambda with result} in
|
||||||
|
return @@ E_recursive { fun_name; fun_type; lambda}
|
||||||
| E_constant c -> (
|
| E_constant c -> (
|
||||||
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}
|
||||||
@ -295,6 +302,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
|
|||||||
let%bind (res,result) = self init' result in
|
let%bind (res,result) = self init' result in
|
||||||
ok ( res, return @@ E_lambda { binder ; input_type ; output_type ; result })
|
ok ( res, return @@ E_lambda { binder ; input_type ; output_type ; result })
|
||||||
)
|
)
|
||||||
|
| E_recursive { fun_name; fun_type; lambda} ->
|
||||||
|
let%bind (res, result) = self init' lambda.result in
|
||||||
|
let lambda = {lambda with result} in
|
||||||
|
ok ( res, return @@ E_recursive { fun_name; fun_type; lambda})
|
||||||
| E_constant c -> (
|
| E_constant c -> (
|
||||||
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})
|
||||||
|
@ -291,6 +291,14 @@ module Wrap = struct
|
|||||||
C_equation (result' , P_variable whole_expr)
|
C_equation (result' , P_variable whole_expr)
|
||||||
] @ rhs_tv_opt', whole_expr
|
] @ rhs_tv_opt', whole_expr
|
||||||
|
|
||||||
|
let recursive : T.type_expression -> (constraints * T.type_variable) =
|
||||||
|
fun fun_type ->
|
||||||
|
let fun_type = type_expression_to_type_value fun_type in
|
||||||
|
let whole_expr = Core.fresh_type_variable () in
|
||||||
|
O.[
|
||||||
|
C_equation (fun_type, P_variable whole_expr)
|
||||||
|
], whole_expr
|
||||||
|
|
||||||
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
|
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
|
||||||
fun v e ->
|
fun v e ->
|
||||||
let v' = type_expression_to_type_value v in
|
let v' = type_expression_to_type_value v in
|
||||||
|
@ -797,26 +797,16 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
|
|||||||
(* | _ -> ( … ) *)
|
(* | _ -> ( … ) *)
|
||||||
|
|
||||||
|
|
||||||
| E_lambda {
|
| E_lambda lambda ->
|
||||||
binder ;
|
let%bind (lambda,state',wrapped) = type_lambda e state lambda in
|
||||||
input_type ;
|
return_wrapped (E_lambda lambda) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
|
||||||
output_type ;
|
|
||||||
result ;
|
|
||||||
} -> (
|
|
||||||
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 binder = fst binder in
|
|
||||||
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 = Wrap.lambda fresh input_type' output_type' in
|
|
||||||
return_wrapped
|
|
||||||
(E_lambda {binder = binder; result}) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
|
|
||||||
state' wrapped
|
state' wrapped
|
||||||
)
|
| E_recursive {fun_name;fun_type;lambda} ->
|
||||||
|
let%bind fun_type = evaluate_type e fun_type in
|
||||||
|
let e = Environment.add_ez_binder fun_name fun_type e in
|
||||||
|
let%bind (lambda,state,_) = type_lambda e state lambda in
|
||||||
|
let wrapped = Wrap.recursive fun_type in
|
||||||
|
return_wrapped (E_recursive {fun_name;fun_type;lambda}) state wrapped
|
||||||
|
|
||||||
| E_constant {cons_name=name; arguments=lst} ->
|
| E_constant {cons_name=name; arguments=lst} ->
|
||||||
let () = ignore (name , lst) in
|
let () = ignore (name , lst) in
|
||||||
@ -838,7 +828,22 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
|
|||||||
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
|
||||||
*)
|
*)
|
||||||
|
and type_lambda e state {
|
||||||
|
binder ;
|
||||||
|
input_type ;
|
||||||
|
output_type ;
|
||||||
|
result ;
|
||||||
|
} =
|
||||||
|
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 (Solver.Wrap.fresh_binder ()) () in
|
||||||
|
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
|
||||||
|
ok (({binder;result}:O.lambda),state',wrapped)
|
||||||
(* Advanced *)
|
(* Advanced *)
|
||||||
|
|
||||||
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
|
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
|
||||||
@ -1040,12 +1045,10 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
|
|||||||
let%bind f' = untype_expression expr1 in
|
let%bind f' = untype_expression expr1 in
|
||||||
let%bind arg' = untype_expression expr2 in
|
let%bind arg' = untype_expression expr2 in
|
||||||
return (e_application f' arg')
|
return (e_application f' arg')
|
||||||
| E_lambda {binder; result} -> (
|
| E_lambda lambda ->
|
||||||
let%bind io = get_t_function e.type_expression in
|
let%bind lambda = untype_lambda e.type_expression lambda in
|
||||||
let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
|
let {binder;input_type;output_type;result} = lambda in
|
||||||
let%bind result = untype_expression result in
|
return (e_lambda (binder) (input_type) (output_type) result)
|
||||||
return (e_lambda (binder) (Some input_type) (Some output_type) result)
|
|
||||||
)
|
|
||||||
| E_constructor {constructor; element} ->
|
| E_constructor {constructor; element} ->
|
||||||
let%bind p' = untype_expression element in
|
let%bind p' = untype_expression element in
|
||||||
let Constructor n = constructor in
|
let Constructor n = constructor in
|
||||||
@ -1092,6 +1095,16 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
|
|||||||
let%bind rhs = untype_expression rhs in
|
let%bind rhs = untype_expression rhs in
|
||||||
let%bind result = untype_expression let_result in
|
let%bind result = untype_expression let_result in
|
||||||
return (e_let_in (let_binder , (Some tv)) false inline rhs result)
|
return (e_let_in (let_binder , (Some tv)) false inline rhs result)
|
||||||
|
| E_recursive {fun_name; fun_type; lambda} ->
|
||||||
|
let%bind lambda = untype_lambda fun_type lambda in
|
||||||
|
let%bind fun_type = untype_type_expression fun_type in
|
||||||
|
return @@ e_recursive fun_name fun_type lambda
|
||||||
|
|
||||||
|
and untype_lambda ty {binder; result} : I.lambda result =
|
||||||
|
let%bind io = get_t_function ty in
|
||||||
|
let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
|
||||||
|
let%bind result = untype_expression result in
|
||||||
|
ok ({binder;input_type = Some input_type; output_type = Some output_type; result}: I.lambda)
|
||||||
|
|
||||||
(*
|
(*
|
||||||
Tranform a Ast_typed matching into an ast_simplified matching
|
Tranform a Ast_typed matching into an ast_simplified matching
|
||||||
|
@ -613,45 +613,12 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
|
|||||||
ok (t_big_map key_type value_type ())
|
ok (t_big_map key_type value_type ())
|
||||||
in
|
in
|
||||||
return (E_big_map lst') tv
|
return (E_big_map lst') tv
|
||||||
| E_lambda {
|
| E_lambda lambda ->
|
||||||
binder ;
|
let%bind (lambda, lambda_type) = type_lambda e lambda in
|
||||||
input_type ;
|
return (E_lambda lambda ) lambda_type
|
||||||
output_type ;
|
|
||||||
result ;
|
|
||||||
} -> (
|
|
||||||
let%bind input_type =
|
|
||||||
let%bind input_type =
|
|
||||||
(* Hack to take care of let_in introduced by `simplify/cameligo.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_content with
|
|
||||||
| I.E_let_in li -> (
|
|
||||||
match li.rhs.expression_content with
|
|
||||||
| I.E_variable name when name = (fst binder) -> (
|
|
||||||
match snd li.let_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 binder = fst binder in
|
|
||||||
let e' = Environment.add_ez_binder binder input_type e in
|
|
||||||
let%bind body = type_expression' ?tv_opt:output_type e' result in
|
|
||||||
let output_type = body.type_expression in
|
|
||||||
return (E_lambda {binder; result=body}) (t_function input_type output_type ())
|
|
||||||
)
|
|
||||||
| E_constant {cons_name=( C_LIST_FOLD | C_MAP_FOLD | C_SET_FOLD) as opname ;
|
| E_constant {cons_name=( C_LIST_FOLD | C_MAP_FOLD | C_SET_FOLD) as opname ;
|
||||||
arguments=[
|
arguments=[
|
||||||
( { expression_content = (I.E_lambda { binder = (lname, None) ;
|
( { expression_content = (I.E_lambda { binder = lname ;
|
||||||
input_type = None ;
|
input_type = None ;
|
||||||
output_type = None ;
|
output_type = None ;
|
||||||
result }) ;
|
result }) ;
|
||||||
@ -683,7 +650,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
|
|||||||
return (E_constant {cons_name=opname';arguments=lst'}) tv
|
return (E_constant {cons_name=opname';arguments=lst'}) tv
|
||||||
| E_constant {cons_name=C_FOLD_WHILE as opname;
|
| E_constant {cons_name=C_FOLD_WHILE as opname;
|
||||||
arguments = [
|
arguments = [
|
||||||
( { expression_content = (I.E_lambda { binder = (lname, None) ;
|
( { expression_content = (I.E_lambda { binder = lname ;
|
||||||
input_type = None ;
|
input_type = None ;
|
||||||
output_type = None ;
|
output_type = None ;
|
||||||
result }) ;
|
result }) ;
|
||||||
@ -773,6 +740,11 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
|
|||||||
let e' = Environment.add_ez_declaration (let_binder) rhs e in
|
let e' = Environment.add_ez_declaration (let_binder) rhs e in
|
||||||
let%bind let_result = type_expression' e' let_result in
|
let%bind let_result = type_expression' e' let_result in
|
||||||
return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
|
return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
|
||||||
|
| E_recursive {fun_name; fun_type; lambda} ->
|
||||||
|
let%bind fun_type = evaluate_type e fun_type in
|
||||||
|
let e' = Environment.add_ez_binder fun_name fun_type e in
|
||||||
|
let%bind (lambda,_) = type_lambda e' lambda in
|
||||||
|
return (E_recursive {fun_name;fun_type;lambda}) fun_type
|
||||||
| E_ascription {anno_expr; type_annotation} ->
|
| E_ascription {anno_expr; type_annotation} ->
|
||||||
let%bind tv = evaluate_type e type_annotation in
|
let%bind tv = evaluate_type e type_annotation in
|
||||||
let%bind expr' = type_expression' ~tv_opt:tv e anno_expr in
|
let%bind expr' = type_expression' ~tv_opt:tv e anno_expr in
|
||||||
@ -788,6 +760,42 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
|
|||||||
| Some tv' -> O.assert_type_expression_eq (tv' , type_annotation) in
|
| Some tv' -> O.assert_type_expression_eq (tv' , type_annotation) in
|
||||||
ok {expr' with type_expression=type_annotation}
|
ok {expr' with type_expression=type_annotation}
|
||||||
|
|
||||||
|
and type_lambda e {
|
||||||
|
binder ;
|
||||||
|
input_type ;
|
||||||
|
output_type ;
|
||||||
|
result ;
|
||||||
|
} =
|
||||||
|
let%bind input_type =
|
||||||
|
let%bind input_type =
|
||||||
|
(* Hack to take care of let_in introduced by `simplify/cameligo.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_content with
|
||||||
|
| I.E_let_in li -> (
|
||||||
|
match li.rhs.expression_content with
|
||||||
|
| I.E_variable name when name = (binder) -> (
|
||||||
|
match snd li.let_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 binder input_type e in
|
||||||
|
let%bind body = type_expression' ?tv_opt:output_type e' result in
|
||||||
|
let output_type = body.type_expression in
|
||||||
|
ok (({binder; result=body}:O.lambda),(t_function input_type output_type ()))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
|
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
|
||||||
let%bind typer = Operators.Typer.constant_typers name in
|
let%bind typer = Operators.Typer.constant_typers name in
|
||||||
@ -820,9 +828,11 @@ let untype_literal (l:O.literal) : I.literal result =
|
|||||||
| Literal_operation s -> ok (Literal_operation s)
|
| Literal_operation s -> ok (Literal_operation s)
|
||||||
|
|
||||||
let rec untype_expression (e:O.expression) : (I.expression) result =
|
let rec untype_expression (e:O.expression) : (I.expression) result =
|
||||||
|
untype_expression_content e.type_expression e.expression_content
|
||||||
|
and untype_expression_content ty (ec:O.expression_content) : (I.expression) result =
|
||||||
let open I in
|
let open I in
|
||||||
let return e = ok e in
|
let return e = ok e in
|
||||||
match e.expression_content with
|
match ec with
|
||||||
| E_literal l ->
|
| E_literal l ->
|
||||||
let%bind l = untype_literal l in
|
let%bind l = untype_literal l in
|
||||||
return (e_literal l)
|
return (e_literal l)
|
||||||
@ -836,7 +846,7 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
|
|||||||
let%bind arg' = untype_expression expr2 in
|
let%bind arg' = untype_expression expr2 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 e.type_expression in
|
let%bind io = get_t_function ty in
|
||||||
let%bind (input_type , output_type) = bind_map_pair untype_type_expression io in
|
let%bind (input_type , output_type) = bind_map_pair untype_type_expression io in
|
||||||
let%bind result = untype_expression result in
|
let%bind result = untype_expression result in
|
||||||
return (e_lambda (binder) (Some input_type) (Some output_type) result)
|
return (e_lambda (binder) (Some input_type) (Some output_type) result)
|
||||||
@ -883,7 +893,12 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
|
|||||||
let%bind tv = untype_type_expression rhs.type_expression in
|
let%bind tv = untype_type_expression rhs.type_expression in
|
||||||
let%bind rhs = untype_expression rhs in
|
let%bind rhs = untype_expression rhs in
|
||||||
let%bind result = untype_expression let_result in
|
let%bind result = untype_expression let_result in
|
||||||
return (I.e_let_in (let_binder , (Some tv)) false inline rhs result)
|
return (e_let_in (let_binder , (Some tv)) false inline rhs result)
|
||||||
|
| E_recursive {fun_name;fun_type; lambda} ->
|
||||||
|
let%bind fun_type = untype_type_expression fun_type in
|
||||||
|
let%bind unty_expr= untype_expression_content ty @@ E_lambda lambda in
|
||||||
|
let lambda = match unty_expr.expression_content with I.E_lambda l -> l | _ -> failwith "impossible case" in
|
||||||
|
return @@ e_recursive fun_name fun_type lambda
|
||||||
|
|
||||||
and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
|
and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
|
||||||
let open I in
|
let open I in
|
||||||
|
@ -371,7 +371,7 @@ and eval : Ast_typed.expression -> env -> value result
|
|||||||
| _ -> simple_fail "not yet supported case"
|
| _ -> simple_fail "not yet supported case"
|
||||||
(* ((ctor,name),body) *)
|
(* ((ctor,name),body) *)
|
||||||
)
|
)
|
||||||
| E_look_up _ ->
|
| E_look_up _ | E_recursive _ ->
|
||||||
let serr = Format.asprintf "Unsupported construct :\n %a\n" Ast_typed.PP.expression term in
|
let serr = Format.asprintf "Unsupported construct :\n %a\n" Ast_typed.PP.expression term in
|
||||||
simple_fail serr
|
simple_fail serr
|
||||||
|
|
||||||
|
@ -379,6 +379,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
|
|||||||
| E_lambda l ->
|
| E_lambda l ->
|
||||||
let%bind io = AST.get_t_function ae.type_expression in
|
let%bind io = AST.get_t_function ae.type_expression in
|
||||||
transpile_lambda l io
|
transpile_lambda l io
|
||||||
|
| E_recursive r ->
|
||||||
|
transpile_recursive r
|
||||||
| E_list lst -> (
|
| E_list lst -> (
|
||||||
let%bind t =
|
let%bind t =
|
||||||
trace_strong (corner_case ~loc:__LOC__ "not a list") @@
|
trace_strong (corner_case ~loc:__LOC__ "not a list") @@
|
||||||
@ -518,6 +520,10 @@ and transpile_lambda l (input_type , output_type) =
|
|||||||
let closure = E_closure { binder; body = result'} in
|
let closure = E_closure { binder; body = result'} in
|
||||||
ok @@ Combinators.Expression.make_tpl (closure , tv)
|
ok @@ Combinators.Expression.make_tpl (closure , tv)
|
||||||
|
|
||||||
|
and transpile_recursive {fun_name; fun_type; lambda} =
|
||||||
|
let closure = E_closure { binder=fun_name; body} in
|
||||||
|
ok @@ Combinators.Expression.make closure fun_type
|
||||||
|
|
||||||
let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
|
let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
|
||||||
match d with
|
match d with
|
||||||
| Declaration_constant (name,expression, inline, _) ->
|
| Declaration_constant (name,expression, inline, _) ->
|
||||||
|
@ -11,7 +11,9 @@ let expression_variable ppf (ev : expression_variable) : unit =
|
|||||||
|
|
||||||
|
|
||||||
let rec expression ppf (e : expression) =
|
let rec expression ppf (e : expression) =
|
||||||
match e.expression_content with
|
expression_content ppf e.expression_content
|
||||||
|
and expression_content ppf (ec : expression_content) =
|
||||||
|
match ec with
|
||||||
| E_literal l ->
|
| E_literal l ->
|
||||||
literal ppf l
|
literal ppf l
|
||||||
| E_variable n ->
|
| E_variable n ->
|
||||||
@ -40,16 +42,23 @@ let rec expression ppf (e : expression) =
|
|||||||
| E_look_up (ds, ind) ->
|
| E_look_up (ds, ind) ->
|
||||||
fprintf ppf "(%a)[%a]" expression ds expression ind
|
fprintf ppf "(%a)[%a]" expression ds expression ind
|
||||||
| E_lambda {binder; input_type; output_type; result} ->
|
| E_lambda {binder; input_type; output_type; result} ->
|
||||||
fprintf ppf "lambda (%a:%a) : %a return %a" option_type_name binder
|
fprintf ppf "lambda (%a:%a) : %a return %a"
|
||||||
|
expression_variable binder
|
||||||
(PP_helpers.option type_expression)
|
(PP_helpers.option type_expression)
|
||||||
input_type
|
input_type
|
||||||
(PP_helpers.option type_expression)
|
(PP_helpers.option type_expression)
|
||||||
output_type expression result
|
output_type expression result
|
||||||
| E_matching {matchee; cases; _} ->
|
| E_matching {matchee; cases; _} ->
|
||||||
fprintf ppf "match %a with %a" expression matchee (matching expression)
|
fprintf ppf "match %a with %a"
|
||||||
|
expression matchee (matching expression)
|
||||||
cases
|
cases
|
||||||
| 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_recursive { fun_name; fun_type; lambda} ->
|
||||||
|
fprintf ppf "rec (%a:%a => %a )"
|
||||||
|
expression_variable fun_name
|
||||||
|
type_expression fun_type
|
||||||
|
expression_content (E_lambda lambda)
|
||||||
| E_skip ->
|
| E_skip ->
|
||||||
fprintf ppf "skip"
|
fprintf ppf "skip"
|
||||||
| E_ascription {anno_expr; type_annotation} ->
|
| E_ascription {anno_expr; type_annotation} ->
|
||||||
|
@ -178,11 +178,12 @@ let e_lambda ?loc (binder : expression_variable)
|
|||||||
(result : expression)
|
(result : expression)
|
||||||
: expression =
|
: expression =
|
||||||
location_wrap ?loc @@ E_lambda {
|
location_wrap ?loc @@ E_lambda {
|
||||||
binder = (binder , input_type) ;
|
binder = binder;
|
||||||
input_type = input_type ;
|
input_type = input_type ;
|
||||||
output_type = output_type ;
|
output_type = output_type ;
|
||||||
result ;
|
result ;
|
||||||
}
|
}
|
||||||
|
let e_recursive ?loc fun_name fun_type lambda = location_wrap ?loc @@ E_recursive {fun_name; fun_type; lambda}
|
||||||
|
|
||||||
|
|
||||||
let e_assign_with_let ?loc var access_path expr =
|
let e_assign_with_let ?loc var access_path expr =
|
||||||
|
@ -106,6 +106,7 @@ val e_typed_big_map : ?loc:Location.t -> ( expression * expression ) list -> ty
|
|||||||
val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expression
|
val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expression
|
||||||
|
|
||||||
val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
|
val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
|
||||||
|
val e_recursive : ?loc:Location.t -> expression_variable -> type_expression -> lambda -> expression
|
||||||
val e_record : ?loc:Location.t -> expr Map.String.t -> expression
|
val e_record : ?loc:Location.t -> expr Map.String.t -> expression
|
||||||
val e_update : ?loc:Location.t -> expression -> string -> expression -> expression
|
val e_update : ?loc:Location.t -> expression -> string -> expression -> expression
|
||||||
val e_assign_with_let : ?loc:Location.t -> string -> string list -> expression -> ((expression_variable*type_expression option)*bool*expression*bool)
|
val e_assign_with_let : ?loc:Location.t -> string -> string list -> expression -> ((expression_variable*type_expression option)*bool*expression*bool)
|
||||||
|
@ -182,7 +182,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
|
|||||||
| (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
|
| (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
|
||||||
| (E_variable _, _) | (E_lambda _, _)
|
| (E_variable _, _) | (E_lambda _, _)
|
||||||
| (E_application _, _) | (E_let_in _, _)
|
| (E_application _, _) | (E_let_in _, _)
|
||||||
| (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_skip, _) -> simple_fail "comparing not a value"
|
||||||
|
|
||||||
|
@ -35,6 +35,7 @@ and expression_content =
|
|||||||
| E_application of application
|
| E_application of application
|
||||||
| E_lambda of lambda
|
| E_lambda of lambda
|
||||||
| E_let_in of let_in
|
| E_let_in of let_in
|
||||||
|
| E_recursive of recursive
|
||||||
| E_skip
|
| E_skip
|
||||||
(* Variant *)
|
(* Variant *)
|
||||||
| E_constructor of constructor (* For user defined constructors *)
|
| E_constructor of constructor (* For user defined constructors *)
|
||||||
@ -60,7 +61,7 @@ and constant =
|
|||||||
and application = {expr1: expression; expr2: expression}
|
and application = {expr1: expression; expr2: expression}
|
||||||
|
|
||||||
and lambda =
|
and lambda =
|
||||||
{ binder: expression_variable * type_expression option
|
{ binder: expression_variable
|
||||||
; input_type: type_expression option
|
; input_type: type_expression option
|
||||||
; output_type: type_expression option
|
; output_type: type_expression option
|
||||||
; result: expression }
|
; result: expression }
|
||||||
@ -72,6 +73,12 @@ and let_in =
|
|||||||
; let_result: expression
|
; let_result: expression
|
||||||
; inline: bool }
|
; inline: bool }
|
||||||
|
|
||||||
|
and recursive = {
|
||||||
|
fun_name : expression_variable;
|
||||||
|
fun_type : type_expression;
|
||||||
|
lambda : lambda;
|
||||||
|
}
|
||||||
|
|
||||||
and constructor = {constructor: constructor'; element: expression}
|
and constructor = {constructor: constructor'; element: expression}
|
||||||
|
|
||||||
and accessor = {expr: expression; label: label}
|
and accessor = {expr: expression; label: label}
|
||||||
|
@ -11,7 +11,10 @@ let expression_variable ppf (ev : expression_variable) : unit =
|
|||||||
|
|
||||||
|
|
||||||
let rec expression ppf (e : expression) =
|
let rec expression ppf (e : expression) =
|
||||||
match e.expression_content with
|
expression_content ppf e.expression_content
|
||||||
|
|
||||||
|
and expression_content ppf (ec: expression_content) =
|
||||||
|
match ec with
|
||||||
| E_literal l ->
|
| E_literal l ->
|
||||||
literal ppf l
|
literal ppf l
|
||||||
| E_variable n ->
|
| E_variable n ->
|
||||||
@ -47,6 +50,11 @@ let rec expression ppf (e : expression) =
|
|||||||
| 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" expression_variable let_binder expression
|
fprintf ppf "let %a = %a%a in %a" expression_variable let_binder expression
|
||||||
rhs option_inline inline expression let_result
|
rhs option_inline inline expression let_result
|
||||||
|
| E_recursive { fun_name;fun_type; lambda} ->
|
||||||
|
fprintf ppf "rec (%a:%a => %a )"
|
||||||
|
expression_variable fun_name
|
||||||
|
type_expression fun_type
|
||||||
|
expression_content (E_lambda lambda)
|
||||||
|
|
||||||
and assoc_expression ppf : expr * expr -> unit =
|
and assoc_expression ppf : expr * expr -> unit =
|
||||||
fun (a, b) -> fprintf ppf "%a -> %a" expression a expression b
|
fun (a, b) -> fprintf ppf "%a -> %a" expression a expression b
|
||||||
|
@ -221,6 +221,9 @@ module Free_variables = struct
|
|||||||
union
|
union
|
||||||
(expression b' let_result)
|
(expression b' let_result)
|
||||||
(self rhs)
|
(self rhs)
|
||||||
|
| E_recursive {fun_name;lambda;_} ->
|
||||||
|
let b' = union (singleton fun_name) b in
|
||||||
|
expression_content b' @@ E_lambda lambda
|
||||||
|
|
||||||
and lambda : bindings -> lambda -> bindings = fun b l ->
|
and lambda : bindings -> lambda -> bindings = fun b l ->
|
||||||
let b' = union (singleton l.binder) b in
|
let b' = union (singleton l.binder) b in
|
||||||
@ -529,7 +532,7 @@ let rec assert_value_eq (a, b: (expression*expression)) : unit result =
|
|||||||
| E_set _, _ ->
|
| E_set _, _ ->
|
||||||
fail @@ different_values_because_different_types "set vs. non-set" a b
|
fail @@ different_values_because_different_types "set vs. non-set" a b
|
||||||
| (E_literal _, _) | (E_variable _, _) | (E_application _, _)
|
| (E_literal _, _) | (E_variable _, _) | (E_application _, _)
|
||||||
| (E_lambda _, _) | (E_let_in _, _)
|
| (E_lambda _, _) | (E_let_in _, _) | (E_recursive _, _)
|
||||||
| (E_record_accessor _, _) | (E_record_update _,_)
|
| (E_record_accessor _, _) | (E_record_update _,_)
|
||||||
| (E_look_up _, _) | (E_matching _, _)
|
| (E_look_up _, _) | (E_matching _, _)
|
||||||
-> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b
|
-> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b
|
||||||
|
@ -45,9 +45,11 @@ module Captured_variables = struct
|
|||||||
let empty : bindings = []
|
let empty : bindings = []
|
||||||
let of_list : expression_variable list -> bindings = fun x -> x
|
let of_list : expression_variable list -> bindings = fun x -> x
|
||||||
|
|
||||||
let rec expression : bindings -> expression -> bindings result = fun b ae ->
|
let rec expression : bindings -> expression -> bindings result = fun b e ->
|
||||||
|
expression_content b e.environment e.expression_content
|
||||||
|
and expression_content : bindings -> full_environment -> expression_content -> bindings result = fun b env ec ->
|
||||||
let self = expression b in
|
let self = expression b in
|
||||||
match ae.expression_content with
|
match ec with
|
||||||
| E_lambda l -> ok @@ Free_variables.lambda empty l
|
| E_lambda l -> ok @@ Free_variables.lambda empty l
|
||||||
| E_literal _ -> ok empty
|
| E_literal _ -> ok empty
|
||||||
| E_constant {arguments;_} ->
|
| E_constant {arguments;_} ->
|
||||||
@ -56,7 +58,7 @@ module Captured_variables = struct
|
|||||||
| E_variable name -> (
|
| E_variable name -> (
|
||||||
let%bind env_element =
|
let%bind env_element =
|
||||||
trace_option (simple_error "missing var in env") @@
|
trace_option (simple_error "missing var in env") @@
|
||||||
Environment.get_opt name ae.environment in
|
Environment.get_opt name env in
|
||||||
match env_element.definition with
|
match env_element.definition with
|
||||||
| ED_binder -> ok empty
|
| ED_binder -> ok empty
|
||||||
| ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
|
| ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
|
||||||
@ -92,6 +94,9 @@ module Captured_variables = struct
|
|||||||
| E_let_in li ->
|
| E_let_in li ->
|
||||||
let b' = union (singleton li.let_binder) b in
|
let b' = union (singleton li.let_binder) b in
|
||||||
expression b' li.let_result
|
expression b' li.let_result
|
||||||
|
| E_recursive r ->
|
||||||
|
let b' = union (singleton r.fun_name) b in
|
||||||
|
expression_content b' env @@ E_lambda r.lambda
|
||||||
|
|
||||||
and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor' * expression_variable) * a) -> bindings result = fun f b ((_,n),c) ->
|
and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor' * expression_variable) * a) -> bindings result = fun f b ((_,n),c) ->
|
||||||
f (union (singleton n) b) c
|
f (union (singleton n) b) c
|
||||||
|
@ -41,6 +41,7 @@ and expression_content =
|
|||||||
| E_application of application
|
| E_application of application
|
||||||
| E_lambda of lambda
|
| E_lambda of lambda
|
||||||
| E_let_in of let_in
|
| E_let_in of let_in
|
||||||
|
| E_recursive of recursive
|
||||||
(* 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
|
||||||
@ -76,6 +77,12 @@ and let_in = {
|
|||||||
inline : inline ;
|
inline : inline ;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
and recursive = {
|
||||||
|
fun_name : expression_variable;
|
||||||
|
fun_type : type_expression;
|
||||||
|
lambda : lambda;
|
||||||
|
}
|
||||||
|
|
||||||
and constructor = {
|
and constructor = {
|
||||||
constructor: constructor';
|
constructor: constructor';
|
||||||
element: expression ;
|
element: expression ;
|
||||||
|
@ -164,6 +164,12 @@ module Substitution = struct
|
|||||||
let%bind rhs = s_expression ~substs rhs in
|
let%bind rhs = s_expression ~substs rhs in
|
||||||
let%bind let_result = s_expression ~substs let_result in
|
let%bind let_result = s_expression ~substs let_result in
|
||||||
ok @@ T.E_let_in { let_binder; rhs; let_result; inline }
|
ok @@ T.E_let_in { let_binder; rhs; let_result; inline }
|
||||||
|
| T.E_recursive { fun_name; fun_type; lambda} ->
|
||||||
|
let%bind fun_name = s_variable ~substs fun_name in
|
||||||
|
let%bind fun_type = s_type_expression ~substs fun_type in
|
||||||
|
let%bind sec = s_expression_content ~substs (T.E_lambda lambda) in
|
||||||
|
let lambda = match sec with E_lambda l -> l | _ -> failwith "impossible case" in
|
||||||
|
ok @@ T.E_recursive { fun_name; fun_type; lambda}
|
||||||
| T.E_constructor {constructor;element} ->
|
| T.E_constructor {constructor;element} ->
|
||||||
let%bind constructor = s_constructor ~substs constructor in
|
let%bind constructor = s_constructor ~substs constructor in
|
||||||
let%bind element = s_expression ~substs element in
|
let%bind element = s_expression ~substs element in
|
||||||
|
Loading…
Reference in New Issue
Block a user