summaryrefslogtreecommitdiff
path: root/compiler/ExtractName.ml
diff options
context:
space:
mode:
authorSon HO2024-03-29 18:02:40 +0100
committerGitHub2024-03-29 18:02:40 +0100
commitf4a89caad1459f2f72295c5baa284fe1f9b4c39f (patch)
tree70237cbc5ff7e0868c9b6918cae21f9bc8ba6272 /compiler/ExtractName.ml
parentbfcec191f68a4cbfab14f5b92a8d6a46d6b02539 (diff)
parent1a86cac476c1f5c0d64d5a12db267d3ac651561b (diff)
Merge pull request #95 from AeneasVerif/escherichia/errors
Escherichia/errors
Diffstat (limited to '')
-rw-r--r--compiler/ExtractName.ml16
1 files changed, 9 insertions, 7 deletions
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 80ed2ca3..0573512d 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -1,6 +1,7 @@
(** Utilities for extracting names *)
open Charon.NameMatcher
+open Errors
let log = Logging.extract_log
let match_with_trait_decl_refs = true
@@ -31,7 +32,8 @@ end
For impl blocks, we simply use the name of the type (without its arguments)
if all the arguments are variables.
*)
-let pattern_to_extract_name (name : pattern) : string list =
+let pattern_to_extract_name (meta : Meta.meta option) (name : pattern) :
+ string list =
let c = { tgt = TkName } in
let all_vars =
let check (g : generic_arg) : bool =
@@ -71,7 +73,7 @@ let pattern_to_extract_name (name : pattern) : string list =
let id = Collections.List.last id in
match id with
| PIdent (_, _) -> super#visit_PImpl () (EComp [ id ])
- | PImpl _ -> raise (Failure "Unreachable"))
+ | PImpl _ -> craise_opt_meta __FILE__ __LINE__ meta "Unreachable")
| _ -> super#visit_PImpl () ty
method! visit_EPrimAdt _ adt g =
@@ -91,9 +93,9 @@ let pattern_to_extract_name (name : pattern) : string list =
let name = visitor#visit_pattern () name in
List.map (pattern_elem_to_string c) name
-let pattern_to_type_extract_name = pattern_to_extract_name
-let pattern_to_fun_extract_name = pattern_to_extract_name
-let pattern_to_trait_impl_extract_name = pattern_to_extract_name
+let pattern_to_type_extract_name = pattern_to_extract_name None
+let pattern_to_fun_extract_name = pattern_to_extract_name None
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name None
(* TODO: this is provisional. We just want to make sure that the extraction
names we derive from the patterns (for the builtin definitions) are
@@ -102,7 +104,7 @@ let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
let c : to_pat_config =
{ tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
in
- pattern_to_extract_name (name_to_pattern ctx c n)
+ pattern_to_extract_name None (name_to_pattern ctx c n)
(** If the [prefix] is Some, we attempt to remove the common prefix
between [prefix] and [name] from [name] *)
@@ -124,4 +126,4 @@ let name_with_generics_to_simple_name (ctx : ctx)
let _, _, name = pattern_common_prefix { equiv = true } prefix name in
name
in
- pattern_to_extract_name name
+ pattern_to_extract_name None name