From f7528e661dbeb377df9a25ad1c3ccd474e53bd67 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Thu, 5 May 2022 13:15:30 -0400 Subject: [PATCH 1/2] Resolve URI-based names when loading the external SAWCore format --- saw-core/src/Verifier/SAW/ExternalFormat.hs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs index 851fbf2b57..1f6c7586da 100644 --- a/saw-core/src/Verifier/SAW/ExternalFormat.hs +++ b/saw-core/src/Verifier/SAW/ExternalFormat.hs @@ -272,13 +272,16 @@ scReadExternal sc input = lift (scResolveNameByURI sc (moduleIdentToURI ident)) >>= \case Just vi' -> pure (EC vi' nmi t') Nothing -> lift $ fail $ "scReadExternal: missing module identifier: " ++ show ident - _ -> - case Map.lookup vi vs of - Just vi' -> pure $ EC vi' nmi t' - Nothing -> - do vi' <- lift $ scFreshGlobalVar sc - State.put (ts, nms, Map.insert vi vi' vs) - pure $ EC vi' nmi t' + ImportedName uri _aliases -> + lift (scResolveNameByURI sc uri) >>= \case + Just vi' -> pure (EC vi' nmi t') + Nothing -> case Map.lookup vi vs of + Just vi' -> pure $ EC vi' nmi t' + Nothing -> + do vi' <- lift $ scFreshGlobalVar sc + State.put (ts, nms, Map.insert vi vi' vs) + liftIO $ print (vi', nmi) + pure $ EC vi' nmi t' readEC :: String -> String -> ReadM (ExtCns Term) readEC i t = From 9d1c02c54a866a42d0e46c5a2a5916193fcb5f82 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 9 May 2022 15:47:56 -0400 Subject: [PATCH 2/2] Remove a debug print statement --- saw-core/src/Verifier/SAW/ExternalFormat.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs index 1f6c7586da..13b69f7a0e 100644 --- a/saw-core/src/Verifier/SAW/ExternalFormat.hs +++ b/saw-core/src/Verifier/SAW/ExternalFormat.hs @@ -280,7 +280,6 @@ scReadExternal sc input = Nothing -> do vi' <- lift $ scFreshGlobalVar sc State.put (ts, nms, Map.insert vi vi' vs) - liftIO $ print (vi', nmi) pure $ EC vi' nmi t' readEC :: String -> String -> ReadM (ExtCns Term)