Skip to content
Snippets Groups Projects
Commit 1b4513eb authored by Samuel Hym's avatar Samuel Hym
Browse files

Collect types also for non-monadic functions

Primitive operations in C world, such as `==`, `&&`, etc. are naturally
represented as non-monadic functions in Gallina.

With this patch, given this code:

    do x <- returnM (eqb y z) ;
    ...

the type for x is properly generated as the return type of eqb, without
requiring an explicit definition of a monadic lifting of eqb.
parent 14467551
Branches
No related tags found
No related merge requests found
...@@ -250,13 +250,16 @@ type SymbolTable = Map.Map Id VTyp ...@@ -250,13 +250,16 @@ type SymbolTable = Map.Map Id VTyp
-- | Extract the "symbol type" -- | Extract the "symbol type"
-- --
-- * if it is a function, the type of the value it returns -- * if it is a monadic function, the type of the value inside the
-- monad
-- * if it is a non-monadic function, the type of the value it returns
-- * if it is a global variable, its type -- * if it is a global variable, its type
extractSymbolType :: ConversionParams -> Type -> Either ErrorMsg VTyp extractSymbolType :: ConversionParams -> Type -> Either ErrorMsg VTyp
extractSymbolType _ (Glob ty []) = pure ty extractSymbolType _ (Glob ty []) = pure ty
extractSymbolType cp typ = go typ extractSymbolType cp typ = go typ
where go (Arrow _ ty) = go ty where go (Arrow _ ty) = go ty
go (Glob m [Glob ty []]) | m == monad cp = pure ty go (Glob m [Glob ty []]) | m == monad cp = pure ty
go (Glob ty []) = pure ty
go ty = Left $ impossibleType ty go ty = Left $ impossibleType ty
impossibleType ty = "Impossible to extract symbol type of: " ++ show ty impossibleType ty = "Impossible to extract symbol type of: " ++ show ty
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment