wtf new sonnet

wtf_new_sonnet.txt

You're a code completion assistant.

###

-- Type.hs:
-- 
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.API where

import Control.Exception (try)
import Control.Monad (forM, forM_, foldM)
import Data.List (stripPrefix, isSuffixOf, nub)
import Highlight (highlightError)
import Kind.Check
import Kind.CompileJS
import Kind.Env
import Kind.Parse
import Kind.Reduce
import Kind.Show
import Kind.Type
import Kind.Util
import System.Console.ANSI
import System.Directory (canonicalizePath, getCurrentDirectory, doesDirectoryExist, doesFileExist, getDirectoryContents)
import System.Environment (getArgs)
import System.Exit (exitWith, ExitCode(ExitSuccess, ExitFailure))
import System.FilePath (takeDirectory, (</>), takeFileName, dropExtension, isExtensionOf)
import System.IO (readFile)
import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M
import qualified Data.Set as S

import Debug.Trace

main :: IO ()
main = do
  args     <- getArgs
  currPath <- getCurrentDirectory
  bookPath <- findBookDir currPath
  case bookPath of
    Nothing -> do
      putStrLn "Error: No 'book' directory found in the path."
      exitWith (ExitFailure 1)
    Just bookPath -> do
      result <- case args of
        ["check"]      -> apiCheckAll bookPath
        ["check", arg] -> runCheckCommand bookPath arg
        ["run", arg]   -> runCommand bookPath arg apiNormal
        ["show", arg]  -> runCommand bookPath arg apiShow
        ["to-js", arg] -> runCommand bookPath arg apiToJS
        ["deps", arg]  -> runDeps bookPath arg
        ["rdeps", arg] -> runRDeps bookPath arg
        ["help"]       -> printHelp
        []             -> printHelp
        _              -> printHelp
      case result of
        Left err -> do
          putStrLn err
          exitWith (ExitFailure 1)
        Right _ -> exitWith ExitSuccess

printHelp :: IO (Either String ())
printHelp = do
  putStrLn "Kind usage:"
  putStrLn "  kind check             # Checks all .kind files in the current directory and subdirectories"
  putStrLn "  kind check <name|path> # Type-checks all definitions in the specified file"
  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 immediate dependencies of the specified definition"
  putStrLn "  kind rdeps <name|path> # Shows all dependencies of the specified definition recursively"
  putStrLn "  kind help              # Shows this help message"
  return $ Right ()

-- API
-- ---

-- Normalizes a term
apiNormal :: Book -> String -> IO (Either String ())
apiNormal book name = case M.lookup "main" book of
  Just term -> do
    result <- infoShow book IM.empty (Print (normal book IM.empty 2 term 0) 0)
    putStrLn result
    return $ Right ()
  Nothing -> return $ Left $ "Error: Definition 'main' not found."

-- Type-checks all terms in a file
apiCheckFile :: Book -> M.Map FilePath [String] -> FilePath -> IO (Either String ())
apiCheckFile book defs path = do
  let termsToCheck = case M.lookup path defs of
        Just names -> [(name, term) | name <- names, Just term <- [M.lookup name book]]
        Nothing    -> []
  results <- forM termsToCheck $ \(name, term) -> do
    case envRun (doCheck term) book of
      Done state value -> do
        apiPrintLogs state
        apiPrintWarn term state
        putStrLn $ "\x1b[32m✓ " ++ name ++ "\x1b[0m"
        return $ Right ()
      Fail state -> do
        apiPrintLogs state
        apiPrintWarn term state
        putStrLn $ "\x1b[31m✗ " ++ name ++ "\x1b[0m"
        return $ Left $ "Error."
  putStrLn ""
  return $ sequence_ results

apiCheckAll :: FilePath -> IO (Either String ())
apiCheckAll bookPath = do
  files <- findKindFiles bookPath
  (book, defs, _) <- foldM (\(b, d, p) f -> do
    (b', d', p') <- apiLoad bookPath b (extractName bookPath f)
    return (b', M.union d d', M.union p p')
    ) (M.empty, M.empty, M.empty) files
  results <- forM (M.toList defs) $ \(_, names) -> do
    forM names $ \name -> do
      case M.lookup name book of
        Just term -> case envRun (doCheck term) book of
          Done _ _ -> do
            putStrLn $ "\x1b[32m✓ " ++ name ++ "\x1b[0m"
            return $ Right ()
          Fail _ -> do
            putStrLn $ "\x1b[31m✗ " ++ name ++ "\x1b[0m"
            return $ Left $ "Error."
        Nothing -> return $ Left $ "Definition not found: " ++ name
  return $ sequence_ (concat results)
  where
    findKindFiles :: FilePath -> IO [FilePath]
    findKindFiles dir = do
      contents <- getDirectoryContents dir
      let properNames = filter (`notElem` [".", ".."]) contents
      paths <- forM properNames $ \name -> do
        let path = dir </> name
        isDirectory <- doesDirectoryExist path
        if isDirectory
          then findKindFiles path
          else return [path | ".kind" `isSuffixOf` path]
      return (concat paths)

-- Shows a term
apiShow :: Book -> String -> IO (Either String ())
apiShow book name = case M.lookup name book of
  Just term -> do
    putStrLn $ termShow term
    return $ Right ()
  Nothing -> return $ Left $ "Error: Definition '" ++ name ++ "' not found."

-- Compiles the whole book to JS
apiToJS :: Book -> String -> IO (Either String ())
apiToJS book name = do
  let jsCode = compileJS book
  putStrLn jsCode
  return $ Right ()

-- Prints logs from the type-checker
apiPrintLogs :: State -> IO ()
apiPrintLogs (State book fill susp logs) = do
  forM_ logs $ \log -> do
    result <- infoShow book fill log
    putStr result

-- Prints a warning if there are unsolved metas
apiPrintWarn :: Term -> State -> IO ()
apiPrintWarn term (State _ fill _ _) = do
  let metaCount = countMetas term
  let fillCount = IM.size fill
  if (metaCount > fillCount) then do
    putStrLn $ "WARNING: " ++ show (metaCount - fillCount) ++ " unsolved metas."
  else
    return ()

runDeps :: FilePath -> String -> IO (Either String ())
runDeps bookPath input = do
  let name = extractName bookPath input
  (book, _, _) <- apiLoad bookPath M.empty name
  case M.lookup name book of
    Just term -> do
      forM_ (filter (/= name) $ nub $ getDeps term) $ \dep -> putStrLn dep
      return $ Right ()
    Nothing -> return $ Left $ "Error: Definition '" ++ name ++ "' not found."

runRDeps :: FilePath -> String -> IO (Either String ())
runRDeps bookPath input = do
  let name = extractName bookPath input
  (book, _, _) <- apiLoad bookPath M.empty name
  let deps = S.toList $ S.delete name $ getAllDeps book name
  forM_ deps $ \dep -> putStrLn dep
  return $ Right ()

-- runCommand
-- ----------

runCommand :: FilePath -> String -> (Book -> String -> IO (Either String ())) -> IO (Either String ())
runCommand bookPath arg cmd = do
  let name = extractName bookPath arg
  (book, _, _) <- apiLoad bookPath M.empty name
  cmd book name

runCheckCommand :: FilePath -> String -> IO (Either String ())
runCheckCommand bookPath input = do
  let name = extractName bookPath input
  let path = bookPath </> name ++ ".kind"
  (book, defs, _) <- apiLoad bookPath M.empty name
  apiCheckFile book defs path

-- Utils
-- -----

-- Finds the directory named "book" or "monobook"
findBookDir :: FilePath -> IO (Maybe FilePath)
findBookDir dir = do
  let kindBookDir = dir </> "kindbook"
  let monoBookDir = dir </> "monobook"
  isKindBook <- doesDirectoryExist kindBookDir
  isMonoBook <- doesDirectoryExist monoBookDir
  if isKindBook
    then return $ Just kindBookDir
    else if isMonoBook
      then return $ Just monoBookDir
      else if takeDirectory dir == dir
        then return Nothing
        else findBookDir (takeDirectory dir)

-- Extracts the definition name from a file path or name
extractName :: FilePath -> String -> String
extractName bookPath = dropBookPath . dropExtension where
  dropExtension path
    | isExtensionOf "kind" path = System.FilePath.dropExtension path
    | otherwise                 = path
  dropBookPath path = maybe path id (stripPrefix (bookPath++"/") path)

-- Loads a file into a string
readSourceFile :: FilePath -> IO String
readSourceFile file = do
  result <- try (readFile file) :: IO (Either IOError String)
  case result of
    Right content -> return content
    Left _ -> do
      result2 <- try (readFile (file ++ "/_.kind2")) :: IO (Either IOError String)
      return $ either (const "Could not read source file.\n") id result2

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

-- Stringification of results
infoShow :: Book -> Fill -> Info -> IO String
infoShow book fill info = case info of
  Found nam typ ctx dep ->
    let nam' = concat ["?", nam]
        typ' = termShower True (normal book fill 0 typ dep) dep
        ctx' = contextShow book fill ctx dep
    in return $ concat ["\x1b[1mGOAL\x1b[0m ", nam', " : ", typ', "\n", ctx']
  Error src exp det bad dep -> do
    let exp' = concat ["- expected : \x1b[32m", termShower True (normal book fill 0 exp dep) dep, "\x1b[0m"]
        det' = concat ["- detected : \x1b[31m", termShower True (normal book fill 0 det dep) dep, "\x1b[0m"]
        bad' = concat ["- origin   : \x1b[2m", termShower True (normal book fill 0 bad dep) dep, "\x1b[0m"]
    (file, text) <- case src of
      Just (Cod (Loc fileName iniLine iniCol) (Loc _ endLine endCol)) -> do
        canonPath <- canonicalizePath fileName
        content   <- readSourceFile canonPath
        let highlighted = highlightError (iniLine, iniCol) (endLine, endCol) content
        -- FIXME: remove this cropping when the parse locations are fixed to exclude suffix trivia
        return (canonPath, unlines $ take 8 $ lines highlighted)
      Nothing -> return ("unknown_file", "Could not read source file.\n")
    let src' = concat ["\x1b[4m", file, "\x1b[0m\n", text]
    return $ concat ["\x1b[1mERROR:\x1b[0m\n", exp', "\n", det', "\n", bad', "\n", src']
  Solve nam val dep ->
    return $ concat ["SOLVE: _", show nam, " = ", termShower True val dep]
  Vague nam ->
    return $ concat ["VAGUE: _", nam]
  Print val dep ->
    return $ termShower True val dep

contextShow :: Book -> Fill -> [Term] -> Int -> String
contextShow book fill ctx dep = unlines $ map (\term -> "- " ++ contextShowAnn book fill term dep) ctx

contextShowAnn :: Book -> Fill -> Term -> Int -> String
contextShowAnn book fill (Ann chk val typ) dep = concat [termShower True (normal book fill 0 val dep) dep, " : ", termShower True (normal book fill 0 typ dep) dep]
contextShowAnn book fill (Src _ val)       dep = contextShowAnn book fill val dep
contextShowAnn book fill term              dep = termShower True (normal book fill 0 term dep) dep

-- Loader
-- ------

apiLoad :: FilePath -> Book -> String -> IO (Book, M.Map FilePath [String], M.Map FilePath [String])
apiLoad bookPath book name = do
  if M.member name book
    then do
      return (book, M.empty, M.empty)
    else do
      let dirPath = bookPath </> name
      isDir <- doesDirectoryExist dirPath
      if isDir
        then loadFile (dirPath </> takeFileName name ++ ".kind")
        else loadFile (bookPath </> name ++ ".kind")
  where
    loadFile filePath = do
      fileExists <- doesFileExist filePath
      if not fileExists
        then do
          return (book, M.empty, M.empty)
        else do
          code  <- readFile filePath
          book0 <- doParseBook filePath code
          let book1 = M.union book book0
          let defs  = M.keys book0
          let deps  = concatMap (getDeps . snd) (M.toList book0)
          let defs' = M.singleton filePath defs
          let deps' = M.singleton filePath deps
          foldDeps book1 defs' deps' deps filePath
    foldDeps book defs deps [] _ = do
      return (book, defs, deps)
    foldDeps book defs deps (dep:rest) originalFile = do
      (book', defs', deps') <- apiLoad bookPath book dep
      foldDeps book' (M.union defs defs') (M.union deps deps') rest originalFile

-- PROBLEM: this file has some messy code. specifically, the runCommand functions
-- should be unified as one. the types of the other functions should be updated
-- accordingly, allowing it to type-check. also, the apiCheckAll and apiCheck
-- functions have some duplicated logic that can be modularized. write below the
-- full refactored file to make it simple, modular and clean. keep the exact same
-- logic and funcionality. do not change any behavior. during your reasoning
-- process, write each function once. then, reason about whether this function is
-- still displaying the same behavior as before. there are many subtle things that
-- can go wrong, you must reason about them. remember: all functions must have the
-- EXACT SAME behavior as before. this is merely a style and code clarity refactor.

-}

-- every ApiAction will receive book, deps and deps now
type ApiAction = {:FILL_HERE:}

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