new sonnet bad?

new_sonnet_bad.txt.hs

You're a code completion assistant.
###
-- 
module Kind.Type where

import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M

import Debug.Trace
import Data.Word (Word32)

-- Kind's AST
data Term
  -- Product: ∀(x: A) B
  = All String Term (Term -> Term)

  -- Lambda: λx f
  | Lam String (Term -> Term)

  -- Application: (fun arg)
  | App Term Term

  -- Annotation: {x: T}
  | Ann Bool Term Term

  -- Self-Type: $(x: A) B
  | Slf String Term (Term -> Term)

  -- Self-Inst: ~x
  | Ins Term

  -- Datatype: "#[i0 i1...]{ #C0 Tele0 #C1 Tele1 ... }
  | Dat [Term] [Ctr] Term

  -- Constructor: #CN { x0 x1 ... }
  | Con String [(Maybe String, Term)]

  -- Match: λ{ #C0:B0 #C1:B1 ... }
  | Mat [(String, Term)]

  -- Top-Level Reference
  | Ref String

  -- Local let-definition
  | Let String Term (Term -> Term)

  -- Local use-definition
  | Use String Term (Term -> Term)

  -- Type : Type
  | Set

  -- U32 Type
  | U32

  -- U32 Value
  | Num Word32

  -- U32 Binary Operation
  | Op2 Oper Term Term

  -- U32 Elimination (updated to use splitting lambda)
  | Swi Term Term

  -- Inspection Hole
  | Hol String [Term]

  -- Unification Metavar
  | Met Int [Term]

  -- Logging
  | Log Term Term

  -- Variable
  | Var String Int

  -- Source Location
  | Src Cod Term

  -- Text Literal (sugar)
  | Txt String

  -- List Literal (sugar)
  | Lst [Term]

  -- Nat Literal (sugar)
  | Nat Integer

-- Location: Name, Line, Column
data Loc = Loc String Int Int
data Cod = Cod Loc Loc

-- Numeric Operators
data Oper
  = ADD | SUB | MUL | DIV
  | MOD | EQ  | NE  | LT
  | GT  | LTE | GTE | AND
  | OR  | XOR | LSH | RSH

-- Telescope
data Tele
  = TRet Term
  | TExt String Term (Term -> Tele)

-- Constructor
data Ctr = Ctr String Tele

-- Book of Definitions
type Book = M.Map String Term

-- Type-Checker Outputs
data Info
  = Found String Term [Term] Int
  | Solve Int Term Int
  | Error (Maybe Cod) Term Term Term Int
  | Vague String
  | Print Term Int

-- Unification Solutions
type Fill = IM.IntMap Term

-- Checker State
data Check = Check (Maybe Cod) Term Term Int -- postponed check
data State = State Book Fill [Check] [Info] -- state type
data Res a = Done State a | Fail State -- result type
data Env a = Env (State -> Res a) -- monadic checker

-- UNCOMMENT THIS TO DEBUG THE TYPE CHECKER
-- debug a b = trace a b
debug a b = b


module Kind.CompileJS where

import Kind.Reduce
import Kind.Type
import Kind.Util

import qualified Data.Map.Strict as M
import qualified Data.IntMap.Strict as IM
import Data.List (intercalate)

import Prelude hiding (EQ, LT, GT)

nameToJS :: String -> String
nameToJS = map (\c -> if c == '/' || c == '.' || 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 (\(f, 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 ->
    termToJS (bod val) dep
  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 zer suc ->
    let zer' = termToJS zer dep
        suc' = termToJS suc dep
    in concat ["((x => x === 0 ? ", zer', " : ", suc', "(x - 1)))"]
  Txt txt ->
    let cons = \x acc -> Con "Cons" [(Nothing, x), (Nothing, acc)]
        nil  = Con "Nil" []
    in  termToJS (foldr cons nil (map (Num . fromIntegral . fromEnum) txt)) dep
  Lst lst ->
    let cons = \x acc -> Con "Cons" [(Nothing, x), (Nothing, acc)]
        nil  = Con "Nil" []
    in  termToJS (foldr cons nil lst) dep
  Nat val ->
    -- TODO: this must be compiled to (Con "Succ" ... and (Con "Zero"
    -- similar to the Txt/Lst cases. do it now:
    {:FILL_HERE:}
  Hol _ _ ->
    "null"
  Met _ _ ->
    "null"
  Log msg nxt ->
    let msg' = termToJS msg dep
        nxt' = termToJS nxt dep
    in concat ["(console.log(", msg', "), ", nxt', ")"]
  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, ";"]) (topoSortBook 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]


### TASK: complete the {:FILL_HERE:} part of the file above. Write ONLY the needed text to replace {:FILL_HERE:} by the correct completion, including correct spacing and indentation. Include the answer inside a <COMPLETION></COMPLETION> tag.