gistfile1.txt

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

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

import Debug.Trace
import Data.Word (Word64)

-- 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 ... }
  | ADT [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

  -- U64 Type
  | U64

  -- F64 Type
  | F64

  -- U64 Value
  | Num Word64

  -- F64 Value
  | Flt Double

  -- Binary Operation
  | Op2 Oper Term Term

  -- U64 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
  deriving Show

-- 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.Check
import Kind.Env
import Kind.Equal
import Kind.Reduce
import Kind.Show
import Kind.Type
import Kind.Util

import Control.Monad (forM)
import Data.List (intercalate)
import Data.Maybe (fromJust)
import Data.Word
import qualified Control.Monad.State.Lazy as ST
import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M

import Debug.Trace

import Prelude hiding (EQ, LT, GT)

-- Type
-- ----

-- Compilable Term
data CT
  = CNul
  | CLam String (CT -> CT)
  | CApp CT CT
  | CCon String [(String, CT)]
  | CMat CT [(String, [String], CT)]
  | CRef String
  | CLet String CT (CT -> CT)
  | CNum Word64
  | CFlt Double
  | COp2 Oper CT CT
  | CSwi CT CT
  | CLog CT CT
  | CVar String Int
  | CTxt String
  | CLst [CT]
  | CNat Integer

-- Transformations
-- ---------------

-- Converts a Term into a Compilable Term
-- Uses type information to:
-- - Ensure constructor fields are present
-- - Annotate Mat cases with the field names
termToCT :: Book -> Fill -> Term -> Maybe Term -> Int -> CT
termToCT book fill term typx dep = bindCT (t2ct book fill term typx dep) [] where
  t2ct book fill term typx dep = go term where
    go (Lam nam bod) =
      let bod' = \x -> t2ct book fill (bod (Var nam dep)) Nothing (dep+1)
      in CLam nam bod'
    go (App fun arg) =
      let fun' = t2ct book fill fun Nothing dep
          arg' = t2ct book fill arg Nothing dep
      in CApp fun' arg'
    go (Ann _ val typ) =
      t2ct book fill val (Just typ) dep
    go (Slf _ _ _) =
      CNul
    go (Ins val) =
      t2ct book fill val typx dep
    go (ADT _ _ _) =
      CNul
    go (Con nam arg) =
      case lookup nam (getADTCts (reduce book fill 2 (fromJust typx))) of
        Just (Ctr _ tele) ->
          let fNames = getTeleNames tele dep []
              fields = map (\ (f,t) -> (f, t2ct book fill t Nothing dep)) $ zip fNames (map snd arg)
          in CCon nam fields
        Nothing -> error $ "constructor-not-found:" ++ nam
    go (Mat cse) =
      case reduce book fill 2 (fromJust typx) of
        (All _ adt _) ->
          let adt' = reduce book fill 2 adt
              cts  = getADTCts adt'
              cses = map (\ (cnam, cbod) ->
                if cnam == "_" then
                  (cnam, [], t2ct book fill cbod Nothing dep)
                else case lookup cnam cts of
                  Just (Ctr _ tele) ->
                    let fNames = getTeleNames tele dep []
                    in (cnam, fNames, t2ct book fill cbod Nothing dep)
                  Nothing -> error $ "constructor-not-found:" ++ cnam) cse
          in CLam "x" $ \x -> CMat x cses
        otherwise -> error "match-without-type"
    go (All _ _ _) =
      CNul
    go (Ref nam) =
      CRef nam
    go (Let nam val bod) =
      let val' = t2ct book fill val Nothing dep
          bod' = \x -> t2ct book fill (bod (Var nam dep)) Nothing (dep+1)
      in CLet nam val' bod'
    go (Use nam val bod) =
      t2ct book fill (bod val) typx dep
    go Set =
      CNul
    go U64 =
      CNul
    go F64 =
      CNul
    go (Num val) =
      CNum val
    go (Flt val) =
      CFlt val
    go (Op2 opr fst snd) =
      let fst' = t2ct book fill fst Nothing dep
          snd' = t2ct book fill snd Nothing dep
      in COp2 opr fst' snd'
    go (Swi zer suc) =
      let zer' = t2ct book fill zer Nothing dep
          suc' = t2ct book fill suc Nothing dep
      in CSwi zer' suc'
    go (Txt txt) =
      CTxt txt
    go (Lst lst) =
      CLst (map (\x -> t2ct book fill x Nothing dep) lst)
    go (Nat val) =
      CNat val
    go (Hol _ _) =
      CNul
    go (Met _ _) =
      CNul
    go (Log msg nxt) =
      let msg' = t2ct book fill msg Nothing dep
          nxt' = t2ct book fill nxt Nothing dep
      in CLog msg' nxt'
    go (Var nam idx) =
      CVar nam idx
    go (Src _ val) =
      t2ct book fill val typx dep

-- Lifts shareable lambdas across branches. Example:
-- lift λx match v { #Foo{a b}: (λy λz A) #Bar: (λy λz B) ... }
--   == λx λy λz match v { #Foo{a b}: A #Bar: B ... }
lift :: CT -> CT
lift ct = bindCT (make lams body 0) [] where
  (lams, body) = pull ct 0 0 0

  pull :: CT -> Int -> Int -> Int -> (Int, CT)
  pull (CLam nam bod) dep nth 0 =
    let (lf, bod') = pull (bod (CVar ("v" ++ show nth) dep)) (dep+1) (nth+1) 0
    in (lf+1, bod')
  pull (CLam nam bod) dep nth skp =
    let (lf, bod') = pull (bod (CVar nam dep)) (dep+1) nth (skp-1)
    in (lf, CLam nam (\x -> bod'))
  pull (CMat val cse) dep nth skp | length cse > 0 =
    let rec   = flip map cse $ \ (cnam, cfds, cbod) -> pull cbod dep nth (skp + length cfds)
        lfs   = map (\(lf,_) -> lf) rec
        cnams = flip map cse $ \ (n,_,_) -> n
        cflds = flip map cse $ \ (_,f,_) -> f
        cbods = flip map rec $ \ (_,cbod) -> cbod
        warn  = if all (== head lfs) lfs
          then trace ("WARNING: inconsistent cross-branch lambda count on: " ++ showCT ct)
          else id
    in warn (head lfs, CMat val (zip3 cnams cflds cbods))
  pull (CLet nam val bod) dep nth skp =
    let (lf, bod') = pull (bod (CVar nam dep)) (dep+1) nth skp
    in (lf, CLet nam val (\x -> bod'))
  pull term dep nth s =
    (0, term)

  make :: Int -> CT -> Int -> CT
  make 0 term i = term
  make n term i = CLam ("v" ++ show i) (\x -> make (n-1) term (i+1))

-- JavaScript Codegen
-- ------------------

-- Converts a compilable term into JavaScript source
ctToJS :: Book -> Fill -> Maybe String -> CT -> Int -> ST.State Int String
ctToJS book fill var term dep = go term where
  go CNul =
    ret var "null"

  -- NEW VERSION:
  -- go (CLam nam bod) = do
    -- let uid = nameToJS nam ++ "$" ++ show dep
    -- bodyName <- fresh
    -- bodyStmt <- ctToJS book fill (Just bodyName) (bod (CVar uid dep)) (dep + 1)
    -- ret var $ concat ["(", uid, " => {", bodyStmt, "return ", bodyName, ";})" ]

  -- OLD VERSION:
  -- go tm@(Lam nam bod) = do
    -- let (names, bodyTerm, bodyType) = lams tm typx dep []
    -- bodyName <- fresh
    -- bodyStmt <- termToJS book fill (Just bodyName) bodyTerm bodyType (dep + length names)
    -- ret var $ concat ["(", intercalate " => " names, " => {", bodyStmt, "return ", bodyName, ";", "})"]
    -- where lams (Lam n b)   ty dep names = let uid = nameToJS n ++ "$" ++ show dep
                                          -- in lams (b (Var uid dep)) Nothing (dep+1) (uid : names)
          -- lams (Src x v)   ty dep names = lams v ty       dep names
          -- lams (Ann c v t) _  dep names = lams v (Just t) dep names
          -- lams tm          ty dep names = (reverse names, tm, ty)


  -- PROBLEM: the old version of the lam compiler merged many lambdas into one.
  -- the new one (port-refactor to use CT instead of Term) lost this ability.
  -- rewrite the new version of the Lam clause to work like the old one.
  -- use the EXACT SAME logic. make the code as similar as possible.

  {:FILL_HERE:}






  go (CApp fun arg) = do
    funExpr <- ctToJS book fill Nothing fun dep
    argExpr <- ctToJS book fill Nothing arg dep
    ret var $ concat ["(", funExpr, ")(", argExpr, ")"]
  go (CCon nam fields) = do
    fieldExprs <- forM fields $ \ (fname, fterm) -> do
      expr <- ctToJS book fill Nothing fterm dep
      return (fname, expr)
    let fields' = concatMap (\ (fname, expr) -> ", " ++ fname ++ ": " ++ expr) fieldExprs
    ret var $ concat ["({$: \"", nam, "\"", fields', "})"]
  go (CMat val cses) = do
    valName <- fresh
    valStmt <- ctToJS book fill (Just valName) val dep
    retName <- case var of
      Just var -> return var
      Nothing  -> fresh
    cases <- forM cses $ \ (cnam, fields, cbod) ->
      if cnam == "_" then do
        retStmt <- ctToJS book fill (Just retName) (CApp cbod (CVar valName 0)) dep
        return $ concat ["default: { " ++ retStmt, " break; }"]
      else do
        let bod = foldl CApp cbod (map (\f -> (CVar (valName++"."++f) 0)) fields)
        retStmt <- ctToJS book fill (Just retName) bod dep
        return $ concat ["case \"", cnam, "\": { ", retStmt, " break; }"]
    let switch = concat [valStmt, "switch (", valName, ".$) { ", unwords cases, " }"]
    case var of
      Just var -> return $ concat ["/*INLINE*/", switch]
      Nothing  -> ret var $ concat ["(()=>{", switch, "})()"]
  go (CRef nam) =
    ret var $ nameToJS nam
  go (CLet nam val bod) =
    case var of
      Just var -> do
        let uid = nameToJS nam ++ "$" ++ show dep
        valExpr <- ctToJS book fill (Just uid) val dep
        bodExpr <- ctToJS book fill (Just var) (bod (CVar uid dep)) (dep + 1)
        return $ concat [valExpr, bodExpr]
      Nothing -> do
        let uid = nameToJS nam ++ "$" ++ show dep
        valExpr <- ctToJS book fill (Just uid) val dep
        bodExpr <- ctToJS book fill Nothing (bod (CVar uid dep)) (dep + 1)
        return $ concat ["(() => {", valExpr, "return ", bodExpr, ";})()"]
  go (CNum val) =
    ret var $ show val
  go (CFlt val) =
    ret var $ show val
  go (COp2 opr fst snd) = do
    let opr' = operToJS opr
    fstExpr <- ctToJS book fill Nothing fst dep
    sndExpr <- ctToJS book fill Nothing snd dep
    ret var $ concat ["((", fstExpr, " ", opr', " ", sndExpr, ") >>> 0)"]
  go (CSwi zer suc) = do
    zerExpr <- ctToJS book fill Nothing zer dep
    sucExpr <- ctToJS book fill Nothing suc dep
    ret var $ concat ["((x => x === 0 ? ", zerExpr, " : ", sucExpr, "(x - 1)))"]
  go (CLog msg nxt) = do
    msgExpr <- ctToJS book fill Nothing msg dep
    nxtExpr <- ctToJS book fill Nothing nxt dep
    ret var $ concat ["(console.log(LIST_TO_JSTR(", msgExpr, ")), ", nxtExpr, ")"]
  go (CVar nam _) =
    ret var nam
  go (CTxt txt) =
    ret var $ "JSTR_TO_LIST(`" ++ txt ++ "`)"
  go (CLst lst) =
    let cons = \x acc -> CCon "Cons" [("head", x), ("tail", acc)]
        nil  = CCon "Nil" []
    in  ctToJS book fill var (foldr cons nil lst) dep
  go (CNat val) =
    let succ = \x -> CCon "Succ" [("pred", x)]
        zero = CCon "Zero" []
    in  ctToJS book fill var (foldr (\_ acc -> succ acc) zero [1..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 = ">>"

nameToJS :: String -> String
nameToJS x = "$" ++ map (\c -> if c == '/' || c == '.' || c == '-' || c == '#' then '$' else c) x

fresh :: ST.State Int String
fresh = do
  n <- ST.get
  ST.put (n + 1)
  return $ "$x" ++ show n

-- Assigns an expression to a name, or return it directly
ret :: Maybe String -> String -> ST.State Int String
ret (Just name) expr = return $ "var " ++ name ++ " = " ++ expr ++ ";"
ret Nothing     expr = return $ expr

prelude :: String
prelude = unlines [
  "function LIST_TO_JSTR(list) {",
  "  try {",
  "    let result = '';",
  "    let current = list;",
  "    while (current.$ === 'Cons') {",
  "      result += String.fromCodePoint(current.head);",
  "      current = current.tail;",
  "    }",
  "    if (current.$ === 'Nil') {",
  "      return result;",
  "    }",
  "  } catch (e) {}",
  "  return list;",
  "}",
  "",
  "function JSTR_TO_LIST(str) {",
  "  let list = {$: 'Nil'};",
  "  for (let i = str.length - 1; i >= 0; i--) {",
  "    list = {$: 'Cons', head: str.charCodeAt(i), tail: list};",
  "  }",
  "  return list;",
  "}"
  ]

compileJS :: Book -> String
compileJS book = prelude ++ "\n\n" ++ concatMap compileDef (topoSortBook book) where
  compileDef (name, term) =
    case envRun (doAnnotate term) book of
      Done _ (term, fill) ->
        let uid = nameToJS name
            ct0 = termToCT book fill (bind term []) Nothing 0
            ct1 = lift ct0
            def = ST.evalState (ctToJS book fill (Just uid) ct1 0) 0
            dbg = trace ("ct0 = " ++ showCT ct0 ++ "\nct1 = " ++ showCT ct1)
        in dbg $ def ++ "\n\n"
      Fail _ ->
        error $ "COMPILATION_ERROR: " ++ name ++ " isn't well-typed."

-- Utils
-- -----

bindCT :: CT -> [(String,CT)] -> CT
bindCT CNul ctx = CNul
bindCT (CLam nam bod) ctx =
  let bod' = \x -> bindCT (bod (CVar nam 0)) ((nam, x) : ctx) in
  CLam nam bod'
bindCT (CApp fun arg) ctx =
  let fun' = bindCT fun ctx in
  let arg' = bindCT arg ctx in
  CApp fun' arg'
bindCT (CCon nam arg) ctx =
  let arg' = map (\(f, x) -> (f, bindCT x ctx)) arg in
  CCon nam arg'
bindCT (CMat val cse) ctx =
  let val' = bindCT val ctx in
  let cse' = map (\(cn,fs,cb) -> (cn, fs, bindCT cb ctx)) cse in
  CMat val' cse'
bindCT (CRef nam) ctx =
  case lookup nam ctx of
    Just x  -> x
    Nothing -> CRef nam
bindCT (CLet nam val bod) ctx =
  let val' = bindCT val ctx in
  let bod' = \x -> bindCT (bod (CVar nam 0)) ((nam, x) : ctx) in
  CLet nam val' bod'
bindCT (CNum val) ctx = CNum val
bindCT (CFlt val) ctx = CFlt val
bindCT (COp2 opr fst snd) ctx =
  let fst' = bindCT fst ctx in
  let snd' = bindCT snd ctx in
  COp2 opr fst' snd'
bindCT (CSwi zer suc) ctx =
  let zer' = bindCT zer ctx in
  let suc' = bindCT suc ctx in
  CSwi zer' suc'
bindCT (CLog msg nxt) ctx =
  let msg' = bindCT msg ctx in
  let nxt' = bindCT nxt ctx in
  CLog msg' nxt'
bindCT (CVar nam idx) ctx =
  case lookup nam ctx of
    Just x  -> x
    Nothing -> CVar nam idx
bindCT (CTxt txt) ctx = CTxt txt
bindCT (CLst lst) ctx =
  let lst' = map (\x -> bindCT x ctx) lst in
  CLst lst'
bindCT (CNat val) ctx = CNat val

-- Stringification
-- ---------------

-- TODO: implement a showCT :: CT -> String function
showCT :: CT -> String
showCT CNul               = "*"
showCT (CLam nam bod)     = "λ" ++ nam ++ " " ++ showCT (bod (CVar nam 0))
showCT (CApp fun arg)     = "(" ++ showCT fun ++ " " ++ showCT arg ++ ")"
showCT (CCon nam fields)  = "#" ++ nam ++ "{" ++ concatMap (\(f,t) -> f ++ ":" ++ showCT t ++ " ") fields ++ "}"
showCT (CMat val cses)    = "match " ++ showCT val ++ " {" ++ concatMap (\(cn,fs,cb) -> "#" ++ cn ++ ":" ++ showCT cb ++ " ") cses ++ "}"
showCT (CRef nam)         = nam
showCT (CLet nam val bod) = "let " ++ nam ++ " = " ++ showCT val ++ "; " ++ showCT (bod (CVar nam 0))
showCT (CNum val)         = show val
showCT (CFlt val)         = show val
showCT (COp2 opr fst snd) = "(<op> " ++ showCT fst ++ " " ++ showCT snd ++ ")"
showCT (CSwi zer suc)     = "switch(" ++ showCT zer ++ "," ++ showCT suc ++ ")"
showCT (CLog msg nxt)     = "log(" ++ showCT msg ++ "," ++ showCT nxt ++ ")"
showCT (CVar nam _)       = nam
showCT (CTxt txt)         = show txt
showCT (CLst lst)         = "[" ++ unwords (map showCT lst) ++ "]"
showCT (CNat val)         = show val

-- Tests
-- -----

-- data A = #Foo{x0 x1} | #Bar
-- data B = #T | #F

-- test0 = λx match x {
--   #Foo: λx0 λx1 λy match y {
--     #Foo: λy0 λy1 λz λw 10
--     #Bar: λz λw 20
--   }
--   #Bar: λy match y {
--     #Foo: λy0 λy1 λz λw 30
--     #Bar: λz λw 40
--   }
-- }
test0 :: CT
test0 = CLam "x" $ \x -> CMat x [
    ("Foo", ["x0", "x1"], CLam "x0" $ \x0 -> CLam "x1" $ \x1 -> CLam "y" $ \y -> CMat y [
      ("Foo", ["y0", "y1"], CLam "y0" $ \y0 -> CLam "y1" $ \y1 -> CLam "z" $ \z -> CLam "w" $ \w -> CNum 10),
      ("Bar", [], CLam "z" $ \z -> CLam "w" $ \w -> CNum 20)
    ]),
    ("Bar", [], CLam "y" $ \y -> CMat y [
      ("Foo", ["y0", "y1"], CLam "y0" $ \y0 -> CLam "y1" $ \y1 -> CLam "z" $ \z -> CLam "w" $ \w -> CNum 30),
      ("Bar", [], CLam "z" $ \z -> CLam "w" $ \w -> CNum 40)
    ])
  ]

-- test1 = λx match x {
--   #Foo: λx0 match x0 {
--     #T: λx1 λy match y {
--       #Foo: λy0 λy1 λz λw 10
--       #Bar: λz λw 20
--     }
--     #F: λx1 λy λz λw 15
--   }
--   #Bar: λy match y {
--     #Foo: λy0 λy1 λz λw 30
--     #Bar: λz λw 40
--   }
-- }
test1 :: CT
test1 = CLam "x" $ \x -> CMat x [
    ("Foo", ["x0"], CLam "x0" $ \x0 -> CMat x0 [
      ("T", ["x1"], CLam "x1" $ \x1 -> CLam "y" $ \y -> CMat y [
        ("Foo", ["y0", "y1"], CLam "y0" $ \y0 -> CLam "y1" $ \y1 -> CLam "z" $ \z -> CLam "w" $ \w -> CNum 10),
        ("Bar", [], CLam "z" $ \z -> CLam "w" $ \w -> CNum 20)
      ]),
      ("F", ["x1"], CLam "x1" $ \x1 -> CLam "y" $ \y -> CLam "z" $ \z -> CLam "w" $ \w -> CNum 15)
    ]),
    ("Bar", [], CLam "y" $ \y -> CMat y [
      ("Foo", ["y0", "y1"], CLam "y0" $ \y0 -> CLam "y1" $ \y1 -> CLam "z" $ \z -> CLam "w" $ \w -> CNum 30),
      ("Bar", [], CLam "z" $ \z -> CLam "w" $ \w -> CNum 40)
    ])
  ]

ctest :: IO ()
ctest = do
  putStrLn $ showCT test1
  putStrLn $ showCT $ lift test1



























### 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.