summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-06-21 16:25:54 +0200
committerGitHub2024-06-21 16:25:54 +0200
commitf264b9dcc6331eb9149d951f308cdc61c8c02801 (patch)
tree2891753ba71bc8ddd3cc367b787a1acddbcf1741 /compiler
parentc8ad44f287215c3c45e5a0f0540ef507b4916c7d (diff)
parentd3f52e23ede39c4fd7845b6c5feb29d28b2a2384 (diff)
Merge pull request #254 from Nadrieril/declarationgroup-mixed
Diffstat (limited to 'compiler')
-rw-r--r--compiler/FunsAnalysis.ml7
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/Print.ml1
-rw-r--r--compiler/Translate.ml3
4 files changed, 11 insertions, 2 deletions
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