Merge pull request #254 from Nadrieril/declarationgroup-mixed

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

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;

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

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

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

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

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