diff options
author | Son HO | 2024-04-12 19:21:29 +0200 |
---|---|---|
committer | GitHub | 2024-04-12 19:21:29 +0200 |
commit | 67eaff0b90d693c86d9848cbf598e7c86caba4c4 (patch) | |
tree | c3b5975b5880e93a96d412d7aca893eda42ea860 /compiler/TranslateCore.ml | |
parent | 03a175b423c9ccff2160300c4d349978f9b1aeb9 (diff) | |
parent | 43ff0300e97ad275fa9b62e89577c754f12e3aa3 (diff) |
Merge pull request #124 from AeneasVerif/son/lean1
Add more definitions to the Lean library
Diffstat (limited to 'compiler/TranslateCore.ml')
-rw-r--r-- | compiler/TranslateCore.ml | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index 3e4c7375..688cbe34 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -91,3 +91,22 @@ let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string = in let pat = Charon.NameMatcher.name_to_pattern mctx c n in Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat + +let name_with_generics_to_pattern_string (ctx : trans_ctx) (n : Types.name) + (params : Types.generic_params) (args : Types.generic_args) : string = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; + } + in + let c : Charon.NameMatcher.to_pat_config = + { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs } + in + let pat = + Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args + in + Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat |