From 03bf4df6b71a7a22f200edf1fdff1d73be2fd660 Mon Sep 17 00:00:00 2001 From: sjeulu Date: Wed, 26 Mar 2025 15:42:09 +0000 Subject: [PATCH 1/3] added a flake (works) --- flake.lock | 161 +++++++++++++++++++++++++++++++++++++++++++++++++++++ flake.nix | 42 ++++++++++++++ 2 files changed, 203 insertions(+) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..d1db8d4 --- /dev/null +++ b/flake.lock @@ -0,0 +1,161 @@ +{ + "nodes": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1741352980, + "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9", + "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" + } + }, + "idris-emacs-src": { + "flake": false, + "locked": { + "lastModified": 1666078909, + "narHash": "sha256-oYNHFIpcrFfPb4sXJwEBFKeH+PB4AGCrAFrfBrSTCeo=", + "owner": "redfish64", + "repo": "idris2-mode", + "rev": "3bcb52a65c488f31c99d20f235f6050418a84c9d", + "type": "github" + }, + "original": { + "owner": "redfish64", + "repo": "idris2-mode", + "type": "github" + } + }, + "idris2_0_5_0": { + "inputs": { + "flake-utils": "flake-utils", + "idris-emacs-src": "idris-emacs-src", + "nixpkgs": "nixpkgs", + "nixpkgs-chez-racket": "nixpkgs-chez-racket" + }, + "locked": { + "lastModified": 1631977654, + "narHash": "sha256-JRI5/dEy9GT8SIj3X+UcJ0SiTQ20pqevWeTNX6e+Nfw=", + "owner": "idris-lang", + "repo": "Idris2", + "rev": "ada3eb44498b53bf3e4673709ac7fab893da1d75", + "type": "github" + }, + "original": { + "owner": "idris-lang", + "ref": "v0.5.0", + "repo": "Idris2", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 0, + "narHash": "sha256-jekur29uz2dd56SNXgQEKjaXc6wGSPMBToFIaifn1G0=", + "path": "/nix/store/346nh2kxbzn1v56h7141kcy5nk8s885f-source", + "type": "path" + }, + "original": { + "id": "nixpkgs", + "type": "indirect" + } + }, + "nixpkgs-chez-racket": { + "locked": { + "lastModified": 1640294068, + "narHash": "sha256-ef5oMS7lTriZ6Yj4pnOXSOuiiz6JOcjmmHDNi2gPCBY=", + "owner": "L-as", + "repo": "nixpkgs", + "rev": "177e4ff31fc51726eebb09b8a2b0b15c791c26a4", + "type": "github" + }, + "original": { + "owner": "L-as", + "ref": "chez-racket", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1740877520, + "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1742889210, + "narHash": "sha256-hw63HnwnqU3ZQfsMclLhMvOezpM7RSB0dMAtD5/sOiw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "698214a32beb4f4c8e3942372c694f40848b360d", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-parts": "flake-parts", + "idris2_0_5_0": "idris2_0_5_0", + "nixpkgs": "nixpkgs_2" + } + }, + "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..8d2a044 --- /dev/null +++ b/flake.nix @@ -0,0 +1,42 @@ +{ + description = "Lua backend for Idris 2"; + + inputs = { + flake-parts.url = "github:hercules-ci/flake-parts"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + + idris2_0_5_0 = { + url = "github:idris-lang/Idris2?ref=v0.5.0"; + }; + }; + + 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, ... }: with pkgs; + let + idris2' = inputs.idris2_0_5_0.packages.${system}.idris2; + buildIdris' = idris2Packages.buildIdris.override { + idris2 = idris2'; + }; + idris2-api' = callPackage ( + { lib, idris2Packages }: (buildIdris' { + inherit (idris2') src version; + ipkgName = "idris2api"; + idrisLibraries = [ ]; + preBuild = '' + export IDRIS2_PREFIX=$out/lib + make src/IdrisPaths.idr + ''; + }).library {} + ) {}; + idris2-lua = buildIdris' { + src = ./.; + idrisLibraries = [ idris2-api' ]; + ipkgName = "idris2-lua"; + }; + in { + packages.default = idris2-lua.executable; + }; + }; +} From b186069a9cfe6088a2212db128aeabfdc0ca41f4 Mon Sep 17 00:00:00 2001 From: sjeulu Date: Thu, 27 Mar 2025 02:46:57 +0000 Subject: [PATCH 2/3] updated to Idris2 0.7.0 --- flake.lock | 114 +++------------------------------------------- flake.nix | 34 +++++--------- src/LuaCommon.idr | 2 +- src/LuaGen.idr | 34 ++++++++------ 4 files changed, 39 insertions(+), 145 deletions(-) diff --git a/flake.lock b/flake.lock index d1db8d4..af26562 100644 --- a/flake.lock +++ b/flake.lock @@ -18,86 +18,18 @@ "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" - } - }, - "idris-emacs-src": { - "flake": false, - "locked": { - "lastModified": 1666078909, - "narHash": "sha256-oYNHFIpcrFfPb4sXJwEBFKeH+PB4AGCrAFrfBrSTCeo=", - "owner": "redfish64", - "repo": "idris2-mode", - "rev": "3bcb52a65c488f31c99d20f235f6050418a84c9d", - "type": "github" - }, - "original": { - "owner": "redfish64", - "repo": "idris2-mode", - "type": "github" - } - }, - "idris2_0_5_0": { - "inputs": { - "flake-utils": "flake-utils", - "idris-emacs-src": "idris-emacs-src", - "nixpkgs": "nixpkgs", - "nixpkgs-chez-racket": "nixpkgs-chez-racket" - }, - "locked": { - "lastModified": 1631977654, - "narHash": "sha256-JRI5/dEy9GT8SIj3X+UcJ0SiTQ20pqevWeTNX6e+Nfw=", - "owner": "idris-lang", - "repo": "Idris2", - "rev": "ada3eb44498b53bf3e4673709ac7fab893da1d75", - "type": "github" - }, - "original": { - "owner": "idris-lang", - "ref": "v0.5.0", - "repo": "Idris2", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 0, - "narHash": "sha256-jekur29uz2dd56SNXgQEKjaXc6wGSPMBToFIaifn1G0=", - "path": "/nix/store/346nh2kxbzn1v56h7141kcy5nk8s885f-source", - "type": "path" - }, - "original": { - "id": "nixpkgs", - "type": "indirect" - } - }, - "nixpkgs-chez-racket": { - "locked": { - "lastModified": 1640294068, - "narHash": "sha256-ef5oMS7lTriZ6Yj4pnOXSOuiiz6JOcjmmHDNi2gPCBY=", - "owner": "L-as", + "lastModified": 1742889210, + "narHash": "sha256-hw63HnwnqU3ZQfsMclLhMvOezpM7RSB0dMAtD5/sOiw=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "177e4ff31fc51726eebb09b8a2b0b15c791c26a4", + "rev": "698214a32beb4f4c8e3942372c694f40848b360d", "type": "github" }, "original": { - "owner": "L-as", - "ref": "chez-racket", + "owner": "NixOS", + "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } @@ -117,42 +49,10 @@ "type": "github" } }, - "nixpkgs_2": { - "locked": { - "lastModified": 1742889210, - "narHash": "sha256-hw63HnwnqU3ZQfsMclLhMvOezpM7RSB0dMAtD5/sOiw=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "698214a32beb4f4c8e3942372c694f40848b360d", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "flake-parts": "flake-parts", - "idris2_0_5_0": "idris2_0_5_0", - "nixpkgs": "nixpkgs_2" - } - }, - "systems": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" + "nixpkgs": "nixpkgs" } } }, diff --git a/flake.nix b/flake.nix index 8d2a044..3c3923d 100644 --- a/flake.nix +++ b/flake.nix @@ -4,10 +4,6 @@ inputs = { flake-parts.url = "github:hercules-ci/flake-parts"; nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; - - idris2_0_5_0 = { - url = "github:idris-lang/Idris2?ref=v0.5.0"; - }; }; outputs = inputs@{ flake-parts, ... }: @@ -15,28 +11,20 @@ systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; perSystem = { config, self', inputs', pkgs, system, ... }: with pkgs; let - idris2' = inputs.idris2_0_5_0.packages.${system}.idris2; - buildIdris' = idris2Packages.buildIdris.override { - idris2 = idris2'; - }; - idris2-api' = callPackage ( - { lib, idris2Packages }: (buildIdris' { - inherit (idris2') src version; - ipkgName = "idris2api"; - idrisLibraries = [ ]; - preBuild = '' - export IDRIS2_PREFIX=$out/lib - make src/IdrisPaths.idr - ''; - }).library {} - ) {}; - idris2-lua = buildIdris' { + idris2-lua = with idris2Packages; (buildIdris { src = ./.; - idrisLibraries = [ idris2-api' ]; + idrisLibraries = [ idris2Api ]; ipkgName = "idris2-lua"; - }; + postInstall = '' + wrapProgram "$out/bin/idris2-lua" \ + --suffix IDRIS2_PACKAGE_PATH ':' ${idris2}/${idris2.name} + ''; + }).executable; in { - packages.default = idris2-lua.executable; + packages = { + inherit idris2-lua; + default = idris2-lua; + }; }; }; } diff --git a/src/LuaCommon.idr b/src/LuaCommon.idr index e455ecf..db96337 100644 --- a/src/LuaCommon.idr +++ b/src/LuaCommon.idr @@ -14,7 +14,7 @@ import Data.String import Data.Vect import Data.Zippable -import Libraries.Utils.Hex +import Protocol.Hex infixl 100 |> diff --git a/src/LuaGen.idr b/src/LuaGen.idr index 0d9c214..4dbd1c9 100644 --- a/src/LuaGen.idr +++ b/src/LuaGen.idr @@ -6,7 +6,9 @@ import Compiler.CompileExpr import Core.Context import Core.Directory -import Libraries.Utils.Hex +import Idris.Syntax + +import Protocol.Hex import Libraries.Utils.Path import Idris.Driver @@ -31,6 +33,9 @@ import LuaCommon import OrderDefs import LuaAst +%hide Libraries.Data.PosMap.infixl.(|>) +%hide Core.Normalise.Eval.Stack + data Stack : Type where data Preamble : Type where @@ -87,7 +92,7 @@ logLine str with (opts |> debugOutput |> get) logLine str | False = pure () export -toMillis : Clock type -> Integer +toMillis : Clock t -> Integer toMillis (MkClock sec nan) = let scale = 1000 in scale * sec + (nan `div` 1000000) @@ -364,7 +369,7 @@ mutual stringify n (LPrimFn (Add ty) [x, y]) = stringifyBinOp n "+" x y stringify n (LPrimFn (Sub ty) [x, y]) = stringifyBinOp n "-" x y stringify n (LPrimFn (Mul ty) [x, y]) = stringifyBinOp n "*" x y - stringify n (LPrimFn (Div IntType) [x, y]) with (copts |> luaVersion |> get >= Lua53) + stringify n (LPrimFn (Div IntType) [x, y]) with ((copts |> luaVersion |> get) >= Lua53) stringify n (LPrimFn (Div IntType) [x, y]) | True = stringifyBinOp n "//" x y stringify n (LPrimFn (Div IntType) [x, y]) | False @@ -511,8 +516,8 @@ pushFrame = s <- get Stack let frame = nextFrame s let index = nextIndex s - put Stack (record{ nextFrame $= (+1) - , nextIndex = indexLowest + put Stack ({ nextFrame $= (+1) + , nextIndex := indexLowest , stack $= (index ::) } s) pure (MkStackFrame frame) @@ -524,7 +529,7 @@ pushLocal = do s <- get Stack let i = nextIndex s - put Stack (record{nextIndex $= (+1)} s) + put Stack ({nextIndex $= (+1)} s) pure (LIndex (LLVar (frameName frame)) (LNumber (show i))) ||| Returns the number of local variables in the popped frame @@ -536,7 +541,7 @@ popFrame = let v = nextIndex s case (i <= frameLowest, stack s) of (False, (nextIndex :: other)) => do - put Stack (record{nextFrame $= (\i => i - 1), nextIndex = nextIndex, stack = other} s) + put Stack ({nextFrame $= (\i => i - 1), nextIndex := nextIndex, stack := other} s) pure (v - 1) (_, _) => throw (UserError "Attempt to pop from an empty stack") @@ -549,7 +554,7 @@ popName = if i <= indexLowest then throw (UserError "attempt to pop from an empty stack frame") else - put Stack (record{nextIndex $= (\i => i - 1)} s) + put Stack ({nextIndex $= (\i => i - 1)} s) getPreamble : @@ -582,7 +587,7 @@ addDefToPreamble name def okIfDefined = do pure () -constantTy : Constant -> Maybe Constant +constantTy : Constant -> Maybe PrimType constantTy (I _) = Just IntType constantTy (BI _) = Just IntegerType constantTy (B8 _) = Just Bits8Type @@ -1310,7 +1315,7 @@ translate defs term = do clock0 <- coreLift $ clockTime Monotonic logLine "Lua compilation started [0/5]" - logLine ("Using " ++ opts |> luaVersion |> get |> show) + logLine ("Using " ++ (opts |> luaVersion |> get |> show)) cdata <- getCompileData False Cases term clock1 <- coreLift $ clockTime Monotonic @@ -1413,7 +1418,7 @@ build defs outputDir term file = do strbuf <- translate defs term let luaFile = file ++ ".lua" Right () <- coreLift $ writeBufferToFile (outputDir luaFile) strbuf.get strbuf.offset - | Left err => throw $ FileErr (outputDir luaFile) err + | Left (err, _) => throw $ FileErr (outputDir luaFile) err luaExe <- coreLift getLuaExe @@ -1426,15 +1431,16 @@ build defs outputDir term file = do pure (outputDir file) compile : Ref Ctxt Defs + -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core (Maybe String) -compile defs tmpDir outputDir term file = Just <$> build defs outputDir term file +compile defs _ tmpDir outputDir term file = Just <$> build defs outputDir term file -execute : Ref Ctxt Defs -> String -> ClosedTerm -> Core () -execute defs tmpDir term = do +execute : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> ClosedTerm -> Core () +execute defs _ tmpDir term = do exe <- build defs tmpDir term "generated" coreLift_ $ fflush stdout coreLift_ $ system $ "'" ++ exe ++ "' " From 7019f072d46341c2b1003155ec4200292299f269 Mon Sep 17 00:00:00 2001 From: sjeulu Date: Thu, 27 Mar 2025 04:02:34 +0000 Subject: [PATCH 3/3] specified the library version --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index 3c3923d..bfa589d 100644 --- a/flake.nix +++ b/flake.nix @@ -15,6 +15,7 @@ src = ./.; idrisLibraries = [ idris2Api ]; ipkgName = "idris2-lua"; + version = idris2Api.version; postInstall = '' wrapProgram "$out/bin/idris2-lua" \ --suffix IDRIS2_PACKAGE_PATH ':' ${idris2}/${idris2.name}