mirror of
https://github.com/unisonweb/unison.git
synced 2024-10-05 14:17:33 +03:00
Keep unqualified names in env
This commit is contained in:
parent
f20ad4dda6
commit
54789edc46
@ -29,7 +29,8 @@ import qualified Unison.Typechecker as Typechecker
|
||||
import Unison.UnisonFile (pattern UnisonFile)
|
||||
import qualified Unison.UnisonFile as UF
|
||||
import Unison.Var (Var)
|
||||
-- import qualified Debug.Trace as Trace
|
||||
import qualified Unison.Var as Var
|
||||
import qualified Data.Text as Text
|
||||
|
||||
type Term v = AnnotatedTerm v Ann
|
||||
type Type v = AnnotatedType v Ann
|
||||
@ -54,12 +55,20 @@ synthesizeFile unisonFile =
|
||||
datas = Map.union dds B.builtinDataDecls -- `Map.union` is left-biased
|
||||
effects = Map.union eds B.builtinEffectDecls
|
||||
env0 = Typechecker.Env
|
||||
Intrinsic [] typeOf dataDeclaration effectDeclaration
|
||||
Intrinsic
|
||||
[]
|
||||
typeOf
|
||||
dataDeclaration
|
||||
effectDeclaration
|
||||
(Map.fromList $
|
||||
fmap (\(v, (_tm, typ)) -> (unqualified $ Var.name v, typ))
|
||||
B.builtinTypedTerms)
|
||||
n = Typechecker.synthesize env0 term
|
||||
die s h = error $ "unknown " ++ s ++ " reference " ++ show h
|
||||
typeOf r = error $ "unknown reference " ++ show r
|
||||
dataDeclaration r = pure $ fromMaybe (die "data" r) $ Map.lookup r datas
|
||||
effectDeclaration r = pure $ fromMaybe (die "effect" r) $ Map.lookup r effects
|
||||
unqualified = last . Text.splitOn "."
|
||||
in (term,) <$> runIdentity n
|
||||
|
||||
synthesizeUnisonFile :: Var v
|
||||
|
@ -290,7 +290,11 @@ iff a cond t f = ABT.tm' a (If cond t f)
|
||||
ann_ :: Ord v => Term' vt v -> Type vt -> Term' vt v
|
||||
ann_ e t = ABT.tm (Ann e t)
|
||||
|
||||
ann :: Ord v => a -> AnnotatedTerm2 vt at ap v a -> Type.AnnotatedType vt at -> AnnotatedTerm2 vt at ap v a
|
||||
ann :: Ord v
|
||||
=> a
|
||||
-> AnnotatedTerm2 vt at ap v a
|
||||
-> Type.AnnotatedType vt at
|
||||
-> AnnotatedTerm2 vt at ap v a
|
||||
ann a e t = ABT.tm' a (Ann e t)
|
||||
|
||||
-- arya: are we sure we want the two annotations to be the same?
|
||||
|
@ -8,7 +8,9 @@
|
||||
|
||||
module Unison.Typechecker where
|
||||
|
||||
import Data.Map (Map)
|
||||
import Data.Maybe (isJust)
|
||||
import Data.Text (Text)
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Blank as B
|
||||
import Unison.DataDeclaration (DataDeclaration', EffectDeclaration')
|
||||
@ -40,7 +42,7 @@ data Env f v loc = Env
|
||||
, typeOf :: Reference -> f (Type v loc)
|
||||
, dataDeclaration :: Reference -> f (DataDeclaration' v loc)
|
||||
, effectDeclaration :: Reference -> f (EffectDeclaration' v loc)
|
||||
-- , terms :: Map Reference (Type v loc)
|
||||
, terms :: Map Text (Type v loc)
|
||||
}
|
||||
|
||||
-- -- | Compute the allowed type of a replacement for a given subterm.
|
||||
@ -124,21 +126,32 @@ synthesize env t =
|
||||
(effectDeclaration env)
|
||||
(Term.vtmap TypeVar.Universal t)
|
||||
|
||||
resolveAndSynthesize
|
||||
-- Synthesize and do type-directed name resolution
|
||||
synthesizeAndResolve
|
||||
:: (Monad f, Var v, Ord loc)
|
||||
=> Env f v loc
|
||||
-> Term v loc
|
||||
-> f (Result (Note v loc) (Type v loc))
|
||||
resolveAndSynthesize env t = do
|
||||
r <- synthesize env t
|
||||
let resolveds = notes r >>= \n ->
|
||||
case n of
|
||||
Typechecking
|
||||
(Context.Note (Context.SolvedBlank (B.Resolve loc name) _ typ) _) ->
|
||||
[(loc, name, typ)]
|
||||
_ -> []
|
||||
_ <- pure $ resolveds
|
||||
pure r
|
||||
synthesizeAndResolve env t = do
|
||||
r <- synthesize env t
|
||||
let _ = notes r >>= \n ->
|
||||
case n of
|
||||
Typechecking
|
||||
(Context.Note (Context.SolvedBlank (B.Resolve loc name) _ typ) _) ->
|
||||
[(loc, name, typ)]
|
||||
_ -> []
|
||||
-- look in the env for references to things with:
|
||||
-- 1. A matching name (prefixed with .+\.) and type.
|
||||
-- Tell the user about these and suggest an import.
|
||||
-- 2. There's more than one name that exactly matches,
|
||||
-- but only one that typechecks. Substitute that one into the code.
|
||||
-- 3. Matching name but incorrect type. Tell the user about this.
|
||||
-- 4. Matching type but not by that name. Tell the user about these.
|
||||
-- 5. No match at all. Throw an unresolved symbol at the user.
|
||||
-- traverse resolveds
|
||||
pure r
|
||||
--where
|
||||
--f (loc, name, typ) = terms env name
|
||||
|
||||
-- | Check whether a term matches a type, using a
|
||||
-- function to resolve the type of @Ref@ constructors
|
||||
|
@ -1,5 +1,6 @@
|
||||
module Unison.Test.Common where
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Unison.Builtin as B
|
||||
import qualified Unison.FileParsers as FP
|
||||
import Unison.Parser (Ann(..))
|
||||
@ -32,7 +33,7 @@ typechecks :: String -> Bool
|
||||
typechecks = Result.isSuccess . file
|
||||
|
||||
env :: Monad m => Typechecker.Env m Symbol Ann
|
||||
env = Typechecker.Env Intrinsic [] typeOf dd ed where
|
||||
env = Typechecker.Env Intrinsic [] typeOf dd ed Map.empty where
|
||||
typeOf r = error $ "no type for: " ++ show r
|
||||
dd r = error $ "no data declaration for: " ++ show r
|
||||
ed r = error $ "no effect declaration for: " ++ show r
|
||||
|
Loading…
Reference in New Issue
Block a user