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.

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

Fix name signature bug and extend test for instance fields #2928

Merged
merged 2 commits into from
Jul 30, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 2 additions & 1 deletion src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,8 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher
where
addField :: RecordStatement s -> Sem r ()
addField = \case
RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType
RecordStatementField RecordField {..} ->
addSymbol @s (fromIsImplicitField _fieldIsImplicit) Nothing _fieldName _fieldType
RecordStatementSyntax d -> goSyntax d

goSyntax :: RecordSyntaxDef s -> Sem r ()
Expand Down
30 changes: 23 additions & 7 deletions src/Juvix/Compiler/Concrete/Print/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -199,19 +199,35 @@ instance (SingI s) => PrettyPrint (NameItem s) where
let defaultVal = do
d <- _nameItemDefault
return (noLoc C.kwAssign <+> ppExpressionType (d ^. argDefaultValue))
ppSymbolType _nameItemSymbol <> ppCode Kw.kwExclamation <> noLoc (pretty _nameItemIndex)
isImplicitDelims _nameItemImplicit (ppSymbolType _nameItemSymbol)
<> ppCode Kw.kwExclamation
<> noLoc (pretty _nameItemIndex)
<+> ppCode Kw.kwColon
<+> ppExpressionType _nameItemType
<+?> defaultVal

isImplicitDelims :: (Member ExactPrint r) => IsImplicit -> Sem r () -> Sem r ()
isImplicitDelims = \case
Implicit -> braces
ImplicitInstance -> doubleBraces
Explicit -> parens

instance (SingI s) => PrettyPrint (NameBlock s) where
ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NameBlock s -> Sem r ()
ppCode NameBlock {..} = do
let delims = case _nameImplicit of
Implicit -> braces
ImplicitInstance -> doubleBraces
Explicit -> parens
delims (hsepSemicolon (map ppCode (toList _nameBlock)))
ppCode NameBlock {..} = isImplicitDelims _nameImplicit (vsepSemicolon (map ppCode (toList _nameBlock)))

instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (HashMap a b) where
ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => HashMap a b -> Sem r ()
ppCode m = do
let ppAssoc :: (a, b) -> Sem r ()
ppAssoc (k, v) =
ppCode k
<+> ppCode Kw.kwAssign
<+> ppCode v
braces (vsepSemicolon (map ppAssoc (HashMap.toList m)))

instance (SingI s) => PrettyPrint (RecordNameSignature s) where
ppCode RecordNameSignature {..} = ppCode _recordNames

instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (a, b) where
ppCode (a, b) = tuple [ppCode a, ppCode b]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1556,15 +1556,18 @@ checkSections sec = topBindings helper
c' <- reserveConstructorSymbol d c
let storeSig :: RecordNameSignature 'Parsed -> Sem r' ()
storeSig sig = modify' (set (scoperConstructorFields . at (c' ^. S.nameId)) (Just sig))
whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (storeSig . mkRecordNameSignature)
whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (registerParsedConstructorSig (c' ^. S.nameId) . mkRecordNameSignature)
mrecord :: Maybe (RhsRecord 'Parsed) = c ^? constructorRhs . _ConstructorRhsRecord
whenJust mrecord $ \r -> do
let sig = mkRecordNameSignature r
storeSig sig
registerParsedConstructorSig (c' ^. S.nameId) sig
return c'

registerRecordType :: S.Symbol -> S.Symbol -> Sem (Fail ': r') ()
registerRecordType mconstr ind = do
registerRecordType mconstr ind =
case d ^. inductiveConstructors of
mkRec :| cs
| not (null cs) -> fail
| notNull cs -> fail
| otherwise -> do
fs <-
failMaybe $
Expand Down Expand Up @@ -2606,13 +2609,13 @@ checkNamedApplicationNew napp = do
args' <- withLocalScope . localBindings . ignoreSyntax $ do
mapM_ reserveNamedArgumentName nargs
mapM (checkNamedArgumentNew puns) nargs
let enames =
HashSet.fromList
let signatureExplicitNames =
hashSet
. concatMap (HashMap.keys . (^. nameBlock))
. filter (not . isImplicitOrInstance . (^. nameImplicit))
$ sig ^. nameSignatureArgs
sargs :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs)
missingArgs = HashSet.difference enames sargs
givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs)
missingArgs = HashSet.difference signatureExplicitNames givenNames
unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive . isExhaustive)) $
throw (ErrMissingArgs (MissingArgs (aname ^. scopedIdenFinal . nameConcrete) missingArgs))
return
Expand Down
6 changes: 5 additions & 1 deletion src/Juvix/Prelude/Trace.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module Juvix.Prelude.Trace
where

