-- |
-- Module      :  Cryptol.TypeCheck.Unify
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards, ViewPatterns #-}
{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-}
{-# LANGUAGE BlockArguments, OverloadedStrings #-}
module Cryptol.TypeCheck.Unify where

import Control.DeepSeq(NFData)
import GHC.Generics(Generic)

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.Utils.RecordMap
import Cryptol.Utils.Ident(Ident)
import Cryptol.ModuleSystem.Name(nameIdent)

import Cryptol.TypeCheck.PP
import Control.Monad.Writer (Writer, writer, runWriter)
import qualified Data.Set as Set

import Prelude ()
import Prelude.Compat

-- | The most general unifier is a substitution and a set of constraints
-- on bound variables.
type MGU = (Subst,[Prop])

type Result a = Writer [(Path,UnificationError)] a

runResult :: Result a -> (a, [(Path,UnificationError)])
runResult :: Result a -> (a, [(Path, UnificationError)])
runResult = Result a -> (a, [(Path, UnificationError)])
forall w a. Writer w a -> (a, w)
runWriter

data UnificationError
  = UniTypeMismatch Type Type
  | UniKindMismatch Kind Kind
  | UniTypeLenMismatch Int Int
  | UniRecursive TVar Type
  | UniNonPolyDepends TVar [TParam]
  | UniNonPoly TVar Type

uniError :: Path -> UnificationError -> Result MGU
uniError :: Path -> UnificationError -> Result MGU
uniError Path
p UnificationError
e = (MGU, [(Path, UnificationError)]) -> Result MGU
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer (MGU
emptyMGU, [(Path
p,UnificationError
e)])


newtype Path = Path [PathElement]
  deriving (Int -> Path -> ShowS
[Path] -> ShowS
Path -> String
(Int -> Path -> ShowS)
-> (Path -> String) -> ([Path] -> ShowS) -> Show Path
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Path] -> ShowS
$cshowList :: [Path] -> ShowS
show :: Path -> String
$cshow :: Path -> String
showsPrec :: Int -> Path -> ShowS
$cshowsPrec :: Int -> Path -> ShowS
Show,(forall x. Path -> Rep Path x)
-> (forall x. Rep Path x -> Path) -> Generic Path
forall x. Rep Path x -> Path
forall x. Path -> Rep Path x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Path x -> Path
$cfrom :: forall x. Path -> Rep Path x
Generic,Path -> ()
(Path -> ()) -> NFData Path
forall a. (a -> ()) -> NFData a
rnf :: Path -> ()
$crnf :: Path -> ()
NFData)

data PathElement =
    TConArg     TC      Int
  | TNewtypeArg Newtype Int
  | TRecArg     Ident
  deriving (Int -> PathElement -> ShowS
[PathElement] -> ShowS
PathElement -> String
(Int -> PathElement -> ShowS)
-> (PathElement -> String)
-> ([PathElement] -> ShowS)
-> Show PathElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PathElement] -> ShowS
$cshowList :: [PathElement] -> ShowS
show :: PathElement -> String
$cshow :: PathElement -> String
showsPrec :: Int -> PathElement -> ShowS
$cshowsPrec :: Int -> PathElement -> ShowS
Show,(forall x. PathElement -> Rep PathElement x)
-> (forall x. Rep PathElement x -> PathElement)
-> Generic PathElement
forall x. Rep PathElement x -> PathElement
forall x. PathElement -> Rep PathElement x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PathElement x -> PathElement
$cfrom :: forall x. PathElement -> Rep PathElement x
Generic,PathElement -> ()
(PathElement -> ()) -> NFData PathElement
forall a. (a -> ()) -> NFData a
rnf :: PathElement -> ()
$crnf :: PathElement -> ()
NFData)

rootPath :: Path
rootPath :: Path
rootPath = [PathElement] -> Path
Path []

isRootPath :: Path -> Bool
isRootPath :: Path -> Bool
isRootPath (Path [PathElement]
xs) = [PathElement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PathElement]
xs

extPath :: Path -> PathElement -> Path
extPath :: Path -> PathElement -> Path
extPath (Path [PathElement]
xs) PathElement
x = [PathElement] -> Path
Path (PathElement
x PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
: [PathElement]
xs)


emptyMGU :: MGU
emptyMGU :: MGU
emptyMGU = (Subst
emptySubst, [])

doMGU :: Type -> Type -> Result MGU
doMGU :: Prop -> Prop -> Result MGU
doMGU Prop
t1 Prop
t2 = Path -> Prop -> Prop -> Result MGU
mgu Path
rootPath Prop
t1 Prop
t2

mgu :: Path -> Type -> Type -> Result MGU

mgu :: Path -> Prop -> Prop -> Result MGU
mgu Path
_ (TUser Name
c1 [Prop]
ts1 Prop
_) (TUser Name
c2 [Prop]
ts2 Prop
_)
  | Name
