From bde5e3c8ba197ab93fbab0f2ee945827606cfbf0 Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 17 Jul 2018 13:35:23 -0400 Subject: [PATCH] filled in synthesize for let of binding that is a closed expression --- parser-typechecker/src/Unison/ABT.hs | 20 +++++++ parser-typechecker/src/Unison/Term.hs | 7 ++- .../src/Unison/Typechecker/Context2.hs | 59 ++++++++++++++----- 3 files changed, 68 insertions(+), 18 deletions(-) diff --git a/parser-typechecker/src/Unison/ABT.hs b/parser-typechecker/src/Unison/ABT.hs index 29be33955..ad5d7235f 100644 --- a/parser-typechecker/src/Unison/ABT.hs +++ b/parser-typechecker/src/Unison/ABT.hs @@ -12,6 +12,7 @@ module Unison.ABT where import Control.Applicative +import Control.Monad import Data.List hiding (cycle) import Data.Maybe import Data.Ord @@ -285,6 +286,25 @@ 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) +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 + Var v -> annotatedVar a v + Cycle body -> cycle' a (go bound body) + Abs x body -> abs' a x (go (Set.insert x bound) body) + Tm body -> tm' a (go bound <$> body) + +foreachSubterm + :: (Traversable f, Applicative g, Ord v) + => (Term f v a -> g b) + -> Term f v a + -> g [b] +foreachSubterm f e = case out e of + Var _ -> pure <$> f e + Cycle body -> liftA2 (:) (f e) (foreachSubterm f body) + Abs _ body -> liftA2 (:) (f e) (foreachSubterm f body) + Tm body -> liftA2 (:) (f e) (join . Foldable.toList <$> (sequenceA $ foreachSubterm f <$> body)) + -- | `visit f t` applies an effectful function to each subtree of -- `t` and sequences the results. When `f` returns `Nothing`, `visit` -- descends into the children of the current subtree. When `f` returns diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 6885ed21d..49d305e7d 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -185,10 +185,10 @@ derived = ref . Reference.Derived derived' :: Ord v => Text -> Maybe (Term' vt v) derived' base58 = derived <$> Hash.fromBase58 base58 -ref :: Ord v => Reference -> Term' vt v +ref :: Ord v => Reference -> ABT.Term (F vt at) v () ref r = ABT.tm (Ref r) -builtin :: Ord v => Text -> Term' vt v +builtin :: Ord v => Text -> ABT.Term (F vt at) v () builtin n = ref (Reference.Builtin n) float :: Ord v => Double -> Term' vt v @@ -236,6 +236,9 @@ iff cond t f = ABT.tm (If cond t f) ann :: Ord v => Term' vt v -> Type vt -> Term' vt v ann e t = ABT.tm (Ann e t) +ann' :: Ord v => a -> ABT.Term (F vt at) v a -> Type.AnnotatedType vt at -> ABT.Term (F vt at) v a +ann' a e t = ABT.tm' a (Ann e t) + vector :: Ord v => [Term' vt v] -> Term' vt v vector es = ABT.tm (Vector (Vector.fromList es)) diff --git a/parser-typechecker/src/Unison/Typechecker/Context2.hs b/parser-typechecker/src/Unison/Typechecker/Context2.hs index 9deff91ee..7957a2833 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context2.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context2.hs @@ -89,6 +89,7 @@ data Note v loc | WithinSynthesizeApp (Type v loc) (Term v loc) (Note 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 @@ -332,6 +333,14 @@ orElse m1 m2 = M go where r @ (_, Just (_, _)) -> r _ -> runM m2 menv +-- If the action fails, preserve all the notes it emitted and then return the +-- provided `a`; if the action succeeds, we're good, just use its result +recover :: a -> M v loc a -> M v loc a +recover ifFail (M action) = M go where + go menv = case action menv of + (notes, Nothing) -> (notes, Just (ifFail, env menv)) + r -> r + getDataDeclarations :: M v loc (DataDeclarations v loc) getDataDeclarations = M $ fromMEnv dataDecls @@ -519,22 +528,21 @@ synthesize e = withinSynthesize e $ go (minimize' e) go (Term.Vector' v) = do ft <- vectorConstructorOfArity (Foldable.length v) foldM synthesizeApp ft v - -- go (Term.Let1' binding e) | Set.null (ABT.freeVars binding) = do - -- -- special case when it is definitely safe to generalize - binding contains - -- -- no free variables, i.e. `let id x = x in ...` - -- decls <- getDataDeclarations - -- abilities <- getAbilities - -- t <- scope "let1 closed" $ synthesizeClosed' abilities decls binding - -- v' <- ABT.freshen e freshenVar - -- e <- pure $ ABT.bind e (Term.builtin (Var.name v') `Term.ann` t) - -- synthesize e - -- --go (Term.Let1' binding e) = do - -- -- -- literally just convert to a lambda application and call synthesize! - -- -- -- NB: this misses out on let generalization - -- -- -- let x = blah p q in foo y <=> (x -> foo y) (blah p q) - -- -- v' <- ABT.freshen e freshenVar - -- -- e <- pure $ ABT.bind e (Term.var v') - -- -- synthesize (Term.lam v' e `Term.app` binding) + go (Term.Let1' binding e) | Set.null (ABT.freeVars binding) = do + -- special case when it is definitely safe to generalize - binding contains + -- no free variables, i.e. `let id x = x in ...` + abilities <- getAbilities + t <- synthesizeClosed' abilities binding + v' <- ABT.freshen e freshenVar + e <- pure $ ABT.bindInheritAnnotation e (Term.ann' () (Term.builtin (Var.name v')) t) + synthesize e + --go (Term.Let1' binding e) = do + -- -- literally just convert to a lambda application and call synthesize! + -- -- NB: this misses out on let generalization + -- -- let x = blah p q in foo y <=> (x -> foo y) (blah p q) + -- v' <- ABT.freshen e freshenVar + -- e <- pure $ ABT.bind e (Term.var v') + -- synthesize (Term.lam v' e `Term.app` binding) -- go (Term.Let1' binding e) = do -- -- note: no need to freshen binding, it can't refer to v -- tbinding <- synthesize binding @@ -915,6 +923,25 @@ abilityCheck requested = do ambient <- getAbilities abilityCheck' ambient requested +verifyDataDeclarations :: (Eq loc, Var v) => DataDeclarations v loc -> M v loc () +verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do + let ctors = DD.constructors decl + forM_ ctors $ \(_ctorName,typ) -> + let isBoundIn v t = Set.member v (snd (ABT.annotation t)) + loc t = fst (ABT.annotation t) + go t@(ABT.Var' v) | not (isBoundIn v t) = recover () $ failNote (UnknownSymbol (loc t) v) + go _ = pure () + in ABT.foreachSubterm go (ABT.annotateBound typ) + +synthesizeClosed' :: (Eq loc, Var v) + => [Type v loc] + -> Term v loc + -> M v loc (Type v loc) +synthesizeClosed' abilities term = do + t <- withEffects0 abilities (synthesize term) + ctx <- getContext + pure $ generalizeExistentials ctx t + instance (Var v, Show loc) => Show (Element v loc) where show (Var v) = case v of TypeVar.Universal x -> "@" <> show x