Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow higher-ranked types #3

Merged
merged 3 commits into from
Jan 30, 2023
Merged

Allow higher-ranked types #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
803babc
Allow higher-ranked types
alexfmpe Jan 7, 2023
6a2ea86
Merge branch 'master' into higher-ranked
alexfmpe Jan 28, 2023
e9f3922
Merge branch 'master' into higher-ranked
alexfmpe Jan 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions free-theorems/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions free-theorems/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions free-theorems/src/Language/Haskell/FreeTheorems/Unfold.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down