From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/ExtractName.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 80ed2ca3..9df5b03e 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,7 @@ 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 = None) (name : pattern) : string list =
   let c = { tgt = TkName } in
   let all_vars =
     let check (g : generic_arg) : bool =
@@ -71,7 +72,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 meta "Unreachable")
         | _ -> super#visit_PImpl () ty
 
       method! visit_EPrimAdt _ adt g =
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/ExtractName.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 9df5b03e..c4e145a0 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -32,7 +32,7 @@ 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 ?(meta = None) (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 =
@@ -92,9 +92,9 @@ let pattern_to_extract_name ?(meta = None) (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
@@ -103,7 +103,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] *)
@@ -125,4 +125,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
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/ExtractName.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index c4e145a0..e9d6116f 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -32,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 (meta : Meta.meta option) (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 =
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/ExtractName.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index e9d6116f..0573512d 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -73,7 +73,7 @@ let pattern_to_extract_name (meta : Meta.meta option) (name : pattern) :
             let id = Collections.List.last id in
             match id with
             | PIdent (_, _) -> super#visit_PImpl () (EComp [ id ])
-            | PImpl _ -> craise_opt_meta meta "Unreachable")
+            | PImpl _ -> craise_opt_meta __FILE__ __LINE__ meta "Unreachable")
         | _ -> super#visit_PImpl () ty
 
       method! visit_EPrimAdt _ adt g =
-- 
cgit v1.2.3