module U.Codebase.Term.Hashing where

import Control.Lens
import Data.Foldable qualified as Foldable
import Data.Map qualified as Map
import U.Codebase.HashTags
import U.Codebase.Reference qualified as Reference
import U.Codebase.Sqlite.HashHandle (HashMismatch (..))
import U.Codebase.Sqlite.LocalIds qualified as LocalIds
import U.Codebase.Sqlite.Queries qualified as Q
import U.Codebase.Sqlite.Symbol qualified as S
import U.Codebase.Sqlite.Term.Format qualified as S.Term
import U.Codebase.Sqlite.Term.Format qualified as TermFormat
import U.Codebase.Term qualified as C
import U.Codebase.Term qualified as C.Term
import U.Codebase.Type qualified as C.Type
import U.Core.ABT qualified as ABT
import Unison.Hash32
import Unison.Hash32 qualified as Hash32
import Unison.Hashing.V2 qualified as H2
import Unison.Hashing.V2.Convert2 qualified as H2
import Unison.Prelude
import Unison.Symbol qualified as Unison
import Unison.Var qualified as Var

verifyTermFormatHash :: ComponentHash -> TermFormat.HashTermFormat -> Maybe (HashMismatch)
verifyTermFormatHash :: ComponentHash -> HashTermFormat -> Maybe HashMismatch
verifyTermFormatHash (ComponentHash Hash
hash) (TermFormat.Term (TermFormat.LocallyIndexedComponent Vector (LocalIds' Text Hash32, Term, Type)
elements)) =
  Vector (LocalIds' Text Hash32, Term, Type)
-> [(LocalIds' Text Hash32, Term, Type)]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Vector (LocalIds' Text Hash32, Term, Type)
elements
    [(LocalIds' Text Hash32, Term, Type)]
-> ([(LocalIds' Text Hash32, Term, Type)]
    -> [(Term Symbol, Type Symbol)])
-> [(Term Symbol, Type Symbol)]
forall a b. a -> (a -> b) -> b
& ((LocalIds' Text Hash32, Term, Type) -> (Term Symbol, Type Symbol))
-> [(LocalIds' Text Hash32, Term, Type)]
-> [(Term Symbol, Type Symbol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LocalIds' Text Hash32, Term, Type) -> (Term Symbol, Type Symbol)
s2cTermWithType
    [(Term Symbol, Type Symbol)]
-> ([(Term Symbol, Type Symbol)]
    -> [((Term Symbol, Type Symbol), Id)])
-> [((Term Symbol, Type Symbol), Id)]
forall a b. a -> (a -> b) -> b
& Hash
-> [(Term Symbol, Type Symbol)]
-> [((Term Symbol, Type Symbol), Id)]
forall k. Hash -> [k] -> [(k, Id)]
Reference.component Hash
hash
    [((Term Symbol, Type Symbol), Id)]
-> ([((Term Symbol, Type Symbol), Id)]
    -> [(Id,
         (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
          Term (F' TypeRef) Symbol ()))])
-> [(Id,
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ()))]
forall a b. a -> (a -> b) -> b
& (((Term Symbol, Type Symbol), Id)
 -> (Id,
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ())))
-> [((Term Symbol, Type Symbol), Id)]
-> [(Id,
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ()))]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((Term Symbol
tm, Type Symbol
typ), Id
refId) -> (Id
refId, ((Term Symbol
-> Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol ()
forall text' termRef' typeRef' termLink' typeLink' a.
Term
  (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
mapTermV Term Symbol
tm), (Type Symbol -> Term (F' TypeRef) Symbol ()
forall r. Term (F' r) Symbol () -> Term (F' r) Symbol ()
mapTypeV Type Symbol
typ))))
    [(Id,
  (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
   Term (F' TypeRef) Symbol ()))]
-> ([(Id,
      (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
       Term (F' TypeRef) Symbol ()))]
    -> Map
         Id
         (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
          Term (F' TypeRef) Symbol ()))
-> Map
     Id
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ())
forall a b. a -> (a -> b) -> b
& [(Id,
  (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
   Term (F' TypeRef) Symbol ()))]
-> Map
     Id
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ())
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    Map
  Id
  (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
   Term (F' TypeRef) Symbol ())
-> (Map
      Id
      (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
       Term (F' TypeRef) Symbol ())
    -> Map
         Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))
-> Map
     Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ())
forall a b. a -> (a -> b) -> b
& Hash
-> (Id -> Symbol)
-> Map
     Id
     (Term (F' Text TermRef TypeRef TermLink TypeRef Symbol) Symbol (),
      Term (F' TypeRef) Symbol ())
-> Map
     Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ())
forall v extra.
Var v =>
Hash
-> (Id -> v)
-> Map Id (Term v, extra)
-> Map Id (v, HashableTerm v, extra)
C.Term.unhashComponent Hash
hash Id -> Symbol
forall v. Var v => Id -> v
Var.unnamedRef
    Map Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ())
-> (Map
      Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ())
    -> [(Id,
         (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))])
-> [(Id,
     (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))]
forall a b. a -> (a -> b) -> b
& Map Id (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ())
-> [(Id,
     (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))]
forall k a. Map k a -> [(k, a)]
Map.toList
    [(Id, (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))]
-> ([(Id,
      (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))]
    -> [(Symbol, (Term Symbol (), Type Symbol (), ()))])
-> [(Symbol, (Term Symbol (), Type Symbol (), ()))]
forall a b. a -> (a -> b) -> b
& ((Id, (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))
 -> (Symbol, (Term Symbol (), Type Symbol (), ())))
-> [(Id,
     (Symbol, HashableTerm Symbol, Term (F' TypeRef) Symbol ()))]
-> [(Symbol, (Term Symbol (), Type Symbol (), ()))]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Id
_refId, (Symbol
v, HashableTerm Symbol
trm, Term (F' TypeRef) Symbol ()
typ)) -> (Symbol
v, (HashableTerm Symbol -> Term Symbol ()
forall v. Ord v => HashableTerm v -> Term v ()
H2.v2ToH2Term HashableTerm Symbol
trm, Term (F' TypeRef) Symbol () -> Type Symbol ()
forall v. Ord v => TypeR TypeRef v -> Type v ()
H2.v2ToH2Type Term (F' TypeRef) Symbol ()
typ, ())))
    [(Symbol, (Term Symbol (), Type Symbol (), ()))]
-> ([(Symbol, (Term Symbol (), Type Symbol (), ()))]
    -> Map Symbol (Term Symbol (), Type Symbol (), ()))
-> Map Symbol (Term Symbol (), Type Symbol (), ())
forall a b. a -> (a -> b) -> b
& [(Symbol, (Term Symbol (), Type Symbol (), ()))]
-> Map Symbol (Term Symbol (), Type Symbol (), ())
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    Map Symbol (Term Symbol (), Type Symbol (), ())
-> (Map Symbol (Term Symbol (), Type Symbol (), ())
    -> Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ()))
-> Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ())
forall a b. a -> (a -> b) -> b
& Map Symbol (Term Symbol (), Type Symbol (), ())
-> Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ())
forall v a extra.
Var v =>
Map v (Term v a, Type v a, extra)
-> Map v (ReferenceId, Term v a, Type v a, extra)
H2.hashTermComponents
    Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ())
-> (Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ())
    -> Maybe HashMismatch)
-> Maybe HashMismatch
forall a b. a -> (a -> b) -> b
& ((ReferenceId, Term Symbol (), Type Symbol (), ())
 -> Maybe HashMismatch)
-> Map Symbol (ReferenceId, Term Symbol (), Type Symbol (), ())
-> Maybe HashMismatch
forall (f :: * -> *) (t :: * -> *) a b.
(Alternative f, Foldable t) =>
(a -> f b) -> t a -> f b
altMap \(H2.ReferenceId Hash
hash' Pos
_, Term Symbol ()
_trm, Type Symbol ()
_typ, ()
_extra) ->
      if Hash
hash Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
hash'
        then Maybe HashMismatch
forall a. Maybe a
Nothing
        else HashMismatch -> Maybe HashMismatch
forall a. a -> Maybe a
Just (Hash -> Hash -> HashMismatch
HashMismatch Hash
hash Hash
hash')
  where
    mapTermV ::
      ABT.Term (C.Term.F' text' termRef' typeRef' termLink' typeLink' S.Symbol) S.Symbol a ->
      ABT.Term (C.Term.F' text' termRef' typeRef' termLink' typeLink' Unison.Symbol) Unison.Symbol a
    mapTermV :: forall text' termRef' typeRef' termLink' typeLink' a.
Term
  (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
mapTermV =
      (text' -> text')
-> (termRef' -> termRef')
-> (typeRef' -> typeRef')
-> (termLink' -> termLink')
-> (typeLink' -> typeLink')
-> (Symbol -> Symbol)
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
forall text termRef typeRef termLink typeLink vt text' termRef'
       typeRef' termLink' typeLink' vt' v a.
(Ord v, Ord vt') =>
(text -> text')
-> (termRef -> termRef')
-> (typeRef -> typeRef')
-> (termLink -> termLink')
-> (typeLink -> typeLink')
-> (vt -> vt')
-> Term (F' text termRef typeRef termLink typeLink vt) v a
-> Term (F' text' termRef' typeRef' termLink' typeLink' vt') v a
C.Term.extraMap text' -> text'
forall a. a -> a
id termRef' -> termRef'
forall a. a -> a
id typeRef' -> typeRef'
forall a. a -> a
id termLink' -> termLink'
forall a. a -> a
id typeLink' -> typeLink'
forall a. a -> a
id Symbol -> Symbol
symbol2to1
        (Term
   (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
 -> Term
      (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a)
-> (Term
      (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
    -> Term
         (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a)
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (Symbol -> Symbol)
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
-> Term
     (F' text' termRef' typeRef' termLink' typeLink' Symbol) Symbol a
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
ABT.vmap Symbol -> Symbol
symbol2to1
    mapTypeV :: ABT.Term (C.Type.F' r) S.Symbol () -> ABT.Term (C.Type.F' r) Unison.Symbol ()
    mapTypeV :: forall r. Term (F' r) Symbol () -> Term (F' r) Symbol ()
mapTypeV = (Symbol -> Symbol)
-> Term (F' r) Symbol () -> Term (F' r) Symbol ()
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
ABT.vmap Symbol -> Symbol
symbol2to1
    symbol2to1 :: S.Symbol -> Unison.Symbol
    symbol2to1 :: Symbol -> Symbol
symbol2to1 (S.Symbol Pos
i Text
t) = Pos -> Type -> Symbol
Unison.Symbol Pos
i (Text -> Type
Var.User Text
t)

s2cTermWithType :: (LocalIds.LocalIds' Text Hash32, S.Term.Term, S.Term.Type) -> (C.Term S.Symbol, C.Term.Type S.Symbol)
s2cTermWithType :: (LocalIds' Text Hash32, Term, Type) -> (Term Symbol, Type Symbol)
s2cTermWithType (LocalIds' Text Hash32
ids, Term
tm, Type
tp) =
  let Identity (LocalTextId -> Text
substText, LocalDefnId -> Hash
substHash) = (Text -> Identity Text)
-> (Hash -> Identity Hash)
-> LocalIds' Text Hash
-> Identity (LocalTextId -> Text, LocalDefnId -> Hash)
forall (m :: * -> *) t d.
Monad m =>
(t -> m Text)
-> (d -> m Hash)
-> LocalIds' t d
-> m (LocalTextId -> Text, LocalDefnId -> Hash)
Q.localIdsToLookups Text -> Identity Text
forall a. a -> Identity a
Identity Hash -> Identity Hash
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Text -> Text)
-> (Hash32 -> Hash) -> LocalIds' Text Hash32 -> LocalIds' Text Hash
forall a b c d.
(a -> b) -> (c -> d) -> LocalIds' a c -> LocalIds' b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Text -> Text
forall a. a -> a
id Hash32 -> Hash
Hash32.toHash LocalIds' Text Hash32
ids)
   in ((LocalTextId -> Text)
-> (LocalDefnId -> Hash) -> Term -> Term Symbol
Q.x2cTerm LocalTextId -> Text
substText LocalDefnId -> Hash
substHash Term
tm, (LocalTextId -> Text)
-> (LocalDefnId -> Hash) -> Type -> Type Symbol
Q.x2cTType LocalTextId -> Text
substText LocalDefnId -> Hash
substHash Type
tp)