module Unison.Cli.TypeCheck
  ( computeTypecheckingEnvironment,
    typecheckTerm,
  )
where

import Data.Map.Strict qualified as Map
import Unison.Codebase (Codebase)
import Unison.Codebase qualified as Codebase
import Unison.FileParsers qualified as FileParsers
import Unison.Parser.Ann (Ann (..))
import Unison.Prelude
import Unison.Result qualified as Result
import Unison.Sqlite qualified as Sqlite
import Unison.Symbol (Symbol (Symbol))
import Unison.Term (Term)
import Unison.Type (Type)
import Unison.Typechecker qualified as Typechecker
import Unison.Typechecker.Variance qualified as Variance
import Unison.UnisonFile (UnisonFile)
import Unison.UnisonFile qualified as UF
import Unison.Var qualified as Var

computeTypecheckingEnvironment ::
  FileParsers.ShouldUseTndr Sqlite.Transaction ->
  Codebase IO Symbol Ann ->
  [Type Symbol Ann] ->
  UnisonFile Symbol Ann ->
  Sqlite.Transaction (Typechecker.Env Symbol Ann)
computeTypecheckingEnvironment :: ShouldUseTndr Transaction
-> Codebase IO Symbol Ann
-> [Type Symbol Ann]
-> UnisonFile Symbol Ann
-> Transaction (Env Symbol Ann)
computeTypecheckingEnvironment ShouldUseTndr Transaction
shouldUseTndr Codebase IO Symbol Ann
codebase [Type Symbol Ann]
ambientAbilities UnisonFile Symbol Ann
unisonFile =
  ShouldUseTndr Transaction
-> [Type Symbol Ann]
-> (DefnsF Set TermReference TermReference
    -> Transaction (TypeLookup Symbol Ann))
-> UnisonFile Symbol Ann
-> Transaction (Env Symbol Ann)
forall (m :: * -> *) v.
(Var v, Monad m) =>
ShouldUseTndr m
-> [Type v]
-> (DefnsF Set TermReference TermReference -> m (TypeLookup v Ann))
-> UnisonFile v
-> m (Env v Ann)
FileParsers.computeTypecheckingEnvironment
    ShouldUseTndr Transaction
shouldUseTndr
    [Type Symbol Ann]
ambientAbilities
    (Codebase IO Symbol Ann
-> DefnsF Set TermReference TermReference
-> Transaction (TypeLookup Symbol Ann)
Codebase.typeLookupForDependencies Codebase IO Symbol Ann
codebase)
    UnisonFile Symbol Ann
unisonFile

typecheckTerm ::
  Codebase IO Symbol Ann ->
  Term Symbol Ann ->
  Sqlite.Transaction
    ( Result.Result
        (Seq (Result.Note Symbol Ann))
        (Type Symbol Ann)
    )
typecheckTerm :: Codebase IO Symbol Ann
-> Term Symbol Ann
-> Transaction (Result (Seq (Note Symbol Ann)) (Type Symbol Ann))
typecheckTerm Codebase IO Symbol Ann
codebase Term Symbol Ann
tm = do
  let v :: Symbol
v = Word64 -> Type -> Symbol
Symbol Word64
0 (InferenceType -> Type
Var.Inference InferenceType
Var.Other)
  let file :: UnisonFile Symbol Ann
file = Map Symbol (TypeReferenceId, DataDeclaration Symbol Ann)
-> Map Symbol (TypeReferenceId, EffectDeclaration Symbol Ann)
-> Map Symbol (Ann, Term Symbol Ann)
-> Map WatchKind [(Symbol, Ann, Term Symbol Ann)]
-> UnisonFile Symbol Ann
forall v a.
Map v (TypeReferenceId, DataDeclaration v a)
-> Map v (TypeReferenceId, EffectDeclaration v a)
-> Map v (a, Term v a)
-> Map WatchKind [(v, a, Term v a)]
-> UnisonFile v a
UF.UnisonFileId Map Symbol (TypeReferenceId, DataDeclaration Symbol Ann)
forall a. Monoid a => a
mempty Map Symbol (TypeReferenceId, EffectDeclaration Symbol Ann)
forall a. Monoid a => a
mempty (Symbol
-> (Ann, Term Symbol Ann) -> Map Symbol (Ann, Term Symbol Ann)
forall k a. k -> a -> Map k a
Map.singleton Symbol
v (Ann
External, Term Symbol Ann
tm)) Map WatchKind [(Symbol, Ann, Term Symbol Ann)]
forall a. Monoid a => a
mempty
  typeLookup <- Codebase IO Symbol Ann
-> DefnsF Set TermReference TermReference
-> Transaction (TypeLookup Symbol Ann)
Codebase.typeLookupForDependencies Codebase IO Symbol Ann
codebase (UnisonFile Symbol Ann -> DefnsF Set TermReference TermReference
forall a v.
(Monoid a, Var v) =>
UnisonFile v a -> DefnsF Set TermReference TermReference
UF.dependencies UnisonFile Symbol Ann
file)
  let typecheckingEnv =
        Typechecker.Env
          { ambientAbilities :: [Type Symbol Ann]
ambientAbilities = [],
            TypeLookup Symbol Ann
typeLookup :: TypeLookup Symbol Ann
typeLookup :: TypeLookup Symbol Ann
typeLookup,
            termsByShortname :: Map Name [Either Name (NamedReference Symbol Ann)]
termsByShortname = Map Name [Either Name (NamedReference Symbol Ann)]
forall k a. Map k a
Map.empty,
            freeNameToFuzzyTermsByShortName :: Map Name (Map Name [Either Name (NamedReference Symbol Ann)])
freeNameToFuzzyTermsByShortName = Map Name (Map Name [Either Name (NamedReference Symbol Ann)])
forall k a. Map k a
Map.empty,
            topLevelComponents :: Map Name (NamedReference Symbol Ann)
topLevelComponents = Map Name (NamedReference Symbol Ann)
forall k a. Map k a
Map.empty,
            variances :: Map TermReference [Variance]
variances = TypeLookup Symbol Ann -> Map TermReference [Variance]
forall v a.
(Var v, Show a) =>
TypeLookup v a -> Map TermReference [Variance]
Variance.fromTypeLookup TypeLookup Symbol Ann
typeLookup
          }
  pure $ fmap extract $ FileParsers.synthesizeFile typecheckingEnv file
  where
    extract :: TypecheckedUnisonFile v a -> Type v a
extract TypecheckedUnisonFile v a
tuf
      | [[(v
_, a
_, Term v a
_, Type v a
ty)]] <- TypecheckedUnisonFile v a -> [[(v, a, Term v a, Type v a)]]
forall v a.
TypecheckedUnisonFile v a -> [[(v, a, Term v a, Type v a)]]
UF.topLevelComponents' TypecheckedUnisonFile v a
tuf = Type v a
ty
      | Bool
otherwise = WatchKind -> Type v a
forall a. HasCallStack => WatchKind -> a
error WatchKind
"internal error: typecheckTerm"