From 14a4f246b61e763cea32281e3a5f73bde38fe5d4 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 16 Feb 2024 20:29:43 -0600 Subject: Add helper function for merging finite sets --- .gitignore | 4 +-- FinMerge.agda | 51 ++++++++++++++++++++++++++++++++++++++ Setup.hs | 2 -- package.yaml | 69 ---------------------------------------------------- src/Circuit.hs | 41 ------------------------------- stack.yaml | 67 -------------------------------------------------- stack.yaml.lock | 13 ---------- tiny/.gitignore | 3 +++ tiny/Setup.hs | 2 ++ tiny/package.yaml | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++ tiny/src/Circuit.hs | 41 +++++++++++++++++++++++++++++++ tiny/stack.yaml | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++ tiny/stack.yaml.lock | 13 ++++++++++ 13 files changed, 247 insertions(+), 195 deletions(-) create mode 100644 FinMerge.agda delete mode 100644 Setup.hs delete mode 100644 package.yaml delete mode 100644 src/Circuit.hs delete mode 100644 stack.yaml delete mode 100644 stack.yaml.lock create mode 100644 tiny/.gitignore create mode 100644 tiny/Setup.hs create mode 100644 tiny/package.yaml create mode 100644 tiny/src/Circuit.hs create mode 100644 tiny/stack.yaml create mode 100644 tiny/stack.yaml.lock diff --git a/.gitignore b/.gitignore index d3e342b..171a389 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1 @@ -.stack-work/ -*~ -circuits.cabal +*.agdai diff --git a/FinMerge.agda b/FinMerge.agda new file mode 100644 index 0000000..a327602 --- /dev/null +++ b/FinMerge.agda @@ -0,0 +1,51 @@ +module FinMerge where + +open import Data.Fin using (Fin; splitAt; join; fromℕ<; cast) +open import Data.Nat using (ℕ; _+_; _≤_; _<_) +open import Data.Nat.Properties using (+-comm) +open import Data.Sum.Base using (_⊎_) +open import Data.Product using (_×_; _,_; Σ-syntax; map₂) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym) +open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) +open import Function using (_$_) + + +_<_≤_ : ℕ → ℕ → ℕ → Set +_<_≤_ i j k = (i < j) × (j ≤ k) + +_<_<_ : ℕ → ℕ → ℕ → Set +_<_<_ i j k = (i < j) × (j < k) + +private + variable + m n : ℕ + +-- Send the 0th index of the right set to the specified index of the left +merge0 : (i : Fin m) → Fin m ⊎ Fin (ℕ.suc n) → Fin m ⊎ Fin n +merge0 i (_⊎_.inj₁ x) = _⊎_.inj₁ x +merge0 i (_⊎_.inj₂ Fin.zero) = _⊎_.inj₁ i +merge0 i (_⊎_.inj₂ (Fin.suc y)) = _⊎_.inj₂ y + +-- Split a natural number into two parts +splitℕ : m ≤ n → Σ[ m′ ∈ ℕ ] n ≡ m + m′ +splitℕ _≤_.z≤n = _ , refl +splitℕ (_≤_.s≤s le) = map₂ (cong ℕ.suc) (splitℕ le) + +-- Merge two elements of a finite set +merge : (i j : ℕ) → i < j ≤ n → Fin (ℕ.suc n) → Fin n +merge {n} i j (lt , le) x with splitℕ le +... | j′ , n≡j+j′ = + cast (sym n≡j+j′) $ + join j j′ $ + merge0 (fromℕ< lt) $ + splitAt j $ + cast Sn≡j+Sj′ x + where + open ≡-Reasoning + Sn≡j+Sj′ : ℕ.suc n ≡ j + ℕ.suc j′ + Sn≡j+Sj′ = begin + ℕ.suc n ≡⟨ cong ℕ.suc (n≡j+j′) ⟩ + ℕ.suc (j + j′) ≡⟨ cong ℕ.suc (+-comm j j′) ⟩ + ℕ.suc (j′ + j) ≡⟨⟩ + ℕ.suc j′ + j ≡⟨ +-comm (ℕ.suc j′) j ⟩ + j + ℕ.suc j′ ∎ diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 index 9a994af..0000000 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/package.yaml b/package.yaml deleted file mode 100644 index 5793777..0000000 --- a/package.yaml +++ /dev/null @@ -1,69 +0,0 @@ -name: circuits -version: 0.1.0.0 -github: "githubuser/circuits" -license: BSD3 -author: "Author name here" -maintainer: "example@example.com" -copyright: "2022 Author name here" - -extra-source-files: -- README.md - -# Metadata used when publishing your package -# synopsis: Short description of your package -# category: Web - -# To avoid duplicated efforts in documentation and dealing with the -# complications of embedding Haddock markup inside cabal files, it is -# common to point users to the README.md file. -description: Please see the README on GitHub at - -dependencies: -- base >= 4.7 && < 5 -- rio - -library: - source-dirs: src - -ghc-options: -- -Wall -- -Wcompat -- -Wincomplete-record-updates -- -Wredundant-constraints -- -Wmissing-local-signatures -- -Wmissing-export-lists -- -Wpartial-fields -- -Wmonomorphism-restriction -- -Widentities -- -Wno-unticked-promoted-constructors -- -fprint-expanded-synonyms - -default-extensions: -- ApplicativeDo -- BangPatterns -- ConstraintKinds -- DataKinds -- EmptyCase -- ExistentialQuantification -- FlexibleContexts -- FlexibleInstances -- GADTs -- GeneralizedNewtypeDeriving -- InstanceSigs -- KindSignatures -- LambdaCase -- MultiParamTypeClasses -- NoImplicitPrelude -- NoStarIsType -- OverloadedStrings -- PatternSynonyms -- PolyKinds -- RankNTypes -- ScopedTypeVariables -- StandaloneDeriving -- StandaloneKindSignatures -- TupleSections -- TypeApplications -- TypeFamilies -- TypeFamilyDependencies -- TypeOperators diff --git a/src/Circuit.hs b/src/Circuit.hs deleted file mode 100644 index d64e8c1..0000000 --- a/src/Circuit.hs +++ /dev/null @@ -1,41 +0,0 @@ -module Circuit () where - -import RIO - -import Data.Kind - - -data Nat = Zero | Succ Nat | Plus Nat Nat - -data Env :: Nat -> Type -> Type where - Leaf :: Env Zero a - Cons :: a -> Env n a -> Env (Succ n) a - Node :: Env l a -> Env r a -> Env (Plus l r) a - -data Circuit :: Nat -> Type -> Type where - Con :: Int -> Circuit Zero t - Var :: t -> Circuit Zero t - Add :: Circuit m t -> Circuit n t -> Circuit (Plus m n) t - Let :: Circuit m t -> (t -> Circuit n t) -> Circuit (Plus m n) t - Fix :: (t -> Circuit n t) -> Circuit n t - Reg :: Circuit n t -> Circuit (Succ n) t - -eval :: (Circuit n Int, Env n Int) -> Int -eval (Con i , _) = i -eval (Var x , _) = x -eval (Add e1 e2, Node l r) = eval (e1, l) + eval (e2, r) -eval (Let e1 e2, Node l r) = eval (e2 (eval (e1, l)), r) -eval (Fix e , env) = fix (\x -> eval (e x, env)) -eval (Reg _ , Cons v _) = v - -step :: (Circuit n Int, Env n Int) -> Env n Int -step (Con i , _) = Leaf -step (Var x , _) = Leaf -step (Add e1 e2, Node l r) = Node (step (e1, l)) (step (e2, r)) -step (Let e1 e2, Node l r) = Node (step (e1, l)) (step (e2 (eval (e1, l)), r)) -step (Fix e , env) = step (fix (\e' -> e (eval (e', env))), env) -step (Reg e , Cons _ vs) = Cons (eval (e, vs)) (step (e, vs)) - -acc i = Fix (\x -> Reg (Add (Var x) (Var i))) -fib = Fix (\x -> Reg (acc x)) -pipe = Reg (Reg (Reg (Reg (Reg (Reg (Con 6)))))) diff --git a/stack.yaml b/stack.yaml deleted file mode 100644 index 3dffb2e..0000000 --- a/stack.yaml +++ /dev/null @@ -1,67 +0,0 @@ -# This file was automatically generated by 'stack init' -# -# Some commonly used options have been documented as comments in this file. -# For advanced use and comprehensive documentation of the format, please see: -# https://docs.haskellstack.org/en/stable/yaml_configuration/ - -# Resolver to choose a 'specific' stackage snapshot or a compiler version. -# A snapshot resolver dictates the compiler version and the set of packages -# to be used for project dependencies. For example: -# -# resolver: lts-3.5 -# resolver: nightly-2015-09-21 -# resolver: ghc-7.10.2 -# -# The location of a snapshot can be provided as a file or url. Stack assumes -# a snapshot provided as a file might change, whereas a url resource does not. -# -# resolver: ./custom-snapshot.yaml -# resolver: https://example.com/snapshots/2018-01-01.yaml -resolver: - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml - -# User packages to be built. -# Various formats can be used as shown in the example below. -# -# packages: -# - some-directory -# - https://example.com/foo/bar/baz-0.0.2.tar.gz -# subdirs: -# - auto-update -# - wai -packages: -- . -# Dependency packages to be pulled from upstream that are not in the resolver. -# These entries can reference officially published versions as well as -# forks / in-progress versions pinned to a git hash. For example: -# -# extra-deps: -# - acme-missiles-0.3 -# - git: https://github.com/commercialhaskell/stack.git -# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a -# -# extra-deps: [] - -# Override default flag values for local packages and extra-deps -# flags: {} - -# Extra package databases containing global packages -# extra-package-dbs: [] - -# Control whether we use the GHC we find on the path -# system-ghc: true -# -# Require a specific version of stack, using version ranges -# require-stack-version: -any # Default -# require-stack-version: ">=2.7" -# -# Override the architecture used by stack, especially useful on Windows -# arch: i386 -# arch: x86_64 -# -# Extra directories used by stack for building -# extra-include-dirs: [/path/to/dir] -# extra-lib-dirs: [/path/to/dir] -# -# Allow a newer minor version of GHC than the snapshot specifies -# compiler-check: newer-minor diff --git a/stack.yaml.lock b/stack.yaml.lock deleted file mode 100644 index dc9b6b0..0000000 --- a/stack.yaml.lock +++ /dev/null @@ -1,13 +0,0 @@ -# This file was autogenerated by Stack. -# You should not edit this file by hand. -# For more information, please see the documentation at: -# https://docs.haskellstack.org/en/stable/lock_files - -packages: [] -snapshots: -- completed: - size: 619405 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml - sha256: 7f4393ad659c579944d12202cffb12d8e4b8114566b015f77bbc303a24cff934 - original: - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml diff --git a/tiny/.gitignore b/tiny/.gitignore new file mode 100644 index 0000000..d3e342b --- /dev/null +++ b/tiny/.gitignore @@ -0,0 +1,3 @@ +.stack-work/ +*~ +circuits.cabal diff --git a/tiny/Setup.hs b/tiny/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/tiny/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/tiny/package.yaml b/tiny/package.yaml new file mode 100644 index 0000000..5793777 --- /dev/null +++ b/tiny/package.yaml @@ -0,0 +1,69 @@ +name: circuits +version: 0.1.0.0 +github: "githubuser/circuits" +license: BSD3 +author: "Author name here" +maintainer: "example@example.com" +copyright: "2022 Author name here" + +extra-source-files: +- README.md + +# Metadata used when publishing your package +# synopsis: Short description of your package +# category: Web + +# To avoid duplicated efforts in documentation and dealing with the +# complications of embedding Haddock markup inside cabal files, it is +# common to point users to the README.md file. +description: Please see the README on GitHub at + +dependencies: +- base >= 4.7 && < 5 +- rio + +library: + source-dirs: src + +ghc-options: +- -Wall +- -Wcompat +- -Wincomplete-record-updates +- -Wredundant-constraints +- -Wmissing-local-signatures +- -Wmissing-export-lists +- -Wpartial-fields +- -Wmonomorphism-restriction +- -Widentities +- -Wno-unticked-promoted-constructors +- -fprint-expanded-synonyms + +default-extensions: +- ApplicativeDo +- BangPatterns +- ConstraintKinds +- DataKinds +- EmptyCase +- ExistentialQuantification +- FlexibleContexts +- FlexibleInstances +- GADTs +- GeneralizedNewtypeDeriving +- InstanceSigs +- KindSignatures +- LambdaCase +- MultiParamTypeClasses +- NoImplicitPrelude +- NoStarIsType +- OverloadedStrings +- PatternSynonyms +- PolyKinds +- RankNTypes +- ScopedTypeVariables +- StandaloneDeriving +- StandaloneKindSignatures +- TupleSections +- TypeApplications +- TypeFamilies +- TypeFamilyDependencies +- TypeOperators diff --git a/tiny/src/Circuit.hs b/tiny/src/Circuit.hs new file mode 100644 index 0000000..d64e8c1 --- /dev/null +++ b/tiny/src/Circuit.hs @@ -0,0 +1,41 @@ +module Circuit () where + +import RIO + +import Data.Kind + + +data Nat = Zero | Succ Nat | Plus Nat Nat + +data Env :: Nat -> Type -> Type where + Leaf :: Env Zero a + Cons :: a -> Env n a -> Env (Succ n) a + Node :: Env l a -> Env r a -> Env (Plus l r) a + +data Circuit :: Nat -> Type -> Type where + Con :: Int -> Circuit Zero t + Var :: t -> Circuit Zero t + Add :: Circuit m t -> Circuit n t -> Circuit (Plus m n) t + Let :: Circuit m t -> (t -> Circuit n t) -> Circuit (Plus m n) t + Fix :: (t -> Circuit n t) -> Circuit n t + Reg :: Circuit n t -> Circuit (Succ n) t + +eval :: (Circuit n Int, Env n Int) -> Int +eval (Con i , _) = i +eval (Var x , _) = x +eval (Add e1 e2, Node l r) = eval (e1, l) + eval (e2, r) +eval (Let e1 e2, Node l r) = eval (e2 (eval (e1, l)), r) +eval (Fix e , env) = fix (\x -> eval (e x, env)) +eval (Reg _ , Cons v _) = v + +step :: (Circuit n Int, Env n Int) -> Env n Int +step (Con i , _) = Leaf +step (Var x , _) = Leaf +step (Add e1 e2, Node l r) = Node (step (e1, l)) (step (e2, r)) +step (Let e1 e2, Node l r) = Node (step (e1, l)) (step (e2 (eval (e1, l)), r)) +step (Fix e , env) = step (fix (\e' -> e (eval (e', env))), env) +step (Reg e , Cons _ vs) = Cons (eval (e, vs)) (step (e, vs)) + +acc i = Fix (\x -> Reg (Add (Var x) (Var i))) +fib = Fix (\x -> Reg (acc x)) +pipe = Reg (Reg (Reg (Reg (Reg (Reg (Con 6)))))) diff --git a/tiny/stack.yaml b/tiny/stack.yaml new file mode 100644 index 0000000..3dffb2e --- /dev/null +++ b/tiny/stack.yaml @@ -0,0 +1,67 @@ +# This file was automatically generated by 'stack init' +# +# Some commonly used options have been documented as comments in this file. +# For advanced use and comprehensive documentation of the format, please see: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# Resolver to choose a 'specific' stackage snapshot or a compiler version. +# A snapshot resolver dictates the compiler version and the set of packages +# to be used for project dependencies. For example: +# +# resolver: lts-3.5 +# resolver: nightly-2015-09-21 +# resolver: ghc-7.10.2 +# +# The location of a snapshot can be provided as a file or url. Stack assumes +# a snapshot provided as a file might change, whereas a url resource does not. +# +# resolver: ./custom-snapshot.yaml +# resolver: https://example.com/snapshots/2018-01-01.yaml +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml + +# User packages to be built. +# Various formats can be used as shown in the example below. +# +# packages: +# - some-directory +# - https://example.com/foo/bar/baz-0.0.2.tar.gz +# subdirs: +# - auto-update +# - wai +packages: +- . +# Dependency packages to be pulled from upstream that are not in the resolver. +# These entries can reference officially published versions as well as +# forks / in-progress versions pinned to a git hash. For example: +# +# extra-deps: +# - acme-missiles-0.3 +# - git: https://github.com/commercialhaskell/stack.git +# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a +# +# extra-deps: [] + +# Override default flag values for local packages and extra-deps +# flags: {} + +# Extra package databases containing global packages +# extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true +# +# Require a specific version of stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: ">=2.7" +# +# Override the architecture used by stack, especially useful on Windows +# arch: i386 +# arch: x86_64 +# +# Extra directories used by stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] +# +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor diff --git a/tiny/stack.yaml.lock b/tiny/stack.yaml.lock new file mode 100644 index 0000000..dc9b6b0 --- /dev/null +++ b/tiny/stack.yaml.lock @@ -0,0 +1,13 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/lock_files + +packages: [] +snapshots: +- completed: + size: 619405 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml + sha256: 7f4393ad659c579944d12202cffb12d8e4b8114566b015f77bbc303a24cff934 + original: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/28.yaml -- cgit v1.2.3