From 7c3fb56808daeee14a5d8c65e039121955993daf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=BAnar=20=C3=93li=20Bjarnason?= Date: Tue, 31 Jul 2018 13:12:53 -0400 Subject: [PATCH 01/11] Three different blanks --- parser-typechecker/src/Unison/Codecs.hs | 2 +- parser-typechecker/src/Unison/Lexer.hs | 7 ++- parser-typechecker/src/Unison/Parser.hs | 6 +++ parser-typechecker/src/Unison/Paths.hs | 2 +- parser-typechecker/src/Unison/Term.hs | 50 +++++++++++++------ parser-typechecker/src/Unison/TermParser.hs | 8 +-- .../src/Unison/Typechecker/Context.hs | 18 ++++--- 7 files changed, 64 insertions(+), 29 deletions(-) diff --git a/parser-typechecker/src/Unison/Codecs.hs b/parser-typechecker/src/Unison/Codecs.hs index 86ee6c59e..a4cdfb878 100644 --- a/parser-typechecker/src/Unison/Codecs.hs +++ b/parser-typechecker/src/Unison/Codecs.hs @@ -165,7 +165,7 @@ serializeTerm x = do putLength $ length casePositions traverse_ serializeCase2 casePositions incPosition - Blank -> error "cannot serialize program with blanks" + Blank _ -> error "cannot serialize program with blanks" Handle h body -> do hpos <- serializeTerm h bpos <- serializeTerm body diff --git a/parser-typechecker/src/Unison/Lexer.hs b/parser-typechecker/src/Unison/Lexer.hs index 3dd130693..57827dbfd 100644 --- a/parser-typechecker/src/Unison/Lexer.hs +++ b/parser-typechecker/src/Unison/Lexer.hs @@ -41,6 +41,7 @@ data Lexeme | Backticks String -- an identifier in backticks | WordyId String -- a (non-infix) identifier | SymbolyId String -- an infix identifier + | Blank String -- a typed hole or placeholder | Numeric String -- numeric literals, left unparsed | Hash Hash -- hash literals | Err Err @@ -69,6 +70,7 @@ instance ShowToken (Token Lexeme) where pretty (Backticks n) = '`' : n ++ ['`'] pretty (WordyId n) = n pretty (SymbolyId n) = n + pretty (Blank s) = "_" ++ s pretty (Numeric n) = n pretty (Hash h) = show h pretty (Err e) = show e @@ -201,7 +203,10 @@ lexer scope rem = '@' : rem -> Token (Reserved "@") pos (inc pos) : goWhitespace l (inc pos) rem '_' : rem | hasSep rem -> - Token (Reserved "_") pos (inc pos) : goWhitespace l (inc pos) rem + Token (Blank "") pos (inc pos) : goWhitespace l (inc pos) rem + '_' : (wordyId -> Right (id, rem)) -> + let pos' = incBy id $ inc pos + in Token (Blank id) pos pos' : goWhitespace l pos' rem '|' : c : rem | isSpace c || isAlphaNum c -> Token (Reserved "|") pos (inc pos) : goWhitespace l (inc pos) (c:rem) '=' : (rem @ (c : _)) | isSpace c || isAlphaNum c -> diff --git a/parser-typechecker/src/Unison/Parser.hs b/parser-typechecker/src/Unison/Parser.hs index fbfa1e010..47a0e997e 100644 --- a/parser-typechecker/src/Unison/Parser.hs +++ b/parser-typechecker/src/Unison/Parser.hs @@ -248,6 +248,12 @@ reserved w = label w $ queryToken getReserved where getReserved (L.Reserved w') | w == w' = Just w getReserved _ = Nothing +-- Parse a placeholder or typed hole +blank :: Var v => P v (L.Token String) +blank = label "blank" $ queryToken getBlank + where getBlank (L.Blank s) = Just s + getBlank _ = Nothing + numeric :: Var v => P v (L.Token String) numeric = queryToken getNumeric where getNumeric (L.Numeric s) = Just s diff --git a/parser-typechecker/src/Unison/Paths.hs b/parser-typechecker/src/Unison/Paths.hs index 0a2d5a104..62491174f 100644 --- a/parser-typechecker/src/Unison/Paths.hs +++ b/parser-typechecker/src/Unison/Paths.hs @@ -146,7 +146,7 @@ insertTerm at ctx = do Term (E.Vector' vs) -> do i <- listToMaybe [i | Index i <- [last at]] let v2 = E.vector'() ((E.vmap ABT.Bound <$> Vector.take (i+1) vs) `mappend` - Vector.singleton (E.blank()) `mappend` + Vector.singleton (E.placeholder ()) `mappend` (E.vmap ABT.Bound <$> Vector.drop (i+1) vs)) asTerm =<< set (Term v2) _ -> Nothing -- todo - allow other types of insertions, like \x -> y to \x x2 -> y diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 43e960609..ccf914afd 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -13,14 +13,15 @@ module Unison.Term where import qualified Control.Monad.Writer.Strict as Writer import Data.Foldable (toList) +import Data.Foldable (traverse_) import Data.Int (Int64) import Data.List (foldl') import Data.Map (Map) import qualified Data.Map as Map -import qualified Data.Monoid as Monoid import Data.Set (Set, union) import qualified Data.Set as Set import Data.Text (Text) +import qualified Data.Text as Text import Data.Vector (Vector) import qualified Data.Vector as Vector import Data.Word (Word64) @@ -40,12 +41,20 @@ import Unison.Type (Type) import qualified Unison.Type as Type import Unison.Var (Var) import Unsafe.Coerce -import Data.Foldable (traverse_) -- todo: add loc to MatchCase data MatchCase loc a = MatchCase (Pattern loc) (Maybe a) a deriving (Show,Eq,Foldable,Functor,Generic,Generic1,Traversable) +data Blank + -- An expression that has not been filled in, has type `forall a . a`. + = Placeholder + -- A user-provided typed hole + | Remember String + -- A name to be resolved with type-directed name resolution. + | Resolve String + deriving (Show, Eq, Ord) + -- | Base functor for terms in the Unison language -- We need `typeVar` because the term and type variables may differ. data F typeVar typeAnn patternAnn a @@ -54,9 +63,11 @@ data F typeVar typeAnn patternAnn a | Float Double | Boolean Bool | Text Text - | Blank -- An expression that has not been filled in, has type `forall a . a` + | Blank Blank | Ref Reference - | Constructor Reference Int -- First argument identifies the data type, second argument identifies the constructor + -- First argument identifies the data type, + -- second argument identifies the constructor + | Constructor Reference Int | Request Reference Int | Handle a a | EffectPure a @@ -159,7 +170,7 @@ pattern UInt64' n <- (ABT.out -> ABT.Tm (UInt64 n)) pattern Float' n <- (ABT.out -> ABT.Tm (Float n)) pattern Boolean' b <- (ABT.out -> ABT.Tm (Boolean b)) pattern Text' s <- (ABT.out -> ABT.Tm (Text s)) -pattern Blank' <- (ABT.out -> ABT.Tm Blank) +pattern Blank' b <- (ABT.out -> ABT.Tm (Blank b)) pattern Ref' r <- (ABT.out -> ABT.Tm (Ref r)) pattern Builtin' r <- (ABT.out -> ABT.Tm (Ref (Builtin r))) pattern App' f x <- (ABT.out -> ABT.Tm (App f x)) @@ -222,8 +233,14 @@ uint64 a d = ABT.tm' a (UInt64 d) text :: Ord v => a -> Text -> AnnotatedTerm2 vt at ap v a text a = ABT.tm' a . Text -blank :: Ord v => a -> AnnotatedTerm2 vt at ap v a -blank a = ABT.tm' a Blank +placeholder :: Ord v => a -> AnnotatedTerm2 vt at ap v a +placeholder a = ABT.tm' a (Blank Placeholder) + +remember :: Ord v => a -> String -> AnnotatedTerm2 vt at ap v a +remember a s = ABT.tm' a . Blank $ Remember s + +resolve :: Ord v => a -> String -> AnnotatedTerm2 vt at ap v a +resolve a s = ABT.tm' a . Blank $ Resolve s constructor :: Ord v => a -> Reference -> Int -> AnnotatedTerm2 vt at ap v a constructor a ref n = ABT.tm' a (Constructor ref n) @@ -411,11 +428,6 @@ updateDependencies u tm = ABT.rebuildUp go tm where go (Ref r) = Ref (Map.findWithDefault r r u) go f = f -countBlanks :: Ord v => Term v -> Int -countBlanks t = Monoid.getSum . Writer.execWriter $ ABT.visit' f t - where f Blank = Writer.tell (Monoid.Sum (1 :: Int)) *> pure Blank - f t = pure t - -- | If the outermost term is a function application, -- perform substitution of the argument into the body betaReduce :: Var v => Term v -> Term v @@ -440,7 +452,11 @@ instance Var v => Hashable1 (F v a p) where Float n -> [tag 66, Hashable.Double n] Boolean b -> [tag 67, accumulateToken b] Text t -> [tag 68, accumulateToken t] - Blank -> [tag 1] + Blank b -> + tag 1 : case b of + Placeholder -> [tag 0] + Remember s -> [tag 1, Hashable.Text (Text.pack s)] + Resolve s -> [tag 2, Hashable.Text (Text.pack s)] Ref (Reference.Builtin name) -> [tag 2, accumulateToken name] Ref (Reference.Derived _) -> error "handled above, but GHC can't figure this out" App a a2 -> [tag 3, hashed (hash a), hashed (hash a2)] @@ -480,7 +496,7 @@ instance (Var vt, Eq a) => Eq (F vt at p a) where Float x == Float y = x == y Boolean x == Boolean y = x == y Text x == Text y = x == y - Blank == Blank = True + Blank b == Blank q = b == q Ref x == Ref y = x == y Constructor r cid == Constructor r2 cid2 = r == r2 && cid == cid2 Request r cid == Request r2 cid2 = r == r2 && cid == cid2 @@ -513,7 +529,11 @@ instance (Var v, Show p, Show a0, Show a) => Show (F v a0 p a) where showParen (p > 9) $ showsPrec 9 f <> s" " <> showsPrec 10 x go _ (Lam body) = showParen True (s"λ " <> showsPrec 0 body) go _ (Vector vs) = showListWith (showsPrec 0) (Vector.toList vs) - go _ Blank = s"_" + go _ (Blank b) = + case b of + Placeholder -> s"_" + Remember r -> s("_" ++ r) + Resolve r -> s r go _ (Ref r) = showsPrec 0 r go _ (Let b body) = showParen True (s"let " <> showsPrec 0 b <> s" in " <> showsPrec 0 body) go _ (LetRec bs body) = showParen True (s"let rec" <> showsPrec 0 bs <> s" in " <> showsPrec 0 body) diff --git a/parser-typechecker/src/Unison/TermParser.hs b/parser-typechecker/src/Unison/TermParser.hs index 4e3ab3113..86adb6d6f 100644 --- a/parser-typechecker/src/Unison/TermParser.hs +++ b/parser-typechecker/src/Unison/TermParser.hs @@ -8,10 +8,10 @@ module Unison.TermParser where +-- import Debug.Trace import Control.Applicative import Control.Monad (guard, join, when) import Control.Monad.Reader (ask) --- import Debug.Trace import Data.Char (isUpper) import Data.Foldable (asum) import Data.Int (Int64) @@ -186,8 +186,8 @@ boolean :: Var v => TermP v boolean = ((\t -> Term.boolean (ann t) True) <$> reserved "true") <|> ((\t -> Term.boolean (ann t) False) <$> reserved "false") -blank :: Var v => TermP v -blank = (\t -> Term.blank (ann t)) <$> reserved "_" +remember :: Var v => TermP v +remember = (\t -> Term.remember (ann t) (L.payload t)) <$> blank vector :: Var v => TermP v -> TermP v vector p = f <$> reserved "[" <*> elements <*> reserved "]" @@ -198,7 +198,7 @@ vector p = f <$> reserved "[" <*> elements <*> reserved "]" termLeaf :: forall v. Var v => TermP v termLeaf = asum [hashLit, prefixTerm, text, number, boolean, - tupleOrParenthesizedTerm, blank, vector term] + tupleOrParenthesizedTerm, remember, vector term] and = label "and" $ f <$> reserved "and" <*> termLeaf <*> termLeaf where f kw x y = Term.and (ann kw <> ann y) x y diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 8c4b8ce00..cdef9f677 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -471,10 +471,10 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var Nothing -> compilerCrash $ UndeclaredTermVariable v ctx Just t -> pure t - go Term.Blank' = do - v <- freshNamed "_" - appendContext $ context [Existential v] - pure $ Type.existential' l v -- forall (TypeVar.Universal v) (Type.universal v) + go (Term.Blank' _) = error "TODO" + -- v <- freshNamed "_" + -- appendContext $ context [Existential v] + -- pure $ Type.existential' l v -- forall (TypeVar.Universal v) (Type.universal v) go (Term.Ann' (Term.Ref' _) t) = case ABT.freeVars t of s | Set.null s -> -- innermost Ref annotation assumed to be correctly provided by `synthesizeClosed` @@ -636,7 +636,7 @@ patternToTerm pat = case pat of (h : t) <- get put t pure $ Term.var loc h - Pattern.Unbound loc -> pure $ Term.blank loc + Pattern.Unbound loc -> pure $ Term.placeholder loc Pattern.As loc p -> do (h : t) <- get put t @@ -668,7 +668,10 @@ checkCase scrutineeType outputType (Term.MatchCase pat guard rhs) = patTerm :: Term v loc patTerm = evalState (patternToTerm (pat :: Pattern loc) :: State [v] (Term v loc)) vs newBody = Term.let1 [((loc rhs', Var.named "_"), Term.ann (loc scrutineeType) patTerm scrutineeType)] rhs' - entireCase = foldr (\locv t -> Term.let1 [(locv, Term.blank (fst locv))] t) newBody (Foldable.toList pat `zip` vs) + entireCase = + foldr (\locv t -> Term.let1 [(locv, Term.placeholder (fst locv))] t) + newBody + (Foldable.toList pat `zip` vs) in check entireCase outputType bindings :: Context v loc -> [(v, Type v loc)] @@ -737,7 +740,8 @@ check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> if wellformedType ctx t then let go :: Term v loc -> Type v loc -> M v loc () - go Term.Blank' _ = pure () -- somewhat hacky short circuit; blank checks successfully against all types + go (Term.Blank' _) _ = error "TODO" + --pure () -- somewhat hacky short circuit; blank checks successfully against all types go _ (Type.Forall' body) = do -- ForallI x <- extendUniversal =<< ABT.freshen body freshenTypeVar check e (ABT.bindInheritAnnotation body (Type.universal x)) From 8a6850ec189e08d4981078753ac52b27f7348e53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=BAnar=20=C3=93li=20Bjarnason?= Date: Tue, 31 Jul 2018 15:07:32 -0400 Subject: [PATCH 02/11] wip --- parser-typechecker/src/Unison/Blank.hs | 11 +++++ parser-typechecker/src/Unison/Term.hs | 10 +---- parser-typechecker/src/Unison/Type.hs | 39 +++++++++-------- parser-typechecker/src/Unison/TypeVar.hs | 27 ++++++++---- .../src/Unison/Typechecker/Context.hs | 43 ++++++++++--------- .../unison-parser-typechecker.cabal | 1 + 6 files changed, 74 insertions(+), 57 deletions(-) create mode 100644 parser-typechecker/src/Unison/Blank.hs diff --git a/parser-typechecker/src/Unison/Blank.hs b/parser-typechecker/src/Unison/Blank.hs new file mode 100644 index 000000000..ba1bd5e10 --- /dev/null +++ b/parser-typechecker/src/Unison/Blank.hs @@ -0,0 +1,11 @@ +module Unison.Blank where + +data Blank + -- An expression that has not been filled in, has type `forall a . a`. + = Placeholder + -- A user-provided typed hole + | Remember String + -- A name to be resolved with type-directed name resolution. + | Resolve String + deriving (Show, Eq, Ord) + diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index ccf914afd..085404d6f 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -29,6 +29,7 @@ import GHC.Generics import Prelude.Extras (Eq1(..), Show1(..)) import Text.Show import qualified Unison.ABT as ABT +import Unison.Blank import Unison.Hash (Hash) import qualified Unison.Hash as Hash import Unison.Hashable (Hashable1, accumulateToken) @@ -46,15 +47,6 @@ import Unsafe.Coerce data MatchCase loc a = MatchCase (Pattern loc) (Maybe a) a deriving (Show,Eq,Foldable,Functor,Generic,Generic1,Traversable) -data Blank - -- An expression that has not been filled in, has type `forall a . a`. - = Placeholder - -- A user-provided typed hole - | Remember String - -- A name to be resolved with type-directed name resolution. - | Resolve String - deriving (Show, Eq, Ord) - -- | Base functor for terms in the Unison language -- We need `typeVar` because the term and type variables may differ. data F typeVar typeAnn patternAnn a diff --git a/parser-typechecker/src/Unison/Type.hs b/parser-typechecker/src/Unison/Type.hs index e2e389502..203c9ee2b 100644 --- a/parser-typechecker/src/Unison/Type.hs +++ b/parser-typechecker/src/Unison/Type.hs @@ -9,21 +9,22 @@ module Unison.Type where -import Data.List -import Data.Set (Set) -import Data.Text (Text) -import GHC.Generics -import Prelude.Extras (Eq1(..),Show1(..)) -import Unison.Hashable (Hashable1) -import Unison.Reference (Reference) -import Unison.TypeVar (TypeVar) -import Unison.Var (Var) +import Data.List +import Data.Set (Set) import qualified Data.Set as Set +import Data.Text (Text) +import GHC.Generics +import Prelude.Extras (Eq1(..),Show1(..)) import qualified Unison.ABT as ABT +import Unison.Blank +import Unison.Hashable (Hashable1) import qualified Unison.Hashable as Hashable import qualified Unison.Kind as K +import Unison.Reference (Reference) import qualified Unison.Reference as Reference +import Unison.TypeVar (TypeVar) import qualified Unison.TypeVar as TypeVar +import Unison.Var (Var) import qualified Unison.Var as Var -- | Base functor for types in the Unison language @@ -91,7 +92,7 @@ pattern Effect'' es t <- (stripEffect -> (es, t)) pattern Forall' subst <- ABT.Tm' (Forall (ABT.Abs' subst)) pattern ForallNamed' v body <- ABT.Tm' (Forall (ABT.out -> ABT.Abs v body)) pattern Var' v <- ABT.Var' v -pattern Existential' v <- ABT.Var' (TypeVar.Existential v) +pattern Existential' b v <- ABT.Var' (TypeVar.Existential b v) pattern Universal' v <- ABT.Var' (TypeVar.Universal v) unArrows :: Type v -> Maybe [Type v] @@ -107,11 +108,11 @@ unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args) go (App' i o) acc = go i (o:acc) go fn args = fn:args -matchExistential :: Eq v => v -> Type (TypeVar v) -> Bool -matchExistential v (Existential' x) = x == v +matchExistential :: Eq v => v -> Type (TypeVar b v) -> Bool +matchExistential v (Existential' _ x) = x == v matchExistential _ _ = False -matchUniversal :: Eq v => v -> Type (TypeVar v) -> Bool +matchUniversal :: Eq v => v -> Type (TypeVar b v) -> Bool matchUniversal v (Universal' x) = x == v matchUniversal _ _ = False @@ -194,16 +195,16 @@ andor' a = arrows (f <$> [boolean a, boolean a]) $ boolean a var :: Ord v => a -> v -> AnnotatedType v a var = ABT.annotatedVar -existential :: Ord v => v -> Type (TypeVar v) -existential v = ABT.var (TypeVar.Existential v) +existential :: Ord v => v -> Type (TypeVar Blank v) +existential v = ABT.var (TypeVar.Existential Placeholder v) -universal :: Ord v => v -> Type (TypeVar v) +universal :: Ord v => v -> Type (TypeVar b v) universal v = ABT.var (TypeVar.Universal v) -existential' :: Ord v => a -> v -> AnnotatedType (TypeVar v) a -existential' a v = ABT.annotatedVar a (TypeVar.Existential v) +existential' :: Ord v => a -> v -> AnnotatedType (TypeVar Blank v) a +existential' a v = ABT.annotatedVar a (TypeVar.Existential Placeholder v) -universal' :: Ord v => a -> v -> AnnotatedType (TypeVar v) a +universal' :: Ord v => a -> v -> AnnotatedType (TypeVar b v) a universal' a v = ABT.annotatedVar a (TypeVar.Universal v) v' :: Var v => Text -> Type v diff --git a/parser-typechecker/src/Unison/TypeVar.hs b/parser-typechecker/src/Unison/TypeVar.hs index 3ccc40f8f..2d122943d 100644 --- a/parser-typechecker/src/Unison/TypeVar.hs +++ b/parser-typechecker/src/Unison/TypeVar.hs @@ -2,23 +2,34 @@ module Unison.TypeVar where -import Unison.Var (Var) import qualified Data.Set as Set +import Unison.Var (Var) import qualified Unison.Var as Var -data TypeVar v = Universal v | Existential v deriving (Eq,Ord,Functor) +data TypeVar b v = Universal v | Existential b v deriving (Functor) -underlying :: TypeVar v -> v +instance Eq v => Eq (TypeVar b v) where + Universal v == Universal v2 = v == v2 + Existential _ v == Existential _ v2 = v == v2 + _ == _ = False + +instance Ord v => Ord (TypeVar b v) where + Universal v `compare` Universal v2 = compare v v2 + Existential _ v `compare` Existential _ v2 = compare v v2 + Universal _ `compare` Existential _ _ = LT + _ `compare` _ = GT + +underlying :: TypeVar b v -> v underlying (Universal v) = v -underlying (Existential v) = v +underlying (Existential _ v) = v -instance Show v => Show (TypeVar v) where +instance Show v => Show (TypeVar b v) where show (Universal v) = show v - show (Existential v) = "'" ++ show v + show (Existential _ v) = "'" ++ show v -instance Var v => Var (TypeVar v) where +instance (Ord b, Var v) => Var (TypeVar b v) where rename n (Universal v) = Universal (Var.rename n v) - rename n (Existential v) = Existential (Var.rename n v) + rename n (Existential b v) = Existential b (Var.rename n v) named txt = Universal (Var.named txt) name v = Var.name (underlying v) qualifiedName v = Var.qualifiedName (underlying v) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index cdef9f677..5b15c6e98 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -8,37 +8,37 @@ module Unison.Typechecker.Context (synthesizeClosed, Note(..), Cause(..), PathElement(..)) where -import Data.Sequence (Seq) - import Control.Monad import Control.Monad.Loops (anyM, allM) import Control.Monad.State (State, get, put, evalState) import qualified Data.Foldable as Foldable -import Data.Maybe import Data.List import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe +import Data.Sequence (Seq) import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text as Text import Debug.Trace import qualified Unison.ABT as ABT +import Unison.Blank import Unison.DataDeclaration (DataDeclaration', EffectDeclaration') import qualified Unison.DataDeclaration as DD import Unison.PatternP (Pattern) import qualified Unison.PatternP as Pattern import Unison.Reference (Reference) -import qualified Unison.Term as Term import Unison.Term (AnnotatedTerm') +import qualified Unison.Term as Term import Unison.Type (AnnotatedType) import qualified Unison.Type as Type -import Unison.TypeVar (TypeVar) import qualified Unison.TypeVar as TypeVar import Unison.Typechecker.Components (minimize') import Unison.Var (Var) import qualified Unison.Var as Var +type TypeVar v = TypeVar.TypeVar Blank v type Type v loc = AnnotatedType (TypeVar v) loc type Term v loc = AnnotatedTerm' (TypeVar v) v loc type Monotype v loc = Type.Monotype (TypeVar v) loc @@ -46,15 +46,14 @@ type Monotype v loc = Type.Monotype (TypeVar v) loc pattern Universal v <- Var (TypeVar.Universal v) where Universal v = Var (TypeVar.Universal v) -pattern Existential v <- Var (TypeVar.Existential v) where - Existential v = Var (TypeVar.Existential v) +pattern Existential b v = Var (TypeVar.Existential b v) -- | Elements of an ordered algorithmic context data Element v loc - = Var (TypeVar v) -- A variable declaration + = Var (TypeVar v) -- A variable declaration | Solved v (Monotype v loc) -- `v` is solved to some monotype | Ann v (Type v loc) -- `v` has type `a`, which may be quantified - | Marker v deriving (Eq) -- used for scoping + | Marker v deriving (Eq) -- used for scoping data Env v loc = Env { freshId :: Word, ctx :: Context v loc } @@ -166,7 +165,7 @@ solved :: Context v loc -> [(v, Monotype v loc)] solved (Context ctx) = [(v, sa) | (Solved v sa, _) <- ctx] unsolved :: Context v loc -> [v] -unsolved (Context ctx) = [v | (Existential v, _) <- ctx] +unsolved (Context ctx) = [v | (Existential _ v, _) <- ctx] replace :: Var v => Element v loc -> Context v loc -> Context v loc -> Context v loc replace e focus ctx = @@ -179,16 +178,16 @@ breakAt m (Context xs) = (r, l) = break (\(e,_) -> e === m) xs -- l is a suffix of xs and is already a valid context; -- r needs to be rebuilt - Existential v === Existential v2 | v == v2 = True - Universal v === Universal v2 | v == v2 = True - Marker v === Marker v2 | v == v2 = True + Existential _ v === Existential _ v2 | v == v2 = True + Universal v === Universal v2 | v == v2 = True + Marker v === Marker v2 | v == v2 = True _ === _ = False in (Context (drop 1 l), context . map fst $ reverse r) -- | ordered Γ α β = True <=> Γ[α^][β^] ordered :: Var v => Context v loc -> v -> v -> Bool -ordered ctx v v2 = Set.member v (existentials (retract' (Existential v2) ctx)) +ordered ctx v v2 = Set.member v (existentials (retract' (Existential Placeholder v2) ctx)) -- env0 :: Env v loc -- env0 = Env 0 context0 @@ -265,7 +264,7 @@ wellformed ctx = isWellformed (info ctx) -- | Check that the type is well formed wrt the given `Context`, see Figure 7 of paper wellformedType :: Var v => Context v loc -> Type v loc -> Bool wellformedType c t = wellformed c && case t of - Type.Existential' v -> Set.member v (existentials c) + Type.Existential' _ v -> Set.member v (existentials c) Type.Universal' v -> Set.member v (universals c) Type.Ref' _ -> True Type.Arrow' i o -> wellformedType c i && wellformedType c o @@ -297,7 +296,7 @@ extend e c@(Context ctx) = Context ((e,i'):ctx) where -- UvarCtx - ensure no duplicates TypeVar.Universal v -> Info es (Set.insert v us) (Set.insert v vs) (ok && Set.notMember v us) -- EvarCtx - ensure no duplicates, and that this existential is not solved earlier in context - TypeVar.Existential v -> Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es) + TypeVar.Existential _ v -> Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es) -- SolvedEvarCtx - ensure `v` is fresh, and the solution is well-formed wrt the context Solved v sa -> Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es && wellformedType c (Type.getPolytype sa)) @@ -388,18 +387,20 @@ extendMarker :: Var v => v -> M v loc v extendMarker v = do v' <- freshenVar v modifyContext (\ctx -> pure $ ctx `mappend` - (context [Marker v', Existential v'])) + (context [Marker v', Existential Placeholder v'])) pure v' notMember :: Var v => v -> Set (TypeVar v) -> Bool -notMember v s = Set.notMember (TypeVar.Universal v) s && Set.notMember (TypeVar.Existential v) s +notMember v s = + Set.notMember (TypeVar.Universal v) s && + Set.notMember (TypeVar.Existential Placeholder v) s -- | Replace any existentials with their solution in the context apply :: Var v => Context v loc -> Type v loc -> Type v loc apply ctx t = case t of Type.Universal' _ -> t Type.Ref' _ -> t - Type.Existential' v -> + Type.Existential' _ v -> maybe t (\(Type.Monotype t') -> apply ctx t') (lookup v (solved ctx)) Type.Arrow' i o -> Type.arrow a (apply ctx i) (apply ctx o) Type.App' x y -> Type.app a (apply ctx x) (apply ctx y) @@ -963,8 +964,8 @@ solve ctx v t solve ctx v t | wellformedType ctxL (Type.getPolytype t) = Just ctx' | otherwise = Nothing - where (ctxL,ctxR) = breakAt (Existential v) ctx - ctx' = ctxL `mappend` context [Solved v t] `mappend` ctxR + where (ctxL,ctxR) = breakAt (Existential v blah) ctx + ctx' = ctxL `mappend` context [Solved blah v t] `mappend` ctxR abilityCheck' :: Var v => [Type v loc] -> [Type v loc] -> M v loc () abilityCheck' ambient requested = do diff --git a/parser-typechecker/unison-parser-typechecker.cabal b/parser-typechecker/unison-parser-typechecker.cabal index 58189c84f..10eccf4ad 100644 --- a/parser-typechecker/unison-parser-typechecker.cabal +++ b/parser-typechecker/unison-parser-typechecker.cabal @@ -35,6 +35,7 @@ library exposed-modules: Unison.ABT + Unison.Blank Unison.Builtin Unison.Codecs Unison.DataDeclaration From ace2ce0ee0d490d60973dd7bc680e0ebe745f1a8 Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 31 Jul 2018 16:37:31 -0400 Subject: [PATCH 03/11] finished plumbing extra Blank info through existentials of the typechecker; all tests passing --- parser-typechecker/src/Unison/TermParser.hs | 2 +- parser-typechecker/src/Unison/Type.hs | 11 +- .../src/Unison/Typechecker/Context.hs | 255 ++++++++++-------- 3 files changed, 144 insertions(+), 124 deletions(-) diff --git a/parser-typechecker/src/Unison/TermParser.hs b/parser-typechecker/src/Unison/TermParser.hs index 86adb6d6f..01442243c 100644 --- a/parser-typechecker/src/Unison/TermParser.hs +++ b/parser-typechecker/src/Unison/TermParser.hs @@ -106,7 +106,7 @@ parsePattern = constructor <|> leaf (\(p, vs) -> (Pattern.As (ann v) p, tokenToPair v : vs)) <$> leaf else pure (Pattern.Var (ann v), [tokenToPair v]) unbound :: P v (Pattern Ann, [(Ann, v)]) - unbound = (\tok -> (Pattern.Unbound (ann tok), [])) <$> reserved "_" + unbound = (\tok -> (Pattern.Unbound (ann tok), [])) <$> blank ctorName = P.try $ do s <- wordyId guard . isUpper . head . L.payload $ s diff --git a/parser-typechecker/src/Unison/Type.hs b/parser-typechecker/src/Unison/Type.hs index 203c9ee2b..4342e1bce 100644 --- a/parser-typechecker/src/Unison/Type.hs +++ b/parser-typechecker/src/Unison/Type.hs @@ -195,14 +195,17 @@ andor' a = arrows (f <$> [boolean a, boolean a]) $ boolean a var :: Ord v => a -> v -> AnnotatedType v a var = ABT.annotatedVar -existential :: Ord v => v -> Type (TypeVar Blank v) -existential v = ABT.var (TypeVar.Existential Placeholder v) +existential :: Ord v => Blank -> v -> Type (TypeVar Blank v) +existential blank v = ABT.var (TypeVar.Existential blank v) universal :: Ord v => v -> Type (TypeVar b v) universal v = ABT.var (TypeVar.Universal v) -existential' :: Ord v => a -> v -> AnnotatedType (TypeVar Blank v) a -existential' a v = ABT.annotatedVar a (TypeVar.Existential Placeholder v) +existentialp :: Ord v => a -> v -> AnnotatedType (TypeVar Blank v) a +existentialp a v = existential' a Placeholder v + +existential' :: Ord v => a -> Blank -> v -> AnnotatedType (TypeVar Blank v) a +existential' a blank v = ABT.annotatedVar a (TypeVar.Existential blank v) universal' :: Ord v => a -> v -> AnnotatedType (TypeVar b v) a universal' a v = ABT.annotatedVar a (TypeVar.Universal v) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 5b15c6e98..8eebb642f 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -43,15 +43,16 @@ type Type v loc = AnnotatedType (TypeVar v) loc type Term v loc = AnnotatedTerm' (TypeVar v) v loc type Monotype v loc = Type.Monotype (TypeVar v) loc -pattern Universal v <- Var (TypeVar.Universal v) where - Universal v = Var (TypeVar.Universal v) - +pattern Universal v = Var (TypeVar.Universal v) pattern Existential b v = Var (TypeVar.Existential b v) +existential :: v -> Element v loc +existential v = Existential Placeholder v + -- | Elements of an ordered algorithmic context data Element v loc = Var (TypeVar v) -- A variable declaration - | Solved v (Monotype v loc) -- `v` is solved to some monotype + | Solved Blank v (Monotype v loc) -- `v` is solved to some monotype | Ann v (Type v loc) -- `v` has type `a`, which may be quantified | Marker v deriving (Eq) -- used for scoping @@ -88,12 +89,17 @@ data PathElement v loc | InSynthesizeApp (Type v loc) (Term v loc) deriving Show +type ExpectedArgCount = Int +type ActualArgCount = Int +type ConstructorId = Int + data Cause v loc = TypeMismatch (Context v loc) | IllFormedType (Context v loc) | UnknownSymbol loc v | CompilerBug (CompilerBug v loc) | AbilityCheckFailure [Type v loc] [Type v loc] -- ambient, requested + | EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount Reference ConstructorId deriving Show data Note v loc = Note { cause :: Cause v loc, path :: Seq (PathElement v loc) } deriving Show @@ -162,17 +168,20 @@ retract' :: Var v => Element v loc -> Context v loc -> Context v loc retract' e ctx = fromMaybe mempty $ retract e ctx solved :: Context v loc -> [(v, Monotype v loc)] -solved (Context ctx) = [(v, sa) | (Solved v sa, _) <- ctx] +solved (Context ctx) = [(v, sa) | (Solved _ v sa, _) <- ctx] unsolved :: Context v loc -> [v] unsolved (Context ctx) = [v | (Existential _ v, _) <- ctx] replace :: Var v => Element v loc -> Context v loc -> Context v loc -> Context v loc replace e focus ctx = - let (l,r) = breakAt e ctx + let (l,_,r) = breakAt e ctx in l `mappend` focus `mappend` r -breakAt :: Var v => Element v loc -> Context v loc -> (Context v loc, Context v loc) +breakAt :: Var v + => Element v loc + -> Context v loc + -> (Context v loc, [Element v loc], Context v loc) breakAt m (Context xs) = let (r, l) = break (\(e,_) -> e === m) xs @@ -182,12 +191,12 @@ breakAt m (Context xs) = Universal v === Universal v2 | v == v2 = True Marker v === Marker v2 | v == v2 = True _ === _ = False - in (Context (drop 1 l), context . map fst $ reverse r) + in (Context (drop 1 l), fst <$> take 1 l, context . map fst $ reverse r) -- | ordered Γ α β = True <=> Γ[α^][β^] ordered :: Var v => Context v loc -> v -> v -> Bool -ordered ctx v v2 = Set.member v (existentials (retract' (Existential Placeholder v2) ctx)) +ordered ctx v v2 = Set.member v (existentials (retract' (existential v2) ctx)) -- env0 :: Env v loc -- env0 = Env 0 context0 @@ -294,14 +303,18 @@ extend e c@(Context ctx) = Context ((e,i'):ctx) where addInfo e (Info es us vs ok) = case e of Var v -> case v of -- UvarCtx - ensure no duplicates - TypeVar.Universal v -> Info es (Set.insert v us) (Set.insert v vs) (ok && Set.notMember v us) + TypeVar.Universal v -> + Info es (Set.insert v us) (Set.insert v vs) (ok && Set.notMember v us) -- EvarCtx - ensure no duplicates, and that this existential is not solved earlier in context - TypeVar.Existential _ v -> Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es) + TypeVar.Existential _ v -> + Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es) -- SolvedEvarCtx - ensure `v` is fresh, and the solution is well-formed wrt the context - Solved v sa -> Info (Set.insert v es) us (Set.insert v vs) (ok && Set.notMember v es - && wellformedType c (Type.getPolytype sa)) + Solved _ v sa -> + Info (Set.insert v es) us (Set.insert v vs) + (ok && Set.notMember v es && wellformedType c (Type.getPolytype sa)) -- VarCtx - ensure `v` is fresh, and annotation is well-formed wrt the context - Ann v t -> Info es us (Set.insert v vs) (ok && Set.notMember v vs && wellformedType c t) + Ann v t -> + Info es us (Set.insert v vs) (ok && Set.notMember v vs && wellformedType c t) -- MarkerCtx - note that since a Marker is always the first mention of a variable, suffices to -- just check that `v` is not previously mentioned Marker v -> Info es us (Set.insert v vs) (ok && Set.notMember v vs) @@ -387,7 +400,7 @@ extendMarker :: Var v => v -> M v loc v extendMarker v = do v' <- freshenVar v modifyContext (\ctx -> pure $ ctx `mappend` - (context [Marker v', Existential Placeholder v'])) + (context [Marker v', existential v'])) pure v' notMember :: Var v => v -> Set (TypeVar v) -> Bool @@ -432,8 +445,8 @@ synthesizeApp :: Var v => Type v loc -> Term v loc -> M v loc (Type v loc) synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where go (Type.Forall' body) = do -- Forall1App v <- ABT.freshen body freshenTypeVar - appendContext (context [Existential v]) - synthesizeApp (ABT.bindInheritAnnotation body (Type.existential v)) arg + appendContext (context [existential v]) + synthesizeApp (ABT.bindInheritAnnotation body (Type.existential Placeholder v)) arg go (Type.Arrow' i o) = do -- ->App let (es, _) = Type.stripEffect o abilityCheck es @@ -441,13 +454,13 @@ synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where -- note - the location on this Type.effect isn't really used for anything, -- and won't be reported to the user o <$ check arg (Type.effect (loc ft) ambientEs i) - go (Type.Existential' a) = do -- a^App + go (Type.Existential' b a) = do -- a^App [i,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"] - let it = Type.existential' (loc ft) i - ot = Type.existential' (loc ft) o + let it = Type.existential' (loc ft) Placeholder i + ot = Type.existential' (loc ft) Placeholder o soln = Type.Monotype (Type.arrow (loc ft) it ot) - ctxMid = context [Existential o, Existential i, Solved a soln] - modifyContext' $ replace (Existential a) ctxMid + ctxMid = context [existential o, existential i, Solved b a soln] + modifyContext' $ replace (existential a) ctxMid ot <$ check arg it go _ = getContext >>= \ctx -> failWith $ TypeMismatch ctx @@ -472,10 +485,10 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var Nothing -> compilerCrash $ UndeclaredTermVariable v ctx Just t -> pure t - go (Term.Blank' _) = error "TODO" - -- v <- freshNamed "_" - -- appendContext $ context [Existential v] - -- pure $ Type.existential' l v -- forall (TypeVar.Universal v) (Type.universal v) + go (Term.Blank' blank) = do + v <- freshNamed "_" + appendContext $ context [Existential blank v] + pure $ Type.existential' l blank v -- forall (TypeVar.Universal v) (Type.universal v) go (Term.Ann' (Term.Ref' _) t) = case ABT.freeVars t of s | Set.null s -> -- innermost Ref annotation assumed to be correctly provided by `synthesizeClosed` @@ -488,11 +501,11 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) if Type.arity t == 0 then do a <- freshNamed "a" - appendContext $ context [Marker a, Existential a] + appendContext $ context [Marker a, existential a] ambient <- getAbilities let l = loc t -- arya: we should revisit these l's too - subtype t (Type.effect l ambient (Type.existential' l a)) + subtype t (Type.effect l ambient (Type.existential' l Placeholder a)) -- modifyContext $ retract [Marker a] pure t else pure t @@ -543,13 +556,13 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.Lam' body) = do -- ->I=> (Full Damas Milner rule) -- arya: are there more meaningful locations we could put into and pull out of the abschain?) [arg, i, o] <- sequence [ABT.freshen body freshenVar, freshVar, freshVar] - let it = Type.existential' l i - ot = Type.existential' l o + let it = Type.existential' l Placeholder i + ot = Type.existential' l Placeholder o appendContext $ - context [Marker i, Existential i, Existential o, Ann arg it] + context [Marker i, existential i, existential o, Ann arg it] body <- pure $ ABT.bindInheritAnnotation body (Term.var() arg) check body ot - (ctx1, ctx2) <- breakAt (Marker i) <$> getContext + (ctx1, _, ctx2) <- breakAt (Marker i) <$> getContext -- unsolved existentials get generalized to universals setContext ctx1 pure $ generalizeExistentials ctx2 (Type.arrow l it ot) @@ -557,7 +570,7 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.LetRec' letrec) = do (marker, e) <- annotateLetRecBindings letrec t <- synthesize e - (ctx, ctx2) <- breakAt marker <$> getContext + (ctx, _, ctx2) <- breakAt marker <$> getContext generalizeExistentials ctx2 t <$ setContext ctx go (Term.If' cond t f) = foldM synthesizeApp (Type.iff' l) [cond, t, f] go (Term.And' a b) = foldM synthesizeApp (Type.andor' l) [a, b] @@ -571,30 +584,28 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.EffectBind' r cid args k) = do cType <- getEffectConstructorType r cid let arity = Type.arity cType - -- TODO: error message algebra - when (length args /= arity) . fail $ - "Effect constructor wanted " <> show arity <> " arguments " <> "but got " - <> show (length args) + when (length args /= arity) . failWith $ + EffectConstructorWrongArgCount arity (length args) r cid ([eType], iType) <- Type.stripEffect <$> withoutAbilityCheck (foldM synthesizeApp cType args) rTypev <- freshNamed "result" - let rType = Type.existential' l rTypev - appendContext $ context [Existential rTypev] + let rType = Type.existential' l Placeholder rTypev + appendContext $ context [existential rTypev] check k (Type.arrow l iType (Type.effect l [eType] rType)) ctx <- getContext pure $ apply ctx (Type.effectV l (l, eType) (l, rType)) go (Term.Match' scrutinee cases) = do scrutineeType <- synthesize scrutinee outputTypev <- freshenVar (Var.named "match-output") - let outputType = Type.existential' l outputTypev - appendContext $ context [Existential outputTypev] + let outputType = Type.existential' l Placeholder outputTypev + appendContext $ context [existential outputTypev] Foldable.traverse_ (checkCase scrutineeType outputType) cases ctx <- getContext pure $ apply ctx outputType go h@(Term.Handle' _ _) = do o <- freshNamed "o" - appendContext $ context [Existential o] - let ot = Type.existential' l o + appendContext $ context [existential o] + let ot = Type.existential' l Placeholder o check h ot ctx <- getContext pure (apply ctx ot) @@ -704,16 +715,17 @@ annotateLetRecBindings letrec = do -- TODO: Think about whether `apply` here is always correct -- Used to have a guard that would only do this if t had no free vars Term.Ann' _ t -> apply ctx t - _ -> Type.existential' (loc binding) e + _ -> Type.existential' (loc binding) Placeholder e let bindingTypes = zipWith f es bindings - appendContext $ context (Marker e1 : map Existential es ++ zipWith Ann vs bindingTypes) + appendContext $ context (Marker e1 : map existential es ++ zipWith Ann vs bindingTypes) -- check each `bi` against `ei`; sequencing resulting contexts Foldable.for_ (zip bindings bindingTypes) $ \((_,b), t) -> check b t -- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`; -- add annotations `v1 : gt1, v2 : gt2 ...` to the context - (ctx1, ctx2) <- breakAt (Marker e1) <$> getContext + (ctx1, _, ctx2) <- breakAt (Marker e1) <$> getContext -- The location of the existential is just the location of the binding - let gen (e,(_,binding)) = generalizeExistentials ctx2 (Type.existential' (loc binding) e) + let gen (e,(_,binding)) = generalizeExistentials ctx2 + (Type.existential' (loc binding) Placeholder e) let annotations = zipWith Ann vs (map gen (es `zip` bindings)) marker <- Marker <$> freshenVar (ABT.v' "let-rec-marker") setContext (ctx1 `mappend` context (marker : annotations)) @@ -726,11 +738,16 @@ generalizeExistentials ctx t = foldr gen (apply ctx t) (unsolved ctx) where gen e t = - if TypeVar.Existential e `ABT.isFreeIn` t + if TypeVar.Existential Placeholder e `ABT.isFreeIn` t -- location of the forall is just the location of the input type -- and the location of each quantified variable is just inherited from -- its source location - then Type.forall (loc t) (TypeVar.Universal e) (ABT.substInheritAnnotation (TypeVar.Existential e) (Type.universal e) t) + then Type.forall (loc t) + (TypeVar.Universal e) + (ABT.substInheritAnnotation + (TypeVar.Existential Placeholder e) + (Type.universal e) + t) else t -- don't bother introducing a forall if type variable is unused -- | Check that under the given context, `e` has type `t`, @@ -741,8 +758,6 @@ check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> if wellformedType ctx t then let go :: Term v loc -> Type v loc -> M v loc () - go (Term.Blank' _) _ = error "TODO" - --pure () -- somewhat hacky short circuit; blank checks successfully against all types go _ (Type.Forall' body) = do -- ForallI x <- extendUniversal =<< ABT.freshen body freshenTypeVar check e (ABT.bindInheritAnnotation body (Type.universal x)) @@ -769,15 +784,15 @@ check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> -- `body` should check against `i` builtinLoc <- getBuiltinLocation [e, i] <- sequence [freshNamed "e", freshNamed "i"] - appendContext $ context [Existential e, Existential i] + appendContext $ context [existential e, existential i] let l = loc block - check h $ Type.arrow l (Type.effectV builtinLoc (l, Type.existential' l e) (l, Type.existential' l i)) t + check h $ Type.arrow l (Type.effectV builtinLoc (l, Type.existentialp l e) (l, Type.existentialp l i)) t ctx <- getContext let Type.Effect'' requested _ = apply ctx t abilityCheck requested - withEffects [apply ctx $ Type.existential' l e] $ do + withEffects [apply ctx $ Type.existentialp l e] $ do ambient <- getAbilities - let (_, i') = Type.stripEffect (apply ctx (Type.existential' l i)) + let (_, i') = Type.stripEffect (apply ctx (Type.existentialp l i)) -- arya: we should revisit these `l`s once we have this up and running check body (Type.effect l ambient i') pure () @@ -790,7 +805,7 @@ check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> e = minimize' e0 in case t of -- expand existentials before checking - t@(Type.Existential' _) -> go e (apply ctx t) + t@(Type.Existential' _ _) -> go e (apply ctx t) t -> go e t else failWith $ IllFormedType ctx @@ -806,7 +821,7 @@ subtype tx ty = scope (InSubtype tx ty) $ go ctx t1@(Type.Universal' v1) t2@(Type.Universal' v2) -- `Var` | v1 == v2 && wellformedType ctx t1 && wellformedType ctx t2 = pure () - go ctx t1@(Type.Existential' v1) t2@(Type.Existential' v2) -- `Exvar` + go ctx t1@(Type.Existential' _ v1) t2@(Type.Existential' _ v2) -- `Exvar` | v1 == v2 && wellformedType ctx t1 && wellformedType ctx t2 = pure () go _ (Type.Arrow' i1 o1) (Type.Arrow' i2 o2) = do -- `-->` @@ -822,18 +837,18 @@ subtype tx ty = scope (InSubtype tx ty) $ doRetract (Universal v') go _ (Type.Forall' t) t2 = do v <- extendMarker =<< ABT.freshen t freshenTypeVar - t <- pure $ ABT.bindInheritAnnotation t (Type.existential v) + t <- pure $ ABT.bindInheritAnnotation t (Type.existential Placeholder v) ctx' <- getContext subtype (apply ctx' t) t2 doRetract (Marker v) go _ (Type.Effect' [] a1) a2 = subtype a1 a2 go _ a1 (Type.Effect' [] a2) = subtype a1 a2 - go ctx (Type.Existential' v) t -- `InstantiateL` + go ctx (Type.Existential' b v) t -- `InstantiateL` | Set.member v (existentials ctx) && notMember v (Type.freeVars t) = - instantiateL v t - go ctx t (Type.Existential' v) -- `InstantiateR` + instantiateL b v t + go ctx t (Type.Existential' b v) -- `InstantiateR` | Set.member v (existentials ctx) && notMember v (Type.freeVars t) = - instantiateR t v + instantiateR t b v go _ (Type.Effect'' es1 a1) (Type.Effect' es2 a2) = do subtype a1 a2 ctx <- getContext @@ -846,109 +861,110 @@ subtype tx ty = scope (InSubtype tx ty) $ -- | Instantiate the given existential such that it is -- a subtype of the given type, updating the context -- in the process. -instantiateL :: Var v => v -> Type v loc -> M v loc () -instantiateL v t | debugEnabled && traceShow ("instantiateL"::String, v, t) False = undefined -instantiateL v t = scope (InInstantiateL v t) $ +instantiateL :: Var v => Blank -> v -> Type v loc -> M v loc () +instantiateL _ v t | debugEnabled && traceShow ("instantiateL"::String, v, t) False = undefined +instantiateL blank v t = scope (InInstantiateL v t) $ getContext >>= \ctx -> case Type.monotype t >>= (solve ctx v) of Just ctx -> setContext ctx -- InstLSolve Nothing -> case t of - Type.Existential' v2 | ordered ctx v v2 -> -- InstLReach (both are existential, set v2 = v) + Type.Existential' _ v2 | ordered ctx v v2 -> -- InstLReach (both are existential, set v2 = v) maybe (failWith $ TypeMismatch ctx) setContext $ - solve ctx v2 (Type.Monotype (Type.existential' (loc t) v)) + solve ctx v2 (Type.Monotype (Type.existentialp (loc t) v)) Type.Arrow' i o -> do -- InstLArr [i',o'] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"] - let s = Solved v (Type.Monotype (Type.arrow (loc t) - (Type.existential' (loc i) i') - (Type.existential' (loc o) o'))) - modifyContext' $ replace (Existential v) - (context [Existential o', Existential i', s]) - instantiateR i i' + let s = Solved blank v (Type.Monotype (Type.arrow (loc t) + (Type.existentialp (loc i) i') + (Type.existentialp (loc o) o'))) + modifyContext' $ replace (existential v) + (context [existential o', existential i', s]) + instantiateR i Placeholder i' -- todo: not sure about this, could also be `blank` ctx <- getContext - instantiateL o' (apply ctx o) + instantiateL Placeholder o' (apply ctx o) Type.App' x y -> do -- analogue of InstLArr [x', y'] <- traverse freshenVar [ABT.v' "x", ABT.v' "y"] - let s = Solved v (Type.Monotype (Type.app (loc t) - (Type.existential' (loc x) x') - (Type.existential' (loc y) y'))) - modifyContext' $ replace (Existential v) - (context [Existential y', Existential x', s]) + let s = Solved blank v (Type.Monotype (Type.app (loc t) + (Type.existentialp (loc x) x') + (Type.existentialp (loc y) y'))) + modifyContext' $ replace (existential v) + (context [existential y', existential x', s]) ctx0 <- getContext - ctx' <- instantiateL x' (apply ctx0 x) >> getContext - instantiateL y' (apply ctx' y) + ctx' <- instantiateL Placeholder x' (apply ctx0 x) >> getContext + instantiateL Placeholder y' (apply ctx' y) Type.Effect' es vt -> do es' <- replicateM (length es) (freshNamed "e") vt' <- freshNamed "vt" let locs = loc <$> es - s = Solved v (Type.Monotype + s = Solved blank v + (Type.Monotype (Type.effect (loc t) - (uncurry Type.existential' <$> locs `zip` es') - (Type.existential' (loc vt) vt'))) - modifyContext' $ replace (Existential v) - (context $ (Existential <$> es') ++ - [Existential vt', s]) + (uncurry Type.existentialp <$> locs `zip` es') + (Type.existentialp (loc vt) vt'))) + modifyContext' $ replace (existential v) + (context $ (existential <$> es') ++ + [existential vt', s]) Foldable.for_ (es' `zip` es) $ \(e',e) -> do ctx <- getContext - instantiateL e' (apply ctx e) + instantiateL Placeholder e' (apply ctx e) ctx <- getContext - instantiateL vt' (apply ctx vt) + instantiateL Placeholder vt' (apply ctx vt) Type.Forall' body -> do -- InstLIIL v <- extendUniversal =<< ABT.freshen body freshenTypeVar - instantiateL v (ABT.bindInheritAnnotation body (Type.universal v)) + instantiateL Placeholder v (ABT.bindInheritAnnotation body (Type.universal v)) doRetract (Universal v) _ -> failWith $ TypeMismatch ctx -- | Instantiate the given existential such that it is -- a supertype of the given type, updating the context -- in the process. -instantiateR :: Var v => Type v loc -> v -> M v loc () -instantiateR t v | debugEnabled && traceShow ("instantiateR"::String, t, v) False = undefined -instantiateR t v = scope (InInstantiateR t v) $ +instantiateR :: Var v => Type v loc -> Blank -> v -> M v loc () +instantiateR t _ v | debugEnabled && traceShow ("instantiateR"::String, t, v) False = undefined +instantiateR t blank v = scope (InInstantiateR t v) $ getContext >>= \ctx -> case Type.monotype t >>= solve ctx v of Just ctx -> setContext ctx -- InstRSolve Nothing -> case t of - Type.Existential' v2 | ordered ctx v v2 -> -- InstRReach (both are existential, set v2 = v) + Type.Existential' _ v2 | ordered ctx v v2 -> -- InstRReach (both are existential, set v2 = v) maybe (failWith $ TypeMismatch ctx) setContext $ - solve ctx v2 (Type.Monotype (Type.existential' (loc t) v)) + solve ctx v2 (Type.Monotype (Type.existentialp (loc t) v)) Type.Arrow' i o -> do -- InstRArrow [i', o'] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"] - let s = Solved v (Type.Monotype + let s = Solved blank v (Type.Monotype (Type.arrow (loc t) - (Type.existential' (loc i) i') - (Type.existential' (loc o) o'))) - modifyContext' $ replace (Existential v) - (context [Existential o', Existential i', s]) - ctx <- instantiateL i' i >> getContext - instantiateR (apply ctx o) o' + (Type.existentialp (loc i) i') + (Type.existentialp (loc o) o'))) + modifyContext' $ replace (existential v) + (context [existential o', existential i', s]) + ctx <- instantiateL Placeholder i' i >> getContext + instantiateR (apply ctx o) Placeholder o' Type.App' x y -> do -- analogue of InstRArr -- example foo a <: v' will -- 1. create foo', a', add these to the context -- 2. add v' = foo' a' to the context -- 3. recurse to refine the types of foo' and a' [x', y'] <- traverse freshenVar [ABT.v' "x", ABT.v' "y"] - let s = Solved v (Type.Monotype (Type.app (loc t) (Type.existential' (loc x) x') (Type.existential' (loc y) y'))) - modifyContext' $ replace (Existential v) (context [Existential y', Existential x', s]) + let s = Solved blank v (Type.Monotype (Type.app (loc t) (Type.existentialp (loc x) x') (Type.existentialp (loc y) y'))) + modifyContext' $ replace (existential v) (context [existential y', existential x', s]) ctx <- getContext - instantiateR (apply ctx x) x' + instantiateR (apply ctx x) Placeholder x' ctx <- getContext - instantiateR (apply ctx y) y' + instantiateR (apply ctx y) Placeholder y' Type.Effect' es vt -> do es' <- replicateM (length es) (freshNamed "e") vt' <- freshNamed "vt" let locs = loc <$> es - s = Solved v (Type.Monotype - (Type.effect (loc t) - (uncurry Type.existential' <$> locs `zip` es') - (Type.existential' (loc vt) vt'))) - modifyContext' $ replace (Existential v) (context $ (Existential <$> es') ++ [Existential vt', s]) + mt = Type.Monotype (Type.effect (loc t) + (uncurry Type.existentialp <$> locs `zip` es') + (Type.existentialp (loc vt) vt')) + s = Solved blank v mt + modifyContext' $ replace (existential v) (context $ (existential <$> es') ++ [existential vt', s]) Foldable.for_ (es `zip` es') $ \(e, e') -> do ctx <- getContext - instantiateR (apply ctx e) e' + instantiateR (apply ctx e) Placeholder e' ctx <- getContext - instantiateR (apply ctx vt) vt' + instantiateR (apply ctx vt) Placeholder vt' Type.Forall' body -> do -- InstRAIIL x' <- ABT.freshen body freshenTypeVar - setContext $ ctx `mappend` context [Marker x', Existential x'] - instantiateR (ABT.bindInheritAnnotation body (Type.existential x')) v + setContext $ ctx `mappend` context [Marker x', existential x'] + instantiateR (ABT.bindInheritAnnotation body (Type.existential Placeholder x')) Placeholder v doRetract (Marker x') _ -> failWith $ TypeMismatch ctx @@ -964,8 +980,9 @@ solve ctx v t solve ctx v t | wellformedType ctxL (Type.getPolytype t) = Just ctx' | otherwise = Nothing - where (ctxL,ctxR) = breakAt (Existential v blah) ctx - ctx' = ctxL `mappend` context [Solved blah v t] `mappend` ctxR + where (ctxL, focus, ctxR) = breakAt (existential v) ctx + mid = [ Solved blank v t | Existential blank v <- focus ] + ctx' = ctxL `mappend` context mid `mappend` ctxR abilityCheck' :: Var v => [Type v loc] -> [Type v loc] -> M v loc () abilityCheck' ambient requested = do @@ -1057,8 +1074,8 @@ synthesizeClosed' abilities term = do instance (Var v, Show loc) => Show (Element v loc) where show (Var v) = case v of TypeVar.Universal x -> "@" <> show x - TypeVar.Existential x -> "'" ++ show x - show (Solved v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t + TypeVar.Existential _ x -> "'" ++ show x + show (Solved _ v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t show (Ann v t) = Text.unpack (Var.shortName v) ++ " : " ++ show t show (Marker v) = "|"++Text.unpack (Var.shortName v)++"|" From a5e7e96321344af15b6711fd276119b94950d78a Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 31 Jul 2018 17:12:44 -0400 Subject: [PATCH 04/11] Adding some machinery so we can detect and do something about existentials with attached Blanks when they pass out of scope, tests still pass --- .../src/Unison/Typechecker/Context.hs | 31 ++++++++++++------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 8eebb642f..8350a3b1b 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -100,10 +100,15 @@ data Cause v loc | CompilerBug (CompilerBug v loc) | AbilityCheckFailure [Type v loc] [Type v loc] -- ambient, requested | EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount Reference ConstructorId + | SolvedBlank Blank v (Type v loc) deriving Show data Note v loc = Note { cause :: Cause v loc, path :: Seq (PathElement v loc) } deriving Show +solveBlank :: Blank -> v -> Type v loc -> M v loc () +solveBlank blank v typ = + M (\menv -> (pure $ Note (SolvedBlank blank v typ) mempty, Just ((), env menv))) + -- Add `p` onto the end of the `path` of this `Note` scope' :: PathElement v loc -> Note v loc -> Note v loc scope' p (Note cause path) = Note cause (path `mappend` pure p) @@ -146,26 +151,26 @@ context xs = foldl' (flip extend) context0 xs -- | Delete from the end of this context up to and including -- the given `Element`. Returns `Nothing` if the element is not found. -retract :: Var v => Element v loc -> Context v loc -> Maybe (Context v loc) -retract e (Context ctx) = +retract0 :: Var v => Element v loc -> Context v loc -> Maybe (Context v loc, [Element v loc]) +retract0 e (Context ctx) = let maybeTail [] = Nothing maybeTail (_:t) = pure t - -- note: no need to recompute used variables; any suffix of the - -- context snoc list is also a valid context - in Context <$> maybeTail (dropWhile (\(e',_) -> e' /= e) ctx) + (discarded, ctx2) = span (\(e',_) -> e' /= e) ctx + -- note: no need to recompute used variables; any suffix of the + -- context snoc list is also a valid context + go ctx2 = (Context ctx2, fst <$> discarded) + in go <$> maybeTail ctx2 -- | Delete from the end of this context up to and including -- the given `Element`. +-- Example, if input context is `[a, b, c, d, ...]` +-- Retract `d` returns `[a, b, c]` doRetract :: Var v => Element v loc -> M v loc () doRetract e = do ctx <- getContext - case retract e ctx of + case retract0 e ctx of Nothing -> compilerCrash (RetractFailure e ctx) - Just t -> setContext t - --- | Like `retract`, but returns the empty context if retracting would remove all elements. -retract' :: Var v => Element v loc -> Context v loc -> Context v loc -retract' e ctx = fromMaybe mempty $ retract e ctx + Just (t, _discarded) -> setContext t solved :: Context v loc -> [(v, Monotype v loc)] solved (Context ctx) = [(v, sa) | (Solved _ v sa, _) <- ctx] @@ -197,6 +202,10 @@ breakAt m (Context xs) = -- | ordered Γ α β = True <=> Γ[α^][β^] ordered :: Var v => Context v loc -> v -> v -> Bool ordered ctx v v2 = Set.member v (existentials (retract' (existential v2) ctx)) + where + -- | Like `retract`, but returns the empty context if retracting would remove all elements. + retract' :: Var v => Element v loc -> Context v loc -> Context v loc + retract' e ctx = fromMaybe mempty $ (fst <$> retract0 e ctx) -- env0 :: Env v loc -- env0 = Env 0 context0 From 790646fc4151eee480bf0097f4be429c2e6bae8c Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 31 Jul 2018 18:31:32 -0400 Subject: [PATCH 05/11] typechecker surgery to propagate info about solved existentials being tracked, tests still passing --- parser-typechecker/src/Unison/Blank.hs | 7 +- parser-typechecker/src/Unison/Term.hs | 20 +-- parser-typechecker/src/Unison/Type.hs | 10 +- parser-typechecker/src/Unison/TypeVar.hs | 2 +- parser-typechecker/src/Unison/Typechecker.hs | 8 +- .../src/Unison/Typechecker/Context.hs | 116 ++++++++++-------- 6 files changed, 91 insertions(+), 72 deletions(-) diff --git a/parser-typechecker/src/Unison/Blank.hs b/parser-typechecker/src/Unison/Blank.hs index ba1bd5e10..3e235c2ca 100644 --- a/parser-typechecker/src/Unison/Blank.hs +++ b/parser-typechecker/src/Unison/Blank.hs @@ -1,11 +1,10 @@ module Unison.Blank where -data Blank +data Blank loc -- An expression that has not been filled in, has type `forall a . a`. = Placeholder -- A user-provided typed hole - | Remember String + | Remember loc String -- A name to be resolved with type-directed name resolution. - | Resolve String + | Resolve loc String deriving (Show, Eq, Ord) - diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 085404d6f..1e9c0a50b 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -55,7 +55,7 @@ data F typeVar typeAnn patternAnn a | Float Double | Boolean Bool | Text Text - | Blank Blank + | Blank (Blank typeAnn) | Ref Reference -- First argument identifies the data type, -- second argument identifies the constructor @@ -228,11 +228,11 @@ text a = ABT.tm' a . Text placeholder :: Ord v => a -> AnnotatedTerm2 vt at ap v a placeholder a = ABT.tm' a (Blank Placeholder) -remember :: Ord v => a -> String -> AnnotatedTerm2 vt at ap v a -remember a s = ABT.tm' a . Blank $ Remember s +remember :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a +remember a s = ABT.tm' a . Blank $ Remember a s -resolve :: Ord v => a -> String -> AnnotatedTerm2 vt at ap v a -resolve a s = ABT.tm' a . Blank $ Resolve s +resolve :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a +resolve a s = ABT.tm' a . Blank $ Resolve a s constructor :: Ord v => a -> Reference -> Int -> AnnotatedTerm2 vt at ap v a constructor a ref n = ABT.tm' a (Constructor ref n) @@ -447,8 +447,8 @@ instance Var v => Hashable1 (F v a p) where Blank b -> tag 1 : case b of Placeholder -> [tag 0] - Remember s -> [tag 1, Hashable.Text (Text.pack s)] - Resolve s -> [tag 2, Hashable.Text (Text.pack s)] + Remember _ s -> [tag 1, Hashable.Text (Text.pack s)] + Resolve _ s -> [tag 2, Hashable.Text (Text.pack s)] Ref (Reference.Builtin name) -> [tag 2, accumulateToken name] Ref (Reference.Derived _) -> error "handled above, but GHC can't figure this out" App a a2 -> [tag 3, hashed (hash a), hashed (hash a2)] @@ -482,7 +482,7 @@ instance Var v => Hashable1 (F v a p) where instance (Eq a, Var v) => Eq1 (F v a p) where (==#) = (==) instance (Show a, Show p, Var v) => Show1 (F v a p) where showsPrec1 = showsPrec -instance (Var vt, Eq a) => Eq (F vt at p a) where +instance (Var vt, Eq at, Eq a) => Eq (F vt at p a) where Int64 x == Int64 y = x == y UInt64 x == UInt64 y = x == y Float x == Float y = x == y @@ -524,8 +524,8 @@ instance (Var v, Show p, Show a0, Show a) => Show (F v a0 p a) where go _ (Blank b) = case b of Placeholder -> s"_" - Remember r -> s("_" ++ r) - Resolve r -> s r + Remember _ r -> s("_" ++ r) + Resolve _ r -> s r go _ (Ref r) = showsPrec 0 r go _ (Let b body) = showParen True (s"let " <> showsPrec 0 b <> s" in " <> showsPrec 0 body) go _ (LetRec bs body) = showParen True (s"let rec" <> showsPrec 0 bs <> s" in " <> showsPrec 0 body) diff --git a/parser-typechecker/src/Unison/Type.hs b/parser-typechecker/src/Unison/Type.hs index 4342e1bce..45ddf9351 100644 --- a/parser-typechecker/src/Unison/Type.hs +++ b/parser-typechecker/src/Unison/Type.hs @@ -64,9 +64,9 @@ freeVars = ABT.freeVars bindBuiltins :: Var v => [(v, Reference)] -> AnnotatedType v a -> AnnotatedType v a bindBuiltins bs = ABT.substsInheritAnnotation [ (v, ref() r) | (v,r) <- bs ] -data Monotype v a = Monotype { getPolytype :: AnnotatedType v a } deriving (Eq) +data Monotype v a = Monotype { getPolytype :: AnnotatedType v a } deriving Eq -instance (Show a, Var v) => Show (Monotype v a) where +instance (Var v) => Show (Monotype v a) where show = show . getPolytype -- Smart constructor which checks if a `Type` has no `Forall` quantifiers. @@ -195,16 +195,16 @@ andor' a = arrows (f <$> [boolean a, boolean a]) $ boolean a var :: Ord v => a -> v -> AnnotatedType v a var = ABT.annotatedVar -existential :: Ord v => Blank -> v -> Type (TypeVar Blank v) +existential :: Ord v => Blank loc -> v -> Type (TypeVar (Blank loc) v) existential blank v = ABT.var (TypeVar.Existential blank v) universal :: Ord v => v -> Type (TypeVar b v) universal v = ABT.var (TypeVar.Universal v) -existentialp :: Ord v => a -> v -> AnnotatedType (TypeVar Blank v) a +existentialp :: Ord v => a -> v -> AnnotatedType (TypeVar (Blank x) v) a existentialp a v = existential' a Placeholder v -existential' :: Ord v => a -> Blank -> v -> AnnotatedType (TypeVar Blank v) a +existential' :: Ord v => a -> Blank x -> v -> AnnotatedType (TypeVar (Blank x) v) a existential' a blank v = ABT.annotatedVar a (TypeVar.Existential blank v) universal' :: Ord v => a -> v -> AnnotatedType (TypeVar b v) a diff --git a/parser-typechecker/src/Unison/TypeVar.hs b/parser-typechecker/src/Unison/TypeVar.hs index 2d122943d..741a60a4e 100644 --- a/parser-typechecker/src/Unison/TypeVar.hs +++ b/parser-typechecker/src/Unison/TypeVar.hs @@ -27,7 +27,7 @@ instance Show v => Show (TypeVar b v) where show (Universal v) = show v show (Existential _ v) = "'" ++ show v -instance (Ord b, Var v) => Var (TypeVar b v) where +instance Var v => Var (TypeVar b v) where rename n (Universal v) = Universal (Var.rename n v) rename n (Existential b v) = Existential b (Var.rename n v) named txt = Universal (Var.named txt) diff --git a/parser-typechecker/src/Unison/Typechecker.hs b/parser-typechecker/src/Unison/Typechecker.hs index 969b27adb..8bf5f9221 100644 --- a/parser-typechecker/src/Unison/Typechecker.hs +++ b/parser-typechecker/src/Unison/Typechecker.hs @@ -107,7 +107,9 @@ data Env f v loc = Env { -- | Infer the type of a 'Unison.Term', using -- a function to resolve the type of @Ref@ constructors -- contained in that term. -synthesize :: (Monad f, Var v) => Env f v loc -> Term v loc +synthesize :: (Monad f, Var v, Ord loc) + => Env f v loc + -> Term v loc -> f (Result (Note v loc) (Type v loc)) synthesize env t = let go (notes, ot) = Result (Result.Typechecking <$> notes) (ABT.vmap TypeVar.underlying <$> ot) @@ -123,7 +125,7 @@ synthesize env t = -- function to resolve the type of @Ref@ constructors -- contained in the term. Returns @typ@ if successful, -- and a note about typechecking failure otherwise. -check :: (Monad f, Var v) => Env f v loc -> Term v loc -> Type v loc +check :: (Monad f, Var v, Ord loc) => Env f v loc -> Term v loc -> Type v loc -> f (Result (Note v loc) (Type v loc)) check env term typ = synthesize env (Term.ann (ABT.annotation term) term typ) @@ -138,7 +140,7 @@ check env term typ = synthesize env (Term.ann (ABT.annotation term) term typ) -- tweak t = Type.arrow() t t -- | Returns `True` if the expression is well-typed, `False` otherwise -wellTyped :: (Monad f, Var v) => Env f v loc -> Term v loc -> f Bool +wellTyped :: (Monad f, Var v, Ord loc) => Env f v loc -> Term v loc -> f Bool wellTyped env term = isJust . result <$> synthesize env term -- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 8350a3b1b..ac5f2258f 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -38,10 +38,10 @@ import Unison.Typechecker.Components (minimize') import Unison.Var (Var) import qualified Unison.Var as Var -type TypeVar v = TypeVar.TypeVar Blank v -type Type v loc = AnnotatedType (TypeVar v) loc -type Term v loc = AnnotatedTerm' (TypeVar v) v loc -type Monotype v loc = Type.Monotype (TypeVar v) loc +type TypeVar v loc = TypeVar.TypeVar (Blank loc) v +type Type v loc = AnnotatedType (TypeVar v loc) loc +type Term v loc = AnnotatedTerm' (TypeVar v loc) v loc +type Monotype v loc = Type.Monotype (TypeVar v loc) loc pattern Universal v = Var (TypeVar.Universal v) pattern Existential b v = Var (TypeVar.Existential b v) @@ -51,10 +51,17 @@ existential v = Existential Placeholder v -- | Elements of an ordered algorithmic context data Element v loc - = Var (TypeVar v) -- A variable declaration - | Solved Blank v (Monotype v loc) -- `v` is solved to some monotype - | Ann v (Type v loc) -- `v` has type `a`, which may be quantified - | Marker v deriving (Eq) -- used for scoping + = Var (TypeVar v loc) -- A variable declaration + | Solved (Blank loc) v (Monotype v loc) -- `v` is solved to some monotype + | Ann v (Type v loc) -- `v` has type `a`, maybe quantified + | Marker v -- used for scoping + +instance (Ord loc, Var v) => Eq (Element v loc) where + Var v == Var v2 = v == v2 + Solved _ v t == Solved _ v2 t2 = v == v2 && t == t2 + Ann v t == Ann v2 t2 = v == v2 && t == t2 + Marker v == Marker v2 = v == v2 + _ == _ = False data Env v loc = Env { freshId :: Word, ctx :: Context v loc } @@ -77,7 +84,7 @@ data CompilerBug v loc | RetractFailure (Element v loc) (Context v loc) | EmptyLetRec (Term v loc) -- the body of the empty let rec | PatternMatchFailure - | FreeVarsInTypeAnnotation (Set (TypeVar v)) + | FreeVarsInTypeAnnotation (Set (TypeVar v loc)) | UnannotatedReference Reference deriving Show data PathElement v loc @@ -100,12 +107,12 @@ data Cause v loc | CompilerBug (CompilerBug v loc) | AbilityCheckFailure [Type v loc] [Type v loc] -- ambient, requested | EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount Reference ConstructorId - | SolvedBlank Blank v (Type v loc) + | SolvedBlank (Blank loc) v (Type v loc) deriving Show data Note v loc = Note { cause :: Cause v loc, path :: Seq (PathElement v loc) } deriving Show -solveBlank :: Blank -> v -> Type v loc -> M v loc () +solveBlank :: Blank loc -> v -> Type v loc -> M v loc () solveBlank blank v typ = M (\menv -> (pure $ Note (SolvedBlank blank v typ) mempty, Just ((), env menv))) @@ -151,7 +158,7 @@ context xs = foldl' (flip extend) context0 xs -- | Delete from the end of this context up to and including -- the given `Element`. Returns `Nothing` if the element is not found. -retract0 :: Var v => Element v loc -> Context v loc -> Maybe (Context v loc, [Element v loc]) +retract0 :: (Var v, Ord loc) => Element v loc -> Context v loc -> Maybe (Context v loc, [Element v loc]) retract0 e (Context ctx) = let maybeTail [] = Nothing maybeTail (_:t) = pure t @@ -165,12 +172,23 @@ retract0 e (Context ctx) = -- the given `Element`. -- Example, if input context is `[a, b, c, d, ...]` -- Retract `d` returns `[a, b, c]` -doRetract :: Var v => Element v loc -> M v loc () +doRetract :: (Var v, Ord loc) => Element v loc -> M v loc () doRetract e = do ctx <- getContext case retract0 e ctx of Nothing -> compilerCrash (RetractFailure e ctx) - Just (t, _discarded) -> setContext t + Just (t, discarded) -> do + let solved = [ (b, v, inst $ Type.getPolytype sa) | + Solved b v sa <- discarded ] + es = [ (b, v) | Existential b v <- discarded ] + resolveds = [ (b, v, inst $ Type.existential' loc b v) | + (b@(Resolve loc _), v) <- es ] + remembers = [ (b, v, inst $ Type.existential' loc b v) | + (b@(Remember loc _), v) <- es ] + go (b, v, sa) = solveBlank b v sa + inst t = apply ctx t + Foldable.traverse_ go (solved ++ resolveds ++ remembers) + setContext t solved :: Context v loc -> [(v, Monotype v loc)] solved (Context ctx) = [(v, sa) | (Solved _ v sa, _) <- ctx] @@ -178,12 +196,12 @@ solved (Context ctx) = [(v, sa) | (Solved _ v sa, _) <- ctx] unsolved :: Context v loc -> [v] unsolved (Context ctx) = [v | (Existential _ v, _) <- ctx] -replace :: Var v => Element v loc -> Context v loc -> Context v loc -> Context v loc +replace :: (Var v, Ord loc) => Element v loc -> Context v loc -> Context v loc -> Context v loc replace e focus ctx = let (l,_,r) = breakAt e ctx in l `mappend` focus `mappend` r -breakAt :: Var v +breakAt :: (Var v, Ord loc) => Element v loc -> Context v loc -> (Context v loc, [Element v loc], Context v loc) @@ -200,11 +218,11 @@ breakAt m (Context xs) = -- | ordered Γ α β = True <=> Γ[α^][β^] -ordered :: Var v => Context v loc -> v -> v -> Bool +ordered :: (Var v, Ord loc) => Context v loc -> v -> v -> Bool ordered ctx v v2 = Set.member v (existentials (retract' (existential v2) ctx)) where -- | Like `retract`, but returns the empty context if retracting would remove all elements. - retract' :: Var v => Element v loc -> Context v loc -> Context v loc + retract' :: (Var v, Ord loc) => Element v loc -> Context v loc -> Context v loc retract' e ctx = fromMaybe mempty $ (fst <$> retract0 e ctx) -- env0 :: Env v loc @@ -242,7 +260,7 @@ modifyContext f = do c <- getContext; c <- f c; setContext c modifyContext' :: (Context v loc -> Context v loc) -> M v loc () modifyContext' f = modifyContext (pure . f) -appendContext :: Var v => Context v loc -> M v loc () +appendContext :: (Var v, Ord loc) => Context v loc -> M v loc () appendContext tl = modifyContext' (\ctx -> ctx `mappend` tl) universals :: Context v loc -> Set v @@ -258,17 +276,17 @@ freshenVar v = id = freshId e in (mempty, pure (Var.freshenId id v, e {freshId = id+1}))) -freshenTypeVar :: Var v => TypeVar v -> M v loc v +freshenTypeVar :: Var v => TypeVar v loc -> M v loc v freshenTypeVar v = M (\menv -> let e = env menv id = freshId e in (mempty, pure (Var.freshenId id (TypeVar.underlying v), e {freshId = id+1}))) -freshNamed :: Var v => Text -> M v loc v +freshNamed :: (Var v, Ord loc) => Text -> M v loc v freshNamed = freshenVar . Var.named -freshVar :: Var v => M v loc v +freshVar :: (Var v, Ord loc) => M v loc v freshVar = freshNamed "v" -- | Check that the context is well formed, see Figure 7 of paper @@ -378,10 +396,10 @@ getEffectDeclaration r = do Nothing -> compilerCrash (UnknownDecl Effect r (DD.toDataDecl <$> decls)) Just decl -> pure decl -getDataConstructorType :: Var v => Reference -> Int -> M v loc (Type v loc) +getDataConstructorType :: (Var v, Ord loc) => Reference -> Int -> M v loc (Type v loc) getDataConstructorType = getConstructorType' Data getDataDeclaration -getEffectConstructorType :: Var v => Reference -> Int -> M v loc (Type v loc) +getEffectConstructorType :: (Var v, Ord loc) => Reference -> Int -> M v loc (Type v loc) getEffectConstructorType = getConstructorType' Effect go where go r = DD.toDataDecl <$> getEffectDeclaration r @@ -399,26 +417,26 @@ getConstructorType' kind get r cid = do [] -> compilerCrash $ UnknownConstructor kind r cid decl (_v, typ) : _ -> pure $ ABT.vmap TypeVar.Universal typ -extendUniversal :: Var v => v -> M v loc v +extendUniversal :: (Var v) => v -> M v loc v extendUniversal v = do v' <- freshenVar v modifyContext (pure . extend (Universal v')) pure v' -extendMarker :: Var v => v -> M v loc v +extendMarker :: (Var v, Ord loc) => v -> M v loc v extendMarker v = do v' <- freshenVar v modifyContext (\ctx -> pure $ ctx `mappend` (context [Marker v', existential v'])) pure v' -notMember :: Var v => v -> Set (TypeVar v) -> Bool +notMember :: (Var v, Ord loc) => v -> Set (TypeVar v loc) -> Bool notMember v s = Set.notMember (TypeVar.Universal v) s && Set.notMember (TypeVar.Existential Placeholder v) s -- | Replace any existentials with their solution in the context -apply :: Var v => Context v loc -> Type v loc -> Type v loc +apply :: (Var v, Ord loc) => Context v loc -> Type v loc -> Type v loc apply ctx t = case t of Type.Universal' _ -> t Type.Ref' _ -> t @@ -449,7 +467,7 @@ withEffects0 abilities' m = -- the given type `ft` is being applied to `arg`. Update the context in -- the process. -- e.g. in `(f:t) x` -- finds the type of (f x) given t and x. -synthesizeApp :: Var v => Type v loc -> Term v loc -> M v loc (Type v loc) +synthesizeApp :: (Var v, Ord loc) => Type v loc -> Term v loc -> M v loc (Type v loc) -- synthesizeApp ft arg | debugEnabled && traceShow ("synthesizeApp"::String, ft, arg) False = undefined synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where go (Type.Forall' body) = do -- Forall1App @@ -475,7 +493,7 @@ synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where -- For arity 3, creates the type `∀ a . a -> a -> a -> Sequence a` -- For arity 2, creates the type `∀ a . a -> a -> Sequence a` -vectorConstructorOfArity :: Var v => Int -> M v loc (Type v loc) +vectorConstructorOfArity :: (Var v, Ord loc) => Int -> M v loc (Type v loc) vectorConstructorOfArity arity = do bl <- getBuiltinLocation let elementVar = Var.named "elem" @@ -486,11 +504,11 @@ vectorConstructorOfArity arity = do -- | Synthesize the type of the given term, updating the context in the process. -- | Figure 11 from the paper -synthesize :: forall v loc . Var v => Term v loc -> M v loc (Type v loc) +synthesize :: forall v loc . (Var v, Ord loc) => Term v loc -> M v loc (Type v loc) synthesize e = scope (InSynthesize e) $ go (minimize' e) where l = loc e - go :: Var v => Term v loc -> M v loc (Type v loc) + go :: (Var v, Ord loc) => Term v loc -> M v loc (Type v loc) go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var Nothing -> compilerCrash $ UndeclaredTermVariable v ctx Just t -> pure t @@ -643,7 +661,7 @@ let x = _ -} -- Make up a fake term for the pattern, that we can typecheck -patternToTerm :: Var v => Pattern loc -> State [v] (Term v loc) +patternToTerm :: (Var v, Ord loc) => Pattern loc -> State [v] (Term v loc) patternToTerm pat = case pat of Pattern.Boolean loc b -> pure $ Term.boolean loc b Pattern.Int64 loc n -> pure $ Term.int64 loc n @@ -670,7 +688,7 @@ patternToTerm pat = case pat of pure $ Term.effectBind loc r cid outputTerms kTerm _ -> error "todo: delete me after deleting PatternP - match fail in patternToTerm" -checkCase :: forall v loc . Var v => Type v loc -> Type v loc -> Term.MatchCase loc (Term v loc) -> M v loc () +checkCase :: forall v loc . (Var v, Ord loc) => Type v loc -> Type v loc -> Term.MatchCase loc (Term v loc) -> M v loc () checkCase scrutineeType outputType (Term.MatchCase pat guard rhs) = -- Get the variables bound in the pattern let (vs, body) = case rhs of @@ -707,7 +725,7 @@ lookupType ctx v = lookup v (bindings ctx) -- which should be used to retract the context after checking/synthesis -- of `body` is complete. See usage in `synthesize` and `check` for `LetRec'` case. annotateLetRecBindings - :: Var v + :: (Var v, Ord loc) => ((v -> M v loc v) -> M v loc ([(v, Term v loc)], Term v loc)) -> M v loc (Element v loc, Term v loc) annotateLetRecBindings letrec = do @@ -742,7 +760,7 @@ annotateLetRecBindings letrec = do -- | Apply the context to the input type, then convert any unsolved existentials -- to universals. -generalizeExistentials :: Var v => Context v loc -> Type v loc -> Type v loc +generalizeExistentials :: (Var v, Ord loc) => Context v loc -> Type v loc -> Type v loc generalizeExistentials ctx t = foldr gen (apply ctx t) (unsolved ctx) where @@ -761,7 +779,7 @@ generalizeExistentials ctx t = -- | Check that under the given context, `e` has type `t`, -- updating the context in the process. -check :: forall v loc . Var v => Term v loc -> Type v loc -> M v loc () +check :: forall v loc . (Var v, Ord loc) => Term v loc -> Type v loc -> M v loc () -- check e t | debugEnabled && traceShow ("check"::String, e, t) False = undefined check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> if wellformedType ctx t then @@ -820,7 +838,7 @@ check e0 t = scope (InCheck e0 t) $ getContext >>= \ctx -> -- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`. -- This may have the effect of altering the context. -subtype :: forall v loc . Var v => Type v loc -> Type v loc -> M v loc () +subtype :: forall v loc . (Var v, Ord loc) => Type v loc -> Type v loc -> M v loc () subtype tx ty | debugEnabled && traceShow ("subtype"::String, tx, ty) False = undefined subtype tx ty = scope (InSubtype tx ty) $ do ctx <- getContext; go (ctx :: Context v loc) tx ty @@ -870,7 +888,7 @@ subtype tx ty = scope (InSubtype tx ty) $ -- | Instantiate the given existential such that it is -- a subtype of the given type, updating the context -- in the process. -instantiateL :: Var v => Blank -> v -> Type v loc -> M v loc () +instantiateL :: (Var v, Ord loc) => Blank loc -> v -> Type v loc -> M v loc () instantiateL _ v t | debugEnabled && traceShow ("instantiateL"::String, v, t) False = undefined instantiateL blank v t = scope (InInstantiateL v t) $ getContext >>= \ctx -> case Type.monotype t >>= (solve ctx v) of @@ -925,7 +943,7 @@ instantiateL blank v t = scope (InInstantiateL v t) $ -- | Instantiate the given existential such that it is -- a supertype of the given type, updating the context -- in the process. -instantiateR :: Var v => Type v loc -> Blank -> v -> M v loc () +instantiateR :: (Var v, Ord loc) => Type v loc -> Blank loc -> v -> M v loc () instantiateR t _ v | debugEnabled && traceShow ("instantiateR"::String, t, v) False = undefined instantiateR t blank v = scope (InInstantiateR t v) $ getContext >>= \ctx -> case Type.monotype t >>= solve ctx v of @@ -980,7 +998,7 @@ instantiateR t blank v = scope (InInstantiateR t v) $ -- | solve (ΓL,α^,ΓR) α τ = (ΓL,α^ = τ,ΓR) -- If the given existential variable exists in the context, -- we solve it to the given monotype, otherwise return `Nothing` -solve :: Var v => Context v loc -> v -> Monotype v loc -> Maybe (Context v loc) +solve :: (Var v, Ord loc) => Context v loc -> v -> Monotype v loc -> Maybe (Context v loc) solve ctx v t -- okay to solve something again if it's to an identical type | v `elem` (map fst (solved ctx)) = same =<< lookup v (solved ctx) @@ -993,28 +1011,28 @@ solve ctx v t mid = [ Solved blank v t | Existential blank v <- focus ] ctx' = ctxL `mappend` context mid `mappend` ctxR -abilityCheck' :: Var v => [Type v loc] -> [Type v loc] -> M v loc () +abilityCheck' :: (Var v, Ord loc) => [Type v loc] -> [Type v loc] -> M v loc () abilityCheck' ambient requested = do success <- flip allM requested $ \req -> flip anyM ambient $ \amb -> (True <$ subtype amb req) `orElse` pure False when (not success) $ failWith $ AbilityCheckFailure ambient requested -abilityCheck :: Var v => [Type v loc] -> M v loc () +abilityCheck :: (Var v, Ord loc) => [Type v loc] -> M v loc () abilityCheck requested = do enabled <- abilityCheckEnabled when enabled $ do ambient <- getAbilities abilityCheck' ambient requested -verifyDataDeclarations :: Var v => DataDeclarations v loc -> M v loc () +verifyDataDeclarations :: (Var v, Ord loc) => DataDeclarations v loc -> M v loc () verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do let ctors = DD.constructors decl forM_ ctors $ \(_ctorName,typ) -> verifyClosed typ id -- | public interface to the typechecker synthesizeClosed - :: (Monad f, Var v) + :: (Monad f, Var v, Ord loc) => loc -> [Type v loc] -> (Reference -> f (Type.AnnotatedType v loc)) @@ -1060,7 +1078,7 @@ annotateRefs synth term = ABT.visit f term where where ra = ABT.annotation r f _ = Nothing -run :: Var v +run :: (Var v, Ord loc) => loc -> [Type v loc] -> DataDeclarations v loc @@ -1071,7 +1089,7 @@ run builtinLoc ambient datas effects m = let (notes, o) = runM m (MEnv (Env 0 mempty) ambient builtinLoc datas effects True) in (notes, fst <$> o) -synthesizeClosed' :: Var v +synthesizeClosed' :: (Var v, Ord loc) => [Type v loc] -> Term v loc -> M v loc (Type v loc) @@ -1110,12 +1128,12 @@ instance Applicative (M v loc) where instance Functor (M v loc) where fmap = liftM -instance Var v => Monoid (Context v loc) where +instance (Var v, Ord loc) => Monoid (Context v loc) where mempty = context0 mappend ctxL (Context es) = -- since `es` is a snoc list, we add it to `ctxL` in reverse order foldl' f ctxL (reverse es) where f ctx (e,_) = extend e ctx -instance Var v => Semigroup (Context v loc) where +instance (Var v, Ord loc) => Semigroup (Context v loc) where (<>) = mappend From f23ca960c8334d751064dab78c92933622afe126 Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 31 Jul 2018 21:35:45 -0400 Subject: [PATCH 06/11] Add retract call in synthesizeClosed to make sure all recorded existentials get noted --- parser-typechecker/src/Unison/Typechecker/Context.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index ac5f2258f..41e1fb7b7 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -1094,8 +1094,16 @@ synthesizeClosed' :: (Var v, Ord loc) -> Term v loc -> M v loc (Type v loc) synthesizeClosed' abilities term = do + -- save current context, for restoration when done + ctx0 <- getContext + setContext $ context [] + v <- extendMarker $ Var.named "start" t <- withEffects0 abilities (synthesize term) ctx <- getContext + -- retract will cause notes to be written out for + -- any `Blank`-tagged existentials passing out of scope + doRetract (Marker v) + setContext ctx0 -- restore the initial context pure $ generalizeExistentials ctx t instance (Var v, Show loc) => Show (Element v loc) where From 0566c26561bc8132371c95fe5105e22c51502ce9 Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 31 Jul 2018 22:08:14 -0400 Subject: [PATCH 07/11] Split `Blank` up into `Recorded` and non-recorded portion, this lets us give a more precise type for `SolvedBlank` notes Also changed naming - `blank` is a noop in the typechecker, `placeholder` is like GHC holes, and `resolve` is used for type-directed term resolution --- parser-typechecker/src/Unison/Blank.hs | 17 ++-- parser-typechecker/src/Unison/Paths.hs | 2 +- parser-typechecker/src/Unison/Term.hs | 30 +++---- parser-typechecker/src/Unison/TermParser.hs | 6 +- parser-typechecker/src/Unison/Type.hs | 2 +- .../src/Unison/Typechecker/Context.hs | 89 +++++++++---------- 6 files changed, 75 insertions(+), 71 deletions(-) diff --git a/parser-typechecker/src/Unison/Blank.hs b/parser-typechecker/src/Unison/Blank.hs index 3e235c2ca..69bcb284c 100644 --- a/parser-typechecker/src/Unison/Blank.hs +++ b/parser-typechecker/src/Unison/Blank.hs @@ -1,10 +1,17 @@ module Unison.Blank where -data Blank loc - -- An expression that has not been filled in, has type `forall a . a`. - = Placeholder - -- A user-provided typed hole - | Remember loc String +loc :: Recorded loc -> loc +loc (Placeholder loc _) = loc +loc (Resolve loc _) = loc + +data Recorded loc + -- A user-provided named placeholder + = Placeholder loc String -- A name to be resolved with type-directed name resolution. | Resolve loc String deriving (Show, Eq, Ord) + +data Blank loc = Blank | Recorded (Recorded loc) + deriving (Show, Eq, Ord) + + diff --git a/parser-typechecker/src/Unison/Paths.hs b/parser-typechecker/src/Unison/Paths.hs index 62491174f..79739336c 100644 --- a/parser-typechecker/src/Unison/Paths.hs +++ b/parser-typechecker/src/Unison/Paths.hs @@ -146,7 +146,7 @@ insertTerm at ctx = do Term (E.Vector' vs) -> do i <- listToMaybe [i | Index i <- [last at]] let v2 = E.vector'() ((E.vmap ABT.Bound <$> Vector.take (i+1) vs) `mappend` - Vector.singleton (E.placeholder ()) `mappend` + Vector.singleton (E.blank ()) `mappend` (E.vmap ABT.Bound <$> Vector.drop (i+1) vs)) asTerm =<< set (Term v2) _ -> Nothing -- todo - allow other types of insertions, like \x -> y to \x x2 -> y diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 1e9c0a50b..37444149e 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -29,7 +29,7 @@ import GHC.Generics import Prelude.Extras (Eq1(..), Show1(..)) import Text.Show import qualified Unison.ABT as ABT -import Unison.Blank +import qualified Unison.Blank as B import Unison.Hash (Hash) import qualified Unison.Hash as Hash import Unison.Hashable (Hashable1, accumulateToken) @@ -55,7 +55,7 @@ data F typeVar typeAnn patternAnn a | Float Double | Boolean Bool | Text Text - | Blank (Blank typeAnn) + | Blank (B.Blank typeAnn) | Ref Reference -- First argument identifies the data type, -- second argument identifies the constructor @@ -225,14 +225,14 @@ uint64 a d = ABT.tm' a (UInt64 d) text :: Ord v => a -> Text -> AnnotatedTerm2 vt at ap v a text a = ABT.tm' a . Text -placeholder :: Ord v => a -> AnnotatedTerm2 vt at ap v a -placeholder a = ABT.tm' a (Blank Placeholder) +blank :: Ord v => a -> AnnotatedTerm2 vt at ap v a +blank a = ABT.tm' a (Blank B.Blank) -remember :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a -remember a s = ABT.tm' a . Blank $ Remember a s +placeholder :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a +placeholder a s = ABT.tm' a . Blank $ B.Recorded (B.Placeholder a s) resolve :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a -resolve a s = ABT.tm' a . Blank $ Resolve a s +resolve a s = ABT.tm' a . Blank $ B.Recorded (B.Resolve a s) constructor :: Ord v => a -> Reference -> Int -> AnnotatedTerm2 vt at ap v a constructor a ref n = ABT.tm' a (Constructor ref n) @@ -444,11 +444,11 @@ instance Var v => Hashable1 (F v a p) where Float n -> [tag 66, Hashable.Double n] Boolean b -> [tag 67, accumulateToken b] Text t -> [tag 68, accumulateToken t] - Blank b -> - tag 1 : case b of - Placeholder -> [tag 0] - Remember _ s -> [tag 1, Hashable.Text (Text.pack s)] - Resolve _ s -> [tag 2, Hashable.Text (Text.pack s)] + Blank b -> tag 1 : + case b of + B.Blank -> [tag 0] + B.Recorded (B.Placeholder _ s) -> [tag 1, Hashable.Text (Text.pack s)] + B.Recorded (B.Resolve _ s) -> [tag 2, Hashable.Text (Text.pack s)] Ref (Reference.Builtin name) -> [tag 2, accumulateToken name] Ref (Reference.Derived _) -> error "handled above, but GHC can't figure this out" App a a2 -> [tag 3, hashed (hash a), hashed (hash a2)] @@ -523,9 +523,9 @@ instance (Var v, Show p, Show a0, Show a) => Show (F v a0 p a) where go _ (Vector vs) = showListWith (showsPrec 0) (Vector.toList vs) go _ (Blank b) = case b of - Placeholder -> s"_" - Remember _ r -> s("_" ++ r) - Resolve _ r -> s r + B.Blank -> s"_" + B.Recorded (B.Placeholder _ r) -> s("_" ++ r) + B.Recorded (B.Resolve _ r) -> s r go _ (Ref r) = showsPrec 0 r go _ (Let b body) = showParen True (s"let " <> showsPrec 0 b <> s" in " <> showsPrec 0 body) go _ (LetRec bs body) = showParen True (s"let rec" <> showsPrec 0 bs <> s" in " <> showsPrec 0 body) diff --git a/parser-typechecker/src/Unison/TermParser.hs b/parser-typechecker/src/Unison/TermParser.hs index 01442243c..18965fd7f 100644 --- a/parser-typechecker/src/Unison/TermParser.hs +++ b/parser-typechecker/src/Unison/TermParser.hs @@ -186,8 +186,8 @@ boolean :: Var v => TermP v boolean = ((\t -> Term.boolean (ann t) True) <$> reserved "true") <|> ((\t -> Term.boolean (ann t) False) <$> reserved "false") -remember :: Var v => TermP v -remember = (\t -> Term.remember (ann t) (L.payload t)) <$> blank +placeholder :: Var v => TermP v +placeholder = (\t -> Term.placeholder (ann t) (L.payload t)) <$> blank vector :: Var v => TermP v -> TermP v vector p = f <$> reserved "[" <*> elements <*> reserved "]" @@ -198,7 +198,7 @@ vector p = f <$> reserved "[" <*> elements <*> reserved "]" termLeaf :: forall v. Var v => TermP v termLeaf = asum [hashLit, prefixTerm, text, number, boolean, - tupleOrParenthesizedTerm, remember, vector term] + tupleOrParenthesizedTerm, placeholder, vector term] and = label "and" $ f <$> reserved "and" <*> termLeaf <*> termLeaf where f kw x y = Term.and (ann kw <> ann y) x y diff --git a/parser-typechecker/src/Unison/Type.hs b/parser-typechecker/src/Unison/Type.hs index 45ddf9351..3df8bd64f 100644 --- a/parser-typechecker/src/Unison/Type.hs +++ b/parser-typechecker/src/Unison/Type.hs @@ -202,7 +202,7 @@ universal :: Ord v => v -> Type (TypeVar b v) universal v = ABT.var (TypeVar.Universal v) existentialp :: Ord v => a -> v -> AnnotatedType (TypeVar (Blank x) v) a -existentialp a v = existential' a Placeholder v +existentialp a v = existential' a Blank v existential' :: Ord v => a -> Blank x -> v -> AnnotatedType (TypeVar (Blank x) v) a existential' a blank v = ABT.annotatedVar a (TypeVar.Existential blank v) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 41e1fb7b7..b74a982a5 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -23,7 +23,7 @@ import Data.Text (Text) import qualified Data.Text as Text import Debug.Trace import qualified Unison.ABT as ABT -import Unison.Blank +import qualified Unison.Blank as B import Unison.DataDeclaration (DataDeclaration', EffectDeclaration') import qualified Unison.DataDeclaration as DD import Unison.PatternP (Pattern) @@ -38,7 +38,7 @@ import Unison.Typechecker.Components (minimize') import Unison.Var (Var) import qualified Unison.Var as Var -type TypeVar v loc = TypeVar.TypeVar (Blank loc) v +type TypeVar v loc = TypeVar.TypeVar (B.Blank loc) v type Type v loc = AnnotatedType (TypeVar v loc) loc type Term v loc = AnnotatedTerm' (TypeVar v loc) v loc type Monotype v loc = Type.Monotype (TypeVar v loc) loc @@ -47,12 +47,12 @@ pattern Universal v = Var (TypeVar.Universal v) pattern Existential b v = Var (TypeVar.Existential b v) existential :: v -> Element v loc -existential v = Existential Placeholder v +existential v = Existential B.Blank v -- | Elements of an ordered algorithmic context data Element v loc = Var (TypeVar v loc) -- A variable declaration - | Solved (Blank loc) v (Monotype v loc) -- `v` is solved to some monotype + | Solved (B.Blank loc) v (Monotype v loc) -- `v` is solved to some monotype | Ann v (Type v loc) -- `v` has type `a`, maybe quantified | Marker v -- used for scoping @@ -107,12 +107,12 @@ data Cause v loc | CompilerBug (CompilerBug v loc) | AbilityCheckFailure [Type v loc] [Type v loc] -- ambient, requested | EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount Reference ConstructorId - | SolvedBlank (Blank loc) v (Type v loc) + | SolvedBlank (B.Recorded loc) v (Type v loc) deriving Show data Note v loc = Note { cause :: Cause v loc, path :: Seq (PathElement v loc) } deriving Show -solveBlank :: Blank loc -> v -> Type v loc -> M v loc () +solveBlank :: B.Recorded loc -> v -> Type v loc -> M v loc () solveBlank blank v typ = M (\menv -> (pure $ Note (SolvedBlank blank v typ) mempty, Just ((), env menv))) @@ -179,15 +179,12 @@ doRetract e = do Nothing -> compilerCrash (RetractFailure e ctx) Just (t, discarded) -> do let solved = [ (b, v, inst $ Type.getPolytype sa) | - Solved b v sa <- discarded ] - es = [ (b, v) | Existential b v <- discarded ] - resolveds = [ (b, v, inst $ Type.existential' loc b v) | - (b@(Resolve loc _), v) <- es ] - remembers = [ (b, v, inst $ Type.existential' loc b v) | - (b@(Remember loc _), v) <- es ] + Solved (B.Recorded b) v sa <- discarded ] + unsolved = [ (b, v, inst $ Type.existential' (B.loc b) b' v) | + Existential b'@(B.Recorded b) v <- discarded ] go (b, v, sa) = solveBlank b v sa inst t = apply ctx t - Foldable.traverse_ go (solved ++ resolveds ++ remembers) + Foldable.traverse_ go (solved ++ unsolved) setContext t solved :: Context v loc -> [(v, Monotype v loc)] @@ -433,7 +430,7 @@ extendMarker v = do notMember :: (Var v, Ord loc) => v -> Set (TypeVar v loc) -> Bool notMember v s = Set.notMember (TypeVar.Universal v) s && - Set.notMember (TypeVar.Existential Placeholder v) s + Set.notMember (TypeVar.Existential B.Blank v) s -- | Replace any existentials with their solution in the context apply :: (Var v, Ord loc) => Context v loc -> Type v loc -> Type v loc @@ -473,7 +470,7 @@ synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where go (Type.Forall' body) = do -- Forall1App v <- ABT.freshen body freshenTypeVar appendContext (context [existential v]) - synthesizeApp (ABT.bindInheritAnnotation body (Type.existential Placeholder v)) arg + synthesizeApp (ABT.bindInheritAnnotation body (Type.existential B.Blank v)) arg go (Type.Arrow' i o) = do -- ->App let (es, _) = Type.stripEffect o abilityCheck es @@ -483,8 +480,8 @@ synthesizeApp ft arg = scope (InSynthesizeApp ft arg) $ go ft where o <$ check arg (Type.effect (loc ft) ambientEs i) go (Type.Existential' b a) = do -- a^App [i,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"] - let it = Type.existential' (loc ft) Placeholder i - ot = Type.existential' (loc ft) Placeholder o + let it = Type.existential' (loc ft) B.Blank i + ot = Type.existential' (loc ft) B.Blank o soln = Type.Monotype (Type.arrow (loc ft) it ot) ctxMid = context [existential o, existential i, Solved b a soln] modifyContext' $ replace (existential a) ctxMid @@ -532,7 +529,7 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) ambient <- getAbilities let l = loc t -- arya: we should revisit these l's too - subtype t (Type.effect l ambient (Type.existential' l Placeholder a)) + subtype t (Type.effect l ambient (Type.existential' l B.Blank a)) -- modifyContext $ retract [Marker a] pure t else pure t @@ -583,8 +580,8 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.Lam' body) = do -- ->I=> (Full Damas Milner rule) -- arya: are there more meaningful locations we could put into and pull out of the abschain?) [arg, i, o] <- sequence [ABT.freshen body freshenVar, freshVar, freshVar] - let it = Type.existential' l Placeholder i - ot = Type.existential' l Placeholder o + let it = Type.existential' l B.Blank i + ot = Type.existential' l B.Blank o appendContext $ context [Marker i, existential i, existential o, Ann arg it] body <- pure $ ABT.bindInheritAnnotation body (Term.var() arg) @@ -616,7 +613,7 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) ([eType], iType) <- Type.stripEffect <$> withoutAbilityCheck (foldM synthesizeApp cType args) rTypev <- freshNamed "result" - let rType = Type.existential' l Placeholder rTypev + let rType = Type.existential' l B.Blank rTypev appendContext $ context [existential rTypev] check k (Type.arrow l iType (Type.effect l [eType] rType)) ctx <- getContext @@ -624,7 +621,7 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go (Term.Match' scrutinee cases) = do scrutineeType <- synthesize scrutinee outputTypev <- freshenVar (Var.named "match-output") - let outputType = Type.existential' l Placeholder outputTypev + let outputType = Type.existential' l B.Blank outputTypev appendContext $ context [existential outputTypev] Foldable.traverse_ (checkCase scrutineeType outputType) cases ctx <- getContext @@ -632,7 +629,7 @@ synthesize e = scope (InSynthesize e) $ go (minimize' e) go h@(Term.Handle' _ _) = do o <- freshNamed "o" appendContext $ context [existential o] - let ot = Type.existential' l Placeholder o + let ot = Type.existential' l B.Blank o check h ot ctx <- getContext pure (apply ctx ot) @@ -675,7 +672,7 @@ patternToTerm pat = case pat of (h : t) <- get put t pure $ Term.var loc h - Pattern.Unbound loc -> pure $ Term.placeholder loc + Pattern.Unbound loc -> pure $ Term.blank loc Pattern.As loc p -> do (h : t) <- get put t @@ -708,7 +705,7 @@ checkCase scrutineeType outputType (Term.MatchCase pat guard rhs) = patTerm = evalState (patternToTerm (pat :: Pattern loc) :: State [v] (Term v loc)) vs newBody = Term.let1 [((loc rhs', Var.named "_"), Term.ann (loc scrutineeType) patTerm scrutineeType)] rhs' entireCase = - foldr (\locv t -> Term.let1 [(locv, Term.placeholder (fst locv))] t) + foldr (\locv t -> Term.let1 [(locv, Term.blank (fst locv))] t) newBody (Foldable.toList pat `zip` vs) in check entireCase outputType @@ -742,7 +739,7 @@ annotateLetRecBindings letrec = do -- TODO: Think about whether `apply` here is always correct -- Used to have a guard that would only do this if t had no free vars Term.Ann' _ t -> apply ctx t - _ -> Type.existential' (loc binding) Placeholder e + _ -> Type.existential' (loc binding) B.Blank e let bindingTypes = zipWith f es bindings appendContext $ context (Marker e1 : map existential es ++ zipWith Ann vs bindingTypes) -- check each `bi` against `ei`; sequencing resulting contexts @@ -752,7 +749,7 @@ annotateLetRecBindings letrec = do (ctx1, _, ctx2) <- breakAt (Marker e1) <$> getContext -- The location of the existential is just the location of the binding let gen (e,(_,binding)) = generalizeExistentials ctx2 - (Type.existential' (loc binding) Placeholder e) + (Type.existential' (loc binding) B.Blank e) let annotations = zipWith Ann vs (map gen (es `zip` bindings)) marker <- Marker <$> freshenVar (ABT.v' "let-rec-marker") setContext (ctx1 `mappend` context (marker : annotations)) @@ -765,14 +762,14 @@ generalizeExistentials ctx t = foldr gen (apply ctx t) (unsolved ctx) where gen e t = - if TypeVar.Existential Placeholder e `ABT.isFreeIn` t + if TypeVar.Existential B.Blank e `ABT.isFreeIn` t -- location of the forall is just the location of the input type -- and the location of each quantified variable is just inherited from -- its source location then Type.forall (loc t) (TypeVar.Universal e) (ABT.substInheritAnnotation - (TypeVar.Existential Placeholder e) + (TypeVar.Existential B.Blank e) (Type.universal e) t) else t -- don't bother introducing a forall if type variable is unused @@ -864,7 +861,7 @@ subtype tx ty = scope (InSubtype tx ty) $ doRetract (Universal v') go _ (Type.Forall' t) t2 = do v <- extendMarker =<< ABT.freshen t freshenTypeVar - t <- pure $ ABT.bindInheritAnnotation t (Type.existential Placeholder v) + t <- pure $ ABT.bindInheritAnnotation t (Type.existential B.Blank v) ctx' <- getContext subtype (apply ctx' t) t2 doRetract (Marker v) @@ -888,7 +885,7 @@ subtype tx ty = scope (InSubtype tx ty) $ -- | Instantiate the given existential such that it is -- a subtype of the given type, updating the context -- in the process. -instantiateL :: (Var v, Ord loc) => Blank loc -> v -> Type v loc -> M v loc () +instantiateL :: (Var v, Ord loc) => B.Blank loc -> v -> Type v loc -> M v loc () instantiateL _ v t | debugEnabled && traceShow ("instantiateL"::String, v, t) False = undefined instantiateL blank v t = scope (InInstantiateL v t) $ getContext >>= \ctx -> case Type.monotype t >>= (solve ctx v) of @@ -904,9 +901,9 @@ instantiateL blank v t = scope (InInstantiateL v t) $ (Type.existentialp (loc o) o'))) modifyContext' $ replace (existential v) (context [existential o', existential i', s]) - instantiateR i Placeholder i' -- todo: not sure about this, could also be `blank` + instantiateR i B.Blank i' -- todo: not sure about this, could also be `blank` ctx <- getContext - instantiateL Placeholder o' (apply ctx o) + instantiateL B.Blank o' (apply ctx o) Type.App' x y -> do -- analogue of InstLArr [x', y'] <- traverse freshenVar [ABT.v' "x", ABT.v' "y"] let s = Solved blank v (Type.Monotype (Type.app (loc t) @@ -915,8 +912,8 @@ instantiateL blank v t = scope (InInstantiateL v t) $ modifyContext' $ replace (existential v) (context [existential y', existential x', s]) ctx0 <- getContext - ctx' <- instantiateL Placeholder x' (apply ctx0 x) >> getContext - instantiateL Placeholder y' (apply ctx' y) + ctx' <- instantiateL B.Blank x' (apply ctx0 x) >> getContext + instantiateL B.Blank y' (apply ctx' y) Type.Effect' es vt -> do es' <- replicateM (length es) (freshNamed "e") vt' <- freshNamed "vt" @@ -931,19 +928,19 @@ instantiateL blank v t = scope (InInstantiateL v t) $ [existential vt', s]) Foldable.for_ (es' `zip` es) $ \(e',e) -> do ctx <- getContext - instantiateL Placeholder e' (apply ctx e) + instantiateL B.Blank e' (apply ctx e) ctx <- getContext - instantiateL Placeholder vt' (apply ctx vt) + instantiateL B.Blank vt' (apply ctx vt) Type.Forall' body -> do -- InstLIIL v <- extendUniversal =<< ABT.freshen body freshenTypeVar - instantiateL Placeholder v (ABT.bindInheritAnnotation body (Type.universal v)) + instantiateL B.Blank v (ABT.bindInheritAnnotation body (Type.universal v)) doRetract (Universal v) _ -> failWith $ TypeMismatch ctx -- | Instantiate the given existential such that it is -- a supertype of the given type, updating the context -- in the process. -instantiateR :: (Var v, Ord loc) => Type v loc -> Blank loc -> v -> M v loc () +instantiateR :: (Var v, Ord loc) => Type v loc -> B.Blank loc -> v -> M v loc () instantiateR t _ v | debugEnabled && traceShow ("instantiateR"::String, t, v) False = undefined instantiateR t blank v = scope (InInstantiateR t v) $ getContext >>= \ctx -> case Type.monotype t >>= solve ctx v of @@ -960,8 +957,8 @@ instantiateR t blank v = scope (InInstantiateR t v) $ (Type.existentialp (loc o) o'))) modifyContext' $ replace (existential v) (context [existential o', existential i', s]) - ctx <- instantiateL Placeholder i' i >> getContext - instantiateR (apply ctx o) Placeholder o' + ctx <- instantiateL B.Blank i' i >> getContext + instantiateR (apply ctx o) B.Blank o' Type.App' x y -> do -- analogue of InstRArr -- example foo a <: v' will -- 1. create foo', a', add these to the context @@ -971,9 +968,9 @@ instantiateR t blank v = scope (InInstantiateR t v) $ let s = Solved blank v (Type.Monotype (Type.app (loc t) (Type.existentialp (loc x) x') (Type.existentialp (loc y) y'))) modifyContext' $ replace (existential v) (context [existential y', existential x', s]) ctx <- getContext - instantiateR (apply ctx x) Placeholder x' + instantiateR (apply ctx x) B.Blank x' ctx <- getContext - instantiateR (apply ctx y) Placeholder y' + instantiateR (apply ctx y) B.Blank y' Type.Effect' es vt -> do es' <- replicateM (length es) (freshNamed "e") vt' <- freshNamed "vt" @@ -985,13 +982,13 @@ instantiateR t blank v = scope (InInstantiateR t v) $ modifyContext' $ replace (existential v) (context $ (existential <$> es') ++ [existential vt', s]) Foldable.for_ (es `zip` es') $ \(e, e') -> do ctx <- getContext - instantiateR (apply ctx e) Placeholder e' + instantiateR (apply ctx e) B.Blank e' ctx <- getContext - instantiateR (apply ctx vt) Placeholder vt' + instantiateR (apply ctx vt) B.Blank vt' Type.Forall' body -> do -- InstRAIIL x' <- ABT.freshen body freshenTypeVar setContext $ ctx `mappend` context [Marker x', existential x'] - instantiateR (ABT.bindInheritAnnotation body (Type.existential Placeholder x')) Placeholder v + instantiateR (ABT.bindInheritAnnotation body (Type.existential B.Blank x')) B.Blank v doRetract (Marker x') _ -> failWith $ TypeMismatch ctx From 2fe89db5ae0170f800f2a5dfdbbc78643b4592db Mon Sep 17 00:00:00 2001 From: Runar Bjarnason Date: Wed, 1 Aug 2018 11:56:51 -0400 Subject: [PATCH 08/11] Type-directed resolve typechecks --- parser-typechecker/src/Unison/ABT.hs | 6 ++++++ parser-typechecker/src/Unison/Term.hs | 12 ++++++++++-- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/parser-typechecker/src/Unison/ABT.hs b/parser-typechecker/src/Unison/ABT.hs index 6a54abc84..08042b471 100644 --- a/parser-typechecker/src/Unison/ABT.hs +++ b/parser-typechecker/src/Unison/ABT.hs @@ -287,6 +287,7 @@ rebuildUp f (Term _ ann body) = case body of Abs x e -> abs' ann x (rebuildUp f e) Tm body -> tm' ann (f $ fmap (rebuildUp f) body) +-- Annotate the tree with the set of bound variables at each node. annotateBound :: (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v) annotateBound t = go Set.empty t where go bound t = let a = (annotation t, bound) in case out t of @@ -343,6 +344,11 @@ visit' f t = case out t of Abs x e -> abs' (annotation t) x <$> visit' f e Tm body -> f body >>= \body -> tm' (annotation t) <$> traverse (visit' f) body +-- | `visit` specialized to the `Identity` effect. +visitPure :: (Traversable f, Ord v) + => (Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a +visitPure f = runIdentity . visit (fmap pure . f) + data Subst f v a = Subst { freshen :: forall m v' . Monad m => (v -> m v') -> m v' , bind :: Term f v a -> Term f v a diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 37444149e..cef209088 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -41,6 +41,7 @@ import qualified Unison.Reference as Reference import Unison.Type (Type) import qualified Unison.Type as Type import Unison.Var (Var) +import qualified Unison.Var as Var import Unsafe.Coerce -- todo: add loc to MatchCase @@ -120,6 +121,13 @@ bindBuiltins dataAndEffectCtors termBuiltins0 typeBuiltins t = h = ABT.substsInheritAnnotation dataAndEffectCtors termBuiltins = [ (v, ref() r) | (v,r) <- termBuiltins0 ] +typeDirectedResolve :: Var v + => ABT.Term (F vt b ap) v b -> ABT.Term (F vt b ap) v b +typeDirectedResolve t = fmap fst . ABT.visitPure f $ ABT.annotateBound t + where f (ABT.Term _ (a, bound) (ABT.Var v)) | Set.notMember v bound = + Just $ resolve (a, bound) a (Text.unpack $ Var.name v) + f _ = Nothing + vmap :: Ord v2 => (v -> v2) -> AnnotatedTerm v a -> AnnotatedTerm v2 a vmap f = ABT.vmap f . typeMap (ABT.vmap f) @@ -231,8 +239,8 @@ blank a = ABT.tm' a (Blank B.Blank) placeholder :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a placeholder a s = ABT.tm' a . Blank $ B.Recorded (B.Placeholder a s) -resolve :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a -resolve a s = ABT.tm' a . Blank $ B.Recorded (B.Resolve a s) +resolve :: Ord v => at -> ab -> String -> AnnotatedTerm2 vt ab ap v at +resolve at ab s = ABT.tm' at . Blank $ B.Recorded (B.Resolve ab s) constructor :: Ord v => a -> Reference -> Int -> AnnotatedTerm2 vt at ap v a constructor a ref n = ABT.tm' a (Constructor ref n) From 794e88e2057419ef5b4821811bca9d8fb85f0022 Mon Sep 17 00:00:00 2001 From: Runar Bjarnason Date: Wed, 1 Aug 2018 11:59:14 -0400 Subject: [PATCH 09/11] Calling type directed resolution --- parser-typechecker/src/Unison/UnisonFile.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/parser-typechecker/src/Unison/UnisonFile.hs b/parser-typechecker/src/Unison/UnisonFile.hs index 825e99914..0b82e51c1 100644 --- a/parser-typechecker/src/Unison/UnisonFile.hs +++ b/parser-typechecker/src/Unison/UnisonFile.hs @@ -94,7 +94,8 @@ environmentFor termBuiltins typeBuiltins0 dataDecls0 effectDecls0 = typesByName = Map.toList $ (fst <$> dataDecls'') `Map.union` (fst <$> effectDecls'') ctorLookup = Map.fromList (constructors' =<< hashDecls') in Env dataDecls'' effectDecls'' - (Term.bindBuiltins dataAndEffectCtors termBuiltins typesByName) + (Term.typeDirectedResolve . + Term.bindBuiltins dataAndEffectCtors termBuiltins typesByName) (Type.bindBuiltins typesByName) ctorLookup From c0beac042ab4ee852a3394fe49c99d555a91ca1a Mon Sep 17 00:00:00 2001 From: Runar Bjarnason Date: Wed, 1 Aug 2018 12:58:05 -0400 Subject: [PATCH 10/11] progress --- parser-typechecker/src/Unison/Builtin.hs | 4 ++ parser-typechecker/src/Unison/FileParser.hs | 5 ++- parser-typechecker/src/Unison/Parsers.hs | 8 +++- parser-typechecker/src/Unison/Typechecker.hs | 40 ++++++++++++++----- parser-typechecker/src/Unison/UnisonFile.hs | 14 +++++-- .../tests/Unison/Test/FileParser.hs | 2 +- .../tests/Unison/Test/Typechecker.hs | 2 +- 7 files changed, 55 insertions(+), 20 deletions(-) diff --git a/parser-typechecker/src/Unison/Builtin.hs b/parser-typechecker/src/Unison/Builtin.hs index 945b4c94e..b044be9f4 100644 --- a/parser-typechecker/src/Unison/Builtin.hs +++ b/parser-typechecker/src/Unison/Builtin.hs @@ -65,6 +65,10 @@ builtinDataAndEffectCtors = (mkConstructors =<< builtinDataDecls') builtinTerms :: forall v. Var v => [(v, R.Reference)] builtinTerms = (\r -> (toSymbol r, r)) <$> Map.keys (builtins @v) +builtinTypedTerms :: forall v. Var v => [(v, (R.Reference, Type v))] +builtinTypedTerms = + (\(r, t) -> (toSymbol r, (r, t))) <$> Map.toList (builtins @v) + builtinTypes :: forall v. Var v => [(v, R.Reference)] builtinTypes = builtinTypes' ++ (f <$> Map.toList (builtinDataDecls @v)) where f (r@(R.Builtin s), _) = (Var.named s, r) diff --git a/parser-typechecker/src/Unison/FileParser.hs b/parser-typechecker/src/Unison/FileParser.hs index 2380ca6dc..3bc51bba6 100644 --- a/parser-typechecker/src/Unison/FileParser.hs +++ b/parser-typechecker/src/Unison/FileParser.hs @@ -24,7 +24,10 @@ import Unison.Var (Var) import Unison.Reference (Reference) -- import Debug.Trace -file :: Var v => [(v, Reference)] -> [(v, Reference)] -> P v (UnisonFile v Ann) +file :: Var v + => [(v, (Reference, AnnotatedType v Ann))] + -> [(v, Reference)] + -> P v (UnisonFile v Ann) file builtinTerms builtinTypes = do traceRemainingTokens "file before parsing declarations" _ <- openBlock diff --git a/parser-typechecker/src/Unison/Parsers.hs b/parser-typechecker/src/Unison/Parsers.hs index c523e6e5f..194529e36 100644 --- a/parser-typechecker/src/Unison/Parsers.hs +++ b/parser-typechecker/src/Unison/Parsers.hs @@ -29,8 +29,12 @@ parseType :: Var v => String -> PEnv -> Either (Parser.Err v) (AnnotatedType v A parseType s = Parser.run (Parser.root TypeParser.valueType) s parseFile :: Var v => FilePath -> String -> PEnv -> Either (Parser.Err v) (UnisonFile v Ann) -parseFile filename s = Parser.run' - (Parser.rootFile $ FileParser.file Builtin.builtinTerms Builtin.builtinTypes) s filename +parseFile filename s = + Parser.run' + (Parser.rootFile $ FileParser.file + Builtin.builtinTypedTerms + Builtin.builtinTypes) + s filename unsafeParseTerm :: Var v => String -> PEnv -> AnnotatedTerm v Ann unsafeParseTerm s = fmap (unsafeGetRightFrom s) . parseTerm $ s diff --git a/parser-typechecker/src/Unison/Typechecker.hs b/parser-typechecker/src/Unison/Typechecker.hs index 8bf5f9221..03f4ae290 100644 --- a/parser-typechecker/src/Unison/Typechecker.hs +++ b/parser-typechecker/src/Unison/Typechecker.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TupleSections #-} @@ -7,21 +8,22 @@ module Unison.Typechecker where -import Unison.Term (AnnotatedTerm) -import Unison.Type (AnnotatedType) -import Unison.Var (Var) -import Unison.DataDeclaration (DataDeclaration', EffectDeclaration') -import Unison.Reference (Reference) -import qualified Unison.Result as Result -import Unison.Result (Result(..), Note) --- import qualified Data.Map as Map -import Data.Maybe (isJust) +import Data.Maybe (isJust) import qualified Unison.ABT as ABT --- import qualified Unison.Paths as Paths +import qualified Unison.Blank as B +import Unison.DataDeclaration (DataDeclaration', EffectDeclaration') +import Unison.Reference (Reference) +import Unison.Result (Result(..), Note(..)) +import qualified Unison.Result as Result +import Unison.Term (AnnotatedTerm) import qualified Unison.Term as Term --- import qualified Unison.Type as Type +import Unison.Type (AnnotatedType) import qualified Unison.TypeVar as TypeVar import qualified Unison.Typechecker.Context as Context +import Unison.Var (Var) +-- import qualified Data.Map as Map +-- import qualified Unison.Paths as Paths +-- import qualified Unison.Type as Type -- import Debug.Trace -- watch msg a = trace (msg ++ show a) a @@ -121,6 +123,22 @@ synthesize env t = (effectDeclaration env) (Term.vtmap TypeVar.Universal t) +resolveAndSynthesize + :: (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 + -- | Check whether a term matches a type, using a -- function to resolve the type of @Ref@ constructors -- contained in the term. Returns @typ@ if successful, diff --git a/parser-typechecker/src/Unison/UnisonFile.hs b/parser-typechecker/src/Unison/UnisonFile.hs index 0b82e51c1..50099b05f 100644 --- a/parser-typechecker/src/Unison/UnisonFile.hs +++ b/parser-typechecker/src/Unison/UnisonFile.hs @@ -53,19 +53,21 @@ data Env v a = Env , resolveType :: AnnotatedType v a -> AnnotatedType v a -- `String` to `(Reference, ConstructorId)` , constructorLookup :: CtorLookup + , terms :: Map v (Reference, AnnotatedType v a) } -- This function computes hashes for data and effect declarations, and -- also returns a function for resolving strings to (Reference, ConstructorId) -- for parsing of pattern matching environmentFor :: forall v a . Var v - => [(v, Reference)] + => [(v, (Reference, AnnotatedType v a))] -> [(v, Reference)] -> Map v (DataDeclaration' v a) -> Map v (EffectDeclaration' v a) -> Env v a -environmentFor termBuiltins typeBuiltins0 dataDecls0 effectDecls0 = +environmentFor termBuiltins0 typeBuiltins0 dataDecls0 effectDecls0 = let -- ignore builtin types that will be shadowed by user-defined data/effects + termBuiltins = fmap fst <$> termBuiltins0 typeBuiltins = [ (v, t) | (v, t) <- typeBuiltins0, Map.notMember v dataDecls0 && Map.notMember v effectDecls0] @@ -82,7 +84,8 @@ environmentFor termBuiltins typeBuiltins0 dataDecls0 effectDecls0 = typeEnv :: [(v, Reference)] typeEnv = Map.toList (fst <$> dataDecls') ++ Map.toList (fst <$> effectDecls') dataDecls'' = second (DD.bindBuiltins typeEnv) <$> dataDecls' - effectDecls'' = second (DD.withEffectDecl (DD.bindBuiltins typeEnv)) <$> effectDecls' + effectDecls'' = + second (DD.withEffectDecl (DD.bindBuiltins typeEnv)) <$> effectDecls' dataRefs = Set.fromList $ (fst <$> Foldable.toList dataDecls'') termFor :: Reference -> Int -> AnnotatedTerm2 v a a v () termFor r cid = if Set.member r dataRefs then Term.constructor() r cid @@ -98,9 +101,12 @@ environmentFor termBuiltins typeBuiltins0 dataDecls0 effectDecls0 = Term.bindBuiltins dataAndEffectCtors termBuiltins typesByName) (Type.bindBuiltins typesByName) ctorLookup + (Map.fromList termBuiltins0) constructors' :: Var v => (v, Reference, DataDeclaration' v a) -> [(String, (Reference, Int))] constructors' (typeSymbol, r, dd) = let qualCtorName ((ctor,_), i) = - (Text.unpack $ mconcat [Var.qualifiedName typeSymbol, ".", Var.qualifiedName ctor], (r, i)) + ( Text.unpack $ + mconcat [Var.qualifiedName typeSymbol, ".", Var.qualifiedName ctor] + , (r, i)) in qualCtorName <$> DD.constructors dd `zip` [0..] diff --git a/parser-typechecker/tests/Unison/Test/FileParser.hs b/parser-typechecker/tests/Unison/Test/FileParser.hs index 541143fed..9c92f2642 100644 --- a/parser-typechecker/tests/Unison/Test/FileParser.hs +++ b/parser-typechecker/tests/Unison/Test/FileParser.hs @@ -61,7 +61,7 @@ module Unison.Test.FileParser where !p = unsafeGetRightFrom s $ Unison.Parser.run (Parser.rootFile $ - file Builtin.builtinTerms Builtin.builtinTypes) + file Builtin.builtinTypedTerms Builtin.builtinTypes) s builtins pure p >> ok diff --git a/parser-typechecker/tests/Unison/Test/Typechecker.hs b/parser-typechecker/tests/Unison/Test/Typechecker.hs index fe2cf2ee2..769e0db4e 100644 --- a/parser-typechecker/tests/Unison/Test/Typechecker.hs +++ b/parser-typechecker/tests/Unison/Test/Typechecker.hs @@ -298,7 +298,7 @@ test = scope "typechecker" . tests $ |-- binding is not guarded by a lambda, it only can access |-- ambient abilities (which will be empty) |ex1 : {IO} () - |ex1 = launch-missiles() + |ex1 = IO.launch-missiles() | |() |] From 5a2ae3e3d1568949141ac7bc826174b0599676a5 Mon Sep 17 00:00:00 2001 From: Runar Bjarnason Date: Wed, 1 Aug 2018 13:04:55 -0400 Subject: [PATCH 11/11] Added pre-existing terms to type env --- parser-typechecker/src/Unison/FileParsers.hs | 2 +- parser-typechecker/src/Unison/Typechecker.hs | 18 ++++++++++-------- parser-typechecker/tests/Unison/Test/Common.hs | 2 +- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/parser-typechecker/src/Unison/FileParsers.hs b/parser-typechecker/src/Unison/FileParsers.hs index 666ee8d99..b62a9356e 100644 --- a/parser-typechecker/src/Unison/FileParsers.hs +++ b/parser-typechecker/src/Unison/FileParsers.hs @@ -57,7 +57,7 @@ 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 B.builtins n = Typechecker.synthesize env0 term die s h = error $ "unknown " ++ s ++ " reference " ++ show h typeOf r = pure $ fromMaybe (die "value" r) $ Map.lookup r B.builtins diff --git a/parser-typechecker/src/Unison/Typechecker.hs b/parser-typechecker/src/Unison/Typechecker.hs index 03f4ae290..dd27df572 100644 --- a/parser-typechecker/src/Unison/Typechecker.hs +++ b/parser-typechecker/src/Unison/Typechecker.hs @@ -8,6 +8,7 @@ module Unison.Typechecker where +import Data.Map (Map) import Data.Maybe (isJust) import qualified Unison.ABT as ABT import qualified Unison.Blank as B @@ -21,7 +22,7 @@ import Unison.Type (AnnotatedType) import qualified Unison.TypeVar as TypeVar import qualified Unison.Typechecker.Context as Context import Unison.Var (Var) --- import qualified Data.Map as Map + -- import qualified Unison.Paths as Paths -- import qualified Unison.Type as Type @@ -34,13 +35,14 @@ type Type v loc = AnnotatedType v loc failNote :: Note v loc -> Result (Note v loc) a failNote note = Result (pure note) Nothing -data Env f v loc = Env { - builtinLoc :: loc, - ambientAbilities :: [Type v loc], - typeOf :: Reference -> f (Type v loc), - dataDeclaration :: Reference -> f (DataDeclaration' v loc), - effectDeclaration :: Reference -> f (EffectDeclaration' v loc) -} +data Env f v loc = Env + { builtinLoc :: loc + , ambientAbilities :: [Type v loc] + , typeOf :: Reference -> f (Type v loc) + , dataDeclaration :: Reference -> f (DataDeclaration' v loc) + , effectDeclaration :: Reference -> f (EffectDeclaration' v loc) + , terms :: Map Reference (Type v loc) + } -- -- | Compute the allowed type of a replacement for a given subterm. -- -- Example, in @\g -> map g [1,2,3]@, @g@ has an admissible type of diff --git a/parser-typechecker/tests/Unison/Test/Common.hs b/parser-typechecker/tests/Unison/Test/Common.hs index 5f6073493..b473172ad 100644 --- a/parser-typechecker/tests/Unison/Test/Common.hs +++ b/parser-typechecker/tests/Unison/Test/Common.hs @@ -33,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 B.builtins where typeOf r = maybe (error $ "no type for: " ++ show r) pure $ Map.lookup r B.builtins dd r = error $ "no data declaration for: " ++ show r ed r = error $ "no effect declaration for: " ++ show r