Cleanup: add function for more direct stringification of uids

This commit is contained in:
Louis Gesbert 2024-09-17 11:59:52 +02:00
parent 5ca37029a8
commit 59afc7f4dd
9 changed files with 51 additions and 93 deletions

View File

@ -284,8 +284,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) : 'm Ast.expr boxed =
| None, Some e ->
Message.error
~suggestion:
(List.map
(fun v -> Mark.remove (ScopeVar.get_info v))
(List.map ScopeVar.to_string
(ScopeVar.Map.keys sc_sig.scope_sig_in_fields))
~fmt_pos:
[
@ -752,9 +751,7 @@ let translate_scope_decl
| None -> AbortOnRound
in
let ctx = { ctx with date_rounding } in
let scope_input_var =
Var.make (Mark.remove (ScopeName.get_info scope_name) ^ "_in")
in
let scope_input_var = Var.make (ScopeName.base scope_name ^ "_in") in
let scope_input_struct_name = scope_sig.scope_sig_input_struct in
let scope_return_struct_name = scope_sig.scope_sig_output_struct in
let pos_sigma = Mark.get sigma_info in
@ -845,7 +842,7 @@ let translate_program (prgm : 'm S.program) : 'm Ast.program =
let scope_path = ScopeName.path scope_name in
let scope_ref =
if scope_path = [] then
let v = Var.make (Mark.remove (ScopeName.get_info scope_name)) in
let v = Var.make (ScopeName.base scope_name) in
Local_scope_ref v
else
External_scope_ref
@ -928,7 +925,7 @@ let translate_program (prgm : 'm S.program) : 'm Ast.program =
let toplevel_vars =
TopdefName.Map.mapi
(fun name (_, ty, _vis) ->
Var.make (Mark.remove (TopdefName.get_info name)), Mark.remove ty)
Var.make (TopdefName.base name), Mark.remove ty)
prgm.S.program_topdefs
in
let ctx =

View File

@ -309,8 +309,7 @@ let build_exceptions_graph
| None ->
RuleName.Map.add rule_to
(LabelName.fresh
( "exception_to_" ^ Mark.remove (RuleName.get_info rule_to),
Pos.no_pos ))
("exception_to_" ^ RuleName.to_string rule_to, Pos.no_pos))
exception_to_rule_implicit_labels)
| _ -> exception_to_rule_implicit_labels)
def RuleName.Map.empty
@ -333,8 +332,7 @@ let build_exceptions_graph
| None ->
LabelName.Map.add label_to
(LabelName.fresh
( "exception_to_" ^ Mark.remove (LabelName.get_info label_to),
Pos.no_pos ))
("exception_to_" ^ LabelName.to_string label_to, Pos.no_pos))
exception_to_label_implicit_labels)
| _ -> exception_to_label_implicit_labels)
def LabelName.Map.empty

View File

