packages feed

zwirn-0.2.2.0: src/zwirn-lang/Zwirn/Language/LSP/Diagnostics.hs

module Zwirn.Language.LSP.Diagnostics where

import Data.Functor (void)
import qualified Data.Text as T
import Zwirn.Language.Compiler
import Zwirn.Language.Location
import Zwirn.Language.Simple (simplify)
import Zwirn.Language.Syntax

diagnoseCI :: T.Text -> CI ()
diagnoseCI input = do
  blocks <- runBlocks 0 input
  as <- concat <$> catchMany (map parseBlock blocks)
  -- debug' $ T.pack $ show blocks
  void $ catchMany $ map typeCheckAction as

validateCode :: Environment -> T.Text -> IO (Maybe ErrorType)
validateCode env input = do
  out <- runCI env (diagnoseCI input)
  case out of
    Left (CIError err _) -> return $ Just err
    Right _ -> return Nothing

runTypeCheckTerm :: LocTerm -> CI ()
runTypeCheckTerm t = do
  (t', _) <- macroCI t
  s <- runSimplify t'
  rot <- runRotate s
  void $ runTypeCheck rot

typeCheckAction :: Syntax -> CI ()
typeCheckAction (Exec t) = runTypeCheckTerm t
typeCheckAction (Def (Located p (Definition _ vs t))) = do
  (t', _) <- macroCI t
  let st = Located p (simplify $ TLambda vs t')
  rot <- runRotate st
  void $ runTypeCheck rot
typeCheckAction (DynDef (Located _ (DynamicDefinition _ t))) = runTypeCheckTerm t
typeCheckAction (MacroDef (Located _ (MacroDefinition _ t))) = runTypeCheckTerm t
typeCheckAction (Command (Located _ (ShowCommand t))) = runTypeCheckTerm t
typeCheckAction (Command (Located _ (TypeCommand t))) = runTypeCheckTerm t
typeCheckAction (Command _) = return ()