From 1b4513eb87fd71ad56363fc62a7536c7d206588e Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@univ-lille.fr>
Date: Mon, 30 May 2022 18:47:56 +0200
Subject: [PATCH] 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.
---
src/Language/Coq/Deep.hs | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/Language/Coq/Deep.hs b/src/Language/Coq/Deep.hs
index 8496e95..a415a7a 100644
--- a/src/Language/Coq/Deep.hs
+++ b/src/Language/Coq/Deep.hs
@@ -250,13 +250,16 @@ type SymbolTable = Map.Map Id VTyp
-- | 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
extractSymbolType :: ConversionParams -> Type -> Either ErrorMsg VTyp
extractSymbolType _ (Glob ty []) = pure ty
extractSymbolType cp typ = go typ
where go (Arrow _ ty) = go ty
go (Glob m [Glob ty []]) | m == monad cp = pure ty
+ go (Glob ty []) = pure ty
go ty = Left $ impossibleType ty
impossibleType ty = "Impossible to extract symbol type of: " ++ show ty
--
GitLab