fix some things

This commit is contained in:
Joeri Exelmans 2025-05-08 21:30:56 +02:00
parent d9111c3969
commit bbac7858ae
16 changed files with 69 additions and 55 deletions

View file

@ -9,12 +9,12 @@ const mkType = makeTypeParser({
});
export const ModuleDict = [
{ i: emptyDict , t: mkType("∀a,b: (a -> a -> Int) -> (a => b)") },
{ i: has , t: mkType("∀a,b: (a => b) -> a -> Bool")},
{ i: set , t: mkType("∀a,b: (a => b) -> a -> b -> (a => b)")},
{ i: remove , t: mkType("∀a,b: (a => b) -> a -> (a => b)")},
{ i: length , t: mkType("∀a,b: (a => b) -> Int")},
{ i: first , t: mkType("∀a,b: (a => b) -> (a |=>| b)")},
{ i: last , t: mkType("∀a,b: (a => b) -> (a |=>| b)")},
{ i: read , t: mkType("∀a,b: (a |=>| b) -> (Unit + ((a*b) * (a |=>| b)))")},
{ i: emptyDict , t: mkType("(a -> a -> Int) -> (a => b)") },
{ i: has , t: mkType("(a => b) -> a -> Bool")},
{ i: set , t: mkType("(a => b) -> a -> b -> (a => b)")},
{ i: remove , t: mkType("(a => b) -> a -> (a => b)")},
{ i: length , t: mkType("(a => b) -> Int")},
{ i: first , t: mkType("(a => b) -> (a |=>| b)")},
{ i: last , t: mkType("(a => b) -> (a |=>| b)")},
{ i: read , t: mkType("(a |=>| b) -> (Unit + ((a*b) * (a |=>| b)))")},
];

View file

@ -4,12 +4,12 @@ import { emptyList, fold, get, length, map, pop, push, put } from "./list.js";
const mkType = getDefaultTypeParser();
export const ModuleList = [
{ i: emptyList, t: mkType("∀a: [a]")},
{ i: get , t: mkType("∀a: [a] -> Int -> a")},
{ i: put , t: mkType("∀a: [a] -> Int -> a -> [a]")},
{ i: push , t: mkType("∀a: [a] -> a -> [a]")},
{ i: pop , t: mkType("∀a: [a] -> a")},
{ i: map , t: mkType("∀a: [a] -> (a -> b) -> [b]")},
{ i: length , t: mkType("∀a: [a] -> Int")},
{ i: fold , t: mkType("∀a: [a] -> (b -> a -> b) -> b -> b")},
{ i: emptyList, t: mkType("[a]")},
{ i: get , t: mkType("[a] -> Int -> a")},
{ i: put , t: mkType("[a] -> Int -> a -> [a]")},
{ i: push , t: mkType("[a] -> a -> [a]")},
{ i: pop , t: mkType("[a] -> a")},
{ i: map , t: mkType("[a] -> (a -> b) -> [b]")},
{ i: length , t: mkType("[a] -> Int")},
{ i: fold , t: mkType("[a] -> (b -> a -> b) -> b -> b")},
];

View file

@ -4,7 +4,7 @@ import { newProduct, getLeft, getRight } from "./product.js";
const mkType = getDefaultTypeParser();
export const ModuleProduct = [
{ i: newProduct, t: mkType("∀a,b: a -> b -> (a * b)") },
{ i: getLeft , t: mkType("∀a,b: (a * b) -> a" ) },
{ i: getRight , t: mkType("∀a,b: (a * b) -> b" ) },
{ i: newProduct, t: mkType("a -> b -> (a * b)") },
{ i: getLeft , t: mkType("(a * b) -> a" ) },
{ i: getRight , t: mkType("(a * b) -> b" ) },
];

View file

@ -9,13 +9,13 @@ const mkType = makeTypeParser({
});
export const ModuleSet = [
{ i: emptySet , t: mkType("∀a: (a -> a -> Int) -> {a}") },
{ i: has , t: mkType("∀a: {a} -> a -> Bool")},
{ i: add , t: mkType("∀a: {a} -> a -> {a}")},
{ i: remove , t: mkType("∀a: {a} -> a -> {a}")},
{ i: length , t: mkType("∀a: {a} -> Int")},
{ i: fold , t: mkType("∀a,b: {a} -> (b -> a -> b) -> b")},
{ i: first , t: mkType("∀a: {a} -> <a>")},
{ i: last , t: mkType("∀a: {a} -> <a>")},
{ i: read , t: mkType("∀a: <a> -> (Unit + (a * <a>))")},
{ i: emptySet , t: mkType("(a -> a -> Int) -> {a}") },
{ i: has , t: mkType("{a} -> a -> Bool")},
{ i: add , t: mkType("{a} -> a -> {a}")},
{ i: remove , t: mkType("{a} -> a -> {a}")},
{ i: length , t: mkType("{a} -> Int")},
{ i: fold , t: mkType("{a} -> (b -> a -> b) -> b")},
{ i: first , t: mkType("{a} -> <a>")},
{ i: last , t: mkType("{a} -> <a>")},
{ i: read , t: mkType("<a> -> (Unit + (a * <a>))")},
];

View file

@ -4,7 +4,7 @@ import { match, newLeft, newRight } from "./sum.js";
const mkType = getDefaultTypeParser();
export const ModuleSum = [
{ i: newLeft , t: mkType("∀a,b: a -> (a + b)") },
{ i: newRight , t: mkType("∀a,b: b -> (a + b)") },
{ i: match , t: mkType("∀a,b,c: (a + b) -> (a -> c) -> (b -> c) -> c") },
{ i: newLeft , t: mkType("a -> (a + b)") },
{ i: newRight , t: mkType("b -> (a + b)") },
{ i: match , t: mkType("(a + b) -> (a -> c) -> (b -> c) -> c") },
];