diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Parser/Core.hs | 19 | ||||
| -rw-r--r-- | src/Script/Expr.hs | 67 |
2 files changed, 83 insertions, 3 deletions
diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs index 7b4da17..cd4031a 100644 --- a/src/Parser/Core.hs +++ b/src/Parser/Core.hs @@ -108,7 +108,7 @@ lookupVarExpr off sline name = do ExprTypeConstr1 _ -> return $ SomeExpr $ (Undefined "incomplete type" :: Expr DynamicType) ExprTypeVar tvar -> return $ SomeExpr $ DynVariable tvar sline fqn ExprTypeFunction args (_ :: Proxy a) -> return $ SomeExpr $ (FunVariable args sline fqn :: Expr (FunctionType a)) - stype@ExprTypeApp {} -> do + stype -> do tvar <- newTypeVar modify $ \s -> s { testTypeUnif = M.insert tvar stype $ testTypeUnif s } return $ SomeExpr $ DynVariable tvar sline fqn @@ -122,7 +122,7 @@ lookupScalarVarExpr off sline name = do ExprTypeVar tvar -> return $ SomeExpr $ DynVariable tvar sline fqn ExprTypeFunction args (pa :: Proxy a) -> do SomeExpr <$> unifyExpr off pa (FunVariable args sline fqn :: Expr (FunctionType a)) - stype@ExprTypeApp {} -> do + stype -> do tvar <- newTypeVar modify $ \s -> s { testTypeUnif = M.insert tvar stype $ testTypeUnif s } return $ SomeExpr $ DynVariable tvar sline fqn @@ -219,6 +219,21 @@ unifyExpr off pa expr = if _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) (ExprTypeVar tvar) return $ Variable sline name + | HideType expr' <- expr + -> do + unifyExpr off pa expr' + + | TypeQuant qvar expr' <- expr + -> do + tvar <- newTypeVar + unifyExpr off pa $ renameTypeVar qvar tvar expr' + + | TypeLambda t tvar f <- expr + -> do + _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) t + Just (ExprTypePrim pt) <- M.lookup tvar <$> gets testTypeUnif + unifyExpr off pa (f $ ExprTypePrim pt) + | Just (Refl :: FunctionType a :~: b) <- eqT -> do let FunctionArguments remaining = exprArgs expr diff --git a/src/Script/Expr.hs b/src/Script/Expr.hs index cc37f73..de66412 100644 --- a/src/Script/Expr.hs +++ b/src/Script/Expr.hs @@ -8,6 +8,7 @@ module Script.Expr ( FunctionType, DynamicType, ExprType(..), SomeExpr(..), TypeVar(..), SomeExprType(..), someExprType, textSomeExprType, + renameTypeVar, VarValue(..), SomeVarValue(..), svvVariables, svvArguments, @@ -61,6 +62,9 @@ data Expr a where ArgsApp :: ExprType a => FunctionArguments SomeExpr -> Expr (FunctionType a) -> Expr (FunctionType a) FunctionAbstraction :: ExprType a => Expr a -> Expr (FunctionType a) FunctionEval :: ExprType a => SourceLine -> Expr (FunctionType a) -> Expr a + HideType :: forall a. ExprType a => Expr a -> Expr DynamicType + TypeLambda :: forall a. ExprType a => SomeExprType -> TypeVar -> (SomeExprType -> Expr a) -> Expr DynamicType + TypeQuant :: forall a. ExprType a => TypeVar -> Expr a -> Expr DynamicType LambdaAbstraction :: ExprType a => TypedVarName a -> Expr b -> Expr (a -> b) Pure :: a -> Expr a App :: AppAnnotation b -> Expr (a -> b) -> Expr a -> Expr b @@ -101,6 +105,9 @@ mapExpr f = go ArgsApp args expr -> f $ ArgsApp (fmap (\(SomeExpr e) -> SomeExpr (go e)) args) (go expr) FunctionAbstraction expr -> f $ FunctionAbstraction (go expr) FunctionEval sline expr -> f $ FunctionEval sline (go expr) + HideType expr -> HideType $ go expr + TypeLambda stype tvar efun -> TypeLambda stype tvar $ (go . efun) + TypeQuant tvar expr -> TypeQuant tvar $ go expr LambdaAbstraction tvar expr -> f $ LambdaAbstraction tvar (go expr) e@Pure {} -> f e App ann efun earg -> f $ App ann (go efun) (go earg) @@ -194,6 +201,9 @@ eval = \case let cs' = CallStack (( sline, vars ) : cs) FunctionType fun <- withVar callStackVarName cs' $ eval efun return $ fun cs' mempty + HideType expr -> return $ DynamicType expr + e@TypeLambda {} -> return $ DynamicType e + e@TypeQuant {} -> return $ DynamicType e LambdaAbstraction (TypedVarName name) expr -> do gdefs <- askGlobalDefs dict <- askDictionary @@ -239,7 +249,7 @@ instance ExprType a => ExprType (FunctionType a) where textExprType _ = "function type" textExprValue _ = "<function type>" -data DynamicType +data DynamicType = forall a. ExprType a => DynamicType (Expr a) instance ExprType DynamicType where textExprType _ = "ambiguous type" @@ -257,6 +267,7 @@ data SomeExprType | ExprTypeVar TypeVar | forall a. ExprType a => ExprTypeFunction (FunctionArguments SomeArgumentType) (Proxy a) | ExprTypeApp SomeExprType [ SomeExprType ] + | ExprTypeForall TypeVar SomeExprType someExprType :: SomeExpr -> SomeExprType someExprType (SomeExpr expr) = go expr @@ -286,6 +297,56 @@ someExprType (SomeExpr expr) = go expr proxyOfFunctionType :: Expr (FunctionType a) -> Proxy a proxyOfFunctionType _ = Proxy +renameTypeVar :: TypeVar -> TypeVar -> Expr a -> Expr a +renameTypeVar a b = go + where + go :: Expr e -> Expr e + go orig = case orig of + Let sline vname x y -> Let sline vname (go x) (go y) + Variable {} -> orig + DynVariable tvar sline name + | tvar == a -> DynVariable b sline name + | otherwise -> orig + FunVariable {} -> orig + ArgsReq args body -> ArgsReq args (go body) + ArgsApp args fun -> ArgsApp (fmap (renameTypeVarInSomeExpr a b) args) (go fun) + FunctionAbstraction expr -> FunctionAbstraction (go expr) + FunctionEval sline expr -> FunctionEval sline (go expr) + HideType expr -> HideType (go expr) + TypeLambda stype tvar expr + | tvar == a -> TypeLambda (renameVarInType a b stype) b expr + | otherwise -> TypeLambda (renameVarInType a b stype) tvar (go . expr) + TypeQuant tvar expr + | tvar == a -> orig + | tvar == b -> error "type var collision" + | otherwise -> TypeQuant tvar (go expr) + LambdaAbstraction vname expr -> LambdaAbstraction vname (go expr) + Pure {} -> orig + App ann f x -> App ann (go f) (go x) + Concat xs -> Concat (map go xs) + Regex xs -> Regex (map go xs) + Undefined {} -> orig + Trace expr -> Trace (go expr) + +renameTypeVarInSomeExpr :: TypeVar -> TypeVar -> SomeExpr -> SomeExpr +renameTypeVarInSomeExpr a b (SomeExpr e) = SomeExpr (renameTypeVar a b e) + +renameVarInType :: TypeVar -> TypeVar -> SomeExprType -> SomeExprType +renameVarInType a b = go + where + go orig = case orig of + ExprTypePrim {} -> orig + ExprTypeConstr1 {} -> orig + ExprTypeVar tvar | tvar == a -> ExprTypeVar b + | otherwise -> orig + ExprTypeFunction {} -> orig + ExprTypeApp c xs -> ExprTypeApp (go c) (map go xs) + ExprTypeForall tvar stype + | tvar == a -> orig + | tvar == b -> error "type var collision" + | otherwise -> ExprTypeForall tvar (go stype) + + textSomeExprType :: SomeExprType -> Text textSomeExprType = go [] where @@ -295,6 +356,7 @@ textSomeExprType = go [] go _ (ExprTypeVar (TypeVar name)) = name go _ (ExprTypeFunction _ r) = "function:" <> textExprType r go _ (ExprTypeApp c xs) = go (map textSomeExprType xs) c + go _ (ExprTypeForall (TypeVar name) ctype) = "∀" <> name <> "." <> go [] ctype data AsFunType a = forall b. (a ~ FunctionType b, ExprType b) => IsFunType @@ -432,6 +494,9 @@ gatherVars = fmap (uniqOn fst . sortOn fst) . helper return $ concat (v : vs) FunctionAbstraction expr -> helper expr FunctionEval _ efun -> helper efun + HideType expr -> helper expr + TypeLambda {} -> return [] + TypeQuant _ expr -> helper expr LambdaAbstraction (TypedVarName var) expr -> withDictionary (filter ((var /=) . fst)) $ helper expr Pure _ -> return [] e@(App (AnnRecord sel) _ x) |