From 419604c2a63cb91307a9b32cc0067428bfd418af Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Sat, 12 Oct 2024 11:39:27 +0200 Subject: [PATCH 1/3] feat(restricted-open): add debug for `find_binders_for_datacons` --- src/syntax/FStarC.Syntax.DsEnv.fst | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index d9aef097e73..8010caa0813 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -1051,15 +1051,20 @@ let find_data_constructors_for_typ env (lid:lident) = | _ -> None in resolve_in_open_namespaces' env lid (fun _ -> None) (fun _ -> None) k_global_def -let find_binders_for_datacons env (lid:lident) = - let k_global_def lid = function - | ({ sigel = Sig_datacon {t} }, _) -> - arrow_formals_comp_ln t - |> fst - |> List.map (fun x -> x.binder_bv.ppname) - |> Some - | _ -> None in - resolve_in_open_namespaces' env lid (fun _ -> None) (fun _ -> None) k_global_def +let find_binders_for_datacons: env -> lident -> option (list ident) = + let debug = FStarC.Compiler.Debug.get_toggle "open_include_restrictions" in + fun env lid -> + let ns = ns_of_lid lid in + let k_global_def lid = function + | ({ sigel = Sig_datacon {t} }, _) -> + arrow_formals_comp_ln t + |> fst + |> List.map (fun x -> x.binder_bv.ppname) + |> Some + | _ -> None in + let result = resolve_in_open_namespaces' env lid (fun _ -> None) (fun _ -> None) k_global_def in + if !debug then print_endline ("find_binders_for_datacons(_, " ^ show lid ^ ") = " ^ show result); + result (** Elaborates a `restriction`: this function adds implicit names (projectors, discriminators, record fields) that F* generates From 1d6bd9125a279533c3818617b786455a18ab14bc Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Sat, 12 Oct 2024 11:40:15 +0200 Subject: [PATCH 2/3] fix(restricted-open): `find_binders_for_datacons`: skip type params Consider the following type: ```fstar type foo (foo_type_arg1: nat): foo_type_arg2:nat -> Type = | FooConstructor : foo_cons_arg1:nat -> foo foo_type_arg1 12 ``` Function `find_binders_for_datacons` exporting `foo_type_arg1`, `foo_type_arg2` and `foo_cons_arg1` as binders for the data constructor `FooConstructor`. This is wrong: the first two are indicies of the type. This commit fixes this function, using the field `num_ty_params` from the constructor `Sig_datacon`. --- src/syntax/FStarC.Syntax.DsEnv.fst | 8 +++++--- tests/bug-reports/Bug3522.Def.fst | 12 ++++++++++++ tests/bug-reports/Bug3522.fst | 6 ++++++ 3 files changed, 23 insertions(+), 3 deletions(-) create mode 100644 tests/bug-reports/Bug3522.Def.fst create mode 100644 tests/bug-reports/Bug3522.fst diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index 8010caa0813..4e34a6a6bb5 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -1056,9 +1056,11 @@ let find_binders_for_datacons: env -> lident -> option (list ident) = fun env lid -> let ns = ns_of_lid lid in let k_global_def lid = function - | ({ sigel = Sig_datacon {t} }, _) -> - arrow_formals_comp_ln t - |> fst + | ({ sigel = Sig_datacon {t; num_ty_params} }, _) -> + arrow_formals_comp_ln t |> fst + // The first `num_ty_params` of each constructors of a type are + // type params, not fields of the constructors: we skip those. + |> List.splitAt num_ty_params |> snd |> List.map (fun x -> x.binder_bv.ppname) |> Some | _ -> None in diff --git a/tests/bug-reports/Bug3522.Def.fst b/tests/bug-reports/Bug3522.Def.fst new file mode 100644 index 00000000000..f9effabb827 --- /dev/null +++ b/tests/bug-reports/Bug3522.Def.fst @@ -0,0 +1,12 @@ +module Bug3522.Def + +class a_class (a_type:Type) = { + a_field : a_type -> a_type; +} + +type b_struct (b_type: Type) = { + b_field : b_type -> b_type; +} + +type foo (foo_type_arg1: nat): foo_type_arg2:nat -> Type + = | FooConstructor : foo_cons_arg1:nat -> foo foo_type_arg1 12 diff --git a/tests/bug-reports/Bug3522.fst b/tests/bug-reports/Bug3522.fst new file mode 100644 index 00000000000..849c090e83b --- /dev/null +++ b/tests/bug-reports/Bug3522.fst @@ -0,0 +1,6 @@ +module Bug3522 + +open Bug3522.Def {a_class as x} +open Bug3522.Def {b_struct as y} +open Bug3522.Def {foo as z} + From 08ea031c1978b99127aa077eb0c9fa4eabc1869f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 12 Oct 2024 07:42:03 -0700 Subject: [PATCH 3/3] snap --- .../generated/FStarC_Syntax_DsEnv.ml | 64 +++++++++++++------ 1 file changed, 45 insertions(+), 19 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml index d8057311592..42b0fd752d1 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml @@ -2678,8 +2678,10 @@ let (find_binders_for_datacons : FStarC_Ident.lident -> FStarC_Ident.ident Prims.list FStar_Pervasives_Native.option) = + let debug = FStarC_Compiler_Debug.get_toggle "open_include_restrictions" in fun env1 -> fun lid -> + let ns = FStarC_Ident.ns_of_lid lid in let k_global_def lid1 uu___ = match uu___ with | ({ @@ -2688,29 +2690,53 @@ let (find_binders_for_datacons : FStarC_Syntax_Syntax.us1 = uu___2; FStarC_Syntax_Syntax.t1 = t; FStarC_Syntax_Syntax.ty_lid = uu___3; - FStarC_Syntax_Syntax.num_ty_params = uu___4; - FStarC_Syntax_Syntax.mutuals1 = uu___5; - FStarC_Syntax_Syntax.injective_type_params1 = uu___6;_}; - FStarC_Syntax_Syntax.sigrng = uu___7; - FStarC_Syntax_Syntax.sigquals = uu___8; - FStarC_Syntax_Syntax.sigmeta = uu___9; - FStarC_Syntax_Syntax.sigattrs = uu___10; - FStarC_Syntax_Syntax.sigopens_and_abbrevs = uu___11; - FStarC_Syntax_Syntax.sigopts = uu___12;_}, - uu___13) -> - let uu___14 = - let uu___15 = - let uu___16 = FStarC_Syntax_Util.arrow_formals_comp_ln t in - FStar_Pervasives_Native.fst uu___16 in + FStarC_Syntax_Syntax.num_ty_params = num_ty_params; + FStarC_Syntax_Syntax.mutuals1 = uu___4; + FStarC_Syntax_Syntax.injective_type_params1 = uu___5;_}; + FStarC_Syntax_Syntax.sigrng = uu___6; + FStarC_Syntax_Syntax.sigquals = uu___7; + FStarC_Syntax_Syntax.sigmeta = uu___8; + FStarC_Syntax_Syntax.sigattrs = uu___9; + FStarC_Syntax_Syntax.sigopens_and_abbrevs = uu___10; + FStarC_Syntax_Syntax.sigopts = uu___11;_}, + uu___12) -> + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = FStarC_Syntax_Util.arrow_formals_comp_ln t in + FStar_Pervasives_Native.fst uu___17 in + FStarC_Compiler_List.splitAt num_ty_params uu___16 in + FStar_Pervasives_Native.snd uu___15 in FStarC_Compiler_List.map (fun x -> (x.FStarC_Syntax_Syntax.binder_bv).FStarC_Syntax_Syntax.ppname) - uu___15 in - FStar_Pervasives_Native.Some uu___14 + uu___14 in + FStar_Pervasives_Native.Some uu___13 | uu___1 -> FStar_Pervasives_Native.None in - resolve_in_open_namespaces' env1 lid - (fun uu___ -> FStar_Pervasives_Native.None) - (fun uu___ -> FStar_Pervasives_Native.None) k_global_def + let result = + resolve_in_open_namespaces' env1 lid + (fun uu___ -> FStar_Pervasives_Native.None) + (fun uu___ -> FStar_Pervasives_Native.None) k_global_def in + (let uu___1 = FStarC_Compiler_Effect.op_Bang debug in + if uu___1 + then + let uu___2 = + let uu___3 = + let uu___4 = + FStarC_Class_Show.show FStarC_Ident.showable_lident lid in + let uu___5 = + let uu___6 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_option + (FStarC_Class_Show.show_list + FStarC_Ident.showable_ident)) result in + Prims.strcat ") = " uu___6 in + Prims.strcat uu___4 uu___5 in + Prims.strcat "find_binders_for_datacons(_, " uu___3 in + FStarC_Compiler_Util.print_endline uu___2 + else ()); + result let elab_restriction : 'uuuuu . (env -> FStarC_Ident.lident -> FStarC_Syntax_Syntax.restriction -> 'uuuuu)