@ -355,7 +355,7 @@ let transform_closures_program ~flags (p : 'm program) : 'm program Bindlib.box
let ctx =
{
decl_ctx = p.decl_ctx;
name_context = new_context (Mark.remove (ScopeName.get_info name));
name_context = new_context (ScopeName.base name);
flags;
globally_bound_vars = toplevel_vars;
}
@ -384,8 +384,7 @@ let transform_closures_program ~flags (p : 'm program) : 'm program Bindlib.box
let ctx =
{
decl_ctx = p.decl_ctx;
name_context =
new_context (Mark.remove (TopdefName.get_info name));
name_context = new_context (TopdefName.base name);
flags;
globally_bound_vars = toplevel_vars;
}
@ -401,8 +400,7 @@ let transform_closures_program ~flags (p : 'm program) : 'm program Bindlib.box
let ctx =
{
decl_ctx = p.decl_ctx;
name_context =
new_context (Mark.remove (TopdefName.get_info name));
name_context = new_context (TopdefName.base name);
flags;
globally_bound_vars = toplevel_vars;
}
@ -618,9 +616,7 @@ let rec hoist_closures_code_item_list
| Topdef (name, ty, vis, (EAbs { binder; tys }, m)) ->
let v, expr = Bindlib.unmbind binder in
let new_hoisted_closures, new_expr =
hoist_closures_expr flags
(new_context (Mark.remove (TopdefName.get_info name)))
expr
hoist_closures_expr flags (new_context (TopdefName.base name)) expr
in
let new_binder = Expr.bind v new_expr in
( new_hoisted_closures,
@ -629,9 +625,7 @@ let rec hoist_closures_code_item_list
(Expr.Box.lift (Expr.eabs new_binder tys m)) )
| Topdef (name, ty, vis, expr) ->
let new_hoisted_closures, new_expr =
hoist_closures_expr flags
(new_context (Mark.remove (TopdefName.get_info name)))
expr
hoist_closures_expr flags (new_context (TopdefName.base name)) expr
in
( new_hoisted_closures,
Bindlib.box_apply

View File

@ -144,9 +144,9 @@ let format_struct_name (fmt : Format.formatter) (v : StructName.t) : unit =
Uid.Path.format fmt path;
Format.pp_print_char fmt '.');
assert (
let n = Mark.remove (StructName.get_info v) in
let n = StructName.base v in
n = String.capitalize_ascii n);
Format.pp_print_string fmt (Mark.remove (StructName.get_info v))
Format.pp_print_string fmt (StructName.base v)
let format_to_module_name
(fmt : Format.formatter)
@ -255,10 +255,8 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
in
Uid.Path.format fmt path;
match Mark.remove name with
| External_value name ->
format_var_str fmt (Mark.remove (TopdefName.get_info name))
| External_scope name ->
format_var_str fmt (Mark.remove (ScopeName.get_info name)))
| External_value name -> format_var_str fmt (TopdefName.base name)
| External_scope name -> format_var_str fmt (ScopeName.base name))
| ETuple es ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list

View File

@ -595,10 +595,7 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
in
let new_scope_body =
translate_scope_body_expr
{
inner_ctx with
context_name = Mark.remove (ScopeName.get_info name);
}
{ inner_ctx with context_name = ScopeName.base name }
scope_body_expr
in
let func_id, outer_ctx =
@ -636,10 +633,7 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
([], ctxt_inner) args abs.tys
in
let ctxt_inner =
{
ctxt_inner with
context_name = Mark.remove (TopdefName.get_info name);
}
{ ctxt_inner with context_name = TopdefName.base name }
in
translate_expr ctxt_inner expr, List.rev rargs_id
in
@ -668,12 +662,7 @@ let translate_program ~(config : translation_config) (p : 'm L.program) :
| Topdef (name, topdef_ty, _vis, expr) ->
(* Toplevel constant def *)
let block, expr, _ren_ctx_inner =
let ctxt =
{
ctxt with
context_name = Mark.remove (TopdefName.get_info name);
}
in
let ctxt = { ctxt with context_name = TopdefName.base name } in
translate_expr ctxt expr
in
let var_id, ctxt =

View File

@ -62,7 +62,7 @@ let c_keywords =
"while";
]
let is_dummy_var v = Mark.remove (VarName.get_info v) = "_"
let is_dummy_var v = VarName.to_string v = "_"
(* this is the marker of a variable that's not expected to be used TODO: mark
and/or detect such variables in a better way *)
@ -118,18 +118,14 @@ let rec format_typ
Format.fprintf fmt "%scatala_closure*%t" sconst element_name
| TTuple _ -> Format.fprintf fmt "%sCATALA_TUPLE%t" sconst element_name
| TStruct s ->
Format.fprintf fmt "%s%s*%t" sconst
(Mark.remove (StructName.get_info s))
element_name
Format.fprintf fmt "%s%s*%t" sconst (StructName.base s) element_name
| TOption t ->
Format.fprintf fmt "%sCATALA_OPTION(%a)%t" sconst
(format_typ decl_ctx ~const:false ignore)
t element_name
| TDefault t -> format_typ decl_ctx ~const element_name fmt t
| TEnum e ->
Format.fprintf fmt "%s%s*%t" sconst
(Mark.remove (EnumName.get_info e))
element_name
Format.fprintf fmt "%s%s*%t" sconst (EnumName.base e) element_name
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hv 4>@[<hov 4>%a@]@,@[<hov 1>(%a)@]@]"
(format_typ decl_ctx ~const (fun fmt ->
@ -154,20 +150,19 @@ let format_ctx
let fields = StructField.Map.bindings struct_fields in
if fields = [] then
Format.fprintf fmt "@,@[<v 2>typedef void %s;@]"
(Mark.remove (StructName.get_info struct_name))
(StructName.base struct_name)
else
Format.fprintf fmt "@,@[<v 2>typedef struct %s {@ %a@;<1 -2>}@] %s;"
(Mark.remove (StructName.get_info struct_name))
(StructName.base struct_name)
(Format.pp_print_list ~pp_sep:Format.pp_print_space
(fun fmt (struct_field, struct_field_type) ->
Format.fprintf fmt "@[<hov>%a;@]"
(format_typ ~const:true ctx (fun fmt ->
Format.pp_print_space fmt ();
Format.pp_print_string fmt
(Mark.remove (StructField.get_info struct_field))))
StructField.format fmt struct_field))
struct_field_type))
fields
(Mark.remove (StructName.get_info struct_name))
(StructName.base struct_name)
in
let format_enum_decl fmt (enum_name, enum_cons) =
if EnumConstructor.Map.is_empty enum_cons then
@ -175,30 +170,27 @@ let format_ctx
else
Format.fprintf fmt "@,@[<v 2>enum %s_code {@,%a@;<0 -2>}@] %s_code;@,"
(* TODO: properly generate a clash-free ident for <enum>_code *)
(Mark.remove (EnumName.get_info enum_name))
(EnumName.base enum_name)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt (enum_cons, _) -> EnumConstructor.format fmt enum_cons))
(EnumConstructor.Map.bindings enum_cons)
(Mark.remove (EnumName.get_info enum_name));
(EnumName.base enum_name);
Format.fprintf fmt
"@,\
@[<v 2>typedef struct %s {@ enum %s_code code;@ @[<v 2>union {@ %a@]@,\
} payload;@]@,\
} %s;"
(Mark.remove (EnumName.get_info enum_name))
(Mark.remove (EnumName.get_info enum_name))
} %s;" (EnumName.base enum_name) (EnumName.base enum_name)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(fun fmt (enum_cons, typ) ->
Format.fprintf fmt "@[<hov 2>%a;@]"
(format_typ ~const:true ctx (fun fmt ->
Format.pp_print_space fmt ();
Format.pp_print_string fmt
(Mark.remove (EnumConstructor.get_info enum_cons))))
EnumConstructor.format fmt enum_cons))
typ))
(EnumConstructor.Map.bindings enum_cons)
(Mark.remove (EnumName.get_info enum_name))
(EnumName.base enum_name)
in
let is_in_type_ordering s =
@ -286,7 +278,7 @@ let rec format_expression
| _ -> "(", ")"
in
Format.fprintf fmt "%s%a%s->%s" lpar format_expression e1 rpar
(Mark.remove (StructField.get_info field))
(StructField.to_string field)
| EInj { e1; cons; name = enum_name; _ }
when EnumName.equal enum_name Expr.option_enum ->
if EnumConstructor.equal cons Expr.none_constr then
@ -413,16 +405,16 @@ let rec format_statement
StructField.Map.iter
(fun field expr ->
Format.fprintf fmt "@,@[<hov 2>%a->%s =@ %a;@]" VarName.format v
(Mark.remove (StructField.get_info field))
(StructField.to_string field)
(format_expression ctx env)
expr)
fields
| SLocalDef { name = v, _; expr = EInj { e1; cons; name; _ }, _; _ }
when not (EnumName.equal name Expr.option_enum) ->
Format.fprintf fmt "@,@[<hov 2>%a->code = %s;@]" VarName.format v
(Mark.remove (EnumConstructor.get_info cons));
(EnumConstructor.to_string cons);
Format.fprintf fmt "@,@[<hov 2>%a->payload.%s = %a;@]" VarName.format v
(Mark.remove (EnumConstructor.get_info cons))
(EnumConstructor.to_string cons)
(format_expression ctx env)
e1
| SLocalDef
@ -545,18 +537,18 @@ let rec format_statement
switch_var;
List.iter2
(fun { case_block; payload_var_name; payload_var_typ } (cons_name, _) ->
Format.fprintf fmt "@,@[<v 2>case %s: {"
(Mark.remove (EnumConstructor.get_info cons_name));
Format.fprintf fmt "@,@[<v 2>case %a: {" EnumConstructor.format
cons_name;
if
(not (Type.equal payload_var_typ (TLit TUnit, Pos.no_pos)))
&& not (is_dummy_var payload_var_name)
then
Format.fprintf fmt "@ @[<hov 2>%a = %a->payload.%s;@]"
Format.fprintf fmt "@ @[<hov 2>%a = %a->payload.%a;@]"
(format_typ ctx.decl_ctx ~const:true (fun fmt ->
Format.pp_print_space fmt ();
VarName.format fmt payload_var_name))
payload_var_typ VarName.format switch_var
(Mark.remove (EnumConstructor.get_info cons_name));
payload_var_typ VarName.format switch_var EnumConstructor.format
cons_name;
Format.fprintf fmt "%a@ break;@;<1 -2>}@]" (format_block ctx env)
case_block)
cases
@ -602,14 +594,9 @@ and format_block (ctx : ctx) (env : env) (fmt : Format.formatter) (b : block) :
then false, fun fmt -> Format.fprintf fmt "0"
else
( false,
fun fmt ->
Format.fprintf fmt "sizeof(%s)"
(Mark.remove (StructName.get_info name)) )
fun fmt -> Format.fprintf fmt "sizeof(%s)" (StructName.base name) )
| TEnum name ->
( false,
fun fmt ->
Format.fprintf fmt "sizeof(%s)"
(Mark.remove (EnumName.get_info name)) )
false, fun fmt -> Format.fprintf fmt "sizeof(%s)" (EnumName.base name)
| TTuple _ when is_closure_typ typ ->
false, fun fmt -> Format.pp_print_string fmt "sizeof(catala_closure)"
| TTuple ts ->

