minor cleanup

This commit is contained in:
Arya Irani 2018-08-17 22:30:00 -04:00
parent d85de446b6
commit da9d46001b
3 changed files with 19 additions and 18 deletions

View File

@ -512,14 +512,16 @@ typeErrorFromNote n@(C.Note (C.TypeMismatch ctx) path) =
Just (foundType, expectedType),
Just mismatchSite) ->
let mismatchLoc = ABT.annotation mismatchSite
booleanMismatch :: Monad m => m a -> BooleanMismatch -> m (TypeError v loc)
booleanMismatch
:: Monad m => m a -> BooleanMismatch -> m (TypeError v loc)
booleanMismatch x y = x >>
(pure $ BooleanMismatch y (ABT.annotation mismatchSite) foundType n)
existentialMismatch :: Monad m
=> m loc -> ExistentialMismatch -> m (TypeError v loc)
existentialMismatch
:: Monad m => m loc -> ExistentialMismatch -> m (TypeError v loc)
existentialMismatch x y = x >>= \expectedLoc -> pure $
ExistentialMismatch y expectedType expectedLoc foundType mismatchLoc n
and,or,cond,guard :: Ex.NoteExtractor v loc (TypeError v loc)
and,or,cond,guard,ifBody,vectorBody,caseBody,all
:: Ex.NoteExtractor v loc (TypeError v loc)
and = booleanMismatch Ex.inAndApp AndMismatch
or = booleanMismatch Ex.inOrApp OrMismatch
cond = booleanMismatch Ex.inIfCond CondMismatch
@ -527,7 +529,6 @@ typeErrorFromNote n@(C.Note (C.TypeMismatch ctx) path) =
ifBody = existentialMismatch Ex.inIfBody IfBody
vectorBody = existentialMismatch Ex.inVectorApp VectorBody
caseBody = existentialMismatch Ex.inMatchCaseBody CaseBody
all :: Ex.NoteExtractor v loc (TypeError v loc)
all = and <|> or <|> cond <|> guard <|>
ifBody <|> vectorBody <|> caseBody

View File

@ -112,9 +112,9 @@ data PathElement v loc
| InAndApp
| InOrApp
| InIfCond
| InIfBody loc
| InVectorApp loc
| InMatch loc
| InIfBody loc -- location of `then` expression
| InVectorApp loc -- location of 1st vector element
| InMatch loc -- location of 1st case body
deriving Show
type ExpectedArgCount = Int
@ -612,9 +612,9 @@ synthesize e = scope (InSynthesize e) $ do
go (Term.Vector' v) = do
ft <- vectorConstructorOfArity (Foldable.length v)
case Foldable.toList v of
(v1:_:_) ->
scope (InVectorApp (ABT.annotation v1)) $ foldM synthesizeApp ft v
_ -> foldM synthesizeApp ft v
[] -> pure ft
v1 : _ ->
scope (InVectorApp (ABT.annotation v1)) $ 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 ...`
@ -711,10 +711,10 @@ synthesize e = scope (InSynthesize e) $ do
outputTypev <- freshenVar (Var.named "match-output")
let outputType = Type.existential' l B.Blank outputTypev
appendContext $ context [existential outputTypev]
case cases of
case cases of -- only relevant with 2 or more cases, but 1 is safe too.
[] -> pure ()
Term.MatchCase _ _ t : _ -> scope (InMatch (ABT.annotation t)) $
Foldable.traverse_ (checkCase scrutineeType outputType) cases
_ -> pure ()
ctx <- getContext
pure $ apply ctx outputType
go h@(Term.Handle' _ _) = do

View File

@ -23,8 +23,8 @@ _path = NoteExtractor $ pure . toList . C.path
_mismatchedTerm :: NoteExtractor v loc (Maybe (C.Term v loc))
_mismatchedTerm = NoteExtractor $ pure . C.innermostErrorTerm
adjacent :: PathExtractor v loc a -> PathExtractor v loc b -> NoteExtractor v loc (a, b)
adjacent (PathExtractor a) (PathExtractor b) =
_adjacent :: PathExtractor v loc a -> PathExtractor v loc b -> NoteExtractor v loc (a, b)
_adjacent (PathExtractor a) (PathExtractor b) =
NoteExtractor $ go Nothing . toList . C.path where
go _ [] = Nothing
go Nothing (h:t) = go (a h) t
@ -32,6 +32,9 @@ adjacent (PathExtractor a) (PathExtractor b) =
type PathPredicate v loc = C.PathElement v loc -> Bool
_fromPredicate :: (PathPredicate v loc) -> PathExtractor v loc ()
_fromPredicate e = PathExtractor (\p -> whenM (e p) (pure ()))
exactly1AppBefore :: PathExtractor v loc a -> NoteExtractor v loc a
exactly1AppBefore p = do
(prefix, a) <- elementsUntil p
@ -94,9 +97,6 @@ inSynthesizeApp = PathExtractor $ \case
C.InSynthesizeApp t e -> Just (t,e)
_ -> Nothing
fromPredicate :: (PathPredicate v loc) -> PathExtractor v loc ()
fromPredicate e = PathExtractor (\p -> whenM (e p) (pure ()))
-- App
-- | Handle v