File tree Expand file tree Collapse file tree 1 file changed +9
-1
lines changed
cryptol-saw-core/src/CryptolSAWCore Expand file tree Collapse file tree 1 file changed +9
-1
lines changed Original file line number Diff line number Diff line change @@ -586,7 +586,11 @@ updateFFITypes m env = env { eFFITypes = eFFITypes' }
586586bindCryptolModule :: (P. ModName , CryptolModule ) -> CryptolEnv -> CryptolEnv
587587bindCryptolModule (modName, CryptolModule sm tm) env =
588588 env { eExtraNames = flip (foldr addName) (Map. keys tm') $
589- flip (foldr addTSyn) (Map. keys sm) $ eExtraNames env
589+ flip (foldr addTSyn) (Map. keys sm) $
590+ flip (foldr addSubModule) (Map. keys tm') $
591+ -- FIXME: This added function doesn't really
592+ -- fix the submodule support bugs.
593+ eExtraNames env
590594 , eExtraTSyns = Map. union sm (eExtraTSyns env)
591595 , eExtraTypes = Map. union (fmap fst tm') (eExtraTypes env)
592596 , eTermEnv = Map. union (fmap snd tm') (eTermEnv env)
@@ -599,6 +603,10 @@ bindCryptolModule (modName, CryptolModule sm tm) env =
599603 f _ = Nothing
600604
601605 addName name = MN. shadowing (MN. singletonNS C. NSValue (P. mkQual modName (MN. nameIdent name)) name)
606+ -- FIXME: suspicious. (we need to do any C.NSModule?)
607+
608+ addSubModule name = MN. shadowing (MN. singletonNS C. NSModule (P. mkQual modName (MN. nameIdent name)) name)
609+
602610 addTSyn name = MN. shadowing (MN. singletonNS C. NSType (P. mkQual modName (MN. nameIdent name)) name)
603611
604612-- | NOTE: this is only used in the "cryptol_extract" primitive.
You can’t perform that action at this time.
0 commit comments