GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 20:03:27 +03:00
Code Issues Projects Releases Wiki Activity

Allow a value parameter to be defined by another value parameter.

Browse Source
This commit is contained in:
Iavor Diatchki 2017-10-18 13:36:37 -07:00
parent 1cbbba7c32
commit 432638a77a
1 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Cryptol/TypeCheck/CheckModuleInstance.hs
View File

@ -119,17 +119,21 @@ checkTyParams func inst =
checkValParams :: Module {- ^ Parameterized module -} ->
checkValParams :: Module {- ^ Parameterized module -} ->
Map TParam Type {- ^ Type instantiations -} ->
Module {- ^ Instantiation module -} ->
Module {- ^ Instantiation module -} ->
InferM (Map Name Expr)
-- ^ Definitions for the parameters
checkValParams func tMap inst =
Map.fromList <$> mapM checkParam (Map.toList (mParamFuns func))
where
valMap = Map.fromList [ (nameIdent (dName d), (dName d, dSignature d))
valMap = Map.fromList (defByParam ++ defByDef)
defByDef = [ (nameIdent (dName d), (dName d, dSignature d))
| dg <- mDecls inst, d <- groupDecls dg ]
defByParam = [ (nameIdent x, (x, s)) | (x,s) <- Map.toList (mParamFuns inst) ]
su = listSubst [ (TVBound x, t) | (x,t) <- Map.toList tMap ]
checkParam (x,sP) =