Squashed commit of the following:

commit 267b34a Author: Jan Mas Rovira <[email protected]> Date: Wed Nov 20 14:18:11 2024 +0100 give proper name of builtins commit d0dc415 Author: Jan Mas Rovira <[email protected]> Date: Wed Nov 20 14:09:37 2024 +0100 better error message commit ccd9044 Author: Jan Mas Rovira <[email protected]> Date: Wed Nov 20 11:27:05 2024 +0100 allow implicit args commit 768f45d Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 18:44:50 2024 +0100 stdlib commit e778aaf Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 18:29:00 2024 +0100 clean commit 17939c7 Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 18:27:22 2024 +0100 update stdlib commit 46d7388 Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 18:18:22 2024 +0100 pragmas commit 58d1063 Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 18:09:23 2024 +0100 do not group deriving statements commit 057fdbb Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 15:14:31 2024 +0100 default case commit d280fe7 Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 14:55:36 2024 +0100 fix commit e3a7a76 Author: Jan Mas Rovira <[email protected]> Date: Tue Nov 19 09:57:22 2024 +0100 from concrete commit f8fd9f4 Author: Jan Mas Rovira <[email protected]> Date: Mon Nov 18 18:45:20 2024 +0100 refactor Fail commit a889cb6 Author: Jan Mas Rovira <[email protected]> Date: Mon Nov 18 18:00:27 2024 +0100 wip commit 734f7c1 Author: Jan Mas Rovira <[email protected]> Date: Mon Nov 18 13:00:14 2024 +0100 wip commit 6a2d7d2 Author: Jan Mas Rovira <[email protected]> Date: Fri Nov 15 13:29:44 2024 +0100 parsing and printing deriving kw commit 412a654 Author: Jan Mas Rovira <[email protected]> Date: Fri Nov 15 12:52:11 2024 +0100 add deriving kw commit 1101462 Author: Jan Mas Rovira <[email protected]> Date: Fri Nov 15 12:51:18 2024 +0100 style commit 3aeec44 Author: Jan Mas Rovira <[email protected]> Date: Thu Nov 14 17:39:09 2024 +0100 remove section titles from parser commit 15ec17d Author: Jan Mas Rovira <[email protected]> Date: Thu Nov 14 15:29:57 2024 +0100 update stdlib commit 546b5b2 Author: Jan Mas Rovira <[email protected]> Date: Thu Nov 14 11:27:04 2024 +0100 make Eq builtin commit 8658420 Author: Paul Cadman <[email protected]> Date: Wed Nov 20 07:53:21 2024 +0000 Support running nockma code with a running Anoma client (#3180) This PR: 1. Adds a new interpretation for the Anoma effect, which makes gRPC calls to an existing Anoma client instead of spawning a new one. 2. Adds a new `nockma run` mode, `with-client`, which can be used to run an Anoma program against a running Anoma client, using its URL and gRPC port. 3. separates the `nockma run` command into subcommands. CLI docs: ## `nockma run` ``` Usage: juvix dev nockma run COMMAND Subcommands used to run an Anoma program. Use with artefacts obtained from compilation with the anoma target Available options: -h,--help Show this help text Available commands: builtin-evaluator Run with the builtin Nockma evaluator ephemeral-client Run with an ephemeral Anoma client with-client Run with a running Anoma client ``` ### `with-client` ``` Usage: juvix dev nockma run with-client NOCKMA_FILE [--args ARGS_FILE] (-p|--grpc-port PORT) [--url URL] Run with a running Anoma client Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). -p,--grpc-port PORT The GRPC port of a running Anoma client --url URL The URL of a running Anoma client. default: localhost -h,--help Show this help text ``` ### `ephemeral-client` ``` Usage: juvix dev nockma run ephemeral-client NOCKMA_FILE [--args ARGS_FILE] --anoma-dir ANOMA_DIR Run with an ephemeral Anoma client Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). --anoma-dir ANOMA_DIR Path to anoma repository -h,--help Show this help text ``` ### `builtin-evaluator` ``` Usage: juvix dev nockma run builtin-evaluator NOCKMA_FILE [--args ARGS_FILE] [--profile] Run with the builtin Nockma evaluator Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). --profile Report evaluator profiling statistics -h,--help Show this help text ``` commit 455249d Author: Łukasz Czajka <[email protected]> Date: Tue Nov 19 20:34:52 2024 +0100 HTML generation: make the light theme lighter (#3168) * Closes #3141 * Adds the `latte-light` theme with lighter background and makes it the default. This is a bit subjective, but in my opinion the light theme should not have a background darker than the browser window pane. It should be close to white. commit eab02a7 Author: Paul Cadman <[email protected]> Date: Tue Nov 19 17:34:13 2024 +0000 Remove `GetAnomaProcess` from the Anoma effect (#3179) This PR removes `GetAnomaProcess` from the Anoma effect. Use the `launchAnoma` function to start a persistent Anoma client / server (used by `juvix dev anoma node`). Other changes: * It's no longer necessary to pass the protobuf files to `grpcurl` because the Anoma client now supports gRPC reflection. * We pass the elixir start command to `mix` via `-e` argument instead of using a temporary file. The purpose for this change is that we I want to add an interpreter for Anoma that makes gRPC calls to an exisitng Anoma client. `GetAnomaProcess` has no meaning for this interpreter.
anoma · Nov 20, 2024 · 84ad004 · 84ad004
1 parent 19ecfa9
commit 84ad004
Show file tree

Hide file tree

Showing 36 changed files with 890 additions and 301 deletions.
diff --git a/juvix-stdlib b/juvix-stdlib
diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
@@ -423,6 +423,7 @@ goStatement = \case
   StatementInductive t -> goInductive t
   StatementOpenModule t -> goOpen t
   StatementFunctionDef t -> goFunctionDef t
+  StatementDeriving t -> goDeriving t
   StatementSyntax syn -> goSyntax syn
   StatementImport t -> goImport t
   StatementModule m -> goLocalModule m
@@ -537,13 +538,15 @@ goAxiom axiom = do
     axiomHeader :: Sem r Html
     axiomHeader = ppCodeHtml defaultOptions (set axiomDoc Nothing axiom)
 
+goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
+goDeriving def = do
+  sig <- ppHelper (ppCode def)
+  defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing
+
 goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
 goFunctionDef def = do
-  sig' <- funSig
-  defHeader (def ^. signName) sig' (def ^. signDoc)
-  where
-    funSig :: Sem r Html
-    funSig = ppHelper (ppCode (functionDefLhs def))
+  sig <- ppHelper (ppCode (functionDefLhs def))
+  defHeader (def ^. signName) sig (def ^. signDoc)
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do

diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
@@ -213,12 +213,13 @@ indModuleFilter :: forall s. [Concrete.Statement s] -> [Concrete.Statement s]
 indModuleFilter =
   filter
     ( \case
-        Concrete.StatementSyntax _ -> True
-        Concrete.StatementFunctionDef _ -> True
-        Concrete.StatementImport _ -> True
-        Concrete.StatementInductive _ -> True
         Concrete.StatementModule o -> o ^. Concrete.moduleOrigin == LocalModuleSource
-        Concrete.StatementOpenModule _ -> True
-        Concrete.StatementAxiom _ -> True
-        Concrete.StatementProjectionDef _ -> True
+        Concrete.StatementSyntax {} -> True
+        Concrete.StatementFunctionDef {} -> True
+        Concrete.StatementDeriving {} -> True
+        Concrete.StatementImport {} -> True
+        Concrete.StatementInductive {} -> True
+        Concrete.StatementOpenModule {} -> True
+        Concrete.StatementAxiom {} -> True
+        Concrete.StatementProjectionDef {} -> True
     )
diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
@@ -1,6 +1,7 @@
 module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
+    module Juvix.Compiler.Builtins.Eq,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
@@ -24,6 +25,7 @@ import Juvix.Compiler.Builtins.ByteArray
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
+import Juvix.Compiler.Builtins.Eq
 import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int

diff --git a/src/Juvix/Compiler/Builtins/Eq.hs b/src/Juvix/Compiler/Builtins/Eq.hs
@@ -0,0 +1,25 @@
+module Juvix.Compiler.Builtins.Eq where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+checkEqDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkEqDef d = do
+  let err :: forall a. Text -> Sem r a
+      err = builtinsErrorText (getLoc d)
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "Lists should be in the small universe")
+  let eqTxt = prettyText BuiltinEq
+  case d ^. inductiveParameters of
+    [_] -> return ()
+    _ -> err (eqTxt <> "should have exactly one type parameter")
+  case d ^. inductiveConstructors of
+    [c1] -> checkMkEq c1
+    _ -> err (eqTxt <> "should have exactly two constructors")
+
+checkMkEq :: ConstructorDef -> Sem r ()
+checkMkEq _ = return ()
+
+checkIsEq :: FunctionDef -> Sem r ()
+checkIsEq _ = return ()
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -59,6 +59,7 @@ builtinConstructors = \case
   BuiltinEcPoint -> [BuiltinMkEcPoint]
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
+  BuiltinEq -> [BuiltinMkEq]
 
 data BuiltinInductive
   = BuiltinNat
