From 9f0f0fa271bfa50492f2077424a90ba600e9f5a1 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Tue, 26 Nov 2024 17:33:20 +0100 Subject: [PATCH 1/7] Squashed commit of the following: commit 432114c2de274bfb7c20e5d406e50e69ed095559 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Tue Nov 26 16:19:56 2024 +0100 test086 -> test087 commit 8b3f47b3d5248dd47c0e93a42b97fbba4cde4d04 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 17:50:05 2024 +0100 move commit 7f97da93c4cedc36614de05cce333613502765b7 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 15:35:19 2024 +0100 change order of definition commit 094c6e934aaa704ee0a76e2679ae780fcf5cddca Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 13:39:14 2024 +0100 add test commit 42a3476e526174c822997472d457e5a6157900ae Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 13:13:09 2024 +0100 refactor commit b5fe58ff38ff78cb092466a52ebafe724d05afe4 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 11:05:24 2024 +0100 change order of Bool constructors commit 03210ab8005fbd54900c31e31b189d905d47e3ec Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Fri Nov 22 10:12:17 2024 +0100 update stdlib commit 59456dfef40db738f65659d4c32f58120bac9aad Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu Nov 21 19:52:23 2024 +0100 update stdlib commit 0f2fae6196720f65b70343e217e4e302404b7cc6 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu Nov 21 19:42:00 2024 +0100 decrease clause number commit 25325bc1791fe0360f769e64af2a081089fbd7e3 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu Nov 21 19:28:53 2024 +0100 improve commit 6fe818e2ae9a32e01c48a74a539389ebb7e50f61 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu Nov 21 18:53:31 2024 +0100 fixes commit 5858b9bd7191c91d7b996603311f93cc3861e890 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu Nov 21 16:59:39 2024 +0100 derive ord commit 6c4db73a189ee44bf6cc001172dc611ed8645120 Author: Jan Mas Rovira <janmasrovira@gmail.com> Date: Wed Nov 20 18:05:12 2024 +0100 wip --- .../package-base/Juvix/Builtin/V1/Bool.juvix | 4 +- src/Juvix/Compiler/Builtins.hs | 4 + src/Juvix/Compiler/Builtins/Ord.hs | 25 ++ src/Juvix/Compiler/Builtins/Ordering.hs | 7 + src/Juvix/Compiler/Concrete/Data/Builtins.hs | 24 +- .../Compiler/Core/Data/InfoTableBuilder.hs | 4 +- src/Juvix/Compiler/Core/Pretty/Base.hs | 2 + .../Compiler/Core/Translation/FromInternal.hs | 37 +-- .../Core/Translation/Stripped/FromCore.hs | 7 + src/Juvix/Compiler/Internal/Extra/Base.hs | 33 ++- .../Internal/Extra/DependencyBuilder.hs | 2 + src/Juvix/Compiler/Internal/Language.hs | 5 +- .../Internal/Translation/FromConcrete.hs | 264 ++++++++++++++---- src/Juvix/Extra/Strings.hs | 18 ++ src/Juvix/Prelude/Effects/Input.hs | 10 + test/Compilation/Positive.hs | 7 +- tests/Compilation/positive/out/test087.out | 5 + tests/Compilation/positive/test087.juvix | 26 ++ tests/negative/Internal/LazyBuiltin.juvix | 4 +- 19 files changed, 412 insertions(+), 76 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/Ord.hs create mode 100644 src/Juvix/Compiler/Builtins/Ordering.hs create mode 100644 tests/Compilation/positive/out/test087.out create mode 100644 tests/Compilation/positive/test087.juvix diff --git a/include/package-base/Juvix/Builtin/V1/Bool.juvix b/include/package-base/Juvix/Builtin/V1/Bool.juvix index 72e7d0616b..2795fd475f 100644 --- a/include/package-base/Juvix/Builtin/V1/Bool.juvix +++ b/include/package-base/Juvix/Builtin/V1/Bool.juvix @@ -3,5 +3,5 @@ module Juvix.Builtin.V1.Bool; --- Inductive definition of booleans. builtin bool type Bool := - | true - | false; + | false + | true; diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index dda105ea62..4e18415a4a 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -2,6 +2,8 @@ module Juvix.Compiler.Builtins ( module Juvix.Compiler.Builtins.Nat, module Juvix.Compiler.Builtins.IO, module Juvix.Compiler.Builtins.Eq, + module Juvix.Compiler.Builtins.Ord, + module Juvix.Compiler.Builtins.Ordering, module Juvix.Compiler.Builtins.Int, module Juvix.Compiler.Builtins.Bool, module Juvix.Compiler.Builtins.List, @@ -33,4 +35,6 @@ import Juvix.Compiler.Builtins.List import Juvix.Compiler.Builtins.Maybe import Juvix.Compiler.Builtins.Monad import Juvix.Compiler.Builtins.Nat +import Juvix.Compiler.Builtins.Ord +import Juvix.Compiler.Builtins.Ordering import Juvix.Compiler.Builtins.String diff --git a/src/Juvix/Compiler/Builtins/Ord.hs b/src/Juvix/Compiler/Builtins/Ord.hs new file mode 100644 index 0000000000..5146870ef8 --- /dev/null +++ b/src/Juvix/Compiler/Builtins/Ord.hs @@ -0,0 +1,25 @@ +module Juvix.Compiler.Builtins.Ord where + +import Juvix.Compiler.Internal.Builtins +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude +import Juvix.Prelude.Pretty + +checkOrdDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () +checkOrdDef d = do + let err :: forall a. Text -> Sem r a + err = builtinsErrorText (getLoc d) + let eqTxt = prettyText BuiltinOrd + unless (isSmallUniverse' (d ^. inductiveType)) (err (eqTxt <> " should be in the small universe")) + case d ^. inductiveParameters of + [_] -> return () + _ -> err (eqTxt <> " should have exactly one type parameter") + case d ^. inductiveConstructors of + [c1] -> checkMkOrd c1 + _ -> err (eqTxt <> " should have exactly two constructors") + +checkMkOrd :: ConstructorDef -> Sem r () +checkMkOrd _ = return () + +checkOrdCompare :: FunctionDef -> Sem r () +checkOrdCompare _ = return () diff --git a/src/Juvix/Compiler/Builtins/Ordering.hs b/src/Juvix/Compiler/Builtins/Ordering.hs new file mode 100644 index 0000000000..c3b1986cdb --- /dev/null +++ b/src/Juvix/Compiler/Builtins/Ordering.hs @@ -0,0 +1,7 @@ +module Juvix.Compiler.Builtins.Ordering where + +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude + +checkOrderingDef :: forall r. InductiveDef -> Sem r () +checkOrderingDef _d = return () diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 64ab634fd3..27ef4f43d3 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -50,7 +50,7 @@ instance Pretty BuiltinPrim where builtinConstructors :: BuiltinInductive -> [BuiltinConstructor] builtinConstructors = \case BuiltinNat -> [BuiltinNatZero, BuiltinNatSuc] - BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse] + BuiltinBool -> [BuiltinBoolFalse, BuiltinBoolTrue] BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc] BuiltinList -> [BuiltinListNil, BuiltinListCons] BuiltinMaybe -> [BuiltinMaybeNothing, BuiltinMaybeJust] @@ -60,6 +60,8 @@ builtinConstructors = \case BuiltinAnomaResource -> [BuiltinMkAnomaResource] BuiltinAnomaAction -> [BuiltinMkAnomaAction] BuiltinEq -> [BuiltinMkEq] + BuiltinOrd -> [BuiltinMkOrd] + BuiltinOrdering -> [BuiltinOrderingLT, BuiltinOrderingEQ, BuiltinOrderingGT] data BuiltinInductive = BuiltinNat @@ -69,6 +71,8 @@ data BuiltinInductive | BuiltinMaybe | BuiltinPair | BuiltinEq + | BuiltinOrd + | BuiltinOrdering | BuiltinPoseidonState | BuiltinEcPoint | BuiltinAnomaResource @@ -90,6 +94,8 @@ instance Pretty BuiltinInductive where BuiltinMaybe -> Str.maybe_ BuiltinPair -> Str.pair BuiltinEq -> Str.eq + BuiltinOrd -> Str.ord + BuiltinOrdering -> Str.ordering BuiltinPoseidonState -> Str.cairoPoseidonState BuiltinEcPoint -> Str.cairoEcPoint BuiltinAnomaResource -> Str.anomaResource @@ -113,17 +119,25 @@ instance Pretty BuiltinConstructor where BuiltinMkAnomaResource -> Str.anomaMkResource BuiltinMkAnomaAction -> Str.anomaMkAction BuiltinMkEq -> Str.mkEq + BuiltinMkOrd -> Str.mkOrd + BuiltinOrderingLT -> Str.lt + BuiltinOrderingEQ -> Str.eq + BuiltinOrderingGT -> Str.gt data BuiltinConstructor = BuiltinNatZero | BuiltinNatSuc | BuiltinBoolTrue | BuiltinBoolFalse + | BuiltinOrderingLT + | BuiltinOrderingEQ + | BuiltinOrderingGT | BuiltinIntOfNat | BuiltinIntNegSuc | BuiltinListNil | BuiltinListCons | BuiltinMkEq + | BuiltinMkOrd | BuiltinMaybeNothing | BuiltinMaybeJust | BuiltinPairConstr @@ -167,6 +181,7 @@ data BuiltinFunction | BuiltinIntLt | BuiltinFromNat | BuiltinIsEqual + | BuiltinOrdCompare | BuiltinFromInt | BuiltinSeq | BuiltinMonadBind @@ -209,6 +224,7 @@ instance Pretty BuiltinFunction where BuiltinFromInt -> Str.fromInt BuiltinSeq -> Str.builtinSeq BuiltinIsEqual -> Str.isEqual + BuiltinOrdCompare -> Str.compare BuiltinMonadBind -> Str.builtinMonadBind data BuiltinAxiom @@ -441,6 +457,7 @@ isNatBuiltin = \case BuiltinNatLt -> True BuiltinNatEq -> True -- + BuiltinOrdCompare -> False BuiltinIsEqual -> False BuiltinAssert -> False BuiltinBoolIf -> False @@ -495,6 +512,7 @@ isIntBuiltin = \case BuiltinFromInt -> False BuiltinSeq -> False BuiltinIsEqual -> False + BuiltinOrdCompare -> False BuiltinMonadBind -> False isCastBuiltin :: BuiltinFunction -> Bool @@ -502,6 +520,7 @@ isCastBuiltin = \case BuiltinFromNat -> True BuiltinFromInt -> True -- + BuiltinOrdCompare -> False BuiltinIsEqual -> False BuiltinAssert -> False BuiltinIntEq -> False @@ -543,6 +562,7 @@ isIgnoredBuiltin f .&&. (not . isCastBuiltin) .&&. (/= BuiltinMonadBind) .&&. (/= BuiltinIsEqual) + .&&. (/= BuiltinOrdCompare) $ f explicit :: Bool @@ -575,6 +595,8 @@ isIgnoredBuiltin f BuiltinNatEq -> False -- Eq BuiltinIsEqual -> False + -- Ord + BuiltinOrdCompare -> False -- Monad BuiltinMonadBind -> False -- Ignored diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index aabf4a5b98..b630bae9ed 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -269,8 +269,8 @@ declareBoolBuiltins = declareInductiveBuiltins "Bool" (Just (BuiltinTypeInductive BuiltinBool)) - [ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue), - (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse) + [ (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse), + (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue) ] declareNatBuiltins :: (Member InfoTableBuilder r) => Sem r () diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 0bc1b6f237..57af9cb552 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -654,6 +654,8 @@ instance PrettyCode InfoTable where BuiltinAnomaAction -> True BuiltinList -> False BuiltinEq -> False + BuiltinOrd -> False + BuiltinOrdering -> False BuiltinMaybe -> False BuiltinNat -> False BuiltinInt -> False diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index b85a36eb5b..c2aa512222 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -215,23 +215,28 @@ goConstructor sym ctor = do ctorTag :: Maybe Internal.BuiltinConstructor -> Sem r Tag ctorTag = \case - Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue) - Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse) - Just Internal.BuiltinMkEq -> freshTag - Just Internal.BuiltinNatZero -> freshTag - Just Internal.BuiltinNatSuc -> freshTag - Just Internal.BuiltinIntOfNat -> freshTag - Just Internal.BuiltinIntNegSuc -> freshTag - Just Internal.BuiltinListNil -> freshTag - Just Internal.BuiltinListCons -> freshTag - Just Internal.BuiltinMaybeNothing -> freshTag - Just Internal.BuiltinMaybeJust -> freshTag - Just Internal.BuiltinPairConstr -> freshTag - Just Internal.BuiltinMkPoseidonState -> freshTag - Just Internal.BuiltinMkEcPoint -> freshTag - Just Internal.BuiltinMkAnomaAction -> freshTag - Just Internal.BuiltinMkAnomaResource -> freshTag Nothing -> freshTag + Just b -> case b of + Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue) + Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse) + Internal.BuiltinMkEq -> freshTag + Internal.BuiltinNatZero -> freshTag + Internal.BuiltinNatSuc -> freshTag + Internal.BuiltinIntOfNat -> freshTag + Internal.BuiltinIntNegSuc -> freshTag + Internal.BuiltinListNil -> freshTag + Internal.BuiltinListCons -> freshTag + Internal.BuiltinMaybeNothing -> freshTag + Internal.BuiltinMaybeJust -> freshTag + Internal.BuiltinPairConstr -> freshTag + Internal.BuiltinMkPoseidonState -> freshTag + Internal.BuiltinMkEcPoint -> freshTag + Internal.BuiltinMkAnomaAction -> freshTag + Internal.BuiltinMkAnomaResource -> freshTag + Internal.BuiltinMkOrd -> freshTag + Internal.BuiltinOrderingLT -> freshTag + Internal.BuiltinOrderingGT -> freshTag + Internal.BuiltinOrderingEQ -> freshTag ctorType :: Sem r Type ctorType = diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index c90354ad68..32c56501e0 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -55,6 +55,7 @@ fromCore fsize tab = BuiltinIntLt -> False BuiltinSeq -> False BuiltinIsEqual -> False + BuiltinOrdCompare -> False BuiltinMonadBind -> True -- TODO revise BuiltinFromNat -> True BuiltinFromInt -> True @@ -64,6 +65,10 @@ fromCore fsize tab = BuiltinListNil -> True BuiltinListCons -> True BuiltinMkEq -> True + BuiltinMkOrd -> True + BuiltinOrderingLT -> True + BuiltinOrderingGT -> True + BuiltinOrderingEQ -> True BuiltinMkPoseidonState -> True BuiltinMkEcPoint -> True BuiltinMaybeNothing -> True @@ -146,6 +151,8 @@ fromCore fsize tab = BuiltinEq -> True BuiltinMaybe -> True BuiltinPair -> True + BuiltinOrd -> True + BuiltinOrdering -> True BuiltinPoseidonState -> True BuiltinEcPoint -> True BuiltinNat -> False diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 8573a0916c..f85fb14257 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -383,6 +383,14 @@ unfoldLambdaClauses t = do mkClause LambdaClause {..} = first (appendList _lambdaPatterns) (unfoldLambda _lambdaBody) return (mkClause <$> _lambdaClauses) +mkLambda :: NonEmpty LambdaClause -> Expression +mkLambda c = + ExpressionLambda + Lambda + { _lambdaType = Nothing, + _lambdaClauses = c + } + -- Unfolds *single* clause lambdas unfoldLambda :: Expression -> ([PatternArg], Expression) unfoldLambda t = case t of @@ -525,6 +533,9 @@ instance IsExpression Iden where instance IsExpression Expression where toExpression = id +instance IsExpression Case where + toExpression = ExpressionCase + instance IsExpression Hole where toExpression = ExpressionHole @@ -655,10 +666,30 @@ freshVar _nameLoc n = do _nameLoc } +mkCaseBranch :: PatternArg -> Expression -> CaseBranch +mkCaseBranch pat body = + CaseBranch + { _caseBranchPattern = pat, + _caseBranchRhs = CaseBranchRhsExpression body + } + +mkCase :: Expression -> NonEmpty CaseBranch -> Expression +mkCase cexpr clauses = + toExpression + Case + { _caseExpression = cexpr, + _caseBranches = clauses, + _caseExpressionType = Nothing, + _caseExpressionWholeType = Nothing + } + +mkVarPattern :: VarName -> IsImplicit -> PatternArg +mkVarPattern var impl = PatternArg impl Nothing (PatternVariable var) + genWildcard :: forall r'. (Members '[NameIdGen] r') => Interval -> IsImplicit -> Sem r' PatternArg genWildcard loc impl = do var <- varFromWildcard (Wildcard loc) - return (PatternArg impl Nothing (PatternVariable var)) + return (mkVarPattern var impl) freshInstanceHole :: (Members '[NameIdGen] r) => Interval -> Sem r InstanceHole freshInstanceHole l = mkInstanceHole l <$> freshNameId diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs index cdd895b7c1..c87f3030be 100644 --- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs @@ -200,6 +200,8 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go BuiltinAnomaResource -> return () BuiltinAnomaAction -> return () BuiltinEq -> return () + BuiltinOrd -> return () + BuiltinOrdering -> return () addInductiveStartNode :: Sem r () addInductiveStartNode = addStartNode (i ^. inductiveName) diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 15be717869..f3e43e2a4f 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -33,7 +33,9 @@ newtype PreLetStatement = PreLetFunctionDef FunctionDef -- | Traits that support builtin deriving -data DerivingTrait = DerivingEq +data DerivingTrait + = DerivingEq + | DerivingOrd deriving stock (Generic, Data, Bounded, Enum, Show) derivingTraitFromBuiltinMap :: HashMap BuiltinPrim DerivingTrait @@ -46,6 +48,7 @@ instance IsBuiltin DerivingTrait where toBuiltinPrim :: DerivingTrait -> BuiltinPrim toBuiltinPrim = \case DerivingEq -> toBuiltinPrim BuiltinEq + DerivingOrd -> toBuiltinPrim BuiltinOrd instance Pretty DerivingTrait where pretty = pretty . toBuiltinPrim diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index edef4b6bdf..42ddd050d8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -64,6 +64,24 @@ newtype DefaultArgsStack = DefaultArgsStack makeLenses ''DefaultArgsStack +data EqBuiltins = EqBuiltins + { _eqBuiltinIsEqual :: Internal.Name, + _eqBuiltinTrue :: Internal.Name, + _eqBuiltinFalse :: Internal.Name, + _eqBuiltinAnd :: Internal.Name + } + +makeLenses ''EqBuiltins + +data OrdBuiltins = OrdBuiltins + { _ordBuiltinCompare :: Internal.Name, + _ordBuiltinLt :: Internal.Name, + _ordBuiltinEq :: Internal.Name, + _ordBuiltinGt :: Internal.Name + } + +makeLenses ''OrdBuiltins + data DerivingArgs = DerivingArgs { _derivingPragmas :: Maybe ParsedPragmas, _derivingInstanceName :: Internal.FunctionName, @@ -295,7 +313,7 @@ goModuleBody stmts = evalState emptyLocalTable $ do funs :: [Indexed Internal.PreStatement] <- concat <$> sequence - [ return . map (Indexed i . Internal.PreFunctionDef) =<< defs + [ map (Indexed i . Internal.PreFunctionDef) <$> defs | Indexed i s <- ss, let defs = mkFunctionLike s ] @@ -312,8 +330,8 @@ goModuleBody stmts = evalState emptyLocalTable $ do mkFunctionLike :: Statement 'Scoped -> Sem (State LocalTable ': r) [Internal.FunctionDef] mkFunctionLike s = case s of StatementFunctionDef d -> goFunctionDef d - StatementProjectionDef d -> goProjectionDef d >>= return . pure - StatementDeriving d -> goDeriving d >>= return . pure + StatementProjectionDef d -> pure <$> goProjectionDef d + StatementDeriving d -> pure <$> goDeriving d StatementSyntax {} -> return [] StatementImport {} -> return [] StatementInductive {} -> return [] @@ -447,6 +465,7 @@ deriveTrait :: Sem r Internal.FunctionDef deriveTrait = \case Internal.DerivingEq -> deriveEq + Internal.DerivingOrd -> deriveOrd findDerivingTrait :: forall r. @@ -510,6 +529,14 @@ getDefinedConstructor ind = do tbl2 <- asks (^. infoConstructors . at ind) return (fromJust (tbl1 <|> tbl2)) +getDefinedInductiveConstructors :: + (Members '[Reader Internal.InfoTable, State LocalTable] r) => + Internal.InductiveName -> + Sem r [ConstructorInfo] +getDefinedInductiveConstructors d = do + i <- getDefinedInductive d + mapM getDefinedConstructor (i ^. Internal.inductiveInfoConstructors) + getDefinedInductive :: (Members '[Reader Internal.InfoTable, State LocalTable] r) => Internal.InductiveName -> @@ -536,6 +563,148 @@ throwDerivingWrongForm ret = do _derivingTypeSupportedBuiltins } +deriveOrd :: + forall r. + ( Members + '[ Reader S.InfoTable, + Reader Internal.InfoTable, + State LocalTable, + NameIdGen, + Error ScoperError, + Reader DefaultArgsStack, + Reader Pragmas + ] + r + ) => + DerivingArgs -> + Sem r Internal.FunctionDef +deriveOrd DerivingArgs {..} = do + arg <- derivingGetConstrs ret args + argsInfo <- goArgsInfo _derivingInstanceName + let loc = getLoc ordName + mkOrd <- getBuiltin loc BuiltinMkOrd + bcmp <- getBuiltin loc BuiltinOrdCompare + blt <- getBuiltin loc BuiltinOrderingLT + bgt <- getBuiltin loc BuiltinOrderingGT + beq <- getBuiltin loc BuiltinOrderingEQ + let bs = + OrdBuiltins + { _ordBuiltinCompare = bcmp, + _ordBuiltinLt = blt, + _ordBuiltinGt = bgt, + _ordBuiltinEq = beq + } + lam <- genOrdCompare (getLoc _derivingInstanceName) bs arg + let ty = Internal.foldFunType _derivingParameters ret + body = mkOrd Internal.@@ lam + pragmas' <- goPragmas _derivingPragmas + return + Internal.FunctionDef + { _funDefTerminating = False, + _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, + _funDefPragmas = pragmas', + _funDefArgsInfo = argsInfo, + _funDefDocComment = Nothing, + _funDefName = _derivingInstanceName, + _funDefType = ty, + _funDefBody = body, + _funDefBuiltin = Nothing + } + where + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression ordName) args + + ordName :: Internal.InductiveName + args :: [Internal.ApplicationArg] + (ordName, args) = _derivingReturnType + +genOrdCompare :: + forall r. + (Members '[NameIdGen] r) => + Interval -> + OrdBuiltins -> + [ConstructorInfo] -> + Sem r Internal.Expression +genOrdCompare loc bs cs = do + res <- + fmap nonEmpty + . execOutputList + . runInputList cs + $ repeatOnInput go + Internal.mkLambda <$> case res of + Nothing -> pure <$> emptyTypeClause + Just l -> return l + where + emptyTypeClause :: Sem r Internal.LambdaClause + emptyTypeClause = do + w1 <- Internal.genWildcard loc Explicit + w2 <- Internal.genWildcard loc Explicit + return + Internal.LambdaClause + { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq), + _lambdaPatterns = w1 :| [w2] + } + + go :: (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r') => ConstructorInfo -> Sem r' () + go c = do + isLast <- isEndOfInput @ConstructorInfo + let mkPat = Internal.genConstructorPattern loc Explicit c + (p1, v1) <- mkPat + (p2, v2) <- mkPat + lord <- lexOrder (zipExact v1 v2) + let sameConstr = + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = lord + } + output sameConstr + unless isLast $ do + p3 <- fst <$> mkPat + w3 <- Internal.genWildcard loc Explicit + output + Internal.LambdaClause + { _lambdaPatterns = p3 :| [w3], + _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt) + } + p4 <- fst <$> mkPat + w4 <- Internal.genWildcard loc Explicit + output + Internal.LambdaClause + { _lambdaPatterns = w4 :| [p4], + _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt) + } + + lexOrder :: forall r'. (Members '[NameIdGen] r') => [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression + lexOrder = lexgo + where + cmp :: Internal.VarName -> Internal.VarName -> Internal.Expression + cmp a b = (bs ^. ordBuiltinCompare) Internal.@@ a Internal.@@ b + + lexgo :: [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression + lexgo = \case + [] -> return (Internal.toExpression (bs ^. ordBuiltinEq)) + (x, x') : vs + | null vs -> return (cmp x x') + | otherwise -> do + v <- Internal.freshVar loc "ltGt" + let pv = Internal.mkVarPattern v Explicit + mkPat :: Internal.Name -> Internal.PatternArg + mkPat p = Internal.mkConstructorVarPattern Explicit p [] + branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v) + branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs + let branches = branchEq :| [branchNEq] + return (Internal.mkCase (cmp x x') branches) + +derivingGetConstrs :: + (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) => + Internal.Expression -> + [Internal.ApplicationArg] -> + Sem r [Internal.ConstructorInfo] +derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do + [Internal.ApplicationArg Explicit a] <- return args + Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) + getDefinedInductiveConstructors ind + deriveEq :: forall r. ( Members @@ -557,7 +726,7 @@ deriveEq DerivingArgs {..} = do argsInfo <- goArgsInfo _derivingInstanceName lamName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText) let lam = Internal.ExpressionIden (Internal.IdenFunction lamName) - lamFun <- eqLambda lam indInfo argty + lamFun <- eqLambda lam argty lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName) let lamDef = Internal.FunctionDef @@ -615,59 +784,57 @@ deriveEq DerivingArgs {..} = do toAppArg :: Internal.InductiveParameter -> Internal.ApplicationArg toAppArg p = Internal.ApplicationArg Explicit (Internal.toExpression (p ^. Internal.inductiveParamName)) - eqLambda :: Internal.Expression -> Internal.InductiveInfo -> Internal.Expression -> Sem r Internal.Expression - eqLambda lam d argty = do + eqLambda :: Internal.Expression -> Internal.Expression -> Sem r Internal.Expression + eqLambda recDef argty = do let loc = getLoc eqName band <- getBuiltin loc BuiltinBoolAnd btrue <- getBuiltin loc BuiltinBoolTrue bfalse <- getBuiltin loc BuiltinBoolFalse bisEqual <- getBuiltin loc BuiltinIsEqual - case nonEmpty (d ^. Internal.inductiveInfoConstructors) of + constrs <- derivingGetConstrs ret args + let bs = + EqBuiltins + { _eqBuiltinTrue = btrue, + _eqBuiltinFalse = bfalse, + _eqBuiltinIsEqual = bisEqual, + _eqBuiltinAnd = band + } + case nonEmpty constrs of Nothing -> return (Internal.toExpression btrue) Just cs -> do - cl' <- mapM (lambdaClause band btrue bisEqual) cs + cl' <- mapM (lambdaClause bs) cs defaultCl' <- if - | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bfalse + | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bs | otherwise -> return Nothing - return - ( Internal.ExpressionLambda - Internal.Lambda - { _lambdaType = Nothing, - _lambdaClauses = snocNonEmptyMaybe cl' defaultCl' - } - ) + return $ + Internal.ExpressionLambda + Internal.Lambda + { _lambdaType = Nothing, + _lambdaClauses = snocNonEmptyMaybe cl' defaultCl' + } where - defaultLambdaClause :: Internal.Name -> Sem r Internal.LambdaClause - defaultLambdaClause btrue = do + defaultLambdaClause :: EqBuiltins -> Sem r Internal.LambdaClause + defaultLambdaClause bs = do let loc = getLoc eqName p1 <- Internal.genWildcard loc Internal.Explicit p2 <- Internal.genWildcard loc Internal.Explicit return Internal.LambdaClause { _lambdaPatterns = p1 :| [p2], - _lambdaBody = Internal.toExpression btrue + _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse) } lambdaClause :: - Internal.FunctionName -> - Internal.FunctionName -> - Internal.FunctionName -> - Internal.ConstructorName -> + EqBuiltins -> + Internal.ConstructorInfo -> Sem r Internal.LambdaClause - lambdaClause band btrue bisEqual c = do + lambdaClause bs cinfo = do argsRecursive :: [Bool] <- getRecursiveArgs - numArgs :: [IsImplicit] <- getNumArgs let loc = getLoc _derivingInstanceName - mkpat :: Sem r ([Internal.VarName], Internal.PatternArg) - mkpat = runOutputList . runStreamOf allWords $ do - xs :: [(IsImplicit, Internal.VarName)] <- forM numArgs $ \impl -> do - v <- yield >>= Internal.freshVar loc - output v - return (impl, v) - return (Internal.mkConstructorVarPattern Explicit c xs) - (v1, p1) <- mkpat - (v2, p2) <- mkpat + mkpat = Internal.genConstructorPattern loc Explicit cinfo + (p1, v1) <- mkpat + (p2, v2) <- mkpat return Internal.LambdaClause { _lambdaPatterns = p1 :| [p2], @@ -676,34 +843,28 @@ deriveEq DerivingArgs {..} = do where allEq :: (Internal.IsExpression expr) => [(expr, expr, Bool)] -> Internal.Expression allEq k = case nonEmpty k of - Nothing -> Internal.toExpression btrue + Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue) Just l -> mkAnds (fmap (uncurry3 mkEq) l) mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression mkAnds = foldl1 mkAnd . fmap Internal.toExpression mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression - mkAnd a b = band Internal.@@ a Internal.@@ b + mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b mkEq :: (Internal.IsExpression expr) => expr -> expr -> Bool -> Internal.Expression mkEq a b isRec - | isRec = lam Internal.@@ a Internal.@@ b - | otherwise = bisEqual Internal.@@ a Internal.@@ b - - getNumArgs :: Sem r [IsImplicit] - getNumArgs = do - def <- getDefinedConstructor c - return $ - def - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramImplicit + | isRec = recDef Internal.@@ a Internal.@@ b + | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b getRecursiveArgs :: Sem r [Bool] getRecursiveArgs = do - def <- getDefinedConstructor c - let argTypes = map (^. Internal.paramType) $ Internal.constructorArgs (def ^. Internal.constructorInfoType) + let argTypes = + cinfo + ^.. Internal.constructorInfoType + . to Internal.constructorArgs + . each + . Internal.paramType return $ map (== argty) argTypes goFunctionDef :: @@ -850,6 +1011,8 @@ checkBuiltinInductive :: checkBuiltinInductive d b = localBuiltins $ case b of BuiltinNat -> checkNatDef d BuiltinEq -> checkEqDef d + BuiltinOrdering -> checkOrderingDef d + BuiltinOrd -> checkOrdDef d BuiltinBool -> checkBoolDef d BuiltinInt -> checkIntDef d BuiltinList -> checkListDef d @@ -873,6 +1036,7 @@ checkBuiltinFunction :: checkBuiltinFunction d f = localBuiltins $ case f of BuiltinAssert -> checkAssert d BuiltinIsEqual -> checkIsEq d + BuiltinOrdCompare -> checkOrdCompare d BuiltinNatPlus -> checkNatPlus d BuiltinNatSub -> checkNatSub d BuiltinNatMul -> checkNatMul d diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index bc5ee62bfd..a3ca02cbb2 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -545,9 +545,24 @@ sseq_ = "seq" isEqual :: (IsString s) => s isEqual = "isEqual" +compare :: (IsString s) => s +compare = "compare" + +lt :: (IsString s) => s +lt = "lt" + +gt :: (IsString s) => s +gt = "gt" + eq :: (IsString s) => s eq = "eq" +ord :: (IsString s) => s +ord = "ord" + +ordering :: (IsString s) => s +ordering = "ordering" + assert_ :: (IsString s) => s assert_ = "assert" @@ -1154,6 +1169,9 @@ anomaMkAction = "mkAction" mkEq :: (IsString s) => s mkEq = "mkEq" +mkOrd :: (IsString s) => s +mkOrd = "mkOrd" + rustFn :: (IsString s) => s rustFn = "fn" diff --git a/src/Juvix/Prelude/Effects/Input.hs b/src/Juvix/Prelude/Effects/Input.hs index 8cc4edf4a5..d2f1f6fe25 100644 --- a/src/Juvix/Prelude/Effects/Input.hs +++ b/src/Juvix/Prelude/Effects/Input.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + module Juvix.Prelude.Effects.Input ( Input, input, @@ -5,6 +7,8 @@ module Juvix.Prelude.Effects.Input inputWhile, peekInput, runInputList, + repeatOnInput, + isEndOfInput, ) where @@ -43,5 +47,11 @@ peekInput = do runInputList :: [i] -> Sem (Input i ': r) a -> Sem r a runInputList = evalStaticRep . Input +isEndOfInput :: forall i r. (Members '[Input i] r) => Sem r Bool +isEndOfInput = isNothing <$> peekInput @i + +repeatOnInput :: (Members '[Input i] r) => (i -> Sem r a) -> Sem r () +repeatOnInput m = whenJustM input (m >=> const (repeatOnInput m)) + inputJust :: (Members '[Input i] r) => Sem r i inputJust = fromMaybe (error "inputJust") <$> input diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 3a46fc3a69..1fbdc9d630 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -505,5 +505,10 @@ tests = "Test086: Patterns in definitions" $(mkRelDir ".") $(mkRelFile "test086.juvix") - $(mkRelFile "out/test086.out") + $(mkRelFile "out/test086.out"), + posTest + "Test087: Deriving Ord" + $(mkRelDir ".") + $(mkRelFile "test087.juvix") + $(mkRelFile "out/test087.out") ] diff --git a/tests/Compilation/positive/out/test087.out b/tests/Compilation/positive/out/test087.out new file mode 100644 index 0000000000..df0c967608 --- /dev/null +++ b/tests/Compilation/positive/out/test087.out @@ -0,0 +1,5 @@ +Equal +LessThan +GreaterThan +LessThan +GreaterThan diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix new file mode 100644 index 0000000000..0e996b6487 --- /dev/null +++ b/tests/Compilation/positive/test087.juvix @@ -0,0 +1,26 @@ +-- Deriving Ord +module test087; + +import Stdlib.Data.Fixity open; +import Stdlib.Data.Bool open; +import Stdlib.Data.Pair open; +import Stdlib.Trait.Ord open; +import Stdlib.System.IO open; + +syntax alias compare := Ord.cmp; + +type T := + | One + | Two + | Three + | Four; + +deriving instance +ordT : Ord T; + +main : IO := + printLn (compare One One) + >>> printLn (compare One Two) + >>> printLn (compare Two One) + >>> printLn (compare (One, One) (One, Three)) + >>> printLn (compare (Four, Four) (Four, Three)); diff --git a/tests/negative/Internal/LazyBuiltin.juvix b/tests/negative/Internal/LazyBuiltin.juvix index cb23733771..b34d3ea33c 100644 --- a/tests/negative/Internal/LazyBuiltin.juvix +++ b/tests/negative/Internal/LazyBuiltin.juvix @@ -2,8 +2,8 @@ module LazyBuiltin; builtin bool type Bool := - | true : Bool - | false : Bool; + | false : Bool + | true : Bool; builtin bool-if ite : {A : Type} -> Bool -> A -> A -> A From 499de4f570c5d5420147304a0e4e89cd1098a8ca Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Tue, 26 Nov 2024 19:54:43 +0100 Subject: [PATCH 2/7] extract common --- src/Juvix/Compiler/Internal/Extra/Base.hs | 7 + .../Internal/Translation/FromConcrete.hs | 221 +++++++++++++++--- 2 files changed, 200 insertions(+), 28 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index f85fb14257..faec8aee0f 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -821,6 +821,13 @@ isSmallUniverse' = \case isTypeConstructor :: Expression -> Bool isTypeConstructor = isSmallUniverse' . snd . unfoldFunType +explicitApplicationArg :: Expression -> ApplicationArg +explicitApplicationArg e = + ApplicationArg + { _appArgIsImplicit = Explicit, + _appArg = e + } + explicitPatternArg :: Pattern -> PatternArg explicitPatternArg _patternArgPattern = PatternArg diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 42ddd050d8..d5f68875c7 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -705,6 +705,189 @@ derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) getDefinedInductiveConstructors ind +deriveRecursiveBinaryFunction :: + (Members '[NameIdGen] r) => + Text -> + Internal.Name -> + DerivingArgs -> + ( ( Internal.ConstructorInfo -> + [(Internal.ApplicationArg, Internal.ApplicationArg)] -> + [Internal.Expression] + ) -> + Sem r Internal.Expression + ) -> + Sem r (Internal.Name, Internal.LetClause) +deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do + let instName = _derivingInstanceName + loc = getLoc instName + recDefName <- Internal.freshFunVar loc (label <> "__" <> instName ^. Internal.nameText) + let rfun isRec + | isRec = recDefName + | otherwise = nonSelfRec + mkRecCall cinfo recArgs = + let selfRecArgs :: [Bool] + selfRecArgs = + let argTypes = + cinfo + ^.. Internal.constructorInfoType + . to Internal.constructorArgs + . each + . Internal.paramType + in map (== ret) argTypes + in [ Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2] + | ((arg1, arg2), isRec) <- zipExact recArgs selfRecArgs + ] + + lamBody <- mkLamDef mkRecCall + lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName) + let lamDef = + Internal.FunctionDef + { _funDefTerminating = False, + _funDefIsInstanceCoercion = Nothing, + _funDefPragmas = mempty, + _funDefArgsInfo = [], + _funDefDocComment = Nothing, + _funDefName = recDefName, + _funDefType = lamTy, + _funDefBody = lamBody, + _funDefBuiltin = Nothing + } + return (recDefName, Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))) + where + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression eqName) args + + eqName :: Internal.InductiveName + args :: [Internal.ApplicationArg] + (eqName, args) = _derivingReturnType + +deriveEq2 :: + forall r. + ( Members + '[ Reader S.InfoTable, + Reader Internal.InfoTable, + State LocalTable, + NameIdGen, + Error ScoperError, + Reader DefaultArgsStack, + Reader Pragmas + ] + r + ) => + DerivingArgs -> + Sem r Internal.FunctionDef +deriveEq2 der@DerivingArgs {..} = do + argsInfo <- goArgsInfo _derivingInstanceName + bs <- mkBuiltins + (recDefName, mutblock :: Internal.LetClause) <- + deriveRecursiveBinaryFunction "eq" (bs ^. eqBuiltinIsEqual) der (eqLambda bs) + mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq + let body = + Internal.ExpressionLet + Internal.Let + { _letClauses = pure mutblock, + _letExpression = mkEq Internal.@@ recDefName + } + ty = Internal.foldFunType _derivingParameters ret + pragmas' <- goPragmas _derivingPragmas + return + Internal.FunctionDef + { _funDefTerminating = False, + _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, + _funDefPragmas = pragmas', + _funDefArgsInfo = argsInfo, + _funDefDocComment = Nothing, + _funDefName = _derivingInstanceName, + _funDefType = ty, + _funDefBody = body, + _funDefBuiltin = Nothing + } + where + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression eqName) args + + eqName :: Internal.InductiveName + args :: [Internal.ApplicationArg] + (eqName, args) = _derivingReturnType + + mkBuiltins :: Sem r EqBuiltins + mkBuiltins = do + let loc = getLoc eqName + band <- getBuiltin loc BuiltinBoolAnd + btrue <- getBuiltin loc BuiltinBoolTrue + bfalse <- getBuiltin loc BuiltinBoolFalse + bisEqual <- getBuiltin loc BuiltinIsEqual + return + EqBuiltins + { _eqBuiltinTrue = btrue, + _eqBuiltinFalse = bfalse, + _eqBuiltinIsEqual = bisEqual, + _eqBuiltinAnd = band + } + + eqLambda :: + EqBuiltins -> + ( Internal.ConstructorInfo -> + [(Internal.ApplicationArg, Internal.ApplicationArg)] -> + [Internal.Expression] + ) -> + Sem r Internal.Expression + eqLambda bs recCalls = do + constrs <- derivingGetConstrs ret args + case nonEmpty constrs of + Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue)) + Just cs -> do + cl' <- mapM lambdaClause cs + defaultCl' <- + if + | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause + | otherwise -> return Nothing + return $ + Internal.ExpressionLambda + Internal.Lambda + { _lambdaType = Nothing, + _lambdaClauses = snocNonEmptyMaybe cl' defaultCl' + } + where + defaultLambdaClause :: Sem r Internal.LambdaClause + defaultLambdaClause = do + let loc = getLoc eqName + p1 <- Internal.genWildcard loc Internal.Explicit + p2 <- Internal.genWildcard loc Internal.Explicit + return + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse) + } + + lambdaClause :: + Internal.ConstructorInfo -> + Sem r Internal.LambdaClause + lambdaClause cinfo = do + let loc = getLoc _derivingInstanceName + mkpat = Internal.genConstructorPattern loc Explicit cinfo + (p1, v1) <- mkpat + (p2, v2) <- mkpat + return + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = allEq (zipExact v1 v2) + } + where + allEq :: (Internal.IsExpression expr) => [(expr, expr)] -> Internal.Expression + allEq k = case nonEmpty (recCalls cinfo kargs) of + Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue) + Just l -> mkAnds l + where + kargs :: [(Internal.ApplicationArg, Internal.ApplicationArg)] + kargs = map (over both (Internal.explicitApplicationArg . Internal.toExpression)) k + + mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression + mkAnds = foldl1 mkAnd . fmap Internal.toExpression + + mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression + mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b + deriveEq :: forall r. ( Members @@ -721,12 +904,9 @@ deriveEq :: DerivingArgs -> Sem r Internal.FunctionDef deriveEq DerivingArgs {..} = do - indInfo <- getIndInfo - let argty = getArgType indInfo argsInfo <- goArgsInfo _derivingInstanceName - lamName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText) - let lam = Internal.ExpressionIden (Internal.IdenFunction lamName) - lamFun <- eqLambda lam argty + recDefName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText) + lamFun <- eqLambda (Internal.toExpression recDefName) lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName) let lamDef = Internal.FunctionDef @@ -735,7 +915,7 @@ deriveEq DerivingArgs {..} = do _funDefPragmas = mempty, _funDefArgsInfo = [], _funDefDocComment = Nothing, - _funDefName = lamName, + _funDefName = recDefName, _funDefType = lamTy, _funDefBody = lamFun, _funDefBuiltin = Nothing @@ -746,7 +926,7 @@ deriveEq DerivingArgs {..} = do Internal.ExpressionLet Internal.Let { _letClauses = pure (Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))), - _letExpression = mkEq Internal.@@ lam + _letExpression = mkEq Internal.@@ recDefName } ty = Internal.foldFunType _derivingParameters ret return @@ -769,23 +949,8 @@ deriveEq DerivingArgs {..} = do args :: [Internal.ApplicationArg] (eqName, args) = _derivingReturnType - getIndInfo :: Sem r Internal.InductiveInfo - getIndInfo = runFailDefaultM (throwDerivingWrongForm ret) $ do - [Internal.ApplicationArg Explicit a] <- return args - Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) - getDefinedInductive ind - - getArgType :: Internal.InductiveInfo -> Internal.Expression - getArgType indInfo = - Internal.foldApplication - (Internal.toExpression (indInfo ^. Internal.inductiveInfoName)) - (map toAppArg (indInfo ^. Internal.inductiveInfoParameters)) - where - toAppArg :: Internal.InductiveParameter -> Internal.ApplicationArg - toAppArg p = Internal.ApplicationArg Explicit (Internal.toExpression (p ^. Internal.inductiveParamName)) - - eqLambda :: Internal.Expression -> Internal.Expression -> Sem r Internal.Expression - eqLambda recDef argty = do + eqLambda :: Internal.Expression -> Sem r Internal.Expression + eqLambda recDef = do let loc = getLoc eqName band <- getBuiltin loc BuiltinBoolAnd btrue <- getBuiltin loc BuiltinBoolTrue @@ -830,7 +995,7 @@ deriveEq DerivingArgs {..} = do Internal.ConstructorInfo -> Sem r Internal.LambdaClause lambdaClause bs cinfo = do - argsRecursive :: [Bool] <- getRecursiveArgs + let argsRecursive :: [Bool] = getRecursiveArgs let loc = getLoc _derivingInstanceName mkpat = Internal.genConstructorPattern loc Explicit cinfo (p1, v1) <- mkpat @@ -857,15 +1022,15 @@ deriveEq DerivingArgs {..} = do | isRec = recDef Internal.@@ a Internal.@@ b | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b - getRecursiveArgs :: Sem r [Bool] - getRecursiveArgs = do + getRecursiveArgs :: [Bool] + getRecursiveArgs = let argTypes = cinfo ^.. Internal.constructorInfoType . to Internal.constructorArgs . each . Internal.paramType - return $ map (== argty) argTypes + in map (== ret) argTypes goFunctionDef :: forall r. From 0e0b91022f2128e6565f849b04994b1b1362af54 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Tue, 26 Nov 2024 19:55:23 +0100 Subject: [PATCH 3/7] remove old --- .../Internal/Translation/FromConcrete.hs | 148 +----------------- 1 file changed, 2 insertions(+), 146 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index d5f68875c7..80e3678a7f 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -761,7 +761,7 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do args :: [Internal.ApplicationArg] (eqName, args) = _derivingReturnType -deriveEq2 :: +deriveEq :: forall r. ( Members '[ Reader S.InfoTable, @@ -776,7 +776,7 @@ deriveEq2 :: ) => DerivingArgs -> Sem r Internal.FunctionDef -deriveEq2 der@DerivingArgs {..} = do +deriveEq der@DerivingArgs {..} = do argsInfo <- goArgsInfo _derivingInstanceName bs <- mkBuiltins (recDefName, mutblock :: Internal.LetClause) <- @@ -888,150 +888,6 @@ deriveEq2 der@DerivingArgs {..} = do mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b -deriveEq :: - forall r. - ( Members - '[ Reader S.InfoTable, - Reader Internal.InfoTable, - State LocalTable, - NameIdGen, - Error ScoperError, - Reader DefaultArgsStack, - Reader Pragmas - ] - r - ) => - DerivingArgs -> - Sem r Internal.FunctionDef -deriveEq DerivingArgs {..} = do - argsInfo <- goArgsInfo _derivingInstanceName - recDefName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText) - lamFun <- eqLambda (Internal.toExpression recDefName) - lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName) - let lamDef = - Internal.FunctionDef - { _funDefTerminating = False, - _funDefIsInstanceCoercion = Nothing, - _funDefPragmas = mempty, - _funDefArgsInfo = [], - _funDefDocComment = Nothing, - _funDefName = recDefName, - _funDefType = lamTy, - _funDefBody = lamFun, - _funDefBuiltin = Nothing - } - mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq - pragmas' <- goPragmas _derivingPragmas - let body = - Internal.ExpressionLet - Internal.Let - { _letClauses = pure (Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))), - _letExpression = mkEq Internal.@@ recDefName - } - ty = Internal.foldFunType _derivingParameters ret - return - Internal.FunctionDef - { _funDefTerminating = False, - _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, - _funDefPragmas = pragmas', - _funDefArgsInfo = argsInfo, - _funDefDocComment = Nothing, - _funDefName = _derivingInstanceName, - _funDefType = ty, - _funDefBody = body, - _funDefBuiltin = Nothing - } - where - ret :: Internal.Expression - ret = Internal.foldApplication (Internal.toExpression eqName) args - - eqName :: Internal.InductiveName - args :: [Internal.ApplicationArg] - (eqName, args) = _derivingReturnType - - eqLambda :: Internal.Expression -> Sem r Internal.Expression - eqLambda recDef = do - let loc = getLoc eqName - band <- getBuiltin loc BuiltinBoolAnd - btrue <- getBuiltin loc BuiltinBoolTrue - bfalse <- getBuiltin loc BuiltinBoolFalse - bisEqual <- getBuiltin loc BuiltinIsEqual - constrs <- derivingGetConstrs ret args - let bs = - EqBuiltins - { _eqBuiltinTrue = btrue, - _eqBuiltinFalse = bfalse, - _eqBuiltinIsEqual = bisEqual, - _eqBuiltinAnd = band - } - case nonEmpty constrs of - Nothing -> return (Internal.toExpression btrue) - Just cs -> do - cl' <- mapM (lambdaClause bs) cs - defaultCl' <- - if - | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bs - | otherwise -> return Nothing - return $ - Internal.ExpressionLambda - Internal.Lambda - { _lambdaType = Nothing, - _lambdaClauses = snocNonEmptyMaybe cl' defaultCl' - } - where - defaultLambdaClause :: EqBuiltins -> Sem r Internal.LambdaClause - defaultLambdaClause bs = do - let loc = getLoc eqName - p1 <- Internal.genWildcard loc Internal.Explicit - p2 <- Internal.genWildcard loc Internal.Explicit - return - Internal.LambdaClause - { _lambdaPatterns = p1 :| [p2], - _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse) - } - - lambdaClause :: - EqBuiltins -> - Internal.ConstructorInfo -> - Sem r Internal.LambdaClause - lambdaClause bs cinfo = do - let argsRecursive :: [Bool] = getRecursiveArgs - let loc = getLoc _derivingInstanceName - mkpat = Internal.genConstructorPattern loc Explicit cinfo - (p1, v1) <- mkpat - (p2, v2) <- mkpat - return - Internal.LambdaClause - { _lambdaPatterns = p1 :| [p2], - _lambdaBody = allEq (zip3Exact v1 v2 argsRecursive) - } - where - allEq :: (Internal.IsExpression expr) => [(expr, expr, Bool)] -> Internal.Expression - allEq k = case nonEmpty k of - Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue) - Just l -> mkAnds (fmap (uncurry3 mkEq) l) - - mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression - mkAnds = foldl1 mkAnd . fmap Internal.toExpression - - mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression - mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b - - mkEq :: (Internal.IsExpression expr) => expr -> expr -> Bool -> Internal.Expression - mkEq a b isRec - | isRec = recDef Internal.@@ a Internal.@@ b - | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b - - getRecursiveArgs :: [Bool] - getRecursiveArgs = - let argTypes = - cinfo - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - in map (== ret) argTypes - goFunctionDef :: forall r. (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => From 78dec074a8e23dc946eda21e21359eb2b4191066 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Tue, 26 Nov 2024 20:29:34 +0100 Subject: [PATCH 4/7] refactor ord --- juvix-stdlib | 2 +- src/Juvix/Compiler/Internal/Extra/Base.hs | 4 +- .../Internal/Translation/FromConcrete.hs | 238 +++++++++--------- 3 files changed, 128 insertions(+), 116 deletions(-) diff --git a/juvix-stdlib b/juvix-stdlib index a6abb99562..9534bd214d 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit a6abb9956261f152cea5b14a0d31a9cce6c1957f +Subproject commit 9534bd214df2983f4f5918ddcff3703f63bd1de1 diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index faec8aee0f..f8a3c4f930 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -821,11 +821,11 @@ isSmallUniverse' = \case isTypeConstructor :: Expression -> Bool isTypeConstructor = isSmallUniverse' . snd . unfoldFunType -explicitApplicationArg :: Expression -> ApplicationArg +explicitApplicationArg :: (IsExpression expr) => expr -> ApplicationArg explicitApplicationArg e = ApplicationArg { _appArgIsImplicit = Explicit, - _appArg = e + _appArg = toExpression e } explicitPatternArg :: Pattern -> PatternArg diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 80e3678a7f..36ccfe6075 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -74,8 +74,7 @@ data EqBuiltins = EqBuiltins makeLenses ''EqBuiltins data OrdBuiltins = OrdBuiltins - { _ordBuiltinCompare :: Internal.Name, - _ordBuiltinLt :: Internal.Name, + { _ordBuiltinLt :: Internal.Name, _ordBuiltinEq :: Internal.Name, _ordBuiltinGt :: Internal.Name } @@ -578,7 +577,7 @@ deriveOrd :: ) => DerivingArgs -> Sem r Internal.FunctionDef -deriveOrd DerivingArgs {..} = do +deriveOrd der@DerivingArgs {..} = do arg <- derivingGetConstrs ret args argsInfo <- goArgsInfo _derivingInstanceName let loc = getLoc ordName @@ -589,14 +588,18 @@ deriveOrd DerivingArgs {..} = do beq <- getBuiltin loc BuiltinOrderingEQ let bs = OrdBuiltins - { _ordBuiltinCompare = bcmp, - _ordBuiltinLt = blt, + { _ordBuiltinLt = blt, _ordBuiltinGt = bgt, _ordBuiltinEq = beq } - lam <- genOrdCompare (getLoc _derivingInstanceName) bs arg - let ty = Internal.foldFunType _derivingParameters ret - body = mkOrd Internal.@@ lam + (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs arg) + let body = + Internal.ExpressionLet + Internal.Let + { _letClauses = pure mutblock, + _letExpression = mkOrd Internal.@@ recName + } + ty = Internal.foldFunType _derivingParameters ret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -618,82 +621,98 @@ deriveOrd DerivingArgs {..} = do args :: [Internal.ApplicationArg] (ordName, args) = _derivingReturnType -genOrdCompare :: - forall r. - (Members '[NameIdGen] r) => - Interval -> - OrdBuiltins -> - [ConstructorInfo] -> - Sem r Internal.Expression -genOrdCompare loc bs cs = do - res <- - fmap nonEmpty - . execOutputList - . runInputList cs - $ repeatOnInput go - Internal.mkLambda <$> case res of - Nothing -> pure <$> emptyTypeClause - Just l -> return l - where - emptyTypeClause :: Sem r Internal.LambdaClause - emptyTypeClause = do - w1 <- Internal.genWildcard loc Explicit - w2 <- Internal.genWildcard loc Explicit - return - Internal.LambdaClause - { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq), - _lambdaPatterns = w1 :| [w2] - } - - go :: (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r') => ConstructorInfo -> Sem r' () - go c = do - isLast <- isEndOfInput @ConstructorInfo - let mkPat = Internal.genConstructorPattern loc Explicit c - (p1, v1) <- mkPat - (p2, v2) <- mkPat - lord <- lexOrder (zipExact v1 v2) - let sameConstr = + genOrdCompare :: + forall r'. + (Members '[NameIdGen] r') => + Interval -> + OrdBuiltins -> + [ConstructorInfo] -> + (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) -> + Sem r' Internal.Expression + genOrdCompare loc bs cs recCmp = do + res <- + fmap nonEmpty + . execOutputList + . runInputList cs + $ repeatOnInput go + Internal.mkLambda <$> case res of + Nothing -> pure <$> emptyTypeClause + Just l -> return l + where + emptyTypeClause :: Sem r' Internal.LambdaClause + emptyTypeClause = do + w1 <- Internal.genWildcard loc Explicit + w2 <- Internal.genWildcard loc Explicit + return Internal.LambdaClause - { _lambdaPatterns = p1 :| [p2], - _lambdaBody = lord + { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq), + _lambdaPatterns = w1 :| [w2] } - output sameConstr - unless isLast $ do - p3 <- fst <$> mkPat - w3 <- Internal.genWildcard loc Explicit - output - Internal.LambdaClause - { _lambdaPatterns = p3 :| [w3], - _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt) - } - p4 <- fst <$> mkPat - w4 <- Internal.genWildcard loc Explicit - output - Internal.LambdaClause - { _lambdaPatterns = w4 :| [p4], - _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt) - } - lexOrder :: forall r'. (Members '[NameIdGen] r') => [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression - lexOrder = lexgo - where - cmp :: Internal.VarName -> Internal.VarName -> Internal.Expression - cmp a b = (bs ^. ordBuiltinCompare) Internal.@@ a Internal.@@ b - - lexgo :: [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression - lexgo = \case - [] -> return (Internal.toExpression (bs ^. ordBuiltinEq)) - (x, x') : vs - | null vs -> return (cmp x x') - | otherwise -> do - v <- Internal.freshVar loc "ltGt" - let pv = Internal.mkVarPattern v Explicit - mkPat :: Internal.Name -> Internal.PatternArg - mkPat p = Internal.mkConstructorVarPattern Explicit p [] - branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v) - branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs - let branches = branchEq :| [branchNEq] - return (Internal.mkCase (cmp x x') branches) + go :: + (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r'') => + ConstructorInfo -> + Sem r'' () + go c = do + isLast <- isEndOfInput @ConstructorInfo + let mkPat = Internal.genConstructorPattern loc Explicit c + (p1, v1) <- mkPat + (p2, v2) <- mkPat + let selfRecArgs :: [Bool] + selfRecArgs = + c + ^.. Internal.constructorInfoType + . to Internal.constructorArgs + . each + . Internal.paramType + . to (== ret) + lord <- lexOrder (zip3Exact selfRecArgs v1 v2) + let sameConstr = + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = lord + } + output sameConstr + unless isLast $ do + p3 <- fst <$> mkPat + w3 <- Internal.genWildcard loc Explicit + output + Internal.LambdaClause + { _lambdaPatterns = p3 :| [w3], + _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt) + } + p4 <- fst <$> mkPat + w4 <- Internal.genWildcard loc Explicit + output + Internal.LambdaClause + { _lambdaPatterns = w4 :| [p4], + _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt) + } + + lexOrder :: + forall r''. + (Members '[NameIdGen] r'') => + [(Bool, Internal.VarName, Internal.VarName)] -> + Sem r'' Internal.Expression + lexOrder = lexgo + where + cmp :: Bool -> Internal.VarName -> Internal.VarName -> Internal.Expression + cmp isRec a b = recCmp isRec (Internal.explicitApplicationArg a) (Internal.explicitApplicationArg b) + + lexgo :: [(Bool, Internal.VarName, Internal.VarName)] -> Sem r'' Internal.Expression + lexgo = \case + [] -> return (Internal.toExpression (bs ^. ordBuiltinEq)) + (isRec, x, x') : vs + | null vs -> return (cmp isRec x x') + | otherwise -> do + v <- Internal.freshVar loc "ltGt" + let pv = Internal.mkVarPattern v Explicit + mkPat :: Internal.Name -> Internal.PatternArg + mkPat p = Internal.mkConstructorVarPattern Explicit p [] + branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v) + branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs + let branches = branchEq :| [branchNEq] + return (Internal.mkCase (cmp isRec x x') branches) derivingGetConstrs :: (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) => @@ -710,9 +729,10 @@ deriveRecursiveBinaryFunction :: Text -> Internal.Name -> DerivingArgs -> - ( ( Internal.ConstructorInfo -> - [(Internal.ApplicationArg, Internal.ApplicationArg)] -> - [Internal.Expression] + ( ( Bool -> -- isSelfRecursive + Internal.ApplicationArg -> + Internal.ApplicationArg -> + Internal.Expression ) -> Sem r Internal.Expression ) -> @@ -724,20 +744,7 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do let rfun isRec | isRec = recDefName | otherwise = nonSelfRec - mkRecCall cinfo recArgs = - let selfRecArgs :: [Bool] - selfRecArgs = - let argTypes = - cinfo - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - in map (== ret) argTypes - in [ Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2] - | ((arg1, arg2), isRec) <- zipExact recArgs selfRecArgs - ] - + mkRecCall isRec arg1 arg2 = Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2] lamBody <- mkLamDef mkRecCall lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName) let lamDef = @@ -753,13 +760,6 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do _funDefBuiltin = Nothing } return (recDefName, Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))) - where - ret :: Internal.Expression - ret = Internal.foldApplication (Internal.toExpression eqName) args - - eqName :: Internal.InductiveName - args :: [Internal.ApplicationArg] - (eqName, args) = _derivingReturnType deriveEq :: forall r. @@ -827,12 +827,13 @@ deriveEq der@DerivingArgs {..} = do eqLambda :: EqBuiltins -> - ( Internal.ConstructorInfo -> - [(Internal.ApplicationArg, Internal.ApplicationArg)] -> - [Internal.Expression] + ( Bool -> + Internal.ApplicationArg -> + Internal.ApplicationArg -> + Internal.Expression ) -> Sem r Internal.Expression - eqLambda bs recCalls = do + eqLambda bs recCall = do constrs <- derivingGetConstrs ret args case nonEmpty constrs of Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue)) @@ -875,12 +876,23 @@ deriveEq der@DerivingArgs {..} = do } where allEq :: (Internal.IsExpression expr) => [(expr, expr)] -> Internal.Expression - allEq k = case nonEmpty (recCalls cinfo kargs) of - Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue) - Just l -> mkAnds l + allEq k = + let rargs = [recCall r a b | ((a, b), r) <- zipExact kargs selfRecArgs] + in case nonEmpty rargs of + Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue) + Just l -> mkAnds l where kargs :: [(Internal.ApplicationArg, Internal.ApplicationArg)] - kargs = map (over both (Internal.explicitApplicationArg . Internal.toExpression)) k + kargs = map (over both Internal.explicitApplicationArg) k + + selfRecArgs :: [Bool] + selfRecArgs = + cinfo + ^.. Internal.constructorInfoType + . to Internal.constructorArgs + . each + . Internal.paramType + . to (== ret) mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression mkAnds = foldl1 mkAnd . fmap Internal.toExpression From 9fea5f8bc2714f88c02b4dd58258600a88e54234 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Wed, 27 Nov 2024 18:07:21 +0100 Subject: [PATCH 5/7] debug --- .../Internal/Translation/FromConcrete.hs | 55 ++++++++++++------- tests/Compilation/positive/test087.juvix | 11 +++- 2 files changed, 44 insertions(+), 22 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 36ccfe6075..a224f20bee 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -28,7 +28,7 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal import Juvix.Compiler.Internal.Extra (mkLetClauses) import Juvix.Compiler.Internal.Extra qualified as Internal import Juvix.Compiler.Internal.Extra.DependencyBuilder -import Juvix.Compiler.Internal.Language (varFromWildcard) +import Juvix.Compiler.Internal.Pretty qualified as I import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker @@ -578,7 +578,7 @@ deriveOrd :: DerivingArgs -> Sem r Internal.FunctionDef deriveOrd der@DerivingArgs {..} = do - arg <- derivingGetConstrs ret args + (constrs, subjectTy) <- derivingGetConstrs fullret args argsInfo <- goArgsInfo _derivingInstanceName let loc = getLoc ordName mkOrd <- getBuiltin loc BuiltinMkOrd @@ -592,14 +592,14 @@ deriveOrd der@DerivingArgs {..} = do _ordBuiltinGt = bgt, _ordBuiltinEq = beq } - (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs arg) + (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs subjectTy constrs) let body = Internal.ExpressionLet Internal.Let { _letClauses = pure mutblock, _letExpression = mkOrd Internal.@@ recName } - ty = Internal.foldFunType _derivingParameters ret + ty = Internal.foldFunType _derivingParameters fullret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -614,8 +614,8 @@ deriveOrd der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - ret :: Internal.Expression - ret = Internal.foldApplication (Internal.toExpression ordName) args + fullret :: Internal.Expression + fullret = Internal.foldApplication (Internal.toExpression ordName) args ordName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -626,10 +626,11 @@ deriveOrd der@DerivingArgs {..} = do (Members '[NameIdGen] r') => Interval -> OrdBuiltins -> + Internal.Expression -> [ConstructorInfo] -> (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) -> Sem r' Internal.Expression - genOrdCompare loc bs cs recCmp = do + genOrdCompare loc bs subjectTy cs recCmp = do res <- fmap nonEmpty . execOutputList @@ -658,14 +659,24 @@ deriveOrd der@DerivingArgs {..} = do let mkPat = Internal.genConstructorPattern loc Explicit c (p1, v1) <- mkPat (p2, v2) <- mkPat - let selfRecArgs :: [Bool] - selfRecArgs = + let tmp = c ^.. Internal.constructorInfoType . to Internal.constructorArgs . each . Internal.paramType - . to (== ret) + + let selfRecArgs :: [Bool] + selfRecArgs = + trace + ("fullret " <> I.ppTrace fullret <> "\nargs = " <> I.ppTrace ((^. Internal.appArg) <$> args)) + tmp + ^.. each + . to (== subjectTy) + traceM ("cargs = " <> I.ppTrace tmp) + traceM ("selfrecargs = " <> prettyText selfRecArgs) + traceM ("subjectTy = " <> I.ppTrace subjectTy) + traceM "\n\n" lord <- lexOrder (zip3Exact selfRecArgs v1 v2) let sameConstr = Internal.LambdaClause @@ -718,11 +729,12 @@ derivingGetConstrs :: (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) => Internal.Expression -> [Internal.ApplicationArg] -> - Sem r [Internal.ConstructorInfo] + Sem r ([Internal.ConstructorInfo], Internal.Expression) derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do [Internal.ApplicationArg Explicit a] <- return args Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) - getDefinedInductiveConstructors ind + cs <- getDefinedInductiveConstructors ind + return (cs, a) deriveRecursiveBinaryFunction :: (Members '[NameIdGen] r) => @@ -788,7 +800,7 @@ deriveEq der@DerivingArgs {..} = do { _letClauses = pure mutblock, _letExpression = mkEq Internal.@@ recDefName } - ty = Internal.foldFunType _derivingParameters ret + ty = Internal.foldFunType _derivingParameters fullret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -803,8 +815,8 @@ deriveEq der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - ret :: Internal.Expression - ret = Internal.foldApplication (Internal.toExpression eqName) args + fullret :: Internal.Expression + fullret = Internal.foldApplication (Internal.toExpression eqName) args eqName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -834,11 +846,11 @@ deriveEq der@DerivingArgs {..} = do ) -> Sem r Internal.Expression eqLambda bs recCall = do - constrs <- derivingGetConstrs ret args + (constrs, subjectTy) <- derivingGetConstrs fullret args case nonEmpty constrs of Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue)) Just cs -> do - cl' <- mapM lambdaClause cs + cl' <- mapM (lambdaClause subjectTy) cs defaultCl' <- if | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause @@ -862,9 +874,10 @@ deriveEq der@DerivingArgs {..} = do } lambdaClause :: + Internal.Expression -> Internal.ConstructorInfo -> Sem r Internal.LambdaClause - lambdaClause cinfo = do + lambdaClause subjectTy cinfo = do let loc = getLoc _derivingInstanceName mkpat = Internal.genConstructorPattern loc Explicit cinfo (p1, v1) <- mkpat @@ -892,7 +905,7 @@ deriveEq der@DerivingArgs {..} = do . to Internal.constructorArgs . each . Internal.paramType - . to (== ret) + . to (== subjectTy) mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression mkAnds = foldl1 mkAnd . fmap Internal.toExpression @@ -962,7 +975,7 @@ argToPattern arg@SigArg {..} = do _patternArgName :: Maybe Internal.Name = Nothing noName = goWildcard (Wildcard (getLoc arg)) goWildcard w = do - _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w + _patternArgPattern <- Internal.PatternVariable <$> Internal.varFromWildcard w return Internal.PatternArg {..} mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg mk = \case @@ -1972,7 +1985,7 @@ goPattern p = case p of PatternApplication a -> Internal.PatternConstructorApp <$> goPatternApplication a PatternInfixApplication a -> Internal.PatternConstructorApp <$> goInfixPatternApplication a PatternPostfixApplication a -> Internal.PatternConstructorApp <$> goPostfixPatternApplication a - PatternWildcard i -> Internal.PatternVariable <$> varFromWildcard i + PatternWildcard i -> Internal.PatternVariable <$> Internal.varFromWildcard i PatternRecord i -> goRecordPattern i PatternEmpty {} -> error "unsupported empty pattern" diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix index 0e996b6487..4f3e9347d8 100644 --- a/tests/Compilation/positive/test087.juvix +++ b/tests/Compilation/positive/test087.juvix @@ -18,9 +18,18 @@ type T := deriving instance ordT : Ord T; +type Tree (A : Type) := + | leaf + | node (Tree A) A (Tree A); + +deriving instance +ordTree {A} {{Ord A}} : Ord (Tree A); + main : IO := printLn (compare One One) >>> printLn (compare One Two) >>> printLn (compare Two One) >>> printLn (compare (One, One) (One, Three)) - >>> printLn (compare (Four, Four) (Four, Three)); + >>> printLn (compare (Four, Four) (Four, Three)) + >>> printLn + (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf)); From f5e92a72f3ba147567333ec60afb8be49c941587 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Wed, 27 Nov 2024 22:02:08 +0100 Subject: [PATCH 6/7] store self recursive args in constructor info --- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 12 +++- .../Internal/Translation/FromConcrete.hs | 58 +++++-------------- .../Compiler/Store/Internal/Data/InfoTable.hs | 1 + 3 files changed, 28 insertions(+), 43 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index e2c936e915..48d818d06b 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -263,5 +263,15 @@ mkConstructorEntries d = let _constructorInfoType = c ^. inductiveConstructorType, let _constructorInfoName = c ^. inductiveConstructorName, let _constructorInfoTrait = d ^. inductiveTrait, - let _constructorInfoRecord = c ^. inductiveConstructorIsRecord + let _constructorInfoRecord = c ^. inductiveConstructorIsRecord, + let _constructorSelfRecursiveArgs = selfRecursiveArgs (c ^. inductiveConstructorType) ] + where + selfRecursiveArgs :: Expression -> [Bool] + selfRecursiveArgs constrTy = constructorArgs constrTy ^.. each . paramType . to (== ty) + where + ty :: Expression + ty = + foldExplicitApplication + (toExpression (d ^. inductiveName)) + (d ^.. inductiveParameters . each . inductiveParamName . to toExpression) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a224f20bee..e812525deb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -28,7 +28,6 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal import Juvix.Compiler.Internal.Extra (mkLetClauses) import Juvix.Compiler.Internal.Extra qualified as Internal import Juvix.Compiler.Internal.Extra.DependencyBuilder -import Juvix.Compiler.Internal.Pretty qualified as I import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker @@ -578,7 +577,7 @@ deriveOrd :: DerivingArgs -> Sem r Internal.FunctionDef deriveOrd der@DerivingArgs {..} = do - (constrs, subjectTy) <- derivingGetConstrs fullret args + constrs <- derivingGetConstrs ret args argsInfo <- goArgsInfo _derivingInstanceName let loc = getLoc ordName mkOrd <- getBuiltin loc BuiltinMkOrd @@ -592,14 +591,14 @@ deriveOrd der@DerivingArgs {..} = do _ordBuiltinGt = bgt, _ordBuiltinEq = beq } - (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs subjectTy constrs) + (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs constrs) let body = Internal.ExpressionLet Internal.Let { _letClauses = pure mutblock, _letExpression = mkOrd Internal.@@ recName } - ty = Internal.foldFunType _derivingParameters fullret + ty = Internal.foldFunType _derivingParameters ret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -614,8 +613,8 @@ deriveOrd der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - fullret :: Internal.Expression - fullret = Internal.foldApplication (Internal.toExpression ordName) args + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression ordName) args ordName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -626,11 +625,10 @@ deriveOrd der@DerivingArgs {..} = do (Members '[NameIdGen] r') => Interval -> OrdBuiltins -> - Internal.Expression -> [ConstructorInfo] -> (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) -> Sem r' Internal.Expression - genOrdCompare loc bs subjectTy cs recCmp = do + genOrdCompare loc bs cs recCmp = do res <- fmap nonEmpty . execOutputList @@ -659,24 +657,8 @@ deriveOrd der@DerivingArgs {..} = do let mkPat = Internal.genConstructorPattern loc Explicit c (p1, v1) <- mkPat (p2, v2) <- mkPat - let tmp = - c - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - let selfRecArgs :: [Bool] - selfRecArgs = - trace - ("fullret " <> I.ppTrace fullret <> "\nargs = " <> I.ppTrace ((^. Internal.appArg) <$> args)) - tmp - ^.. each - . to (== subjectTy) - traceM ("cargs = " <> I.ppTrace tmp) - traceM ("selfrecargs = " <> prettyText selfRecArgs) - traceM ("subjectTy = " <> I.ppTrace subjectTy) - traceM "\n\n" + selfRecArgs = c ^. constructorSelfRecursiveArgs lord <- lexOrder (zip3Exact selfRecArgs v1 v2) let sameConstr = Internal.LambdaClause @@ -729,12 +711,11 @@ derivingGetConstrs :: (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) => Internal.Expression -> [Internal.ApplicationArg] -> - Sem r ([Internal.ConstructorInfo], Internal.Expression) + Sem r [Internal.ConstructorInfo] derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do [Internal.ApplicationArg Explicit a] <- return args Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) - cs <- getDefinedInductiveConstructors ind - return (cs, a) + getDefinedInductiveConstructors ind deriveRecursiveBinaryFunction :: (Members '[NameIdGen] r) => @@ -800,7 +781,7 @@ deriveEq der@DerivingArgs {..} = do { _letClauses = pure mutblock, _letExpression = mkEq Internal.@@ recDefName } - ty = Internal.foldFunType _derivingParameters fullret + ty = Internal.foldFunType _derivingParameters ret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -815,8 +796,8 @@ deriveEq der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - fullret :: Internal.Expression - fullret = Internal.foldApplication (Internal.toExpression eqName) args + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression eqName) args eqName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -846,11 +827,11 @@ deriveEq der@DerivingArgs {..} = do ) -> Sem r Internal.Expression eqLambda bs recCall = do - (constrs, subjectTy) <- derivingGetConstrs fullret args + constrs <- derivingGetConstrs ret args case nonEmpty constrs of Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue)) Just cs -> do - cl' <- mapM (lambdaClause subjectTy) cs + cl' <- mapM lambdaClause cs defaultCl' <- if | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause @@ -874,10 +855,9 @@ deriveEq der@DerivingArgs {..} = do } lambdaClause :: - Internal.Expression -> Internal.ConstructorInfo -> Sem r Internal.LambdaClause - lambdaClause subjectTy cinfo = do + lambdaClause cinfo = do let loc = getLoc _derivingInstanceName mkpat = Internal.genConstructorPattern loc Explicit cinfo (p1, v1) <- mkpat @@ -899,13 +879,7 @@ deriveEq der@DerivingArgs {..} = do kargs = map (over both Internal.explicitApplicationArg) k selfRecArgs :: [Bool] - selfRecArgs = - cinfo - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - . to (== subjectTy) + selfRecArgs = cinfo ^. Internal.constructorSelfRecursiveArgs mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression mkAnds = foldl1 mkAnd . fmap Internal.toExpression diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 71c71145a9..47ed0b90c7 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -9,6 +9,7 @@ data ConstructorInfo = ConstructorInfo _constructorInfoType :: Expression, _constructorInfoInductive :: InductiveName, _constructorInfoName :: ConstructorName, + _constructorSelfRecursiveArgs :: [Bool], _constructorInfoBuiltin :: Maybe BuiltinConstructor, _constructorInfoTrait :: Bool, _constructorInfoRecord :: Bool From 1cdcb02fb4b6fb132e8ff94b39850be72ea9515e Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira <janmasrovira@gmail.com> Date: Thu, 28 Nov 2024 09:38:11 +0100 Subject: [PATCH 7/7] extend test --- tests/Compilation/positive/out/test087.out | 3 +++ tests/Compilation/positive/test087.juvix | 10 +++++++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/tests/Compilation/positive/out/test087.out b/tests/Compilation/positive/out/test087.out index df0c967608..b686bb0401 100644 --- a/tests/Compilation/positive/out/test087.out +++ b/tests/Compilation/positive/out/test087.out @@ -3,3 +3,6 @@ LessThan GreaterThan LessThan GreaterThan +LessThan +GreaterThan +Equal diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix index 4f3e9347d8..2252dce3a6 100644 --- a/tests/Compilation/positive/test087.juvix +++ b/tests/Compilation/positive/test087.juvix @@ -32,4 +32,12 @@ main : IO := >>> printLn (compare (One, One) (One, Three)) >>> printLn (compare (Four, Four) (Four, Three)) >>> printLn - (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf)); + (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf)) + >>> printLn + (compare + (node (node leaf One leaf) Four leaf) + (node (node leaf One leaf) Two leaf)) + >>> printLn + (compare + (node (node leaf One leaf) Four leaf) + (node (node leaf One leaf) Four leaf));