diff options
| -rw-r--r-- | charon-pin | 2 | ||||
| -rw-r--r-- | compiler/AssociatedTypes.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 1 | ||||
| -rw-r--r-- | flake.lock | 6 |
4 files changed, 7 insertions, 6 deletions
@@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -c049120c15567d22520c94f570363eb4948d849f +7cb5b367aec5768bee003d395634b30e13638b7d diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 27425a51..c0c5399f 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -95,7 +95,7 @@ let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = match id with | Self | Clause _ -> true | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ - | Closure _ -> + | Closure _ | Unsolved _ -> false | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> trait_instance_id_is_local_clause id @@ -443,7 +443,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) | Closure (fid, generics) -> let generics = norm_ctx_normalize_generic_args ctx generics in (Closure (fid, generics), None) - | UnknownTrait _ -> + | Unsolved _ | UnknownTrait _ -> (* This is actually an error case *) (id, None) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 4aa24fcf..3e22d36b 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -462,6 +462,7 @@ and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty) | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr) | FnPointer _ | Closure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | Unsolved _ -> craise __FILE__ __LINE__ meta "Couldn't solve trait bound" | UnknownTrait s -> craise __FILE__ __LINE__ meta ("Unknown trait found: " ^ s) (** Translate a signature type - TODO: factor out the different translation functions *) @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1716398715, - "narHash": "sha256-z4COmDxa3DY6pVLgB85n6EVWFPkx87tr+xkJGiQvpV8=", + "lastModified": 1716542431, + "narHash": "sha256-Q+WLCH7teTpBG1ScWi5VsvpjNmUrgDSv6I6Vv8CLkaM=", "owner": "aeneasverif", "repo": "charon", - "rev": "c049120c15567d22520c94f570363eb4948d849f", + "rev": "7cb5b367aec5768bee003d395634b30e13638b7d", "type": "github" }, "original": { |