From 64cbb454dabe05b656fd56bd88b4132c20e7db57 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 3 Feb 2025 23:08:02 +0100 Subject: [PATCH] Allow named arguments for some anoma builtins (#3310) Use expression equivalence to match the expected type of anoma builtins --- src/Juvix/Compiler/Builtins/Anoma.hs | 12 ++++++------ src/Juvix/Compiler/Internal/Extra/Base.hs | 3 +++ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 2ff184f82e..9339e443dc 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -95,7 +95,7 @@ checkAnomaByteArrayToAnomaContents f = do byteArray <- getBuiltinNameScoper l BuiltinByteArray nat_ <- getBuiltinNameScoper l BuiltinNat unless - (ftype == (byteArray --> nat_)) + (ftype === (byteArray --> nat_)) $ builtinsErrorText l "toAnomaContents must be of type ByteArray -> Nat" checkAnomaByteArrayFromAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () @@ -105,7 +105,7 @@ checkAnomaByteArrayFromAnomaContents f = do byteArray <- getBuiltinNameScoper l BuiltinByteArray nat_ <- getBuiltinNameScoper l BuiltinNat unless - (ftype == (nat_ --> nat_ --> byteArray)) + (ftype === (nat_ --> nat_ --> byteArray)) $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray" checkAnomaSha256 :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () @@ -115,7 +115,7 @@ checkAnomaSha256 f = do byteArray <- getBuiltinNameScoper l BuiltinByteArray nat_ <- getBuiltinNameScoper l BuiltinNat unless - (ftype == (nat_ --> byteArray)) + (ftype === (nat_ --> byteArray)) $ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray" checkResource :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () @@ -257,7 +257,7 @@ checkAnomaIsCommitment f = do let l = getLoc f nat_ <- getBuiltinNameScoper l BuiltinNat bool_ <- getBuiltinNameScoper l BuiltinBool - unless (f ^. axiomType == (nat_ --> bool_)) $ + unless (f ^. axiomType === (nat_ --> bool_)) $ builtinsErrorText l "isCommitment must be of type Nat -> Bool" checkAnomaIsNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () @@ -265,7 +265,7 @@ checkAnomaIsNullifier f = do let l = getLoc f nat_ <- getBuiltinNameScoper l BuiltinNat bool_ <- getBuiltinNameScoper l BuiltinBool - unless (f ^. axiomType == (nat_ --> bool_)) $ + unless (f ^. axiomType === (nat_ --> bool_)) $ builtinsErrorText l "isNullifier must be of type Nat -> Bool" checkAnomaSet :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r () @@ -273,7 +273,7 @@ checkAnomaSet t = do let ty = t ^. axiomType l = getLoc t u = ExpressionUniverse smallUniverseNoLoc - unless (ty == (u --> u)) $ + unless (ty === (u --> u)) $ builtinsErrorText l "AnomaSet should have type: Type -> Type" checkAnomaSetToList :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index f8a3c4f930..a2b6f0ca91 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -711,6 +711,7 @@ matchExpressions = go -- Soft free vars are allowed to be matched isSoftFreeVar :: VarName -> Sem r Bool isSoftFreeVar = asks . HashSet.member + go :: Expression -> Expression -> Sem r () go a b = case (a, b) of (ExpressionIden ia, ExpressionIden ib) -> case (ia, ib) of @@ -805,8 +806,10 @@ matchFunctionParameter pa pb = do where goParamType :: Expression -> Expression -> Sem r () goParamType ua ub = matchExpressions ua ub + goParamImplicit :: IsImplicit -> IsImplicit -> Sem r () goParamImplicit ua ub = unless (ua == ub) (throw @Text "implicit mismatch") + goParamName :: Maybe VarName -> Maybe VarName -> Sem r () goParamName (Just va) (Just vb) = addName va vb goParamName _ _ = return ()