| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Conformance.Story.Binding
Description
Revision-bound Lean identities and statement anchors.
Synopsis
- data BoundObligation = BoundObligation {
- boName :: !String
- boDigest :: !String
- boRevision :: !String
- type Binding = BoundObligation
- data ManifestEntry = ManifestEntry {}
- mkBoundObligation :: String -> String -> String -> BoundObligation
- firstExisting :: [FilePath] -> IO (Maybe FilePath)
- loadManifest :: IO (Either String [(String, String)])
- resolveBinding :: [(String, String)] -> Binding -> Bool
- loadStatementSource :: IO (Either String String)
- anchorsPresent :: String -> [(String, [String])] -> Bool
- nameViolation :: String -> Bool
- resolveClause :: [(String, [String])] -> Binding -> [Text] -> Bool
Documentation
data BoundObligation Source #
A Lean obligation the programs bind to.
Constructors
| BoundObligation | |
Fields
| |
Instances
| Show BoundObligation Source # | |
Defined in Conformance.Story.Binding Methods showsPrec :: Int -> BoundObligation -> ShowS Source # show :: BoundObligation -> String Source # showList :: [BoundObligation] -> ShowS Source # | |
| Eq BoundObligation Source # | |
Defined in Conformance.Story.Binding Methods (==) :: BoundObligation -> BoundObligation -> Bool Source # (/=) :: BoundObligation -> BoundObligation -> Bool Source # | |
type Binding = BoundObligation Source #
A binding is a bound obligation.
data ManifestEntry Source #
One row of the repository's statement manifest.
Constructors
| ManifestEntry | |
Instances
| FromJSON ManifestEntry Source # | |
Defined in Conformance.Story.Binding Methods parseJSON :: Value -> Parser ManifestEntry parseJSONList :: Value -> Parser [ManifestEntry] omittedField :: Maybe ManifestEntry | |
mkBoundObligation :: String -> String -> String -> BoundObligation Source #
Name a bound obligation by qualified declaration, digest, revision.
firstExisting :: [FilePath] -> IO (Maybe FilePath) Source #
First of the candidate paths that exists on disk.
loadManifest :: IO (Either String [(String, String)]) Source #
Read the repository's own statement manifest.
resolveBinding :: [(String, String)] -> Binding -> Bool Source #
A binding resolves exactly when the manifest carries the named declaration under the pinned digest.
loadStatementSource :: IO (Either String String) Source #
Read the bound Lean source.
anchorsPresent :: String -> [(String, [String])] -> Bool Source #
Every anchor quoted anywhere in the inventory appears verbatim in the source.
nameViolation :: String -> Bool Source #
Whether a clause or example name smuggles in a row ID or ticket number. One predicate, used by every hygiene check.
resolveClause :: [(String, [String])] -> Binding -> [Text] -> Bool Source #
A clause resolves exactly when every selected anchor belongs to the named obligation's inventory.