165 lines
3.7 KiB
Plaintext
165 lines
3.7 KiB
Plaintext
module Lib
|
|
|
|
-- Prelude
|
|
data Unit : U where
|
|
MkUnit : Unit
|
|
|
|
data Bool : U where
|
|
True : Bool
|
|
False : Bool
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
data Maybe : U -> U where
|
|
Just : {a : U} -> a -> Maybe a
|
|
Nothing : {a : U} -> Maybe a
|
|
|
|
data Either : U -> U -> U where
|
|
Left : {a b : U} -> a -> Either a b
|
|
Right : {a b : U} -> b -> Either a b
|
|
|
|
|
|
infixr 4 _::_
|
|
data List : U -> U where
|
|
Nil : {a : U} -> List a
|
|
_::_ : {a : U} -> a -> List a -> List a
|
|
|
|
Cons : {a : U} -> a -> List a -> List a
|
|
Cons x xs = x :: xs
|
|
|
|
-- TODO where clauses
|
|
reverse' : {A : U} -> List A -> List A -> List A
|
|
reverse' Nil acc = acc
|
|
reverse' (x :: xs) acc = reverse' xs (x :: acc)
|
|
|
|
reverse : {A : U} -> List A -> List A
|
|
reverse xs = reverse' xs Nil
|
|
|
|
length : {a : U} -> List a -> Nat
|
|
length Nil = Z
|
|
length (x :: xs) = S (length xs)
|
|
|
|
infixr 2 _,_
|
|
|
|
data Pair : U -> U -> U where
|
|
_,_ : {a b : U} -> a -> b -> Pair a b
|
|
|
|
infixr 0 _$_
|
|
|
|
_$_ : {a b : U} -> (a -> b) -> a -> b
|
|
f $ a = f a
|
|
|
|
-- JS Bridge
|
|
|
|
ptype Dummy
|
|
|
|
|
|
ptype World
|
|
data IO : U -> U where
|
|
MkIO : {a : U} -> (World -> Pair World a) -> IO a
|
|
|
|
-- TODO unified Number for now
|
|
ptype Int
|
|
ptype String
|
|
|
|
ptype Char
|
|
|
|
ptype Array : U -> U
|
|
|
|
pfunc arrayToList : {a : U} -> Array a -> List a := "
|
|
(a, arr) => {
|
|
let rval = Nil(a)
|
|
for (let i = arr.length - 1; i >= 0; i--) {
|
|
rval = Cons(a, arr[i], rval)
|
|
}
|
|
return rval
|
|
}
|
|
"
|
|
|
|
pfunc listToArray : {a : U} -> List a -> Array a := "
|
|
(a, l) => {
|
|
let rval = []
|
|
while (l.tag !== 'Nil') {
|
|
rval.push(l.h1)
|
|
l = l.h2
|
|
}
|
|
return rval
|
|
}
|
|
"
|
|
pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length"
|
|
pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
|
|
pfunc aempty : {a : U} -> Unit -> Array a := "() => []"
|
|
|
|
pfunc getArgs : List String := "arrayToList(String, process.argv)"
|
|
-- Maybe integrate promises?
|
|
|
|
|
|
pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)"
|
|
|
|
pfunc _<_ : Int -> Int -> Bool := "(x,y) => (x < y) ? True : False"
|
|
pfunc _<=_ : Int -> Int -> Bool := "(x,y) => (x <= y) ? True : False"
|
|
pfunc _+_ : Int -> Int -> Int := "(x,y) => x + y"
|
|
pfunc _-_ : Int -> Int -> Int := "(x,y) => x - y"
|
|
pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
|
|
pfunc _/_ : Int -> Int -> Int := "(x,y) => x / y"
|
|
infix 3 _<_
|
|
infix 3 _<=_
|
|
infixl 4 _-_
|
|
infixl 4 _+_
|
|
infixl 5 _*_
|
|
infixl 5 _/_
|
|
|
|
|
|
-- Ideally we'd have newt write the arrows for us to keep things correct
|
|
-- We'd still have difficulty with callbacks...
|
|
pfunc fs : Dummy := "require('fs')"
|
|
pfunc readFile : (fn : String) -> String := "(fn) => fs.readFileSync(fn, 'utf8')"
|
|
pfunc log : {a : U} -> a -> Dummy := "(a, obj) => console.log(obj)"
|
|
|
|
pfunc p_strHead : (s : String) -> Char := "(s) => s[0]"
|
|
pfunc p_strTail : (s : String) -> String := "(s) => s[0]"
|
|
|
|
pfunc trim : String -> String := "s => s.trim()"
|
|
pfunc split : String -> String -> List String := "(s, by) => {
|
|
let parts = s.split(by)
|
|
let rval = Nil(String)
|
|
parts.reverse()
|
|
parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
|
|
return rval
|
|
}"
|
|
|
|
pfunc slen : String -> Int := "s => s.length"
|
|
pfunc sindex : String -> Int -> Char := "(s,i) => s[i]"
|
|
|
|
|
|
infixl 4 _++_
|
|
pfunc _++_ : String -> String -> String := "(a,b) => a + b"
|
|
|
|
|
|
pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => {
|
|
console.log(lab,a)
|
|
return a
|
|
}"
|
|
|
|
pfunc unpack : String -> List Char
|
|
:= "(s) => {
|
|
let acc = Nil(Char)
|
|
for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
|
|
return acc
|
|
}"
|
|
|
|
foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
|
|
foldl f acc Nil = acc
|
|
foldl f acc (x :: xs) = foldl f (f acc x) xs
|
|
|
|
map : {A B : U} -> (A -> B) -> List A -> List B
|
|
map f Nil = Nil
|
|
map f (x :: xs) = f x :: map f xs
|
|
|
|
|
|
infixl 7 _._
|
|
_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
|
|
(f . g) x = f ( g x)
|