From 5cbf0d8318eea3f769a3436caa1944f4e4082a70 Mon Sep 17 00:00:00 2001 From: Sam Stites Date: Wed, 13 Aug 2025 18:32:14 -0500 Subject: [PATCH 1/2] add nix flake --- .gitignore | 1 + flake.lock | 117 +++++++++++++++++++++++++++++++++++++++++++++++++++++ flake.nix | 38 +++++++++++++++++ 3 files changed, 156 insertions(+) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.gitignore b/.gitignore index 857becf..4f1ea75 100644 --- a/.gitignore +++ b/.gitignore @@ -27,3 +27,4 @@ build.ninja # Cabal-generated files /dist-newstyle/ +*.agdai diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..1e8685d --- /dev/null +++ b/flake.lock @@ -0,0 +1,117 @@ +{ + "nodes": { + "agda2hs": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1755060529, + "narHash": "sha256-akEfg2d8u0tiPsBm3PxLWnykd5XY+Iq52B1CWA2LFhg=", + "owner": "stites", + "repo": "agda2hs", + "rev": "fd22217f17ede6bf8cdbf710d575411fc49b180b", + "type": "github" + }, + "original": { + "owner": "stites", + "ref": "acorn", + "repo": "agda2hs", + "type": "github" + } + }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1754487366, + "narHash": "sha256-pHYj8gUBapuUzKV/kN/tR3Zvqc7o6gdFB9XKXIp1SQ8=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "af66ad14b28a127c5c0f3bbb298218fc63528a18", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1711555030, + "narHash": "sha256-PuFoxVlnKIIqI83o5yVFjR9XWiCSMTsHhvGoCpUNpvU=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "cb11f8589769078fa154fb57ed8edd185281f1db", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1753579242, + "narHash": "sha256-zvaMGVn14/Zz8hnp4VWT9xVnhc8vuL3TStRqwk22biA=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "0f36c44e01a6129be94e3ade315a5883f0228a6e", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "root": { + "inputs": { + "agda2hs": "agda2hs", + "flake-parts": "flake-parts", + "nixpkgs": [ + "agda2hs", + "nixpkgs" + ] + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..b44597b --- /dev/null +++ b/flake.nix @@ -0,0 +1,38 @@ +{ + description = "Description for the project"; + + inputs = { + flake-parts.url = "github:hercules-ci/flake-parts"; + agda2hs.url = "github:stites/agda2hs/acorn"; + nixpkgs.follows = "agda2hs/nixpkgs"; + }; + + outputs = inputs@{ flake-parts, ... }: + flake-parts.lib.mkFlake { inherit inputs; } { + systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; + perSystem = { config, self', inputs', pkgs, system, ... }: rec { + packages = let + agda2hs-lib = inputs'.agda2hs.packages.agda2hs-lib; + agda-packages = [ + agda2hs-lib + pkgs.agdaPackages.cubical + pkgs.agdaPackages.standard-library + ]; + agda2hs = inputs.agda2hs.lib.${system}.withPackages agda-packages; + agda-with-packages = pkgs.agda.withPackages (ps: agda-packages); + in { + inherit agda2hs agda-with-packages; + }; + devShells.default = with packages; pkgs.haskellPackages.shellFor { + packages = p: []; + buildInputs = with pkgs.haskellPackages; [ + self'.packages.agda2hs + self'.packages.agda-with-packages + cabal-install + cabal2nix + haskell-language-server + ]; + }; + }; + }; +} From 68b45d26284c3da2b7a7e64ec6fdc0c5b5328977 Mon Sep 17 00:00:00 2001 From: Sam Stites Date: Wed, 13 Aug 2025 18:32:33 -0500 Subject: [PATCH 2/2] erase constraints in data constructors https://github.com/agda/agda2hs/issues/366#issuecomment-2385064760 --- src/Implementation/Frac.agda | 2 +- src/Operator/Pow.agda | 3 ++- src/RealTheory/Completion.agda | 2 +- src/RealTheory/Continuity.agda | 4 ++-- 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Implementation/Frac.agda b/src/Implementation/Frac.agda index 1ad7904..bdbfc89 100644 --- a/src/Implementation/Frac.agda +++ b/src/Implementation/Frac.agda @@ -45,7 +45,7 @@ open import Operator.Pow -- Since we don't use classes below SemiRing to maintain -- Haskell compatibility (by avoiding to give operators as parameters); -- the constraint here is SemiRing a. -record Frac (a : Set) {{semiRing : SemiRing a}} : Set where +record Frac (a : Set) {{@0 semiRing : SemiRing a}} : Set where constructor MkFrac field num den : a diff --git a/src/Operator/Pow.agda b/src/Operator/Pow.agda index 5f08c00..d8d4a9c 100644 --- a/src/Operator/Pow.agda +++ b/src/Operator/Pow.agda @@ -10,7 +10,8 @@ open import Algebra.Setoid open import Algebra.SemiRing -- Actually, the exponent need not be a Nat; it can also be from a "similar" structure. -record Pow (a : Set) {{semiringa : SemiRing a}} (b : Set) {{semiringb : SemiRing b}} +-- erase semi-ring constraints: https://github.com/agda/agda2hs/issues/366#issuecomment-2385064760 +record Pow (a : Set) {{@0 semiringa : SemiRing a}} (b : Set) {{@0 semiringb : SemiRing b}} : Set₁ where infixr 8 _^_ field diff --git a/src/RealTheory/Completion.agda b/src/RealTheory/Completion.agda index f5dc272..a3e21c8 100644 --- a/src/RealTheory/Completion.agda +++ b/src/RealTheory/Completion.agda @@ -49,7 +49,7 @@ open import RealTheory.Interval -- This will be a newtype in Haskell. -- Sometimes, the range of a function might not be a prelength space; -- hence we allow this. -record C (a : Set) {{metricSpace : MetricSpace a}} +record C (a : Set) {{@0 metricSpace : MetricSpace a}} : Set where constructor MkC field diff --git a/src/RealTheory/Continuity.agda b/src/RealTheory/Continuity.agda index b6ef365..bea233d 100644 --- a/src/RealTheory/Continuity.agda +++ b/src/RealTheory/Continuity.agda @@ -35,7 +35,7 @@ UcFunOn {a} subset b = Σ' (a -> b) (UniformlyContinuousOn subset) -} -record UniformlyContinuous {a b : Set} {{msa : MetricSpace a}} {{msb : MetricSpace b}} +record UniformlyContinuous {a b : Set} {{@0 msa : MetricSpace a}} {{@0 msb : MetricSpace b}} (@0 f : a -> b) : Set where constructor WrapMod field @@ -47,7 +47,7 @@ open UniformlyContinuous public -- What if we used instances for that? -UcFun : (a b : Set) {{msa : MetricSpace a}} {{msb : MetricSpace b}} +UcFun : (a b : Set) {{@0 msa : MetricSpace a}} {{@0 msb : MetricSpace b}} -> Set UcFun a b = Σ' (a -> b) UniformlyContinuous {-# COMPILE AGDA2HS UcFun #-}