From aa6caf2c758e3be9410ad7ba28b3d467328eeedc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Tue, 6 Sep 2022 11:45:20 +0200 Subject: [PATCH] Dynamic type in Core (#1508) --- src/Juvix/Compiler/Core/Evaluator.hs | 1 + src/Juvix/Compiler/Core/Extra/Base.hs | 8 ++++++++ src/Juvix/Compiler/Core/Language.hs | 13 +++++++++++++ src/Juvix/Compiler/Core/Pretty/Base.hs | 4 ++++ src/Juvix/Compiler/Core/Translation/FromSource.hs | 9 +++------ 5 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 6e20fb994..cc711010c 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -72,6 +72,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0 NPi {} -> substEnv env n NUniv {} -> n NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args) + NDyn {} -> n Closure {} -> n branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index 674288f3e..31b721425 100644 --- a/src/Juvix/Compiler/Core/Extra/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Base.hs @@ -90,6 +90,12 @@ mkTypeConstr i sym args = NTyp (TypeConstr i sym args) mkTypeConstr' :: Symbol -> [Type] -> Type mkTypeConstr' = mkTypeConstr Info.empty +mkDynamic :: Info -> Type +mkDynamic i = NDyn (Dynamic i) + +mkDynamic' :: Type +mkDynamic' = mkDynamic Info.empty + {------------------------------------------------------------------------} {- functions on Type -} @@ -214,6 +220,8 @@ destruct = \case NodeDetails i [] [] [] (\i' _ -> mkUniv i' l) NTyp (TypeConstr i sym args) -> NodeDetails i args (map (const 0) args) (map (const []) args) (`mkTypeConstr` sym) + NDyn (Dynamic i) -> + NodeDetails i [] [] [] (\i' _ -> mkDynamic i') Closure env (Lambda i b) -> NodeDetails i diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs index 01486323d..28c4ce18e 100644 --- a/src/Juvix/Compiler/Core/Language.hs +++ b/src/Juvix/Compiler/Core/Language.hs @@ -82,6 +82,11 @@ data TypeConstr = TypeConstr _typeConstrArgs :: ![Type] } +-- | Dynamic type. A Node with a dynamic type has an unknown type. Useful +-- for transformations that introduce partial type information, e.g., one can +-- have types `* -> *` and `* -> * -> Nat` where `*` is the dynamic type. +newtype Dynamic = Dynamic {_dynamicInfo :: Info} + -- | `Node` is the type of nodes in the program tree. The nodes themselves -- contain only runtime-relevant information. Runtime-irrelevant annotations -- (including all type information) are stored in the infos associated with each @@ -99,6 +104,7 @@ data Node | NPi {-# UNPACK #-} !Pi | NUniv {-# UNPACK #-} !Univ | NTyp {-# UNPACK #-} !TypeConstr + | NDyn !Dynamic -- Dynamic is already a newtype, so it's unpacked. | -- Evaluation only: `Closure env body` Closure { _closureEnv :: !Env, @@ -180,6 +186,9 @@ instance HasAtomicity Univ where instance HasAtomicity TypeConstr where atomicity _ = Aggregate lambdaFixity +instance HasAtomicity Dynamic where + atomicity _ = Atom + instance HasAtomicity Node where atomicity = \case NVar x -> atomicity x @@ -194,6 +203,7 @@ instance HasAtomicity Node where NPi x -> atomicity x NUniv x -> atomicity x NTyp x -> atomicity x + NDyn x -> atomicity x Closure {} -> Aggregate lambdaFixity lambdaFixity :: Fixity @@ -235,6 +245,9 @@ instance Eq Univ where instance Eq TypeConstr where (TypeConstr _ sym1 args1) == (TypeConstr _ sym2 args2) = sym1 == sym2 && args1 == args2 +instance Eq Dynamic where + Dynamic _ == Dynamic _ = True + makeLenses ''Var makeLenses ''Ident makeLenses ''Constant diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 3289b741f..4230998dd 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -155,6 +155,7 @@ instance PrettyCode Node where Just ni -> ppCode (ni ^. NameInfo.infoName) Nothing -> return $ kwUnnamedIdent <> pretty _typeConstrSymbol return $ foldl' (<+>) n' args' + NDyn {} -> return kwDynamic Closure env l@Lambda {} -> ppCode (substEnv env (NLam l)) @@ -253,3 +254,6 @@ kwTrace = keyword Str.trace_ kwFail :: Doc Ann kwFail = keyword Str.fail_ + +kwDynamic :: Doc Ann +kwDynamic = keyword Str.mul diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index 183121bd4..1c70e145b 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -43,9 +43,6 @@ runParser root fileName tab input = { _parserParamsRoot = root } -starType :: Type -starType = mkPi Info.empty (mkUniv Info.empty 0) (mkVar Info.empty 0) - binderNameInfo :: Name -> Info binderNameInfo name = Info.singleton (BinderInfo (Info.singleton (NameInfo name))) @@ -79,7 +76,7 @@ declareBuiltinConstr btag nameTxt i = do ( ConstructorInfo { _constructorName = name, _constructorTag = BuiltinTag btag, - _constructorType = starType, + _constructorType = mkDynamic', _constructorArgsNum = builtinConstrArgsNum btag } ) @@ -143,7 +140,7 @@ statementDef = do IdentifierInfo { _identifierName = name, _identifierSymbol = sym, - _identifierType = starType, + _identifierType = mkDynamic', _identifierArgsNum = 0, _identifierArgsInfo = [], _identifierIsExported = False @@ -190,7 +187,7 @@ statementConstr = do ConstructorInfo { _constructorName = name, _constructorTag = tag, - _constructorType = starType, + _constructorType = mkDynamic', _constructorArgsNum = argsNum } lift $ registerConstructor info