diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | source/Felix/Cache/Codec.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Checking/Authority.hs (renamed from source/Checking/Authority.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Checking/Backend/Problem.hs (renamed from source/Checking/Backend/Problem.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Checking/Backend/Tptp.hs (renamed from source/Checking/Backend/Tptp.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Checking/Core.hs (renamed from source/Checking/Core.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Checking/Datatype.hs (renamed from source/Checking/Datatype.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Checking/Declaration.hs (renamed from source/Checking/Declaration.hs) | 26 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact.hs (renamed from source/Checking/Exact.hs) | 22 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Datatype.hs (renamed from source/Checking/Exact/Datatype.hs) | 28 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Global.hs (renamed from source/Checking/Exact/Global.hs) | 16 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Inductive.hs (renamed from source/Checking/Exact/Inductive.hs) | 28 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Proof.hs (renamed from source/Checking/Exact/Proof.hs) | 28 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Vocabulary.hs (renamed from source/Checking/Exact/Vocabulary.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Checking/FinalPrelude.hs (renamed from source/Checking/FinalPrelude.hs) | 30 | ||||
| -rw-r--r-- | source/Felix/Checking/Foundation.hs (renamed from source/Checking/Foundation.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Checking/Identity.hs (renamed from source/Checking/Identity.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/Derivation.hs (renamed from source/Checking/Kernel/Derivation.hs) | 10 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/Proof.hs (renamed from source/Checking/Kernel/Proof.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/Semantics.hs (renamed from source/Checking/Kernel/Semantics.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/SetLfp.hs (renamed from source/Checking/Kernel/SetLfp.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Checking/Materialization.hs (renamed from source/Checking/Materialization.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Checking/Module.hs (renamed from source/Checking/Module.hs) | 26 | ||||
| -rw-r--r-- | source/Felix/Checking/Semantic.hs (renamed from source/Checking/Semantic.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Checking/SetConstruction.hs (renamed from source/Checking/SetConstruction.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Checking/Typed/Inductive.hs (renamed from source/Checking/Typed/Inductive.hs) | 16 | ||||
| -rw-r--r-- | source/Felix/CommandLine.hs | 8 | ||||
| -rw-r--r-- | source/Felix/Math/Codec.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Meaning.hs | 12 | ||||
| -rw-r--r-- | source/Felix/OutputPlan.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Parse.hs | 16 | ||||
| -rw-r--r-- | source/Felix/Parsed/Identity.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Parsed/Payload.hs | 10 | ||||
| -rw-r--r-- | source/Felix/Prelude.hs | 8 | ||||
| -rw-r--r-- | source/Felix/Provers.hs | 8 | ||||
| -rw-r--r-- | source/Felix/Render/Html.hs (renamed from source/Render/Html.hs) | 13 | ||||
| -rw-r--r-- | source/Felix/Render/Html/Context.hs (renamed from source/Render/Html/Context.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Render/Html/Export.hs (renamed from source/Render/Html/Export.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Render/Html/Layout.hs (renamed from source/Render/Html/Layout.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Render/Html/Output.hs (renamed from source/Render/Html/Output.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Report/Location.hs (renamed from source/Report/Location.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Source.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Source/Graph.hs | 4 | ||||
| -rw-r--r-- | source/Felix/Store.hs | 12 | ||||
| -rw-r--r-- | source/Felix/Syntax/Abstract.hs (renamed from source/Syntax/Abstract.hs) | 14 | ||||
| -rw-r--r-- | source/Felix/Syntax/Adapt.hs (renamed from source/Syntax/Adapt.hs) | 10 | ||||
| -rw-r--r-- | source/Felix/Syntax/Concrete.hs (renamed from source/Syntax/Concrete.hs) | 14 | ||||
| -rw-r--r-- | source/Felix/Syntax/Concrete/Keywords.hs (renamed from source/Syntax/Concrete/Keywords.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Syntax/Interface.hs (renamed from source/Syntax/Interface.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Syntax/Internal.hs (renamed from source/Syntax/Internal.hs) | 20 | ||||
| -rw-r--r-- | source/Felix/Syntax/LexicalPhrase.hs (renamed from source/Syntax/LexicalPhrase.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Syntax/Lexicon.hs (renamed from source/Syntax/Lexicon.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Syntax/Mixfix.hs (renamed from source/Syntax/Mixfix.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Syntax/Pragma.hs (renamed from source/Syntax/Pragma.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Syntax/Token.hs (renamed from source/Syntax/Token.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Test/All.hs (renamed from source/Test/All.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Test/Golden.hs (renamed from source/Test/Golden.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Test/Unit.hs | 52 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Abstract.hs (renamed from source/Test/Unit/Abstract.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Backend.hs (renamed from source/Test/Unit/Backend.hs) | 10 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/CommandLine.hs (renamed from source/Test/Unit/CommandLine.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Concrete.hs (renamed from source/Test/Unit/Concrete.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Core.hs (renamed from source/Test/Unit/Core.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Declaration.hs (renamed from source/Test/Unit/Declaration.hs) | 36 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Foundation.hs (renamed from source/Test/Unit/Foundation.hs) | 6 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Html.hs (renamed from source/Test/Unit/Html.hs) | 12 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/HtmlLayout.hs (renamed from source/Test/Unit/HtmlLayout.hs) | 4 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/HtmlOutput.hs (renamed from source/Test/Unit/HtmlOutput.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Identity.hs (renamed from source/Test/Unit/Identity.hs) | 10 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Kernel.hs (renamed from source/Test/Unit/Kernel.hs) | 18 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Lexicon.hs (renamed from source/Test/Unit/Lexicon.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Materialization.hs (renamed from source/Test/Unit/Materialization.hs) | 14 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Meaning.hs (renamed from source/Test/Unit/Meaning.hs) | 10 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Module.hs (renamed from source/Test/Unit/Module.hs) | 46 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/OutputPlan.hs (renamed from source/Test/Unit/OutputPlan.hs) | 2 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Provers.hs (renamed from source/Test/Unit/Provers.hs) | 8 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Semantic.hs (renamed from source/Test/Unit/Semantic.hs) | 16 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Source.hs (renamed from source/Test/Unit/Source.hs) | 18 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Store.hs (renamed from source/Test/Unit/Store.hs) | 18 | ||||
| -rw-r--r-- | source/Felix/Test/Unit/Token.hs (renamed from source/Test/Unit/Token.hs) | 14 | ||||
| -rw-r--r-- | source/Felix/Verification.hs | 18 | ||||
| -rw-r--r-- | source/Felix/Workspace.hs | 10 | ||||
| -rw-r--r-- | source/Test/Unit.hs | 52 |
83 files changed, 494 insertions, 493 deletions
@@ -77,18 +77,18 @@ publish: .PHONY: profile profile: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile felix -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex +RTS -s -p + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex +RTS -s -p ghc-prof-flamegraph felix.prof .PHONY: profilemem profilemem: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile felix -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex +RTS -hc -RTS + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex +RTS -hc -RTS hp2ps felix.hp gs -q -dNOPAUSE -dBATCH -sOutputFile=temp.ps -sDEVICE=ps2write -c "<</Orientation 1>> setpagedevice" -- felix.ps && mv temp.ps felix.ps .PHONY: profileparser profileparser: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile felix -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex --parseonly +RTS -p + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex --parseonly +RTS -p ghc-prof-flamegraph felix.prof diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs index b216576..34f2694 100644 --- a/source/Felix/Cache/Codec.hs +++ b/source/Felix/Cache/Codec.hs @@ -49,7 +49,7 @@ module Felix.Cache.Codec ) where import Base hiding (Empty) -import Checking.Core +import Felix.Checking.Core import Felix.Math.Codec import Control.DeepSeq (NFData) diff --git a/source/Checking/Authority.hs b/source/Felix/Checking/Authority.hs index fb6cea0..58c123f 100644 --- a/source/Checking/Authority.hs +++ b/source/Felix/Checking/Authority.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Compact public fact authority and exact contextual authorization. -module Checking.Authority +module Felix.Checking.Authority ( EscapeKind(..) , EscapeKinds , emptyEscapeKinds @@ -59,8 +59,8 @@ module Checking.Authority ) where import Base -import Checking.Foundation -import Checking.Identity +import Felix.Checking.Foundation +import Felix.Checking.Identity import Felix.Cache.Codec import Control.DeepSeq (NFData) diff --git a/source/Checking/Backend/Problem.hs b/source/Felix/Checking/Backend/Problem.hs index 8d3a071..0390020 100644 --- a/source/Checking/Backend/Problem.hs +++ b/source/Felix/Checking/Backend/Problem.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Complete-problem FOF/TH0 classification and construction. -module Checking.Backend.Problem +module Felix.Checking.Backend.Problem ( SupportedProposition , supportedProposition , projectSupportedProposition @@ -55,8 +55,8 @@ module Checking.Backend.Problem ) where import Base -import Checking.Core -import Checking.Foundation +import Felix.Checking.Core +import Felix.Checking.Foundation import Control.Monad (foldM, unless) import Data.Bifunctor (first) diff --git a/source/Checking/Backend/Tptp.hs b/source/Felix/Checking/Backend/Tptp.hs index e70277e..a5c0546 100644 --- a/source/Checking/Backend/Tptp.hs +++ b/source/Felix/Checking/Backend/Tptp.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Deterministic task-wide TPTP preparation for checked typed problems. -module Checking.Backend.Tptp +module Felix.Checking.Backend.Tptp ( TypedFormulaOccurrence(..) , TypedTptpNameOrigin(..) , PreparedTypedTptpProblem @@ -16,8 +16,8 @@ module Checking.Backend.Tptp ) where import Base hiding (Empty) -import Checking.Backend.Problem -import Checking.Core +import Felix.Checking.Backend.Problem +import Felix.Checking.Core import Tptp.UnsortedFirstOrder qualified as Tptp import Control.Monad (foldM) diff --git a/source/Checking/Core.hs b/source/Felix/Checking/Core.hs index bf5bf3b..13ec218 100644 --- a/source/Checking/Core.hs +++ b/source/Felix/Checking/Core.hs @@ -8,7 +8,7 @@ -- -- Scoped syntax is an operational construction language. Only a checked, -- frozen value is semantic input to later kernel and backend boundaries. -module Checking.Core +module Felix.Checking.Core ( CoreType(..) , CoreIntrinsicTag(..) , coreIntrinsicType diff --git a/source/Checking/Datatype.hs b/source/Felix/Checking/Datatype.hs index a47f93d..66e64db 100644 --- a/source/Checking/Datatype.hs +++ b/source/Felix/Checking/Datatype.hs @@ -1,7 +1,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE NamedFieldPuns #-} -module Checking.Datatype +module Felix.Checking.Datatype ( CheckedDatatype , DatatypeValidationError , datatypeValidationErrorLocation @@ -16,9 +16,9 @@ module Checking.Datatype ) where import Base -import Report.Location -import Syntax.Internal -import Syntax.Lexicon +import Felix.Report.Location +import Felix.Syntax.Internal +import Felix.Syntax.Lexicon import Data.List qualified as List import Data.List.NonEmpty qualified as NonEmpty diff --git a/source/Checking/Declaration.hs b/source/Felix/Checking/Declaration.hs index c1ecd55..15050c7 100644 --- a/source/Checking/Declaration.hs +++ b/source/Felix/Checking/Declaration.hs @@ -5,7 +5,7 @@ {-# LANGUAGE RankNTypes #-} -- | Builder-confined authorization and atomic typed declaration append. -module Checking.Declaration +module Felix.Checking.Declaration ( ModuleDriver , DriverFailure(..) , DriverResult(..) @@ -171,21 +171,21 @@ module Checking.Declaration ) where import Base -import Checking.Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Backend.Tptp qualified as Tptp -import Checking.Core -import Checking.Foundation -import Checking.Identity -import Checking.Kernel.Derivation -import Checking.Materialization qualified as Materialization -import Checking.Semantic -import Checking.SetConstruction import Felix.Cache.Codec (encodeCache) +import Felix.Checking.Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Backend.Tptp qualified as Tptp +import Felix.Checking.Core +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Kernel.Derivation +import Felix.Checking.Materialization qualified as Materialization +import Felix.Checking.Semantic +import Felix.Checking.SetConstruction import Felix.Module import Felix.Provers qualified as Provers -import Report.Location -import Syntax.Abstract (StructSymbol) +import Felix.Report.Location +import Felix.Syntax.Abstract (StructSymbol) import Control.Exception qualified as Exception import Control.DeepSeq (deepseq) diff --git a/source/Checking/Exact.hs b/source/Felix/Checking/Exact.hs index 47e3859..c829743 100644 --- a/source/Checking/Exact.hs +++ b/source/Felix/Checking/Exact.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Direct compiler for the first exact monomorphic declaration family. -module Checking.Exact +module Felix.Checking.Exact ( ExactLocalId , exactLocalId , exactLocalIdValue @@ -60,18 +60,18 @@ module Checking.Exact ) where import Base hiding (Empty) -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.SetConstruction -import Checking.Semantic import Felix.Cache.Codec +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.SetConstruction import Felix.Module -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface (CanonicalLexicalEntry(..)) -import Syntax.Lexicon qualified as Lexicon +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface (CanonicalLexicalEntry(..)) +import Felix.Syntax.Lexicon qualified as Lexicon import Control.Monad.Except (ExceptT) import Control.Monad.Except (MonadError, throwError) diff --git a/source/Checking/Exact/Datatype.hs b/source/Felix/Checking/Exact/Datatype.hs index 61d99e5..be943cd 100644 --- a/source/Checking/Exact/Datatype.hs +++ b/source/Felix/Checking/Exact/Datatype.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Exact preparation of deterministic datatype declarations. -module Checking.Exact.Datatype +module Felix.Checking.Exact.Datatype ( PreparedExactDatatype , preparedExactDatatypeObjects , preparedExactDatatypeBindings @@ -23,22 +23,22 @@ module Checking.Exact.Datatype ) where import Base hiding (Empty) -import Checking.Authority -import Checking.Core -import Checking.Datatype qualified as Datatype -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Datatype qualified as Datatype +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Global qualified as ExactGlobal +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed import Felix.Cache.Codec import Felix.Module import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import Syntax.Internal qualified as Internal +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Internal qualified as Internal import Control.Monad (unless, when) import Control.Monad.Except (ExceptT) diff --git a/source/Checking/Exact/Global.hs b/source/Felix/Checking/Exact/Global.hs index 772a7e2..d4040e6 100644 --- a/source/Checking/Exact/Global.hs +++ b/source/Felix/Checking/Exact/Global.hs @@ -2,19 +2,19 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Exact resolution of source symbols to checked semantic globals. -module Checking.Exact.Global +module Felix.Checking.Exact.Global ( ExactGlobalResolutionError(..) , resolveExactSourceGlobals ) where import Base -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import Syntax.Internal qualified as Internal +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Syntax.Internal qualified as Internal import Control.Monad (foldM) import Control.Monad.Except diff --git a/source/Checking/Exact/Inductive.hs b/source/Felix/Checking/Exact/Inductive.hs index 441c773..5817b34 100644 --- a/source/Checking/Exact/Inductive.hs +++ b/source/Felix/Checking/Exact/Inductive.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Exact preparation and atomic publication of direct set inductives. -module Checking.Exact.Inductive +module Felix.Checking.Exact.Inductive ( PreparedExactInductive , preparedExactInductiveCarrierId , preparedExactInductiveCarrierType @@ -19,21 +19,21 @@ module Checking.Exact.Inductive ) where import Base hiding (Empty) -import Checking.Authority -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Foundation -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Global qualified as ExactGlobal +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed import Felix.Cache.Codec import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import Syntax.Internal qualified as Internal +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Internal qualified as Internal import Control.Monad (unless, when) import Control.Monad.Except (ExceptT) diff --git a/source/Checking/Exact/Proof.hs b/source/Felix/Checking/Exact/Proof.hs index 92ff500..e2149c4 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Felix/Checking/Exact/Proof.hs @@ -8,7 +8,7 @@ -- become available and executes discharges depth-first. The declaration -- boundary validates typed tasks and authority; it does not reconstruct this -- derivation. -module Checking.Exact.Proof +module Felix.Checking.Exact.Proof ( PreparedExactProof , preparedExactProofSyntaxId , preparedExactProofFirstOmission @@ -27,20 +27,20 @@ module Checking.Exact.Proof ) where import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Foundation -import Checking.Identity -import Checking.Kernel.Derivation (foundationFactDerivation) -import Checking.Kernel.Proof qualified as KernelProof -import Checking.SetConstruction -import Checking.Semantic +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Kernel.Derivation (foundationFactDerivation) +import Felix.Checking.Kernel.Proof qualified as KernelProof +import Felix.Checking.SetConstruction +import Felix.Checking.Semantic import Felix.Cache.Codec -import Report.Location -import Syntax.Abstract qualified as Raw +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw import Control.Monad.Except (ExceptT) import Control.Monad.Except qualified as Except diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Felix/Checking/Exact/Vocabulary.hs index 45a2844..a712bf1 100644 --- a/source/Checking/Exact/Vocabulary.hs +++ b/source/Felix/Checking/Exact/Vocabulary.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Semantic classification shared by the exact source compilers. -module Checking.Exact.Vocabulary +module Felix.Checking.Exact.Vocabulary ( FixedSemanticMeaning(..) , fixedSemanticMeaning , lowerFixedEqualityPredicate @@ -13,11 +13,11 @@ module Checking.Exact.Vocabulary ) where import Base hiding (Empty) -import Checking.Core -import Checking.Semantic -import Syntax.Abstract qualified as Raw -import Syntax.Internal qualified as Internal -import Syntax.Lexicon qualified as Lexicon +import Felix.Checking.Core +import Felix.Checking.Semantic +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Internal qualified as Internal +import Felix.Syntax.Lexicon qualified as Lexicon import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map diff --git a/source/Checking/FinalPrelude.hs b/source/Felix/Checking/FinalPrelude.hs index acb3c7b..9cc43f4 100644 --- a/source/Checking/FinalPrelude.hs +++ b/source/Felix/Checking/FinalPrelude.hs @@ -3,7 +3,7 @@ {-# LANGUAGE RankNTypes #-} -- | Authority-confined construction of the inert final-prelude candidate. -module Checking.FinalPrelude +module Felix.Checking.FinalPrelude ( FinalPreludeCandidate , finalPreludeParsed , finalPreludeSyntax @@ -23,25 +23,25 @@ module Checking.FinalPrelude ) where import Base hiding (Empty) -import Checking.Authority qualified as Authority -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Proof qualified as ExactProof -import Checking.Foundation -import Checking.Identity -import Checking.SetConstruction -import Checking.Semantic -import Checking.Semantic qualified as Semantic +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Exact.Proof qualified as ExactProof +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.SetConstruction +import Felix.Checking.Semantic +import Felix.Checking.Semantic qualified as Semantic import Felix.Module import Felix.Cache.Codec (CacheDigest) import Felix.Parse import Felix.Prelude qualified as Prelude import Felix.Source (ImportRef) -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import Syntax.Lexicon qualified as Lexicon +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Lexicon qualified as Lexicon import Control.Monad (unless) import Data.Bifunctor (first) diff --git a/source/Checking/Foundation.hs b/source/Felix/Checking/Foundation.hs index 317d1b5..5852901 100644 --- a/source/Checking/Foundation.hs +++ b/source/Felix/Checking/Foundation.hs @@ -6,7 +6,7 @@ -- Constructing 'CheckedFoundation' requires exact manifest coverage, closed -- well-typed schemas, and structural backend classification. This gate -- certifies manifest conformance only; it is not a consistency proof. -module Checking.Foundation +module Felix.Checking.Foundation ( FoundationAxiomTag(..) , KernelRuleTag(..) , KernelRuleSignature(..) @@ -32,7 +32,7 @@ module Checking.Foundation ) where import Base hiding (Empty) -import Checking.Core +import Felix.Checking.Core import Control.Monad (unless) import Data.List qualified as List diff --git a/source/Checking/Identity.hs b/source/Felix/Checking/Identity.hs index fe846dc..67347a3 100644 --- a/source/Checking/Identity.hs +++ b/source/Felix/Checking/Identity.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Content-addressed identities for checked mathematical content. -module Checking.Identity +module Felix.Checking.Identity ( TheoryId , theoryId , theoryIdDigest @@ -67,8 +67,8 @@ module Checking.Identity ) where import Base -import Checking.Core -import Checking.Foundation +import Felix.Checking.Core +import Felix.Checking.Foundation import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module diff --git a/source/Checking/Kernel/Derivation.hs b/source/Felix/Checking/Kernel/Derivation.hs index 65bcc25..e83b376 100644 --- a/source/Checking/Kernel/Derivation.hs +++ b/source/Felix/Checking/Kernel/Derivation.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Private in-memory proof trees and independent kernel replay. -module Checking.Kernel.Derivation +module Felix.Checking.Kernel.Derivation ( ImportIx , importIx , importIxValue @@ -53,10 +53,10 @@ module Checking.Kernel.Derivation ) where import Base -import Checking.Core -import Checking.Foundation -import Checking.Kernel.Semantics qualified as Semantics -import Checking.Kernel.SetLfp qualified as SetLfp +import Felix.Checking.Core +import Felix.Checking.Foundation +import Felix.Checking.Kernel.Semantics qualified as Semantics +import Felix.Checking.Kernel.SetLfp qualified as SetLfp import Control.Monad (unless) import Data.Bifunctor (first) diff --git a/source/Checking/Kernel/Proof.hs b/source/Felix/Checking/Kernel/Proof.hs index 5fc0d96..d4ccedc 100644 --- a/source/Checking/Kernel/Proof.hs +++ b/source/Felix/Checking/Kernel/Proof.hs @@ -3,7 +3,7 @@ -- | Small proof-producing natural-deduction combinators. Every resulting tree -- is still replayed independently before it can authorize a fact. -module Checking.Kernel.Proof +module Felix.Checking.Kernel.Proof ( ProofContext , rootProofContext , proofContextTypes @@ -47,11 +47,11 @@ module Checking.Kernel.Proof ) where import Base -import Checking.Core -import Checking.Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Semantics qualified as Semantics -import Checking.Kernel.SetLfp qualified as SetLfp +import Felix.Checking.Core +import Felix.Checking.Foundation +import Felix.Checking.Kernel.Derivation +import Felix.Checking.Kernel.Semantics qualified as Semantics +import Felix.Checking.Kernel.SetLfp qualified as SetLfp import Control.Monad (unless) import Data.Bifunctor (first) diff --git a/source/Checking/Kernel/Semantics.hs b/source/Felix/Checking/Kernel/Semantics.hs index 3306b09..f9cfcfa 100644 --- a/source/Checking/Kernel/Semantics.hs +++ b/source/Felix/Checking/Kernel/Semantics.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Checked logical inference over scoped canonical HOL terms. -module Checking.Kernel.Semantics +module Felix.Checking.Kernel.Semantics ( implicationElimination , implicationIntroduction , forallElimination @@ -17,7 +17,7 @@ module Checking.Kernel.Semantics ) where import Base -import Checking.Core +import Felix.Checking.Core import Control.Monad (unless) import Data.Bifunctor (first) diff --git a/source/Checking/Kernel/SetLfp.hs b/source/Felix/Checking/Kernel/SetLfp.hs index e3fa175..19f6714 100644 --- a/source/Checking/Kernel/SetLfp.hs +++ b/source/Felix/Checking/Kernel/SetLfp.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | The four checked rules for the bounded set-valued least fixed point. -module Checking.Kernel.SetLfp +module Felix.Checking.Kernel.SetLfp ( setLfpBound , setLfpLeast , setLfpFixed @@ -16,8 +16,8 @@ module Checking.Kernel.SetLfp ) where import Base -import Checking.Core -import Checking.Foundation +import Felix.Checking.Core +import Felix.Checking.Foundation import Data.Bifunctor (first) import Numeric.Natural (Natural) diff --git a/source/Checking/Materialization.hs b/source/Felix/Checking/Materialization.hs index 6dcf1f0..51944a5 100644 --- a/source/Checking/Materialization.hs +++ b/source/Felix/Checking/Materialization.hs @@ -5,7 +5,7 @@ -- -- Successful checks are inert. Fresh completion and validated loading or -- sealing own the runtime authority that may publish a fact. -module Checking.Materialization +module Felix.Checking.Materialization ( CandidateValidation , candidateProofValidation , candidateDeclarationValidation @@ -17,9 +17,9 @@ module Checking.Materialization ) where import Base -import Checking.Authority -import Checking.Identity -import Checking.Semantic +import Felix.Checking.Authority +import Felix.Checking.Identity +import Felix.Checking.Semantic import Control.Monad (unless) import Numeric.Natural (Natural) diff --git a/source/Checking/Module.hs b/source/Felix/Checking/Module.hs index d0e1d52..88c8fef 100644 --- a/source/Checking/Module.hs +++ b/source/Felix/Checking/Module.hs @@ -3,7 +3,7 @@ {-# LANGUAGE RankNTypes #-} -- | Explicit inputs and sealed outputs for the typed module driver. -module Checking.Module +module Felix.Checking.Module ( LiveModuleBinding(..) , IdentifiedModuleInput , identifiedPhysicalModule @@ -55,23 +55,23 @@ module Checking.Module ) where import Base -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Datatype qualified as ExactDatatype -import Checking.Exact.Inductive qualified as ExactInductive -import Checking.Exact.Proof qualified as ExactProof -import Checking.FinalPrelude qualified as FinalPrelude -import Checking.Foundation -import Checking.Identity -import Checking.Semantic +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Exact.Datatype qualified as ExactDatatype +import Felix.Checking.Exact.Inductive qualified as ExactInductive +import Felix.Checking.Exact.Proof qualified as ExactProof +import Felix.Checking.FinalPrelude qualified as FinalPrelude +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Semantic import Felix.Module import Felix.Parse import Felix.Prelude qualified as Prelude import Felix.Source import Felix.Store qualified as Store -import Report.Location -import Syntax.Interface -import Syntax.Abstract qualified as Raw +import Felix.Report.Location +import Felix.Syntax.Interface +import Felix.Syntax.Abstract qualified as Raw import Control.Monad (unless) import Data.Bifunctor (first) diff --git a/source/Checking/Semantic.hs b/source/Felix/Checking/Semantic.hs index 7a05f39..c9442f3 100644 --- a/source/Checking/Semantic.hs +++ b/source/Felix/Checking/Semantic.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Canonical semantic declaration, prefix, interface, and validation keys. -module Checking.Semantic +module Felix.Checking.Semantic ( DeclarationSlot , declarationSlot , declarationSlotModule @@ -150,16 +150,16 @@ module Checking.Semantic ) where import Base -import Checking.Authority -import Checking.Core -import Checking.Identity +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Identity import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module import Felix.Parsed.Identity import Felix.Source -import Syntax.Interface -import Syntax.Abstract +import Felix.Syntax.Interface +import Felix.Syntax.Abstract import Control.DeepSeq (NFData) import Control.Monad (unless, when) diff --git a/source/Checking/SetConstruction.hs b/source/Felix/Checking/SetConstruction.hs index 4c4b4bc..a5e1d80 100644 --- a/source/Checking/SetConstruction.hs +++ b/source/Felix/Checking/SetConstruction.hs @@ -8,7 +8,7 @@ -- telescope and derive one canonical term. Local views, transparent content, -- direct extensional facts, and cache-scoped descriptors all consume that -- same checked value. -module Checking.SetConstruction +module Felix.Checking.SetConstruction ( NamedSetConstruction , checkedSeparationConstruction , checkedFunctionalReplacementConstruction @@ -36,9 +36,9 @@ module Checking.SetConstruction ) where import Base hiding (Empty) -import Checking.Core -import Checking.Foundation -import Checking.Identity +import Felix.Checking.Core +import Felix.Checking.Foundation +import Felix.Checking.Identity import Felix.Cache.Codec ( CacheDigest , encodeCache diff --git a/source/Checking/Typed/Inductive.hs b/source/Felix/Checking/Typed/Inductive.hs index eb6c0f7..4094083 100644 --- a/source/Checking/Typed/Inductive.hs +++ b/source/Felix/Checking/Typed/Inductive.hs @@ -4,7 +4,7 @@ -- | Direct checked lowering of the current one-carrier set-valued inductive -- declaration. -module Checking.Typed.Inductive +module Felix.Checking.Typed.Inductive ( DirectInductive(..) , DirectInductiveClause(..) , DirectInductiveCondition(..) @@ -37,13 +37,13 @@ module Checking.Typed.Inductive ) where import Base hiding (Empty) -import Checking.Core -import Checking.Exact.Vocabulary -import Checking.Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Proof -import Report.Location (Location) -import Syntax.Internal +import Felix.Checking.Core +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Foundation +import Felix.Checking.Kernel.Derivation +import Felix.Checking.Kernel.Proof +import Felix.Report.Location (Location) +import Felix.Syntax.Internal import Control.Monad ((<=<), foldM) import Data.Bifunctor (first) diff --git a/source/Felix/CommandLine.hs b/source/Felix/CommandLine.hs index 701020f..448d698 100644 --- a/source/Felix/CommandLine.hs +++ b/source/Felix/CommandLine.hs @@ -26,10 +26,10 @@ import Felix.Store qualified as Store import Felix.Verification qualified as Verification import Felix.Version qualified as Version import Felix.Workspace qualified as Workspace -import Render.Html.Export qualified as HtmlExport -import Render.Html.Layout qualified as HtmlLayout -import Render.Html.Output qualified as HtmlOutput -import Report.Location +import Felix.Render.Html.Export qualified as HtmlExport +import Felix.Render.Html.Layout qualified as HtmlLayout +import Felix.Render.Html.Output qualified as HtmlOutput +import Felix.Report.Location import Control.Monad (unless, when) import Data.Maybe (catMaybes) diff --git a/source/Felix/Math/Codec.hs b/source/Felix/Math/Codec.hs index 4a5c7b1..a551f53 100644 --- a/source/Felix/Math/Codec.hs +++ b/source/Felix/Math/Codec.hs @@ -24,7 +24,7 @@ module Felix.Math.Codec ) where import Base hiding (Empty) -import Checking.Core +import Felix.Checking.Core import Control.DeepSeq (NFData) import Crypto.Hash qualified as Crypto diff --git a/source/Felix/Meaning.hs b/source/Felix/Meaning.hs index 60c4cfc..268a1a6 100644 --- a/source/Felix/Meaning.hs +++ b/source/Felix/Meaning.hs @@ -9,12 +9,12 @@ module Felix.Meaning where import Base -import Syntax.Abstract (Sign(..)) -import Syntax.Abstract qualified as Raw -import Syntax.Internal (VarSymbol(..), pattern FreshVar) -import Syntax.Internal qualified as Sem -import Syntax.LexicalPhrase (unsafeReadPhrase) -import Report.Location +import Felix.Syntax.Abstract (Sign(..)) +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Internal (VarSymbol(..), pattern FreshVar) +import Felix.Syntax.Internal qualified as Sem +import Felix.Syntax.LexicalPhrase (unsafeReadPhrase) +import Felix.Report.Location import Bound import Control.Monad.Except diff --git a/source/Felix/OutputPlan.hs b/source/Felix/OutputPlan.hs index 58314db..78d7e7a 100644 --- a/source/Felix/OutputPlan.hs +++ b/source/Felix/OutputPlan.hs @@ -18,7 +18,7 @@ module Felix.OutputPlan import Base import Felix.Source import Felix.Store -import Render.Html.Output qualified as Html +import Felix.Render.Html.Output qualified as Html import Control.Exception (displayException) import Data.List qualified as List diff --git a/source/Felix/Parse.hs b/source/Felix/Parse.hs index e03feb9..0a46d82 100644 --- a/source/Felix/Parse.hs +++ b/source/Felix/Parse.hs @@ -90,9 +90,9 @@ import Felix.Source import Felix.Source.Content qualified as Content import Felix.Source.Graph import Felix.Store qualified as Store -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Adapt +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Adapt ( LexicalScanError(..) , ScannedLexicalItem , SyntaxMaterializationError(..) @@ -101,11 +101,11 @@ import Syntax.Adapt , scanChunk , scannedItemMarker ) -import Syntax.Concrete (grammar) -import Syntax.Interface -import Syntax.Lexicon (Lexicon) -import Syntax.Pragma -import Syntax.Token +import Felix.Syntax.Concrete (grammar) +import Felix.Syntax.Interface +import Felix.Syntax.Lexicon (Lexicon) +import Felix.Syntax.Pragma +import Felix.Syntax.Token import Control.DeepSeq (NFData, force) import Control.Exception (Exception, evaluate) diff --git a/source/Felix/Parsed/Identity.hs b/source/Felix/Parsed/Identity.hs index e11b2c7..b76c26e 100644 --- a/source/Felix/Parsed/Identity.hs +++ b/source/Felix/Parsed/Identity.hs @@ -20,7 +20,7 @@ module Felix.Parsed.Identity import Base import Felix.Cache.Codec import Felix.Source.Content -import Syntax.Interface +import Felix.Syntax.Interface import Control.DeepSeq (NFData) import Data.ByteString (ByteString) diff --git a/source/Felix/Parsed/Payload.hs b/source/Felix/Parsed/Payload.hs index 2506973..5e63c70 100644 --- a/source/Felix/Parsed/Payload.hs +++ b/source/Felix/Parsed/Payload.hs @@ -30,11 +30,11 @@ import Base import Felix.Cache.Codec import Felix.Parsed.Identity qualified as Identity import Felix.Source -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import Syntax.LexicalPhrase qualified as Phrase -import Syntax.Token qualified as Token +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.LexicalPhrase qualified as Phrase +import Felix.Syntax.Token qualified as Token import Control.DeepSeq (NFData) import Control.Monad (unless) diff --git a/source/Felix/Prelude.hs b/source/Felix/Prelude.hs index 28ad961..ccd5623 100644 --- a/source/Felix/Prelude.hs +++ b/source/Felix/Prelude.hs @@ -30,10 +30,10 @@ import Felix.Parse import Felix.Parsed.Identity qualified as Parsed import Felix.Source import Felix.Source.Graph -import Report.Location -import Syntax.Adapt (SyntaxMaterializationError) -import Syntax.Interface -import Syntax.Pragma +import Felix.Report.Location +import Felix.Syntax.Adapt (SyntaxMaterializationError) +import Felix.Syntax.Interface +import Felix.Syntax.Pragma import Control.Exception (IOException, displayException, try) import Data.ByteString (ByteString) diff --git a/source/Felix/Provers.hs b/source/Felix/Provers.hs index eb6f62c..16ef655 100644 --- a/source/Felix/Provers.hs +++ b/source/Felix/Provers.hs @@ -79,9 +79,9 @@ module Felix.Provers ) where import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem -import Checking.Backend.Tptp +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem +import Felix.Checking.Backend.Tptp import Control.Concurrent.STM ( STM @@ -130,7 +130,7 @@ import Data.Text qualified as Text import Data.Text.Encoding qualified as TextEncoding import Data.Text.Encoding.Error qualified as TextEncodingError import Numeric.Natural (Natural) -import Report.Location (Location) +import Felix.Report.Location (Location) import System.Exit (ExitCode(..)) import System.Posix.Signals (sigKILL, signalProcessGroup) import System.Posix.Types (ProcessGroupID) diff --git a/source/Render/Html.hs b/source/Felix/Render/Html.hs index c37a278..7081e52 100644 --- a/source/Render/Html.hs +++ b/source/Felix/Render/Html.hs @@ -3,7 +3,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -module Render.Html +module Felix.Render.Html ( HtmlRenderIndex , HtmlPagePresentation , buildRenderIndex @@ -12,14 +12,14 @@ module Render.Html , supportScriptAssetContents ) where -import Syntax.Abstract +import Felix.Syntax.Abstract import Base import Felix.Source (ResolvedSource) import Lucid hiding (Term, for_) import Lucid.Base (makeAttributes) import Lucid.Math -import Render.Html.Context +import Felix.Render.Html.Context ( HtmlRenderContext , HtmlRenderContextError , htmlCurrentPageLabel @@ -29,7 +29,9 @@ import Render.Html.Context , htmlSourcePageHref , htmlSupportScriptHref ) -import Render.Html.Layout (renderUrlFragment) +import Felix.Render.Html.Layout (renderUrlFragment) +import Felix.Report.Location (Location, pattern Nowhere) +import Felix.Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText) import Control.Monad (unless, when) import Data.Char (digitToInt, isAlphaNum, isDigit, isSpace, toUpper) @@ -39,8 +41,7 @@ import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.Lazy qualified as LazyText -import Report.Location (Location, pattern Nowhere) -import Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText) + data HintCategory diff --git a/source/Render/Html/Context.hs b/source/Felix/Render/Html/Context.hs index 151edd5..469d986 100644 --- a/source/Render/Html/Context.hs +++ b/source/Felix/Render/Html/Context.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Browser-facing routing authority for one rendered HTML page. -module Render.Html.Context +module Felix.Render.Html.Context ( HtmlRenderEnvironment , htmlRenderEnvironment , HtmlRenderContext @@ -23,7 +23,7 @@ module Render.Html.Context import Base import Felix.Source -import Render.Html.Layout +import Felix.Render.Html.Layout import Control.Exception (Exception) import Data.Map.Strict qualified as Map diff --git a/source/Render/Html/Export.hs b/source/Felix/Render/Html/Export.hs index 2c747d8..a3f0e39 100644 --- a/source/Render/Html/Export.hs +++ b/source/Felix/Render/Html/Export.hs @@ -3,7 +3,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Prepare a complete HTML export from retained parsed presentation. -module Render.Html.Export +module Felix.Render.Html.Export ( HtmlPresentation , htmlPresentationFromParsedWorkspace , HtmlExportError(..) @@ -16,11 +16,11 @@ module Render.Html.Export import Base import Felix.Parse import Felix.Source -import Render.Html qualified as Html -import Render.Html.Context -import Render.Html.Layout -import Render.Html.Output -import Syntax.Abstract (Block) +import Felix.Render.Html qualified as Html +import Felix.Render.Html.Context +import Felix.Render.Html.Layout +import Felix.Render.Html.Output +import Felix.Syntax.Abstract (Block) import Control.Exception (Exception, IOException, displayException) import Control.Exception qualified as Exception diff --git a/source/Render/Html/Layout.hs b/source/Felix/Render/Html/Layout.hs index c26b6b5..7e5bfcf 100644 --- a/source/Render/Html/Layout.hs +++ b/source/Felix/Render/Html/Layout.hs @@ -2,7 +2,7 @@ {-# LANGUAGE NoImplicitPrelude #-} -- | Pure browser and destination routing for a resolved source graph. -module Render.Html.Layout +module Felix.Render.Html.Layout ( UrlSegment , UrlSegmentError(..) , urlSegment diff --git a/source/Render/Html/Output.hs b/source/Felix/Render/Html/Output.hs index 685c83a..8e36f97 100644 --- a/source/Render/Html/Output.hs +++ b/source/Felix/Render/Html/Output.hs @@ -8,7 +8,7 @@ -- accepted only when they resolve inside the canonical root. Final-target -- symlinks are rejected without following them; regular generated files may be -- replaced. This policy prevents stable-tree escapes, not TOCTOU attacks. -module Render.Html.Output +module Felix.Render.Html.Output ( PreparedHtmlArtifact , preparedHtmlArtifact , preparedHtmlArtifactDestination diff --git a/source/Report/Location.hs b/source/Felix/Report/Location.hs index 4495360..36b8997 100644 --- a/source/Report/Location.hs +++ b/source/Felix/Report/Location.hs @@ -1,7 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} -module Report.Location where +module Felix.Report.Location where import Base import Text.Megaparsec.Pos (SourcePos (sourceColumn, sourceLine), unPos) diff --git a/source/Felix/Source.hs b/source/Felix/Source.hs index 350bb50..68d596c 100644 --- a/source/Felix/Source.hs +++ b/source/Felix/Source.hs @@ -80,7 +80,7 @@ import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.Encoding qualified as Encoding -import Report.Location +import Felix.Report.Location ( Location , LocationRegistrationError(..) , locationToText diff --git a/source/Felix/Source/Graph.hs b/source/Felix/Source/Graph.hs index cb8990e..9c8753d 100644 --- a/source/Felix/Source/Graph.hs +++ b/source/Felix/Source/Graph.hs @@ -25,11 +25,11 @@ module Felix.Source.Graph import Base import Felix.Source -import Report.Location +import Felix.Report.Location ( FileId , registerFilePathWithDisplay ) -import Syntax.Token (Located(..), gatherImports) +import Felix.Syntax.Token (Located(..), gatherImports) import Control.Monad (unless) import Control.Monad.State.Strict diff --git a/source/Felix/Store.hs b/source/Felix/Store.hs index 038b4dc..fb12670 100644 --- a/source/Felix/Store.hs +++ b/source/Felix/Store.hs @@ -54,16 +54,16 @@ module Felix.Store ) where import Base -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Identity -import Checking.Materialization qualified as Materialization -import Checking.Semantic +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Identity +import Felix.Checking.Materialization qualified as Materialization +import Felix.Checking.Semantic import Felix.Cache.Codec import Felix.Module (ModuleName) import Felix.Parsed.Identity qualified as Parsed import Felix.Parsed.Payload qualified as ParsedPayload -import Syntax.Interface qualified as Syntax +import Felix.Syntax.Interface qualified as Syntax import Control.Concurrent.MVar ( MVar diff --git a/source/Syntax/Abstract.hs b/source/Felix/Syntax/Abstract.hs index 76ce6b6..b18612a 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Felix/Syntax/Abstract.hs @@ -9,17 +9,17 @@ -- | Data types for the abstract syntax tree and helper functions -- for constructing the lexicon. -- -module Syntax.Abstract - ( module Syntax.Abstract - , module Syntax.LexicalPhrase - , module Syntax.Token +module Felix.Syntax.Abstract + ( module Felix.Syntax.Abstract + , module Felix.Syntax.LexicalPhrase + , module Felix.Syntax.Token ) where import Base -import Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase) -import Syntax.Token (Token(..), Located(..)) -import Report.Location +import Felix.Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase) +import Felix.Syntax.Token (Token(..), Located(..)) +import Felix.Report.Location import Control.DeepSeq (NFData) import Text.Earley.Mixfix (Holey) diff --git a/source/Syntax/Adapt.hs b/source/Felix/Syntax/Adapt.hs index f496ead..eb0cb6c 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Felix/Syntax/Adapt.hs @@ -2,7 +2,7 @@ {-# LANGUAGE ApplicativeDo #-} {-# LANGUAGE RecordWildCards #-} -module Syntax.Adapt +module Felix.Syntax.Adapt ( FunctionPatternError(..) , LexicalScanError(..) , ScannedLexicalItem(..) @@ -14,10 +14,10 @@ module Syntax.Adapt ) where import Base -import Syntax.Abstract -import Syntax.Interface -import Syntax.Lexicon -import Report.Location +import Felix.Syntax.Abstract +import Felix.Syntax.Interface +import Felix.Syntax.Lexicon +import Felix.Report.Location import Control.Monad (foldM) import Data.Bifunctor qualified as Bifunctor diff --git a/source/Syntax/Concrete.hs b/source/Felix/Syntax/Concrete.hs index 62d1f92..8be8ab6 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Felix/Syntax/Concrete.hs @@ -3,25 +3,25 @@ {-# LANGUAGE RecursiveDo #-} -- | Concrete syntax of the surface language. -module Syntax.Concrete where +module Felix.Syntax.Concrete where import Base -import Syntax.Abstract -import Syntax.Concrete.Keywords -import Syntax.Lexicon +import Felix.Syntax.Abstract +import Felix.Syntax.Concrete.Keywords +import Felix.Syntax.Lexicon ( Lexicon(..) , SignatureHeadForm(..) , concreteSignatureHeadForms , lexiconAdjs , splitOnVariableSlot ) -import Syntax.Token -import Report.Location +import Felix.Syntax.Token +import Felix.Report.Location import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map import Text.Earley (Grammar, Prod, (<?>), rule, satisfy, terminal) -import Syntax.Mixfix +import Felix.Syntax.Mixfix grammar :: Lexicon -> Grammar r (Prod r Text (Located Token) Block) diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Felix/Syntax/Concrete/Keywords.hs index a7ac169..eb6d09c 100644 --- a/source/Syntax/Concrete/Keywords.hs +++ b/source/Felix/Syntax/Concrete/Keywords.hs @@ -18,12 +18,12 @@ The names are chosen using the following criteria: This module also defines symbols that have special uses (such as @_colon@ for its use in type signatures). -} -module Syntax.Concrete.Keywords where +module Felix.Syntax.Concrete.Keywords where import Base -import Syntax.Token -import Report.Location +import Felix.Syntax.Token +import Felix.Report.Location import Text.Earley (Prod, (<?>), terminal) diff --git a/source/Syntax/Interface.hs b/source/Felix/Syntax/Interface.hs index 4b84cec..1820705 100644 --- a/source/Syntax/Interface.hs +++ b/source/Felix/Syntax/Interface.hs @@ -2,7 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -module Syntax.Interface +module Felix.Syntax.Interface ( MixfixLevel , mixfixLevel , mixfixLevelValue @@ -56,9 +56,9 @@ module Syntax.Interface import Base import Felix.Cache.Codec -import Syntax.Abstract -import Syntax.Lexicon -import Syntax.Pragma +import Felix.Syntax.Abstract +import Felix.Syntax.Lexicon +import Felix.Syntax.Pragma import Control.DeepSeq (NFData) import Control.Monad (unless) diff --git a/source/Syntax/Internal.hs b/source/Felix/Syntax/Internal.hs index 5a8cb65..d129947 100644 --- a/source/Syntax/Internal.hs +++ b/source/Felix/Syntax/Internal.hs @@ -6,25 +6,25 @@ {-# LANGUAGE ViewPatterns #-} -- | Data types for the internal (semantic) syntax tree. -module Syntax.Internal - ( module Syntax.Internal - , module Syntax.Abstract - , module Syntax.LexicalPhrase - , module Syntax.Token +module Felix.Syntax.Internal + ( module Felix.Syntax.Internal + , module Felix.Syntax.Abstract + , module Felix.Syntax.LexicalPhrase + , module Felix.Syntax.Token ) where import Base -import Syntax.Lexicon +import Felix.Syntax.Lexicon ( pattern PairSymbol , pattern UnionsSymbol , pattern UpairSymbol ) -import Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl) -import Syntax.Token (Token(..)) -import Report.Location +import Felix.Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl) +import Felix.Syntax.Token (Token(..)) +import Felix.Report.Location -import Syntax.Abstract +import Felix.Syntax.Abstract ( Chain(..) , Associativity(..) , Connective(..) diff --git a/source/Syntax/LexicalPhrase.hs b/source/Felix/Syntax/LexicalPhrase.hs index a0e0f19..5eb5b18 100644 --- a/source/Syntax/LexicalPhrase.hs +++ b/source/Felix/Syntax/LexicalPhrase.hs @@ -1,11 +1,11 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE NoImplicitPrelude #-} -module Syntax.LexicalPhrase where +module Felix.Syntax.LexicalPhrase where import Base -import Syntax.Token (Token(..)) +import Felix.Syntax.Token (Token(..)) import Control.DeepSeq (NFData) import Data.Char (isAlpha) diff --git a/source/Syntax/Lexicon.hs b/source/Felix/Syntax/Lexicon.hs index 3e815c7..c3332c7 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Felix/Syntax/Lexicon.hs @@ -9,8 +9,8 @@ -- extension easier. -- -module Syntax.Lexicon - ( module Syntax.Lexicon +module Felix.Syntax.Lexicon + ( module Felix.Syntax.Lexicon , pattern ConsSymbol , pattern PairSymbol , pattern UpairSymbol @@ -22,14 +22,14 @@ module Syntax.Lexicon import Base -import Syntax.Abstract +import Felix.Syntax.Abstract import Data.List qualified as List import Data.Sequence qualified as Seq import Data.Set qualified as Set import Data.Map.Strict qualified as Map import Data.Text qualified as Text -import Syntax.Mixfix (Holey) +import Felix.Syntax.Mixfix (Holey) data SignatureHeadForm diff --git a/source/Syntax/Mixfix.hs b/source/Felix/Syntax/Mixfix.hs index 6489d46..a3ce4bb 100644 --- a/source/Syntax/Mixfix.hs +++ b/source/Felix/Syntax/Mixfix.hs @@ -1,6 +1,6 @@ {-# LANGUAGE RecursiveDo #-} -module Syntax.Mixfix where +module Felix.Syntax.Mixfix where {- Original code Copyright (c) 2014-2019, Olle Fredriksson @@ -39,7 +39,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. import Base import Text.Earley import Data.Either -import Syntax.Abstract +import Felix.Syntax.Abstract replicateA :: Applicative f => Int -> f a -> f [a] diff --git a/source/Syntax/Pragma.hs b/source/Felix/Syntax/Pragma.hs index 94c0d46..97d1482 100644 --- a/source/Syntax/Pragma.hs +++ b/source/Felix/Syntax/Pragma.hs @@ -2,7 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -module Syntax.Pragma +module Felix.Syntax.Pragma ( SourceMixfixLevel , sourceMixfixLevelValue , SyntaxPragma(..) @@ -14,8 +14,8 @@ module Syntax.Pragma import Base -import Report.Location -import Syntax.Abstract (Associativity(..)) +import Felix.Report.Location +import Felix.Syntax.Abstract (Associativity(..)) import Control.DeepSeq (NFData) import Control.Monad (unless, when) diff --git a/source/Syntax/Token.hs b/source/Felix/Syntax/Token.hs index b16379b..31d1d19 100644 --- a/source/Syntax/Token.hs +++ b/source/Felix/Syntax/Token.hs @@ -13,7 +13,7 @@ -- (α, β, γ, ..., 𝔸, 𝔹, ℂ, ...). Similarly, @\\begin{...}@ and @\\end{...}@ commands -- are each parsed as single tokens. -- -module Syntax.Token +module Felix.Syntax.Token ( Token(..) , VariableDisplay(..) , VariableSuffix(..) @@ -30,7 +30,7 @@ module Syntax.Token import Base hiding (many) -import Report.Location +import Felix.Report.Location import Control.DeepSeq (NFData) import Control.Monad.Combinators diff --git a/source/Test/All.hs b/source/Felix/Test/All.hs index 7fb5bd3..7cdc49c 100644 --- a/source/Test/All.hs +++ b/source/Felix/Test/All.hs @@ -1,9 +1,9 @@ -module Test.All where +module Felix.Test.All where import Base -import Test.Golden -import Test.Unit +import Felix.Test.Golden +import Felix.Test.Unit import Test.Tasty diff --git a/source/Test/Golden.hs b/source/Felix/Test/Golden.hs index c700d06..905ff73 100644 --- a/source/Test/Golden.hs +++ b/source/Felix/Test/Golden.hs @@ -1,7 +1,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RecordWildCards #-} -module Test.Golden where +module Felix.Test.Golden where import Base diff --git a/source/Felix/Test/Unit.hs b/source/Felix/Test/Unit.hs new file mode 100644 index 0000000..f11d21f --- /dev/null +++ b/source/Felix/Test/Unit.hs @@ -0,0 +1,52 @@ +module Felix.Test.Unit where + + +import Felix.Test.Unit.Abstract qualified as Abstract +import Felix.Test.Unit.Backend qualified as Backend +import Felix.Test.Unit.CommandLine qualified as CommandLine +import Felix.Test.Unit.Concrete qualified as Concrete +import Felix.Test.Unit.Core qualified as Core +import Felix.Test.Unit.Declaration qualified as Declaration +import Felix.Test.Unit.Foundation qualified as Foundation +import Felix.Test.Unit.Html qualified as Html +import Felix.Test.Unit.HtmlLayout qualified as HtmlLayout +import Felix.Test.Unit.HtmlOutput qualified as HtmlOutput +import Felix.Test.Unit.Identity qualified as Identity +import Felix.Test.Unit.Kernel qualified as Kernel +import Felix.Test.Unit.Lexicon qualified as Lexicon +import Felix.Test.Unit.Materialization qualified as Materialization +import Felix.Test.Unit.Meaning qualified as Meaning +import Felix.Test.Unit.Module qualified as Module +import Felix.Test.Unit.OutputPlan qualified as OutputPlan +import Felix.Test.Unit.Provers qualified as Provers +import Felix.Test.Unit.Semantic qualified as Semantic +import Felix.Test.Unit.Source qualified as Source +import Felix.Test.Unit.Store qualified as Store +import Felix.Test.Unit.Token qualified as Token +import Test.Tasty + +unitTests :: TestTree +unitTests = testGroup "unit tests" + [ Abstract.unitTests + , Backend.unitTests + , CommandLine.unitTests + , Concrete.unitTests + , Core.unitTests + , Declaration.unitTests + , Foundation.unitTests + , Identity.unitTests + , Html.unitTests + , HtmlLayout.unitTests + , HtmlOutput.unitTests + , Kernel.unitTests + , Lexicon.unitTests + , Meaning.unitTests + , Materialization.unitTests + , Module.unitTests + , OutputPlan.unitTests + , Provers.unitTests + , Semantic.unitTests + , Source.unitTests + , Store.unitTests + , Token.unitTests + ] diff --git a/source/Test/Unit/Abstract.hs b/source/Felix/Test/Unit/Abstract.hs index 61118bd..c487c2a 100644 --- a/source/Test/Unit/Abstract.hs +++ b/source/Felix/Test/Unit/Abstract.hs @@ -1,10 +1,10 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Abstract (unitTests) where +module Felix.Test.Unit.Abstract (unitTests) where import Base -import Report.Location -import Syntax.Abstract +import Felix.Report.Location +import Felix.Syntax.Abstract import Hedgehog import Hedgehog.Gen qualified as Gen diff --git a/source/Test/Unit/Backend.hs b/source/Felix/Test/Unit/Backend.hs index 5243c96..384d21b 100644 --- a/source/Test/Unit/Backend.hs +++ b/source/Felix/Test/Unit/Backend.hs @@ -1,13 +1,13 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Backend (unitTests) where +module Felix.Test.Unit.Backend (unitTests) where import Base hiding (Empty) -import Checking.Backend.Problem -import Checking.Backend.Tptp -import Checking.Core -import Checking.Foundation qualified as Foundation +import Felix.Checking.Backend.Problem +import Felix.Checking.Backend.Tptp +import Felix.Checking.Core +import Felix.Checking.Foundation qualified as Foundation import Felix.Provers import Tptp.UnsortedFirstOrder qualified as Tptp diff --git a/source/Test/Unit/CommandLine.hs b/source/Felix/Test/Unit/CommandLine.hs index 110e00d..f2a4a10 100644 --- a/source/Test/Unit/CommandLine.hs +++ b/source/Felix/Test/Unit/CommandLine.hs @@ -1,6 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.CommandLine (unitTests) where +module Felix.Test.Unit.CommandLine (unitTests) where import Base import Felix.CommandLine @@ -9,8 +9,8 @@ import Felix.Source (safeRelativePath) import Felix.Store qualified as Store import Felix.Verification qualified as Verification import Felix.Provers qualified as Provers -import Render.Html.Output qualified as HtmlOutput -import Report.Location (pattern Nowhere) +import Felix.Render.Html.Output qualified as HtmlOutput +import Felix.Report.Location (pattern Nowhere) import Control.Exception (IOException, bracket) import Control.Exception qualified as Exception diff --git a/source/Test/Unit/Concrete.hs b/source/Felix/Test/Unit/Concrete.hs index 7776552..7eac7df 100644 --- a/source/Test/Unit/Concrete.hs +++ b/source/Felix/Test/Unit/Concrete.hs @@ -1,13 +1,13 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Concrete (unitTests) where +module Felix.Test.Unit.Concrete (unitTests) where import Base -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Concrete (grammar) -import Syntax.Lexicon (builtins) -import Syntax.Token (runLexer) +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Concrete (grammar) +import Felix.Syntax.Lexicon (builtins) +import Felix.Syntax.Token (runLexer) import Data.Text qualified as Text import Test.Tasty diff --git a/source/Test/Unit/Core.hs b/source/Felix/Test/Unit/Core.hs index 643dc38..0388c7f 100644 --- a/source/Test/Unit/Core.hs +++ b/source/Felix/Test/Unit/Core.hs @@ -1,11 +1,11 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Core (unitTests) where +module Felix.Test.Unit.Core (unitTests) where import Base hiding (Empty) -import Checking.Core -import Checking.Foundation qualified as Foundation -import Checking.SetConstruction +import Felix.Checking.Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.SetConstruction import Control.DeepSeq (NFData(..), force) import Hedgehog diff --git a/source/Test/Unit/Declaration.hs b/source/Felix/Test/Unit/Declaration.hs index 32d979c..f3d9be7 100644 --- a/source/Test/Unit/Declaration.hs +++ b/source/Felix/Test/Unit/Declaration.hs @@ -1,31 +1,31 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Declaration (unitTests) where +module Felix.Test.Unit.Declaration (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core qualified as Core -import Checking.Declaration qualified as Declaration -import Checking.Foundation qualified as Foundation -import Checking.Exact qualified as Exact -import Checking.Exact.Vocabulary qualified as Vocabulary -import Checking.Identity qualified as Identity -import Checking.Kernel.Derivation qualified as Kernel -import Checking.SetConstruction qualified as SetConstruction -import Checking.Semantic qualified as Semantic -import Checking.Typed.Inductive qualified as Typed +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Core qualified as Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Exact.Vocabulary qualified as Vocabulary +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Kernel.Derivation qualified as Kernel +import Felix.Checking.SetConstruction qualified as SetConstruction +import Felix.Checking.Semantic qualified as Semantic +import Felix.Checking.Typed.Inductive qualified as Typed import Felix.Math.Codec import Felix.Module import Felix.Source import Felix.Store qualified as Store import Felix.Meaning qualified as Meaning import Felix.Provers qualified as Provers -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface qualified as Syntax -import Syntax.Internal qualified as Internal -import Syntax.Lexicon qualified as Lexicon +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax +import Felix.Syntax.Internal qualified as Internal +import Felix.Syntax.Lexicon qualified as Lexicon import Data.List.NonEmpty qualified as NonEmpty import Data.IORef qualified as IORef diff --git a/source/Test/Unit/Foundation.hs b/source/Felix/Test/Unit/Foundation.hs index 17ff526..18ead04 100644 --- a/source/Test/Unit/Foundation.hs +++ b/source/Felix/Test/Unit/Foundation.hs @@ -1,10 +1,10 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Foundation (unitTests) where +module Felix.Test.Unit.Foundation (unitTests) where import Base -import Checking.Core -import Checking.Foundation +import Felix.Checking.Core +import Felix.Checking.Foundation import Data.List qualified as List import Data.Set qualified as Set diff --git a/source/Test/Unit/Html.hs b/source/Felix/Test/Unit/Html.hs index c7f24c4..c8395ec 100644 --- a/source/Test/Unit/Html.hs +++ b/source/Felix/Test/Unit/Html.hs @@ -1,17 +1,17 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Html (unitTests) where +module Felix.Test.Unit.Html (unitTests) where import Base import Felix.Parse qualified as Parse import Felix.Source import Felix.Source.Graph import Felix.Workspace qualified as Workspace -import Render.Html qualified as Html -import Render.Html.Context -import Render.Html.Layout -import Report.Location (Location, pattern Nowhere) -import Syntax.Abstract +import Felix.Render.Html qualified as Html +import Felix.Render.Html.Context +import Felix.Render.Html.Layout +import Felix.Report.Location (Location, pattern Nowhere) +import Felix.Syntax.Abstract import Data.Text qualified as Text import Data.Text.IO qualified as TextIO diff --git a/source/Test/Unit/HtmlLayout.hs b/source/Felix/Test/Unit/HtmlLayout.hs index a248f3b..a3d701f 100644 --- a/source/Test/Unit/HtmlLayout.hs +++ b/source/Felix/Test/Unit/HtmlLayout.hs @@ -1,11 +1,11 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.HtmlLayout (unitTests) where +module Felix.Test.Unit.HtmlLayout (unitTests) where import Base import Felix.Source import Felix.Source.Graph -import Render.Html.Layout +import Felix.Render.Html.Layout import Control.Exception (bracket) import Data.List qualified as List diff --git a/source/Test/Unit/HtmlOutput.hs b/source/Felix/Test/Unit/HtmlOutput.hs index 0087f82..34fe2e7 100644 --- a/source/Test/Unit/HtmlOutput.hs +++ b/source/Felix/Test/Unit/HtmlOutput.hs @@ -1,15 +1,15 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.HtmlOutput (unitTests) where +module Felix.Test.Unit.HtmlOutput (unitTests) where import Base import Felix.Parse qualified as Parse import Felix.Source import Felix.Source.Graph qualified as SourceGraph -import Render.Html qualified as Html -import Render.Html.Export -import Render.Html.Output +import Felix.Render.Html qualified as Html +import Felix.Render.Html.Export +import Felix.Render.Html.Output import Control.Exception (bracket) import Data.ByteString qualified as ByteString diff --git a/source/Test/Unit/Identity.hs b/source/Felix/Test/Unit/Identity.hs index 0cb46a5..7e1e73f 100644 --- a/source/Test/Unit/Identity.hs +++ b/source/Felix/Test/Unit/Identity.hs @@ -1,12 +1,12 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Identity (unitTests) where +module Felix.Test.Unit.Identity (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Core qualified as Core -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core qualified as Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module diff --git a/source/Test/Unit/Kernel.hs b/source/Felix/Test/Unit/Kernel.hs index d01a194..7762a7e 100644 --- a/source/Test/Unit/Kernel.hs +++ b/source/Felix/Test/Unit/Kernel.hs @@ -1,17 +1,17 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PatternSynonyms #-} -module Test.Unit.Kernel (unitTests) where +module Felix.Test.Unit.Kernel (unitTests) where import Base hiding (Empty) -import Checking.Core -import Checking.Foundation qualified as Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Semantics qualified as Semantics -import Checking.Kernel.SetLfp qualified as SetLfp -import Checking.Typed.Inductive qualified as Inductive -import Report.Location (pattern Nowhere) -import Syntax.Internal qualified as Internal +import Felix.Checking.Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Kernel.Derivation +import Felix.Checking.Kernel.Semantics qualified as Semantics +import Felix.Checking.Kernel.SetLfp qualified as SetLfp +import Felix.Checking.Typed.Inductive qualified as Inductive +import Felix.Report.Location (pattern Nowhere) +import Felix.Syntax.Internal qualified as Internal import Data.Set qualified as Set import Data.Vector qualified as Vector diff --git a/source/Test/Unit/Lexicon.hs b/source/Felix/Test/Unit/Lexicon.hs index 54b4bd4..4b7f9e7 100644 --- a/source/Test/Unit/Lexicon.hs +++ b/source/Felix/Test/Unit/Lexicon.hs @@ -1,12 +1,12 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Lexicon (unitTests) where +module Felix.Test.Unit.Lexicon (unitTests) where import Base import Felix.Cache.Codec -import Syntax.Abstract -import Syntax.Interface -import Syntax.Lexicon +import Felix.Syntax.Abstract +import Felix.Syntax.Interface +import Felix.Syntax.Lexicon import Data.Set qualified as Set import Test.Tasty diff --git a/source/Test/Unit/Materialization.hs b/source/Felix/Test/Unit/Materialization.hs index fcad7b5..9c4f54f 100644 --- a/source/Test/Unit/Materialization.hs +++ b/source/Felix/Test/Unit/Materialization.hs @@ -1,14 +1,14 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Materialization (unitTests) where +module Felix.Test.Unit.Materialization (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Core qualified as Core -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Materialization qualified as Materialization -import Checking.Semantic qualified as Semantic +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core qualified as Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Materialization qualified as Materialization +import Felix.Checking.Semantic qualified as Semantic import Felix.Math.Codec import Felix.Module import Felix.Source diff --git a/source/Test/Unit/Meaning.hs b/source/Felix/Test/Unit/Meaning.hs index acb33d0..3093a84 100644 --- a/source/Test/Unit/Meaning.hs +++ b/source/Felix/Test/Unit/Meaning.hs @@ -1,13 +1,13 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Meaning (unitTests) where +module Felix.Test.Unit.Meaning (unitTests) where import Base import Felix.Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Internal qualified as Sem -import Syntax.LexicalPhrase +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Internal qualified as Sem +import Felix.Syntax.LexicalPhrase ( unsafeReadPhrase , unsafeReadPhraseSgPl ) diff --git a/source/Test/Unit/Module.hs b/source/Felix/Test/Unit/Module.hs index 13fe90d..44f0ccb 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Felix/Test/Unit/Module.hs @@ -1,40 +1,40 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Module (unitTests) where +module Felix.Test.Unit.Module (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core qualified as Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Datatype qualified as ExactDatatype -import Checking.Exact.Inductive qualified as ExactInductive -import Checking.Exact.Proof qualified as ExactProof -import Checking.FinalPrelude qualified as FinalPrelude -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Module qualified as Module -import Checking.Semantic qualified as Semantic -import Checking.Typed.Inductive qualified as TypedInductive +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Core qualified as Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Exact.Datatype qualified as ExactDatatype +import Felix.Checking.Exact.Inductive qualified as ExactInductive +import Felix.Checking.Exact.Proof qualified as ExactProof +import Felix.Checking.FinalPrelude qualified as FinalPrelude +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Module qualified as Module +import Felix.Checking.Semantic qualified as Semantic +import Felix.Checking.Typed.Inductive qualified as TypedInductive import Felix.CommandLine qualified as CommandLine -import Felix.Module import Felix.Math.Codec +import Felix.Module import Felix.Parse qualified as Parse import Felix.Prelude qualified as Prelude +import Felix.Provers qualified as Provers +import Felix.Report.Location import Felix.Source import Felix.Source.Content qualified as Content import Felix.Store qualified as Store +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax +import Felix.Syntax.Internal qualified as Internal +import Felix.Syntax.Lexicon qualified as Lexicon +import Felix.Syntax.Pragma qualified as Pragma import Felix.Verification qualified as Verification import Felix.Workspace qualified as Workspace -import Report.Location -import Felix.Provers qualified as Provers import Paths_felix qualified as Paths -import Syntax.Abstract qualified as Raw -import Syntax.Internal qualified as Internal -import Syntax.Interface qualified as Syntax -import Syntax.Lexicon qualified as Lexicon -import Syntax.Pragma qualified as Pragma import Control.Concurrent (threadDelay) import Control.Concurrent.STM diff --git a/source/Test/Unit/OutputPlan.hs b/source/Felix/Test/Unit/OutputPlan.hs index 45658bf..803b7da 100644 --- a/source/Test/Unit/OutputPlan.hs +++ b/source/Felix/Test/Unit/OutputPlan.hs @@ -1,6 +1,6 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.OutputPlan (unitTests) where +module Felix.Test.Unit.OutputPlan (unitTests) where import Base import Felix.OutputPlan qualified as Output diff --git a/source/Test/Unit/Provers.hs b/source/Felix/Test/Unit/Provers.hs index 0d0cf1b..f1e3cc1 100644 --- a/source/Test/Unit/Provers.hs +++ b/source/Felix/Test/Unit/Provers.hs @@ -1,10 +1,10 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Provers (unitTests) where +module Felix.Test.Unit.Provers (unitTests) where import Base hiding (Empty) -import Checking.Backend.Problem -import Checking.Core +import Felix.Checking.Backend.Problem +import Felix.Checking.Core import Felix.Provers import Control.Concurrent @@ -26,7 +26,7 @@ import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.IO qualified as Text import Data.Vector qualified as Vector -import Report.Location (Location(..)) +import Felix.Report.Location (Location(..)) import System.Directory qualified as Directory import System.Exit (ExitCode(..)) import System.FilePath.Posix ((</>)) diff --git a/source/Test/Unit/Semantic.hs b/source/Felix/Test/Unit/Semantic.hs index 160735c..f62a003 100644 --- a/source/Test/Unit/Semantic.hs +++ b/source/Felix/Test/Unit/Semantic.hs @@ -1,21 +1,21 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Semantic (unitTests) where +module Felix.Test.Unit.Semantic (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Core qualified as Core -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Semantic qualified as Semantic +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core qualified as Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Semantic qualified as Semantic import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module import Felix.Parsed.Identity import Felix.Source import Felix.Source.Content -import Syntax.Interface qualified as Syntax -import Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax +import Felix.Syntax.Abstract qualified as Raw import Data.ByteString (ByteString) import Data.List qualified as List diff --git a/source/Test/Unit/Source.hs b/source/Felix/Test/Unit/Source.hs index a8e4506..6216381 100644 --- a/source/Test/Unit/Source.hs +++ b/source/Felix/Test/Unit/Source.hs @@ -2,12 +2,12 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} -module Test.Unit.Source (unitTests) where +module Felix.Test.Unit.Source (unitTests) where import Base -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Semantic qualified as Semantic +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Semantic qualified as Semantic import Felix.Cache.Codec qualified as Cache import Felix.Module qualified as Module import Felix.Parse qualified as Parse @@ -18,7 +18,7 @@ import Felix.Source import Felix.Source.Content qualified as Content import Felix.Source.Graph import Felix.Store qualified as Store -import Report.Location +import Felix.Report.Location ( FileId(..) , FileIdAllocator(..) , Location(..) @@ -30,10 +30,10 @@ import Report.Location , locLine , lookupFileIdentityPath ) -import Syntax.Abstract qualified as Raw -import Syntax.Adapt qualified as Adapt -import Syntax.Interface qualified as Interface -import Syntax.Token (runLexer) +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Adapt qualified as Adapt +import Felix.Syntax.Interface qualified as Interface +import Felix.Syntax.Token (runLexer) import Control.Exception (bracket, evaluate) import Data.ByteString qualified as ByteString diff --git a/source/Test/Unit/Store.hs b/source/Felix/Test/Unit/Store.hs index fb207d1..423204c 100644 --- a/source/Test/Unit/Store.hs +++ b/source/Felix/Test/Unit/Store.hs @@ -1,15 +1,15 @@ {-# LANGUAGE NoImplicitPrelude #-} -module Test.Unit.Store (unitTests) where +module Felix.Test.Unit.Store (unitTests) where import Base -import Checking.Authority qualified as Authority -import Checking.Core qualified as Core -import Checking.Declaration qualified as Declaration -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Module qualified as Typed -import Checking.Semantic qualified as Semantic +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core qualified as Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Module qualified as Typed +import Felix.Checking.Semantic qualified as Semantic import Felix.Cache.Codec qualified as Cache import Felix.Math.Codec import Felix.Module @@ -19,7 +19,7 @@ import Felix.Source.Content qualified as Content import Felix.Source import Felix.Store qualified as Store import Felix.Provers qualified as Provers -import Syntax.Interface qualified as Syntax +import Felix.Syntax.Interface qualified as Syntax import Control.Concurrent (threadDelay) import Control.Exception qualified as Exception diff --git a/source/Test/Unit/Token.hs b/source/Felix/Test/Unit/Token.hs index d399e2a..00c6755 100644 --- a/source/Test/Unit/Token.hs +++ b/source/Felix/Test/Unit/Token.hs @@ -1,14 +1,14 @@ {-# LANGUAGE OverloadedStrings #-} -module Test.Unit.Token (unitTests) where +module Felix.Test.Unit.Token (unitTests) where import Base -import Report.Location -import Syntax.Adapt -import Syntax.Abstract (Associativity(..)) -import Syntax.Interface -import Syntax.Pragma -import Syntax.Token +import Felix.Report.Location +import Felix.Syntax.Adapt +import Felix.Syntax.Abstract (Associativity(..)) +import Felix.Syntax.Interface +import Felix.Syntax.Pragma +import Felix.Syntax.Token import Data.Text qualified as Text import Test.Tasty diff --git a/source/Felix/Verification.hs b/source/Felix/Verification.hs index 572f3ce..716beea 100644 --- a/source/Felix/Verification.hs +++ b/source/Felix/Verification.hs @@ -48,11 +48,11 @@ module Felix.Verification import Base -import Checking.Declaration qualified as Declaration -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Module qualified as Typed -import Checking.Semantic qualified as Semantic +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Module qualified as Typed +import Felix.Checking.Semantic qualified as Semantic import Felix.Module (localDeclarationOrdinal) import Felix.Parse (ParseWorkspaceError(..), ParsedSourceWorkspace) import Felix.Parse qualified as Felix @@ -61,10 +61,10 @@ import Felix.Provers import Felix.Source import Felix.Source.Graph (ResolvedSourceGraph) import Felix.Store qualified as Store -import Render.Html.Export qualified as HtmlExport -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface qualified as Syntax +import Felix.Render.Html.Export qualified as HtmlExport +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax import Control.Exception qualified as Exception import Control.Monad (unless) diff --git a/source/Felix/Workspace.hs b/source/Felix/Workspace.hs index 6a13d42..b9034c5 100644 --- a/source/Felix/Workspace.hs +++ b/source/Felix/Workspace.hs @@ -29,11 +29,11 @@ import Felix.Prelude qualified as Prelude import Felix.Source import Felix.Source.Graph (ResolvedSourceGraph) import Felix.Source.Graph qualified as SourceGraph -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Adapt (ScannedLexicalItem, scanChunk) -import Syntax.Lexicon (builtins) -import Syntax.Token +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Adapt (ScannedLexicalItem, scanChunk) +import Felix.Syntax.Lexicon (builtins) +import Felix.Syntax.Token import Control.Exception qualified as Exception import Data.Bifunctor (first) diff --git a/source/Test/Unit.hs b/source/Test/Unit.hs deleted file mode 100644 index 3e5817c..0000000 --- a/source/Test/Unit.hs +++ /dev/null @@ -1,52 +0,0 @@ -module Test.Unit where - - -import Test.Tasty -import Test.Unit.Abstract qualified as Abstract -import Test.Unit.Backend qualified as Backend -import Test.Unit.CommandLine qualified as CommandLine -import Test.Unit.Concrete qualified as Concrete -import Test.Unit.Core qualified as Core -import Test.Unit.Declaration qualified as Declaration -import Test.Unit.Foundation qualified as Foundation -import Test.Unit.Identity qualified as Identity -import Test.Unit.Html qualified as Html -import Test.Unit.HtmlLayout qualified as HtmlLayout -import Test.Unit.HtmlOutput qualified as HtmlOutput -import Test.Unit.Kernel qualified as Kernel -import Test.Unit.Lexicon qualified as Lexicon -import Test.Unit.Meaning qualified as Meaning -import Test.Unit.Materialization qualified as Materialization -import Test.Unit.Module qualified as Module -import Test.Unit.OutputPlan qualified as OutputPlan -import Test.Unit.Provers qualified as Provers -import Test.Unit.Semantic qualified as Semantic -import Test.Unit.Source qualified as Source -import Test.Unit.Store qualified as Store -import Test.Unit.Token qualified as Token - -unitTests :: TestTree -unitTests = testGroup "unit tests" - [ Abstract.unitTests - , Backend.unitTests - , CommandLine.unitTests - , Concrete.unitTests - , Core.unitTests - , Declaration.unitTests - , Foundation.unitTests - , Identity.unitTests - , Html.unitTests - , HtmlLayout.unitTests - , HtmlOutput.unitTests - , Kernel.unitTests - , Lexicon.unitTests - , Meaning.unitTests - , Materialization.unitTests - , Module.unitTests - , OutputPlan.unitTests - , Provers.unitTests - , Semantic.unitTests - , Source.unitTests - , Store.unitTests - , Token.unitTests - ] |