<commit_before>{-# LANGUAGE ViewPatterns
           , TupleSections
 #-}
module Spire.Canonical.Unification where
import Control.Applicative ((<*>) , (<$>))
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import Common.BwdFwd
import PatternUnify.Tm
import PatternUnify.Context
import qualified PatternUnify.Test
-- import PatternUnify.Tm hiding (Elim)
-- import qualified PatternUnify.Tm as T
import Spire.Canonical.Types
import Unbound.LocallyNameless hiding ( Spine )

----------------------------------------------------------------------

unify :: Spire.Canonical.Types.Type -> Value -> Value -> SpireM Bool
unify _T v1 v2 = do
  declareProblem _T v1 v2
  uCtx <- gets unifierCtx
  case PatternUnify.Test.unify uCtx of
    -- XXX: should report this error. What we really need is a stack
    -- of errors?
    Left _err -> return False -- throwError err
    Right uCtx' -> do modify (\r -> r { unifierCtx = uCtx' })
                      return True

----------------------------------------------------------------------

value2Tm :: Value -> SpireM Tm
value2Tm v = case v of
  VBool -> return $ C Bool
  -- Using 'C Type' here results in "Type Set does not make Set equal
  -- to Type" error.
  VType -> return $ C Set
  VPi _A _B -> Pi <$> value2Tm _A <*> mapBindM value2Tm _B
  VSg _A _B -> Sig <$> value2Tm _A <*> mapBindM value2Tm _B
  VTrue -> return $ C Tt
  VFalse -> return $ C Ff
  VPair x y -> C <$> (Pair <$> value2Tm x <*> value2Tm y)
  VLam b -> L <$> mapBindM value2Tm b
  VNeut x s -> N (nom2Head x) <$> spine2BwdElim s
  -- XXX: no support for unit type right now!
  _ -> throwError $ "Unsupported input in value2Tm: " ++ show v
  where
    nom2Head x = if isMV x
                 then M (translate x)
                 else V (translate x) Only

    elim2Elim e = case e of
      EApp v -> A <$> value2Tm v
      EProj1 -> return Hd
      EProj2 -> return Tl
      ECaseBool b x y -> If <$> mapBindM value2Tm b <*> value2Tm x <*> value2Tm y

    spine2BwdElim Id = return B0
    spine2BwdElim (Pipe s e) = (:<) <$> spine2BwdElim s <*> elim2Elim e

tm2Value :: Tm -> SpireM Value
tm2Value t = case t of
  L b -> VLam <$> mapBindM tm2Value b
  C Type -> return VType
  C (Pair x y) -> VPair <$> tm2Value x <*> tm2Value y
  C Bool -> return VBool
  C Tt -> return VTrue<commit_msg>Disable unification when --metavars flag is false (default).<commit_after>{-# LANGUAGE ViewPatterns
           , TupleSections
 #-}
module Spire.Canonical.Unification where
import Control.Applicative ((<*>) , (<$>))
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import Unbound.LocallyNameless hiding ( Spine )

import Common.BwdFwd
import PatternUnify.Tm
import PatternUnify.Context
import qualified PatternUnify.Test
-- import PatternUnify.Tm hiding (Elim)
-- import qualified PatternUnify.Tm as T
import Spire.Canonical.Types
import Spire.Options

----------------------------------------------------------------------

unify :: Spire.Canonical.Types.Type -> Value -> Value -> SpireM Bool
unify _T v1 v2 = do
  solveMetaVars <- asks (metavars . conf)
  if solveMetaVars
  then unify' _T v1 v2
  else return $ v1 == v2

unify' _T v1 v2 = do
  declareProblem _T v1 v2
  uCtx <- gets unifierCtx
  case PatternUnify.Test.unify uCtx of
    -- XXX: should report this error. What we really need is a stack
    -- of errors?
    Left _err -> throwError _err -- return False
    Right uCtx' -> do modify (\r -> r { unifierCtx = uCtx' })
                      return True

----------------------------------------------------------------------

value2Tm :: Value -> SpireM Tm
value2Tm v = case v of
  VBool -> return $ C Bool
  -- Using 'C Type' here results in "Type Set does not make Set equal
  -- to Type" error.
  -- VType -> return $ C Set
  VType -> return $ C Type
  VPi _A _B -> Pi <$> value2Tm _A <*> mapBindM value2Tm _B
  VSg _A _B -> Sig <$> value2Tm _A <*> mapBindM value2Tm _B
  VTrue -> return $ C Tt
  VFalse -> return $ C Ff
  VPair x y -> C <$> (Pair <$> value2Tm x <*> value2Tm y)
  VLam b -> L <$> mapBindM value2Tm b
  VNeut x s -> N (nom2Head x) <$> spine2BwdElim s
  -- XXX: no support for unit type right now!
  _ -> throwError $ "Unsupported input in value2Tm: " ++ show v
  where
    nom2Head x = if isMV x
                 then M (translate x)
                 else V (translate x) Only

    elim2Elim e = case e of
      EApp v -> A <$> value2Tm v
      EProj1 -> return Hd
      EProj2 -> return Tl
      ECaseBool b x y -> If <$> mapBindM value2Tm b <*> value2Tm x <*> value2Tm y

    spine2BwdElim Id = return B0
    spine2BwdElim (Pipe s e) = (:<) <$> spine2BwdElim s <*> elim2Elim e

tm2Value :: Tm -> SpireM Value
tm2Value t = case t of
  L b -> VLam <$> mapBindM tm2Value b
  C Type -> return VType
  C (Pair x y) -> VPair <$> tm2Value x <*> tm2Value y
  C Bool -> return VBool
  C Tt -> return VTrue
{'fraction_non_alphanumeric': 0.15676668707899571, 'fraction_numerical': 0.015105123494590733, 'mean_word_length': 2.1349968010236724, 'pattern_counts': {'":': 0, '<': 48, '<?xml version=': 0, '>': 98, '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': '2868475', 'n_tokens_mistral': 1710, 'n_tokens_neox': 1709, 'n_words': 590}