c1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
c2 Bool -> Bool -> Bool
&& [Prop]
ts1 [Prop] -> [Prop] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prop]
ts2  = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

mgu Path
p (TVar TVar
x) Prop
t     = Path -> TVar -> Prop -> Result MGU
bindVar Path
p TVar
x Prop
t
mgu Path
p Prop
t (TVar TVar
x)     = Path -> TVar -> Prop -> Result MGU
bindVar Path
p TVar
x Prop
t

mgu Path
p (TUser Name
_ [Prop]
_ Prop
t1) Prop
t2 = Path -> Prop -> Prop -> Result MGU
mgu Path
p Prop
t1 Prop
t2
mgu Path
p Prop
t1 (TUser Name
_ [Prop]
_ Prop
t2) = Path -> Prop -> Prop -> Result MGU
mgu Path
p Prop
t1 Prop
t2

mgu Path
p (TCon (TC TC
tc1) [Prop]
ts1) (TCon (TC TC
tc2) [Prop]
ts2)
  | TC
tc1 TC -> TC -> Bool
forall a. Eq a => a -> a -> Bool
== TC
tc2 =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (TC -> Int -> PathElement
TConArg TC
tc1 Int
i) | Int
i <- [ Int
0 .. ] ]
    in Path -> [Path] -> [Prop] -> [Prop] -> Result MGU
mguMany Path
p [Path]
paths [Prop]
ts1 [Prop]
ts2

mgu Path
_ (TCon (TF TFun
f1) [Prop]
ts1) (TCon (TF TFun
f2) [Prop]
ts2)
  | TFun
f1 TFun -> TFun -> Bool
forall a. Eq a => a -> a -> Bool
== TFun
f2 Bool -> Bool -> Bool
&& [Prop]
ts1 [Prop] -> [Prop] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prop]
ts2  = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

-- XXX: here we loose the information about where the constarint came from
mgu Path
_ Prop
t1 Prop
t2
  | TCon (TF TFun
_) [Prop]
_ <- Prop
t1, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Prop
t1 Prop -> Prop -> Prop
=#= Prop
t2])
  | TCon (TF TFun
_) [Prop]
_ <- Prop
t2, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Prop
t1 Prop -> Prop -> Prop
=#= Prop
t2])
  where
  k1 :: Kind
k1 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t1
  k2 :: Kind
k2 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t2

  isNum :: Bool
isNum = Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum

mgu Path
p (TRec RecordMap Ident Prop
fs1) (TRec RecordMap Ident Prop
fs2)
  | RecordMap Ident Prop -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Prop
fs1 Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Prop -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Prop
fs2 =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (Ident -> PathElement
TRecArg Ident
i) | (Ident
i,Prop
_) <- RecordMap Ident Prop -> [(Ident, Prop)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident Prop
fs1 ]
    in Path -> [Path] -> [Prop] -> [Prop] -> Result MGU
mguMany Path
p [Path]
paths (RecordMap Ident Prop -> [Prop]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Prop
fs1) (RecordMap Ident Prop -> [Prop]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Prop
fs2)

mgu Path
p (TNewtype Newtype
ntx [Prop]
xs) (TNewtype Newtype
nty [Prop]
ys)
  | Newtype
ntx Newtype -> Newtype -> Bool
forall a. Eq a => a -> a -> Bool
== Newtype
nty =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (Newtype -> Int -> PathElement
TNewtypeArg Newtype
ntx Int
i) | Int
i <- [ Int
0 .. ] ]
    in Path -> [Path] -> [Prop] -> [Prop] -> Result MGU
mguMany Path
p [Path]
paths [Prop]
xs [Prop]
ys

mgu Path
p Prop
t1 Prop
t2
  | Bool -> Bool
not (Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2)  = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
  | Bool
otherwise       = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> UnificationError
UniTypeMismatch Prop
t1 Prop
t2
  where
  k1 :: Kind
k1 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t1
  k2 :: Kind
k2 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t2


-- XXX: could pass the path to the lists themselvs
mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany :: Path -> [Path] -> [Prop] -> [Prop] -> Result MGU
mguMany Path
_ [Path]
_ [] [] = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
mguMany Path
p (Path
p1:[Path]
ps) (Prop
t1 : [Prop]
ts1) (Prop
t2 : [Prop]
ts2) =
  do (Subst
su1,[Prop]
ps1) <- Path -> Prop -> Prop -> Result MGU
mgu Path
p1 Prop
t1 Prop
t2
     (Subst
su2,[Prop]
ps2) <- Path -> [Path] -> [Prop] -> [Prop] -> Result MGU
mguMany Path
p [Path]
ps (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Prop]
ts1) (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Prop]
ts2)
     MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Prop]
ps1 [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps2)
mguMany Path
p [Path]
_ [Prop]
t1 [Prop]
t2 = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Int -> Int -> UnificationError
UniTypeLenMismatch ([Prop] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
t1) ([Prop] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
t2)
-- XXX: I think by this point the types should have been kind checked,
-- so there should be no mismatches with the lengths...


