Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add ValueType #2143

Merged
merged 2 commits into from
May 30, 2023
Merged

Add ValueType #2143

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4f69053
add ValueType
janmasrovira May 30, 2023
547ac42
fun -> function
janmasrovira May 30, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 18 additions & 3 deletions src/Juvix/Compiler/Core/Extra/Value.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,20 @@ toValue tab = \case
NCtr c -> goConstr c
NLam lam -> goLambda lam
Closure {..} -> toValue tab (substEnv _closureEnv _closureNode)
_ -> impossible
NPi {} -> goType
NUniv {} -> goType
NTyp {} -> goType
NPrim {} -> goType
NVar {} -> impossible
NIdt {} -> impossible
NApp {} -> impossible
NBlt {} -> impossible
NLet {} -> impossible
NRec {} -> impossible
NCase {} -> impossible
NMatch {} -> impossible
NDyn {} -> impossible
NBot {} -> impossible
where
goConstr :: Constr -> Value
goConstr Constr {..} =
Expand All @@ -29,6 +42,9 @@ toValue tab = \case
ii = lookupInductiveInfo tab (ci ^. constructorInductive)
paramsNum = length (ii ^. inductiveParams)

goType :: Value
goType = ValueType

goLambda :: Lambda -> Value
goLambda lam =
let (lams, body) = unfoldLambdas (NLam lam)
Expand All @@ -40,5 +56,4 @@ toValue tab = \case
case body of
NCtr c ->
toValue tab (NCtr (over constrArgs (dropEnd n) c))
_ ->
ValueFun
_ -> ValueFun
2 changes: 2 additions & 0 deletions src/Juvix/Compiler/Core/Language/Value.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ data Value
| ValueConstant ConstantValue
| ValueWildcard
| ValueFun
| ValueType

makeLenses ''ConstrApp

Expand All @@ -29,3 +30,4 @@ instance HasAtomicity Value where
ValueConstant {} -> Atom
ValueWildcard -> Atom
ValueFun -> Atom
ValueType -> Atom
3 changes: 2 additions & 1 deletion src/Juvix/Compiler/Core/Pretty/Base.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -597,7 +597,8 @@ instance PrettyCode Value where
ValueConstrApp x -> ppCode x
ValueConstant c -> ppCode c
ValueWildcard -> return "_"
ValueFun -> return "<fun>"
ValueFun -> return "<function>"
ValueType -> return "<type>"

ppValueSequence :: Member (Reader Options) r => [Value] -> Sem r (Doc Ann)
ppValueSequence vs = hsep <$> mapM (ppRightExpression appFixity) vs
Expand Down