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.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 Symbol Ann
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 :: Env Symbol Ann
typecheckingEnv =
        Typechecker.Env
          { $sel:ambientAbilities:Env :: [Type Symbol Ann]
ambientAbilities = [],
            TypeLookup Symbol Ann
typeLookup :: TypeLookup Symbol Ann
$sel:typeLookup:Env :: TypeLookup Symbol Ann
typeLookup,
            $sel:termsByShortname:Env :: Map Name [Either Name (NamedReference Symbol Ann)]
termsByShortname = Map Name [Either Name (NamedReference Symbol Ann)]
forall k a. Map k a
Map.empty,
            $sel:topLevelComponents:Env :: Map Name (NamedReference Symbol Ann)
topLevelComponents = Map Name (NamedReference Symbol Ann)
forall k a. Map k a
Map.empty
          }
  Result (Seq (Note Symbol Ann)) (Type Symbol Ann)
-> Transaction (Result (Seq (Note Symbol Ann)) (Type Symbol Ann))
forall a. a -> Transaction a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result (Seq (Note Symbol Ann)) (Type Symbol Ann)
 -> Transaction (Result (Seq (Note Symbol Ann)) (Type Symbol Ann)))
-> Result (Seq (Note Symbol Ann)) (Type Symbol Ann)
-> Transaction (Result (Seq (Note Symbol Ann)) (Type Symbol Ann))
forall a b. (a -> b) -> a -> b
$ (TypecheckedUnisonFile Symbol Ann -> Type Symbol Ann)
-> MaybeT
     (WriterT (Seq (Note Symbol Ann)) Identity)
     (TypecheckedUnisonFile Symbol Ann)
-> Result (Seq (Note Symbol Ann)) (Type Symbol Ann)
forall a b.
(a -> b)
-> MaybeT (WriterT (Seq (Note Symbol Ann)) Identity) a
-> MaybeT (WriterT (Seq (Note Symbol Ann)) Identity) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypecheckedUnisonFile Symbol Ann -> Type Symbol Ann
forall {v} {a}. TypecheckedUnisonFile v a -> Type v a
extract (MaybeT
   (WriterT (Seq (Note Symbol Ann)) Identity)
   (TypecheckedUnisonFile Symbol Ann)
 -> Result (Seq (Note Symbol Ann)) (Type Symbol Ann))
-> MaybeT
     (WriterT (Seq (Note Symbol Ann)) Identity)
     (TypecheckedUnisonFile Symbol Ann)
-> Result (Seq (Note Symbol Ann)) (Type Symbol Ann)
forall a b. (a -> b) -> a -> b
$ Env Symbol Ann
-> UnisonFile Symbol Ann
-> MaybeT
     (WriterT (Seq (Note Symbol Ann)) Identity)
     (TypecheckedUnisonFile Symbol Ann)
forall (m :: * -> *) v.
(Monad m, Var v) =>
Env v Ann
-> UnisonFile v
-> ResultT (Seq (Note v Ann)) m (TypecheckedUnisonFile v Ann)
FileParsers.synthesizeFile Env Symbol Ann
typecheckingEnv UnisonFile Symbol Ann
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"