JS compiler, initial book

book/Nat.kind

@@ -0,0 +1,4 @@
+Nat : * = #[]{
+  #zero{} : Nat
+  #succ{ pred: Nat } : Nat
+}

book/Nat/double.kind

@@ -0,0 +1,7 @@
+Nat/double
+: ∀(n: Nat)
+  Nat
+= λ{
+  #zero: #zero{}
+  #succ: λpred #succ{#succ{(Nat/double pred)}}
+}

book/U32/double.kind

@@ -0,0 +1,4 @@
+U32/double
+: ∀(x: U32)
+  U32
+= λx (* x 2)

book/U48/double.kind

@@ -1,4 +0,0 @@
-U48/double
-: ∀(x: U48)
-  U48
-= λx (* x 2)

book/main.js

@@ -0,0 +1,32 @@
+function APPLY(f, x) {
+  switch (x.length) {
+    case 0: return f;
+    case 1: console.log("a"); return f(x.x0);
+    case 2: return f(x.x0)(x.x1);
+    case 3: return f(x.x0)(x.x1)(x.x2);
+    case 4: return f(x.x0)(x.x1)(x.x2)(x.x3);
+    case 5: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4);
+    case 6: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5);
+    case 7: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5)(x.x6);
+    case 8: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5)(x.x6)(x.x7);
+    default:
+      for (let i = 0; i < x.length; i++) {
+        f = f(x['x' + i]);
+      }
+      return f;
+  }
+}
+
+Nat = null;
+Nat_double = (x => {
+  switch (x.$) {
+    case "zero":
+      return APPLY({$: "zero", length: 0}, x);
+    case "succ":
+      return APPLY((pred$0 => ({$: "succ", length: 1, x0: {$: "succ", length: 1, x0: (Nat_double)(pred$0)}})), x);
+  }
+});
+
+main = (Nat_double)({$: "succ", length: 1, x0: {$: "succ", length: 1, x0: {$: "zero", length: 0}}});
+
+console.log(JSON.stringify(main));

book/main.kind

@@ -1,3 +1,3 @@
 main