@@ -67,6 +68,7 @@ data BuiltinInductive
   | BuiltinList
   | BuiltinMaybe
   | BuiltinPair
+  | BuiltinEq
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
@@ -87,6 +89,7 @@ instance Pretty BuiltinInductive where
     BuiltinList -> Str.list
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
+    BuiltinEq -> Str.eq
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
@@ -109,6 +112,7 @@ instance Pretty BuiltinConstructor where
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
+    BuiltinMkEq -> Str.mkEq
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -119,6 +123,7 @@ data BuiltinConstructor
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
+  | BuiltinMkEq
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr
@@ -161,6 +166,7 @@ data BuiltinFunction
   | BuiltinIntLe
   | BuiltinIntLt
   | BuiltinFromNat
+  | BuiltinIsEqual
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -202,6 +208,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
+    BuiltinIsEqual -> Str.isEqual
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -434,6 +441,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
@@ -486,13 +494,15 @@ isIntBuiltin = \case
   BuiltinFromNat -> False
   BuiltinFromInt -> False
   BuiltinSeq -> False
+  BuiltinIsEqual -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
@@ -532,6 +542,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
+        .&&. (/= BuiltinIsEqual)
         $ f
 
     explicit :: Bool
@@ -562,6 +573,8 @@ isIgnoredBuiltin f
       BuiltinNatLe -> False
       BuiltinNatLt -> False
       BuiltinNatEq -> False
