module Unison.DataDeclaration.Dependencies
  ( -- Too many variants of decl dependencies. Read carefully to choose the right one.
    DD.declTypeDependencies,
    DD.typeDependencies,
    DD.labeledTypeDependencies,
    DD.labeledDeclTypeDependencies,
    DD.labeledDeclDependenciesIncludingSelf,
    labeledDeclDependenciesIncludingSelfAndFieldAccessors,
    hashFieldAccessors,
  )
where

import Control.Lens
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Set.Lens (setOf)
import Unison.DataDeclaration qualified as DD
import Unison.DataDeclaration.Records (generateRecordAccessors)
import Unison.Hashing.V2.Convert qualified as Hashing
import Unison.LabeledDependency qualified as LD
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.PrettyPrintEnv qualified as PPE
import Unison.Reference (TermReferenceId, TypeReference)
import Unison.Referent (Referent)
import Unison.Referent qualified as Referent
import Unison.Result qualified as Result
import Unison.Syntax.Var qualified as Var (namespaced)
import Unison.Term (Term)
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Typechecker qualified as Typechecker
import Unison.Typechecker.TypeLookup (TypeLookup (..))
import Unison.Util.Tuple qualified as Tuple
import Unison.Var (Var)
import Unison.Var qualified as Var

-- | Generate the LabeledDependencies for everything in a Decl, including the Decl itself, all
-- its constructors, all referenced types, and all possible record accessors.
--
-- Note that we can't actually tell whether the Decl was originally a record or not, so we
-- include all possible accessors, but they may or may not exist in the codebase.
labeledDeclDependenciesIncludingSelfAndFieldAccessors :: (Var v) => TypeReference -> (DD.Decl v a) -> Set LD.LabeledDependency
labeledDeclDependenciesIncludingSelfAndFieldAccessors :: forall v a.
Var v =>
TypeReference -> Decl v a -> Set LabeledDependency
labeledDeclDependenciesIncludingSelfAndFieldAccessors TypeReference
selfRef Decl v a
decl =
  TypeReference -> Decl v a -> Set LabeledDependency
forall v a.
Ord v =>
TypeReference -> Decl v a -> Set LabeledDependency
DD.labeledDeclDependenciesIncludingSelf TypeReference
selfRef Decl v a
decl
    Set LabeledDependency
-> Set LabeledDependency -> Set LabeledDependency
forall a. Semigroup a => a -> a -> a
<> case Decl v a
decl of
      Left EffectDeclaration v a
_effect -> Set LabeledDependency
forall a. Monoid a => a
mempty
      Right DataDeclaration v a
dataDecl ->
        TypeReference -> DataDeclaration v a -> Maybe (Set Referent)
forall v a.
Var v =>
TypeReference -> DataDeclaration v a -> Maybe (Set Referent)
fieldAccessorRefs TypeReference
selfRef DataDeclaration v a
dataDecl
          Maybe (Set Referent)
-> (Maybe (Set Referent) -> Set LabeledDependency)
-> Set LabeledDependency
forall a b. a -> (a -> b) -> b
& Set LabeledDependency
-> (Set Referent -> Set LabeledDependency)
-> Maybe (Set Referent)
-> Set LabeledDependency
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set LabeledDependency
forall a. Set a
Set.empty ((Referent -> LabeledDependency)
-> Set Referent -> Set LabeledDependency
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Referent -> LabeledDependency
LD.TermReferent)

-- | Generate Referents for all possible field accessors of a Decl.
--
-- Returns @Nothing@ if this couldn't be a record because it doesn't contain exactly one constructor, or because the
-- record contains a field with a higher rank type (and thus fails type inference).
fieldAccessorRefs :: forall v a. (Var v) => TypeReference -> DD.DataDeclaration v a -> Maybe (Set Referent)
fieldAccessorRefs :: forall v a.
Var v =>
TypeReference -> DataDeclaration v a -> Maybe (Set Referent)
fieldAccessorRefs TypeReference
declRef DataDeclaration v a
dd = do
  [(v
_, Type v a
typ)] <- [(v, Type v a)] -> Maybe [(v, Type v a)]
forall a. a -> Maybe a
Just (DataDeclaration v a -> [(v, Type v a)]
forall v a. DataDeclaration v a -> [(v, Type v a)]
DD.constructors DataDeclaration v a
dd)

  -- This name isn't important, we just need a name to generate field names from.
  -- The field names are thrown away afterwards.
  let typeName :: v
