From a491382dfe2ad290bb7fc2b75665efe85475b6ec Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 30 Jul 2024 14:47:04 +0200 Subject: [PATCH 1/2] fix bug and extend test --- .../Concrete/Data/NameSignature/Builder.hs | 3 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 30 +++++++-- .../FromParsed/Analysis/Scoping.hs | 19 +++--- src/Juvix/Prelude/Trace.hs | 6 +- test/Compilation/Positive.hs | 7 +- tests/Compilation/positive/out/test077.out | 2 + tests/Compilation/positive/test077.juvix | 67 +++++++++++++++++++ tests/positive/Internal/InstanceFields.juvix | 28 -------- 8 files changed, 116 insertions(+), 46 deletions(-) create mode 100644 tests/Compilation/positive/out/test077.out create mode 100644 tests/Compilation/positive/test077.juvix delete mode 100644 tests/positive/Internal/InstanceFields.juvix diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 1bd9bcd77e..5db1059ddd 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -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 () diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index f290170bc8..9a111c35b8 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -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] diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index ab94a02fe2..f86f203880 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -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 $ @@ -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 diff --git a/src/Juvix/Prelude/Trace.hs b/src/Juvix/Prelude/Trace.hs index 0f4751d925..c926ba1aa0 100644 --- a/src/Juvix/Prelude/Trace.hs +++ b/src/Juvix/Prelude/Trace.hs @@ -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 @@ -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" #-} diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index f9b11d71e6..9483972e56 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -455,5 +455,10 @@ tests = "Test076: Builtin Maybe" $(mkRelDir ".") $(mkRelFile "test076.juvix") - $(mkRelFile "out/test076.out") + $(mkRelFile "out/test076.out"), + posTestEval + "Test077: Instance fields" + $(mkRelDir ".") + $(mkRelFile "test077.juvix") + $(mkRelFile "out/test077.out") ] diff --git a/tests/Compilation/positive/out/test077.out b/tests/Compilation/positive/out/test077.out new file mode 100644 index 0000000000..66c0e977e4 --- /dev/null +++ b/tests/Compilation/positive/out/test077.out @@ -0,0 +1,2 @@ +nothing +just 1 diff --git a/tests/Compilation/positive/test077.juvix b/tests/Compilation/positive/test077.juvix new file mode 100644 index 0000000000..f365ef5c71 --- /dev/null +++ b/tests/Compilation/positive/test077.juvix @@ -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); diff --git a/tests/positive/Internal/InstanceFields.juvix b/tests/positive/Internal/InstanceFields.juvix deleted file mode 100644 index 7e0fd6218a..0000000000 --- a/tests/positive/Internal/InstanceFields.juvix +++ /dev/null @@ -1,28 +0,0 @@ -module InstanceFields; - -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; - -monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x; From 62a3729e0de16f3656bdae0c7d6778d0776278db Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 30 Jul 2024 16:41:48 +0200 Subject: [PATCH 2/2] make the test posTest instead of posTestEval --- test/Compilation/Positive.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 9483972e56..941bbbab93 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -456,7 +456,7 @@ tests = $(mkRelDir ".") $(mkRelFile "test076.juvix") $(mkRelFile "out/test076.out"), - posTestEval + posTest "Test077: Instance fields" $(mkRelDir ".") $(mkRelFile "test077.juvix")