diff options
Diffstat (limited to 'source/Checking/Datatype.hs')
| -rw-r--r-- | source/Checking/Datatype.hs | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/source/Checking/Datatype.hs b/source/Checking/Datatype.hs index d694ec8..a47f93d 100644 --- a/source/Checking/Datatype.hs +++ b/source/Checking/Datatype.hs @@ -13,13 +13,9 @@ module Checking.Datatype , CheckedDatatypePremiseView(..) , checkedDatatypeClauseViews , checkedDatatypeGeneratedFacts - , checkedDatatypeFacts - , checkedDatatypeFactRoles ) where import Base -import Checking.Facts -import Checking.Legacy import Report.Location import Syntax.Internal import Syntax.Lexicon @@ -278,50 +274,6 @@ checkedDatatypeGeneratedFacts checkedDatatypeGeneratedFacts = datatypeFacts -checkedDatatypeFacts - :: Location - -> Marker - -> CheckedDatatype - -> NonEmpty StagedFact -checkedDatatypeFacts location blockMarker checked = - fmap stage (datatypeFacts checked) - where - stage (factMarker, formula) = - stageFact - (factMarker :| []) - (factOrigin location blockMarker) - (prepareSemanticFact formula) - -checkedDatatypeFactRoles - :: CheckedDatatype - -> NonEmpty LegacyDatatypeFactRole -checkedDatatypeFactRoles datatype = - appendList - (LegacyDatatypeIntroduction - <$ checkedDatatypeClauses datatype) - ( replicate - (length - (unorderedPairs - (NonEmpty.toList - (checkedDatatypeClauses datatype)))) - LegacyDatatypeDistinctness - <> [ LegacyDatatypeInjectivity - | clause <- - NonEmpty.toList - (checkedDatatypeClauses datatype) - , not - (null - (checkedDatatypeClauseConstructorArgs - clause)) - ] - <> [ LegacyDatatypeCases - , LegacyDatatypeInduction - ] - ) - where - appendList (first :| rest) trailing = - first :| (rest <> trailing) - datatypeFacts :: CheckedDatatype -> NonEmpty (Marker, Formula) datatypeFacts datatype = appendList |