rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

wip nix

Browse source
This commit is contained in:
rhiannon morris 2022-05-04 17:09:49 +02:00
parent 4973ce15bd
commit 7f415328a2
14 changed files with 667 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -1,7 +1,6 @@
.build
build
depends
*.ipkg
*~
quox
quox-tests

1
default.nix Normal file
View file

@ -0,0 +1 @@
(import (fetchTarball "https://github.com/edolstra/flake-compat/archive/master.tar.gz") { src = ./.; }).defaultNix

8
exe/quox-exe.ipkg Normal file
View file

@ -0,0 +1,8 @@
package quox-exe
version = 0
depends = base, contrib, elab-util, sop, quox
executable = quox
sourcedir = "src"
main = Main

14
exe/sirdi.json
View file

@ -1,14 +0,0 @@
[
{
"name" : "quox-exe",
"deps" : [
{ "name" : "base", "legacy" : true },
{ "name" : "contrib", "legacy" : true },
{ "name" : "quox", "local" : ".." }
],
"main" : "Main",
"modules" : ["Main"]
}
]

1
exe/src/Main.idr
View file

@ -9,6 +9,7 @@ import public Quox.Typechecker
import Data.Nat
import Data.Vect
import Data.List
import Control.ANSI

575
flake.lock Normal file
View file

