update agda2hs

.gitignore

@@ -27,3 +27,4 @@ build.ninja
 
 # Cabal-generated files
 /dist-newstyle/
+*.agdai

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
+          ];
+        };
+      };
+    };
+}

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

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

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

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 #-}