-: U48
-= (U48/double 20);
+: Nat
+= (Nat/double #succ{#succ{#zero{}}})

kind-lang.cabal

@@ -15,14 +15,15 @@ common warnings
 library
     import:           warnings
     exposed-modules:  Kind
-                    , Kind.Type
-                    , Kind.Env
-                    , Kind.Reduce
-                    , Kind.Equal
-                    , Kind.Check
-                    , Kind.Show
-                    , Kind.Parse
                     , Kind.API
+                    , Kind.Check
+                    , Kind.Compile
+                    , Kind.Env
+                    , Kind.Equal
+                    , Kind.Parse
+                    , Kind.Reduce
+                    , Kind.Show
+                    , Kind.Type
     other-modules:    
     build-depends:    base ^>=4.20.0.0
                     , containers ==0.7

src/Kind.hs

@@ -1,19 +1,20 @@
 module Kind (
-  module Kind.Type,
-  module Kind.Env,
-  module Kind.Reduce,
-  module Kind.Equal,
+  module Kind.API,
   module Kind.Check,
-  module Kind.Show,
+  module Kind.Env,
+  module Kind.Equal,
   module Kind.Parse,
-  module Kind.API
+  module Kind.Reduce,
+  module Kind.Show,
+  module Kind.Type,
 ) where
 
-import Kind.Type
-import Kind.Env
-import Kind.Reduce
-import Kind.Equal
-import Kind.Check
-import Kind.Show
-import Kind.Parse
 import Kind.API
+import Kind.Check
+import Kind.Compile
+import Kind.Env
+import Kind.Equal
+import Kind.Parse
+import Kind.Reduce
+import Kind.Show
+import Kind.Type

src/Kind/API.hs

@@ -1,3 +1,11 @@
+-- //./Type.hs//
+-- //./Compile.hs//
+
+
+
+
+
+
 module Kind.API where
 
 import Control.Monad (forM_, foldM)
@@ -8,6 +16,7 @@ import Kind.Parse
 import Kind.Reduce
 import Kind.Show
 import Kind.Type
+import Kind.Compile
 import System.Directory (getCurrentDirectory, doesDirectoryExist, doesFileExist)
 import System.Environment (getArgs)
 import System.Exit (exitFailure)
@@ -81,6 +90,12 @@ apiShow book name = case M.lookup name book of
   Just term -> putStrLn $ termShow term
   Nothing -> putStrLn $ "Error: Definition '" ++ name ++ "' not found."
 
+-- Compiles the whole book to JS
+apiToJS :: Book -> String -> IO ()
+apiToJS book name = do
+  let jsCode = compileJS book
+  putStrLn jsCode
+
 -- Prints logs from the type-checker
 apiPrintLogs :: State -> IO ()
 apiPrintLogs (State book fill susp logs) = 
@@ -138,6 +153,7 @@ main = do
         ["check", input] -> runCommand basePath apiCheck input
         ["run", input]   -> runCommand basePath apiNormal input
         ["show", input]  -> runCommand basePath apiShow input
+        ["to-js", input] -> runCommand basePath apiToJS input
         ["deps", input]  -> runDeps basePath input
         ["help"]         -> printHelp
         []               -> printHelp
@@ -162,5 +178,6 @@ printHelp = do
   putStrLn "  kind check <name|path> # Type-checks the specified definition"
   putStrLn "  kind run   <name|path> # Normalizes the specified definition"
   putStrLn "  kind show  <name|path> # Stringifies the specified definition"
+  putStrLn "  kind to-js <name|path> # Compiles the specified definition to JavaScript"
   putStrLn "  kind deps  <name|path> # Shows dependencies of the specified definition"
   putStrLn "  kind help              # Shows this help message"

src/Kind/Check.hs

@@ -108,16 +108,16 @@ infer term dep = {-trace ("infer: " ++ termShower True term dep) $-} go term dep
     return Set
 
   -- ...
-  -- --------- U48-type
-  -- U48 : Set
-  go U48 dep = do
+  -- --------- U32-type
+  -- U32 : Set
+  go U32 dep = do
     return Set
 
   -- ...
-  -- ----------- U48-value
-  -- <num> : U48
+  -- ----------- U32-value
+  -- <num> : U32
   go (Num num) dep = do
-    return U48
+    return U32
 
   -- ...
   -- -------------- String-literal
@@ -131,26 +131,26 @@ infer term dep = {-trace ("infer: " ++ termShower True term dep) $-} go term dep
   go (Nat val) dep = do
     return (Ref "Nat")
 
-  -- fst : U48
-  -- snd : U48
-  -- ----------------- U48-operator
-  -- (+ fst snd) : U48
+  -- fst : U32
+  -- snd : U32
+  -- ----------------- U32-operator
+  -- (+ fst snd) : U32
   go (Op2 opr fst snd) dep = do
-    envSusp (Check Nothing fst U48 dep)
-    envSusp (Check Nothing snd U48 dep)
-    return U48
+    envSusp (Check Nothing fst U32 dep)
+    envSusp (Check Nothing snd U32 dep)
+    return U32
 
-  -- x : U48
-  -- p : U48 -> Set
+  -- x : U32
+  -- p : U32 -> Set
   -- z : (p 0)
-  -- s : (n: U48) -> (p (+ 1 n))
-  -- ------------------------------------- U48-elim
+  -- s : (n: U32) -> (p (+ 1 n))
+  -- ------------------------------------- U32-elim
   -- (switch x { 0: z ; _: s }: p) : (p x)
   go (Swi nam x z s p) dep = do
-    envSusp (Check Nothing x U48 dep)
-    envSusp (Check Nothing (p (Ann False (Var nam dep) U48)) Set dep)
+    envSusp (Check Nothing x U32 dep)
+    envSusp (Check Nothing (p (Ann False (Var nam dep) U32)) Set dep)
     envSusp (Check Nothing z (p (Num 0)) dep)
-    envSusp (Check Nothing (s (Ann False (Var (nam ++ "-1") dep) U48)) (p (Op2 ADD (Num 1) (Var (nam ++ "-1") dep))) (dep + 1))
+    envSusp (Check Nothing (s (Ann False (Var (nam ++ "-1") dep) U32)) (p (Op2 ADD (Num 1) (Var (nam ++ "-1") dep))) (dep + 1))
     return (p x)
 
   -- val : typ

src/Kind/Compile.hs

@@ -0,0 +1,126 @@
+module Kind.Compile where
+
+import Kind.Type
+import Kind.Reduce
+
+import qualified Data.Map.Strict as M
+import qualified Data.IntMap.Strict as IM
+
+import Prelude hiding (EQ, LT, GT)
+
+nameToJS :: String -> String
+nameToJS = map (\c -> if c == '/' || c == '.' then '$' else c)
+
+termToJS :: Term -> Int -> String
+termToJS term dep = case term of
+  All _ _ _ ->
+    "null"
+  Lam nam bod ->
+    let nam' = nameToJS nam ++ "$" ++ show dep
+        bod' = termToJS (bod (Var nam dep)) (dep + 1)
+    in concat ["(", nam', " => ", bod', ")"]
+  App fun arg   ->
+    let fun' = termToJS fun dep
+        arg' = termToJS arg dep
+    in concat ["(", fun', ")(", arg', ")"]
+  Ann _ val _ ->
+    termToJS val dep
+  Slf _ _ _ ->
+    "null"
+  Ins val ->
+    termToJS val dep
+  Dat _ _ ->
+    "null"
+  Con nam arg ->
+    let arg' = map (\x -> termToJS x dep) arg
+        fds' = concat (zipWith (\i x -> concat [", x", show i, ": ", x]) [0..] arg')
+    in concat ["{$: \"", nameToJS nam, "\", length: ", show (length arg), fds', "}"]
+  Mat cse ->
+    let cse' = map (\(cnam, cbod) -> concat ["case \"", nameToJS cnam, "\": return APPLY(", termToJS cbod dep, ", x);"]) cse
+    in concat ["(x => ({ switch (x.$) { ", unwords cse', " } }))"]
+  Ref nam ->
+    nameToJS nam
+  Let nam val bod ->
+    let nam' = nameToJS nam ++ "$" ++ show dep
+        val' = termToJS val dep
+        bod' = termToJS (bod (Var nam dep)) (dep + 1)
+    in concat ["((", nam', " => ", bod', ")(", val', "))"]
+  Use nam val bod ->
+    let val' = termToJS val dep
+        bod' = termToJS (bod val) dep
+    in concat ["((", val', ") => ", bod', ")"]
+  Set ->
+    "null"
+  U32 ->
+    "null"
+  Num val ->
+    show val
+  Op2 opr fst snd ->
+    let opr' = operToJS opr
+        fst' = termToJS fst dep
+        snd' = termToJS snd dep
+    in concat ["((", fst', " ", opr', " ", snd', ") >>> 0)"]
+  Swi nam x z s p ->
+    let x' = termToJS x dep
+        z' = termToJS z dep
+        s' = termToJS (s (Var (nam ++ "-1") dep)) (dep + 1)
+        p' = termToJS (p (Var nam dep)) dep
+    in concat ["((", x', " === 0) ? ", z', " : ", s', ")"]
+  Txt txt ->
+    show txt
+  Nat val ->
+    show val
+  Hol _ _ ->
+    "null"
+  Met _ _ ->
+    "null"
+  Var nam idx ->
+    nameToJS nam ++ "$" ++ show idx
+  Src _ val ->
+    termToJS val dep
+
+operToJS :: Oper -> String
+operToJS ADD = "+"
+operToJS SUB = "-"
+operToJS MUL = "*"
+operToJS DIV = "/"
+operToJS MOD = "%"
+operToJS EQ  = "==="
+operToJS NE  = "!=="
+operToJS LT  = "<"
+operToJS GT  = ">"
+operToJS LTE = "<="
+operToJS GTE = ">="
+operToJS AND = "&"
+operToJS OR  = "|"
+operToJS XOR = "^"
+operToJS LSH = "<<"
+operToJS RSH = ">>"
+
+bookToJS :: Book -> String
+bookToJS book = unlines $ map (\(nm, tm) -> concat [nameToJS nm, " = ", termToJS tm 0, ";"]) (M.toList book)
+
+compileJS :: Book -> String
+compileJS book =
+  let prelude = unlines [
+        "function APPLY(f, x) {",
+        "  switch (x.length) {",
+        "    case 0: return f;",
+        "    case 1: return f(x.x0);",
+        "    case 2: return f(x.x0)(x.x1);",
+        "    case 3: return f(x.x0)(x.x1)(x.x2);",
+        "    case 4: return f(x.x0)(x.x1)(x.x2)(x.x3);",
+        "    case 5: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4);",
+        "    case 6: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5);",
+        "    case 7: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5)(x.x6);",
+        "    case 8: return f(x.x0)(x.x1)(x.x2)(x.x3)(x.x4)(x.x5)(x.x6)(x.x7);",
+        "    default:",
+        "      for (let i = 0; i < x.length; i++) {",
+        "        f = f(x['x' + i]);",
+        "      }",
+        "      return f;",
+        "  }",
+        "}"]
+      bookJS  = bookToJS book
+  in concat [prelude, "\n\n", bookJS]
+

src/Kind/Equal.hs

@@ -85,7 +85,7 @@ identical a b dep = go a b dep where
     return True
   go a (Hol bNam bCtx) dep =
     return True
-  go U48 U48 dep =
+  go U32 U32 dep =
     return True
   go (Num aVal) (Num bVal) dep =
     return (aVal == bVal)

src/Kind/Parse.hs

@@ -182,7 +182,7 @@ parseMat = withSrc $ do
 parseRef = withSrc $ do
   name <- parseName
   return $ case name of
-    "U48" -> U48
+    "U32" -> U32
     _     -> Ref name
 
 parseUse = withSrc $ do

src/Kind/Reduce.hs

@@ -130,7 +130,7 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
     Use nam nf_val nf_bod
   go (Hol nam ctx) dep = Hol nam ctx
   go Set dep = Set
-  go U48 dep = U48
+  go U32 dep = U32
   go (Num val) dep = Num val
   go (Op2 opr fst snd) dep =
     let nf_fst = normal book fill lv fst dep in
@@ -205,7 +205,7 @@ bind (Use nam val bod) ctx =
   let bod' = \x -> bind (bod (Var nam 0)) ((nam, x) : ctx) in
   Use nam val' bod'
 bind Set ctx = Set
-bind U48 ctx = U48
+bind U32 ctx = U32
 bind (Num val) ctx = Num val
 bind (Op2 opr fst snd) ctx =
   let fst' = bind fst ctx in
@@ -254,7 +254,7 @@ subst lvl neo term = go term where
   go (Met uid spn)     = Met uid (map go spn)
   go (Hol nam ctx)     = Hol nam (map go ctx)
   go Set               = Set
-  go U48               = U48
+  go U32               = U32
   go (Num n)           = Num n
   go (Op2 opr fst snd) = Op2 opr (go fst) (go snd)
   go (Swi nam x z s p) = Swi nam (go x) (go z) (\k -> go (s k)) (\k -> go (p k))

src/Kind/Show.hs

@@ -69,7 +69,7 @@ termShower small term dep = case term of
         bod' = termShower small (bod (Var nam dep)) (dep + 1)
     in concat ["use " , nam' , " = " , val' , "; " , bod']
   Set -> "*"
-  U48 -> "U48"
+  U32 -> "U32"
   Num val ->
     let val' = show val
     in concat [val']

src/Kind/Type.hs

@@ -44,16 +44,16 @@ data Term
   -- Type : Type
   | Set
 
-  -- U48 Type
-  | U48
+  -- U32 Type
+  | U32
 
-  -- U48 Value
+  -- U32 Value (FIXME: this is wrong, should be Word32)
   | Num Int
 
-  -- U48 Binary Operation
+  -- U32 Binary Operation
   | Op2 Oper Term Term
 
-  -- U48 Elimination
+  -- U32 Elimination
   | Swi String Term Term (Term -> Term) (Term -> Term)
 
   -- Inspection Hole