@ -0,0 +1,575 @@
{
"nodes": {
"Prettier": {
"flake": false,
"locked": {
"lastModified": 1639310097,
"narHash": "sha256-+eSLEJDuy2ZRkh1h0Y5IF6RUeHEcWhAHpWhwdwW65f0=",
"owner": "Z-snails",
"repo": "prettier",
"rev": "4a90663b1d586f6d6fce25873aa0f0d7bc633b89",
"type": "github"
},
"original": {
"owner": "Z-snails",
"repo": "prettier",
"type": "github"
}
},
"collie": {
"flake": false,
"locked": {
"lastModified": 1631011321,
"narHash": "sha256-goYctB+WBoLgsbjA0DlqGjD8i9wr1K0lv0agqpuwflU=",
"owner": "ohad",
"repo": "collie",
"rev": "ed2eda5e04fbd02a7728e915d396e14cc7ec298e",
"type": "github"
},
"original": {
"owner": "ohad",
"repo": "collie",
"type": "github"
}
},
"comonad": {
"flake": false,
"locked": {
"lastModified": 1638093386,
"narHash": "sha256-kxmN6XuszFLK2i76C6LSGHe5XxAURFu9NpzJbi3nodk=",
"owner": "stefan-hoeck",
"repo": "idris2-comonad",
"rev": "06d6b551db20f1f940eb24c1dae051c957de97ad",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-comonad",
"type": "github"
}
},
"dom": {
"flake": false,
"locked": {
"lastModified": 1639041519,
"narHash": "sha256-4ZYc0qaUEVARxhWuH3JgejIeT+GEDNxdS6zIGhBCk34=",
"owner": "stefan-hoeck",
"repo": "idris2-dom",
"rev": "01ab52d0ffdb3b47481413a949b8f0c0688c97e4",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-dom",
"type": "github"
}
},
"dot-parse": {
"flake": false,
"locked": {
"lastModified": 1638264571,
"narHash": "sha256-VJQITz+vuQgl5HwR5QdUGwN8SRtGcb2/lJaAVfFbiSk=",
"owner": "CodingCellist",
"repo": "idris2-dot-parse",
"rev": "48fbda8bf8adbaf9e8ebd6ea740228e4394154d9",
"type": "github"
},
"original": {
"owner": "CodingCellist",
"repo": "idris2-dot-parse",
"type": "github"
}
},
"effect": {
"flake": false,
"locked": {
"lastModified": 1637477153,
"narHash": "sha256-Ta2Vogg/IiSBkfhhD57jjPTEf3S4DOiVRmof38hmwlM=",
"owner": "russoul",
"repo": "idris2-effect",
"rev": "ea1daf53b2d7e52f9917409f5653adc557f0ee1a",
"type": "github"
},
"original": {
"owner": "russoul",
"repo": "idris2-effect",
"type": "github"
}
},
"elab-util": {
"flake": false,
"locked": {
"lastModified": 1639041013,
"narHash": "sha256-K61s/xifFiTDXJTak5NZmZL6757CTYCY+TGywRZMD7M=",
"owner": "stefan-hoeck",
"repo": "idris2-elab-util",
"rev": "7a381c7c5dc3adb7b97c8b8be17e4fb4cc63027d",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-elab-util",
"type": "github"
}
},
"flake-utils": {
"locked": {
"lastModified": 1649676176,
"narHash": "sha256-OWKJratjt2RW151VUlJPRALb7OU2S5s+f0vLj4o1bHM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "a4b154ebbdc88c8498a5c7b01589addc9e9cb678",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"flake-utils_2": {
"locked": {
"lastModified": 1638122382,
"narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "74f7e4319258e287b0f9cb95426c9853b282730b",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"frex": {
"flake": false,
"locked": {
"lastModified": 1637410704,
"narHash": "sha256-BthU1t++n0ZvS76p0fCHsE33QSoXYxf0hMUSKajDY8w=",
"owner": "frex-project",
"repo": "idris-frex",
"rev": "22c480e879c757a5cebca7bb555ec3d21ae3ac28",
"type": "github"
},
"original": {
"owner": "frex-project",
"repo": "idris-frex",
"type": "github"
}
},
"fvect": {
"flake": false,
"locked": {
"lastModified": 1633247988,
"narHash": "sha256-zElIze03XpcrYL4H5Aj0ZGNplJGbtOx+iWnivJMzHm0=",
"owner": "mattpolzin",
"repo": "idris-fvect",
"rev": "1c5e3761e0cd83e711a3535ef9051bea45e6db3f",
"type": "github"
},
"original": {
"owner": "mattpolzin",
"repo": "idris-fvect",
"type": "github"
}
},
"hashable": {
"flake": false,
"locked": {
"lastModified": 1633965157,
"narHash": "sha256-Dggf5K//RCZ7uvtCyeiLNJS6mm+8/n0RFW3zAc7XqPg=",
"owner": "z-snails",
"repo": "idris2-hashable",
"rev": "d6fec8c878057909b67f3d4da334155de4f37907",
"type": "github"
},
"original": {
"owner": "z-snails",
"repo": "idris2-hashable",
"type": "github"
}
},
"hedgehog": {
"flake": false,
"locked": {
"lastModified": 1639041435,
"narHash": "sha256-893cPy7gGSQpVmm9co3QCpWsgjukafZHy8YFk9xts30=",
"owner": "stefan-hoeck",
"repo": "idris2-hedgehog",
"rev": "a66b1eb0bf84c4a7b743cfb217be69866bc49ad8",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-hedgehog",
"type": "github"
}
},
"idrall": {
"flake": false,
"locked": {
"lastModified": 1636495701,
"narHash": "sha256-aOdCRd4XsSxwqVGta1adlZBy8TVTxTwFDnJ1dyMZK8M=",
"owner": "alexhumphreys",
"repo": "idrall",
"rev": "13ef174290169d05c9e9abcd77c53412e3e0c944",
"type": "github"
},
"original": {
"owner": "alexhumphreys",
"ref": "13ef174",
"repo": "idrall",
"type": "github"
}
},
"idris-server": {
"flake": false,
"locked": {
"lastModified": 1634507315,
"narHash": "sha256-ulo23yLJXsvImoMB/1C6yRRTqmn/Odo+aUaVi+tUhJo=",
"owner": "avidela",
"repo": "idris-server",
"rev": "661a4ecf0fadaa2bd79c8e922c2d4f79b0b7a445",
"type": "gitlab"
},
"original": {
"owner": "avidela",
"repo": "idris-server",
"type": "gitlab"
}
},
"idris2": {
"flake": false,
"locked": {
"lastModified": 1639427352,
"narHash": "sha256-C1K2FM1Kio8vi9FTrivdacYCX4cywIsLBeNCsZ6ft4g=",
"owner": "idris-lang",
"repo": "idris2",
"rev": "36918e618646177b1e0c2fd01f21cc8d04d9da30",
"type": "github"
},
"original": {
"owner": "idris-lang",
"repo": "idris2",
"type": "github"
}
},
"idris2-pkgs": {
"inputs": {
"Prettier": "Prettier",
"collie": "collie",
"comonad": "comonad",
"dom": "dom",
"dot-parse": "dot-parse",
"effect": "effect",
"elab-util": "elab-util",
"flake-utils": "flake-utils_2",
"frex": "frex",
"fvect": "fvect",
"hashable": "hashable",
"hedgehog": "hedgehog",
"idrall": "idrall",
"idris-server": "idris-server",
"idris2": "idris2",
"indexed": "indexed",
"inigo": "inigo",
"ipkg-to-json": "ipkg-to-json",
"json": "json",
"katla": "katla",
"lsp": "lsp",
"nixpkgs": "nixpkgs",
"odf": "odf",
"pretty-show": "pretty-show",
"python": "python",
"rhone": "rhone",
"rhone-js": "rhone-js",
"snocvect": "snocvect",
"sop": "sop",
"tailrec": "tailrec",
"xml": "xml"
},
"locked": {
"lastModified": 1642030375,
"narHash": "sha256-J1uXnpPR72mjFjLBuYcvDHStBxVya6/MjBNNwqxGeD0=",
"owner": "claymager",
"repo": "idris2-pkgs",
"rev": "ac33a49d4d4bd2b50fddb040cd889733a02c8f09",
"type": "github"
},
"original": {
"owner": "claymager",
"repo": "idris2-pkgs",
"type": "github"
}
},
"indexed": {
"flake": false,
"locked": {
"lastModified": 1638685238,
"narHash": "sha256-FceB7o88yKYzjTfRC6yfhOL6oDPMmCQAsJZu/pjE2uA=",
"owner": "mattpolzin",
"repo": "idris-indexed",
"rev": "ff3ba99b0063da6a74c96178e7f3c58a4ac1693e",
"type": "github"
},
"original": {
"owner": "mattpolzin",
"repo": "idris-indexed",
"type": "github"
}
},
"inigo": {
"flake": false,
"locked": {
"lastModified": 1637596767,
"narHash": "sha256-LNx30LO0YWDVSPTxRLWGTFL4f3d5ANG6c60WPdmiYdY=",
"owner": "idris-community",
"repo": "Inigo",
"rev": "57f5b5c051222d8c630010a0a3cf7d7138910127",
"type": "github"
},
"original": {
"owner": "idris-community",
"repo": "Inigo",
"type": "github"
}
},
"ipkg-to-json": {
"flake": false,
"locked": {
"lastModified": 1634937414,
"narHash": "sha256-LhSmWRpI7vyIQE7QTo38ZTjlqYPVSvV/DIpIxzPmqS0=",
"owner": "claymager",
"repo": "ipkg-to-json",
"rev": "2969b6b83714eeddc31e41577a565778ee5922e6",
"type": "github"
},
"original": {
"owner": "claymager",
"repo": "ipkg-to-json",
"type": "github"
}
},
"json": {
"flake": false,
"locked": {
"lastModified": 1639041459,
"narHash": "sha256-TP/V1jBBP1hFPm/cJ5O2EJiaNoZ19KvBOAI0S9lvAR4=",
"owner": "stefan-hoeck",
"repo": "idris2-json",
"rev": "7c0c028acad0ba0b63b37b92199f37e6ec73864a",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-json",
"type": "github"
}
},
"katla": {
"flake": false,
"locked": {
"lastModified": 1636542431,
"narHash": "sha256-X83NA/P3k1iPcBa8g5z8JldEmFEz/jxVeViJX0/FikY=",
"owner": "idris-community",
"repo": "katla",
"rev": "d841ec243f96b4762074211ee81033e28884c858",
"type": "github"
},
"original": {
"owner": "idris-community",
"repo": "katla",
"type": "github"
}
},
"lsp": {
"flake": false,
"locked": {
"lastModified": 1639486283,
"narHash": "sha256-po396FnUu8iqiipwPxqpFZEU4rtpX3jnt3cySwjLsH8=",
"owner": "idris-community",
"repo": "idris2-lsp",
"rev": "7ebb6caf6bb4b57c5107579aba2b871408e6f183",
"type": "github"
},
"original": {
"owner": "idris-community",
"repo": "idris2-lsp",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1639213685,
"narHash": "sha256-Evuobw7o9uVjAZuwz06Al0fOWZ5JMKOktgXR0XgWBtg=",
"owner": "nixos",
"repo": "nixpkgs",
"rev": "453bcb8380fd1777348245b3c44ce2a2b93b2e2d",
"type": "github"
},
"original": {
"owner": "nixos",
"ref": "nixpkgs-21.11-darwin",
"repo": "nixpkgs",
"type": "github"
}
},
"odf": {
"flake": false,
"locked": {
"lastModified": 1638184051,
"narHash": "sha256-usSdPx+UqOGImHHdHcrytdzi2LXtIRZuUW0fkD/Wwnk=",
"owner": "madman-bob",
"repo": "idris2-odf",
"rev": "d2f532437321c8336f1ca786b44b6ebef4117126",
"type": "github"
},
"original": {
"owner": "madman-bob",
"repo": "idris2-odf",
"type": "github"
}
},
"pretty-show": {
"flake": false,
"locked": {
"lastModified": 1639041411,
"narHash": "sha256-BzEe1fpX+lqGEk8b1JZoQT1db5I7s7SZnLCttRVGXdY=",
"owner": "stefan-hoeck",
"repo": "idris2-pretty-show",
"rev": "a4bc6156b9dac43699f87504cbdb8dada5627863",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-pretty-show",
"type": "github"
}
},
"python": {
"flake": false,
"locked": {
"lastModified": 1635936936,
"narHash": "sha256-c9mcMApN0qgu0AXQVu0V+NXt2poP258wCPkyvtQvv4I=",
"owner": "madman-bob",
"repo": "idris2-python",
"rev": "0eab028933c65bebe744e879881416f5136d6943",
"type": "github"
},
"original": {
"owner": "madman-bob",
"repo": "idris2-python",
"type": "github"
}
},
"rhone": {
"flake": false,
"locked": {
"lastModified": 1639041532,
"narHash": "sha256-2g43shlWQIT/1ogesUBUBV9N8YiD3RwaCbbhdKLVp1s=",
"owner": "stefan-hoeck",
"repo": "idris2-rhone",
"rev": "c4d828b0b8efea495d9a5f1e842a9c67cad57724",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-rhone",
"type": "github"
}
},
"rhone-js": {
"flake": false,
"locked": {
"lastModified": 1639041546,
"narHash": "sha256-ddWVsSRbfA6ghmwiRMzDpHBPM+esGdutuqm1qQZgs88=",
"owner": "stefan-hoeck",
"repo": "idris2-rhone-js",
"rev": "520dd59549f5b14075045314b6805c7492ed636e",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-rhone-js",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": "flake-utils",
"idris2-pkgs": "idris2-pkgs",
"nixpkgs": [
"idris2-pkgs",
"nixpkgs"
]
}
},
"snocvect": {
"flake": false,
"locked": {
"lastModified": 1641633224,
"narHash": "sha256-6zTU4sDzd/R/dFCTNZaX41H4L3/USGLFghMS0Oc9liY=",
"owner": "mattpolzin",
"repo": "idris-snocvect",
"rev": "ff1e7afba360a62f7e522e9bbb856096a79702c4",
"type": "github"
},
"original": {
"owner": "mattpolzin",
"repo": "idris-snocvect",
"type": "github"
}
},
"sop": {
"flake": false,
"locked": {
"lastModified": 1639041379,
"narHash": "sha256-PDTf1Wx6EygiWszguvoVPiqIISYFLabI4e0lXHlrjcA=",
"owner": "stefan-hoeck",
"repo": "idris2-sop",
"rev": "e4354d1883cd73616019457cb9ebf864d99df6a0",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-sop",
"type": "github"
}
},
"tailrec": {
"flake": false,
"locked": {
"lastModified": 1637146655,
"narHash": "sha256-0yi7MQIrISPvAwkgDC1M5PHDEeVyIaISF0HjKDaT0Rw=",
"owner": "stefan-hoeck",
"repo": "idris2-tailrec",
"rev": "dd0bc6381b3a2e69aa37f9a8c1b165d4b1516ad7",
"type": "github"
},
"original": {
"owner": "stefan-hoeck",
"repo": "idris2-tailrec",
"type": "github"
}
},
"xml": {
"flake": false,
"locked": {
"lastModified": 1637939752,
"narHash": "sha256-yYJBhPfwYoi7amlHmeNGrVCOAc3BjZpKTCd9wDs3XEM=",
"owner": "madman-bob",
"repo": "idris2-xml",
"rev": "1292ccfcd58c551089ef699e4560343d5c473d64",
"type": "github"
},
"original": {
"owner": "madman-bob",
"repo": "idris2-xml",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

30
flake.nix Normal file
View file

@ -0,0 +1,30 @@
{ description = "quox: quantitative extensional type theory";
inputs = {
flake-utils.url = "github:numtide/flake-utils";
idris2-pkgs.url = "github:claymager/idris2-pkgs";
nixpkgs.follows = "idris2-pkgs/nixpkgs";
};
outputs = { self, nixpkgs, idris2-pkgs, flake-utils }:
let systems = [ "x86_64-darwin" "x86_64-linux" "i686-linux" ]; in
flake-utils.lib.eachSystem systems (system:
let
pkgs = import nixpkgs {
inherit system;
overlays = [ idris2-pkgs.overlay ];
};
inherit (pkgs.idris2-pkgs._builders) idrisPackage devEnv;
quox = idrisPackage ./. { };
quox-exe = idrisPackage ./exe { extraPkgs.quox = quox; };
quox-tests = idrisPackage ./tests { extraPkgs.quox = quox; };
in
{
defaultPackage = quox-exe;
packages = { inherit quox quox-exe quox-tests; };
devShell = pkgs.mkShell { buildInputs = [ (devEnv quox) ]; };
}
);
}

37
quox.ipkg Normal file
View file

@ -0,0 +1,37 @@
package quox
version = 0
authors = "rhiannon morris"
sourceloc = "https://git.rhiannon.website/rhi/quox"
license = "acsl"
depends = base, contrib, elab-util, sop
sourcedir = "src"
modules =
Quox.Error,
Quox.NatExtra,
Quox.OPE,
Quox.Pretty,
Quox.Syntax,
Quox.Syntax.Dim,
Quox.Syntax.DimEq,
Quox.Syntax.Qty,
Quox.Syntax.Shift,
Quox.Syntax.Subst,
Quox.Syntax.Term,
Quox.Syntax.Term.Base,
Quox.Syntax.Term.Pretty,
Quox.Syntax.Term.Reduce,
Quox.Syntax.Term.Split,
Quox.Syntax.Term.Subst,
Quox.Syntax.Universe,
Quox.Syntax.Var,
Quox.Token,
Quox.Lexer,
Quox.Context,
Quox.Equal,
Quox.Name,
Quox.Reduce,
Quox.Typing,
Quox.Typechecker

55
sirdi.json
View file

@ -1,55 +0,0 @@
[
{
"name" : "quox",
"version" : "0.0.0",
"passthru": {
"license" : "acsl",
"authors" : ["rhiannon morris"],
"sourceloc" : "https://git.rhiannon.website/rhi/quox"
},
"deps" : [
{ "name" : "base", "legacy" : true },
{ "name" : "contrib", "legacy" : true },
{ "name" : "sop",
"git" : {
"url" : "https://git.rhiannon.website/rhi/idris2-sop",
"commit" : "defdbc74a28104a32149922ed9f9ee70099d4f59"
}
}
],
"modules" : [
"Quox.Error",
"Quox.NatExtra",
"Quox.OPE",
"Quox.Pretty",
"Quox.Syntax",
"Quox.Syntax.Dim",
"Quox.Syntax.DimEq",
"Quox.Syntax.Qty",
"Quox.Syntax.Shift",
"Quox.Syntax.Subst",
"Quox.Syntax.Term",
"Quox.Syntax.Term.Base",
"Quox.Syntax.Term.Pretty",
"Quox.Syntax.Term.Reduce",
"Quox.Syntax.Term.Split",
"Quox.Syntax.Term.Subst",
"Quox.Syntax.Universe",
"Quox.Syntax.Var",
"Quox.Token",
"Quox.Lexer",
"Quox.Context",
"Quox.Equal",
"Quox.Name",
"Quox.Reduce",
"Quox.Typing",
"Quox.Typechecker"
]
}
]

7
tests/quox-tests.ipkg Normal file
View file

@ -0,0 +1,7 @@
package quox-tests
depends = base, contrib, elab-util, sop, quox
executable = quox-tests
sourcedir = "src"
main = Tests

21
tests/sirdi.json
View file

@ -1,21 +0,0 @@
[
{
"name" : "quox-tests",
"deps" : [
{ "name" : "base", "legacy" : true },
{ "name" : "contrib", "legacy" : true },
{ "name" : "quox", "local" : ".." }
],
"main" : "Tests",
"modules" : [
"Tests",
"Options",
"TAP",
"Tests.Lexer",
"Tests.Equal"
]
}
]

8
tests/src/Options.idr
View file

@ -30,11 +30,15 @@ getArgs1 : IO (List String)
getArgs1 =
case !getArgs of
_ :: args => pure args
[] => die "expecting getArgs to start with exe name"
[] => do
putStrLn "expecting getArgs to start with exe name"
exitFailure
export
getTestOpts : IO Options
getTestOpts =
case getOpt Permute opts !getArgs1 of
MkResult opts [] [] [] => pure $ makeOpts opts
res => die $ unlines $ res.errors ++ [usageInfo "quox test suite" opts]
res => do
traverse_ putStrLn $ res.errors ++ [usageInfo "quox test suite" opts]
exitFailure

1
tests/src/TAP.idr
View file

@ -5,6 +5,7 @@ import public Quox.Error
import Data.String
import Data.List.Elem
import Data.SnocList
import Control.Monad.Reader
import Control.Monad.State
import System

2
tests/src/Tests.idr
View file

@ -17,5 +17,5 @@ main = do
go <- case opts.tapVersion of
"13" => pure TAP.mainFlat
"14" => pure TAP.main
_ => die "unrecognised TAP version; use 13 or 14"
_ => do putStrLn "unrecognised TAP version; use 13 or 14"; exitFailure
go allTests