Resolve URI-based names when loading the external SAWCore format (#1658)

* Resolve URI-based names when loading the external SAWCore format * Remove a debug print statement
GaloisInc · May 10, 2022 · e1d8d9d · e1d8d9d
1 parent e4c2c47
commit e1d8d9d
Showing 1 changed file with 9 additions and 7 deletions.
diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs
@@ -272,13 +272,15 @@ 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)
+                      pure $ EC vi' nmi t'
 
     readEC :: String -> String -> ReadM (ExtCns Term)
     readEC i t =