mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-26 18:37:43 +03:00
Merge branch 'master' of github.com:uwu-tech/kind
I had to temporarily comment some lines on export.kind due to a error type-checking the cached version on KindJS.
This commit is contained in:
commit
d831cf5037
2
.gitignore
vendored
2
.gitignore
vendored
@ -5,6 +5,8 @@ scripts/
|
||||
src/_*
|
||||
src/tmp*
|
||||
bin/hs/cabal.project.local*
|
||||
bin/scm/scheme/
|
||||
bin/scm/bin/
|
||||
tmp.js
|
||||
.vscode
|
||||
*.orig
|
||||
|
6
.gitmodules
vendored
6
.gitmodules
vendored
@ -0,0 +1,6 @@
|
||||
[submodule "bin/scm/chez-exe"]
|
||||
path = bin/scm/chez-exe
|
||||
url = git@github.com:rigille/chez-exe.git
|
||||
[submodule "bin/scm/ChezScheme"]
|
||||
path = bin/scm/ChezScheme
|
||||
url = git@github.com:racket/ChezScheme.git
|
92
INSTALL.md
92
INSTALL.md
@ -2,96 +2,32 @@
|
||||
|
||||
The Scheme backend handles recursion better than the default Javascript backend. That means it never stack overflows in deep recursions.
|
||||
|
||||
## Linux
|
||||
# Prebuilt binaries
|
||||
|
||||
If you're using a Debian-based distro, like Ubuntu or Mint, you could download the [latest debian binary package](https://github.com/uwu-tech/Kind/releases) and install it by double-clicking the file. In other cases building from source is the way to go.
|
||||
Kind is distributed as a single binary executable. You can download it [here](https://github.com/uwu-tech/Kind/releases).
|
||||
|
||||
### Building from source
|
||||
# Building from source
|
||||
|
||||
**1.** First [install chezscheme](https://command-not-found.com/scheme). To check if you succeeded run.
|
||||
|
||||
```shell
|
||||
scheme --version
|
||||
```
|
||||
|
||||
**2.** Go to the Kind directory, pull the latest version, and run:
|
||||
**1.** Go to the root of the repository, pull the latest version, and run:
|
||||
|
||||
```shell
|
||||
cd bin/scm
|
||||
git submodule update --init --recursive
|
||||
make
|
||||
```
|
||||
|
||||
if you're fine installing the binary in `/usr/local/bin/`
|
||||
It may take some time. You can grab a cup of coffee while you wait. At the end you should see the `kind-scm` executable inside `bin/scm/bin/`. Try running it:
|
||||
|
||||
```shell
|
||||
./bin/kind-scm
|
||||
```
|
||||
|
||||
You can install it wherever you want. If you're fine placing it in `/usr/local/bin/` then run.
|
||||
|
||||
```shell
|
||||
sudo make install
|
||||
```
|
||||
|
||||
**3.** To check if the install succeeded, navigate to the `Kind/base` folder and run
|
||||
To update repeat those same steps, it'll probably be much faster.
|
||||
|
||||
```shell
|
||||
kind-scm
|
||||
```
|
||||
|
||||
If you're greeted with a help message then `kind-scm` is installed. :slightly_smiling_face:
|
||||
|
||||
## MacOS
|
||||
|
||||
Currently, the only way to install the Scheme backend on macOS is to build from the source.
|
||||
|
||||
### Building from source
|
||||
|
||||
**1.** First you'll need to [build](https://github.com/racket/ChezScheme/blob/master/BUILDING) and install [Racket's fork](https://github.com/racket/ChezScheme) of ChezScheme:
|
||||
|
||||
```shell
|
||||
git clone https://github.com/racket/ChezScheme.git
|
||||
cd ChezScheme
|
||||
```
|
||||
|
||||
**2.** Then install the dependencies and configure:
|
||||
|
||||
```bash
|
||||
git submodule init
|
||||
git submodule update
|
||||
./configure --pb --disable-curses --disable-x11
|
||||
```
|
||||
|
||||
- For Macbook chip M1 run `make tarm64osx.bootquick`. It should output `Configuring for tarm64osx`.
|
||||
|
||||
- For Macbook chip Intel run `make ta6osx.bootquick`. It should run without errors.
|
||||
|
||||
```bash
|
||||
./configure --disable-curses --disable-x11
|
||||
make
|
||||
sudo make install
|
||||
```
|
||||
|
||||
**3.** To check if ChezScheme was successfully installed run:
|
||||
|
||||
```bash
|
||||
scheme --version
|
||||
```
|
||||
|
||||
it should print the version, like `9.5.5`.
|
||||
|
||||
**4.** Go to the Kind directory (if you don't have it yet, just clone it) and run:
|
||||
|
||||
```bash
|
||||
cd bin/scm
|
||||
make
|
||||
sudo make install
|
||||
```
|
||||
|
||||
It may take some time. You can grab a cup of coffee while it finishes.
|
||||
|
||||
**5.** Now `kind-scm` is installed, great! Run `kind-scm` inside the `Kind` repository and see if you're greeted with help text.
|
||||
|
||||
If you have any problem, [let us know](https://github.com/uwu-tech/Kind/issues).
|
||||
|
||||
### Update
|
||||
Go to the Kind directory, pull the latest version, and run:
|
||||
```bash
|
||||
cd bin/scm
|
||||
make
|
||||
sudo make install
|
||||
```
|
||||
If something doesn't work, [let us know](https://github.com/uwu-tech/Kind/issues) ;)
|
||||
|
@ -298,7 +298,7 @@ branch as `name.field`. For example, when matching a `List`, we gain access to
|
||||
its head and tail as `list.head` and `list.tail`:
|
||||
|
||||
```
|
||||
sum(list: List<Nat>): List<Nat>
|
||||
sum(list: List<Nat>): Nat
|
||||
case list {
|
||||
nil: 0
|
||||
cons: list.head + sum(list.tail)
|
||||
|
@ -575,9 +575,10 @@ App.KL.Game.Phase.Play.draw.canvas(
|
||||
}
|
||||
let img = App.KL.Game.Phase.Play.draw.board(game, local@preview, hits, local@user, local@mouse, img)
|
||||
let img = App.KL.Game.Phase.Play.draw.bases(game, local@user, img)
|
||||
let img = App.KL.Game.Phase.Play.draw.cursor(local@mouse, img)
|
||||
let img = App.KL.Game.Phase.Play.draw.cursor(local@mouse,game.board, img)
|
||||
img
|
||||
|
||||
|
||||
// draw canvas board
|
||||
App.KL.Game.Phase.Play.draw.landscape(blueprint: App.KL.Game.Board.Blueprint, img: VoxBox): VoxBox
|
||||
let landscape = blueprint@landscape
|
||||
@ -720,11 +721,18 @@ App.KL.Game.Phase.Play.Draw.get_indicators(
|
||||
// draw mouse indicator
|
||||
App.KL.Game.Phase.Play.draw.cursor(
|
||||
mouse: Pair<U32, U32>
|
||||
board: App.KL.Game.Board
|
||||
img: VoxBox
|
||||
): VoxBox
|
||||
coord = Hexagonal.Axial.from_screen_xy(mouse, App.KL.Constants.hexagon_radius, App.KL.Constants.center_x, App.KL.Constants.center_y)
|
||||
{x,y} = App.KL.Game.Phase.Play.draw.centralize.old(coord)
|
||||
VoxBox.Draw.image(x, y, App.KL.Constants.z_index.cursor, App.KL.Game.Field.Mouse.mouse_ui, img)
|
||||
let has_tile = App.KL.Game.Tile.get(coord, board)
|
||||
case has_tile {
|
||||
none:
|
||||
img
|
||||
some:
|
||||
VoxBox.Draw.image(x, y, App.KL.Constants.z_index.cursor, App.KL.Game.Field.Mouse.mouse_ui, img)
|
||||
}
|
||||
|
||||
// draws tile terrain
|
||||
App.KL.Game.Phase.Play.draw.tile.terrain(
|
||||
|
@ -47,7 +47,7 @@ App.Sharmi.Mouse.deserialize(hex: String): Maybe<App.Sharmi.Mouse>
|
||||
Deserializer.run!(App.Sharmi.Mouse.deserializer, Bits.hex.decode(hex))
|
||||
|
||||
App.Sharmi.room: String
|
||||
App.room("asodovciveneiejenfufjfj3n2os")
|
||||
App.room("110202039383883737370sj1i202")
|
||||
|
||||
type App.Sharmi.Goal {
|
||||
new(
|
||||
@ -66,7 +66,7 @@ type App.Sharmi.Body {
|
||||
type App.Sharmi.Player {
|
||||
new(
|
||||
address: String
|
||||
throttle: I32
|
||||
throttle: F64
|
||||
dir: V2
|
||||
pos: Physics.Verlet
|
||||
)
|
||||
@ -135,9 +135,9 @@ App.Sharmi.Player.draw(
|
||||
img
|
||||
)
|
||||
let col = if e@throttle =? 0 then
|
||||
Col32.new(255, 0, 0, 255)
|
||||
else
|
||||
Col32.new(0, 0, 0, 255)
|
||||
else
|
||||
Col32.new(255, 0, 0, 255)
|
||||
let img =
|
||||
VoxBox.Draw.line(
|
||||
F64.to_i32(e@pos@pos@x)
|
||||
@ -224,25 +224,23 @@ App.Sharmi.when: App.When<App.Sharmi.State>
|
||||
let new_players = []
|
||||
for player in state.local.state.players with new_players:
|
||||
open player; open player.pos
|
||||
let new_acc = App.Sharmi.Gravity(state.local.state, player.pos.pos)
|
||||
open new_acc;
|
||||
//log(player.name|" new_acc: {"|F64.show(new_acc.x)|", "|F64.show(new_acc.y)|"}")
|
||||
let new_pos = player.pos@acc <- new_acc
|
||||
let player =
|
||||
case state.global.state@mouses{player@address} as mouse {
|
||||
some:
|
||||
let new_dir = App.Sharmi.Mouse.pos_to_v2(mouse.value@pos) - player@pos@pos
|
||||
let player = player@dir <- new_dir
|
||||
if mouse.value@pressed then
|
||||
player@throttle <- 200
|
||||
player@throttle <- 20
|
||||
else
|
||||
player@throttle <- 0
|
||||
none:
|
||||
player
|
||||
}
|
||||
let player = player@acc <- player@acc + V2.scale(player@throttle/V2.len(new.player@dir), player@dir)
|
||||
let new_pos = Physics.Verlet.step(new_pos, 1.0/60.0)
|
||||
let player = player@pos <- new_pos
|
||||
open player; open player.pos;
|
||||
let new_acc = App.Sharmi.Gravity(state.local.state, player.pos.pos) + V2.scale(player.throttle/V2.len(player.dir), player.dir)
|
||||
let pos = player.pos@acc <- new_acc
|
||||
let pos = Physics.Verlet.step(pos, 1.0/60.0)
|
||||
let player = player@pos <- pos
|
||||
player & new_players
|
||||
let new_players = List.reverse!(new_players)
|
||||
|
||||
|
@ -1,13 +1,13 @@
|
||||
type Cmp.Order<A: Type>(cmp: A -> A -> Cmp) {
|
||||
new(
|
||||
refl:
|
||||
(a: A, b: A, H: Equal<Cmp>(cmp(a, b), Cmp.eql))
|
||||
(a: A, b: A, H: Equal<Cmp>(cmp(a, b), Cmp.eql)) ->
|
||||
(Equal<A>(a, b))
|
||||
antisym:
|
||||
(a: A, b: A)
|
||||
(a: A, b: A) ->
|
||||
(Equal<Cmp>(cmp(a, b), Cmp.inv(cmp(b, a)))),
|
||||
trans:
|
||||
(a: A, b: A, c: A, H0: Equal<Cmp>(cmp(a, b), cmp(b, c)))
|
||||
(a: A, b: A, c: A, H0: Equal<Cmp>(cmp(a, b), cmp(b, c))) ->
|
||||
(Equal<Cmp>(cmp(b, c), cmp(a, c)))
|
||||
)
|
||||
}
|
||||
|
@ -1,21 +1,28 @@
|
||||
String.at(len : Nat, str : String) : Pair<String, String>
|
||||
{String.take(len, str), String.drop(len, str)}
|
||||
|
||||
|
||||
Ether.RLP.merge_tree(x : List<Ether.RLP.Tree>, y : Ether.RLP.Tree) : Ether.RLP.Tree
|
||||
case y {
|
||||
tip : Ether.RLP.Tree.list(y & x)
|
||||
list : Ether.RLP.Tree.list(y.value ++ x)
|
||||
}
|
||||
|
||||
Ether.RLP.listing(encode : String) : Pair<List<Ether.RLP.Tree>, String>
|
||||
Ether.RLP.decode.list(encode : String) : Pair<List<Ether.RLP.Tree>, String>
|
||||
if (String.length(encode) =? 0) || String.eql(encode, "error") then
|
||||
{[], encode}
|
||||
else
|
||||
let {tree, rest} = Ether.RLP.decode.read(encode)
|
||||
let {trees, rest} = Ether.RLP.listing(rest)
|
||||
let {trees, rest} = Ether.RLP.decode.list(rest)
|
||||
{tree & trees, rest}
|
||||
|
||||
Ether.RLP.decode.binary(value : String) : Nat
|
||||
let {head, rest} = String.at(2, value)
|
||||
let decode = Bits.to_nat(Bits.hex.decode(String.reverse(head)))
|
||||
if (String.length(rest) =? 0) then
|
||||
decode
|
||||
else
|
||||
Ether.RLP.decode.binary(rest) + (decode * 256)
|
||||
|
||||
Ether.RLP.decode.read(encode : String) : Pair<Ether.RLP.Tree, String>
|
||||
let {prefix, rest} = String.at(2, encode)
|
||||
let byte_prefix = Bits.hex.decode(String.reverse(prefix))
|
||||
@ -24,60 +31,32 @@ Ether.RLP.decode.read(encode : String) : Pair<Ether.RLP.Tree, String>
|
||||
Ether.RLP.Constants.bits_128 : {Ether.RLP.Tree.tip(byte_prefix), rest} // between (0, 127)
|
||||
Ether.RLP.Constants.bits_184 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 128) * 2
|
||||
if (bytes_size >? content_length) then
|
||||
let {prefix, rest} = String.at(content_length, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
let {prefix, rest} = String.at(content_length, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
Ether.RLP.Constants.bits_192 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 183) * 2
|
||||
let {head, rest} = String.at(content_length, rest)
|
||||
let length = Ether.RLP.decode_binary(head)
|
||||
let verifier = (Bits.to_nat(byte_prefix) - (183 + length)) * 2
|
||||
if (bytes_size >? content_length) && (bytes_size >? verifier) then
|
||||
let {prefix, rest} = String.at(length *2, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
let length = Ether.RLP.decode.binary(head)
|
||||
let {prefix, rest} = String.at(length *2, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
Ether.RLP.Constants.bits_248 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 192) * 2
|
||||
if (bytes_size >? content_length) then
|
||||
if String.length(rest) =? 0 then
|
||||
{Ether.RLP.Tree.list([]), rest}
|
||||
else
|
||||
let {xs, rest} = Ether.RLP.listing(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
let {xs, rest} = Ether.RLP.decode.list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
Ether.RLP.Constants.bits_255 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 247) * 2
|
||||
let {head, rest} = String.at(content_length, rest)
|
||||
let length = Ether.RLP.decode_binary(head)
|
||||
let verifier = (Bits.to_nat(byte_prefix) - (247 + length)) * 2
|
||||
if (bytes_size >? content_length) && (bytes_size >? verifier) then
|
||||
if String.length(rest) =? 0 then
|
||||
{Ether.RLP.Tree.list([]), rest}
|
||||
else
|
||||
let {xs, rest} = Ether.RLP.listing(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"}
|
||||
let length = Ether.RLP.decode.binary(head)
|
||||
let {xs, rest} = Ether.RLP.decode.list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
} default {Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
|
||||
Ether.RLP.decode_binary(value : String) : Nat
|
||||
let {head, rest} = String.at(2, value)
|
||||
let decode = Bits.to_nat(Bits.hex.decode(String.reverse(head)))
|
||||
if (String.length(rest) =? 0) then
|
||||
decode
|
||||
else
|
||||
Ether.RLP.decode_binary(rest) + (decode * 256)
|
||||
|
||||
Ether.RLP.decode : _
|
||||
// let x = Nat.pow(2, 16) - 1
|
||||
// let v = Ether.RLP.encode.read(Ether.RPL.encode.binary(x))
|
||||
|
||||
// {Ether.RPL.encode.binary(x),
|
||||
// Ether.RLP.decode_binary(String.drop(2, v))}
|
||||
// Ether.RLP.decode.binary(String.drop(2, v))}
|
||||
|
||||
let hello = Bits.read(String.reverse("011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001011000010110000101100001"))
|
||||
let xs = Ether.RLP.encode.bytes(Ether.RLP.Tree.list([Ether.RLP.Tree.list([Ether.RLP.Tree.tip(hello)]), Ether.RLP.Tree.tip(hello)]))
|
||||
|
43
base/Ether/RLP/verifiy/decode.kind
Normal file
43
base/Ether/RLP/verifiy/decode.kind
Normal file
@ -0,0 +1,43 @@
|
||||
String.at(len : Nat, str : String) : Pair<String, String>
|
||||
{String.take(len, str), String.drop(len, str)}
|
||||
|
||||
Ether.RLP.verifiy.decode(encode : String) : Pair<Ether.RLP.Tree, String>
|
||||
let {prefix, rest} = String.at(2, encode)
|
||||
let byte_prefix = Bits.hex.decode(String.reverse(prefix))
|
||||
def bytes_size = String.length(encode)
|
||||
switch (Bits.ltn(byte_prefix)) {
|
||||
Ether.RLP.Constants.bits_128 : {Ether.RLP.Tree.tip(byte_prefix), rest} // between (0, 127)
|
||||
Ether.RLP.Constants.bits_184 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 128) * 2
|
||||
if (bytes_size >? content_length) then
|
||||
let {prefix, rest} = String.at(content_length, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
Ether.RLP.Constants.bits_192 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 183) * 2
|
||||
let {head, rest} = String.at(content_length, rest)
|
||||
let length = Ether.RLP.decode.binary(head)
|
||||
let verifier = (Bits.to_nat(byte_prefix) - (183 + length)) * 2
|
||||
if (bytes_size >? content_length) && (bytes_size >? verifier) then
|
||||
let {prefix, rest} = String.at(length *2, rest)
|
||||
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
Ether.RLP.Constants.bits_248 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 192) * 2
|
||||
if (bytes_size >? content_length) then
|
||||
if String.length(rest) =? 0 then
|
||||
{Ether.RLP.Tree.list([]), rest}
|
||||
else
|
||||
let {xs, rest} = Ether.RLP.decode.list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
else
|
||||
{Ether.RLP.Tree.list([]), "error"} // treat this case after
|
||||
Ether.RLP.Constants.bits_255 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 247) * 2
|
||||
let {head, rest} = String.at(content_length, rest)
|
||||
let length = Ether.RLP.decode.binary(head)
|
||||
let {xs, rest} = Ether.RLP.decode.list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
} default {Ether.RLP.Tree.list([]), "error"} // treat this case after
|
@ -1,12 +1,12 @@
|
||||
Fin(lim: Nat): Type
|
||||
case lim {
|
||||
zero:
|
||||
Fin.self<P: (:Fin(Nat.zero)) Type>
|
||||
Fin.self<P: (:Fin(Nat.zero)) -> Type> ->
|
||||
P(Fin.self)
|
||||
succ:
|
||||
Fin.self<P: (:Fin(Nat.succ(lim.pred))) Type>
|
||||
Fin.self<P: (:Fin(Nat.succ(lim.pred))) -> Type>
|
||||
(zero: P(Fin.zero(lim.pred)))
|
||||
(succ: (pred: Fin(lim.pred)) P(Fin.succ(lim.pred, pred)))
|
||||
(succ: (pred: Fin(lim.pred)) -> P(Fin.succ(lim.pred, pred))) ->
|
||||
P(Fin.self)
|
||||
}
|
||||
|
||||
|
@ -1,4 +1,3 @@
|
||||
I32.show(a: I32): String
|
||||
open a
|
||||
Word.s_show!(a.value)
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
type IO <A: Type> {
|
||||
end(value: A),
|
||||
ask(query: String, param: String, then: (response: String) IO<A>),
|
||||
ask(query: String, param: String, then: (response: String) -> IO<A>),
|
||||
}
|
@ -383,8 +383,9 @@ Kind.Comp.Target.Scheme.basics: Kind.Comp.Basics
|
||||
""
|
||||
(kstring-append
|
||||
(if fst "" sep)
|
||||
(car strs)
|
||||
(kstring_join sep (cdr strs) #f))))
|
||||
(kstring-append
|
||||
(car strs)
|
||||
(kstring_join sep (cdr strs) #f)))))
|
||||
|
||||
; Short alias to vector-ref
|
||||
(define get vector-ref)
|
||||
|
@ -2,7 +2,7 @@ Kind.Parser.forall: Parser(Kind.Term)
|
||||
Kind.Parser.block("forall", Parser {
|
||||
get self = Kind.Parser.name
|
||||
get bind = Kind.Parser.binder(":")
|
||||
Parser.maybe!(Kind.Parser.text("->"))
|
||||
Kind.Parser.text("->")
|
||||
get body = Kind.Parser.term
|
||||
let term = List.fold!(bind)!(body, (x,t) case x {
|
||||
new: Kind.Term.all(x.eras, "", x.name, x.term, (s,x) t)
|
||||
|
@ -1,4 +1,12 @@
|
||||
Kind.Parser.lambda: Parser(Kind.Term)
|
||||
Kind.Parser.block("term", Parser {
|
||||
Parser.choice!([
|
||||
Kind.Parser.lambda.1,
|
||||
Kind.Parser.lambda.2
|
||||
])
|
||||
})
|
||||
|
||||
Kind.Parser.lambda.1: Parser(Kind.Term)
|
||||
Kind.Parser.block("lambda", Parser {
|
||||
get nams = Kind.Parser.items!("(", Kind.Parser.name1, ")")
|
||||
get body = Parser.avoiding!(Kind.Parser.text_now("("), Kind.Parser.term)
|
||||
@ -35,3 +43,36 @@ Kind.Parser.lambda.make(names: List<Kind.Name>, body: Kind.Term): Kind.Term
|
||||
cons: Kind.Term.lam(names.head, (x) Kind.Parser.lambda.make(names.tail, body))
|
||||
}
|
||||
|
||||
Kind.Parser.lambda.name_term: Parser(Pair<Kind.Name, Maybe<Kind.Term>>)
|
||||
Parser {
|
||||
get name = Kind.Parser.name1
|
||||
get term = Parser.maybe!(Parser {
|
||||
Kind.Parser.text(":")
|
||||
get type = Kind.Parser.term
|
||||
return type
|
||||
})
|
||||
return {name, term}
|
||||
}
|
||||
|
||||
|
||||
Kind.Parser.lambda.2: Parser<Kind.Term>
|
||||
Kind.Parser.block("lambda", Parser {
|
||||
get nams = Kind.Parser.items!("(", Kind.Parser.lambda.name_term, ")")
|
||||
get body = Parser.avoiding!(Kind.Parser.text_now("("), Kind.Parser.term)
|
||||
let {nams, types} = List.unzip!!(nams)
|
||||
let lamb = Kind.Parser.lambda.make.start(nams, body)
|
||||
let type = Kind.Parser.lambda.get_type(types)
|
||||
let term = Kind.Term.ann(false, lamb, type)
|
||||
return term
|
||||
})
|
||||
|
||||
Kind.Parser.lambda.get_type(types: List<Maybe<Kind.Term>>): Kind.Term
|
||||
case types {
|
||||
nil: Kind.Term.hol(Bits.e)
|
||||
cons:
|
||||
let type = case types.head {
|
||||
none: Kind.Term.hol(Bits.e)
|
||||
some: types.head.value
|
||||
}
|
||||
Kind.Term.all(false, "", "", type, (s,x) Kind.Parser.lambda.get_type(types.tail))
|
||||
}
|
@ -1,8 +1,8 @@
|
||||
Kind.api.export: IO<Unit>
|
||||
IO {
|
||||
let e = Kind.api.io.term_to_core
|
||||
let e = Kind.api.io.term_to_scheme
|
||||
let e = Kind.api.io.terms_to_scheme_lib
|
||||
//let e = Kind.api.io.term_to_scheme
|
||||
//let e = Kind.api.io.terms_to_scheme_lib
|
||||
let e = Kind.api.io.check_file
|
||||
let e = Kind.api.io.check_files
|
||||
let e = Kind.api.io.check_term
|
||||
|
@ -1,2 +1,2 @@
|
||||
Kind.version: String
|
||||
"1.0.86"
|
||||
"1.0.90"
|
||||
|
9
base/List/unzip.kind
Normal file
9
base/List/unzip.kind
Normal file
@ -0,0 +1,9 @@
|
||||
List.unzip<A: Type, B: Type>(xs: List<Pair<A,B>>): Pair<List<A>,List<B>>
|
||||
case xs {
|
||||
nil: {List.nil!, List.nil!},
|
||||
cons:
|
||||
let rec = List.unzip!!(xs.tail)
|
||||
open xs.head
|
||||
open rec
|
||||
{xs.head.fst & rec.fst, xs.head.snd & rec.snd}
|
||||
}
|
@ -1,6 +1,6 @@
|
||||
type Monad <M: Type -> Type> {
|
||||
new(
|
||||
bind: <A: Type, B: Type> M<A> -> (A -> M<B>) -> M<B>
|
||||
pure: <A: Type> A -> M<A>
|
||||
bind: <A: Type, B: Type> -> M<A> -> (A -> M<B>) -> M<B>
|
||||
pure: <A: Type> -> A -> M<A>
|
||||
)
|
||||
}
|
||||
|
@ -2,8 +2,8 @@ type Monoid<A: Type>{
|
||||
new(
|
||||
op: A -> A -> A,
|
||||
e: A,
|
||||
assoc: (a: A, b: A, c: A) Equal(A,op(op(a,b),c),op(a,op(b,c))),
|
||||
neuter_left: (a: A) Equal(A,op(e, a), a),
|
||||
neuter_right: (a: A) Equal(A, op(a, e), a),
|
||||
assoc: (a: A, b: A, c: A) -> Equal(A,op(op(a,b),c),op(a,op(b,c))),
|
||||
neuter_left: (a: A) -> Equal(A,op(e, a), a),
|
||||
neuter_right: (a: A) -> Equal(A, op(a, e), a),
|
||||
)
|
||||
}
|
||||
|
@ -1,4 +1,4 @@
|
||||
Nat.apply<A: Type>(n: Nat, f: (x:A) A, x: A): A
|
||||
Nat.apply<A: Type>(n: Nat, f: (x:A) -> A, x: A): A
|
||||
case n {
|
||||
zero: x,
|
||||
succ: Nat.apply<A>(n.pred, f, f(x)),
|
||||
|
@ -1,9 +1,2 @@
|
||||
UPair<A: Type, B: Type>: Type
|
||||
self<P: UPair<A,B> -> Type>
|
||||
(new: (fst: A, snd: B) -> P(UPair.new<A,B>(fst,snd)))
|
||||
P(self)
|
||||
|
||||
UPair.new<A: Type, B: Type>(fst: A, snd: B): UPair<A,B>
|
||||
<P> (new) new(fst, snd)
|
||||
|
||||
|
||||
Test: _
|
||||
(x: Nat) x + x
|
||||
|
@ -16,6 +16,11 @@ type User.rigille.Elementary.Expression {
|
||||
)
|
||||
}
|
||||
|
||||
User.rigille.Elementary.Expression.from_nat(n: Nat): User.rigille.Elementary.Expression
|
||||
let i = Int.from_nat(n)
|
||||
User.rigille.Elementary.constexp(i)
|
||||
|
||||
|
||||
type User.rigille.Elementary.Op {
|
||||
add
|
||||
mult
|
||||
|
3
base/V2/len.kind
Normal file
3
base/V2/len.kind
Normal file
@ -0,0 +1,3 @@
|
||||
V2.len(a: V2): F64
|
||||
open a
|
||||
F64.sqrt((a.x*a.x) + (a.y*a.y))
|
@ -14,11 +14,11 @@
|
||||
Vector(A: Type, len: Nat): Type
|
||||
case len {
|
||||
zero:
|
||||
self(P: (self: Vector(A,0)) Type) ->
|
||||
self(P: (self: Vector(A,0)) -> Type) ->
|
||||
(nil: P(Vector.nil(A))) ->
|
||||
P(self)
|
||||
succ:
|
||||
self(P: (self: Vector(A,Nat.succ(len.pred))) Type) ->
|
||||
self(P: (self: Vector(A,Nat.succ(len.pred))) -> Type) ->
|
||||
(cons: (head: A) -> (tail: Vector(A, len.pred)) -> P(Vector.cons(A,len.pred,head,tail))) ->
|
||||
P(self)
|
||||
}
|
||||
|
@ -1,2 +1,2 @@
|
||||
Vector.main: Nat
|
||||
Vector.head<Nat,_>(Vector.from_list<Nat>(3, [1, 2, 3]))
|
||||
Vector.head<Nat,_>(Vector.from_list<Nat>([1, 2, 3]))
|
||||
|
@ -2,4 +2,4 @@ Word.s_show(size: Nat)(a: Word(size)): String
|
||||
neg = Word.is_neg(size, a)
|
||||
n = Word.to_nat!(Word.abs!(a))
|
||||
sgn = if neg then "-" else "+"
|
||||
sgn | Nat.show(n) | "#" | Nat.show(size)
|
||||
sgn | Nat.show(n)
|
||||
|
44967
bin/js/src/kind.js
44967
bin/js/src/kind.js
File diff suppressed because one or more lines are too long
@ -1,4 +1,4 @@
|
||||
#!/usr/bin/env -S node --stack-size=100000
|
||||
#!/usr/bin/env node
|
||||
|
||||
var kind = require("./kind.js");
|
||||
var fs = require("fs");
|
||||
|
1
bin/scm/ChezScheme
Submodule
1
bin/scm/ChezScheme
Submodule
@ -0,0 +1 @@
|
||||
Subproject commit bf49dfbd8c47c759bc2ac99978a0db02b2969578
|
@ -1,17 +1,45 @@
|
||||
all: bin/kind-scm kind-scm.deb
|
||||
chezdir := ChezScheme
|
||||
chezexedir := chez-exe
|
||||
# choose wether to use kind or kind-scm for bootstrapping
|
||||
kind := kind-scm
|
||||
|
||||
all: bin/kind-scm
|
||||
|
||||
deb: kind-scm.deb
|
||||
|
||||
# compiles kind files to scheme
|
||||
# do this after modifying the compiler source-code
|
||||
bootstrap:
|
||||
cd ../../base && kind-scm Kind.Comp.Target.Scheme.bootstrap --run
|
||||
cd ../../base && $(kind) Kind.Comp.Target.Scheme.bootstrap --run
|
||||
|
||||
clean:
|
||||
rm src/*.wpo
|
||||
rm src/*.so
|
||||
rm src/*.chez
|
||||
rm src/*.generated.c
|
||||
rm bin/*
|
||||
bin/kind-scm:
|
||||
cd src/ && scheme compile.scm
|
||||
|
||||
bin/kind-scm: scheme/bin/compile-chez-program scheme/bin/scheme
|
||||
./$(chezexedir)/compile-chez-program --full-chez --libdirs src --optimize-level 2 src/main.scm
|
||||
mv src/main bin/kind-scm
|
||||
chmod +x bin/kind-scm
|
||||
|
||||
kind-scm.deb: bin/kind-scm
|
||||
mkdir -p kind-scm_1.0.1-0_amd64/usr/local/bin/
|
||||
cp bin/kind-scm kind-scm_1.0.1-0_amd64/usr/local/bin/
|
||||
dpkg-deb --root-owner-group --build kind-scm_1.0.1-0_amd64/ bin/kind-scm_1.0.1-0_amd64.deb
|
||||
|
||||
install: bin/kind-scm
|
||||
chmod +x bin/kind-scm
|
||||
cp bin/kind-scm /usr/local/bin/
|
||||
|
||||
scheme/bin/scheme:
|
||||
cd $(chezdir) && git submodule init && git submodule update
|
||||
cd $(chezdir) && ./configure --pb --kernelobj --disable-curses --disable-iconv --disable-x11
|
||||
cd $(chezdir) && make auto.bootquick
|
||||
cd $(chezdir) && ./configure --kernelobj --disable-curses --disable-iconv --disable-x11 --installprefix=$(PWD)/scheme
|
||||
cd $(chezdir) && make -j && make install
|
||||
|
||||
scheme/bin/compile-chez-program: scheme/bin/scheme
|
||||
cd $(chezexedir) && ./../scheme/bin/scheme --script gen-config.ss --scheme $(PWD)/scheme/bin/scheme --bootpath $$(dirname $$(find ../scheme -name kernel.o)) --prefix $(PWD)/scheme
|
||||
cd $(chezexedir) && make install
|
||||
|
BIN
bin/scm/bin/kind-scm
Executable file
BIN
bin/scm/bin/kind-scm
Executable file
Binary file not shown.
1
bin/scm/chez-exe
Submodule
1
bin/scm/chez-exe
Submodule
@ -0,0 +1 @@
|
||||
Subproject commit 937629ad6cdcec698f0b25d996bb9b01a3b7cce7
|
@ -1,7 +1,6 @@
|
||||
Package: kind-scm
|
||||
Version: 1.0.59
|
||||
Version: 1.0.90
|
||||
Architecture: amd64
|
||||
Maintainer: Rígille S. B. Menezes <rigillesbmenezes@protonmail.com>
|
||||
Depends: chezscheme
|
||||
Description: ChezScheme release of the kind programming language.
|
||||
A minimal, efficient and practical proof and programming language. Under the hoods, it is basically Haskell, except purer and with dependent types. That means it can handle mathematical theorems just like Coq, Idris, Lean and Agda. On the surface, it aims to be more practical and looks more like TypeScript.
|
||||
|
0
bin/scm/scheme/.keep
Normal file
0
bin/scm/scheme/.keep
Normal file
File diff suppressed because one or more lines are too long
@ -4,7 +4,7 @@
|
||||
(let ([args (cdr (command-line))])
|
||||
(if (null? args)
|
||||
(print-lines
|
||||
'("# kind-scm 1.0.85"
|
||||
'("# kind-scm 1.0.86"
|
||||
""
|
||||
"Usage:"
|
||||
""
|
||||
@ -73,4 +73,4 @@
|
||||
(display (run_io (Kind.api.io.term_to_core fst_arg))))
|
||||
(else
|
||||
(display "unrecognized cli argument: ")
|
||||
(display snd_arg))))))))
|
||||
(display snd_arg))))))))
|
Loading…
Reference in New Issue
Block a user