GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

FFI: Use evalFinType in marshalTyArg

Browse Source
This commit is contained in:
Bretton 2022-08-10 14:52:58 -07:00
parent 7ae7489553
commit c6162c6a8e
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Cryptol/Eval/FFI.hs
View File

@ -46,7 +46,6 @@ import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
@ -136,13 +135,11 @@ foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes []
-- Look up the value of a type parameter in the type environment and marshal
-- it.
marshalTyArg :: TParam -> Eval SomeFFIArg
marshalTyArg tp = case lookupTypeVar (TVBound tp) tenv of
Just (Left (Nat n))
| n <= toInteger (maxBound :: CSize) ->
pure $ SomeFFIArg @CSize $ fromInteger n
| otherwise -> raiseError Concrete $ FFITypeNumTooBig name tp n
x -> evalPanic "marshalTyArg"
["Bad type env lookup", show name, show tp, show x]
marshalTyArg tp
| n <= toInteger (maxBound :: CSize) =
pure $ SomeFFIArg @CSize $ fromInteger n
| otherwise = raiseError Concrete $ FFITypeNumTooBig name tp n
where n = evalFinType $ TVar $ TVBound tp
-- Marshal the given value as the given FFIType and call the given function
-- with the results. A single Cryptol argument may correspond to any number of