Skip to content

Commit f484512

Browse files
committed
refactor: change updateFFITypes (and calls to)
- this done to make data dependencies clearer, and thus other refactorings more obviously correct.
1 parent 146f57f commit f484512

File tree

1 file changed

+15
-14
lines changed

1 file changed

+15
-14
lines changed

cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -511,10 +511,10 @@ loadCryptolModule sc env path = do
511511
-- command line.
512512

513513
return ( cryptolModule
514-
, updateFFITypes m
515-
env { eModuleEnv = modEnv''
516-
, eTermEnv = newTermEnv
517-
}
514+
, env { eModuleEnv = modEnv''
515+
, eTermEnv = newTermEnv
516+
, eFFITypes = updateFFITypes m newTermEnv (eFFITypes env)
517+
}
518518
-- NOTE here the difference between this function and
519519
-- `importModule`:
520520
-- 1. the `eImports` field is not updated, as
@@ -557,14 +557,14 @@ mkCryptolModule m types newTermEnv =
557557
newTermEnv
558558
)
559559

560-
updateFFITypes :: T.Module -> CryptolEnv -> CryptolEnv
561-
updateFFITypes m env = env { eFFITypes = eFFITypes' }
560+
updateFFITypes :: T.Module -> Map MN.Name Term -> Map NameInfo T.FFI -> Map NameInfo T.FFI
561+
updateFFITypes m eTermEnv' eFFITypes' =
562+
foldr (\(nm, ty) -> Map.insert (getNameInfo nm) ty)
563+
eFFITypes'
564+
(T.findForeignDecls m)
562565
where
563-
eFFITypes' = foldr (\(nm, ty) -> Map.insert (getNameInfo nm) ty)
564-
(eFFITypes env)
565-
(T.findForeignDecls m)
566566
getNameInfo nm =
567-
case Map.lookup nm (eTermEnv env) of
567+
case Map.lookup nm eTermEnv' of
568568
Just tm ->
569569
case asConstant tm of
570570
Just n -> nameInfo n
@@ -685,10 +685,11 @@ importModule sc env src as vis imps = do
685685
locate x = P.Located P.emptyRange x
686686

687687
return $
688-
(updateFFITypes m env{ eModuleEnv = modEnv'
689-
, eTermEnv = newTermEnv
690-
})
691-
{eImports = newImport : eImports env}
688+
env{ eModuleEnv = modEnv'
689+
, eTermEnv = newTermEnv
690+
, eFFITypes = updateFFITypes m newTermEnv (eFFITypes env)
691+
, eImports = newImport : eImports env
692+
}
692693

693694
bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv)
694695
bindIdent ident env = (name, env')

0 commit comments

Comments
 (0)