diff options
| author | Guillaume Boisseau | 2024-05-06 13:17:45 +0000 |
|---|---|---|
| committer | GitHub | 2024-05-06 13:17:45 +0000 |
| commit | a935064196f7fcc65355726a523508f4317d16ee (patch) | |
| tree | d03ee22990ffa3780d8b3316dc0fd7249c76b6aa | |
| parent | e2983a390de8758640d9e526e1bb9f908813891e (diff) | |
| parent | 8cd1eede6d9fd4c979cf01b48536dfda6b2e6bd6 (diff) | |
Merge pull request #166 from AeneasVerif/afromher/traits
Propagate handling of (unsupported) mutually recursive trait declarations
Diffstat (limited to '')
| -rw-r--r-- | compiler/Translate.ml | 5 | ||||
| -rw-r--r-- | flake.lock | 6 |
2 files changed, 7 insertions, 4 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 222b3c57..72a98c3d 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -798,7 +798,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) (* Translate *) export_functions_group pure_funs | GlobalGroup id -> export_global id - | TraitDeclGroup id -> + | TraitDeclGroup (RecGroup _ids) -> + craise_opt_meta __FILE__ __LINE__ None + "Mutually recursive trait declarations are not supported" + | TraitDeclGroup (NonRecGroup id) -> (* TODO: update to extract groups *) if config.extract_trait_decls && config.extract_transparent then ( export_trait_decl_group id; @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1714668124, - "narHash": "sha256-66QkLemEGCWI+XnGYOA666XLMdrV5PU6Oew2B1fil+4=", + "lastModified": 1715000450, + "narHash": "sha256-N7VGgAwoMeSEYblcKzo7TZWv6upuJdknrnZO1ZSwJWQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "9d08aa01e4c2b94c24c7c79e47191d626a1a03b4", + "rev": "f8fab8d2f4f279f973057d0f7f58c2fd59146e30", "type": "github" }, "original": { |