diff --git a/aoc2023/Day2.newt b/aoc2023/Day2.newt index 7da3e30..85e78c8 100644 --- a/aoc2023/Day2.newt +++ b/aoc2023/Day2.newt @@ -25,9 +25,9 @@ max x y = case x < y of True => y False => x -pfunc repr : {a : U} -> a -> String := "(a,o) => ''+o" -pfunc jrepr : {a : U} -> a -> String := "(a,o) => JSON.stringify(o, null, ' ')" -pfunc toInt : String -> Int := "s => Number(s)" +pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o` +pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, ' ')` +pfunc toInt : String -> Int := `s => Number(s)` mapM : {a b c : U} -> (a -> Either b c) -> List a -> Either b (List c) mapM f Nil = Right Nil diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt index f90c397..eaddf0b 100644 --- a/aoc2023/Lib.newt +++ b/aoc2023/Lib.newt @@ -89,22 +89,22 @@ pfunc listToArray : {a : U} -> List a -> Array a := " 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 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)" +pfunc getArgs : List String := `arrayToList(String, process.argv)` -- Maybe integrate promises? -pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)" +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" +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 6 _<_ _<=_ infixl 8 _+_ _-_ @@ -112,14 +112,14 @@ infixl 9 _*_ _/_ -- 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 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 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 trim : String -> String := `s => s.trim()` pfunc split : String -> String -> List String := "(s, by) => { let parts = s.split(by) let rval = Nil(String) @@ -128,12 +128,12 @@ pfunc split : String -> String -> List String := "(s, by) => { return rval }" -pfunc slen : String -> Int := "s => s.length" -pfunc sindex : String -> Int -> Char := "(s,i) => s[i]" +pfunc slen : String -> Int := `s => s.length` +pfunc sindex : String -> Int -> Char := `(s,i) => s[i]` infixl 7 _++_ -pfunc _++_ : String -> String -> String := "(a,b) => a + b" +pfunc _++_ : String -> String -> String := `(a,b) => a + b` pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => { diff --git a/aoc2023/Node.newt b/aoc2023/Node.newt index 37a04e8..b255c66 100644 --- a/aoc2023/Node.newt +++ b/aoc2023/Node.newt @@ -2,6 +2,6 @@ module Node import Prelude -pfunc fs : JSObject := "require('fs')" -pfunc getArgs : List String := "arrayToList(String, process.argv)" -pfunc readFile : (fn : String) -> IO String := "(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)" +pfunc fs : JSObject := `require('fs')` +pfunc getArgs : List String := `arrayToList(String, process.argv)` +pfunc readFile : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 7a8c8b1..05b1d04 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -20,8 +20,8 @@ }, { "name": "string.js", - "begin": ":=\\s*\"", - "end": "\"", + "begin": "`", + "end": "`", "patterns": [ { "include": "source.js" } ] diff --git a/newt/JSLib.newt b/newt/JSLib.newt index 1004de3..a9a1b1a 100644 --- a/newt/JSLib.newt +++ b/newt/JSLib.newt @@ -6,12 +6,12 @@ ptype String infixl 4 _+_ infixl 5 _*_ -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` ptype JVoid -- REVIEW - maybe we only have body, use names from the pi-type and generate -- the arrow (or inline?) ourselves -pfunc log : String -> JVoid := "x => console.log(x)" -pfunc debug : {a : U} -> String -> a -> JVoid := "(_,x,a) => console.log(x,a)" +pfunc log : String -> JVoid := `x => console.log(x)` +pfunc debug : {a : U} -> String -> a -> JVoid := `(_,x,a) => console.log(x,a)` diff --git a/newt/Prelude.newt b/newt/Prelude.newt index f75dc9e..642502f 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -231,13 +231,13 @@ pfunc listToArray : {a : U} -> List a -> Array a := " 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 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 fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')" -pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')" +pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` +pfunc replicate : Nat -> Char → String := `() => abort('FIXME replicate')` @@ -261,4 +261,4 @@ iopure a = \ w => MkIORes a w IOMonad : Monad IO IOMonad = MkMonad iobind iopure -pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)" +pfunc putStrLn : String -> IO Unit := `(s) => (w) => console.log(s)` diff --git a/newt/tutorial.newt b/newt/tutorial.newt index 33441d2..593afe5 100644 --- a/newt/tutorial.newt +++ b/newt/tutorial.newt @@ -11,5 +11,5 @@ ptype Int ptype Array : U -> U -- declare a primitive function -pfunc alength : {a : U} -> Array a -> Int := "(x) => x.length" +pfunc alength : {a : U} -> Array a -> Int := `(x) => x.length` diff --git a/playground/samples/Day2.newt b/playground/samples/Day2.newt index 45f9e76..5ebcae8 100644 --- a/playground/samples/Day2.newt +++ b/playground/samples/Day2.newt @@ -24,9 +24,9 @@ max x y = case x < y of True => y False => x -pfunc repr : {a : U} -> a -> String := "(a,o) => ''+o" -pfunc jrepr : {a : U} -> a -> String := "(a,o) => JSON.stringify(o, null, ' ')" -pfunc toInt : String -> Int := "s => Number(s)" +pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o` +pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, ' ')` +pfunc toInt : String -> Int := `s => Number(s)` mapM : {a b c : U} -> (a -> Either b c) -> List a -> Either b (List c) mapM f Nil = Right Nil diff --git a/playground/samples/Lib.newt b/playground/samples/Lib.newt deleted file mode 100644 index f90c397..0000000 --- a/playground/samples/Lib.newt +++ /dev/null @@ -1,162 +0,0 @@ -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 7 _::_ -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 0 _,_ - -data Pair : U -> U -> U where - _,_ : {a b : U} -> a -> b -> Pair a b - --- Idris says it special cases to deal with unification issues -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 6 _<_ _<=_ -infixl 8 _+_ _-_ -infixl 9 _*_ _/_ - --- 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 7 _++_ -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 9 _∘_ -_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C -(f ∘ g) x = f (g x) diff --git a/playground/samples/Prelude.newt b/playground/samples/Prelude.newt index 4a98028..da29d0a 100644 --- a/playground/samples/Prelude.newt +++ b/playground/samples/Prelude.newt @@ -182,13 +182,13 @@ ptype Int ptype Char -- probably want to switch to Int or implement magic Nat -pfunc length : String → Nat := "(s) => { +pfunc length : String → Nat := `(s) => { let rval = Z for (let i = 0; i < s.length; s++) rval = S(rval) return rval -}" +}` -pfunc sconcat : String → String → String := "(x,y) => x + y" +pfunc sconcat : String → String → String := `(x,y) => x + y` instance Concat String where _++_ = sconcat @@ -196,7 +196,7 @@ data Unit : U where MkUnit : Unit ptype Array : U → U -pfunc listToArray : {a : U} -> List a -> Array a := " +pfunc listToArray : {a : U} -> List a -> Array a := ` (a, l) => { let rval = [] while (l.tag !== 'Nil') { @@ -205,52 +205,52 @@ pfunc listToArray : {a : U} -> List a -> Array a := " } 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 alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length` +pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]` +pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []` -pfunc arrayToList : {a} → Array a → List a := "(a,arr) => { +pfunc arrayToList : {0 a} → Array a → List a := `(a,arr) => { let rval = Nil(a) for (let i = arr.length - 1;i >= 0; i--) { rval = _$3A$3A_(a, arr[i], rval) } return rval -}" +}` -- for now I'll run this in JS -pfunc lines : String → List String := "(s) => arrayToList(s.split('\\n'))" +pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))` -pfunc p_strHead : (s : String) -> Char := "(s) => s[0]" -pfunc p_strTail : (s : String) -> String := "(s) => s[0]" +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) => { +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]" +pfunc slen : String -> Int := `s => s.length` +pfunc sindex : String -> Int -> Char := `(s,i) => s[i]` -- TODO represent Nat as number at runtime -pfunc natToInt : Nat -> Int := "(n) => { +pfunc natToInt : Nat -> Int := `(n) => { let rval = 0 while (n.tag === 'S') { n = n.h0 rval++ } return rval -}" +}` -pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')" -pfunc replicate : Nat -> Char → String := "(n,c) => c.repeat(natToInt(n))" +pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` +pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` -- I don't want to use an empty type because it would be a proof of void ptype World @@ -266,12 +266,12 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w -pfunc putStrLn : String -> IO Unit := "(s) => (w) => { +pfunc putStrLn : String -> IO Unit := `(s) => (w) => { console.log(s) return MkIORes(Unit,MkUnit,w) -}" +}` -pfunc showInt : Int -> String := "(i) => String(i)" +pfunc showInt : Int -> String := `(i) => String(i)` class Show a where show : a → String @@ -282,18 +282,18 @@ instance Show String where instance Show Int where show = showInt -pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)" +pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` infix 6 _<=_ -pfunc _<=_ : Int -> Int -> Bool := "(x,y) => (x <= y) ? True : False" +pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False` pfunc unpack : String -> List Char - := "(s) => { + := `(s) => { let acc = Nil(Char) for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) return acc -}" +}` @@ -306,10 +306,10 @@ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C (f ∘ g) x = f (g x) -pfunc addInt : Int → Int → Int := "(x,y) => x + y" -pfunc mulInt : Int → Int → Int := "(x,y) => x * y" -pfunc subInt : Int → Int → Int := "(x,y) => x - y" -pfunc ltInt : Int → Int → Bool := "(x,y) => x < y ? True : False" +pfunc addInt : Int → Int → Int := `(x,y) => x + y` +pfunc mulInt : Int → Int → Int := `(x,y) => x * y` +pfunc subInt : Int → Int → Int := `(x,y) => x - y` +pfunc ltInt : Int → Int → Bool := `(x,y) => x < y ? True : False` instance Mul Int where x * y = mulInt x y diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt index 59c379d..3c5977a 100644 --- a/playground/samples/Tour.newt +++ b/playground/samples/Tour.newt @@ -118,8 +118,8 @@ isVowel _ = False -- And primitive functions have a type and a javascript definition: -pfunc plusInt : Int -> Int -> Int := "(x,y) => x + y" -pfunc plusString : String -> String -> String := "(x,y) => x + y" +pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y` +pfunc plusString : String -> String -> String := `(x,y) => x + y` -- We can make them Plus instances: diff --git a/playground/src/worker.ts b/playground/src/worker.ts index b9d737d..ea4b326 100644 --- a/playground/src/worker.ts +++ b/playground/src/worker.ts @@ -118,7 +118,6 @@ process.stdout.write = (s) => { }; // hack for now const preload = [ - "Lib.newt", "Prelude.newt", "aoc2023/day1/eg.txt", "aoc2023/day1/eg2.txt", diff --git a/port/Prelude.newt b/port/Prelude.newt index d0352e3..da29d0a 100644 --- a/port/Prelude.newt +++ b/port/Prelude.newt @@ -182,13 +182,13 @@ ptype Int ptype Char -- probably want to switch to Int or implement magic Nat -pfunc length : String → Nat := "(s) => { +pfunc length : String → Nat := `(s) => { let rval = Z for (let i = 0; i < s.length; s++) rval = S(rval) return rval -}" +}` -pfunc sconcat : String → String → String := "(x,y) => x + y" +pfunc sconcat : String → String → String := `(x,y) => x + y` instance Concat String where _++_ = sconcat @@ -196,7 +196,7 @@ data Unit : U where MkUnit : Unit ptype Array : U → U -pfunc listToArray : {a : U} -> List a -> Array a := " +pfunc listToArray : {a : U} -> List a -> Array a := ` (a, l) => { let rval = [] while (l.tag !== 'Nil') { @@ -205,52 +205,52 @@ pfunc listToArray : {a : U} -> List a -> Array a := " } return rval } -" +` -pfunc alen : {0 a : U} -> Array a -> Int := "(a,arr) => arr.length" -pfunc aget : {0 a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]" -pfunc aempty : {0 a : U} -> Unit -> Array a := "() => []" +pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length` +pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]` +pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []` -pfunc arrayToList : {0 a} → Array a → List a := "(a,arr) => { +pfunc arrayToList : {0 a} → Array a → List a := `(a,arr) => { let rval = Nil(a) for (let i = arr.length - 1;i >= 0; i--) { rval = _$3A$3A_(a, arr[i], rval) } return rval -}" +}` -- for now I'll run this in JS -pfunc lines : String → List String := "(s) => arrayToList(s.split('\\n'))" +pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))` -pfunc p_strHead : (s : String) -> Char := "(s) => s[0]" -pfunc p_strTail : (s : String) -> String := "(s) => s[0]" +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) => { +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]" +pfunc slen : String -> Int := `s => s.length` +pfunc sindex : String -> Int -> Char := `(s,i) => s[i]` -- TODO represent Nat as number at runtime -pfunc natToInt : Nat -> Int := "(n) => { +pfunc natToInt : Nat -> Int := `(n) => { let rval = 0 while (n.tag === 'S') { n = n.h0 rval++ } return rval -}" +}` -pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')" -pfunc replicate : Nat -> Char → String := "(n,c) => c.repeat(natToInt(n))" +pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` +pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` -- I don't want to use an empty type because it would be a proof of void ptype World @@ -266,12 +266,12 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w -pfunc putStrLn : String -> IO Unit := "(s) => (w) => { +pfunc putStrLn : String -> IO Unit := `(s) => (w) => { console.log(s) return MkIORes(Unit,MkUnit,w) -}" +}` -pfunc showInt : Int -> String := "(i) => String(i)" +pfunc showInt : Int -> String := `(i) => String(i)` class Show a where show : a → String @@ -282,18 +282,18 @@ instance Show String where instance Show Int where show = showInt -pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)" +pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` infix 6 _<=_ -pfunc _<=_ : Int -> Int -> Bool := "(x,y) => (x <= y) ? True : False" +pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False` pfunc unpack : String -> List Char - := "(s) => { + := `(s) => { let acc = Nil(Char) for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) return acc -}" +}` @@ -306,10 +306,10 @@ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C (f ∘ g) x = f (g x) -pfunc addInt : Int → Int → Int := "(x,y) => x + y" -pfunc mulInt : Int → Int → Int := "(x,y) => x * y" -pfunc subInt : Int → Int → Int := "(x,y) => x - y" -pfunc ltInt : Int → Int → Bool := "(x,y) => x < y ? True : False" +pfunc addInt : Int → Int → Int := `(x,y) => x + y` +pfunc mulInt : Int → Int → Int := `(x,y) => x * y` +pfunc subInt : Int → Int → Int := `(x,y) => x - y` +pfunc ltInt : Int → Int → Bool := `(x,y) => x < y ? True : False` instance Mul Int where x * y = mulInt x y diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index b642a59..b4eca45 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -399,7 +399,7 @@ parsePFunc = do keyword ":" ty <- typeExpr keyword ":=" - src <- cast <$> token StringKind + src <- cast <$> token JSLit pure $ PFunc fc nm ty src export diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr index 162b65b..087da5e 100644 --- a/src/Lib/Token.idr +++ b/src/Lib/Token.idr @@ -13,6 +13,7 @@ data Kind | Number | Character | StringKind + | JSLit | Symbol | Space | Comment @@ -40,6 +41,7 @@ Show Kind where show EOI = "EOI" show Pragma = "Pragma" show StringKind = "String" + show JSLit = "JSLit" export Eq Kind where Ident == Ident = True @@ -54,6 +56,7 @@ Eq Kind where Semi == Semi = True RBrace == RBrace = True StringKind == StringKind = True + JSLit == JSLit = True _ == _ = False export diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 7fd6611..bc692bb 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -49,6 +49,18 @@ unquote str = case unpack str of opMiddle = pred (\c => not (isSpace c || c == '_')) +btick = is '`' + +trimJS : String -> String +trimJS str = case unpack str of + ('`' :: xs) => pack $ go xs + bug => pack $ go bug + where + go : List Char -> List Char + go [] = [] + go ['`'] = [] + go (x :: xs) = x :: go xs + rawTokens : Tokenizer (Token Kind) rawTokens = match spaces (Tok Space) @@ -68,6 +80,7 @@ rawTokens <|> match (lineComment (exact "--")) (Tok Space) <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space) <|> match (upper <+> many identMore) checkUKW + <|> match (btick <+> manyUntil btick any <+> btick) (Tok JSLit . trimJS) <|> match (quo <+> manyUntil quo (esc any <|> any) <+> quo) (Tok StringKind . unquote) -- accept almost everything, but <|> match (some (non (space <|> singleton))) checkKW diff --git a/tests/black/Auto.newt b/tests/black/Auto.newt index 9ee8c84..d070a74 100644 --- a/tests/black/Auto.newt +++ b/tests/black/Auto.newt @@ -3,8 +3,8 @@ module Auto ptype String ptype Int -pfunc i2s : Int -> String := "(i) => ''+i" -pfunc _++_ : String -> String -> String := "(a,b) => a + b" +pfunc i2s : Int -> String := `(i) => ''+i` +pfunc _++_ : String -> String -> String := `(a,b) => a + b` infixl 4 _++_ @@ -21,7 +21,7 @@ showInt : Show Int showInt = MkShow i2s ptype World -pfunc log : {A : U} -> A -> World := "(_, a) => console.log(a)" +pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)` main : Int -> World main _ = log ("answer: " ++ show 42) diff --git a/tests/black/Auto2.newt b/tests/black/Auto2.newt index 1dc63de..c04a400 100644 --- a/tests/black/Auto2.newt +++ b/tests/black/Auto2.newt @@ -1,10 +1,10 @@ module Auto2 ptype World -pfunc log : {A : U} -> A -> World := "(_, a) => console.log(a)" +pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)` ptype Int -pfunc i_plus : Int -> Int -> Int := "(x,y) => x + y" +pfunc i_plus : Int -> Int -> Int := `(x,y) => x + y` data Nat : U where Z : Nat diff --git a/tests/black/Oper.newt b/tests/black/Oper.newt index a0350c7..8d5282c 100644 --- a/tests/black/Oper.newt +++ b/tests/black/Oper.newt @@ -20,9 +20,9 @@ ptype JVoid -- If we had a different quote here, we could tell vscode it's javascript. -- or actually just switch modes inside pfunc -pfunc log : String -> JVoid := "(x) => console.log(x)" -pfunc plus : Int -> Int -> Int := "(x,y) => x + y" -pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y" +pfunc log : String -> JVoid := `(x) => console.log(x)` +pfunc plus : Int -> Int -> Int := `(x,y) => x + y` +pfunc _*_ : Int -> Int -> Int := `(x,y) => x * y` -- We now have to clean JS identifiers _+_ : Int -> Int -> Int diff --git a/tests/black/TestCase5.newt b/tests/black/TestCase5.newt index a700eb9..a26eebb 100644 --- a/tests/black/TestCase5.newt +++ b/tests/black/TestCase5.newt @@ -10,7 +10,7 @@ _+_ : {A : U} {{_ : Plus A}} -> A -> A -> A _+_ {{MkPlus plus}} x y = plus x y ptype Int -pfunc plusInt : Int -> Int -> Int := "(x,y) => x + y" +pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y` PlusInt : Plus Int PlusInt = MkPlus plusInt diff --git a/tests/black/TestPrim.newt b/tests/black/TestPrim.newt index 0116af8..7de5eca 100644 --- a/tests/black/TestPrim.newt +++ b/tests/black/TestPrim.newt @@ -7,7 +7,7 @@ module TestPrim ptype String ptype Int -pfunc strlen : String -> Int := "(x) => x.length()" +pfunc strlen : String -> Int := `(x) => x.length()` -- why is there an eta in here? foo : String -> Int @@ -16,12 +16,12 @@ foo = \ x => strlen x bar : String -> String -> Int bar = \ x y => strlen x -pfunc append : String -> String -> String := "(a,b) => a + b" +pfunc append : String -> String -> String := `(a,b) => a + b` blah : String blah = append "hello" "world" -pfunc plus : Int -> Int -> Int := "(a,b) => a + b" +pfunc plus : Int -> Int -> Int := `(a,b) => a + b` answer : Int answer = plus 40 2 @@ -30,7 +30,7 @@ answer = plus 40 2 -- codegen test cases -- works, but two looks like () => (eta1) => (eta0) => one(eta1, eta0) -pfunc one : Int -> Int -> Int := "(x,y) => x + y" +pfunc one : Int -> Int -> Int := `(x,y) => x + y` two : Int -> Int -> Int two = one