<commit_before>module Uroboro.Checker where

import Control.Monad (foldM)
import Data.List (find, intercalate, (\\))

import Uroboro.Tree

data PTSig = PTSig Identifier [Type] Type deriving (Eq, Show)

data Program = Program {
      typeNames    :: [Type]  -- Cache types from constructors and destructors.
    , constructors :: [PTCon]
    , destructors  :: [PTDes]
    , functions    :: [PTSig] -- Always update functions and rules together.
    , rules        :: Rules
    } deriving (Eq, Show)

emptyProgram :: Program
emptyProgram = Program [] [] [] [] []

type Context = [(Identifier, Type)]

inferPExp :: Program -> Context -> PExp -> Either String TExp
inferPExp _ context (PVar name) = case lookup name context of
    Nothing  -> Left "Unbound Variable"
    Just typ -> Right (TVar typ name)
inferPExp p _ (PApp name _) = Left "TODO"
inferPExp _ _ (PDes _ _ _) = Left "TODO"

-- |Fold over type definitions.
checkPT :: Program -> PT -> Either String Program
checkPT prog@(Program names cons _ _ _) (PTPos name cons')
    | name `elem` names  = Left "Shadowed Definition"
    | any mismatch cons' = Left "Definition Mismatch"
    | any missing cons'  = Left "Missing Definition"
    | otherwise          = Right prog {
          typeNames = (name:names)
        , constructors = cons ++ cons'
        }
  where
    mismatch (PTCon returnType _ _) = returnType /= name
    missing (PTCon _ _ args)        = args \\ (name:names) /= []
checkPT prog@(Program names _ des _ _) (PTNeg name des')
    | name `elem` names = Left "Shadowed Definition"
    | any mismatch des' = Left "Definition Mismatch"
    | any missing des'  = Left "Missing Definition"
    | otherwise         = Right prog {
          typeNames = (name:names)
        , destructors = des ++ des'
        }
  where
    mismatch (PTDes _ _ _ innerType) = innerType /= name
    missing (PTDes _ _ args _)       = args \\ (name:names) /= []
checkPT prog@(Program names _ _ funs rules) (PTFun name args t rules')
    | any clash rules     = Left "Shadowed Definition"
  where
    clash (name', _) = name' == name

-- |Turn parser output into interpreter input.
typecheck :: [PT] -> Either String Rules
typecheck defs = foldM checkPT emptyProgram defs >>= return . rules

-- |Infer a term's type
expInfer :: [PT] -> Context -> PExp -> Either String TExp
expInfer _ vars (PVar name) = case lookup name vars of
    Just t  -> return (TVar t name)
    Nothing -> Left $ "Unknown Variable: " ++ name ++ " isn't bound"
expInfer defs vars (PApp name args) = Left "TODO"
expInfer defs vars (PDes name args inner) = do
    fromType <- expInfer defs vars inner
    Left "TODO"

-- |Typecheck a term
exp :: [PT] -> Context -> PExp -> Type -> Either String TExp
exp defs vars (PVar name) returnType = Left "TODO"
exp defs vars (PApp name args) returnType = Left "TODO"
exp defs vars (PDes name args inner) returnType = Left "TODO"
<commit_msg>Infer term type<commit_after>module Uroboro.Checker where

import Control.Monad (foldM, zipWithM)
import Data.List (find, intercalate, (\\))

import Uroboro.Tree

type PTSig = (Identifier, ([Type], Type))

data Program = Program {
      typeNames    :: [Type]  -- Cache types from constructors and destructors.
    , constructors :: [PTCon]
    , destructors  :: [PTDes]
    , functions    :: [PTSig] -- Always update functions and rules together.
    , rules        :: Rules
    } deriving (Eq, Show)

emptyProgram :: Program
emptyProgram = Program [] [] [] [] []

type Context = [(Identifier, Type)]

texpReturnType :: TExp -> Type
texpReturnType (TVar t _) = t
texpReturnType (TApp t _ _) = t
texpReturnType (TCon t _ _) = t
texpReturnType (TDes t _ _ _) = t

-- |Typecheck a term
checkPExp :: Program -> Context -> PExp -> Type -> Either String TExp
checkPExp p c e t = Left "TODO"

-- |Infer a term's type
inferPExp :: Program -> Context -> PExp -> Either String TExp
inferPExp _ context (PVar name) = case lookup name context of
    Nothing  -> Left "Unbound Variable"
    Just typ -> Right (TVar typ name)
inferPExp p c (PApp name args) = case lookup name (functions p) of  -- TODO catch ambiguous
    Just (argTypes, returnType) ->
        zipWithM (checkPExp p c) args argTypes >>= return . TApp returnType name
    Nothing -> case find match (constructors p) of
        Just (PTCon returnType _ argTypes) ->
            zipWithM (checkPExp p c) args argTypes >>= return . TCon returnType name
        Nothing -> Left "Missing Definition"
  where
    match (PTCon _ n _) = n == name
inferPExp p c (PDes name args inner) = do
    tinner <- inferPExp p c inner
    (argTypes, returnType) <- nu p (texpReturnType tinner) name
    targs <- zipWithM (checkPExp p c) args argTypes
    return $ TDes returnType name targs tinner
  where
    -- |Look up signature of named destructor for type
    nu :: Program -> Type -> Identifier -> Either String ([Type], Type)
    nu p innerType name = case find match (destructors p) of
        Just (PTDes returnType _ argTypes _) -> return (argTypes, returnType)
        Nothing -> Left "Missing Definition"
      where
        match (PTDes _ n _ t) = n == name && t == innerType

-- |Fold over type definitions.
checkPT :: Program -> PT -> Either String Program
checkPT prog@(Program names cons _ _ _) (PTPos name cons')
    | name `elem` names  = Left "Shadowed Definition"
    | any mismatch cons' = Left "Definition Mismatch"
    | any missing cons'  = Left "Missing Definition"
    | otherwise          = Right prog {
          typeNames = (name:names)
        , constructors = cons ++ cons'
        }
  where
    mismatch (PTCon returnType _ _) = returnType /= name
    missing (PTCon _ _ args)        = args \\ (name:names) /= []
checkPT prog@(Program names _ des _ _) (PTNeg name des')
    | name `elem` names = Left "Shadowed Definition"
    | any mismatch des' = Left "Definition Mismatch"
    | any missing des'  = Left "Missing Definition"
    | otherwise         = Right prog {
          typeNames = (name:names)
        , destructors = des ++ des'
        }
  where
    mismatch (PTDes _ _ _ innerType) = innerType /= name
    missing (PTDes _ _ args _)       = args \\ (name:names) /= []
checkPT prog@(Program names _ _ funs rules) (PTFun name args t rules')
    | any clash rules     = Left "Shadowed Definition"
  where
    clash (name', _) = name' == name

-- |Turn parser output into interpreter input.
typecheck :: [PT] -> Either String Rules
typecheck defs = foldM checkPT emptyProgram defs >>= return . rules

{'fraction_non_alphanumeric': 0.10929046220435926, 'fraction_numerical': 0.0, 'mean_word_length': 2.8238770685579198, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 50, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6163931', 'n_tokens_mistral': 1999, 'n_tokens_neox': 1959, 'n_words': 725}