bindVar :: Path -> TVar -> Type -> Result MGU

bindVar :: Path -> TVar -> Prop -> Result MGU
bindVar Path
_ TVar
x (Prop -> Prop
tNoUser -> TVar TVar
y)
  | TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y                      = MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

bindVar Path
p v :: TVar
v@(TVBound {})
          (Prop -> Prop
tNoUser -> TVar v1 :: TVar
v1@(TVFree {})) = Path -> TVar -> Prop -> Result MGU
bindVar Path
p TVar
v1 (TVar -> Prop
TVar TVar
v)

bindVar Path
p v :: TVar
v@(TVBound {}) Prop
t
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t = if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum
                       then MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Prop
TVar TVar
v Prop -> Prop -> Prop
=#= Prop
t])
                       else Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Prop -> UnificationError
UniNonPoly TVar
v Prop
t
  | Bool
otherwise     = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k (Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t)
  where k :: Kind
k = TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
v

bindVar Path
_ x :: TVar
x@(TVFree Int
_ Kind
xk Set TParam
xscope TVarInfo
_) (Prop -> Prop
tNoUser -> TVar y :: TVar
y@(TVFree Int
_ Kind
yk Set TParam
yscope TVarInfo
_))
  | Set TParam
xscope Set TParam -> Set TParam -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isProperSubsetOf` Set TParam
yscope, Kind
xk Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
yk =
    MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar -> Prop -> Subst
uncheckedSingleSubst TVar
y (TVar -> Prop
TVar TVar
x), [])
    -- In this case, we can add the reverse binding y ~> x to the
    -- substitution, but the instantiation x ~> y would be forbidden
    -- because it would allow y to escape from its scope.

bindVar Path
p TVar
x Prop
t =
  case TVar -> Prop -> Either SubstError Subst
singleSubst TVar
x Prop
t of
    Left SubstError
SubstRecursive
      | TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KType -> Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Prop -> UnificationError
UniRecursive TVar
x Prop
t
      | Bool
otherwise -> MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Prop
TVar TVar
x Prop -> Prop -> Prop
=#= Prop
t])
    Left (SubstEscaped [TParam]
tps) ->
      Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> [TParam] -> UnificationError
UniNonPolyDepends TVar
x [TParam]
tps
    Left (SubstKindMismatch Kind
k1 Kind
k2) ->
      Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
    Right Subst
su ->
      MGU -> Result MGU
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su, [])


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

ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
el Int
prec Int -> Doc
k =
  case PathElement
el of
    TRecArg Ident
l -> Doc -> Doc
braces (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
0 Doc -> Doc -> Doc
<.> Doc
comma Doc -> Doc -> Doc
<+> Doc
"…")

    TConArg TC
tc Int
n ->
      case TC
tc of

       TC
TCSeq -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4)
                if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Doc -> Doc
brackets (Int -> Doc
k Int
0) Doc -> Doc -> Doc
<+> Doc
"_"
                          else Doc -> Doc
brackets Doc
"_" Doc -> Doc -> Doc
<+> (Int -> Doc
k Int
4)

       TC
TCFun -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)
                if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Int -> Doc
k Int
2 Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Doc
"_"
                          else Doc
"_" Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
1

       TCTuple Int
i  -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
0] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
          where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
                after :: [Doc]
after  = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"

       TC
_ -> Int -> Doc -> Int -> Doc
justPrefix (Kind -> Int
forall p. Num p => Kind -> p
kindArity (TC -> Kind
forall t. HasKind t => t -> Kind
kindOf TC
tc)) (TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc) Int
n

    TNewtypeArg Newtype
nt Int
n ->
      Int -> Doc -> Int -> Doc
justPrefix ([TParam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Newtype -> [TParam]
ntParams Newtype
nt)) (Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent (Newtype -> Name
ntName Newtype
nt))) Int
n

  where
  justPrefix :: Int -> Doc -> Int -> Doc
justPrefix Int
arity Doc
fun Int
n =
    Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (Doc
fun Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
5] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
    where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
          after :: [Doc]
after  = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"

  kindArity :: Kind -> p
kindArity Kind
ki =
    case Kind
ki of
      Kind
_ :-> Kind
k1 -> p
1 p -> p -> p
forall a. Num a => a -> a -> a
+ Kind -> p
kindArity Kind
k1
      Kind
_        -> p
0

instance PP Path where
  ppPrec :: Int -> Path -> Doc
ppPrec Int
prec0 (Path [PathElement]
ps0) = [PathElement] -> Int -> Doc
go ([PathElement] -> [PathElement]
forall a. [a] -> [a]
reverse [PathElement]
ps0) Int
prec0
    where
    go :: [PathElement] -> Int -> Doc
go [PathElement]
ps Int
prec =
      case [PathElement]
ps of
        []       -> Doc
"ERROR"
        PathElement
p : [PathElement]
more -> PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
p Int
prec ([PathElement] -> Int -> Doc
go [PathElement]
more)