Merge pull request #3 from alexfmpe/higher-ranked

Allow higher-ranked types
ichistmeinname · Jan 30, 2023 · 9a84f28 · 9a84f28
2 parents 35ef9db + e9f3922
commit 9a84f28
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 2 deletions.
diff --git a/free-theorems/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs b/free-theorems/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs
@@ -12,7 +12,8 @@ import Control.Monad.Writer (Writer, tell)
 import Data.Generics (everywhere, mkT)
 import Data.Maybe (fromMaybe)
 import Data.List (nub, (\\), intersect)
-import Language.Haskell.Exts.Parser (parseModule, ParseResult(..))
+import Language.Haskell.Exts.Extension (Extension(EnableExtension), KnownExtension(RankNTypes))
+import Language.Haskell.Exts.Parser (defaultParseMode, parseModuleWithMode, ParseMode(..), ParseResult(..))
 import Language.Haskell.Exts.SrcLoc (SrcLoc, SrcSpanInfo, srcFilename, srcColumn, srcLine, fromSrcInfo)
 import Language.Haskell.Exts.Syntax
 --import Language.Haskell.Syntax;
@@ -72,13 +73,15 @@ import Language.Haskell.FreeTheorems.Frontend.Error
 --   successfully.
 
 parse :: String -> Parsed [S.Declaration]
-parse text = case parseModule text of
+parse text = case parseModuleWithMode mode text of
   ParseOk hsModule -> let decls = transform . filterDeclarations $ hsModule
                        in foldM collectDeclarations [] decls
   ParseFailed l _  -> do tell [pp ("Parse error at (" ++ show (srcLine l)
                                    ++ ":" ++ show (srcColumn l) ++ ").")]
                          return []
   where
+    mode = defaultParseMode { extensions = [EnableExtension RankNTypes] }
+
     collectDeclarations :: [S.Declaration] -> Decl SrcSpanInfo -> Parsed [S.Declaration]
     collectDeclarations ds d =
       case mkDeclaration d of

diff --git a/free-theorems/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs b/free-theorems/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs
@@ -328,6 +328,8 @@ prettyTermVariable (TVar v) = text v
 prettyRelation :: PrettyControl -> Bool -> Relation -> Doc
 prettyRelation _ _ (RelVar _ rv) = prettyRelationVariable rv
 
+prettyRelation _ _ (RelConsFunVar _ rv) = prettyRelationVariable rv
+
 prettyRelation pc _ (FunVar ri (Left t)) =
   case theoremType (relationLanguageSubset ri) of
     EquationalTheorem   -> prettyTerm (noParens pc) t

diff --git a/free-theorems/src/Language/Haskell/FreeTheorems/Unfold.hs b/free-theorems/src/Language/Haskell/FreeTheorems/Unfold.hs
@@ -165,6 +165,7 @@ asCompleteTheorem i =
 unfoldFormula :: Term -> Term -> Relation -> Unfolded Formula
 unfoldFormula x y rel = case rel of
   RelVar _ _           -> return . Predicate . IsMember x y $ rel
+  RelConsFunVar _ _    -> return . Predicate . IsMember x y $ rel
   FunVar ri term       -> unfoldTerm x y ri term
   RelBasic ri          -> unfoldBasic x y ri
   RelLift _ _ _        -> return . Predicate . IsMember x y $ rel