summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Parser/Core.hs21
-rw-r--r--src/Parser/Expr.hs2
-rw-r--r--src/Script/Expr.hs57
3 files changed, 49 insertions, 31 deletions
diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs
index 6f12af1..3a3450b 100644
--- a/src/Parser/Core.hs
+++ b/src/Parser/Core.hs
@@ -215,19 +215,20 @@ unifyExpr off pa expr = if
, ExprTypeForall qvar itype <- stype
-> do
tvar <- newTypeVar
- _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) $ renameVarInType qvar tvar itype
+ res <- unify off (ExprTypePrim (Proxy :: Proxy a)) $ renameVarInType qvar tvar itype
rtype <- M.lookup tvar <$> gets testTypeUnif
- return $ TypeApp (Variable sline name) $ fromMaybe (ExprTypeVar tvar) rtype
+ return $ ExposePrimType $ TypeApp res (fromMaybe (ExprTypeVar tvar) rtype) (Variable sline name)
| DynVariable stype sline name <- expr
-> do
_ <- unify off (ExprTypePrim (Proxy :: Proxy a)) stype
return $ Variable sline name
- | HideType (ExprTypePrim (_ :: Proxy b'')) (expr' :: Expr b') <- expr
- , Just (Refl :: b'' :~: b') <- eqT
- -> do
- unifyExpr off pa expr'
+ | HidePrimType (_ :: Expr b') <- expr
+ -> unifyExpr off pa (ExposePrimType expr :: Expr b')
+
+ | HideFunType args (_ :: Expr (FunctionType b')) <- expr
+ -> unifyExpr off pa (ExposeFunType args expr :: Expr (FunctionType b'))
| TypeLambda tvar t f <- expr
-> do
@@ -284,13 +285,7 @@ unifySomeExpr off stype sexpr@(SomeExpr (expr :: Expr a))
tvar <- newTypeVar
itype' <- unify off stype $ renameVarInType qvar tvar itype
rtype <- M.lookup tvar <$> gets testTypeUnif
- case itype' of
- ExprTypeFunction _ (ExprTypePrim (Proxy :: Proxy r)) ->
- return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr (FunctionType a))
- ExprTypeFunction _ _ ->
- return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr (FunctionType DynamicType))
- _ ->
- return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr DynamicType)
+ return $ SomeExpr (TypeApp itype' (fromMaybe (ExprTypeVar tvar) rtype) expr)
| ExprTypeFunction args res <- stype
= case someExprType sexpr of
diff --git a/src/Parser/Expr.hs b/src/Parser/Expr.hs
index 16c2b45..c8a9e85 100644
--- a/src/Parser/Expr.hs
+++ b/src/Parser/Expr.hs
@@ -195,7 +195,7 @@ list = label "list" $ do
return $ SomeExpr $
TypeLambda tvar (ExprTypeApp (ExprTypeConstr1 (Proxy :: Proxy [])) [ ExprTypeVar tvar ]) $
\case
- (ExprTypePrim (Proxy :: Proxy a)) -> HideType (ExprTypePrim (Proxy @[ a ])) $ Pure ([] :: [ a ])
+ (ExprTypePrim (Proxy :: Proxy a)) -> HidePrimType $ Pure ([] :: [ a ])
_ -> Undefined "incomplete type"
,do SomeExpr x <- someExpr FunctionTerm
diff --git a/src/Script/Expr.hs b/src/Script/Expr.hs
index 3e56f8e..bff363c 100644
--- a/src/Script/Expr.hs
+++ b/src/Script/Expr.hs
@@ -63,9 +63,12 @@ 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. Typeable a => SomeExprType -> Expr a -> Expr DynamicType
+ HidePrimType :: forall a. ExprType a => Expr a -> Expr DynamicType
+ HideFunType :: forall a. ExprType a => FunctionArguments SomeArgumentType -> Expr (FunctionType a) -> Expr DynamicType
+ ExposePrimType :: forall a. ExprType a => Expr DynamicType -> Expr a
+ ExposeFunType :: forall a. ExprType a => FunctionArguments SomeArgumentType -> Expr DynamicType -> Expr (FunctionType a)
TypeLambda :: TypeVar -> SomeExprType -> (SomeExprType -> Expr DynamicType) -> Expr DynamicType
- TypeApp :: forall a. ExprType a => Expr DynamicType -> SomeExprType -> Expr a
+ TypeApp :: SomeExprType {- result type -} -> SomeExprType {- type argument -} -> Expr DynamicType -> 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
@@ -107,9 +110,12 @@ 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 stype expr -> HideType stype $ go expr
+ HidePrimType expr -> f $ HidePrimType $ go expr
+ HideFunType args expr -> f $ HideFunType args $ go expr
+ ExposePrimType expr -> f $ ExposePrimType $ go expr
+ ExposeFunType args expr -> f $ ExposeFunType args $ go expr
TypeLambda tvar stype efun -> TypeLambda tvar stype (go . efun)
- TypeApp expr stype -> TypeApp (go expr) stype
+ TypeApp restype arg expr -> TypeApp restype arg (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)
@@ -204,19 +210,26 @@ eval = \case
let cs' = CallStack (( sline, vars ) : cs)
FunctionType fun <- withVar callStackVarName cs' $ eval efun
return $ fun cs' mempty
- HideType _ expr -> DynamicType <$> eval expr
+ HidePrimType expr -> DynamicType <$> eval expr
+ HideFunType _ expr -> DynamicType <$> eval expr
+ ExposePrimType expr -> do
+ DynamicType x <- eval expr
+ case cast x of
+ Just x' -> return x'
+ n@Nothing -> fail $ "type error in expose primitive type result " <> show ( typeOf x, typeOf n )
+ ExposeFunType _ expr -> do
+ DynamicType x <- eval expr
+ case cast x of
+ Just x' -> return x'
+ n@Nothing -> fail $ "type error in expose function type result " <> show ( typeOf x, typeOf n )
TypeLambda _ _ f -> do
gdefs <- askGlobalDefs
dict <- askDictionary
return $ DynamicType $ \t -> runSimpleEval (eval $ f t) gdefs dict
- TypeApp expr stype -> do
+ TypeApp _ arg expr -> do
DynamicType f <- eval expr
case cast f of
- Just f' -> do
- case f' stype of
- DynamicType x -> case cast x of
- Just x' -> return x'
- n@Nothing -> fail $ "type error in type application result " <> show ( typeOf x, typeOf n )
+ Just f' -> return (f' arg)
n@Nothing -> fail $ "type error in type application " <> show ( typeOf f, typeOf n )
LambdaAbstraction (TypedVarName name) expr -> do
gdefs <- askGlobalDefs
@@ -298,8 +311,11 @@ someExprType (SomeExpr expr) = go expr
go = \case
DynVariable stype _ _ -> stype
e@(FunVariable args _ _) -> ExprTypeFunction args (ExprTypePrim (proxyOfFunctionType e))
- HideType stype _ -> stype
+ HidePrimType (_ :: Expr a) -> ExprTypePrim (Proxy @a)
+ HideFunType args e -> ExprTypeFunction (ExprTypeArguments args) (ExprTypePrim (proxyOfFunctionType e))
+ e@(ExposeFunType args _) -> ExprTypeFunction (ExprTypeArguments args) (ExprTypePrim (proxyOfFunctionType e))
TypeLambda tvar stype _ -> ExprTypeForall tvar stype
+ TypeApp stype _ _ -> stype
ArgsReq args inner -> exprTypeFunction (fmap snd args) (go inner)
ArgsApp (FunctionArguments used) inner
@@ -333,12 +349,15 @@ renameTypeVar a b = go
ArgsApp args fun -> ArgsApp (fmap (renameTypeVarInSomeExpr a b) args) (go fun)
FunctionAbstraction expr -> FunctionAbstraction (go expr)
FunctionEval sline expr -> FunctionEval sline (go expr)
- HideType stype expr -> HideType (renameVarInType a b stype) (go expr)
+ HidePrimType expr -> HidePrimType (go expr)
+ HideFunType args expr -> HideFunType args (go expr)
+ ExposePrimType {} -> orig
+ ExposeFunType {} -> orig
TypeLambda tvar stype expr
| tvar == a -> orig
| tvar == b -> error "type var collision"
| otherwise -> TypeLambda tvar (renameVarInType a b stype) (go . expr)
- TypeApp expr stype -> TypeApp (go expr) (renameVarInType a b stype)
+ TypeApp restype arg expr -> TypeApp (renameVarInType a b restype) (renameVarInType a b arg) (go expr)
LambdaAbstraction vname expr -> LambdaAbstraction vname (go expr)
Pure {} -> orig
App ann f x -> App ann (go f) (go x)
@@ -460,7 +479,8 @@ exprArgs = \case
in FunctionArguments (args `M.difference` applied)
FunctionAbstraction {} -> mempty
FunctionEval {} -> mempty
- TypeApp {} -> error "exprArgs: type application"
+ ExposePrimType {} -> mempty
+ ExposeFunType args _ -> args
Pure {} -> error "exprArgs: pure"
App {} -> error "exprArgs: app"
Undefined {} -> error "exprArgs: undefined"
@@ -501,9 +521,12 @@ gatherVars = fmap (uniqOn fst . sortOn fst) . helper
return $ concat (v : vs)
FunctionAbstraction expr -> helper expr
FunctionEval _ efun -> helper efun
- HideType _ expr -> helper expr
+ HidePrimType expr -> helper expr
+ HideFunType _ expr -> helper expr
+ ExposePrimType expr -> helper expr
+ ExposeFunType _ expr -> helper expr
TypeLambda {} -> return []
- TypeApp expr _ -> helper expr
+ TypeApp _ _ expr -> helper expr
LambdaAbstraction (TypedVarName var) expr -> withDictionary (filter ((var /=) . fst)) $ helper expr
Pure _ -> return []
e@(App (AnnRecord sel) _ x)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-23 09:09:36 +0000