Merge pull request #254 from Nadrieril/declarationgroup-mixed

8 files changed, 19 insertions, 10 deletions

diff --git a/charon-pin b/charon-pin
index 838e423c..e4f6e42a 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c
+61685783db8135df945e53b302dc3e364b7892ee
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 815c470f..e0a86145 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -223,6 +223,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
         let global = GlobalDeclId.Map.find id globals_map in
         analyze_fun_decl_group (NonRecGroup global.body);
         analyze_decl_groups decls'
+    | MixedGroup ids :: _ ->
+        craise_opt_span __FILE__ __LINE__ None
+          ("Mixed declaration groups are not supported yet: ["
+          ^ String.concat ", "
+              (List.map Charon.PrintGAst.any_decl_id_to_string
+                 (Charon.GAstUtils.g_declaration_group_to_list ids))
+          ^ "]")
   in
 
   analyze_decl_groups m.declarations;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 7e292906..075672fe 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -17,7 +17,7 @@ module SA = SymbolicAst
 let log = Logging.interpreter_log
 
 let compute_contexts (m : crate) : decls_ctx =
-  let type_decls_list, _, _, _, _ = split_declarations m.declarations in
+  let type_decls_list, _, _, _, _, _ = split_declarations m.declarations in
   let type_decls = m.type_decls in
   let fun_decls = m.fun_decls in
   let global_decls = m.global_decls in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 76793548..90dadbcc 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -5,7 +5,6 @@ open Charon.PrintTypes
 open Charon.PrintExpressions
 open Charon.PrintLlbcAst.Ast
 open Types
-open TypesUtils
 open Values
 open ValuesUtils
 open Expressions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 23c0782a..0474d233 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -820,6 +820,9 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     | TraitImplGroup id ->
         if config.extract_trait_impls && config.extract_transparent then
           export_trait_impl id
+    | MixedGroup _ ->
+        craise_opt_span __FILE__ __LINE__ None
+          "Mixed-recursive declaration groups are not supported"
   in
 
   (* If we need to export the state type: we try to export it after we defined
diff --git a/flake.lock b/flake.lock
index 948d25d2..a35ba103 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1718897879,
-        "narHash": "sha256-sRbyKlrsEgx7FYDjlYeQpT8wLUgfBiNnMqEQ5029K14=",
+        "lastModified": 1718979132,
+        "narHash": "sha256-MZbG1JOuKpV47fVfi+OhUsf3uRG+ln2KseMNitxqHmQ=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c",
+        "rev": "61685783db8135df945e53b302dc3e364b7892ee",
         "type": "github"
       },
       "original": {
diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh
index 1fa706ae..304b2d83 100755
--- a/scripts/update-charon-pin.sh
+++ b/scripts/update-charon-pin.sh
@@ -5,7 +5,7 @@ if ! which jq 2> /dev/null 1>&2; then
 fi
 
 if [ -L charon ]; then
-    echo '`./charon` is a symlink; we using the commit there for our new pin.'
+    echo '`./charon` is a symlink; we will use the commit there for our new pin.'
     COMMIT="$(git -C charon rev-parse HEAD)"
     nix flake lock --override-input charon "github:aeneasverif/charon/$COMMIT"
 else
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index dffbb470..df80ccc6 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -11,7 +11,7 @@ Uncaught exception:
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 839, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 966, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1515, characters 5-42
 Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66