typeName = Text -> v
forall v. Var v => Text -> v
Var.named Text
"Type"
  -- These names are arbitrary and don't show up anywhere.
  let vars :: [v]
      -- We add `n` to the end of the variable name as a quick fix to #4752, but we suspect there's a more
      -- fundamental fix to be made somewhere in the term printer to automatically suffix a var name with its
      -- freshened id if it would be ambiguous otherwise.
      vars :: [v]
vars = [Word64 -> v -> v
forall v. Var v => Word64 -> v -> v
Var.freshenId (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) (Text -> v
forall v. Var v => Text -> v
Var.named (Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
tShow Int
n)) | Int
n <- [Int
0 .. Type v a -> Int
forall v a. Type v a -> Int
Type.arity Type v a
typ Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]

  Map v (TermReferenceId, Term v (), Type v ())
accessors <- PrettyPrintEnv
-> v
-> [v]
-> TypeReference
-> DataDeclaration v a
-> Maybe (Map v (TermReferenceId, Term v (), Type v ()))
forall v a.
Var v =>
PrettyPrintEnv
-> v
-> [v]
-> TypeReference
-> DataDeclaration v a
-> Maybe (Map v (TermReferenceId, Term v (), Type v ()))
hashFieldAccessors PrettyPrintEnv
PPE.empty v
typeName [v]
vars TypeReference
declRef DataDeclaration v a
dd

  Set Referent -> Maybe (Set Referent)
forall a. a -> Maybe a
Just (Getting
  (Set Referent)
  (Map v (TermReferenceId, Term v (), Type v ()))
  Referent
-> Map v (TermReferenceId, Term v (), Type v ()) -> Set Referent
forall a s. Getting (Set a) s a -> s -> Set a
setOf (((TermReferenceId, Term v (), Type v ())
 -> Const (Set Referent) (TermReferenceId, Term v (), Type v ()))
-> Map v (TermReferenceId, Term v (), Type v ())
-> Const
     (Set Referent) (Map v (TermReferenceId, Term v (), Type v ()))
forall (f :: * -> *) a. Foldable f => IndexedFold Int (f a) a
IndexedFold
  Int
  (Map v (TermReferenceId, Term v (), Type v ()))
  (TermReferenceId, Term v (), Type v ())
folded (((TermReferenceId, Term v (), Type v ())
  -> Const (Set Referent) (TermReferenceId, Term v (), Type v ()))
 -> Map v (TermReferenceId, Term v (), Type v ())
 -> Const
      (Set Referent) (Map v (TermReferenceId, Term v (), Type v ())))
-> ((Referent -> Const (Set Referent) Referent)
    -> (TermReferenceId, Term v (), Type v ())
    -> Const (Set Referent) (TermReferenceId, Term v (), Type v ()))
-> Getting
     (Set Referent)
     (Map v (TermReferenceId, Term v (), Type v ()))
     Referent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermReferenceId -> Const (Set Referent) TermReferenceId)
-> (TermReferenceId, Term v (), Type v ())
-> Const (Set Referent) (TermReferenceId, Term v (), Type v ())
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (TermReferenceId, Term v (), Type v ())
  (TermReferenceId, Term v (), Type v ())
  TermReferenceId
  TermReferenceId
_1 ((TermReferenceId -> Const (Set Referent) TermReferenceId)
 -> (TermReferenceId, Term v (), Type v ())
 -> Const (Set Referent) (TermReferenceId, Term v (), Type v ()))
-> ((Referent -> Const (Set Referent) Referent)
    -> TermReferenceId -> Const (Set Referent) TermReferenceId)
-> (Referent -> Const (Set Referent) Referent)
-> (TermReferenceId, Term v (), Type v ())
-> Const (Set Referent) (TermReferenceId, Term v (), Type v ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermReferenceId -> Referent)
-> (Referent -> Const (Set Referent) Referent)
-> TermReferenceId
-> Const (Set Referent) TermReferenceId
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to TermReferenceId -> Referent
Referent.fromTermReferenceId) Map v (TermReferenceId, Term v (), Type v ())
accessors)

-- | Generate Referents for all possible field accessors of a Decl.
--
-- Returns @Nothing@ if inferring/typechecking of any accessor fails, which shouldn't normally happen, but does when
-- record fields are higher rank, because the higher rank types can't be inferred.
--
-- See https://github.com/unisonweb/unison/issues/498
hashFieldAccessors ::
  forall v a.
  (Var.Var v) =>
  PrettyPrintEnv ->
  v ->
  [v] ->
  TypeReference ->
  DD.DataDeclaration v a ->
  Maybe (Map v (TermReferenceId, Term v (), Type v ()))
hashFieldAccessors :: forall v a.
Var v =>
PrettyPrintEnv
-> v
-> [v]
-> TypeReference
-> DataDeclaration v a
-> Maybe (Map v (TermReferenceId, Term v (), Type v ()))
hashFieldAccessors PrettyPrintEnv
ppe v
declName [v]
vars TypeReference
declRef DataDeclaration v a
dd = do
  let accessors :: [(v, (), Term v ())]
      accessors :: [(v, (), Term v ())]
accessors =
        (NonEmpty v -> v)
-> (() -> ())
-> [(v, ())]
-> v
-> TypeReference
-> [(v, (), Term v ())]
forall a v.
(Semigroup a, Var v) =>
(NonEmpty v -> v)
-> (a -> a) -> [(v, a)] -> v -> TypeReference -> [(v, a, Term v a)]
generateRecordAccessors NonEmpty v -> v
forall v. Var v => NonEmpty v -> v
Var.namespaced () -> ()
forall a. a -> a
id ((v -> (v, ())) -> [v] -> [(v, ())]
forall a b. (a -> b) -> [a] -> [b]
map (,()) [v]
vars) v
declName TypeReference
declRef

  [(v, (Term v (), Type v (), ()))]
typecheckedAccessors <-
    [(v, (), Term v ())]
-> ((v, (), Term v ()) -> Maybe (v, (Term v (), Type v (), ())))
-> Maybe [(v, (Term v (), Type v (), ()))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(v, (), Term v ())]
accessors \(v
v, ()
_a, Term v ()
term) -> do
      Type v ()
typ <- Term v () -> Maybe (Type v ())
typecheck Term v ()
term
      (v, (Term v (), Type v (), ()))
-> Maybe (v, (Term v (), Type v (), ()))
forall a. a -> Maybe a
Just (v
v, (Term v ()
term, Type v ()
typ, ()))

  [(v, (Term v (), Type v (), ()))]
typecheckedAccessors
    [(v, (Term v (), Type v (), ()))]
-> ([(v, (Term v (), Type v (), ()))]
    -> Map v (Term v (), Type v (), ()))
-> Map v (Term v (), Type v (), ())
forall a b. a -> (a -> b) -> b
& [(v, (Term v (), Type v (), ()))]
-> Map v (Term v (), Type v (), ())
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    Map v (Term v (), Type v (), ())
-> (Map v (Term v (), Type v (), ())
    -> Map v (TermReferenceId, Term v (), Type v (), ()))
-> Map v (TermReferenceId, Term v (), Type v (), ())
forall a b. a -> (a -> b) -> b
& Map v (Term v (), Type v (), ())
-> Map v (TermReferenceId, Term v (), Type v (), ())
forall v a extra.
Var v =>
Map v (Term v a, Type v a, extra)
-> Map v (TermReferenceId, Term v a, Type v a, extra)
Hashing.hashTermComponents
    Map v (TermReferenceId, Term v (), Type v (), ())