+      -- Eq
+      BuiltinIsEqual -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored

diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
@@ -28,7 +28,7 @@ data InfoTableBuilder :: Effect where
   RegisterRecordInfo :: S.NameId -> RecordInfo -> InfoTableBuilder m ()
   RegisterAlias :: S.NameId -> PreSymbolEntry -> InfoTableBuilder m ()
   RegisterLocalModule :: ScopedModule -> InfoTableBuilder m ()
-  GetInfoTable :: InfoTableBuilder m InfoTable
+  GetBuilderInfoTable :: InfoTableBuilder m InfoTable
   GetBuiltinSymbol' :: Interval -> BuiltinPrim -> InfoTableBuilder m S.Symbol
   RegisterBuiltin' :: BuiltinPrim -> S.Symbol -> InfoTableBuilder m ()
 
@@ -92,7 +92,7 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
     modify (over infoScoperAlias (HashMap.insert uid a))
   RegisterLocalModule m ->
     mapM_ (uncurry registerBuiltinHelper) (m ^. scopedModuleInfoTable . infoBuiltins . to HashMap.toList)
-  GetInfoTable ->
+  GetBuilderInfoTable ->
     get
   GetBuiltinSymbol' i b -> do
     tbl <- get @InfoTable
@@ -153,16 +153,22 @@ anameFromScopedIden s =
       _anameVerbatim = s ^. scopedIdenSrcName . nameVerbatim
     }
 
-lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a
+getInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a
+getInfo f = do
+  tab1 <- ask
+  fromMaybe (fromJust (f tab1)) . f <$> getBuilderInfoTable
+
+lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r (Maybe a)
 lookupInfo f = do
   tab1 <- ask
-  fromMaybe (fromJust (f tab1)) . f <$> getInfoTable
+  tab2 <- getBuilderInfoTable
+  return (f tab1 <|> f tab2)
 
 lookupFixity :: (Members '[InfoTableBuilder, Reader InfoTable] r) => S.NameId -> Sem r FixityDef
-lookupFixity uid = lookupInfo (HashMap.lookup uid . (^. infoFixities))
+lookupFixity uid = getInfo (^. infoFixities . at uid)
 
 getPrecedenceGraph :: (Members '[InfoTableBuilder, Reader InfoTable] r) => Sem r PrecedenceGraph
 getPrecedenceGraph = do
   tab <- ask
-  tab' <- getInfoTable
+  tab' <- getBuilderInfoTable
   return $ combinePrecedenceGraphs (tab ^. infoPrecedenceGraph) (tab' ^. infoPrecedenceGraph)
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
@@ -63,8 +63,13 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where
   addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
   addArgs a = addArgs (a ^. axiomTypeSig)
 
+instance (SingI s) => HasNameSignature s (FunctionLhs s) where
+  addArgs a = do
+    mapM_ addSigArg (a ^. funLhsArgs)
+    whenJust (a ^. funLhsRetType) addExpressionType
+
 instance (SingI s) => HasNameSignature s (FunctionDef s) where
-  addArgs a = addArgs (a ^. signTypeSig)
+  addArgs = addArgs . functionDefLhs
 
 instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
   addArgs ::

diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs
@@ -9,6 +9,7 @@ module Juvix.Compiler.Concrete.Extra
     getPatternAtomIden,
     isBodyExpression,
     isFunctionLike,
+    isLhsFunctionLike,
     symbolParsed,
   )
 where
@@ -46,6 +47,7 @@ groupStatements = \case
     -- blank line
     g :: Statement s -> Statement s -> Bool
     g a b = case (a, b) of
+      (StatementDeriving _, _) -> False
       (StatementSyntax _, StatementSyntax _) -> True
       (StatementSyntax (SyntaxFixity _), _) -> False
       (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s
@@ -108,6 +110,9 @@ isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
 
-isFunctionLike :: FunctionDef a -> Bool
-isFunctionLike = \case
-  FunctionDef {..} -> not (null (_signTypeSig ^. typeSigArgs)) || not (isBodyExpression _signBody)
+isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool
+isLhsFunctionLike FunctionLhs {..} = notNull _funLhsArgs
+
+isFunctionLike :: FunctionDef 'Parsed -> Bool
+isFunctionLike d@FunctionDef {..} =
+  isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody
diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs
@@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All
     kwCase,
     kwCoercion,
     kwColon,
+    kwDeriving,
     kwDo,
     kwElse,
     kwEnd,
@@ -85,6 +86,7 @@ reservedKeywords :: [Keyword]
 reservedKeywords =
   [ delimSemicolon,
     kwAssign,
+    kwDeriving,
     kwAt,
     kwAtQuestion,
     kwAxiom,

diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
@@ -31,6 +31,7 @@ statementLabel = \case
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
   StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
+  StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
   StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
   StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
   StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel)