Prototype: OGPoset Diagram daa structure
This commit is contained in:
commit
d251afe902
3
.gitignore
vendored
Normal file
3
.gitignore
vendored
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
TAGS
|
||||||
|
tags
|
||||||
|
dist-newstyle/
|
5
CHANGELOG.md
Normal file
5
CHANGELOG.md
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
# Revision history for proto
|
||||||
|
|
||||||
|
## 0.1.0.0 -- YYYY-mm-dd
|
||||||
|
|
||||||
|
* First version. Released on an unsuspecting world.
|
29
LICENSE
Normal file
29
LICENSE
Normal file
@ -0,0 +1,29 @@
|
|||||||
|
Copyright (c) 2025, Obsidian Systems
|
||||||
|
|
||||||
|
|
||||||
|
Redistribution and use in source and binary forms, with or without
|
||||||
|
modification, are permitted provided that the following conditions are met:
|
||||||
|
|
||||||
|
* Redistributions of source code must retain the above copyright
|
||||||
|
notice, this list of conditions and the following disclaimer.
|
||||||
|
|
||||||
|
* Redistributions in binary form must reproduce the above
|
||||||
|
copyright notice, this list of conditions and the following
|
||||||
|
disclaimer in the documentation and/or other materials provided
|
||||||
|
with the distribution.
|
||||||
|
|
||||||
|
* Neither the name of the copyright holder nor the names of its
|
||||||
|
contributors may be used to endorse or promote products derived
|
||||||
|
from this software without specific prior written permission.
|
||||||
|
|
||||||
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||||
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||||
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||||
|
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||||
|
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||||
|
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||||
|
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||||
|
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||||
|
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||||
|
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||||
|
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
2
nix-thunk/default.nix
Normal file
2
nix-thunk/default.nix
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
# DO NOT HAND-EDIT THIS FILE
|
||||||
|
import (import ./thunk.nix)
|
7
nix-thunk/github.json
Normal file
7
nix-thunk/github.json
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
{
|
||||||
|
"owner": "obsidiansystems",
|
||||||
|
"repo": "nix-thunk",
|
||||||
|
"private": false,
|
||||||
|
"rev": "c10ac03047c88c1f2aed882d3cf2e60d0f7a0ac4",
|
||||||
|
"sha256": "1bhf9hq1wpb6qd126w6d54zbyjwggdky50ppsxlvg1fxmfd2kv67"
|
||||||
|
}
|
12
nix-thunk/thunk.nix
Normal file
12
nix-thunk/thunk.nix
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
# DO NOT HAND-EDIT THIS FILE
|
||||||
|
let fetch = { private ? false, fetchSubmodules ? false, owner, repo, rev, sha256, ... }:
|
||||||
|
if !fetchSubmodules && !private then builtins.fetchTarball {
|
||||||
|
url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; inherit sha256;
|
||||||
|
} else (import (builtins.fetchTarball {
|
||||||
|
url = "https://github.com/NixOS/nixpkgs/archive/3aad50c30c826430b0270fcf8264c8c41b005403.tar.gz";
|
||||||
|
sha256 = "0xwqsf08sywd23x0xvw4c4ghq0l28w2ki22h0bdn766i16z9q2gr";
|
||||||
|
}) {}).fetchFromGitHub {
|
||||||
|
inherit owner repo rev sha256 fetchSubmodules private;
|
||||||
|
};
|
||||||
|
json = builtins.fromJSON (builtins.readFile ./github.json);
|
||||||
|
in fetch json
|
2
nixpkgs/default.nix
Normal file
2
nixpkgs/default.nix
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
# DO NOT HAND-EDIT THIS FILE
|
||||||
|
import (import ./thunk.nix)
|
8
nixpkgs/github.json
Normal file
8
nixpkgs/github.json
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
{
|
||||||
|
"owner": "nixos",
|
||||||
|
"repo": "nixpkgs",
|
||||||
|
"branch": "nixos-25.05",
|
||||||
|
"private": false,
|
||||||
|
"rev": "ddae11e58c0c345bf66efbddbf2192ed0e58f896",
|
||||||
|
"sha256": "1g53q4i7b2qs2h1iwif9ixjlmk65mrznf322x8sl2vbjcbjq1ify"
|
||||||
|
}
|
12
nixpkgs/thunk.nix
Normal file
12
nixpkgs/thunk.nix
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
# DO NOT HAND-EDIT THIS FILE
|
||||||
|
let fetch = { private ? false, fetchSubmodules ? false, owner, repo, rev, sha256, ... }:
|
||||||
|
if !fetchSubmodules && !private then builtins.fetchTarball {
|
||||||
|
url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; inherit sha256;
|
||||||
|
} else (import (builtins.fetchTarball {
|
||||||
|
url = "https://github.com/NixOS/nixpkgs/archive/3aad50c30c826430b0270fcf8264c8c41b005403.tar.gz";
|
||||||
|
sha256 = "0xwqsf08sywd23x0xvw4c4ghq0l28w2ki22h0bdn766i16z9q2gr";
|
||||||
|
}) {}).fetchFromGitHub {
|
||||||
|
inherit owner repo rev sha256 fetchSubmodules private;
|
||||||
|
};
|
||||||
|
json = builtins.fromJSON (builtins.readFile ./github.json);
|
||||||
|
in fetch json
|
82
proto.cabal
Normal file
82
proto.cabal
Normal file
@ -0,0 +1,82 @@
|
|||||||
|
cabal-version: 3.0
|
||||||
|
-- The cabal-version field refers to the version of the .cabal specification,
|
||||||
|
-- and can be different from the cabal-install (the tool) version and the
|
||||||
|
-- Cabal (the library) version you are using. As such, the Cabal (the library)
|
||||||
|
-- version used must be equal or greater than the version stated in this field.
|
||||||
|
-- Starting from the specification version 2.2, the cabal-version field must be
|
||||||
|
-- the first thing in the cabal file.
|
||||||
|
|
||||||
|
-- Initial package description 'proto' generated by
|
||||||
|
-- 'cabal init'. For further documentation, see:
|
||||||
|
-- http://haskell.org/cabal/users-guide/
|
||||||
|
--
|
||||||
|
-- The name of the package.
|
||||||
|
name: proto
|
||||||
|
|
||||||
|
-- The package version.
|
||||||
|
-- See the Haskell package versioning policy (PVP) for standards
|
||||||
|
-- guiding when and how versions should be incremented.
|
||||||
|
-- https://pvp.haskell.org
|
||||||
|
-- PVP summary: +-+------- breaking API changes
|
||||||
|
-- | | +----- non-breaking API additions
|
||||||
|
-- | | | +--- code changes with no API change
|
||||||
|
version: 0.1.0.0
|
||||||
|
|
||||||
|
-- A short (one-line) description of the package.
|
||||||
|
-- synopsis:
|
||||||
|
|
||||||
|
-- A longer description of the package.
|
||||||
|
-- description:
|
||||||
|
|
||||||
|
-- The license under which the package is released.
|
||||||
|
license: BSD-3-Clause
|
||||||
|
|
||||||
|
-- The file containing the license text.
|
||||||
|
license-file: LICENSE
|
||||||
|
|
||||||
|
-- The package author(s).
|
||||||
|
author: Obsidian Systems
|
||||||
|
|
||||||
|
-- An email address to which users can send suggestions, bug reports, and patches.
|
||||||
|
maintainer: maintainer@obsidian.systems
|
||||||
|
|
||||||
|
-- A copyright notice.
|
||||||
|
-- copyright:
|
||||||
|
build-type: Simple
|
||||||
|
|
||||||
|
-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.
|
||||||
|
extra-doc-files: CHANGELOG.md
|
||||||
|
|
||||||
|
-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
|
||||||
|
-- extra-source-files:
|
||||||
|
|
||||||
|
common warnings
|
||||||
|
ghc-options: -Wall
|
||||||
|
|
||||||
|
library
|
||||||
|
-- Import common warning flags.
|
||||||
|
import: warnings
|
||||||
|
|
||||||
|
-- Modules exported by the library.
|
||||||
|
exposed-modules: Diagram
|
||||||
|
|
||||||
|
-- Modules included in this library but not exported.
|
||||||
|
-- other-modules:
|
||||||
|
|
||||||
|
-- LANGUAGE extensions used by modules in this package.
|
||||||
|
default-extensions:
|
||||||
|
ImportQualifiedPost
|
||||||
|
LambdaCase
|
||||||
|
RankNTypes
|
||||||
|
|
||||||
|
-- Other library packages from which modules are imported.
|
||||||
|
build-depends: base ^>=4.19.2.0
|
||||||
|
, containers
|
||||||
|
, semialign
|
||||||
|
, these
|
||||||
|
|
||||||
|
-- Directories containing source files.
|
||||||
|
hs-source-dirs: src
|
||||||
|
|
||||||
|
-- Base language which the package is written in.
|
||||||
|
default-language: Haskell2010
|
18
shell.nix
Normal file
18
shell.nix
Normal file
@ -0,0 +1,18 @@
|
|||||||
|
let
|
||||||
|
pkgs = import ./nixpkgs {};
|
||||||
|
nixThunk = import ./nix-thunk {};
|
||||||
|
haskellPackages = pkgs.haskellPackages.override {
|
||||||
|
overrides = self: super: {
|
||||||
|
};
|
||||||
|
};
|
||||||
|
in
|
||||||
|
pkgs.mkShell {
|
||||||
|
name = "proto";
|
||||||
|
buildInputs = [
|
||||||
|
pkgs.cabal-install
|
||||||
|
pkgs.ghcid
|
||||||
|
];
|
||||||
|
inputsFrom = [
|
||||||
|
(haskellPackages.callCabal2nix "proto" (import ./src.nix) {}).env
|
||||||
|
];
|
||||||
|
}
|
8
src.nix
Normal file
8
src.nix
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
builtins.filterSource (path: type: !(builtins.elem (baseNameOf path) [
|
||||||
|
"release.nix"
|
||||||
|
".git"
|
||||||
|
"dist"
|
||||||
|
"cabal.haskell-ci"
|
||||||
|
"cabal.project"
|
||||||
|
".travis.yml"
|
||||||
|
])) ./.
|
78
src/Diagram.hs
Normal file
78
src/Diagram.hs
Normal file
@ -0,0 +1,78 @@
|
|||||||
|
module Diagram
|
||||||
|
( Polarity(..)
|
||||||
|
, Diagram
|
||||||
|
, empty
|
||||||
|
, insert
|
||||||
|
, InsertError(..)
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad
|
||||||
|
import Data.Map (Map)
|
||||||
|
import Data.Map qualified as Map
|
||||||
|
import Data.Semialign.Indexed
|
||||||
|
import Data.Set qualified as Set
|
||||||
|
import Data.Set (Set)
|
||||||
|
import Data.These
|
||||||
|
|
||||||
|
data Polarity = Negative | Positive
|
||||||
|
deriving (Eq, Ord, Read, Show)
|
||||||
|
|
||||||
|
-- | Diagram supporting oriented graded posets
|
||||||
|
data Diagram vtx = Diagram
|
||||||
|
{ _diagram_grades :: Map vtx Int
|
||||||
|
-- ^ The grade of each vertex
|
||||||
|
, _diagram_down :: Map vtx (Map vtx Polarity)
|
||||||
|
-- ^ Only the "downward" connections. Can be thought of as "boundaries" or "faces"
|
||||||
|
, _diagram_up :: Map vtx (Map vtx Polarity)
|
||||||
|
-- ^ Only the "upward" connections. The outer vertex is what we're focused on
|
||||||
|
-- and the things in the inner map represent cells that the outer vertex is a
|
||||||
|
-- face of
|
||||||
|
}
|
||||||
|
deriving (Show, Read)
|
||||||
|
|
||||||
|
data Direction
|
||||||
|
= Up
|
||||||
|
| Down
|
||||||
|
deriving (Eq, Ord, Read, Show)
|
||||||
|
|
||||||
|
data InsertError vtx
|
||||||
|
= InsertError_DuplicateVertex
|
||||||
|
| InsertError_UnknownDownVertex vtx
|
||||||
|
| InsertError_DownVertexUnreachable vtx
|
||||||
|
| InsertError_DownPolarityMissing (Set Polarity)
|
||||||
|
deriving (Show, Read)
|
||||||
|
|
||||||
|
empty :: Diagram vtx
|
||||||
|
empty = Diagram Map.empty Map.empty Map.empty
|
||||||
|
|
||||||
|
insert
|
||||||
|
:: forall vtx. Ord vtx
|
||||||
|
=> vtx
|
||||||
|
-> Int
|
||||||
|
-> Map vtx Polarity
|
||||||
|
-> Diagram vtx
|
||||||
|
-> Either (InsertError vtx) (Diagram vtx)
|
||||||
|
insert vtx grade down d = do
|
||||||
|
when (Map.member vtx $ _diagram_grades d) $ Left InsertError_DuplicateVertex
|
||||||
|
when (grade /= 0) $ do
|
||||||
|
let expectedPolarities = Set.fromList [Negative, Positive]
|
||||||
|
missingPolarities = Set.difference expectedPolarities (Set.fromList (Map.elems down))
|
||||||
|
when (not $ Set.null missingPolarities) $
|
||||||
|
Left $ InsertError_DownPolarityMissing missingPolarities
|
||||||
|
sequence_ $ ialignWith check (_diagram_grades d) down
|
||||||
|
let up = Map.fromList $ [ (vtx', Map.singleton vtx p) | (vtx', p) <- Map.toList down ]
|
||||||
|
return $ Diagram
|
||||||
|
{ _diagram_grades = Map.insert vtx grade $ _diagram_grades d
|
||||||
|
, _diagram_down = Map.insert vtx down $ _diagram_down d
|
||||||
|
, _diagram_up = Map.unionWith Map.union up $ _diagram_up d
|
||||||
|
}
|
||||||
|
where
|
||||||
|
check
|
||||||
|
:: vtx
|
||||||
|
-> These Int Polarity
|
||||||
|
-> Either (InsertError vtx) ()
|
||||||
|
check k = \case
|
||||||
|
This _ -> pure () -- Not in the down set
|
||||||
|
That _ -> Left $ InsertError_UnknownDownVertex k
|
||||||
|
These g _ | g == grade-1 -> pure ()
|
||||||
|
These _ _ -> Left $ InsertError_DownVertexUnreachable k
|
Loading…
x
Reference in New Issue
Block a user