-> (Map v (TermReferenceId, Term v (), Type v (), ())
    -> Map v (TermReferenceId, Term v (), Type v ()))
-> Map v (TermReferenceId, Term v (), Type v ())
forall a b. a -> (a -> b) -> b
& ((TermReferenceId, Term v (), Type v (), ())
 -> (TermReferenceId, Term v (), Type v ()))
-> Map v (TermReferenceId, Term v (), Type v (), ())
-> Map v (TermReferenceId, Term v (), Type v ())
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (TermReferenceId, Term v (), Type v (), ())
-> (TermReferenceId, Term v (), Type v ())
forall a b. Drop4th a b => a -> b
Tuple.drop4th
    Map v (TermReferenceId, Term v (), Type v ())
-> (Map v (TermReferenceId, Term v (), Type v ())
    -> Maybe (Map v (TermReferenceId, Term v (), Type v ())))
-> Maybe (Map v (TermReferenceId, Term v (), Type v ()))
forall a b. a -> (a -> b) -> b
& Map v (TermReferenceId, Term v (), Type v ())
-> Maybe (Map v (TermReferenceId, Term v (), Type v ()))
forall a. a -> Maybe a
Just
  where
    typecheck :: Term v () -> Maybe (Type v ())
    typecheck :: Term v () -> Maybe (Type v ())
typecheck Term v ()
term = do
      Type v ()
typ <- Result (Notes v ()) (Type v ()) -> Maybe (Type v ())
forall notes a. Result notes a -> Maybe a
Result.result (PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v ()
-> Term v ()
-> Result (Notes v ()) (Type v ())
forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
Typechecker.synthesize PrettyPrintEnv
ppe PatternMatchCoverageCheckAndKindInferenceSwitch
Typechecker.PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled Env v ()
typecheckingEnv Term v ()
term)
      -- Note: Typechecker.synthesize doesn't normalize the output
      -- type. We do so here using `Type.cleanup`, mirroring what's
      -- done when typechecking a whole file and ensuring we get the
      -- same inferred type.
      Type v () -> Maybe (Type v ())
forall a. a -> Maybe a
Just (Type v () -> Type v ()
forall v a. Var v => Type v a -> Type v a
Type.cleanup Type v ()
typ)

    typecheckingEnv :: Typechecker.Env v ()
    typecheckingEnv :: Env v ()
typecheckingEnv =
      Typechecker.Env
        { $sel:ambientAbilities:Env :: [Type v ()]
ambientAbilities = [Type v ()]
forall a. Monoid a => a
mempty,
          $sel:typeLookup:Env :: TypeLookup v ()
typeLookup =
            TypeLookup
              { $sel:typeOfTerms:TypeLookup :: Map TypeReference (Type v ())
typeOfTerms = Map TypeReference (Type v ())
forall a. Monoid a => a
mempty,
                $sel:dataDecls:TypeLookup :: Map TypeReference (DataDeclaration v ())
dataDecls = TypeReference
-> DataDeclaration v () -> Map TypeReference (DataDeclaration v ())
forall k a. k -> a -> Map k a
Map.singleton TypeReference
declRef (DataDeclaration v a -> DataDeclaration v ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void DataDeclaration v a
dd),
                $sel:effectDecls:TypeLookup :: Map TypeReference (EffectDeclaration v ())
effectDecls = Map TypeReference (EffectDeclaration v ())
forall a. Monoid a => a
mempty
              },
          $sel:termsByShortname:Env :: Map Name [Either Name (NamedReference v ())]
termsByShortname = Map Name [Either Name (NamedReference v ())]
forall a. Monoid a => a
mempty,
          $sel:topLevelComponents:Env :: Map Name (NamedReference v ())
topLevelComponents = Map Name (NamedReference v ())
forall k a. Map k a
Map.empty
        }