View File

@ -681,7 +681,7 @@ let translate_rule
(String.concat "."
[
Mark.remove (ScopeVar.get_info (Mark.remove v));
Mark.remove (ScopeVar.get_info var_within_origin_scope);
ScopeVar.to_string var_within_origin_scope;
])
in
let typ =

View File

@ -660,8 +660,8 @@ let rec evaluate_expr :
let runtime_path =
( List.map ModuleName.to_string path,
match Mark.remove name with
| External_value name -> Mark.remove (TopdefName.get_info name)
| External_scope name -> Mark.remove (ScopeName.get_info name) )
| External_value name -> TopdefName.base name
| External_scope name -> ScopeName.base name )
(* we have the guarantee that the two cases won't collide because they
have different capitalisation rules inherited from the input *)
in

View File

@ -174,7 +174,7 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
| TStruct name ->
let s = StructName.Map.find name ctx.ctx_decl.ctx_structs in
let get_fieldname (fn : StructField.t) : string =
Mark.remove (StructField.get_info fn)
StructField.to_string fn
in
let fields =
List.map2
@ -187,9 +187,7 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
let fields_str = String.concat " " fields in
Format.asprintf "%s { %s }"
(Mark.remove (StructName.get_info name))
fields_str
Format.asprintf "%s { %s }" (StructName.base name) fields_str
| TTuple _ ->
failwith "[Z3 model]: Pretty-printing of unnamed structs not supported"
| TEnum name ->
@ -203,7 +201,7 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
List.find
(fun (ctr, _) ->
(* FIXME: don't match on strings *)
String.equal fd_name (Mark.remove (EnumConstructor.get_info ctr)))
String.equal fd_name (EnumConstructor.to_string ctr))
(EnumConstructor.Map.bindings enum_ctrs)
in
@ -303,7 +301,7 @@ and find_or_create_enum (ctx : context) (enum : EnumName.t) :
(* Creates a Z3 constructor corresponding to the Catala constructor [c] *)
let create_constructor (name : EnumConstructor.t) (ty : typ) (ctx : context) :
context * Datatype.Constructor.constructor =
let name = Mark.remove (EnumConstructor.get_info name) in
let name = EnumConstructor.to_string name in
let ctx, arg_z3_ty = translate_typ ctx (Mark.remove ty) in
(* The mk_constructor_s Z3 function is not so well documented. From my
@ -337,9 +335,7 @@ and find_or_create_enum (ctx : context) (enum : EnumName.t) :
ctrs (ctx, [])
in
let z3_enum =
Datatype.mk_sort_s ctx.ctx_z3
(Mark.remove (EnumName.get_info enum))
(List.rev z3_ctrs)
Datatype.mk_sort_s ctx.ctx_z3 (EnumName.base enum) (List.rev z3_ctrs)
in
add_z3enum enum z3_enum ctx, z3_enum
@ -352,12 +348,11 @@ and find_or_create_struct (ctx : context) (s : StructName.t) :
match StructName.Map.find_opt s ctx.ctx_z3structs with
| Some s -> ctx, s
| None ->
let s_name = Mark.remove (StructName.get_info s) in
let s_name = StructName.base s in
let fields = StructName.Map.find s ctx.ctx_decl.ctx_structs in
let z3_fieldnames =
List.map
(fun f ->
Mark.remove (StructField.get_info f) |> Symbol.mk_string ctx.ctx_z3)
(fun f -> StructField.to_string f |> Symbol.mk_string ctx.ctx_z3)
(StructField.Map.keys fields)
in
let ctx, z3_fieldtypes_rev =