wip

Author: janmasrovira

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -280,6 +280,8 @@ data BuiltinAxiom
   | BuiltinAnomaRandomSplit
   | BuiltinAnomaIsCommitment
   | BuiltinAnomaIsNullifier
+  | BuiltinAnomaActionCreate
+  | BuiltinAnomaTransactionCompose
   | BuiltinAnomaSet
   | BuiltinAnomaSetToList
   | BuiltinAnomaSetFromList
@@ -350,6 +352,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaRandomSplit -> KNameFunction
     BuiltinAnomaIsCommitment -> KNameFunction
     BuiltinAnomaIsNullifier -> KNameFunction
+    BuiltinAnomaActionCreate -> KNameFunction
+    BuiltinAnomaTransactionCompose -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -427,6 +431,8 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaRandomSplit -> Str.anomaRandomSplit
     BuiltinAnomaIsCommitment -> Str.anomaIsCommitment
     BuiltinAnomaIsNullifier -> Str.anomaIsNullifier
+    BuiltinAnomaTransactionCompose -> Str.anomaTransactionCompose
+    BuiltinAnomaActionCreate -> Str.anomaActionCreate
     BuiltinAnomaSet -> Str.anomaSet
     BuiltinAnomaSetToList -> Str.anomaSetToList
     BuiltinAnomaSetFromList -> Str.anomaSetFromList

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -703,6 +703,8 @@ builtinInductive a =
         Internal.BuiltinAnomaRandomSplit -> Nothing
         Internal.BuiltinAnomaIsCommitment -> Nothing
         Internal.BuiltinAnomaIsNullifier -> Nothing
+        Internal.BuiltinAnomaActionCreate -> Nothing
+        Internal.BuiltinAnomaTransactionCompose -> Nothing
         Internal.BuiltinAnomaSet -> Just (registerInductiveAxiom (Just BuiltinAnomaSet) [])
         Internal.BuiltinAnomaSetToList -> Nothing
         Internal.BuiltinAnomaSetFromList -> Nothing
@@ -1039,6 +1041,22 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               natType
               (mkBuiltinApp' OpAnomaIsCommitment [mkVar' 0])
           )
+      Internal.BuiltinAnomaActionCreate -> do
+        registerAxiomDef
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          $ mkBuiltinApp' OpAnomaActionCreate [mkVar' 2, mkVar' 1, mkVar' 0]
+      Internal.BuiltinAnomaTransactionCompose -> do
+        registerAxiomDef
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          $ mkBuiltinApp' OpAnomaTransactionCompose [mkVar' 1, mkVar' 0]
       Internal.BuiltinAnomaIsNullifier -> do
         natType <- getNatType
         registerAxiomDef
@@ -1518,6 +1536,8 @@ goApplication a = do
         Just Internal.BuiltinAnomaRandomSplit -> app
         Just Internal.BuiltinAnomaIsCommitment -> app
         Just Internal.BuiltinAnomaIsNullifier -> app
+        Just Internal.BuiltinAnomaTransactionCompose -> app
+        Just Internal.BuiltinAnomaActionCreate -> app
         Just Internal.BuiltinAnomaSet -> app
         Just Internal.BuiltinAnomaSetToList -> app
         Just Internal.BuiltinAnomaSetFromList -> app

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -147,6 +147,8 @@ fromCore' tab =
         BuiltinAnomaRandomSplit -> False
         BuiltinAnomaIsCommitment -> False
         BuiltinAnomaIsNullifier -> False
+        BuiltinAnomaTransactionCompose -> False
+        BuiltinAnomaActionCreate -> False
         BuiltinAnomaSet -> False
         BuiltinAnomaSetToList -> False
         BuiltinAnomaSetFromList -> False

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -1081,6 +1081,8 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d
   BuiltinAnomaIsCommitment -> checkAnomaIsCommitment d
   BuiltinAnomaIsNullifier -> checkAnomaIsNullifier d
+  BuiltinAnomaActionCreate -> return ()
+  BuiltinAnomaTransactionCompose -> return ()
   BuiltinAnomaSet -> checkAnomaSet d
   BuiltinAnomaSetToList -> checkAnomaSetToList d
   BuiltinAnomaSetFromList -> checkAnomaSetFromList d

test/Anoma.hs

@@ -8,6 +8,6 @@ allTests :: TestTree
 allTests =
   testGroup
     "Anoma tests"
-    [ Compilation.allTests,
-      Client.allTests
+    [ Compilation.allTests
+    -- Client.allTests
     ]