From 5535bb19125bfeaa53e71689f15e06bf374e7863 Mon Sep 17 00:00:00 2001 From: cmcmA20 Date: Tue, 7 Apr 2026 06:31:12 +0000 Subject: [PATCH] flake support --- .gitignore | 1 + flake.lock | 612 +++++++++++++++++++++++++++++++++++++++++++ flake.nix | 59 +++++ src/Forester/Data.hs | 4 +- 4 files changed, 674 insertions(+), 2 deletions(-) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.gitignore b/.gitignore index 8c0743a..39a4954 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ trees **/*.agdai .DS_Store .vscode +result diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..84904a7 --- /dev/null +++ b/flake.lock @@ -0,0 +1,612 @@ +{ + "nodes": { + "agda": { + "inputs": { + "flake-parts": [ + "flake-parts" + ], + "ghc-wasm": "ghc-wasm", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1775233973, + "narHash": "sha256-jr4eDgQtXHcap/ZzPjYeEMu3RcStBRTvixLOes4yh+c=", + "owner": "agda", + "repo": "agda", + "rev": "295c60c79cd49e880b9f07add98462f1b82d26f2", + "type": "github" + }, + "original": { + "owner": "agda", + "repo": "agda", + "type": "github" + } + }, + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-compat_2": { + "flake": false, + "locked": { + "lastModified": 1747046372, + "narHash": "sha256-CIVLLkVgvHYbgI2UpXvIIBJ12HWgX+fjA8Xf8PUmqCY=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "9100a0f413b0c601e0533d1d94ffd501ce2e7885", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1775087534, + "narHash": "sha256-91qqW8lhL7TLwgQWijoGBbiD4t7/q75KTi8NxjVmSmA=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "3107b77cd68437b9a76194f0f7f9c55f2329ca5b", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_3": { + "inputs": { + "systems": "systems_3" + }, + "locked": { + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_4": { + "inputs": { + "systems": "systems_4" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_5": { + "inputs": { + "systems": "systems_5" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "forester": { + "inputs": { + "flake-utils": "flake-utils_2", + "nixpkgs": "nixpkgs_2", + "opam-nix": "opam-nix", + "opam-repository": "opam-repository" + }, + "locked": { + "lastModified": 1770539626, + "narHash": "sha256-RMkVHOPsaDRy6+wddnHsoS9sLTMJzVK97o+9EzHuuTc=", + "owner": "~jonsterling", + "repo": "ocaml-forester", + "rev": "d6f33c845e7e3b2815bd4ed1d55d1f50f4ac5fae", + "type": "sourcehut" + }, + "original": { + "owner": "~jonsterling", + "repo": "ocaml-forester", + "type": "sourcehut" + } + }, + "ghc-wasm": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1764532453, + "narHash": "sha256-83PtOfCHZhby/isbpHiEG61BkoPK42zCi0lr3JTRStw=", + "ref": "refs/heads/master", + "rev": "01679cb5e8c6ed1c80218ce09f2d10766c1a5b1d", + "revCount": 450, + "type": "git", + "url": "https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta.git" + }, + "original": { + "type": "git", + "url": "https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta.git" + } + }, + "mirage-opam-overlays": { + "flake": false, + "locked": { + "lastModified": 1710922379, + "narHash": "sha256-j4QREQDUf8oHOX7qg6wAOupgsNQoYlufxoPrgagD+pY=", + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "rev": "797cb363df3ff763c43c8fbec5cd44de2878757e", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "type": "github" + } + }, + "mirage-opam-overlays_2": { + "flake": false, + "locked": { + "lastModified": 1710922379, + "narHash": "sha256-j4QREQDUf8oHOX7qg6wAOupgsNQoYlufxoPrgagD+pY=", + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "rev": "797cb363df3ff763c43c8fbec5cd44de2878757e", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1759326671, + "narHash": "sha256-h9jyjb62WDgKs0MBUDFhSlV3F4n+64ygJeo3ijhEF80=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "840e8405978644a20844b54e70a09b518f5c7709", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-25.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1774748309, + "narHash": "sha256-+U7gF3qxzwD5TZuANzZPeJTZRHS29OFQgkQ2kiTJBIQ=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "333c4e0545a6da976206c74db8773a1645b5870a", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "nixpkgs-tl": { + "locked": { + "lastModified": 1762111121, + "narHash": "sha256-4vhDuZ7OZaZmKKrnDpxLZZpGIJvAeMtK6FKLJYUtAdw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "b3d51a0365f6695e7dd5cdf3e180604530ed33b4", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "b3d51a0365f6695e7dd5cdf3e180604530ed33b4", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1743095683, + "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { + "locked": { + "lastModified": 1775544523, + "narHash": "sha256-QnyjiTIogebNzsdBSuLhCKT/t3CaSxJIFs3/WvMoX04=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "ec884511015176e25f1900f8110e171851357935", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "type": "github" + } + }, + "opam-nix": { + "inputs": { + "flake-compat": "flake-compat", + "flake-utils": "flake-utils_3", + "mirage-opam-overlays": "mirage-opam-overlays", + "nixpkgs": [ + "forester", + "nixpkgs" + ], + "opam-overlays": "opam-overlays", + "opam-repository": [ + "forester", + "opam-repository" + ], + "opam2json": "opam2json" + }, + "locked": { + "lastModified": 1741156005, + "narHash": "sha256-JBPvXe5g1V2xpmPVMlf5CP5+T1E+TCK73lqeqV89EJE=", + "owner": "tweag", + "repo": "opam-nix", + "rev": "e71936b31658f0b039a7d26b0c9c7a461d949ba4", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam-nix", + "type": "github" + } + }, + "opam-nix_2": { + "inputs": { + "flake-compat": "flake-compat_2", + "flake-utils": "flake-utils_5", + "mirage-opam-overlays": "mirage-opam-overlays_2", + "nixpkgs": [ + "treelist", + "nixpkgs" + ], + "opam-overlays": "opam-overlays_2", + "opam-repository": [ + "treelist", + "opam-repository" + ], + "opam2json": "opam2json_2" + }, + "locked": { + "lastModified": 1771067167, + "narHash": "sha256-XSw8dQIkdr+6eLvbUHo3cJPtTU7o5SMODz3qlnzmGpQ=", + "owner": "tweag", + "repo": "opam-nix", + "rev": "2e20bbbe8130d1880338291446fd4e710a4db9a1", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam-nix", + "type": "github" + } + }, + "opam-overlays": { + "flake": false, + "locked": { + "lastModified": 1726822209, + "narHash": "sha256-bwM18ydNT9fYq91xfn4gmS21q322NYrKwfq0ldG9GYw=", + "owner": "dune-universe", + "repo": "opam-overlays", + "rev": "f2bec38beca4aea9e481f2fd3ee319c519124649", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "opam-overlays", + "type": "github" + } + }, + "opam-overlays_2": { + "flake": false, + "locked": { + "lastModified": 1741116009, + "narHash": "sha256-Z0PIW82fHJFvAv/JYpAffnp2DaOjLhsPutqyIrORZd0=", + "owner": "dune-universe", + "repo": "opam-overlays", + "rev": "e031bb64e33bf93be963e9a38b28962e6e14381f", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "opam-overlays", + "type": "github" + } + }, + "opam-repository": { + "flake": false, + "locked": { + "lastModified": 1743193860, + "narHash": "sha256-nuss395vu6kN4IKRLviyPztBgeD/tBYIp3x66GQpLK0=", + "owner": "ocaml", + "repo": "opam-repository", + "rev": "a8a89f62d8abd2a9f0cbb04826bfec1ef6b563e7", + "type": "github" + }, + "original": { + "owner": "ocaml", + "repo": "opam-repository", + "type": "github" + } + }, + "opam-repository_2": { + "flake": false, + "locked": { + "lastModified": 1775486623, + "narHash": "sha256-BJxHlmBKWqADRhXxpPz1PG86KGAMMfhFTC7yIvNC174=", + "owner": "ocaml", + "repo": "opam-repository", + "rev": "67472cd54293d750a62d6d4423024d55f77268b0", + "type": "github" + }, + "original": { + "owner": "ocaml", + "repo": "opam-repository", + "type": "github" + } + }, + "opam2json": { + "inputs": { + "nixpkgs": [ + "forester", + "opam-nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1671540003, + "narHash": "sha256-5pXfbUfpVABtKbii6aaI2EdAZTjHJ2QntEf0QD2O5AM=", + "owner": "tweag", + "repo": "opam2json", + "rev": "819d291ea95e271b0e6027679de6abb4d4f7f680", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam2json", + "type": "github" + } + }, + "opam2json_2": { + "inputs": { + "nixpkgs": [ + "treelist", + "opam-nix", + "nixpkgs" + ], + "systems": "systems_6" + }, + "locked": { + "lastModified": 1749457947, + "narHash": "sha256-+QVm+HOYikF3wUhqSIV8qJbE/feSG+p48fgxIosbHS0=", + "owner": "tweag", + "repo": "opam2json", + "rev": "0ecd66fc2bfb25d910522c990dd36412259eac1f", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam2json", + "type": "github" + } + }, + "root": { + "inputs": { + "agda": "agda", + "flake-parts": "flake-parts", + "forester": "forester", + "nixpkgs": "nixpkgs_3", + "nixpkgs-tl": "nixpkgs-tl", + "treelist": "treelist" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_3": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_4": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_5": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_6": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "treelist": { + "inputs": { + "flake-utils": "flake-utils_4", + "nixpkgs": [ + "nixpkgs-tl" + ], + "opam-nix": "opam-nix_2", + "opam-repository": "opam-repository_2" + }, + "locked": { + "lastModified": 1770819889, + "narHash": "sha256-fqcgm+1K4dg8AOMgJ9CaeUpoVaU5tU+0bYhdjbKTPtk=", + "owner": "samtoth", + "repo": "treelist", + "rev": "5b5a7e36a1cbbb89c83f15cc770c5a5609a1a2c1", + "type": "github" + }, + "original": { + "owner": "samtoth", + "repo": "treelist", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..6d5baae --- /dev/null +++ b/flake.nix @@ -0,0 +1,59 @@ +{ + description = "Agda backend for Forester"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs"; + flake-parts.url = "github:hercules-ci/flake-parts"; + agda = { + url = "github:agda/agda"; + inputs.nixpkgs.follows = "nixpkgs"; + inputs.flake-parts.follows = "flake-parts"; + }; + + nixpkgs-tl.url = "github:NixOS/nixpkgs?rev=b3d51a0365f6695e7dd5cdf3e180604530ed33b4"; + treelist = { + url = "github:samtoth/treelist"; + inputs.nixpkgs.follows = "nixpkgs-tl"; + }; + + forester.url = "sourcehut:~jonsterling/ocaml-forester"; + }; + + outputs = inputs@{ agda , flake-parts , forester , treelist , ... }: + flake-parts.lib.mkFlake { inherit inputs; } { + perSystem = {pkgs , system , lib , ...}: let + agda-forester = pkgs.haskell.packages.ghc910.developPackage { + root = lib.fileset.toSource { + root = ./. ; + fileset = lib.fileset.unions [ + ./src + ./app + ./agda-forester.cabal + ./LICENSE + ]; + }; + modifier = pkgs.haskell.lib.compose.overrideCabal (drv: { + enableLibraryProfiling = false; + enableExecutableProfiling = false; + doHaddock = false; + }); + }; + + in { + _module.args.pkgs = import inputs.nixpkgs { + inherit system; + overlays = [ inputs.agda.overlays.default ]; + }; + + packages.default = agda-forester; + devShells.default = pkgs.mkShell { + packages = [ + forester.packages.${system}.default + treelist.packages.${system}.default + ]; + }; + }; + + systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; + }; +} diff --git a/src/Forester/Data.hs b/src/Forester/Data.hs index d5eb3db..f302109 100644 --- a/src/Forester/Data.hs +++ b/src/Forester/Data.hs @@ -1,7 +1,7 @@ {-# LANGUAGE OverloadedStrings, FlexibleInstances #-} module Forester.Data where -import Agda.Compiler.Backend hiding (topLevelModuleName, Name, Constructor) +import Agda.Compiler.Backend hiding (topLevelModuleName, Name, Constructor, (.=)) import Agda.Syntax.Common.Pretty import Agda.Syntax.Position import Agda.Syntax.Internal @@ -53,4 +53,4 @@ getSubtree [] _ = Nothing getSubtree ((IntTree tid (_,sp) (_,ep) cp):xs) os = if os >= sp && os <= ep then maybe (Just tid) Just $ getSubtree cp os - else getSubtree xs os \ No newline at end of file + else getSubtree xs os