import Data.Text qualified as Text
import Debug.Trace hiding (trace, traceM, traceShow)
import Debug.Trace hiding (trace, traceM, traceShow, traceWith)
import Debug.Trace qualified as T
import GHC.IO (unsafePerformIO)
import Juvix.Prelude.Base
Expand All @@ -21,6 +21,10 @@ traceLabel :: Text -> Text -> a -> a
traceLabel msg a = T.trace (unpack $ setDebugMsg msg <> a)
{-# WARNING traceLabel "Using traceLabel" #-}

traceWith :: (a -> Text) -> a -> a
traceWith f a = trace (f a) a
{-# WARNING traceWith "Using traceWith" #-}

trace :: Text -> a -> a
trace = traceLabel ""
{-# WARNING trace "Using trace" #-}
Expand Down
7 changes: 6 additions & 1 deletion test/Compilation/Positive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -455,5 +455,10 @@ tests =
"Test076: Builtin Maybe"
$(mkRelDir ".")
$(mkRelFile "test076.juvix")
$(mkRelFile "out/test076.out")
$(mkRelFile "out/test076.out"),
posTest
"Test077: Instance fields"
$(mkRelDir ".")
$(mkRelFile "test077.juvix")
$(mkRelFile "out/test077.out")
]
2 changes: 2 additions & 0 deletions tests/Compilation/positive/out/test077.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
nothing
just 1
67 changes: 67 additions & 0 deletions tests/Compilation/positive/test077.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
-- Instance Fields
module test077;

import Stdlib.Data.Nat.Base open;
import Stdlib.Data.Fixity open;
import Stdlib.System.IO open;
import Stdlib.Data.Maybe open;

trait
type Functor (f : Type -> Type) := mkFunctor {map : {A B : Type} -> (A -> B) -> f A -> f B};

trait
type Applicative (f : Type -> Type) :=
mkApplicative {
{{ApplicativeFunctor}} : Functor f;
pure : {A : Type} -> A -> f A;
ap : {A B : Type} -> f (A -> B) -> f A -> f B
};

trait
type Monad (f : Type -> Type) :=
mkMonad {
{{MonadApplicative}} : Applicative f;
bind : {A B : Type} -> f A -> (A -> f B) -> f B
};

open Functor;
open Applicative;
open Monad;

syntax operator >>= seq;
>>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g;

monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x;

instance
maybeFunctor : Functor Maybe :=
mkFunctor@{
map {A B} (f : A -> B) : Maybe A -> Maybe B
| nothing := nothing
| (just x) := just (f x)
};

instance
maybeApplicative : Applicative Maybe :=
mkApplicative@{
pure := just;
ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
| (just f) (just x) := just (f x)
| _ _ := nothing
};

instance
maybeMonad : Monad Maybe :=
mkMonad@{
bind {A B} : Maybe A -> (A -> Maybe B) -> Maybe B
| nothing _ := nothing
| (just a) f := f a
};

minusOne : Nat -> Maybe Nat
| zero := nothing
| (suc n) := just n;

minusThree (n : Nat) : Maybe Nat := pure n >>= minusOne >>= minusOne >>= minusOne;

main : IO := printLn (minusThree 1) >>> printLn (minusThree 4);
28 changes: 0 additions & 28 deletions tests/positive/Internal/InstanceFields.juvix

This file was deleted.

Loading