Trying to progress

This commit is contained in:
Denis Merigoux 2023-12-11 13:56:13 +01:00
parent 1d4119c3a3
commit f072694e50
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -32,79 +32,85 @@ type 'm ctxt = {
(* Expressions can spill out side effect, hence this function also returns a (* Expressions can spill out side effect, hence this function also returns a
list of statements to be prepended before the expression is evaluated *) list of statements to be prepended before the expression is evaluated *)
let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr = let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr =
match Mark.remove expr with try
| EVar v -> match Mark.remove expr with
let local_var = | EVar v ->
try A.EVar (Var.Map.find v ctxt.var_dict) let local_var =
with Var.Map.Not_found _ -> ( try A.EVar (Var.Map.find v ctxt.var_dict)
try A.EFunc (Var.Map.find v ctxt.func_dict) with Var.Map.Not_found _ -> (
with Var.Map.Not_found _ -> try A.EFunc (Var.Map.find v ctxt.func_dict)
Message.raise_spanned_error (Expr.pos expr) with Var.Map.Not_found _ ->
"Var not found in lambda→scalc: %a@\nknown: @[<hov>%a@]@\n" Message.raise_spanned_error (Expr.pos expr)
Print.var_debug v "Var not found in lambda→scalc: %a@\nknown: @[<hov>%a@]@\n"
(Format.pp_print_list ~pp_sep:Format.pp_print_space (fun ppf v -> Print.var_debug v
Print.var_debug ppf v)) (Format.pp_print_list ~pp_sep:Format.pp_print_space (fun ppf v ->
(Var.Map.keys ctxt.var_dict)) Print.var_debug ppf v))
in (Var.Map.keys ctxt.var_dict))
[], (local_var, Expr.pos expr) in
| EStruct { fields; name } -> [], (local_var, Expr.pos expr)
let args_stmts, new_args = | EStruct { fields; name } ->
StructField.Map.fold let args_stmts, new_args =
(fun _ arg (args_stmts, new_args) -> StructField.Map.fold
let arg_stmts, new_arg = translate_expr ctxt arg in (fun _ arg (args_stmts, new_args) ->
arg_stmts @ args_stmts, new_arg :: new_args) let arg_stmts, new_arg = translate_expr ctxt arg in
fields ([], []) arg_stmts @ args_stmts, new_arg :: new_args)
in fields ([], [])
let new_args = List.rev new_args in in
let args_stmts = List.rev args_stmts in let new_args = List.rev new_args in
args_stmts, (A.EStruct (new_args, name), Expr.pos expr) let args_stmts = List.rev args_stmts in
| ETuple args -> args_stmts, (A.EStruct (new_args, name), Expr.pos expr)
let args_stmts, new_args = | ETuple args ->
List.fold_left let args_stmts, new_args =
(fun (args_stmts, new_args) arg -> List.fold_left
let arg_stmts, new_arg = translate_expr ctxt arg in (fun (args_stmts, new_args) arg ->
arg_stmts @ args_stmts, new_arg :: new_args) let arg_stmts, new_arg = translate_expr ctxt arg in
([], []) args arg_stmts @ args_stmts, new_arg :: new_args)
in ([], []) args
let new_args = List.rev new_args in in
args_stmts, (A.ETuple new_args, Expr.pos expr) let new_args = List.rev new_args in
| EStructAccess { e = e1; field; name } -> args_stmts, (A.ETuple new_args, Expr.pos expr)
let e1_stmts, new_e1 = translate_expr ctxt e1 in | EStructAccess { e = e1; field; name } ->
e1_stmts, (A.EStructFieldAccess (new_e1, field, name), Expr.pos expr) let e1_stmts, new_e1 = translate_expr ctxt e1 in
| ETupleAccess { e = e1; index; _ } -> e1_stmts, (A.EStructFieldAccess (new_e1, field, name), Expr.pos expr)
let e1_stmts, new_e1 = translate_expr ctxt e1 in | ETupleAccess { e = e1; index; _ } ->
e1_stmts, (A.ETupleAccess (new_e1, index), Expr.pos expr) let e1_stmts, new_e1 = translate_expr ctxt e1 in
| EInj { e = e1; cons; name } -> e1_stmts, (A.ETupleAccess (new_e1, index), Expr.pos expr)
let e1_stmts, new_e1 = translate_expr ctxt e1 in | EInj { e = e1; cons; name } ->
e1_stmts, (A.EInj (new_e1, cons, name), Expr.pos expr) let e1_stmts, new_e1 = translate_expr ctxt e1 in
| EApp e1_stmts, (A.EInj (new_e1, cons, name), Expr.pos expr)
{ f = EOp { op = Op.HandleDefaultOpt; tys = _ }, _binder_mark; args = _ } | EApp
when ctxt.keep_special_ops -> {
assert false f = EOp { op = Op.HandleDefaultOpt; tys = _ }, _binder_mark;
| EApp { f; args } -> args = [_exceptions; _just; _cons];
let f_stmts, new_f = translate_expr ctxt f in }
let args_stmts, new_args = when ctxt.keep_special_ops ->
List.fold_left (* This should be translated as a statement *)
(fun (args_stmts, new_args) arg -> raise Not_found
let arg_stmts, new_arg = translate_expr ctxt arg in | EApp { f; args } ->
arg_stmts @ args_stmts, new_arg :: new_args) let f_stmts, new_f = translate_expr ctxt f in
([], []) args let args_stmts, new_args =
in List.fold_left
let new_args = List.rev new_args in (fun (args_stmts, new_args) arg ->
f_stmts @ args_stmts, (A.EApp (new_f, new_args), Expr.pos expr) let arg_stmts, new_arg = translate_expr ctxt arg in
| EArray args -> arg_stmts @ args_stmts, new_arg :: new_args)
let args_stmts, new_args = ([], []) args
List.fold_left in
(fun (args_stmts, new_args) arg -> let new_args = List.rev new_args in
let arg_stmts, new_arg = translate_expr ctxt arg in f_stmts @ args_stmts, (A.EApp (new_f, new_args), Expr.pos expr)
arg_stmts @ args_stmts, new_arg :: new_args) | EArray args ->
([], []) args let args_stmts, new_args =
in List.fold_left
let new_args = List.rev new_args in (fun (args_stmts, new_args) arg ->
args_stmts, (A.EArray new_args, Expr.pos expr) let arg_stmts, new_arg = translate_expr ctxt arg in
| EOp { op; _ } -> [], (A.EOp (Operator.translate op), Expr.pos expr) arg_stmts @ args_stmts, new_arg :: new_args)
| ELit l -> [], (A.ELit l, Expr.pos expr) ([], []) args
| _ -> in
let new_args = List.rev new_args in
args_stmts, (A.EArray new_args, Expr.pos expr)
| EOp { op; _ } -> [], (A.EOp (Operator.translate op), Expr.pos expr)
| ELit l -> [], (A.ELit l, Expr.pos expr)
| _ -> raise Not_found
with Not_found ->
let tmp_var = let tmp_var =
A.VarName.fresh A.VarName.fresh
( (*This piece of logic is used to make the code more readable. TODO: ( (*This piece of logic is used to make the code more readable. TODO:
@ -137,6 +143,31 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
(* Assertions are always encapsulated in a unit-typed let binding *) (* Assertions are always encapsulated in a unit-typed let binding *)
let e_stmts, new_e = translate_expr ctxt e in let e_stmts, new_e = translate_expr ctxt e in
e_stmts @ [A.SAssert (Mark.remove new_e), Expr.pos block_expr] e_stmts @ [A.SAssert (Mark.remove new_e), Expr.pos block_expr]
| EApp
{
f = EOp { op = Op.HandleDefaultOpt; tys = _ }, _binder_mark;
args = [exceptions; just; cons];
}
when ctxt.keep_special_ops ->
let exceptions =
match Mark.remove exceptions with
| EArray exceptions -> exceptions
| _ -> failwith "should not happen"
in
List.iter
(fun ex ->
Message.emit_debug "exception: %a" (Print.expr ~debug:true ()) ex)
exceptions;
Message.emit_debug "just: %a" (Print.expr ~debug:true ()) just;
Message.emit_debug "cons: %a" (Print.expr ~debug:true ()) cons;
let exceptions_stmts, new_exceptions =
List.fold_left
(fun (exceptions_stmts, new_exceptions) arg ->
let arg_stmts, new_arg = translate_expr ctxt arg in
arg_stmts @ exceptions_stmts, new_arg :: new_exceptions)
([], []) exceptions
in
assert false
| EApp { f = EAbs { binder; tys }, binder_mark; args } -> | EApp { f = EAbs { binder; tys }, binder_mark; args } ->
(* This defines multiple local variables at the time *) (* This defines multiple local variables at the time *)
let binder_pos = Expr.mark_pos binder_mark in let binder_pos = Expr.mark_pos binder_mark in