From 2ea049cea9c11781a8e85b195bb15f40f1323f41 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Fri, 15 Jul 2022 19:39:11 +0300 Subject: [PATCH] Refine hole in type signature to function type (#1379) * infer hole in type from pattern * Refine hole in signature when patterns are found * fix --- src/Juvix/Syntax/MicroJuvix/Error/Types.hs | 4 +- src/Juvix/Syntax/MicroJuvix/Language/Extra.hs | 11 ++- src/Juvix/Syntax/MicroJuvix/TypeChecker.hs | 76 +++++++++++-------- .../MicroJuvix/TypeChecker/Inference.hs | 31 ++++---- test/TypeCheck/Positive.hs | 4 + tests/positive/272/M.juvix | 28 +++++++ tests/positive/272/juvix.yaml | 0 7 files changed, 103 insertions(+), 51 deletions(-) create mode 100644 tests/positive/272/M.juvix create mode 100644 tests/positive/272/juvix.yaml diff --git a/src/Juvix/Syntax/MicroJuvix/Error/Types.hs b/src/Juvix/Syntax/MicroJuvix/Error/Types.hs index 6ee7389c50..8fcd473f98 100644 --- a/src/Juvix/Syntax/MicroJuvix/Error/Types.hs +++ b/src/Juvix/Syntax/MicroJuvix/Error/Types.hs @@ -9,8 +9,8 @@ import Juvix.Syntax.MicroJuvix.Language -- not match the type of the inductive being matched data WrongConstructorType = WrongConstructorType { _wrongCtorTypeName :: Name, - _wrongCtorTypeExpected :: Name, - _wrongCtorTypeActual :: Name, + _wrongCtorTypeExpected :: InductiveName, + _wrongCtorTypeActual :: InductiveName, _wrongCtorTypeFunName :: Name } diff --git a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs index af0e2e0ffb..017003a61f 100644 --- a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs @@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Juvix.Prelude import Juvix.Syntax.MicroJuvix.Language +import Juvix.Syntax.MicroJuvix.LocalVars data Caller = CallerInductive InductiveName @@ -192,7 +193,12 @@ typeAbstraction :: IsImplicit -> Name -> FunctionParameter typeAbstraction i var = FunctionParameter (Just var) i (ExpressionUniverse (SmallUniverse (getLoc var))) unnamedParameter :: Expression -> FunctionParameter -unnamedParameter = FunctionParameter Nothing Explicit +unnamedParameter ty = + FunctionParameter + { _paramName = Nothing, + _paramImplicit = Explicit, + _paramType = ty + } renameToSubsE :: Rename -> SubsE renameToSubsE = fmap (ExpressionIden . IdenVar) @@ -272,6 +278,9 @@ substitutionApp (mv, ty) = case mv of Nothing -> id Just v -> substitutionE (HashMap.singleton v ty) +localsToSubsE :: LocalVars -> SubsE +localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap + substitutionE :: SubsE -> Expression -> Expression substitutionE m = go where diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs index 0e67fded72..9b04112c65 100644 --- a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs @@ -89,7 +89,7 @@ checkFunctionDefType :: forall r. Members '[Inference] r => Expression -> Sem r checkFunctionDefType = traverseOf_ (leafExpressions . _ExpressionHole) go where go :: Hole -> Sem r () - go h = void (freshMetavar h) + go h = freshMetavar h checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r => @@ -138,38 +138,45 @@ checkFunctionClauseBody locals expectedTy body = runReader locals (checkExpression expectedTy body) checkFunctionClause :: + forall r. Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Inference] r => FunctionInfo -> FunctionClause -> Sem r FunctionClause checkFunctionClause info FunctionClause {..} = do - let (argTys, rty) = unfoldFunType (info ^. functionInfoDef . funDefType) - (patTys, restTys) = splitAt (length _clausePatterns) argTys - bodyTy = foldFunType restTys rty - if - | length patTys /= length _clausePatterns -> impossible - | otherwise -> do - locals <- checkPatterns _clauseName (zipExact patTys _clausePatterns) - let bodyTy' = - substitutionE - ( fmap - (ExpressionIden . IdenVar) - (locals ^. localTyMap) - ) - bodyTy - _clauseBody' <- checkFunctionClauseBody locals bodyTy' _clauseBody - return - FunctionClause - { _clauseBody = _clauseBody', - .. - } - -checkPatterns :: - Members '[Reader InfoTable, Error TypeCheckerError, Inference, NameIdGen] r => - FunctionName -> - [(FunctionParameter, Pattern)] -> - Sem r LocalVars -checkPatterns name = execState emptyLocalVars . mapM_ (uncurry (checkPattern name)) + (locals, bodyTy) <- helper _clausePatterns clauseType + let bodyTy' = substitutionE (localsToSubsE locals) bodyTy + _clauseBody' <- checkFunctionClauseBody locals bodyTy' _clauseBody + return + FunctionClause + { _clauseBody = _clauseBody', + .. + } + where + clauseType :: Expression + clauseType = info ^. functionInfoDef . funDefType + helper :: [Pattern] -> Expression -> Sem r (LocalVars, Expression) + helper pats ty = runState emptyLocalVars (go pats ty) + go :: [Pattern] -> Expression -> Sem (State LocalVars ': r) Expression + go pats bodyTy = case pats of + [] -> return bodyTy + (p : ps) -> case bodyTy of + ExpressionHole h -> do + s <- queryMetavar h + case s of + Just h' -> go pats h' + Nothing -> do + freshMetavar h + l <- ExpressionHole <$> freshHole (getLoc h) + r <- ExpressionHole <$> freshHole (getLoc h) + let fun = ExpressionFunction (Function (unnamedParameter l) r) + whenJustM (matchTypes (ExpressionHole h) fun) impossible + go pats fun + _ -> case unfoldFunType bodyTy of + ([], _) -> error "too many patterns" + (par : pars, ret) -> do + checkPattern _clauseName par p + go ps (foldFunType pars ret) typeOfArg :: FunctionParameter -> Expression typeOfArg = (^. paramType) @@ -303,7 +310,7 @@ freshHole :: Members '[Inference, NameIdGen] r => Interval -> Sem r Hole freshHole l = do uid <- freshNameId let h = Hole uid l - void (freshMetavar h) + freshMetavar h return h -- | Returns {A : Expression} → A @@ -345,9 +352,18 @@ inferExpression' e = case e of ExpressionApplication a -> inferApplication a ExpressionLiteral l -> goLiteral l ExpressionFunction f -> goExpressionFunction f - ExpressionHole h -> freshMetavar h + ExpressionHole h -> inferHole h ExpressionUniverse u -> goUniverse u where + inferHole :: Hole -> Sem r TypedExpression + inferHole h = do + freshMetavar h + return + TypedExpression + { _typedExpression = ExpressionHole h, + _typedType = ExpressionUniverse (SmallUniverse (getLoc h)) + } + goUniverse :: SmallUniverse -> Sem r TypedExpression goUniverse u = return diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs index abc390260c..14c8940e7d 100644 --- a/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs +++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs @@ -18,7 +18,6 @@ data MatchError = MatchError makeLenses ''MatchError data Inference m a where - FreshMetavar :: Hole -> Inference m TypedExpression MatchTypes :: Expression -> Expression -> Inference m (Maybe MatchError) QueryMetavar :: Hole -> Inference m (Maybe Expression) NormalizeType :: Expression -> Inference m Expression @@ -93,29 +92,25 @@ normalizeType' = go Fresh -> return (ExpressionHole h) Refined r -> go r +freshMetavar :: Members '[Inference] r => Hole -> Sem r () +freshMetavar = void . queryMetavar + +queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression) +queryMetavar' h = do + m <- gets (^. inferenceMap . at h) + case m of + Nothing -> do + modify (over inferenceMap (HashMap.insert h Fresh)) + return Nothing + Just Fresh -> return Nothing + Just (Refined e) -> return (Just e) + re :: Member (Error TypeCheckerError) r => Sem (Inference ': r) a -> Sem (State InferenceState ': r) a re = reinterpret $ \case - FreshMetavar h -> freshMetavar' h MatchTypes a b -> matchTypes' a b QueryMetavar h -> queryMetavar' h NormalizeType t -> normalizeType' t where - queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression) - queryMetavar' h = do - s <- getMetavar h - case s of - Fresh -> return Nothing - Refined t -> return (Just t) - - freshMetavar' :: Members '[State InferenceState] r => Hole -> Sem r TypedExpression - freshMetavar' h = do - modify (over inferenceMap (HashMap.insert h Fresh)) - return - TypedExpression - { _typedExpression = ExpressionHole h, - _typedType = ExpressionUniverse (SmallUniverse (getLoc h)) - } - refineFreshMetavar :: Members '[Error TypeCheckerError, State InferenceState] r => Hole -> diff --git a/test/TypeCheck/Positive.hs b/test/TypeCheck/Positive.hs index f689ca1f91..252cd83001 100644 --- a/test/TypeCheck/Positive.hs +++ b/test/TypeCheck/Positive.hs @@ -87,6 +87,10 @@ tests = "Implicit arguments" "MicroJuvix" "Implicit.juvix", + PosTest + "Refine hole in type signature" + "272" + "M.juvix", PosTest "Pattern match a hole type" "265" diff --git a/tests/positive/272/M.juvix b/tests/positive/272/M.juvix new file mode 100644 index 0000000000..f0e5846328 --- /dev/null +++ b/tests/positive/272/M.juvix @@ -0,0 +1,28 @@ +module M; + +inductive Bool { + false : Bool; + true : Bool; +}; + +inductive T { +t : T; +}; + +inductive Nat { + zero : Nat; + suc : Nat → Nat; +}; + +f : _; +f false false ≔ true; +f true _ ≔ false; + +inductive Pair (A : Type) (B : Type) { + mkPair : A → B → Pair A B; +}; + +g : _; +g (mkPair (mkPair zero false) true) ≔ mkPair false zero; + +end; diff --git a/tests/positive/272/juvix.yaml b/tests/positive/272/juvix.yaml new file mode 100644 index 0000000000..e69de29bb2