Translation to scalc: fix renaming in blocks

Statements are often flattened, in which case their idents need to be
conflict-free. We pass along the renaming context to handle this.
This commit is contained in:
Louis Gesbert 2024-08-08 12:03:53 +02:00
parent f565e84dae
commit 14a378a33d
4 changed files with 146 additions and 134 deletions

View File

@ -98,16 +98,16 @@ let register_fresh_arg ~pos ctxt (x, _) =
ctxt ctxt
let rec translate_expr_list ctxt args = let rec translate_expr_list ctxt args =
let stmts, args = let stmts, args, ren_ctx =
List.fold_left List.fold_left
(fun (args_stmts, new_args) arg -> (fun (args_stmts, new_args, ren_ctx) arg ->
let arg_stmts, new_arg = translate_expr ctxt arg in let arg_stmts, new_arg, ren_ctx = translate_expr { ctxt with ren_ctx } arg in
args_stmts ++ arg_stmts, new_arg :: new_args) args_stmts ++ arg_stmts, new_arg :: new_args, ren_ctx)
(RevBlock.empty, []) args (RevBlock.empty, [], ctxt.ren_ctx) args
in in
stmts, List.rev args stmts, List.rev args, ren_ctx
and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr = and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr * Renaming.context =
try try
match Mark.remove expr with match Mark.remove expr with
| EVar v -> | EVar v ->
@ -123,27 +123,27 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
Print.var_debug ppf v)) Print.var_debug ppf v))
(Var.Map.keys ctxt.var_dict)) (Var.Map.keys ctxt.var_dict))
in in
RevBlock.empty, (local_var, Expr.pos expr) RevBlock.empty, (local_var, Expr.pos expr), ctxt.ren_ctx
| EStruct { fields; name } -> | EStruct { fields; name } ->
if ctxt.config.no_struct_literals then if ctxt.config.no_struct_literals then
(* In C89, struct literates have to be initialized at variable (* In C89, struct literates have to be initialized at variable
definition... *) definition... *)
raise (NotAnExpr { needs_a_local_decl = false }); raise (NotAnExpr { needs_a_local_decl = false });
let args_stmts, new_args = let args_stmts, new_args, ren_ctx =
StructField.Map.fold StructField.Map.fold
(fun field arg (args_stmts, new_args) -> (fun field arg (args_stmts, new_args, ren_ctx) ->
let arg_stmts, new_arg = translate_expr ctxt arg in let arg_stmts, new_arg, ren_ctx = translate_expr { ctxt with ren_ctx } arg in
args_stmts ++ arg_stmts, StructField.Map.add field new_arg new_args) args_stmts ++ arg_stmts, StructField.Map.add field new_arg new_args, ren_ctx)
fields fields
(RevBlock.empty, StructField.Map.empty) (RevBlock.empty, StructField.Map.empty, ctxt.ren_ctx)
in in
args_stmts, (A.EStruct { fields = new_args; name }, Expr.pos expr) args_stmts, (A.EStruct { fields = new_args; name }, Expr.pos expr), ren_ctx
| EInj { e = e1; cons; name } -> | EInj { e = e1; cons; name } ->
if ctxt.config.no_struct_literals then if ctxt.config.no_struct_literals then
(* In C89, struct literates have to be initialized at variable (* In C89, struct literates have to be initialized at variable
definition... *) definition... *)
raise (NotAnExpr { needs_a_local_decl = false }); raise (NotAnExpr { needs_a_local_decl = false });
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1, ren_ctx = translate_expr ctxt e1 in
( e1_stmts, ( e1_stmts,
( A.EInj ( A.EInj
{ {
@ -152,21 +152,23 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
name; name;
expr_typ = Expr.maybe_ty (Mark.get expr); expr_typ = Expr.maybe_ty (Mark.get expr);
}, },
Expr.pos expr ) ) Expr.pos expr ),
ren_ctx )
| ETuple args -> | ETuple args ->
let args_stmts, new_args = translate_expr_list ctxt args in let args_stmts, new_args, ren_ctx = translate_expr_list ctxt args in
args_stmts, (A.ETuple new_args, Expr.pos expr) args_stmts, (A.ETuple new_args, Expr.pos expr), ren_ctx
| EStructAccess { e = e1; field; name } -> | EStructAccess { e = e1; field; name } ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1, ren_ctx = translate_expr ctxt e1 in
( e1_stmts, ( e1_stmts,
(A.EStructFieldAccess { e1 = new_e1; field; name }, Expr.pos expr) ) (A.EStructFieldAccess { e1 = new_e1; field; name }, Expr.pos expr),
ren_ctx)
| ETupleAccess { e = e1; index; _ } -> | ETupleAccess { e = e1; index; _ } ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1, ren_ctx = translate_expr ctxt e1 in
e1_stmts, (A.ETupleAccess { e1 = new_e1; index }, Expr.pos expr) e1_stmts, (A.ETupleAccess { e1 = new_e1; index }, Expr.pos expr), ren_ctx
| EAppOp { op; args; tys = _ } -> | EAppOp { op; args; tys = _ } ->
let args_stmts, new_args = translate_expr_list ctxt args in let args_stmts, new_args, ren_ctx = translate_expr_list ctxt args in
(* FIXME: what happens if [arg] is not a tuple but reduces to one ? *) (* FIXME: what happens if [arg] is not a tuple but reduces to one ? *)
args_stmts, (A.EAppOp { op; args = new_args }, Expr.pos expr) args_stmts, (A.EAppOp { op; args = new_args }, Expr.pos expr), ren_ctx
| EApp { f = EAbs { binder; tys }, binder_mark; args; tys = _ } -> | EApp { f = EAbs { binder; tys }, binder_mark; args; tys = _ } ->
(* 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
@ -190,39 +192,42 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
(Var.Map.find x ctxt.var_dict, binder_pos), tau, arg) (Var.Map.find x ctxt.var_dict, binder_pos), tau, arg)
vars_tau args vars_tau args
in in
let def_blocks = let def_blocks, ren_ctx =
List.fold_left List.fold_left
(fun acc (x, _tau, arg) -> (fun (rblock, ren_ctx) (x, _tau, arg) ->
let ctxt = let ctxt =
{ {
ctxt with ctxt with
inside_definition_of = Some (Mark.remove x); inside_definition_of = Some (Mark.remove x);
context_name = Mark.remove (A.VarName.get_info (Mark.remove x)); context_name = Mark.remove (A.VarName.get_info (Mark.remove x));
ren_ctx;
} }
in in
let arg_stmts, new_arg = translate_expr ctxt arg in let arg_stmts, new_arg, ren_ctx = translate_expr ctxt arg in
RevBlock.append (acc ++ arg_stmts) RevBlock.append (rblock ++ arg_stmts)
( A.SLocalDef ( A.SLocalDef
{ {
name = x; name = x;
expr = new_arg; expr = new_arg;
typ = Expr.maybe_ty (Mark.get arg); typ = Expr.maybe_ty (Mark.get arg);
}, },
binder_pos )) binder_pos ),
RevBlock.empty vars_args ren_ctx)
(RevBlock.empty, ctxt.ren_ctx) vars_args
in in
let rest_of_expr_stmts, rest_of_expr = translate_expr ctxt body in let rest_of_expr_stmts, rest_of_expr, ren_ctx = translate_expr { ctxt with ren_ctx } body in
local_decls ++ def_blocks ++ rest_of_expr_stmts, rest_of_expr local_decls ++ def_blocks ++ rest_of_expr_stmts, rest_of_expr, ren_ctx
| EApp { f; args; tys = _ } -> | EApp { f; args; tys = _ } ->
let f_stmts, new_f = translate_expr ctxt f in let f_stmts, new_f, ren_ctx = translate_expr ctxt f in
let args_stmts, new_args = translate_expr_list ctxt args in let args_stmts, new_args, ren_ctx = translate_expr_list { ctxt with ren_ctx } args in
(* FIXME: what happens if [arg] is not a tuple but reduces to one ? *) (* FIXME: what happens if [arg] is not a tuple but reduces to one ? *)
( f_stmts ++ args_stmts, ( f_stmts ++ args_stmts,
(A.EApp { f = new_f; args = new_args }, Expr.pos expr) ) (A.EApp { f = new_f; args = new_args }, Expr.pos expr),
ren_ctx )
| EArray args -> | EArray args ->
let args_stmts, new_args = translate_expr_list ctxt args in let args_stmts, new_args, ren_ctx = translate_expr_list ctxt args in
args_stmts, (A.EArray new_args, Expr.pos expr) args_stmts, (A.EArray new_args, Expr.pos expr), ren_ctx
| ELit l -> RevBlock.empty, (A.ELit l, Expr.pos expr) | ELit l -> RevBlock.empty, (A.ELit l, Expr.pos expr), ctxt.ren_ctx
| EExternal { name } -> | EExternal { name } ->
let path, name = let path, name =
match Mark.remove name with match Mark.remove name with
@ -233,7 +238,7 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
( ModuleName.Map.find (List.hd (List.rev path)) ctxt.program_ctx.modules, ( ModuleName.Map.find (List.hd (List.rev path)) ctxt.program_ctx.modules,
Expr.pos expr ) Expr.pos expr )
in in
RevBlock.empty, (EExternal { modname; name }, Expr.pos expr) RevBlock.empty, (EExternal { modname; name }, Expr.pos expr), ctxt.ren_ctx
| EAbs _ | EIfThenElse _ | EMatch _ | EAssert _ | EFatalError _ -> | EAbs _ | EIfThenElse _ | EMatch _ | EAssert _ | EFatalError _ ->
raise (NotAnExpr { needs_a_local_decl = true }) raise (NotAnExpr { needs_a_local_decl = true })
| _ -> . | _ -> .
@ -253,7 +258,7 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
context_name = Mark.remove (A.VarName.get_info tmp_var); context_name = Mark.remove (A.VarName.get_info tmp_var);
} }
in in
let tmp_stmts = translate_statements ctxt expr in let tmp_stmts, ren_ctx = translate_statements ctxt expr in
( (if needs_a_local_decl then ( (if needs_a_local_decl then
RevBlock.make RevBlock.make
(( A.SLocalDecl (( A.SLocalDecl
@ -264,17 +269,19 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
Expr.pos expr ) Expr.pos expr )
:: tmp_stmts) :: tmp_stmts)
else RevBlock.make tmp_stmts), else RevBlock.make tmp_stmts),
(A.EVar tmp_var, Expr.pos expr) ) (A.EVar tmp_var, Expr.pos expr),
ren_ctx )
and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block = and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block * Renaming.context =
match Mark.remove block_expr with match Mark.remove block_expr with
| EAssert e -> | EAssert e ->
(* 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, ren_ctx = translate_expr ctxt e in
RevBlock.rebuild RevBlock.rebuild
~tail:[A.SAssert (Mark.remove new_e), Expr.pos block_expr] ~tail:[A.SAssert (Mark.remove new_e), Expr.pos block_expr]
e_stmts e_stmts,
| EFatalError err -> [SFatalError err, Expr.pos block_expr] ren_ctx
| EFatalError err -> [SFatalError err, Expr.pos block_expr], ctxt.ren_ctx
(* | EAppOp (* | EAppOp
* { op = Op.HandleDefaultOpt, _; tys = _; args = [exceptions; just; cons] } * { op = Op.HandleDefaultOpt, _; tys = _; args = [exceptions; just; cons] }
* when ctxt.config.keep_special_ops -> * when ctxt.config.keep_special_ops ->
@ -351,32 +358,31 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
(Var.Map.find x ctxt.var_dict, binder_pos), tau, arg) (Var.Map.find x ctxt.var_dict, binder_pos), tau, arg)
vars_tau args vars_tau args
in in
let def_blocks = let def_blocks, ren_ctx =
List.map List.fold_left
(fun (x, _tau, arg) -> (fun (def_blocks, ren_ctx) (x, _tau, arg) ->
let ctxt = let ctxt =
{ {
ctxt with ctxt with
inside_definition_of = Some (Mark.remove x); inside_definition_of = Some (Mark.remove x);
context_name = Mark.remove (A.VarName.get_info (Mark.remove x)); context_name = Mark.remove (A.VarName.get_info (Mark.remove x));
ren_ctx;
} }
in in
let arg_stmts, new_arg = translate_expr ctxt arg in let arg_stmts, new_arg, ren_ctx = translate_expr { ctxt with ren_ctx } arg in
RevBlock.rebuild arg_stmts RevBlock.append (def_blocks ++ arg_stmts)
~tail:
[
( A.SLocalDef ( A.SLocalDef
{ {
name = x; name = x;
expr = new_arg; expr = new_arg;
typ = Expr.maybe_ty (Mark.get arg); typ = Expr.maybe_ty (Mark.get arg);
}, },
binder_pos ); binder_pos ),
]) ren_ctx)
vars_args (RevBlock.empty, ctxt.ren_ctx) vars_args
in in
let rest_of_block = translate_statements ctxt body in let rest_of_block, ren_ctx = translate_statements { ctxt with ren_ctx } body in
local_decls @ List.flatten def_blocks @ rest_of_block local_decls @ RevBlock.rebuild def_blocks ~tail:rest_of_block, ren_ctx
| EAbs { binder; tys } -> | EAbs { binder; tys } ->
let closure_name, ctxt = let closure_name, ctxt =
match ctxt.inside_definition_of with match ctxt.inside_definition_of with
@ -392,7 +398,7 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
{ ctxt with inside_definition_of = None } { ctxt with inside_definition_of = None }
vars_tau vars_tau
in in
let new_body = translate_statements ctxt body in let new_body, _ren_ctx = translate_statements ctxt body in
[ [
( A.SInnerFuncDef ( A.SInnerFuncDef
{ {
@ -413,9 +419,9 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
}; };
}, },
binder_pos ); binder_pos );
] ], ctxt.ren_ctx
| EMatch { e = e1; cases; name } -> | EMatch { e = e1; cases; name } ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1, ren_ctx = translate_expr ctxt e1 in
let new_cases = let new_cases =
EnumConstructor.Map.fold EnumConstructor.Map.fold
(fun _ arg new_args -> (fun _ arg new_args ->
@ -427,7 +433,7 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
let scalc_var, ctxt = let scalc_var, ctxt =
register_fresh_var ctxt var ~pos:(Expr.pos arg) register_fresh_var ctxt var ~pos:(Expr.pos arg)
in in
let new_arg = translate_statements ctxt body in let new_arg, _ren_ctx = translate_statements ctxt body in
{ {
A.case_block = new_arg; A.case_block = new_arg;
payload_var_name = scalc_var; payload_var_name = scalc_var;
@ -449,11 +455,12 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
switch_cases = new_args; switch_cases = new_args;
}, },
Expr.pos block_expr ); Expr.pos block_expr );
] ],
ren_ctx
| EIfThenElse { cond; etrue; efalse } -> | EIfThenElse { cond; etrue; efalse } ->
let cond_stmts, s_cond = translate_expr ctxt cond in let cond_stmts, s_cond, ren_ctx = translate_expr ctxt cond in
let s_e_true = translate_statements ctxt etrue in let s_e_true, _ = translate_statements ctxt etrue in
let s_e_false = translate_statements ctxt efalse in let s_e_false, _ = translate_statements ctxt efalse in
RevBlock.rebuild cond_stmts RevBlock.rebuild cond_stmts
~tail: ~tail:
[ [
@ -464,14 +471,14 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
else_block = s_e_false; else_block = s_e_false;
}, },
Expr.pos block_expr ); Expr.pos block_expr );
] ],
ren_ctx
| EInj { e = e1; cons; name } when ctxt.config.no_struct_literals -> | EInj { e = e1; cons; name } when ctxt.config.no_struct_literals ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1, ren_ctx = translate_expr ctxt e1 in
let tmp_struct_var_name = let tmp_struct_var_name =
match ctxt.inside_definition_of with match ctxt.inside_definition_of with
| None -> | None -> assert false
failwith "should not happen" (* [translate_expr] should create this [inside_definition_of]*)
(* [translate_expr] should create this [inside_definition_of]*)
| Some x -> x, Expr.pos block_expr | Some x -> x, Expr.pos block_expr
in in
let inj_expr = let inj_expr =
@ -496,15 +503,16 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
Expr.pos block_expr ); Expr.pos block_expr );
}, },
Expr.pos block_expr ); Expr.pos block_expr );
] ],
ren_ctx
| EStruct { fields; name } when ctxt.config.no_struct_literals -> | EStruct { fields; name } when ctxt.config.no_struct_literals ->
let args_stmts, new_args = let args_stmts, new_args, ren_ctx =
StructField.Map.fold StructField.Map.fold
(fun field arg (args_stmts, new_args) -> (fun field arg (args_stmts, new_args, ren_ctx) ->
let arg_stmts, new_arg = translate_expr ctxt arg in let arg_stmts, new_arg, ren_ctx = translate_expr { ctxt with ren_ctx } arg in
args_stmts ++ arg_stmts, StructField.Map.add field new_arg new_args) args_stmts ++ arg_stmts, StructField.Map.add field new_arg new_args, ren_ctx)
fields fields
(RevBlock.empty, StructField.Map.empty) (RevBlock.empty, StructField.Map.empty, ctxt.ren_ctx)
in in
let struct_expr = let struct_expr =
A.EStruct { fields = new_args; name }, Expr.pos block_expr A.EStruct { fields = new_args; name }, Expr.pos block_expr
@ -526,10 +534,11 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
typ = TStruct name, Expr.pos block_expr; typ = TStruct name, Expr.pos block_expr;
}, },
Expr.pos block_expr ); Expr.pos block_expr );
] ],
ren_ctx
| ELit _ | EAppOp _ | EArray _ | EVar _ | EStruct _ | EInj _ | ETuple _ | ELit _ | EAppOp _ | EArray _ | EVar _ | EStruct _ | EInj _ | ETuple _
| ETupleAccess _ | EStructAccess _ | EExternal _ | EApp _ -> | ETupleAccess _ | EStructAccess _ | EExternal _ | EApp _ ->
let e_stmts, new_e = translate_expr ctxt block_expr in let e_stmts, new_e, ren_ctx = translate_expr ctxt block_expr in
let tail = let tail =
match (e_stmts :> (A.stmt * Pos.t) list) with match (e_stmts :> (A.stmt * Pos.t) list) with
| (A.SRaiseEmpty, _) :: _ -> | (A.SRaiseEmpty, _) :: _ ->
@ -551,7 +560,8 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
Expr.pos block_expr ); Expr.pos block_expr );
] ]
in in
RevBlock.rebuild e_stmts ~tail RevBlock.rebuild e_stmts ~tail,
ren_ctx
| _ -> . | _ -> .
let rec translate_scope_body_expr ctx (scope_expr : 'm L.expr scope_body_expr) : let rec translate_scope_body_expr ctx (scope_expr : 'm L.expr scope_body_expr) :
@ -559,59 +569,50 @@ let rec translate_scope_body_expr ctx (scope_expr : 'm L.expr scope_body_expr) :
let ctx = { ctx with inside_definition_of = None } in let ctx = { ctx with inside_definition_of = None } in
match scope_expr with match scope_expr with
| Last e -> | Last e ->
let block, new_e = translate_expr ctx e in let block, new_e, _ren_ctx = translate_expr ctx e in
RevBlock.rebuild block ~tail:[A.SReturn (Mark.remove new_e), Mark.get new_e] RevBlock.rebuild block ~tail:[A.SReturn (Mark.remove new_e), Mark.get new_e]
| Cons (scope_let, next_bnd) -> ( | Cons (scope_let, next_bnd) ->
let let_var, scope_let_next, ctx1 = unbind ctx next_bnd in let let_var, scope_let_next, ctx = unbind ctx next_bnd in
let let_var_id, ctx = let let_var_id, ctx =
register_fresh_var ctx1 let_var ~pos:scope_let.scope_let_pos register_fresh_var ctx let_var ~pos:scope_let.scope_let_pos
in in
let next = translate_scope_body_expr ctx scope_let_next in let statements, ren_ctx =
match scope_let.scope_let_kind with match scope_let.scope_let_kind with
| Assertion -> | Assertion ->
translate_statements let stmts, ren_ctx =
{ ctx with inside_definition_of = Some let_var_id } translate_statements
scope_let.scope_let_expr { ctx with inside_definition_of = Some let_var_id }
@ next scope_let.scope_let_expr
| _ -> in
let let_expr_stmts, new_let_expr = RevBlock.make stmts, ren_ctx
translate_expr | _ ->
{ ctx with inside_definition_of = Some let_var_id } let let_expr_stmts, new_let_expr, ren_ctx =
scope_let.scope_let_expr translate_expr
in { ctx with inside_definition_of = Some let_var_id }
RevBlock.rebuild let_expr_stmts scope_let.scope_let_expr
~tail: in
(( A.SLocalDecl let (+>) = RevBlock.append in
{ let_expr_stmts +>
name = let_var_id, scope_let.scope_let_pos; ( A.SLocalDecl
typ = scope_let.scope_let_typ; {
}, name = let_var_id, scope_let.scope_let_pos;
scope_let.scope_let_pos ) typ = scope_let.scope_let_typ;
:: ( A.SLocalDef },
{ scope_let.scope_let_pos ) +>
name = let_var_id, scope_let.scope_let_pos; ( A.SLocalDef
expr = new_let_expr; {
typ = scope_let.scope_let_typ; name = let_var_id, scope_let.scope_let_pos;
}, expr = new_let_expr;
scope_let.scope_let_pos ) typ = scope_let.scope_let_typ;
:: next)) },
scope_let.scope_let_pos ),
ren_ctx
in
let tail = translate_scope_body_expr { ctx with ren_ctx } scope_let_next in
RevBlock.rebuild statements ~tail
let translate_program ~(config : translation_config) (p : 'm L.program) : let translate_program ~(config : translation_config) (p : 'm L.program) :
A.program = A.program =
let modules =
List.fold_left
(fun acc (m, _) ->
let vname = Mark.map (( ^ ) "Module_") (ModuleName.get_info m) in
(* The "Module_" prefix is a workaround name clashes for same-name
structs and modules, Python in particular mixes everything in one
namespaces. It can be removed once we have full clash-free variable
renaming in the Python backend (requiring all idents to go through
one stage of being bindlib vars) *)
ModuleName.Map.add m (A.VarName.fresh vname) acc)
ModuleName.Map.empty
(Program.modules_to_list p.decl_ctx.ctx_modules)
in
let program_ctx = { A.decl_ctx = p.decl_ctx; A.modules } in
let ctxt = let ctxt =
{ {
func_dict = Var.Map.empty; func_dict = Var.Map.empty;
@ -619,10 +620,21 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
inside_definition_of = None; inside_definition_of = None;
context_name = ""; context_name = "";
config; config;
program_ctx; program_ctx = { A.decl_ctx = p.decl_ctx; modules = ModuleName.Map.empty};
ren_ctx = config.renaming_context; ren_ctx = config.renaming_context;
} }
in in
let modules, ctxt =
List.fold_left
(fun (modules, ctxt) (m, _) ->
let name, pos = ModuleName.get_info m in
let vname, ctxt = get_name ctxt name in
ModuleName.Map.add m (A.VarName.fresh (vname, pos)) modules, ctxt)
(ModuleName.Map.empty, ctxt)
(Program.modules_to_list p.decl_ctx.ctx_modules)
in
let program_ctx = { ctxt.program_ctx with A.modules } in
let ctxt = { ctxt with program_ctx } in
let (_, rev_items), _vlist = let (_, rev_items), _vlist =
BoundList.fold_left ~init:(ctxt, []) BoundList.fold_left ~init:(ctxt, [])
~f:(fun (ctxt, rev_items) code_item var -> ~f:(fun (ctxt, rev_items) code_item var ->
@ -661,7 +673,7 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
:: rev_items ) :: rev_items )
| Topdef (name, topdef_ty, (EAbs abs, m)) -> | Topdef (name, topdef_ty, (EAbs abs, m)) ->
(* Toplevel function def *) (* Toplevel function def *)
let (block, expr), args_id = let (block, expr, _ren_ctx), args_id =
let args_a, expr, ctxt = unmbind ctxt abs.binder in let args_a, expr, ctxt = unmbind ctxt abs.binder in
let args = Array.to_list args_a in let args = Array.to_list args_a in
let rargs_id, ctxt = let rargs_id, ctxt =
@ -705,7 +717,7 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
:: rev_items ) :: rev_items )
| Topdef (name, topdef_ty, expr) -> | Topdef (name, topdef_ty, expr) ->
(* Toplevel constant def *) (* Toplevel constant def *)
let block, expr = let block, expr, _ren_ctx =
let ctxt = let ctxt =
{ {
ctxt with ctxt with

View File

@ -160,6 +160,7 @@ let renaming =
~reset_context_for_closed_terms:false ~skip_constant_binders:false ~reset_context_for_closed_terms:false ~skip_constant_binders:false
~constant_binder_name:None ~namespaced_fields_constrs:true ~constant_binder_name:None ~namespaced_fields_constrs:true
~f_struct:String.to_camel_case ~f_struct:String.to_camel_case
~f_enum:String.to_camel_case
let typ_needs_parens (e : typ) : bool = let typ_needs_parens (e : typ) : bool =
match Mark.remove e with TArrow _ | TArray _ -> true | _ -> false match Mark.remove e with TArrow _ | TArray _ -> true | _ -> false
@ -413,7 +414,7 @@ let rec format_statement ctx (fmt : Format.formatter) (s : stmt Mark.pos) : unit
let pos = Mark.get s in let pos = Mark.get s in
Format.fprintf fmt Format.fprintf fmt
"@[<hv 4>if not (%a):@,\ "@[<hv 4>if not (%a):@,\
raise AssertionFailure(@[<hov>SourcePosition(@[<hov 0>filename=\"%s\",@ \ raise AssertionFailed(@[<hov>SourcePosition(@[<hov 0>filename=\"%s\",@ \
start_line=%d,@ start_column=%d,@ end_line=%d,@ end_column=%d,@ \ start_line=%d,@ start_column=%d,@ end_line=%d,@ end_column=%d,@ \
law_headings=@[<hv>%a@])@])@]@]" law_headings=@[<hv>%a@])@])@]@]"
(format_expression ctx) (format_expression ctx)

View File

@ -15,7 +15,6 @@
License for the specific language governing permissions and limitations under License for the specific language governing permissions and limitations under
the License. *) the License. *)
open Catala_utils
open Definitions open Definitions
let map_decl_ctx ~f ctx = let map_decl_ctx ~f ctx =

View File

@ -162,11 +162,11 @@ def b(b_in:BIn):
arg = perhaps_none_arg arg = perhaps_none_arg
result1 = arg result1 = arg
result = some_name(SomeNameIn(i_in = result1)) result = some_name(SomeNameIn(i_in = result1))
result1 = SomeName(o = result.o) result4 = SomeName(o = result.o)
if True: if True:
some_name2 = result1 some_name2 = result4
else: else:
some_name2 = result1 some_name2 = result4
some_name1 = some_name2 some_name1 = some_name2
return B(some_name = some_name1) return B(some_name = some_name1)
``` ```