From ea89ff65e687c9e37bfe1c0be79e4a7661e24dcd Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Thu, 21 Jun 2018 14:38:38 +0300 Subject: [PATCH 01/10] Function evaluation --- .../src/Data/Kore/AST/MLPatterns.hs | 60 ++-- .../language-kore/src/Data/Kore/AST/PureML.hs | 26 ++ .../Data/Kore/ASTVerifier/PatternVerifier.hs | 5 +- .../Data/Kore/IndexedModule/MetadataTools.hs | 2 + .../src/Data/Kore/Step/Condition/Condition.hs | 107 +++++++ .../src/Data/Kore/Step/Condition/Evaluator.hs | 127 +++++++++ .../src/Data/Kore/Step/Function/Data.hs | 50 ++++ .../src/Data/Kore/Step/Function/Evaluator.hs | 267 ++++++++++++++++++ .../Data/Kore/Step/Function/UserDefined.hs | 162 +++++++++++ .../src/Data/Kore/Unparser/Unparse.hs | 12 +- .../src/Data/Kore/Variables/Sort.hs | 2 +- .../test/parser/AllParserTests.hs | 2 + .../test/parser/Data/Kore/Comparators.hs | 93 +++++- .../parser/Data/Kore/Step/BaseStepTest.hs | 1 + .../test/parser/Data/Kore/Step/StepTest.hs | 1 + .../Data/Kore/Unification/UnifierTest.hs | 3 +- 16 files changed, 887 insertions(+), 33 deletions(-) create mode 100644 src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs create mode 100644 src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs create mode 100644 src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs create mode 100644 src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs create mode 100644 src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs diff --git a/src/main/haskell/language-kore/src/Data/Kore/AST/MLPatterns.hs b/src/main/haskell/language-kore/src/Data/Kore/AST/MLPatterns.hs index f6782e94c5..2a8b89cbf1 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/AST/MLPatterns.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/AST/MLPatterns.hs @@ -1,6 +1,8 @@ -{-# LANGUAGE ExplicitForAll #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} {-| Module : Data.Kore.MLPatterns Description : Data structures and functions for handling patterns uniformly. @@ -27,13 +29,14 @@ import Data.Kore.Implicit.ImplicitSorts {-|'MLPatternClass' offers a common interface to ML patterns (those starting with '\', except for 'Exists' and 'Forall') -} -class MLPatternClass pat where +class MLPatternClass pat level where getPatternType :: pat level child -> MLPatternType getMLPatternOperandSorts :: MetaOrObject level => pat level child -> [UnifiedSort] getMLPatternResultSort :: pat level child -> Sort level getPatternSorts :: pat level child -> [Sort level] getPatternChildren :: pat level child -> [child] + mlPatternToPattern :: pat level child -> Pattern level variable child {-|'MLBinderPatternClass' offers a common interface to the 'Exists' and 'Forall' ML patterns. @@ -49,108 +52,123 @@ class MLBinderPatternClass pat where :: MetaOrObject level => pat level variable child -> Sort level -> variable level -> child -> Pattern level variable child + mlBinderPatternToPattern :: pat level variable child -> Pattern level variable child -instance MLPatternClass And where +instance MLPatternClass And level where getPatternType _ = AndPatternType getMLPatternOperandSorts x = [asUnified (andSort x), asUnified (andSort x)] getMLPatternResultSort = andSort getPatternSorts a = [andSort a] getPatternChildren a = [andFirst a, andSecond a] + mlPatternToPattern = AndPattern -instance MLPatternClass Bottom where +instance MLPatternClass Bottom level where getPatternType _ = BottomPatternType getMLPatternOperandSorts _ = [] getMLPatternResultSort = bottomSort getPatternSorts t = [bottomSort t] getPatternChildren _ = [] + mlPatternToPattern = BottomPattern -instance MLPatternClass Ceil where +instance MLPatternClass Ceil level where getPatternType _ = CeilPatternType getMLPatternOperandSorts x = [asUnified (ceilOperandSort x)] getMLPatternResultSort = ceilResultSort getPatternSorts c = [ceilOperandSort c, ceilResultSort c] getPatternChildren c = [ceilChild c] + mlPatternToPattern = CeilPattern -instance MLPatternClass DomainValue where +instance MLPatternClass DomainValue Object where getPatternType _ = DomainValuePatternType getMLPatternOperandSorts _ = [asUnified charListMetaSort] getMLPatternResultSort = domainValueSort getPatternSorts d = [domainValueSort d] getPatternChildren d = [domainValueChild d] + mlPatternToPattern = DomainValuePattern -instance MLPatternClass Equals where +instance MLPatternClass Equals level where getPatternType _ = EqualsPatternType getMLPatternOperandSorts x = [asUnified (equalsOperandSort x), asUnified (equalsOperandSort x)] getMLPatternResultSort = equalsResultSort getPatternSorts e = [equalsOperandSort e, equalsResultSort e] getPatternChildren e = [equalsFirst e, equalsSecond e] + mlPatternToPattern = EqualsPattern -instance MLPatternClass Floor where +instance MLPatternClass Floor level where getPatternType _ = FloorPatternType getMLPatternOperandSorts x = [asUnified (floorOperandSort x)] getMLPatternResultSort = floorResultSort getPatternSorts f = [floorOperandSort f, floorResultSort f] getPatternChildren f = [floorChild f] + mlPatternToPattern = FloorPattern -instance MLPatternClass Iff where +instance MLPatternClass Iff level where getPatternType _ = IffPatternType getMLPatternOperandSorts x = [asUnified (iffSort x), asUnified (iffSort x)] getMLPatternResultSort = iffSort getPatternSorts i = [iffSort i] getPatternChildren i = [iffFirst i, iffSecond i] + mlPatternToPattern = IffPattern -instance MLPatternClass Implies where +instance MLPatternClass Implies level where getPatternType _ = ImpliesPatternType getMLPatternOperandSorts x = [asUnified (impliesSort x), asUnified (impliesSort x)] getMLPatternResultSort = impliesSort getPatternSorts i = [impliesSort i] getPatternChildren i = [impliesFirst i, impliesSecond i] + mlPatternToPattern = ImpliesPattern -instance MLPatternClass In where +instance MLPatternClass In level where getPatternType _ = InPatternType getMLPatternOperandSorts x = [asUnified (inOperandSort x), asUnified (inOperandSort x)] getMLPatternResultSort = inResultSort getPatternSorts i = [inOperandSort i, inResultSort i] getPatternChildren i = [inContainedChild i, inContainingChild i] + mlPatternToPattern = InPattern -instance MLPatternClass Next where +instance MLPatternClass Next Object where getPatternType _ = NextPatternType getMLPatternOperandSorts x = [asUnified (nextSort x)] getMLPatternResultSort = nextSort getPatternSorts e = [nextSort e] getPatternChildren e = [nextChild e] + mlPatternToPattern = NextPattern -instance MLPatternClass Not where +instance MLPatternClass Not level where getPatternType _ = NotPatternType getMLPatternOperandSorts x = [asUnified (notSort x)] getMLPatternResultSort = notSort getPatternSorts n = [notSort n] getPatternChildren n = [notChild n] + mlPatternToPattern = NotPattern -instance MLPatternClass Or where +instance MLPatternClass Or level where getPatternType _ = OrPatternType getMLPatternOperandSorts x = [asUnified (orSort x), asUnified (orSort x)] getMLPatternResultSort = orSort getPatternSorts a = [orSort a] getPatternChildren a = [orFirst a, orSecond a] + mlPatternToPattern = OrPattern -instance MLPatternClass Rewrites where +instance MLPatternClass Rewrites Object where getPatternType _ = RewritesPatternType getMLPatternOperandSorts x = [asUnified (rewritesSort x), asUnified (rewritesSort x)] getMLPatternResultSort = rewritesSort getPatternSorts e = [rewritesSort e] getPatternChildren e = [rewritesFirst e, rewritesSecond e] + mlPatternToPattern = RewritesPattern -instance MLPatternClass Top where +instance MLPatternClass Top level where getPatternType _ = TopPatternType getMLPatternOperandSorts _ = [] getMLPatternResultSort = topSort getPatternSorts t = [topSort t] getPatternChildren _ = [] + mlPatternToPattern = TopPattern instance MLBinderPatternClass Exists where getBinderPatternType _ = ExistsPatternType @@ -162,6 +180,7 @@ instance MLBinderPatternClass Exists where , existsVariable = variable , existsChild = pat } + mlBinderPatternToPattern = ExistsPattern instance MLBinderPatternClass Forall where getBinderPatternType _ = ForallPatternType @@ -173,6 +192,7 @@ instance MLBinderPatternClass Forall where , forallVariable = variable , forallChild = pat } + mlBinderPatternToPattern = ForallPattern {-|`PatternLeveledFunction` holds a full set of functions that can be applied to the elements of a `Pattern` (e.g. `Implies`). Together @@ -181,7 +201,7 @@ with `applyPatternLeveledFunction` they form a function on patterns, hence the n -- TODO: consider parameterizing on variable also data PatternLeveledFunction level variable child result = PatternLeveledFunction { patternLeveledFunctionML - :: !(forall patt . MLPatternClass patt + :: !(forall patt . MLPatternClass patt level => patt level child -> result level) , patternLeveledFunctionMLBinder :: !(forall patt . MLBinderPatternClass patt @@ -248,7 +268,7 @@ with `applyPatternFunction` they form a function on patterns, hence the name. -- TODO: consider parameterizing on variable also data PatternFunction level variable child result = PatternFunction { patternFunctionML - :: !(forall patt . MLPatternClass patt => patt level child -> result) + :: !(forall patt . MLPatternClass patt level => patt level child -> result) , patternFunctionMLBinder :: !(forall patt . MLBinderPatternClass patt => patt level variable child diff --git a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs index 1dfb056012..33e0478952 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs @@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeSynonymInstances #-} {-| Module : Data.Kore.AST.PureML @@ -32,6 +33,30 @@ asPurePattern :: Pattern level var (PureMLPattern level var) -> PureMLPattern level var asPurePattern = Fix +fromPurePattern + :: PureMLPattern level var -> Pattern level var (PureMLPattern level var) +fromPurePattern (Fix p) = p + +{- +pattern PureMLAnd p <- Fix (PatternAnd p) +pattern PureMLApplication p <- Fix (PatternApplication p) +pattern PureMLBottom p <- Fix (PatternBottom p) +pattern PureMLCeil p <- Fix (PatternCeil p) +pattern PureMLDomainValue p <- Fix (PatternDomainValue p) +pattern PureMLEquals p <- Fix (PatternEquals p) +pattern PureMLExists p <- Fix (PatternExists p) +pattern PureMLForall p <- Fix (PatternForall p) +pattern PureMLIff p <- Fix (PatternIff p) +pattern PureMLImplies p <- Fix (PatternImplies p) +pattern PureMLIn p <- Fix (PatternIn p) +pattern PureMLNext p <- Fix (PatternNext p) +pattern PureMLNot p <- Fix (PatternNot p) +pattern PureMLOr p <- Fix (PatternOr p) +pattern PureMLRewrites p <- Fix (PatternRewrites p) +pattern PureMLTop p <- Fix (PatternTop p) +and so on +-} + -- |'PureSentenceAxiom' is the pure (fixed-@level@) version of 'SentenceAxiom' type PureSentenceAxiom level = SentenceAxiom (SortVariable level) (Pattern level) Variable @@ -102,6 +127,7 @@ constant patternHead = apply patternHead [] type CommonPurePattern level = PureMLPattern level Variable type UnFixedPureMLPattern level variable = Pattern level variable (PureMLPattern level variable) +type UnfixedCommonPurePattern level = UnFixedPureMLPattern level Variable type PurePatternStub level variable = PatternStub level variable (PureMLPattern level variable) diff --git a/src/main/haskell/language-kore/src/Data/Kore/ASTVerifier/PatternVerifier.hs b/src/main/haskell/language-kore/src/Data/Kore/ASTVerifier/PatternVerifier.hs index b8bac9e24f..a23e4d3b0b 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/ASTVerifier/PatternVerifier.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/ASTVerifier/PatternVerifier.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-| Module : Data.Kore.ASTVerifier.PatternVerifier Description : Tools for verifying the wellformedness of a Kore 'Pattern'. @@ -252,7 +253,7 @@ verifyParameterizedPattern pat indexedModule helpers sortParams vars = pat verifyMLPattern - :: (MLPatternClass p, MetaOrObject level) + :: (MLPatternClass p level, MetaOrObject level) => p level CommonKorePattern -> KoreIndexedModule -> VerifyHelpers level diff --git a/src/main/haskell/language-kore/src/Data/Kore/IndexedModule/MetadataTools.hs b/src/main/haskell/language-kore/src/Data/Kore/IndexedModule/MetadataTools.hs index fd2c0fabd4..41286eaef2 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/IndexedModule/MetadataTools.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/IndexedModule/MetadataTools.hs @@ -27,6 +27,7 @@ import Data.Kore.IndexedModule.Resolvers data MetadataTools level = MetadataTools { isConstructor :: SymbolOrAlias level -> Bool , isFunctional :: SymbolOrAlias level -> Bool + , isFunction :: SymbolOrAlias level -> Bool , getArgumentSorts :: SymbolOrAlias level -> [Sort level] , getResultSort :: SymbolOrAlias level -> Sort level } @@ -48,6 +49,7 @@ extractMetadataTools m = MetadataTools { isConstructor = hasAttribute constructorAttribute , isFunctional = hasAttribute functionalAttribute + , isFunction = error "Not implemented." , getArgumentSorts = applicationSortsOperands . getHeadApplicationSorts m , getResultSort = applicationSortsResult . getHeadApplicationSorts m } diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs new file mode 100644 index 0000000000..67e6ca5586 --- /dev/null +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs @@ -0,0 +1,107 @@ +{-| +Module : Data.Kore.Step.Condition.Condition +Description : Data structure holding a condition. +Copyright : (c) Runtime Verification, 2018 +License : UIUC/NCSA +Maintainer : virgil.serbanuta@runtimeverification.com +Stability : experimental +Portability : portable +-} +module Data.Kore.Step.Condition.Condition + ( EvaluatedCondition (..) + , UnevaluatedCondition (..) + , makeEvaluatedAnd + , makeEvaluatedIff + , makeEvaluatedImplies + , makeEvaluatedNot + , makeEvaluatedOr + , makeUnevaluatedAnd + ) where + +import Data.Kore.AST.Common (And (..), Iff (..), Implies (..), + Not (..), Or (..), Pattern (..), + Sort (..)) +import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern) + +-- TODO: Maybe rename +data EvaluatedCondition level + = ConditionTrue + | ConditionFalse + -- This should be changed to Satisfiable or something when adding + -- the SMT solver. When doing that, also change the make{And,Or,...} + -- functions to return somenthing that forces reevaluation. + | ConditionUnevaluable !(CommonPurePattern level) + deriving Show + +newtype UnevaluatedCondition level = + UnevaluatedCondition (CommonPurePattern level) + deriving Show + +makeEvaluatedAnd + :: Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level + -> EvaluatedCondition level +makeEvaluatedAnd _ ConditionFalse _ = ConditionFalse +makeEvaluatedAnd _ _ ConditionFalse = ConditionFalse +makeEvaluatedAnd _ ConditionTrue second = second +makeEvaluatedAnd _ first ConditionTrue = first +makeEvaluatedAnd sort (ConditionUnevaluable first) (ConditionUnevaluable second) = + ConditionUnevaluable $ asPurePattern $ AndPattern $ And sort first second + +-- TODO: Do I need this? +makeUnevaluatedAnd + :: Sort level + -> UnevaluatedCondition level + -> UnevaluatedCondition level + -> UnevaluatedCondition level +makeUnevaluatedAnd sort (UnevaluatedCondition first) (UnevaluatedCondition second) = + UnevaluatedCondition $ asPurePattern $ AndPattern $ And sort first second + + +makeEvaluatedOr + :: Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level + -> EvaluatedCondition level +makeEvaluatedOr _ ConditionTrue _ = ConditionTrue +makeEvaluatedOr _ _ ConditionTrue = ConditionTrue +makeEvaluatedOr _ ConditionFalse second = second +makeEvaluatedOr _ first ConditionFalse = first +makeEvaluatedOr sort (ConditionUnevaluable first) (ConditionUnevaluable second) = + ConditionUnevaluable $ asPurePattern $ OrPattern $ Or sort first second + +makeEvaluatedImplies + :: Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level + -> EvaluatedCondition level +-- TODO: Is it reasonable to use a different thing here? +makeEvaluatedImplies _ ConditionFalse _ = ConditionTrue +makeEvaluatedImplies _ _ ConditionTrue = ConditionTrue +makeEvaluatedImplies _ ConditionTrue second = second +makeEvaluatedImplies sort first ConditionFalse = makeEvaluatedNot sort first +makeEvaluatedImplies sort (ConditionUnevaluable first) (ConditionUnevaluable second) = + ConditionUnevaluable $ asPurePattern $ ImpliesPattern $ Implies sort first second + +makeEvaluatedIff + :: Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level + -> EvaluatedCondition level +-- TODO: Is it reasonable to use a different thing here? +makeEvaluatedIff sort ConditionFalse second = makeEvaluatedNot sort second +makeEvaluatedIff _ ConditionTrue second = second +makeEvaluatedIff sort first@(ConditionUnevaluable _) ConditionFalse = makeEvaluatedNot sort first +makeEvaluatedIff _ first@(ConditionUnevaluable _) ConditionTrue = first +makeEvaluatedIff sort (ConditionUnevaluable first) (ConditionUnevaluable second) = + ConditionUnevaluable $ asPurePattern $ IffPattern $ Iff sort first second + +makeEvaluatedNot + :: Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level +makeEvaluatedNot _ ConditionFalse = ConditionTrue +makeEvaluatedNot _ ConditionTrue = ConditionFalse +makeEvaluatedNot sort (ConditionUnevaluable condition) = + ConditionUnevaluable $ asPurePattern $ NotPattern $ Not sort condition diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs new file mode 100644 index 0000000000..d0869d9410 --- /dev/null +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE GADTs #-} +{-| +Module : Data.Kore.Step.Condition.Evaluator +Description : Evaluates conditions +Copyright : (c) Runtime Verification, 2018 +License : UIUC/NCSA +Maintainer : virgil.serbanuta@runtimeverification.com +Stability : experimental +Portability : portable +-} +module Data.Kore.Step.Condition.Evaluator + ( evaluateFunctionCondition + ) where + +import Data.Kore.AST.Common (And (..), Equals (..), + Iff (..), Implies (..), + Not (..), Or (..), + Pattern (..), Sort (..), + Variable) +import Data.Kore.AST.PureML (CommonPurePattern, + asPurePattern, + fromPurePattern) +import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), + UnevaluatedCondition (..), + makeEvaluatedAnd, + makeEvaluatedIff, + makeEvaluatedImplies, + makeEvaluatedNot, + makeEvaluatedOr) +import Data.Kore.Step.Function.Data (CommonPurePatternFunctionEvaluator (..), + FunctionResult (..)) +import Data.Kore.Variables.Fresh.IntCounter (IntCounter) + + +evaluateFunctionCondition + :: CommonPurePatternFunctionEvaluator level + -> Sort level + -> UnevaluatedCondition level + -> IntCounter (EvaluatedCondition level) +evaluateFunctionCondition + functionEvaluator + conditionSort + (UnevaluatedCondition condition) + = + evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (fromPurePattern condition) + +evaluateFunctionConditionInternal + :: CommonPurePatternFunctionEvaluator level + -> Sort level + -> Pattern level Variable (CommonPurePattern level) + -> IntCounter (EvaluatedCondition level) +evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (AndPattern And {andFirst = first, andSecond = second}) + = do + a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) + b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + return $ makeEvaluatedAnd conditionSort a b +evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (OrPattern Or {orFirst = first, orSecond = second}) + = do + a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) + b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + return $ makeEvaluatedOr conditionSort a b +evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (NotPattern Not {notChild = patt}) + = do + a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern patt) + return (makeEvaluatedNot conditionSort a) +evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (ImpliesPattern Implies {impliesFirst = first, impliesSecond = second}) + = do + a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) + b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + return $ makeEvaluatedImplies conditionSort a b +evaluateFunctionConditionInternal + functionEvaluator + conditionSort + (IffPattern Iff {iffFirst = first, iffSecond = second}) + = do + a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) + b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + return $ makeEvaluatedIff conditionSort a b +evaluateFunctionConditionInternal + (CommonPurePatternFunctionEvaluator functionEvaluator) + conditionSort + (EqualsPattern Equals {equalsFirst = first, equalsSecond = second}) + = do + firstValue <- functionEvaluator first + secondValue <- functionEvaluator second + let + FunctionResult + { functionResultPattern = firstPattern + , functionResultCondition = firstCondition + } = firstValue + FunctionResult + { functionResultPattern = secondPattern + -- TODO: Maybe Make two types of condition: functionResult and evaluated + , functionResultCondition = secondCondition + } = secondValue + -- TODO: This is more complex than implemented here, e.g. commutativity + -- may be an issue. + --firstCondition' <- firstCondition + --secondCondition' <- secondCondition + if firstPattern == secondPattern + -- TODO: this should probably call evaluateFunctionCondition + then return $ makeEvaluatedAnd conditionSort firstCondition secondCondition + else return ConditionFalse +evaluateFunctionConditionInternal + _ _ (TopPattern _) + = return ConditionTrue +evaluateFunctionConditionInternal + _ _ (BottomPattern _) + = return ConditionFalse +evaluateFunctionConditionInternal + _ _ patt + = return (ConditionUnevaluable (asPurePattern patt)) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs new file mode 100644 index 0000000000..4b5612d0a8 --- /dev/null +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs @@ -0,0 +1,50 @@ +{-| +Module : Data.Kore.Step.Function.Data +Description : Data structures used for function evaluation +Copyright : (c) Runtime Verification, 2018 +License : UIUC/NCSA +Maintainer : virgil.serbanuta@runtimeverification.com +Stability : experimental +Portability : portable +-} +module Data.Kore.Step.Function.Data + ( ApplicationFunctionEvaluator (..) + , CommonPurePatternFunctionEvaluator (..) + , ConditionEvaluator (..) + , FunctionResult (..) + , FunctionEvaluation (..) + ) where + +import Data.Kore.AST.Common (Application) +import Data.Kore.AST.PureML (CommonPurePattern) +import Data.Kore.Step.Condition.Condition (EvaluatedCondition, + UnevaluatedCondition) +import Data.Kore.Variables.Fresh.IntCounter (IntCounter) + +newtype CommonPurePatternFunctionEvaluator level = + CommonPurePatternFunctionEvaluator + (CommonPurePattern level -> IntCounter (FunctionResult level)) + +newtype ApplicationFunctionEvaluator level = + ApplicationFunctionEvaluator + ( ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Application level (CommonPurePattern level) + -> IntCounter (FunctionEvaluation level) + ) + +-- TODO: this should probably be replaced by a StepperConfiguration +data FunctionResult level = FunctionResult + { functionResultPattern :: !(CommonPurePattern level) + , functionResultCondition :: !(EvaluatedCondition level) + } + deriving Show + +data FunctionEvaluation level + = NotApplicable + | Symbolic !(EvaluatedCondition level) + | Applied !(FunctionResult level) + deriving Show + +newtype ConditionEvaluator level = ConditionEvaluator + (UnevaluatedCondition level -> IntCounter (EvaluatedCondition level)) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs new file mode 100644 index 0000000000..18cda7d8e5 --- /dev/null +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs @@ -0,0 +1,267 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-| +Module : Data.Kore.Step.Function.Evaluator +Description : Evaluates functions in a pattern +Copyright : (c) Runtime Verification, 2018 +License : UIUC/NCSA +Maintainer : virgil.serbanuta@runtimeverification.com +Stability : experimental +Portability : portable +-} +module Data.Kore.Step.Function.Evaluator + ( evaluateFunctions + ) where + +import qualified Data.Map as Map + +import Data.Kore.AST.Common (Application (..), + Id (..), Pattern (..), + Sort (..), + SymbolOrAlias (..), + Variable) +import Data.Kore.AST.MLPatterns (MLBinderPatternClass (..), + MLPatternClass (..), + PatternLeveledFunction (..), + applyPatternLeveledFunction) +import Data.Kore.AST.PureML (CommonPurePattern, + UnFixedPureMLPattern, + asPurePattern) +import Data.Kore.FixTraversals (fixTopDownVisitor) +import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) +import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), + makeEvaluatedAnd) +import Data.Kore.Step.Condition.Evaluator (evaluateFunctionCondition) +import Data.Kore.Step.Function.Data (ApplicationFunctionEvaluator (..), + CommonPurePatternFunctionEvaluator (..), + ConditionEvaluator (..), + FunctionEvaluation (..), + FunctionResult (..)) +import Data.Kore.Variables.Fresh.IntCounter (IntCounter) + +import Debug.Trace + +multiTrace :: [String] -> a -> a +multiTrace [] a = a +multiTrace (x:xs) a = trace x $ multiTrace xs a + +evaluateFunctions + :: MetadataTools level + -> Map.Map (Id level) [ApplicationFunctionEvaluator level] + -> Sort level + -> CommonPurePattern level + -> IntCounter (FunctionResult level) +evaluateFunctions metadataTools functionIdToEvaluator conditionSort = + trace "Evaluate functions" $ + fixTopDownVisitor + (filterUnhandledPatterns metadataTools) + (evaluateLocalFunction + (ConditionEvaluator conditionEvaluator) + (CommonPurePatternFunctionEvaluator functionEvaluator) + functionIdToEvaluator + conditionSort) + where + conditionEvaluator = + evaluateFunctionCondition + (CommonPurePatternFunctionEvaluator functionEvaluator) + conditionSort + functionEvaluator = + evaluateFunctions metadataTools functionIdToEvaluator conditionSort + +newtype FilterWrapper level = FilterWrapper + { filterUnwrap :: Either (IntCounter (FunctionResult level)) (UnFixedPureMLPattern level Variable) + } + +filterUnhandledPatterns + :: MetadataTools level + -> Pattern level Variable (CommonPurePattern level) + -> Either + (IntCounter (FunctionResult level)) + (UnFixedPureMLPattern level Variable) +filterUnhandledPatterns metadataTools patt = + filterUnwrap + (applyPatternLeveledFunction + PatternLeveledFunction + { patternLeveledFunctionML = wrapUnchanged . mlPatternToPattern + , patternLeveledFunctionMLBinder = wrapUnchanged . mlBinderPatternToPattern + , stringLeveledFunction = wrapUnchanged . StringLiteralPattern + , charLeveledFunction = wrapUnchanged . CharLiteralPattern + , applicationLeveledFunction = + \ app@Application {applicationSymbolOrAlias = symbol} -> + trace ("Hi " ++ getId (symbolOrAliasConstructor symbol)) $ + if isConstructor metadataTools symbol || isFunction metadataTools symbol + then trace "Right" $ FilterWrapper $ Right $ ApplicationPattern app + else trace "Left" $ wrapUnchanged $ ApplicationPattern app + , variableLeveledFunction = wrapUnchanged . VariablePattern + } + patt + ) + where + wrapUnchanged + :: Pattern level Variable (CommonPurePattern level) + -> FilterWrapper level + wrapUnchanged patt' = + FilterWrapper $ Left $ return FunctionResult + { functionResultPattern = asPurePattern patt' + , functionResultCondition = ConditionTrue + } + +newtype EvaluationWrapper level = EvaluationWrapper + { evaluationUnwrap :: IntCounter (FunctionResult level) } + +evaluateLocalFunction + :: ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Map.Map (Id level) [ApplicationFunctionEvaluator level] + -> Sort level -- TODO: Wrap in a type. + -> Pattern level Variable (IntCounter (FunctionResult level)) + -> IntCounter (FunctionResult level) +evaluateLocalFunction + conditionEvaluator + functionEvaluator + symbolIdToEvaluators + conditionSort + pattIF + = do + pattF <- sequenceA pattIF + let + childrenCondition = + foldr + (makeEvaluatedAnd conditionSort) + ConditionTrue + (fmap functionResultCondition pattF) + normalPattern = fmap functionResultPattern pattF + unchanged = returnUnchanged childrenCondition + evaluationUnwrap + ( applyPatternLeveledFunction + PatternLeveledFunction + { patternLeveledFunctionML = unchanged . mlPatternToPattern + , patternLeveledFunctionMLBinder = unchanged . mlBinderPatternToPattern + , stringLeveledFunction = + assertTrue childrenCondition + . returnUnchanged ConditionTrue + . StringLiteralPattern + , charLeveledFunction = + assertTrue childrenCondition + . returnUnchanged ConditionTrue + . CharLiteralPattern + , applicationLeveledFunction = + evaluateApplication + conditionEvaluator + functionEvaluator + symbolIdToEvaluators + conditionSort + childrenCondition + , variableLeveledFunction = unchanged . VariablePattern + } + normalPattern + ) + where + returnUnchanged + :: EvaluatedCondition level + -> Pattern level Variable (CommonPurePattern level) + -> EvaluationWrapper level + returnUnchanged condition patt = + EvaluationWrapper $ return FunctionResult + { functionResultPattern = asPurePattern patt + , functionResultCondition = condition + } + assertTrue :: EvaluatedCondition level -> a -> a + assertTrue ConditionTrue x = x + assertTrue _ _ = error "Expecting the condition to be true." + +evaluateApplication + :: ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Map.Map (Id level) [ApplicationFunctionEvaluator level] + -> Sort level + -> EvaluatedCondition level + -> Application level (CommonPurePattern level) + -> EvaluationWrapper level +evaluateApplication + conditionEvaluator + functionEvaluator + symbolIdToEvaluator + conditionSort + childrenCondition + app @ Application + { applicationSymbolOrAlias = SymbolOrAlias + -- TODO: Also use the symbolOrAliasParams. + { symbolOrAliasConstructor = symbolId } + } + = trace "evaluate-application" $ + EvaluationWrapper $ + case Map.lookup symbolId symbolIdToEvaluator of + Nothing -> return unchanged + Just evaluators -> do + results <- mapM (applyEvaluator app) evaluators + mergedResults <- + mapM (mergeWithCondition conditionEvaluator conditionSort childrenCondition) results + trace (show results) $ case filter notNotApplicable mergedResults of + [] -> return unchanged + [NotApplicable] -> error "Should not reach this line." + [Symbolic condition] -> + return FunctionResult + { functionResultPattern = + asPurePattern $ ApplicationPattern app + , functionResultCondition = condition + } + [Applied functionResult] -> trace ("evaluate-application " ++ show functionResult) $ return functionResult + (_ : _ : _) -> error "Not implemented yet." + where + unchanged = FunctionResult + { functionResultPattern = asPurePattern $ ApplicationPattern app + , functionResultCondition = childrenCondition + } + applyEvaluator app' (ApplicationFunctionEvaluator evaluator) = + evaluator + conditionEvaluator + functionEvaluator + app' + notNotApplicable = + \case + NotApplicable -> False + _ -> True + +mergeWithCondition + :: ConditionEvaluator level + -> Sort level + -> EvaluatedCondition level + -> FunctionEvaluation level + -> IntCounter (FunctionEvaluation level) +mergeWithCondition _ _ _ NotApplicable = return NotApplicable +mergeWithCondition conditionEvaluator conditionSort toMerge (Symbolic condition) + = trace ("mergeWithCondition - Symbolic: " ++ show toMerge) $ do + mergedCondition <- + mergeConditions conditionEvaluator conditionSort condition toMerge + case mergedCondition of + ConditionFalse -> return NotApplicable + _ -> return $ Symbolic mergedCondition +mergeWithCondition + conditionEvaluator + conditionSort + toMerge + (Applied functionResult) + = multiTrace ["mergeWithCondition - Applied: ", " " ++ show toMerge, " " ++ show (functionResultCondition functionResult), " " ++ show (functionResultPattern functionResult)] $ do + mergedCondition <- + mergeConditions + conditionEvaluator + conditionSort + (functionResultCondition functionResult) + toMerge + case mergedCondition of + ConditionFalse -> return NotApplicable + _ -> trace ("mergeWithCondition - Applied: " ++ show mergedCondition) $ return $ + Applied functionResult {functionResultCondition = mergedCondition} + +mergeConditions + :: ConditionEvaluator level + -> Sort level + -> EvaluatedCondition level + -> EvaluatedCondition level + -> IntCounter (EvaluatedCondition level) +mergeConditions _ conditionSort first second = + return $ makeEvaluatedAnd conditionSort first second + -- TODO: Should be something like: + -- conditionEvaluator (makeEvaluatedAnd conditionSort first second) + -- but, right now, we don't have conditions which are partly satisfiable. diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs new file mode 100644 index 0000000000..49b1d28c3b --- /dev/null +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs @@ -0,0 +1,162 @@ +{-# LANGUAGE GADTs #-} +{-| +Module : Data.Kore.Step.Function.UserDefined +Description : Evaluates user-defined functions in a pattern +Copyright : (c) Runtime Verification, 2018 +License : UIUC/NCSA +Maintainer : virgil.serbanuta@runtimeverification.com +Stability : experimental +Portability : portable +-} +module Data.Kore.Step.Function.UserDefined + ( CommonPurePatternFunctionEvaluator + , axiomFunctionEvaluator + ) where + +import Data.Kore.AST.Common (Application (..), + Pattern (..), Sort (..), + Top (..)) +import Data.Kore.AST.MetaOrObject (MetaOrObject) +import Data.Kore.AST.PureML (CommonPurePattern, + asPurePattern) +import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) +import Data.Kore.Step.BaseStep (AxiomPattern, StepperConfiguration (..), + stepWithAxiom) +import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), UnevaluatedCondition (..), + makeEvaluatedAnd) +import Data.Kore.Step.Function.Data (CommonPurePatternFunctionEvaluator (..), + ConditionEvaluator (..), + FunctionEvaluation (..), + FunctionResult (..)) +import Data.Kore.Variables.Fresh.IntCounter (IntCounter) + +import Debug.Trace + +axiomFunctionEvaluator + :: MetaOrObject level + => MetadataTools level + -> Sort level + -> AxiomPattern level + -> ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Application level (CommonPurePattern level) + -> IntCounter (FunctionEvaluation level) +axiomFunctionEvaluator + metadataTools + conditionSort + axiom + (ConditionEvaluator conditionEvaluator) + functionEvaluator + app + = trace "axiomFunctionEvaluator" $ + case stepResult of + Left err -> do + e <- err + trace ("axiomFunctionEvaluator-Left " ++ show e) $ return NotApplicable + Right configurationWithProof -> trace "axiomFunctionEvaluator-Right" $ + do + ( StepperConfiguration + { stepperConfigurationPattern = rewrittenPattern + , stepperConfigurationCondition = rewritingCondition + } + , _ + ) <- configurationWithProof + evaluatedRewritingCondition <- + conditionEvaluator (UnevaluatedCondition rewritingCondition) + axiomFunctionEvaluatorAfterStep + metadataTools + conditionSort + functionEvaluator + FunctionResult + { functionResultPattern = rewrittenPattern + , functionResultCondition = evaluatedRewritingCondition + } + where + stepResult = + stepWithAxiom + metadataTools + (stepperConfiguration conditionSort app) + axiom + stepperConfiguration + :: Sort level + -> Application level (CommonPurePattern level) + -> StepperConfiguration level + stepperConfiguration conditionSort' app' = StepperConfiguration + { stepperConfigurationPattern = asPurePattern $ ApplicationPattern app' + , stepperConfigurationCondition = + asPurePattern $ TopPattern $ Top conditionSort' + , stepperConfigurationConditionSort = conditionSort' + } + +axiomFunctionEvaluatorAfterStep + :: MetadataTools level + -> Sort level + -> CommonPurePatternFunctionEvaluator level + -> FunctionResult level + -> IntCounter (FunctionEvaluation level) +axiomFunctionEvaluatorAfterStep + _ + conditionSort + (CommonPurePatternFunctionEvaluator functionEvaluator) + FunctionResult + { functionResultPattern = rewrittenPattern + , functionResultCondition = rewritingCondition + } + = case rewritingCondition of + ConditionFalse -> return NotApplicable + _ -> do + FunctionResult + { functionResultPattern = simplifiedPattern + , functionResultCondition = simplificationCondition + } <- functionEvaluator rewrittenPattern + return $ resultFromSimplification + conditionSort + simplifiedPattern + --TODO: Maybe call a ConditionEvaluator + (makeEvaluatedAnd conditionSort rewritingCondition simplificationCondition) + rewrittenPattern + rewritingCondition + +resultFromSimplification + :: Sort level + -> CommonPurePattern level + -> EvaluatedCondition level + -> CommonPurePattern level + -> EvaluatedCondition level + -> FunctionEvaluation level +resultFromSimplification + _ simplifiedPattern ConditionTrue _ _ + = Applied FunctionResult + { functionResultPattern = simplifiedPattern + , functionResultCondition = ConditionTrue + } +resultFromSimplification + _ + simplifiedPattern + simplificationCondition @ (ConditionUnevaluable _) + _ _ + = Applied FunctionResult + { functionResultPattern = simplifiedPattern + , functionResultCondition = simplificationCondition + } +resultFromSimplification + _ _ + ConditionFalse + rewrittenPattern + ConditionTrue + = Applied FunctionResult + { functionResultPattern = rewrittenPattern + , functionResultCondition = ConditionTrue + } +resultFromSimplification + _ _ + ConditionFalse + rewrittenPattern + rewritingCondition @ (ConditionUnevaluable _) + = Applied FunctionResult + { functionResultPattern = rewrittenPattern + , functionResultCondition = rewritingCondition + } +resultFromSimplification + _ _ ConditionFalse _ ConditionFalse + = error "Unexpected case." diff --git a/src/main/haskell/language-kore/src/Data/Kore/Unparser/Unparse.hs b/src/main/haskell/language-kore/src/Data/Kore/Unparser/Unparse.hs index d3556404fd..a0e6b4f3e3 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Unparser/Unparse.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Unparser/Unparse.hs @@ -16,10 +16,10 @@ Portability : portable module Data.Kore.Unparser.Unparse (Unparse(..), unparseToString) where import Data.Kore.AST.Common -import Data.Kore.AST.Sentence import Data.Kore.AST.Kore import Data.Kore.AST.MetaOrObject import Data.Kore.AST.MLPatterns +import Data.Kore.AST.Sentence import Data.Kore.IndentingPrinter (PrinterOutput, StringPrinter, betweenLines, printToString, withIndent, write) @@ -135,7 +135,7 @@ instance instance Unparse MLPatternType where unparse pt = write ('\\' : patternString pt) -unparseMLPattern :: (PrinterOutput w m, MLPatternClass p, Unparse rpt) +unparseMLPattern :: (PrinterOutput w m, MLPatternClass p level, Unparse rpt) => p level rpt -> m () unparseMLPattern p = do unparse (getPatternType p) @@ -172,7 +172,7 @@ instance Unparse (Bottom level p) where instance Unparse p => Unparse (Ceil level p) where unparse = unparseMLPattern -instance Unparse p => Unparse (DomainValue level p) where +instance Unparse p => Unparse (DomainValue Object p) where unparse = unparseMLPattern instance Unparse p => Unparse (Equals level p) where @@ -198,7 +198,7 @@ instance Unparse p => Unparse (Implies level p) where instance Unparse p => Unparse (In level p) where unparse = unparseMLPattern -instance Unparse p => Unparse (Next level p) where +instance Unparse p => Unparse (Next Object p) where unparse = unparseMLPattern instance Unparse p => Unparse (Not level p) where @@ -207,7 +207,7 @@ instance Unparse p => Unparse (Not level p) where instance Unparse p => Unparse (Or level p) where unparse = unparseMLPattern -instance Unparse p => Unparse (Rewrites level p) where +instance Unparse p => Unparse (Rewrites Object p) where unparse = unparseMLPattern instance Unparse (Top level p) where @@ -242,7 +242,7 @@ instance (Unparse p, Unparse (v level)) instance Unparse CommonKorePattern where unparse = applyKorePattern unparse unparse -instance Unparse (Attributes) where +instance Unparse Attributes where unparse = inSquareBrackets . unparse . getAttributes instance diff --git a/src/main/haskell/language-kore/src/Data/Kore/Variables/Sort.hs b/src/main/haskell/language-kore/src/Data/Kore/Variables/Sort.hs index 4b6c6487b0..8c40fc8431 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Variables/Sort.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Variables/Sort.hs @@ -86,7 +86,7 @@ addPatternSortVariables pattern1 addSortVariables1 existing = pattern1 addMLPatternSortVariables - :: (MLPatternClass p) + :: (MLPatternClass p level) => p level child -> (Set.Set sortvar -> Sort level -> Set.Set sortvar) -> Set.Set sortvar diff --git a/src/main/haskell/language-kore/test/parser/AllParserTests.hs b/src/main/haskell/language-kore/test/parser/AllParserTests.hs index f6b56a6089..2cf265a694 100644 --- a/src/main/haskell/language-kore/test/parser/AllParserTests.hs +++ b/src/main/haskell/language-kore/test/parser/AllParserTests.hs @@ -29,6 +29,7 @@ import Data.Kore.Parser.LexemeTest import Data.Kore.Parser.ParserTest import Data.Kore.Parser.RegressionTest import Data.Kore.Step.BaseStepTest +import Data.Kore.Step.Function.IntegrationTest import Data.Kore.Step.StepTest import Data.Kore.Substitution.ClassTest import Data.Kore.Substitution.ListTest @@ -95,4 +96,5 @@ unitTests = , topologicalSortTest , baseStepTests , stepTests + , functionIntegrationTests ] diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs index 53e69cb728..bcd8df3d65 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs @@ -18,7 +18,9 @@ import Test.Tasty.HUnit.Extensions import Data.Kore.AST.Common import Data.Kore.Step.BaseStep +import Data.Kore.Step.Condition.Condition import Data.Kore.Step.Error +import Data.Kore.Step.Function.Data import Data.Kore.Unification.Error import Data.Kore.Unification.Unifier @@ -272,11 +274,33 @@ instance (EqualWithExplanation child, Eq child, Show child) where compareWithExplanation = rawCompareWithExplanation printWithExplanation = show -instance (EqualWithExplanation child, Eq child, Show child) + +instance (Show child, EqualWithExplanation child) + => StructEqualWithExplanation (Ceil level child) + where + structFieldsWithNames + expected @ (Ceil _ _ _) + actual @ (Ceil _ _ _) + = [ EqWrap + "ceilOperandSort = " + (ceilOperandSort expected) + (ceilOperandSort actual) + , EqWrap + "ceilResultSort = " + (ceilResultSort expected) + (ceilResultSort actual) + , EqWrap + "ceilChild = " + (ceilChild expected) + (ceilChild actual) + ] + structConstructorName _ = "Ceil" +instance (EqualWithExplanation child, Show child) => EqualWithExplanation (Ceil level child) where - compareWithExplanation = rawCompareWithExplanation + compareWithExplanation = structCompareWithExplanation printWithExplanation = show + instance (EqualWithExplanation child, Eq child, Show child) => EqualWithExplanation (DomainValue level child) where @@ -443,9 +467,24 @@ instance EqualWithExplanation (Sort level) compareWithExplanation = rawCompareWithExplanation printWithExplanation = show +instance StructEqualWithExplanation (SymbolOrAlias level) + where + structFieldsWithNames + expected @ (SymbolOrAlias _ _) + actual @ (SymbolOrAlias _ _) + = [ EqWrap + "symbolOrAliasConstructor = " + (symbolOrAliasConstructor expected) + (symbolOrAliasConstructor actual) + , EqWrap + "symbolOrAliasParams = " + (symbolOrAliasParams expected) + (symbolOrAliasParams actual) + ] + structConstructorName _ = "SymbolOrAlias" instance EqualWithExplanation (SymbolOrAlias level) where - compareWithExplanation = rawCompareWithExplanation + compareWithExplanation = structCompareWithExplanation printWithExplanation = show instance SumEqualWithExplanation (UnificationError level) @@ -680,3 +719,51 @@ instance EqualWithExplanation (StepperVariable level) compareWithExplanation = sumCompareWithExplanation printWithExplanation = show +instance StructEqualWithExplanation (FunctionResult level) + where + structFieldsWithNames + expected @ (FunctionResult _ _) + actual @ (FunctionResult _ _) + = [ EqWrap + "functionResultPattern = " + (functionResultPattern expected) + (functionResultPattern actual) + , EqWrap + "functionResultCondition = " + (functionResultCondition expected) + (functionResultCondition actual) + ] + structConstructorName _ = "FunctionResult" + +instance EqualWithExplanation (FunctionResult level) + where + compareWithExplanation = structCompareWithExplanation + printWithExplanation = show + +instance SumEqualWithExplanation (EvaluatedCondition level) + where + sumConstructorPair ConditionTrue ConditionTrue = + SumConstructorSameNoArguments + sumConstructorPair a1@ConditionTrue a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + + sumConstructorPair ConditionFalse ConditionFalse = + SumConstructorSameNoArguments + sumConstructorPair a1@ConditionFalse a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + + sumConstructorPair + (ConditionUnevaluable a1) (ConditionUnevaluable a2) + = + SumConstructorSameWithArguments + (EqWrap "ConditionUnevaluable" a1 a2) + sumConstructorPair a1@(ConditionUnevaluable _) a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + +instance EqualWithExplanation (EvaluatedCondition level) + where + compareWithExplanation = sumCompareWithExplanation + printWithExplanation = show diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs index 7018c6d526..0c63eeb120 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs @@ -703,6 +703,7 @@ mockMetadataTools :: MetadataTools Meta mockMetadataTools = MetadataTools { isConstructor = const True , isFunctional = const True + , isFunction = const False , getArgumentSorts = const [asAst PatternSort, asAst PatternSort] , getResultSort = const (asAst PatternSort) } diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs index ff345e0abd..af10f8c7e5 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs @@ -463,6 +463,7 @@ mockMetadataTools :: MetadataTools Meta mockMetadataTools = MetadataTools { isConstructor = const True , isFunctional = const True + , isFunction = const False , getArgumentSorts = const [asAst PatternSort, asAst PatternSort] , getResultSort = const (asAst PatternSort) } diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Unification/UnifierTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Unification/UnifierTest.hs index ef8838d91f..379e1f6200 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Unification/UnifierTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Unification/UnifierTest.hs @@ -9,11 +9,11 @@ import Test.Tasty.HUnit.Extensions import Data.Kore.AST.Builders import Data.Kore.AST.Common -import Data.Kore.AST.Sentence import Data.Kore.AST.MetaOrObject import Data.Kore.AST.MLPatterns import Data.Kore.AST.MLPatternsTest (extractPurePattern) import Data.Kore.AST.PureML +import Data.Kore.AST.Sentence import Data.Kore.ASTPrettyPrint import Data.Kore.ASTVerifier.DefinitionVerifierTestHelpers import Data.Kore.Comparators () @@ -128,6 +128,7 @@ tools :: MetadataTools Object tools = MetadataTools { isConstructor = mockIsConstructor , isFunctional = mockIsFunctional + , isFunction = const False , getArgumentSorts = mockGetArgumentSorts , getResultSort = mockGetResultSort } From 7c77147a1bc930a7fe2a2d5b8ba650b5e4fb0188 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Thu, 28 Jun 2018 15:50:11 +0300 Subject: [PATCH 02/10] Tmp --- .../Kore/Step/Function/IntegrationTest.hs | 439 ++++++++++++++++++ 1 file changed, 439 insertions(+) create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs new file mode 100644 index 0000000000..2ec3f43870 --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs @@ -0,0 +1,439 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +module Data.Kore.Step.Function.IntegrationTest (functionIntegrationTests) where + +import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) +import qualified Data.Map as Map + + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) + +import Data.Kore.AST.Common (Application (..), + AstLocation (..), + Id (..), Pattern (..), + Sort, + SymbolOrAlias (..)) +import Data.Kore.AST.MetaOrObject +import Data.Kore.AST.PureML (CommonPurePattern) +import Data.Kore.AST.PureToKore (patternKoreToPure) +import Data.Kore.Building.AsAst +import Data.Kore.Building.Patterns +import Data.Kore.Building.Sorts +import Data.Kore.Comparators () +import Data.Kore.MetaML.AST (CommonMetaPattern) +import Data.Kore.Step.BaseStep (AxiomPattern (..)) +import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..)) +import Data.Kore.Step.Function.Data (ApplicationFunctionEvaluator (..), + CommonPurePatternFunctionEvaluator, + ConditionEvaluator, + FunctionEvaluation (..), + FunctionResult (..)) +import Data.Kore.Step.Function.Evaluator (evaluateFunctions) +import Data.Kore.Step.Function.UserDefined (axiomFunctionEvaluator) +import Data.Kore.Variables.Fresh.IntCounter (IntCounter, + runIntCounter) + +import Test.Tasty.HUnit.Extensions + +functionIntegrationTests :: TestTree +functionIntegrationTests = + testGroup + "Function evaluation integration tests" + [ testCase "Simple evaluation" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern (metaG metaC) + , functionResultCondition = ConditionTrue + } + (evaluate + mockMetadataTools + (Map.singleton fId + [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (v1 PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (v1 PatternSort)) + } + ] + ) + (asAst SortSort) + (asPureMetaPattern (metaF metaC)) + ) + ) + , testCase "Evaluates inside functions" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern (metaG (metaG metaC)) + , functionResultCondition = ConditionTrue + } + (evaluate + mockMetadataTools + (Map.singleton fId + [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (v1 PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (v1 PatternSort)) + } + ] + ) + (asAst SortSort) + (asPureMetaPattern (metaF (metaF metaC))) + ) + ) + , testCase "Does not evaluate with 'or' - may chage in the future" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern + (metaF (metaOr PatternSort (metaF metaC) (metaF metaC))) + , functionResultCondition = ConditionTrue + } + (evaluate + mockMetadataTools + (Map.singleton fId + [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (v1 PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (v1 PatternSort)) + } + ] + ) + (asAst SortSort) + (asPureMetaPattern + (metaF (metaOr PatternSort (metaF metaC) (metaF metaC))) + ) + ) + ) + , testCase "Evaluates on multiple branches" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern + (metaG (metaSigma (metaG metaC) (metaG metaC))) + , functionResultCondition = ConditionTrue + } + (evaluate + mockMetadataTools + (Map.singleton fId + [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (v1 PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (v1 PatternSort)) + } + ] + ) + (asAst SortSort) + (asPureMetaPattern + (metaF (metaSigma (metaF metaC) (metaF metaC))) + ) + ) + ) + , testCase "Returns conditions" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern (metaF metaD) + , functionResultCondition = ConditionUnevaluable (asPureMetaPattern metaC) + } + (evaluate + mockMetadataTools + (Map.singleton cId + [ ApplicationFunctionEvaluator $ mockEvaluator + (Applied FunctionResult + { functionResultPattern = asPureMetaPattern metaD + , functionResultCondition = + ConditionUnevaluable (asPureMetaPattern metaC) + } + ) + ] + ) + (asAst SortSort) + (asPureMetaPattern (metaF metaC)) + ) + ) + , testCase "Merges conditions" + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern (metaG (metaSigma metaE metaE)) + , functionResultCondition = + ConditionUnevaluable $ asPureMetaPattern + (metaAnd SortSort + (metaCeil (ResultSort SortSort) PatternSort metaC) + (metaCeil (ResultSort SortSort) PatternSort metaD) + ) + } + (evaluate + mockMetadataTools + (Map.fromList + [ ( cId + , [ ApplicationFunctionEvaluator $ mockEvaluator + (Applied FunctionResult + { functionResultPattern = asPureMetaPattern metaE + , functionResultCondition = + ConditionUnevaluable (asPureMetaPattern (metaCeil (ResultSort SortSort) PatternSort metaC)) + } + ) + ] + ) + , ( dId + , [ ApplicationFunctionEvaluator $ mockEvaluator + (Applied FunctionResult + { functionResultPattern = asPureMetaPattern metaE + , functionResultCondition = + ConditionUnevaluable (asPureMetaPattern (metaCeil (ResultSort SortSort) PatternSort metaD)) + } + ) + ] + ) + , (fId + , [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (v1 PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (v1 PatternSort)) + } + ] + ) + ] + ) + (asAst SortSort) + (asPureMetaPattern (metaF (metaSigma metaC metaD))) + ) + ) + , testCase "Reevaluates user-defined function results." + (assertEqualWithExplanation "" + FunctionResult + { functionResultPattern = asPureMetaPattern (metaF metaE) + , functionResultCondition = ConditionUnevaluable (asPureMetaPattern metaD) + } + (evaluate + mockMetadataTools + (Map.fromList + [ ( cId + , [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator + mockMetadataTools + (asAst SortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern metaC + , axiomPatternRight = + asPureMetaPattern metaD + } + ] + ) + , ( dId + , [ ApplicationFunctionEvaluator $ mockEvaluator + (Applied FunctionResult + { functionResultPattern = asPureMetaPattern metaE + , functionResultCondition = + ConditionUnevaluable (asPureMetaPattern metaD) + } + ) + ] + ) + ] + ) + (asAst SortSort) + (asPureMetaPattern (metaF metaC)) + ) + ) + ] + +mockEvaluator + :: FunctionEvaluation level + -> ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Application level (CommonPurePattern level) + -> IntCounter (FunctionEvaluation level) +mockEvaluator evaluation _ _ _ = + return evaluation + +evaluate + :: MetadataTools level + -> Map.Map (Id level) [ApplicationFunctionEvaluator level] + -> Sort level + -> CommonPurePattern level + -> FunctionResult level +evaluate metadataTools functionIdToEvaluator conditionSort patt = + fst + (runIntCounter + (evaluateFunctions + metadataTools functionIdToEvaluator conditionSort patt + ) + 0 + ) + +v1 :: MetaSort sort => sort -> MetaVariable sort +v1 = metaVariable "#v1" AstLocationTest +a1 :: MetaSort sort => sort -> MetaVariable sort +a1 = metaVariable "#a1" AstLocationTest +b1 :: MetaSort sort => sort -> MetaVariable sort +b1 = metaVariable "#b1" AstLocationTest +x1 :: MetaSort sort => sort -> MetaVariable sort +x1 = metaVariable "#x1" AstLocationTest +y1 :: MetaSort sort => sort -> MetaVariable sort +y1 = metaVariable "#y1" AstLocationTest +var_0 :: MetaSort sort => sort -> MetaVariable sort +var_0 = metaVariable "#var_0" AstLocationTest +var_1 :: MetaSort sort => sort -> MetaVariable sort +var_1 = metaVariable "#var_1" AstLocationTest +top :: MetaSort sort => sort -> CommonMetaPattern +top sort = asPureMetaPattern $ metaTop sort + +asPureMetaPattern + :: ProperPattern Meta sort patt => patt -> CommonMetaPattern +asPureMetaPattern patt = patternKoreToPure Meta (asAst patt) + +mockMetadataTools :: MetadataTools Meta +mockMetadataTools = MetadataTools + { isConstructor = const True + , isFunctional = const True + , isFunction = const True + , getArgumentSorts = const [asAst PatternSort, asAst PatternSort] + , getResultSort = const (asAst PatternSort) + } + +fId :: Id Meta +fId = Id "#f" AstLocationTest + +fSymbol :: SymbolOrAlias Meta +fSymbol = SymbolOrAlias + { symbolOrAliasConstructor = fId + , symbolOrAliasParams = [] + } + +newtype MetaF p1 = MetaF p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaF p1) + where + asProperPattern (MetaF p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = fSymbol + , applicationChildren = [asAst p1] + } +metaF + :: (MetaPattern PatternSort p1) + => p1 -> MetaF p1 +metaF = MetaF + +gId :: Id Meta +gId = Id "#g" AstLocationTest + +gSymbol :: SymbolOrAlias Meta +gSymbol = SymbolOrAlias + { symbolOrAliasConstructor = gId + , symbolOrAliasParams = [] + } + +newtype MetaG p1 = MetaG p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaG p1) + where + asProperPattern (MetaG p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = gSymbol + , applicationChildren = [asAst p1] + } +metaG + :: (MetaPattern PatternSort p1) + => p1 -> MetaG p1 +metaG = MetaG + +cId :: Id Meta +cId = Id "#c" AstLocationTest + +cSymbol :: SymbolOrAlias Meta +cSymbol = SymbolOrAlias + { symbolOrAliasConstructor = cId + , symbolOrAliasParams = [] + } + +data MetaC = MetaC + +instance ProperPattern Meta PatternSort MetaC + where + asProperPattern MetaC = + ApplicationPattern Application + { applicationSymbolOrAlias = cSymbol + , applicationChildren = [] + } +metaC :: MetaC +metaC = MetaC + +dId :: Id Meta +dId = Id "#d" AstLocationTest + +dSymbol :: SymbolOrAlias Meta +dSymbol = SymbolOrAlias + { symbolOrAliasConstructor = dId + , symbolOrAliasParams = [] + } + +data MetaD = MetaD + +instance ProperPattern Meta PatternSort MetaD + where + asProperPattern MetaD = + ApplicationPattern Application + { applicationSymbolOrAlias = dSymbol + , applicationChildren = [] + } +metaD :: MetaD +metaD = MetaD + +eId :: Id Meta +eId = Id "#e" AstLocationTest + +eSymbol :: SymbolOrAlias Meta +eSymbol = SymbolOrAlias + { symbolOrAliasConstructor = eId + , symbolOrAliasParams = [] + } + +data MetaE = MetaE + +instance ProperPattern Meta PatternSort MetaE + where + asProperPattern MetaE = + ApplicationPattern Application + { applicationSymbolOrAlias = eSymbol + , applicationChildren = [] + } +metaE :: MetaE +metaE = MetaE + +sigmaSymbol :: SymbolOrAlias Meta +sigmaSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#sigma" AstLocationTest + , symbolOrAliasParams = [] + } + +data MetaSigma p1 p2 = MetaSigma p1 p2 +instance (MetaPattern PatternSort p1, MetaPattern PatternSort p2) + => ProperPattern Meta PatternSort (MetaSigma p1 p2) + where + asProperPattern (MetaSigma p1 p2) = + ApplicationPattern Application + { applicationSymbolOrAlias = sigmaSymbol + , applicationChildren = [asAst p1, asAst p2] + } +metaSigma + :: (MetaPattern PatternSort p1, MetaPattern PatternSort p2) + => p1 -> p2 -> MetaSigma p1 p2 +metaSigma = MetaSigma From 60265639fafba2766780419a79f7e3d679e9be60 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Thu, 28 Jun 2018 20:10:28 +0300 Subject: [PATCH 03/10] Eliminate function result duplicates. --- .../language-kore/src/Data/Kore/Step/Condition/Condition.hs | 2 +- .../haskell/language-kore/src/Data/Kore/Step/Function/Data.hs | 4 ++-- .../language-kore/src/Data/Kore/Step/Function/Evaluator.hs | 4 +++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs index 67e6ca5586..7f64917b78 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs @@ -31,7 +31,7 @@ data EvaluatedCondition level -- the SMT solver. When doing that, also change the make{And,Or,...} -- functions to return somenthing that forces reevaluation. | ConditionUnevaluable !(CommonPurePattern level) - deriving Show + deriving (Show, Eq) newtype UnevaluatedCondition level = UnevaluatedCondition (CommonPurePattern level) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs index 4b5612d0a8..ef99508f01 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs @@ -38,13 +38,13 @@ data FunctionResult level = FunctionResult { functionResultPattern :: !(CommonPurePattern level) , functionResultCondition :: !(EvaluatedCondition level) } - deriving Show + deriving (Show, Eq) data FunctionEvaluation level = NotApplicable | Symbolic !(EvaluatedCondition level) | Applied !(FunctionResult level) - deriving Show + deriving (Show, Eq) newtype ConditionEvaluator level = ConditionEvaluator (UnevaluatedCondition level -> IntCounter (EvaluatedCondition level)) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs index 18cda7d8e5..e7a7b92cae 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs @@ -13,6 +13,7 @@ module Data.Kore.Step.Function.Evaluator ( evaluateFunctions ) where +import Data.List (nub) import qualified Data.Map as Map import Data.Kore.AST.Common (Application (..), @@ -197,7 +198,8 @@ evaluateApplication results <- mapM (applyEvaluator app) evaluators mergedResults <- mapM (mergeWithCondition conditionEvaluator conditionSort childrenCondition) results - trace (show results) $ case filter notNotApplicable mergedResults of + -- TODO: nub is O(n^2), should do better than that + trace (show results) $ case nub (filter notNotApplicable mergedResults) of [] -> return unchanged [NotApplicable] -> error "Should not reach this line." [Symbolic condition] -> From c3ab23b26d274e9d27b738c1f59b9d54883eca58 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Fri, 29 Jun 2018 19:02:04 +0300 Subject: [PATCH 04/10] Tmp. --- .../src/Data/Kore/Step/BaseStep.hs | 26 +- .../src/Data/Kore/Step/Condition/Condition.hs | 157 ++++++++---- .../src/Data/Kore/Step/Condition/Evaluator.hs | 97 ++++--- .../src/Data/Kore/Step/Function/Data.hs | 44 +++- .../src/Data/Kore/Step/Function/Evaluator.hs | 240 ++++++++++++------ .../Data/Kore/Step/Function/UserDefined.hs | 163 ++++++------ .../test/parser/Data/Kore/Comparators.hs | 14 + .../parser/Data/Kore/Step/BaseStepTest.hs | 56 ++-- .../Kore/Step/Function/IntegrationTest.hs | 237 +++++++++-------- .../test/parser/Data/Kore/Step/StepTest.hs | 44 +++- 10 files changed, 664 insertions(+), 414 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs index 16a7dce25f..d45d3af867 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs @@ -32,6 +32,7 @@ import Data.Kore.AST.PureML (CommonPurePatt mapPatternVariables) import Data.Kore.FixTraversals (fixBottomUpVisitor) import Data.Kore.IndexedModule.MetadataTools (MetadataTools) +import Data.Kore.Step.Condition.Condition (ConditionSort (..)) import Data.Kore.Step.Error import Data.Kore.Substitution.Class (Hashable (..), PatternSubstitutionClass (..)) import qualified Data.Kore.Substitution.List as ListSubstitution @@ -66,10 +67,11 @@ data StepperConfiguration level = StepperConfiguration -- ^ The pattern being rewritten. -- TODO(virgil): Remove and extract from condition. - , stepperConfigurationConditionSort :: !(Sort level) + , stepperConfigurationConditionSort :: !(ConditionSort level) -- ^ The sort for the configuration condition. , stepperConfigurationCondition :: !(CommonPurePattern level) -- ^ The condition predicate. + -- TODO(virgil): Make this an EvaluatedCondition. } deriving (Show, Eq) @@ -175,7 +177,8 @@ stepWithAxiom StepperConfiguration { stepperConfigurationPattern = startPatternRaw , stepperConfigurationCondition = startConditionRaw - , stepperConfigurationConditionSort = conditionSort + , stepperConfigurationConditionSort = + conditionSort @ (ConditionSort unwrappedConditionSort) } AxiomPattern { axiomPatternLeft = axiomLeftRaw @@ -224,7 +227,7 @@ stepWithAxiom (variableMapping1, condition) <- patternStepVariablesToCommon existingVars variableMapping (Fix $ AndPattern And - { andSort = conditionSort + { andSort = unwrappedConditionSort , andFirst = startCondition , andSecond = substitutionToPattern conditionSort @@ -556,26 +559,29 @@ makeUnifiedSubstitution = substitutionToPattern :: SortedVariable variable - => Sort level + => ConditionSort level -> [(variable level, PureMLPattern level variable)] -> PureMLPattern level variable -substitutionToPattern sort [] = +substitutionToPattern (ConditionSort sort) [] = asPurePattern $ TopPattern Top { topSort = sort } substitutionToPattern sort [subst] = singleSubstitutionToPattern sort subst -substitutionToPattern sort (subst : substs) = +substitutionToPattern + conditionSort @ (ConditionSort sort) + (subst : substs) + = asPurePattern $ AndPattern And { andSort = sort - , andFirst = singleSubstitutionToPattern sort subst - , andSecond = substitutionToPattern sort substs + , andFirst = singleSubstitutionToPattern conditionSort subst + , andSecond = substitutionToPattern conditionSort substs } singleSubstitutionToPattern :: SortedVariable variable - => Sort level + => ConditionSort level -> (variable level, PureMLPattern level variable) -> PureMLPattern level variable -singleSubstitutionToPattern sort (var, patt) = +singleSubstitutionToPattern (ConditionSort sort) (var, patt) = asPurePattern $ EqualsPattern Equals { equalsOperandSort = sortedVariableSort var , equalsResultSort = sort diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs index 7f64917b78..ebc4a64fb3 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs @@ -8,14 +8,15 @@ Stability : experimental Portability : portable -} module Data.Kore.Step.Condition.Condition - ( EvaluatedCondition (..) + ( ConditionProof (..) + , ConditionSort (..) + , EvaluatedCondition (..) , UnevaluatedCondition (..) , makeEvaluatedAnd , makeEvaluatedIff , makeEvaluatedImplies , makeEvaluatedNot , makeEvaluatedOr - , makeUnevaluatedAnd ) where import Data.Kore.AST.Common (And (..), Iff (..), Implies (..), @@ -23,7 +24,21 @@ import Data.Kore.AST.Common (And (..), Iff (..), Implies (..), Sort (..)) import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern) --- TODO: Maybe rename +{--| 'ConditionProof' is a placeholder for a proof about a condition's +evaluation. +--} +data ConditionProof level = ConditionProof + deriving (Show, Eq) + +{--| 'ConditionSort' represents a sort that is meant to be used when building +conditions. Usually it is assumed that the existing condition pieces already +have this sort. +--} +newtype ConditionSort level = ConditionSort (Sort level) + deriving (Show, Eq) + +{--| 'EvaluatedCondition' holds the result of evaluating a condition. +--} data EvaluatedCondition level = ConditionTrue | ConditionFalse @@ -33,75 +48,111 @@ data EvaluatedCondition level | ConditionUnevaluable !(CommonPurePattern level) deriving (Show, Eq) +{--| 'UnevaluatedCondition' holds a condition that was not yet evaluated. +--} newtype UnevaluatedCondition level = UnevaluatedCondition (CommonPurePattern level) deriving Show +{--| 'makeEvaluatedAnd' combines two evaluated conditions with an 'and', +doing some simplification. +--} makeEvaluatedAnd - :: Sort level + :: ConditionSort level -> EvaluatedCondition level -> EvaluatedCondition level - -> EvaluatedCondition level -makeEvaluatedAnd _ ConditionFalse _ = ConditionFalse -makeEvaluatedAnd _ _ ConditionFalse = ConditionFalse -makeEvaluatedAnd _ ConditionTrue second = second -makeEvaluatedAnd _ first ConditionTrue = first -makeEvaluatedAnd sort (ConditionUnevaluable first) (ConditionUnevaluable second) = - ConditionUnevaluable $ asPurePattern $ AndPattern $ And sort first second - --- TODO: Do I need this? -makeUnevaluatedAnd - :: Sort level - -> UnevaluatedCondition level - -> UnevaluatedCondition level - -> UnevaluatedCondition level -makeUnevaluatedAnd sort (UnevaluatedCondition first) (UnevaluatedCondition second) = - UnevaluatedCondition $ asPurePattern $ AndPattern $ And sort first second - + -> (EvaluatedCondition level, ConditionProof level) +makeEvaluatedAnd _ ConditionFalse _ = (ConditionFalse, ConditionProof) +makeEvaluatedAnd _ _ ConditionFalse = (ConditionFalse, ConditionProof) +makeEvaluatedAnd _ ConditionTrue second = (second, ConditionProof) +makeEvaluatedAnd _ first ConditionTrue = (first, ConditionProof) +makeEvaluatedAnd + (ConditionSort sort) + (ConditionUnevaluable first) + (ConditionUnevaluable second) + = + ( ConditionUnevaluable $ asPurePattern $ AndPattern $ And sort first second + , ConditionProof + ) +{--| 'makeEvaluatedOr' combines two evaluated conditions with an 'or', doing +some simplification. +--} makeEvaluatedOr - :: Sort level - -> EvaluatedCondition level + :: ConditionSort level -> EvaluatedCondition level -> EvaluatedCondition level -makeEvaluatedOr _ ConditionTrue _ = ConditionTrue -makeEvaluatedOr _ _ ConditionTrue = ConditionTrue -makeEvaluatedOr _ ConditionFalse second = second -makeEvaluatedOr _ first ConditionFalse = first -makeEvaluatedOr sort (ConditionUnevaluable first) (ConditionUnevaluable second) = - ConditionUnevaluable $ asPurePattern $ OrPattern $ Or sort first second + -> (EvaluatedCondition level, ConditionProof level) +makeEvaluatedOr _ ConditionTrue _ = (ConditionTrue, ConditionProof) +makeEvaluatedOr _ _ ConditionTrue = (ConditionTrue, ConditionProof) +makeEvaluatedOr _ ConditionFalse second = (second, ConditionProof) +makeEvaluatedOr _ first ConditionFalse = (first, ConditionProof) +makeEvaluatedOr + (ConditionSort sort) + (ConditionUnevaluable first) + (ConditionUnevaluable second) + = + ( ConditionUnevaluable $ asPurePattern $ OrPattern $ Or sort first second + , ConditionProof + ) +{--| 'makeEvaluatedImplies' combines two evaluated conditions into an +implication, doing some simplification. +--} makeEvaluatedImplies - :: Sort level - -> EvaluatedCondition level + :: ConditionSort level -> EvaluatedCondition level -> EvaluatedCondition level --- TODO: Is it reasonable to use a different thing here? -makeEvaluatedImplies _ ConditionFalse _ = ConditionTrue -makeEvaluatedImplies _ _ ConditionTrue = ConditionTrue -makeEvaluatedImplies _ ConditionTrue second = second -makeEvaluatedImplies sort first ConditionFalse = makeEvaluatedNot sort first -makeEvaluatedImplies sort (ConditionUnevaluable first) (ConditionUnevaluable second) = - ConditionUnevaluable $ asPurePattern $ ImpliesPattern $ Implies sort first second + -> (EvaluatedCondition level, ConditionProof level) +makeEvaluatedImplies _ ConditionFalse _ = (ConditionTrue, ConditionProof) +makeEvaluatedImplies _ _ ConditionTrue = (ConditionTrue, ConditionProof) +makeEvaluatedImplies _ ConditionTrue second = (second, ConditionProof) +makeEvaluatedImplies sort first ConditionFalse = + (fst $ makeEvaluatedNot sort first, ConditionProof) +makeEvaluatedImplies + (ConditionSort sort) + (ConditionUnevaluable first) + (ConditionUnevaluable second) + = + ( ConditionUnevaluable $ asPurePattern $ ImpliesPattern $ + Implies sort first second + , ConditionProof + ) +{--| 'makeEvaluatedIff' combines two evaluated conditions with an 'iff', doing +some simplification. +--} makeEvaluatedIff - :: Sort level + :: ConditionSort level -> EvaluatedCondition level -> EvaluatedCondition level - -> EvaluatedCondition level --- TODO: Is it reasonable to use a different thing here? -makeEvaluatedIff sort ConditionFalse second = makeEvaluatedNot sort second -makeEvaluatedIff _ ConditionTrue second = second -makeEvaluatedIff sort first@(ConditionUnevaluable _) ConditionFalse = makeEvaluatedNot sort first -makeEvaluatedIff _ first@(ConditionUnevaluable _) ConditionTrue = first -makeEvaluatedIff sort (ConditionUnevaluable first) (ConditionUnevaluable second) = - ConditionUnevaluable $ asPurePattern $ IffPattern $ Iff sort first second + -> (EvaluatedCondition level, ConditionProof level) +makeEvaluatedIff sort ConditionFalse second = + (fst $ makeEvaluatedNot sort second, ConditionProof) +makeEvaluatedIff _ ConditionTrue second = (second, ConditionProof) +makeEvaluatedIff sort first@(ConditionUnevaluable _) ConditionFalse = + (fst $ makeEvaluatedNot sort first, ConditionProof) +makeEvaluatedIff _ first@(ConditionUnevaluable _) ConditionTrue = + (first, ConditionProof) +makeEvaluatedIff + (ConditionSort sort) + (ConditionUnevaluable first) + (ConditionUnevaluable second) + = + ( ConditionUnevaluable $ asPurePattern $ IffPattern $ Iff sort first second + , ConditionProof + ) +{--| 'makeEvaluatedNot' negates an evaluated condition, doing some +simplification. +--} makeEvaluatedNot - :: Sort level - -> EvaluatedCondition level + :: ConditionSort level -> EvaluatedCondition level -makeEvaluatedNot _ ConditionFalse = ConditionTrue -makeEvaluatedNot _ ConditionTrue = ConditionFalse -makeEvaluatedNot sort (ConditionUnevaluable condition) = - ConditionUnevaluable $ asPurePattern $ NotPattern $ Not sort condition + -> (EvaluatedCondition level, ConditionProof level) +makeEvaluatedNot _ ConditionFalse = (ConditionTrue, ConditionProof) +makeEvaluatedNot _ ConditionTrue = (ConditionFalse, ConditionProof) +makeEvaluatedNot (ConditionSort sort) (ConditionUnevaluable condition) = + ( ConditionUnevaluable $ asPurePattern $ NotPattern $ Not sort condition + , ConditionProof + ) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs index d0869d9410..3076ca36bb 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs @@ -1,7 +1,7 @@ {-# LANGUAGE GADTs #-} {-| Module : Data.Kore.Step.Condition.Evaluator -Description : Evaluates conditions +Description : Evaluates conditions. Copyright : (c) Runtime Verification, 2018 License : UIUC/NCSA Maintainer : virgil.serbanuta@runtimeverification.com @@ -15,12 +15,13 @@ module Data.Kore.Step.Condition.Evaluator import Data.Kore.AST.Common (And (..), Equals (..), Iff (..), Implies (..), Not (..), Or (..), - Pattern (..), Sort (..), - Variable) + Pattern (..), Variable) import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern, fromPurePattern) -import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), +import Data.Kore.Step.Condition.Condition (ConditionProof (..), + ConditionSort (..), + EvaluatedCondition (..), UnevaluatedCondition (..), makeEvaluatedAnd, makeEvaluatedIff, @@ -31,12 +32,20 @@ import Data.Kore.Step.Function.Data (CommonPurePatternFunction FunctionResult (..)) import Data.Kore.Variables.Fresh.IntCounter (IntCounter) +{--| 'evaluateFunctionCondition' attempts to evaluate a Kore condition. +Right now the evaluation is rather rudimentary and gives up failry easy, +returning 'ConditionUnevaluable'. +--} evaluateFunctionCondition :: CommonPurePatternFunctionEvaluator level - -> Sort level + -- ^ Evaluates functions in a pattern. + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> UnevaluatedCondition level - -> IntCounter (EvaluatedCondition level) + -- ^ The condition to be evaluated. + -> IntCounter (EvaluatedCondition level, ConditionProof level) evaluateFunctionCondition functionEvaluator conditionSort @@ -47,49 +56,63 @@ evaluateFunctionCondition conditionSort (fromPurePattern condition) +{--| 'evaluateFunctionCondition' attempts to evaluate a Kore condition. + +Right now the evaluation is rather rudimentary and gives up failry easy, +returning 'ConditionUnevaluable'. +--} evaluateFunctionConditionInternal :: CommonPurePatternFunctionEvaluator level - -> Sort level + -> ConditionSort level -> Pattern level Variable (CommonPurePattern level) - -> IntCounter (EvaluatedCondition level) + -> IntCounter (EvaluatedCondition level, ConditionProof level) evaluateFunctionConditionInternal functionEvaluator conditionSort (AndPattern And {andFirst = first, andSecond = second}) = do - a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) - b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + (a, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern first) + (b, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern second) return $ makeEvaluatedAnd conditionSort a b evaluateFunctionConditionInternal functionEvaluator conditionSort (OrPattern Or {orFirst = first, orSecond = second}) = do - a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) - b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + (a, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern first) + (b, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern second) return $ makeEvaluatedOr conditionSort a b evaluateFunctionConditionInternal functionEvaluator conditionSort (NotPattern Not {notChild = patt}) = do - a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern patt) + (a, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern patt) return (makeEvaluatedNot conditionSort a) evaluateFunctionConditionInternal functionEvaluator conditionSort (ImpliesPattern Implies {impliesFirst = first, impliesSecond = second}) = do - a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) - b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + (a, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern first) + (b, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern second) return $ makeEvaluatedImplies conditionSort a b evaluateFunctionConditionInternal functionEvaluator conditionSort (IffPattern Iff {iffFirst = first, iffSecond = second}) = do - a <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern first) - b <- evaluateFunctionConditionInternal functionEvaluator conditionSort (fromPurePattern second) + (a, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern first) + (b, _) <- evaluateFunctionConditionInternal + functionEvaluator conditionSort (fromPurePattern second) return $ makeEvaluatedIff conditionSort a b evaluateFunctionConditionInternal (CommonPurePatternFunctionEvaluator functionEvaluator) @@ -99,29 +122,31 @@ evaluateFunctionConditionInternal firstValue <- functionEvaluator first secondValue <- functionEvaluator second let - FunctionResult - { functionResultPattern = firstPattern - , functionResultCondition = firstCondition - } = firstValue - FunctionResult - { functionResultPattern = secondPattern - -- TODO: Maybe Make two types of condition: functionResult and evaluated - , functionResultCondition = secondCondition - } = secondValue - -- TODO: This is more complex than implemented here, e.g. commutativity - -- may be an issue. - --firstCondition' <- firstCondition - --secondCondition' <- secondCondition + ( FunctionResult + { functionResultPattern = firstPattern + , functionResultCondition = firstCondition + } + , _ + ) = firstValue + ( FunctionResult + { functionResultPattern = secondPattern + , functionResultCondition = secondCondition + } + , _ + ) = secondValue + -- TODO(virgil): This is more complex than implemented here, e.g. + -- we should evaluate functions on these patterns. if firstPattern == secondPattern - -- TODO: this should probably call evaluateFunctionCondition - then return $ makeEvaluatedAnd conditionSort firstCondition secondCondition - else return ConditionFalse + -- TODO(virgil): this should probably call evaluateFunctionCondition + then return $ + makeEvaluatedAnd conditionSort firstCondition secondCondition + else return (ConditionFalse, ConditionProof) evaluateFunctionConditionInternal _ _ (TopPattern _) - = return ConditionTrue + = return (ConditionTrue, ConditionProof) evaluateFunctionConditionInternal _ _ (BottomPattern _) - = return ConditionFalse + = return (ConditionFalse, ConditionProof) evaluateFunctionConditionInternal _ _ patt - = return (ConditionUnevaluable (asPurePattern patt)) + = return (ConditionUnevaluable (asPurePattern patt), ConditionProof) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs index ef99508f01..f3e25b120b 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs @@ -1,6 +1,6 @@ {-| Module : Data.Kore.Step.Function.Data -Description : Data structures used for function evaluation +Description : Data structures used for function evaluation. Copyright : (c) Runtime Verification, 2018 License : UIUC/NCSA Maintainer : virgil.serbanuta@runtimeverification.com @@ -12,39 +12,65 @@ module Data.Kore.Step.Function.Data , CommonPurePatternFunctionEvaluator (..) , ConditionEvaluator (..) , FunctionResult (..) - , FunctionEvaluation (..) + , FunctionResultProof (..) + , AttemptedFunctionResult (..) ) where import Data.Kore.AST.Common (Application) import Data.Kore.AST.PureML (CommonPurePattern) -import Data.Kore.Step.Condition.Condition (EvaluatedCondition, +import Data.Kore.Step.Condition.Condition (ConditionProof, + EvaluatedCondition, UnevaluatedCondition) import Data.Kore.Variables.Fresh.IntCounter (IntCounter) +{--| 'FunctionResultProof' is a placeholder for proofs about a Kore function +evaluation's result correctness. +--} +data FunctionResultProof level = FunctionResultProof + deriving (Show, Eq) + +{--| 'CommonPurePatternFunctionEvaluator' wraps a function that evaluates +Kore functions on patterns. +--} newtype CommonPurePatternFunctionEvaluator level = CommonPurePatternFunctionEvaluator - (CommonPurePattern level -> IntCounter (FunctionResult level)) + ( CommonPurePattern level + -> IntCounter (FunctionResult level, FunctionResultProof level) + ) +{--| 'ApplicationFunctionEvaluator' evaluates functions on an 'Application' +pattern. This can be either a built-in evaluator or a user-defined one. +--} newtype ApplicationFunctionEvaluator level = ApplicationFunctionEvaluator - ( ConditionEvaluator level + ( ConditionEvaluator level -> CommonPurePatternFunctionEvaluator level -> Application level (CommonPurePattern level) - -> IntCounter (FunctionEvaluation level) + -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) ) --- TODO: this should probably be replaced by a StepperConfiguration +{--| 'FunctionResult' represents the result of evaluating a Kore function on +a pattern. +--} +-- TODO(virgil): Consider replacing this by a StepperConfiguration data FunctionResult level = FunctionResult { functionResultPattern :: !(CommonPurePattern level) , functionResultCondition :: !(EvaluatedCondition level) } deriving (Show, Eq) -data FunctionEvaluation level +{--| 'AttemptedFunctionResult' is a generalized 'FunctionResult' that handles +cases where the function can't be fully evaluated. +--} +data AttemptedFunctionResult level = NotApplicable | Symbolic !(EvaluatedCondition level) | Applied !(FunctionResult level) deriving (Show, Eq) +{--| 'ConditionEvaluator' is a wrapper for a function that evaluates conditions. +--} newtype ConditionEvaluator level = ConditionEvaluator - (UnevaluatedCondition level -> IntCounter (EvaluatedCondition level)) + ( UnevaluatedCondition level + -> IntCounter (EvaluatedCondition level, ConditionProof level) + ) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs index e7a7b92cae..a711c1c0a9 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs @@ -2,7 +2,7 @@ {-# LANGUAGE LambdaCase #-} {-| Module : Data.Kore.Step.Function.Evaluator -Description : Evaluates functions in a pattern +Description : Evaluates functions in a pattern. Copyright : (c) Runtime Verification, 2018 License : UIUC/NCSA Maintainer : virgil.serbanuta@runtimeverification.com @@ -18,7 +18,6 @@ import qualified Data.Map as Map import Data.Kore.AST.Common (Application (..), Id (..), Pattern (..), - Sort (..), SymbolOrAlias (..), Variable) import Data.Kore.AST.MLPatterns (MLBinderPatternClass (..), @@ -30,30 +29,37 @@ import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern) import Data.Kore.FixTraversals (fixTopDownVisitor) import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) -import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), +import Data.Kore.Step.Condition.Condition (ConditionProof (..), + ConditionSort (..), + EvaluatedCondition (..), makeEvaluatedAnd) import Data.Kore.Step.Condition.Evaluator (evaluateFunctionCondition) import Data.Kore.Step.Function.Data (ApplicationFunctionEvaluator (..), + AttemptedFunctionResult (..), CommonPurePatternFunctionEvaluator (..), ConditionEvaluator (..), - FunctionEvaluation (..), - FunctionResult (..)) + FunctionResult (..), + FunctionResultProof (..)) import Data.Kore.Variables.Fresh.IntCounter (IntCounter) -import Debug.Trace - -multiTrace :: [String] -> a -> a -multiTrace [] a = a -multiTrace (x:xs) a = trace x $ multiTrace xs a +{-|'evaluateFunctions' evaluates Kore functions (in a bottom-up manner). +It currently assumes that functions are unambiguous. Patterns that are not +applications of functional constructors may prevent function evaluation in +various ways. +-} evaluateFunctions :: MetadataTools level + -- ^ Defines what is a function and what is not. -> Map.Map (Id level) [ApplicationFunctionEvaluator level] - -> Sort level + -- ^ Map from a symbol's ID to all the function definitions for that symbol. + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> CommonPurePattern level - -> IntCounter (FunctionResult level) + -- ^ Pattern on which to evaluate functions + -> IntCounter (FunctionResult level, FunctionResultProof level) evaluateFunctions metadataTools functionIdToEvaluator conditionSort = - trace "Evaluate functions" $ fixTopDownVisitor (filterUnhandledPatterns metadataTools) (evaluateLocalFunction @@ -69,30 +75,40 @@ evaluateFunctions metadataTools functionIdToEvaluator conditionSort = functionEvaluator = evaluateFunctions metadataTools functionIdToEvaluator conditionSort +{--| 'FilterWrapper' adapts the natural result of filtering patterns to +the interface expected by 'applyPatternLeveledFunction' +--} newtype FilterWrapper level = FilterWrapper - { filterUnwrap :: Either (IntCounter (FunctionResult level)) (UnFixedPureMLPattern level Variable) + { filterUnwrap + :: Either + (IntCounter (FunctionResult level, FunctionResultProof level)) + (UnFixedPureMLPattern level Variable) } +{--|'filterUnhandledPatterns' rejects everything that is not an application of +a constructor or a function. +--} filterUnhandledPatterns :: MetadataTools level -> Pattern level Variable (CommonPurePattern level) -> Either - (IntCounter (FunctionResult level)) + (IntCounter (FunctionResult level, FunctionResultProof level)) (UnFixedPureMLPattern level Variable) filterUnhandledPatterns metadataTools patt = filterUnwrap (applyPatternLeveledFunction PatternLeveledFunction { patternLeveledFunctionML = wrapUnchanged . mlPatternToPattern - , patternLeveledFunctionMLBinder = wrapUnchanged . mlBinderPatternToPattern + , patternLeveledFunctionMLBinder = + wrapUnchanged . mlBinderPatternToPattern , stringLeveledFunction = wrapUnchanged . StringLiteralPattern , charLeveledFunction = wrapUnchanged . CharLiteralPattern , applicationLeveledFunction = \ app@Application {applicationSymbolOrAlias = symbol} -> - trace ("Hi " ++ getId (symbolOrAliasConstructor symbol)) $ - if isConstructor metadataTools symbol || isFunction metadataTools symbol - then trace "Right" $ FilterWrapper $ Right $ ApplicationPattern app - else trace "Left" $ wrapUnchanged $ ApplicationPattern app + if isConstructor metadataTools symbol + || isFunction metadataTools symbol + then FilterWrapper $ Right $ ApplicationPattern app + else wrapUnchanged $ ApplicationPattern app , variableLeveledFunction = wrapUnchanged . VariablePattern } patt @@ -102,21 +118,35 @@ filterUnhandledPatterns metadataTools patt = :: Pattern level Variable (CommonPurePattern level) -> FilterWrapper level wrapUnchanged patt' = - FilterWrapper $ Left $ return FunctionResult - { functionResultPattern = asPurePattern patt' - , functionResultCondition = ConditionTrue - } + FilterWrapper $ Left $ return + ( FunctionResult + { functionResultPattern = asPurePattern patt' + , functionResultCondition = ConditionTrue + } + , FunctionResultProof + ) +{--| 'EvaluationWrapper' adapts the natural result of evaluating functions +the interface expected by 'applyPatternLeveledFunction' +--} newtype EvaluationWrapper level = EvaluationWrapper - { evaluationUnwrap :: IntCounter (FunctionResult level) } + { evaluationUnwrap + :: IntCounter (FunctionResult level, FunctionResultProof level) + } +{--| 'evaluateLocalFunction' assumes that a pattern's children have been +evaluated and evaluates the pattern. +--} evaluateLocalFunction :: ConditionEvaluator level -> CommonPurePatternFunctionEvaluator level -> Map.Map (Id level) [ApplicationFunctionEvaluator level] - -> Sort level -- TODO: Wrap in a type. - -> Pattern level Variable (IntCounter (FunctionResult level)) - -> IntCounter (FunctionResult level) + -> ConditionSort level + -> Pattern + level + Variable + (IntCounter (FunctionResult level, FunctionResultProof level)) + -> IntCounter (FunctionResult level, FunctionResultProof level) evaluateLocalFunction conditionEvaluator functionEvaluator @@ -126,18 +156,19 @@ evaluateLocalFunction = do pattF <- sequenceA pattIF let - childrenCondition = + (childrenCondition, _) = foldr - (makeEvaluatedAnd conditionSort) - ConditionTrue - (fmap functionResultCondition pattF) - normalPattern = fmap functionResultPattern pattF + (andChildrenConditions conditionSort) + (ConditionTrue, FunctionResultProof) + (fmap (functionResultCondition . fst) pattF) + normalPattern = fmap (functionResultPattern . fst) pattF unchanged = returnUnchanged childrenCondition evaluationUnwrap ( applyPatternLeveledFunction PatternLeveledFunction { patternLeveledFunctionML = unchanged . mlPatternToPattern - , patternLeveledFunctionMLBinder = unchanged . mlBinderPatternToPattern + , patternLeveledFunctionMLBinder = + unchanged . mlBinderPatternToPattern , stringLeveledFunction = assertTrue childrenCondition . returnUnchanged ConditionTrue @@ -163,21 +194,45 @@ evaluateLocalFunction -> Pattern level Variable (CommonPurePattern level) -> EvaluationWrapper level returnUnchanged condition patt = - EvaluationWrapper $ return FunctionResult - { functionResultPattern = asPurePattern patt - , functionResultCondition = condition - } + EvaluationWrapper $ return + ( FunctionResult + { functionResultPattern = asPurePattern patt + , functionResultCondition = condition + } + , FunctionResultProof + ) assertTrue :: EvaluatedCondition level -> a -> a assertTrue ConditionTrue x = x assertTrue _ _ = error "Expecting the condition to be true." +{--| 'andChildrenConditions' combines two children's conditions. +--} +andChildrenConditions + :: ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. + -> EvaluatedCondition level + -> (EvaluatedCondition level, FunctionResultProof level) + -> (EvaluatedCondition level, FunctionResultProof level) +andChildrenConditions conditionSort first (second, _) = + (fst (makeEvaluatedAnd conditionSort first second), FunctionResultProof) + +{--| 'evaluateApplication' - evaluates functions on an application pattern. +--} evaluateApplication :: ConditionEvaluator level + -- ^ Evaluates conditions -> CommonPurePatternFunctionEvaluator level + -- ^ Evaluates functions. -> Map.Map (Id level) [ApplicationFunctionEvaluator level] - -> Sort level + -- ^ Map from symbol IDs to defined functions + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> EvaluatedCondition level + -- ^ Aggregated children condition. -> Application level (CommonPurePattern level) + -- ^ The pattern to be evaluated -> EvaluationWrapper level evaluateApplication conditionEvaluator @@ -187,34 +242,48 @@ evaluateApplication childrenCondition app @ Application { applicationSymbolOrAlias = SymbolOrAlias - -- TODO: Also use the symbolOrAliasParams. + -- TODO(virgil): Should we use the symbolOrAliasParams? Should + -- not matter for correctness since each function can reject the + -- input, and it would be more complex to handle them properly. { symbolOrAliasConstructor = symbolId } } - = trace "evaluate-application" $ - EvaluationWrapper $ + = EvaluationWrapper $ case Map.lookup symbolId symbolIdToEvaluator of Nothing -> return unchanged Just evaluators -> do results <- mapM (applyEvaluator app) evaluators mergedResults <- - mapM (mergeWithCondition conditionEvaluator conditionSort childrenCondition) results - -- TODO: nub is O(n^2), should do better than that - trace (show results) $ case nub (filter notNotApplicable mergedResults) of + mapM + (mergeWithCondition + conditionEvaluator conditionSort childrenCondition + ) + results + -- After removing N/A results and duplicates we expect at most + -- one result, i.e. we don't handle ambiguity + -- TODO(virgil): nub is O(n^2), should do better than that. + case nub (filter notNotApplicable mergedResults) of [] -> return unchanged - [NotApplicable] -> error "Should not reach this line." - [Symbolic condition] -> - return FunctionResult - { functionResultPattern = - asPurePattern $ ApplicationPattern app - , functionResultCondition = condition - } - [Applied functionResult] -> trace ("evaluate-application " ++ show functionResult) $ return functionResult + [(NotApplicable, _)] -> error "Should not reach this line." + [(Symbolic condition, proof)] -> + return + ( FunctionResult + { functionResultPattern = + asPurePattern $ ApplicationPattern app + , functionResultCondition = condition + } + , proof + ) + [(Applied functionResult, proof)] -> + return (functionResult, proof) (_ : _ : _) -> error "Not implemented yet." where - unchanged = FunctionResult - { functionResultPattern = asPurePattern $ ApplicationPattern app - , functionResultCondition = childrenCondition - } + unchanged = + ( FunctionResult + { functionResultPattern = asPurePattern $ ApplicationPattern app + , functionResultCondition = childrenCondition + } + , FunctionResultProof + ) applyEvaluator app' (ApplicationFunctionEvaluator evaluator) = evaluator conditionEvaluator @@ -222,29 +291,42 @@ evaluateApplication app' notNotApplicable = \case - NotApplicable -> False + (NotApplicable, _) -> False _ -> True +{--| 'mergeWithCondition' ands the given condition to the given function +evaluation. +--} mergeWithCondition :: ConditionEvaluator level - -> Sort level + -- ^ Can evaluate conditions. + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> EvaluatedCondition level - -> FunctionEvaluation level - -> IntCounter (FunctionEvaluation level) -mergeWithCondition _ _ _ NotApplicable = return NotApplicable -mergeWithCondition conditionEvaluator conditionSort toMerge (Symbolic condition) - = trace ("mergeWithCondition - Symbolic: " ++ show toMerge) $ do - mergedCondition <- + -- ^ Condition to add. + -> (AttemptedFunctionResult level, FunctionResultProof level) + -- ^ AttemptedFunctionResult to which the condition should be added. + -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) +mergeWithCondition _ _ _ (NotApplicable, _) = + return (NotApplicable, FunctionResultProof) +mergeWithCondition + conditionEvaluator + conditionSort + toMerge + (Symbolic condition, _) + = do + (mergedCondition, _) <- mergeConditions conditionEvaluator conditionSort condition toMerge case mergedCondition of - ConditionFalse -> return NotApplicable - _ -> return $ Symbolic mergedCondition + ConditionFalse -> return (NotApplicable, FunctionResultProof) + _ -> return (Symbolic mergedCondition, FunctionResultProof) mergeWithCondition conditionEvaluator conditionSort toMerge - (Applied functionResult) - = multiTrace ["mergeWithCondition - Applied: ", " " ++ show toMerge, " " ++ show (functionResultCondition functionResult), " " ++ show (functionResultPattern functionResult)] $ do + (Applied functionResult, _) + = do mergedCondition <- mergeConditions conditionEvaluator @@ -252,18 +334,26 @@ mergeWithCondition (functionResultCondition functionResult) toMerge case mergedCondition of - ConditionFalse -> return NotApplicable - _ -> trace ("mergeWithCondition - Applied: " ++ show mergedCondition) $ return $ - Applied functionResult {functionResultCondition = mergedCondition} + (ConditionFalse, _) -> return (NotApplicable, FunctionResultProof) + _ -> return + ( Applied functionResult + {functionResultCondition = fst mergedCondition} + , FunctionResultProof + ) +{--| 'mergeConditions' merges two conditions with an 'and'. +--} mergeConditions :: ConditionEvaluator level - -> Sort level + -- ^ Can evaluate conditions. + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> EvaluatedCondition level -> EvaluatedCondition level - -> IntCounter (EvaluatedCondition level) + -> IntCounter (EvaluatedCondition level, ConditionProof level) mergeConditions _ conditionSort first second = return $ makeEvaluatedAnd conditionSort first second - -- TODO: Should be something like: + -- TODO(virgil): Should be something like: -- conditionEvaluator (makeEvaluatedAnd conditionSort first second) -- but, right now, we don't have conditions which are partly satisfiable. diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs index 49b1d28c3b..ca08eaf92e 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs @@ -1,7 +1,7 @@ {-# LANGUAGE GADTs #-} {-| Module : Data.Kore.Step.Function.UserDefined -Description : Evaluates user-defined functions in a pattern +Description : Evaluates user-defined functions in a pattern. Copyright : (c) Runtime Verification, 2018 License : UIUC/NCSA Maintainer : virgil.serbanuta@runtimeverification.com @@ -14,33 +14,44 @@ module Data.Kore.Step.Function.UserDefined ) where import Data.Kore.AST.Common (Application (..), - Pattern (..), Sort (..), - Top (..)) + Pattern (..), Top (..)) import Data.Kore.AST.MetaOrObject (MetaOrObject) import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern) import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) import Data.Kore.Step.BaseStep (AxiomPattern, StepperConfiguration (..), stepWithAxiom) -import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..), UnevaluatedCondition (..), +import Data.Kore.Step.Condition.Condition (ConditionSort (..), + EvaluatedCondition (..), + UnevaluatedCondition (..), makeEvaluatedAnd) -import Data.Kore.Step.Function.Data (CommonPurePatternFunctionEvaluator (..), +import Data.Kore.Step.Function.Data (AttemptedFunctionResult (..), + CommonPurePatternFunctionEvaluator (..), ConditionEvaluator (..), - FunctionEvaluation (..), - FunctionResult (..)) + FunctionResult (..), + FunctionResultProof (..)) import Data.Kore.Variables.Fresh.IntCounter (IntCounter) -import Debug.Trace +{--| 'axiomFunctionEvaluator' evaluates a user-defined function. After +evaluating the function, it tries to re-evaluate all functions on the result. +The function is assumed to be defined through an axiom. +--} axiomFunctionEvaluator :: MetaOrObject level => MetadataTools level - -> Sort level + -> ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> AxiomPattern level + -- ^ Axiom defining the current function. -> ConditionEvaluator level + -- ^ Evaluates conditions -> CommonPurePatternFunctionEvaluator level + -- ^ Evaluates functions in patterns -> Application level (CommonPurePattern level) - -> IntCounter (FunctionEvaluation level) + -- ^ The function on which to evaluate the current function. + -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) axiomFunctionEvaluator metadataTools conditionSort @@ -48,12 +59,10 @@ axiomFunctionEvaluator (ConditionEvaluator conditionEvaluator) functionEvaluator app - = trace "axiomFunctionEvaluator" $ + = case stepResult of - Left err -> do - e <- err - trace ("axiomFunctionEvaluator-Left " ++ show e) $ return NotApplicable - Right configurationWithProof -> trace "axiomFunctionEvaluator-Right" $ + Left _ -> return (NotApplicable, FunctionResultProof) + Right configurationWithProof -> do ( StepperConfiguration { stepperConfigurationPattern = rewrittenPattern @@ -61,10 +70,11 @@ axiomFunctionEvaluator } , _ ) <- configurationWithProof - evaluatedRewritingCondition <- + -- TODO(virgil): Get the step substitution and use it on the + -- condition. + (evaluatedRewritingCondition, _) <- conditionEvaluator (UnevaluatedCondition rewritingCondition) - axiomFunctionEvaluatorAfterStep - metadataTools + reevaluateFunctions conditionSort functionEvaluator FunctionResult @@ -78,24 +88,31 @@ axiomFunctionEvaluator (stepperConfiguration conditionSort app) axiom stepperConfiguration - :: Sort level + :: ConditionSort level -> Application level (CommonPurePattern level) -> StepperConfiguration level - stepperConfiguration conditionSort' app' = StepperConfiguration - { stepperConfigurationPattern = asPurePattern $ ApplicationPattern app' - , stepperConfigurationCondition = - asPurePattern $ TopPattern $ Top conditionSort' - , stepperConfigurationConditionSort = conditionSort' - } + stepperConfiguration conditionSort'@(ConditionSort sort) app' = + StepperConfiguration + { stepperConfigurationPattern = + asPurePattern $ ApplicationPattern app' + , stepperConfigurationCondition = + asPurePattern $ TopPattern $ Top sort + , stepperConfigurationConditionSort = conditionSort' + } -axiomFunctionEvaluatorAfterStep - :: MetadataTools level - -> Sort level +{--| 'reevaluateFunctions' re-evaluates functions after a user-defined function +was evaluated. +--} +reevaluateFunctions + :: ConditionSort level + -- ^ Sort used for conditions. This function assumes that all conditions + -- have this sort and will use it to create new conditions. -> CommonPurePatternFunctionEvaluator level + -- ^ Evaluates functions in patterns. -> FunctionResult level - -> IntCounter (FunctionEvaluation level) -axiomFunctionEvaluatorAfterStep - _ + -- ^ Function evaluation result. + -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) +reevaluateFunctions conditionSort (CommonPurePatternFunctionEvaluator functionEvaluator) FunctionResult @@ -103,60 +120,48 @@ axiomFunctionEvaluatorAfterStep , functionResultCondition = rewritingCondition } = case rewritingCondition of - ConditionFalse -> return NotApplicable + ConditionFalse -> return (NotApplicable, FunctionResultProof) _ -> do - FunctionResult + ( FunctionResult { functionResultPattern = simplifiedPattern , functionResultCondition = simplificationCondition - } <- functionEvaluator rewrittenPattern - return $ resultFromSimplification - conditionSort - simplifiedPattern - --TODO: Maybe call a ConditionEvaluator - (makeEvaluatedAnd conditionSort rewritingCondition simplificationCondition) - rewrittenPattern - rewritingCondition + } + , _ + ) <- functionEvaluator rewrittenPattern + return + ( firstSatisfiablePattern + [ ( simplifiedPattern + -- TODO(virgil): Maybe evaluate the 'and' + , fst $ makeEvaluatedAnd + conditionSort + rewritingCondition + simplificationCondition + ) + , (rewrittenPattern, rewritingCondition) + ] + , FunctionResultProof + ) -resultFromSimplification - :: Sort level - -> CommonPurePattern level - -> EvaluatedCondition level - -> CommonPurePattern level - -> EvaluatedCondition level - -> FunctionEvaluation level -resultFromSimplification - _ simplifiedPattern ConditionTrue _ _ +{--| Returns the first pattern if its condition might be satisfiable, otherwise +returns the second. Assumes that at least one pattern might be satisfiable. +--} +firstSatisfiablePattern + :: [(CommonPurePattern level, EvaluatedCondition level)] + -> AttemptedFunctionResult level +firstSatisfiablePattern + ((patt, ConditionTrue) : _) = Applied FunctionResult - { functionResultPattern = simplifiedPattern + { functionResultPattern = patt , functionResultCondition = ConditionTrue } -resultFromSimplification - _ - simplifiedPattern - simplificationCondition @ (ConditionUnevaluable _) - _ _ - = Applied FunctionResult - { functionResultPattern = simplifiedPattern - , functionResultCondition = simplificationCondition - } -resultFromSimplification - _ _ - ConditionFalse - rewrittenPattern - ConditionTrue +firstSatisfiablePattern + ((patt, condition @ (ConditionUnevaluable _)) : _) = Applied FunctionResult - { functionResultPattern = rewrittenPattern - , functionResultCondition = ConditionTrue - } -resultFromSimplification - _ _ - ConditionFalse - rewrittenPattern - rewritingCondition @ (ConditionUnevaluable _) - = Applied FunctionResult - { functionResultPattern = rewrittenPattern - , functionResultCondition = rewritingCondition + { functionResultPattern = patt + , functionResultCondition = condition } -resultFromSimplification - _ _ ConditionFalse _ ConditionFalse - = error "Unexpected case." +firstSatisfiablePattern + ((_, ConditionFalse) : reminder) + = firstSatisfiablePattern reminder +firstSatisfiablePattern [] = + error "Unexpected case." diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs index bcd8df3d65..5561e41980 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs @@ -767,3 +767,17 @@ instance EqualWithExplanation (EvaluatedCondition level) where compareWithExplanation = sumCompareWithExplanation printWithExplanation = show + + +instance SumEqualWithExplanation (ConditionSort level) + where + sumConstructorPair + (ConditionSort a1) (ConditionSort a2) + = + SumConstructorSameWithArguments + (EqWrap "ConditionSort" a1 a2) + +instance EqualWithExplanation (ConditionSort level) + where + compareWithExplanation = sumCompareWithExplanation + printWithExplanation = show diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs index 0c63eeb120..fbed53690d 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/BaseStepTest.hs @@ -10,6 +10,7 @@ import Data.Kore.AST.Common (Application (..), AstLocation (..), Id (..), Pattern (ApplicationPattern), + Sort, SymbolOrAlias (..), Variable) import Data.Kore.AST.MetaOrObject @@ -21,6 +22,7 @@ import Data.Kore.Comparators () import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) import Data.Kore.MetaML.AST (CommonMetaPattern) import Data.Kore.Step.BaseStep +import Data.Kore.Step.Condition.Condition (ConditionSort (..)) import Data.Kore.Step.Error import Data.Kore.Unification.Error import Data.Kore.Unification.Unifier (FunctionalProof (..), @@ -39,7 +41,8 @@ baseStepTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -67,7 +70,8 @@ baseStepTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -82,7 +86,8 @@ baseStepTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (y1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -110,7 +115,8 @@ baseStepTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (y1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -125,7 +131,8 @@ baseStepTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -165,7 +172,8 @@ baseStepTests = { stepperConfigurationPattern = asPureMetaPattern (metaSigma (v1 PatternSort) (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -185,7 +193,8 @@ baseStepTests = { stepperConfigurationPattern = asPureMetaPattern (metaF (b1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -239,7 +248,8 @@ baseStepTests = (a1 PatternSort) (metaF (b1 PatternSort)) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -259,7 +269,8 @@ baseStepTests = { stepperConfigurationPattern = asPureMetaPattern (metaF (b1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -317,7 +328,8 @@ baseStepTests = (metaF (a1 PatternSort)) (metaF (b1 PatternSort)) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -348,7 +360,8 @@ baseStepTests = { stepperConfigurationPattern = asPureMetaPattern (metaSigma (b1 PatternSort) (b1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -432,7 +445,8 @@ baseStepTests = (a1 PatternSort) ) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -465,7 +479,8 @@ baseStepTests = (var_0 PatternSort) (a1 PatternSort) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -496,7 +511,8 @@ baseStepTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (a1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -526,7 +542,8 @@ baseStepTests = (metaG (a1 PatternSort)) (metaF (b1 PatternSort)) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -563,7 +580,8 @@ baseStepTests = (a1 PatternSort) (b1 PatternSort) ) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -642,7 +660,7 @@ baseStepTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (var PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -687,7 +705,7 @@ baseStepTests = (var PatternSort) (var PatternSort) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = conditionSort SortSort , stepperConfigurationCondition = top SortSort } AxiomPattern @@ -698,6 +716,8 @@ baseStepTests = } ) +conditionSort :: AsAst (Sort level) s => s -> ConditionSort level +conditionSort sort = ConditionSort (asAst sort) mockMetadataTools :: MetadataTools Meta mockMetadataTools = MetadataTools diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs index 2ec3f43870..84dd6f5f61 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} module Data.Kore.Step.Function.IntegrationTest (functionIntegrationTests) where @@ -23,12 +24,14 @@ import Data.Kore.Building.Sorts import Data.Kore.Comparators () import Data.Kore.MetaML.AST (CommonMetaPattern) import Data.Kore.Step.BaseStep (AxiomPattern (..)) -import Data.Kore.Step.Condition.Condition (EvaluatedCondition (..)) +import Data.Kore.Step.Condition.Condition (ConditionSort (..), + EvaluatedCondition (..)) import Data.Kore.Step.Function.Data (ApplicationFunctionEvaluator (..), + AttemptedFunctionResult (..), CommonPurePatternFunctionEvaluator, ConditionEvaluator, - FunctionEvaluation (..), - FunctionResult (..)) + FunctionResult (..), + FunctionResultProof (..)) import Data.Kore.Step.Function.Evaluator (evaluateFunctions) import Data.Kore.Step.Function.UserDefined (axiomFunctionEvaluator) import Data.Kore.Variables.Fresh.IntCounter (IntCounter, @@ -49,42 +52,33 @@ functionIntegrationTests = (evaluate mockMetadataTools (Map.singleton fId - [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern (metaF (v1 PatternSort)) - , axiomPatternRight = - asPureMetaPattern (metaG (v1 PatternSort)) - } + [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern (metaF (v1 PatternSort))) + (asPureMetaPattern (metaG (v1 PatternSort))) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF metaC)) ) ) , testCase "Evaluates inside functions" (assertEqualWithExplanation "" FunctionResult - { functionResultPattern = asPureMetaPattern (metaG (metaG metaC)) + { functionResultPattern = + asPureMetaPattern (metaG (metaG metaC)) , functionResultCondition = ConditionTrue } (evaluate mockMetadataTools (Map.singleton fId - [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern (metaF (v1 PatternSort)) - , axiomPatternRight = - asPureMetaPattern (metaG (v1 PatternSort)) - } + [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern (metaF (v1 PatternSort))) + (asPureMetaPattern (metaG (v1 PatternSort))) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF (metaF metaC))) ) ) @@ -98,18 +92,13 @@ functionIntegrationTests = (evaluate mockMetadataTools (Map.singleton fId - [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern (metaF (v1 PatternSort)) - , axiomPatternRight = - asPureMetaPattern (metaG (v1 PatternSort)) - } + [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern (metaF (v1 PatternSort))) + (asPureMetaPattern (metaG (v1 PatternSort))) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF (metaOr PatternSort (metaF metaC) (metaF metaC))) ) @@ -125,18 +114,13 @@ functionIntegrationTests = (evaluate mockMetadataTools (Map.singleton fId - [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern (metaF (v1 PatternSort)) - , axiomPatternRight = - asPureMetaPattern (metaG (v1 PatternSort)) - } + [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern (metaF (v1 PatternSort))) + (asPureMetaPattern (metaG (v1 PatternSort))) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF (metaSigma (metaF metaC) (metaF metaC))) ) @@ -146,73 +130,77 @@ functionIntegrationTests = (assertEqualWithExplanation "" FunctionResult { functionResultPattern = asPureMetaPattern (metaF metaD) - , functionResultCondition = ConditionUnevaluable (asPureMetaPattern metaC) + , functionResultCondition = conditionUnevaluable metaC } (evaluate mockMetadataTools (Map.singleton cId - [ ApplicationFunctionEvaluator $ mockEvaluator - (Applied FunctionResult - { functionResultPattern = asPureMetaPattern metaD - , functionResultCondition = - ConditionUnevaluable (asPureMetaPattern metaC) - } - ) + [ appliedMockEvaluator FunctionResult + { functionResultPattern = asPureMetaPattern metaD + , functionResultCondition = + conditionUnevaluable metaC + } ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF metaC)) ) ) , testCase "Merges conditions" (assertEqualWithExplanation "" FunctionResult - { functionResultPattern = asPureMetaPattern (metaG (metaSigma metaE metaE)) + { functionResultPattern = + asPureMetaPattern (metaG (metaSigma metaE metaE)) , functionResultCondition = - ConditionUnevaluable $ asPureMetaPattern + conditionUnevaluable (metaAnd SortSort - (metaCeil (ResultSort SortSort) PatternSort metaC) - (metaCeil (ResultSort SortSort) PatternSort metaD) + (metaCeil + (ResultSort SortSort) PatternSort metaC + ) + (metaCeil + (ResultSort SortSort) PatternSort metaD + ) ) } (evaluate mockMetadataTools (Map.fromList [ ( cId - , [ ApplicationFunctionEvaluator $ mockEvaluator - (Applied FunctionResult - { functionResultPattern = asPureMetaPattern metaE - , functionResultCondition = - ConditionUnevaluable (asPureMetaPattern (metaCeil (ResultSort SortSort) PatternSort metaC)) - } - ) + , [ appliedMockEvaluator FunctionResult + { functionResultPattern = + asPureMetaPattern metaE + , functionResultCondition = + conditionUnevaluable + (metaCeil + (ResultSort SortSort) + PatternSort + metaC) + } ] ) , ( dId - , [ ApplicationFunctionEvaluator $ mockEvaluator - (Applied FunctionResult - { functionResultPattern = asPureMetaPattern metaE - , functionResultCondition = - ConditionUnevaluable (asPureMetaPattern (metaCeil (ResultSort SortSort) PatternSort metaD)) - } - ) + , [ appliedMockEvaluator FunctionResult + { functionResultPattern = + asPureMetaPattern metaE + , functionResultCondition = + conditionUnevaluable + (metaCeil + (ResultSort SortSort) + PatternSort + metaD) + } ] ) , (fId - , [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern (metaF (v1 PatternSort)) - , axiomPatternRight = - asPureMetaPattern (metaG (v1 PatternSort)) - } + , [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern (metaF (v1 PatternSort))) + (asPureMetaPattern (metaG (v1 PatternSort))) ] ) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF (metaSigma metaC metaD))) ) ) @@ -220,81 +208,90 @@ functionIntegrationTests = (assertEqualWithExplanation "" FunctionResult { functionResultPattern = asPureMetaPattern (metaF metaE) - , functionResultCondition = ConditionUnevaluable (asPureMetaPattern metaD) + , functionResultCondition = conditionUnevaluable metaD } (evaluate mockMetadataTools (Map.fromList [ ( cId - , [ ApplicationFunctionEvaluator $ axiomFunctionEvaluator - mockMetadataTools - (asAst SortSort) - AxiomPattern - { axiomPatternLeft = - asPureMetaPattern metaC - , axiomPatternRight = - asPureMetaPattern metaD - } + , [ axiomEvaluator + (conditionSort SortSort) + (asPureMetaPattern metaC) + (asPureMetaPattern metaD) ] ) , ( dId - , [ ApplicationFunctionEvaluator $ mockEvaluator - (Applied FunctionResult - { functionResultPattern = asPureMetaPattern metaE - , functionResultCondition = - ConditionUnevaluable (asPureMetaPattern metaD) - } - ) + , [ appliedMockEvaluator FunctionResult + { functionResultPattern = + asPureMetaPattern metaE + , functionResultCondition = + conditionUnevaluable metaD + } ] ) ] ) - (asAst SortSort) + (conditionSort SortSort) (asPureMetaPattern (metaF metaC)) ) ) ] +axiomEvaluator + :: ConditionSort Meta + -> CommonPurePattern Meta + -> CommonPurePattern Meta + -> ApplicationFunctionEvaluator Meta +axiomEvaluator sort left right = + ApplicationFunctionEvaluator + (axiomFunctionEvaluator + mockMetadataTools + sort + AxiomPattern + { axiomPatternLeft = left + , axiomPatternRight = right + } + ) + +conditionSort :: AsAst (Sort level) s => s -> ConditionSort level +conditionSort sort = ConditionSort (asAst sort) + +appliedMockEvaluator + :: FunctionResult level -> ApplicationFunctionEvaluator level +appliedMockEvaluator result = + ApplicationFunctionEvaluator (mockEvaluator (Applied result)) + mockEvaluator - :: FunctionEvaluation level + :: AttemptedFunctionResult level -> ConditionEvaluator level -> CommonPurePatternFunctionEvaluator level -> Application level (CommonPurePattern level) - -> IntCounter (FunctionEvaluation level) + -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) mockEvaluator evaluation _ _ _ = - return evaluation + return (evaluation, FunctionResultProof) evaluate :: MetadataTools level -> Map.Map (Id level) [ApplicationFunctionEvaluator level] - -> Sort level + -> ConditionSort level -> CommonPurePattern level -> FunctionResult level -evaluate metadataTools functionIdToEvaluator conditionSort patt = - fst +evaluate metadataTools functionIdToEvaluator conditionSort' patt = + fst $ fst (runIntCounter (evaluateFunctions - metadataTools functionIdToEvaluator conditionSort patt + metadataTools functionIdToEvaluator conditionSort' patt ) 0 ) v1 :: MetaSort sort => sort -> MetaVariable sort v1 = metaVariable "#v1" AstLocationTest -a1 :: MetaSort sort => sort -> MetaVariable sort -a1 = metaVariable "#a1" AstLocationTest -b1 :: MetaSort sort => sort -> MetaVariable sort -b1 = metaVariable "#b1" AstLocationTest -x1 :: MetaSort sort => sort -> MetaVariable sort -x1 = metaVariable "#x1" AstLocationTest -y1 :: MetaSort sort => sort -> MetaVariable sort -y1 = metaVariable "#y1" AstLocationTest -var_0 :: MetaSort sort => sort -> MetaVariable sort -var_0 = metaVariable "#var_0" AstLocationTest -var_1 :: MetaSort sort => sort -> MetaVariable sort -var_1 = metaVariable "#var_1" AstLocationTest -top :: MetaSort sort => sort -> CommonMetaPattern -top sort = asPureMetaPattern $ metaTop sort + +conditionUnevaluable + :: ProperPattern Meta sort patt => patt -> EvaluatedCondition Meta +conditionUnevaluable patt = + ConditionUnevaluable (asPureMetaPattern patt) asPureMetaPattern :: ProperPattern Meta sort patt => patt -> CommonMetaPattern diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs index af10f8c7e5..8152b6bb0c 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/StepTest.hs @@ -10,6 +10,7 @@ import Data.Kore.AST.Common (Application (..), AstLocation (..), Id (..), Pattern (ApplicationPattern), + Sort, SymbolOrAlias (..), Variable) import Data.Kore.AST.MetaOrObject @@ -21,6 +22,7 @@ import Data.Kore.Comparators () import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) import Data.Kore.MetaML.AST (CommonMetaPattern) import Data.Kore.Step.BaseStep +import Data.Kore.Step.Condition.Condition (ConditionSort (..)) import Data.Kore.Step.Step import Data.Kore.Unification.Unifier (FunctionalProof (..), UnificationProof (..)) @@ -63,7 +65,8 @@ singleStepTests = [ ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -91,7 +94,8 @@ singleStepTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -111,7 +115,8 @@ singleStepTests = [ ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -140,7 +145,8 @@ singleStepTests = (v1 PatternSort) (v1 PatternSort) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -168,7 +174,8 @@ singleStepTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (v1 PatternSort) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -202,7 +209,8 @@ singleStepTests = (metaG (a1 PatternSort)) (metaF (b1 PatternSort)) ) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -229,7 +237,7 @@ multipleStepPickFirstTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaG (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -263,7 +271,8 @@ multipleStepPickFirstTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaF (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -284,7 +293,7 @@ multipleStepPickFirstTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaH (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -339,7 +348,8 @@ multipleStepPickFirstTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaF (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -366,7 +376,7 @@ multipleStepPickFirstTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaG (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaAnd @@ -400,7 +410,8 @@ multipleStepPickFirstTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaF (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -427,7 +438,8 @@ multipleStepPickFirstTests = ( StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaF (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = asPureMetaPattern (metaTop SortSort) } @@ -439,7 +451,8 @@ multipleStepPickFirstTests = StepperConfiguration { stepperConfigurationPattern = asPureMetaPattern (metaF (v1 PatternSort)) - , stepperConfigurationConditionSort = asAst SortSort + , stepperConfigurationConditionSort = + conditionSort SortSort , stepperConfigurationCondition = top SortSort } [ AxiomPattern @@ -459,6 +472,9 @@ multipleStepPickFirstTests = ) ] +conditionSort :: AsAst (Sort level) s => s -> ConditionSort level +conditionSort sort = ConditionSort (asAst sort) + mockMetadataTools :: MetadataTools Meta mockMetadataTools = MetadataTools { isConstructor = const True From 25d58dd8edce84a54e59feacf5fdcbc384db6363 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Mon, 2 Jul 2018 18:02:47 +0300 Subject: [PATCH 05/10] Fix merge errors. --- .../language-kore/src/Data/Kore/Step/BaseStep.hs | 11 +---------- .../parser/Data/Kore/Step/Function/IntegrationTest.hs | 6 +++++- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs index f9b308f8c6..a18450daf7 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/BaseStep.hs @@ -32,8 +32,8 @@ import Data.Kore.AST.PureML (CommonPurePatt mapPatternVariables) import Data.Kore.FixTraversals (fixBottomUpVisitor) import Data.Kore.IndexedModule.MetadataTools (MetadataTools) -import Data.Kore.Step.Condition.Condition (ConditionSort (..)) import Data.Kore.Step.AxiomPatterns +import Data.Kore.Step.Condition.Condition (ConditionSort (..)) import Data.Kore.Step.Error import Data.Kore.Substitution.Class (Hashable (..), PatternSubstitutionClass (..)) import qualified Data.Kore.Substitution.List as ListSubstitution @@ -48,15 +48,6 @@ import Data.Kore.Variables.Fresh.IntCounter (IntCounter) import Data.Kore.Variables.Int (IntVariable (..)) import Data.Maybe (fromMaybe) -{--| 'AxiomPattern' is a rewriting axiom in a normalized form. Right now -it can only represent axioms that look like left-pattern => right-pattern. ---} -data AxiomPattern level = AxiomPattern - { axiomPatternLeft :: !(CommonPurePattern level) - , axiomPatternRight :: !(CommonPurePattern level) - } - deriving (Show, Eq) - {--| 'StepperConfiguration' represents the configuration to which a rewriting axiom is applied. diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs index 84dd6f5f61..7019d864b9 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs @@ -22,6 +22,7 @@ import Data.Kore.Building.AsAst import Data.Kore.Building.Patterns import Data.Kore.Building.Sorts import Data.Kore.Comparators () +import Data.Kore.Error (printError) import Data.Kore.MetaML.AST (CommonMetaPattern) import Data.Kore.Step.BaseStep (AxiomPattern (..)) import Data.Kore.Step.Condition.Condition (ConditionSort (..), @@ -295,7 +296,10 @@ conditionUnevaluable patt = asPureMetaPattern :: ProperPattern Meta sort patt => patt -> CommonMetaPattern -asPureMetaPattern patt = patternKoreToPure Meta (asAst patt) +asPureMetaPattern patt = + case patternKoreToPure Meta (asAst patt) of + Left err -> error (printError err) + Right p -> p mockMetadataTools :: MetadataTools Meta mockMetadataTools = MetadataTools From 620816eaafa65f4b260416971bd65b04bbbf25af Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 4 Jul 2018 15:19:27 +0300 Subject: [PATCH 06/10] Cleanup --- .../language-kore/src/Data/Kore/AST/PureML.hs | 20 ------------------- 1 file changed, 20 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs index 33e0478952..2703541462 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs @@ -37,26 +37,6 @@ fromPurePattern :: PureMLPattern level var -> Pattern level var (PureMLPattern level var) fromPurePattern (Fix p) = p -{- -pattern PureMLAnd p <- Fix (PatternAnd p) -pattern PureMLApplication p <- Fix (PatternApplication p) -pattern PureMLBottom p <- Fix (PatternBottom p) -pattern PureMLCeil p <- Fix (PatternCeil p) -pattern PureMLDomainValue p <- Fix (PatternDomainValue p) -pattern PureMLEquals p <- Fix (PatternEquals p) -pattern PureMLExists p <- Fix (PatternExists p) -pattern PureMLForall p <- Fix (PatternForall p) -pattern PureMLIff p <- Fix (PatternIff p) -pattern PureMLImplies p <- Fix (PatternImplies p) -pattern PureMLIn p <- Fix (PatternIn p) -pattern PureMLNext p <- Fix (PatternNext p) -pattern PureMLNot p <- Fix (PatternNot p) -pattern PureMLOr p <- Fix (PatternOr p) -pattern PureMLRewrites p <- Fix (PatternRewrites p) -pattern PureMLTop p <- Fix (PatternTop p) -and so on --} - -- |'PureSentenceAxiom' is the pure (fixed-@level@) version of 'SentenceAxiom' type PureSentenceAxiom level = SentenceAxiom (SortVariable level) (Pattern level) Variable From eca9e3e937b68ca36fd98d884e9ad1ce769c3ada Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 4 Jul 2018 20:17:35 +0300 Subject: [PATCH 07/10] Add tests for function evaluation --- .../src/Data/Kore/Step/Condition/Condition.hs | 2 +- .../src/Data/Kore/Step/Function/Data.hs | 6 +- .../src/Data/Kore/Step/Function/Evaluator.hs | 31 +- .../Data/Kore/Step/Function/UserDefined.hs | 16 +- .../test/parser/AllParserTests.hs | 6 + .../test/parser/Data/Kore/Comparators.hs | 35 ++ .../Data/Kore/Step/Condition/ConditionTest.hs | 105 ++++ .../Data/Kore/Step/Condition/EvaluatorTest.hs | 574 ++++++++++++++++++ .../parser/Data/Kore/Step/Condition/Mocks.hs | 36 ++ .../Kore/Step/Function/IntegrationTest.hs | 3 +- .../parser/Data/Kore/Step/Function/Mocks.hs | 42 ++ .../Kore/Step/Function/UserDefinedTest.hs | 334 ++++++++++ 12 files changed, 1169 insertions(+), 21 deletions(-) create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/ConditionTest.hs create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/EvaluatorTest.hs create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/Mocks.hs create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/Mocks.hs create mode 100644 src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/UserDefinedTest.hs diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs index ebc4a64fb3..7b38e1499d 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs @@ -52,7 +52,7 @@ data EvaluatedCondition level --} newtype UnevaluatedCondition level = UnevaluatedCondition (CommonPurePattern level) - deriving Show + deriving (Show, Eq) {--| 'makeEvaluatedAnd' combines two evaluated conditions with an 'and', doing some simplification. diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs index f3e25b120b..1cb27d1197 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs @@ -63,9 +63,9 @@ data FunctionResult level = FunctionResult cases where the function can't be fully evaluated. --} data AttemptedFunctionResult level - = NotApplicable - | Symbolic !(EvaluatedCondition level) - | Applied !(FunctionResult level) + = AttemptedFunctionResultNotApplicable + | AttemptedFunctionResultSymbolic !(EvaluatedCondition level) + | AttemptedFunctionResultApplied !(FunctionResult level) deriving (Show, Eq) {--| 'ConditionEvaluator' is a wrapper for a function that evaluates conditions. diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs index a711c1c0a9..b916830501 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Evaluator.hs @@ -263,8 +263,9 @@ evaluateApplication -- TODO(virgil): nub is O(n^2), should do better than that. case nub (filter notNotApplicable mergedResults) of [] -> return unchanged - [(NotApplicable, _)] -> error "Should not reach this line." - [(Symbolic condition, proof)] -> + [(AttemptedFunctionResultNotApplicable, _)] -> + error "Should not reach this line." + [(AttemptedFunctionResultSymbolic condition, proof)] -> return ( FunctionResult { functionResultPattern = @@ -273,7 +274,7 @@ evaluateApplication } , proof ) - [(Applied functionResult, proof)] -> + [(AttemptedFunctionResultApplied functionResult, proof)] -> return (functionResult, proof) (_ : _ : _) -> error "Not implemented yet." where @@ -291,7 +292,7 @@ evaluateApplication app' notNotApplicable = \case - (NotApplicable, _) -> False + (AttemptedFunctionResultNotApplicable, _) -> False _ -> True {--| 'mergeWithCondition' ands the given condition to the given function @@ -308,24 +309,29 @@ mergeWithCondition -> (AttemptedFunctionResult level, FunctionResultProof level) -- ^ AttemptedFunctionResult to which the condition should be added. -> IntCounter (AttemptedFunctionResult level, FunctionResultProof level) -mergeWithCondition _ _ _ (NotApplicable, _) = - return (NotApplicable, FunctionResultProof) +mergeWithCondition _ _ _ (AttemptedFunctionResultNotApplicable, _) = + return (AttemptedFunctionResultNotApplicable, FunctionResultProof) mergeWithCondition conditionEvaluator conditionSort toMerge - (Symbolic condition, _) + (AttemptedFunctionResultSymbolic condition, _) = do (mergedCondition, _) <- mergeConditions conditionEvaluator conditionSort condition toMerge case mergedCondition of - ConditionFalse -> return (NotApplicable, FunctionResultProof) - _ -> return (Symbolic mergedCondition, FunctionResultProof) + ConditionFalse -> + return (AttemptedFunctionResultNotApplicable, FunctionResultProof) + _ -> + return + ( AttemptedFunctionResultSymbolic mergedCondition + , FunctionResultProof + ) mergeWithCondition conditionEvaluator conditionSort toMerge - (Applied functionResult, _) + (AttemptedFunctionResultApplied functionResult, _) = do mergedCondition <- mergeConditions @@ -334,9 +340,10 @@ mergeWithCondition (functionResultCondition functionResult) toMerge case mergedCondition of - (ConditionFalse, _) -> return (NotApplicable, FunctionResultProof) + (ConditionFalse, _) -> + return (AttemptedFunctionResultNotApplicable, FunctionResultProof) _ -> return - ( Applied functionResult + ( AttemptedFunctionResultApplied functionResult {functionResultCondition = fst mergedCondition} , FunctionResultProof ) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs index ca08eaf92e..0ce9384146 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/UserDefined.hs @@ -61,7 +61,8 @@ axiomFunctionEvaluator app = case stepResult of - Left _ -> return (NotApplicable, FunctionResultProof) + Left _ -> + return (AttemptedFunctionResultNotApplicable, FunctionResultProof) Right configurationWithProof -> do ( StepperConfiguration @@ -120,13 +121,18 @@ reevaluateFunctions , functionResultCondition = rewritingCondition } = case rewritingCondition of - ConditionFalse -> return (NotApplicable, FunctionResultProof) + ConditionFalse -> + return (AttemptedFunctionResultNotApplicable, FunctionResultProof) _ -> do ( FunctionResult { functionResultPattern = simplifiedPattern , functionResultCondition = simplificationCondition } , _ + -- TODO(virgil): This call should be done in Evaluator.hs, but, + -- for optimization purposes, it's done here. Make sure that + -- this still makes sense after the evaluation code is fully + -- optimized. ) <- functionEvaluator rewrittenPattern return ( firstSatisfiablePattern @@ -137,6 +143,8 @@ reevaluateFunctions rewritingCondition simplificationCondition ) + -- TODO(virgil): Returning the rewrittenPattern here is + -- fishy. , (rewrittenPattern, rewritingCondition) ] , FunctionResultProof @@ -150,13 +158,13 @@ firstSatisfiablePattern -> AttemptedFunctionResult level firstSatisfiablePattern ((patt, ConditionTrue) : _) - = Applied FunctionResult + = AttemptedFunctionResultApplied FunctionResult { functionResultPattern = patt , functionResultCondition = ConditionTrue } firstSatisfiablePattern ((patt, condition @ (ConditionUnevaluable _)) : _) - = Applied FunctionResult + = AttemptedFunctionResultApplied FunctionResult { functionResultPattern = patt , functionResultCondition = condition } diff --git a/src/main/haskell/language-kore/test/parser/AllParserTests.hs b/src/main/haskell/language-kore/test/parser/AllParserTests.hs index 260b21e27c..c2416bc580 100644 --- a/src/main/haskell/language-kore/test/parser/AllParserTests.hs +++ b/src/main/haskell/language-kore/test/parser/AllParserTests.hs @@ -30,7 +30,10 @@ import Data.Kore.Parser.ParserTest import Data.Kore.Parser.RegressionTest import Data.Kore.Step.AxiomPatternsTest import Data.Kore.Step.BaseStepTest +import Data.Kore.Step.Condition.ConditionTest +import Data.Kore.Step.Condition.EvaluatorTest import Data.Kore.Step.Function.IntegrationTest +import Data.Kore.Step.Function.UserDefinedTest import Data.Kore.Step.StepTest import Data.Kore.Substitution.ClassTest import Data.Kore.Substitution.ListTest @@ -98,5 +101,8 @@ unitTests = , baseStepTests , stepTests , axiomPatternsTests + , conditionTests + , conditionEvaluatorTests + , userDefinedFunctionTests , functionIntegrationTests ] diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs index 5561e41980..1e7b7bd44d 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Comparators.hs @@ -781,3 +781,38 @@ instance EqualWithExplanation (ConditionSort level) where compareWithExplanation = sumCompareWithExplanation printWithExplanation = show + + +instance SumEqualWithExplanation (AttemptedFunctionResult level) + where + sumConstructorPair + AttemptedFunctionResultNotApplicable + AttemptedFunctionResultNotApplicable + = + SumConstructorSameNoArguments + sumConstructorPair a1@AttemptedFunctionResultNotApplicable a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + + sumConstructorPair + (AttemptedFunctionResultSymbolic a1) (AttemptedFunctionResultSymbolic a2) + = + SumConstructorSameWithArguments + (EqWrap "Symbolic" a1 a2) + sumConstructorPair a1@(AttemptedFunctionResultSymbolic _) a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + + sumConstructorPair + (AttemptedFunctionResultApplied a1) (AttemptedFunctionResultApplied a2) + = + SumConstructorSameWithArguments + (EqWrap "Applied" a1 a2) + sumConstructorPair a1@(AttemptedFunctionResultApplied _) a2 = + SumConstructorDifferent + (printWithExplanation a1) (printWithExplanation a2) + +instance EqualWithExplanation (AttemptedFunctionResult level) + where + compareWithExplanation = sumCompareWithExplanation + printWithExplanation = show diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/ConditionTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/ConditionTest.hs new file mode 100644 index 0000000000..b052be2667 --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/ConditionTest.hs @@ -0,0 +1,105 @@ +module Data.Kore.Step.Condition.ConditionTest (conditionTests) where + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) + +import Data.Kore.AST.MetaOrObject +import Data.Kore.Building.AsAst +import Data.Kore.Building.Sorts +import Data.Kore.Comparators () +import Data.Kore.Step.Condition.Condition + +import Test.Tasty.HUnit.Extensions + +conditionTests :: TestTree +conditionTests = + testGroup + "Step Condition Tests" + [ let + makeAnd sort c1 c2 = fst (makeEvaluatedAnd sort c1 c2) + in + testCase "And truth table" + (do + assertEqualWithExplanation "false and false = false" + ConditionFalse + (makeAnd sortSort ConditionFalse ConditionFalse) + assertEqualWithExplanation "false and true = false" + ConditionFalse + (makeAnd sortSort ConditionFalse ConditionTrue) + assertEqualWithExplanation "true and false = false" + ConditionFalse + (makeAnd sortSort ConditionTrue ConditionFalse) + assertEqualWithExplanation "true and true = true" + ConditionTrue + (makeAnd sortSort ConditionTrue ConditionTrue) + ) + , let + makeOr sort c1 c2 = fst (makeEvaluatedOr sort c1 c2) + in + testCase "Or truth table" + (do + assertEqualWithExplanation "false or false = false" + ConditionFalse + (makeOr sortSort ConditionFalse ConditionFalse) + assertEqualWithExplanation "false or true = true" + ConditionTrue + (makeOr sortSort ConditionFalse ConditionTrue) + assertEqualWithExplanation "true or false = true" + ConditionTrue + (makeOr sortSort ConditionTrue ConditionFalse) + assertEqualWithExplanation "true or true = true" + ConditionTrue + (makeOr sortSort ConditionTrue ConditionTrue) + ) + , let + makeImplies sort c1 c2 = fst (makeEvaluatedImplies sort c1 c2) + in + testCase "Implies truth table" + (do + assertEqualWithExplanation "false implies false = true" + ConditionTrue + (makeImplies sortSort ConditionFalse ConditionFalse) + assertEqualWithExplanation "false implies true = true" + ConditionTrue + (makeImplies sortSort ConditionFalse ConditionTrue) + assertEqualWithExplanation "true implies false = false" + ConditionFalse + (makeImplies sortSort ConditionTrue ConditionFalse) + assertEqualWithExplanation "true implies true = true" + ConditionTrue + (makeImplies sortSort ConditionTrue ConditionTrue) + ) + , let + makeIff sort c1 c2 = fst (makeEvaluatedIff sort c1 c2) + in + testCase "Iff truth table" + (do + assertEqualWithExplanation "false iff false = true" + ConditionTrue + (makeIff sortSort ConditionFalse ConditionFalse) + assertEqualWithExplanation "false iff true = false" + ConditionFalse + (makeIff sortSort ConditionFalse ConditionTrue) + assertEqualWithExplanation "true iff false = false" + ConditionFalse + (makeIff sortSort ConditionTrue ConditionFalse) + assertEqualWithExplanation "true iff true = true" + ConditionTrue + (makeIff sortSort ConditionTrue ConditionTrue) + ) + , let + makeNot sort c2 = fst (makeEvaluatedNot sort c2) + in + testCase "Not truth table" + (do + assertEqualWithExplanation "not false = true" + ConditionTrue + (makeNot sortSort ConditionFalse) + assertEqualWithExplanation "not true = false" + ConditionFalse + (makeNot sortSort ConditionTrue) + ) + ] + +sortSort :: ConditionSort Meta +sortSort = ConditionSort (asAst SortSort) diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/EvaluatorTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/EvaluatorTest.hs new file mode 100644 index 0000000000..7cc6f271e8 --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/EvaluatorTest.hs @@ -0,0 +1,574 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +module Data.Kore.Step.Condition.EvaluatorTest (conditionEvaluatorTests) where + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) + +import Data.Kore.AST.Common (Application (..), + AstLocation (..), + Id (..), Pattern (..), + Sort, SymbolOrAlias (..)) +import Data.Kore.AST.MetaOrObject +import Data.Kore.AST.PureToKore (patternKoreToPure) +import Data.Kore.Building.AsAst +import Data.Kore.Building.Patterns +import Data.Kore.Building.Sorts +import Data.Kore.Comparators () +import Data.Kore.Error +import Data.Kore.MetaML.AST (CommonMetaPattern) +import Data.Kore.Step.Condition.Condition +import Data.Kore.Step.Condition.Evaluator (evaluateFunctionCondition) +import Data.Kore.Step.Function.Data (CommonPurePatternFunctionEvaluator (..), + FunctionResult (..), + FunctionResultProof (..)) +import Data.Kore.Step.Function.Mocks (mockFunctionEvaluator) +import Data.Kore.Variables.Fresh.IntCounter + +import Test.Tasty.HUnit.Extensions + +conditionEvaluatorTests :: TestTree +conditionEvaluatorTests = + testGroup + "Condition evaluator tests" + [ testCase "And truth table" + (do + assertEqualWithExplanation "false and false = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortFalse sortSortFalse) + ) + ) + assertEqualWithExplanation "false and true = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortFalse sortSortTrue) + ) + ) + assertEqualWithExplanation "true and false = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortTrue sortSortFalse) + ) + ) + assertEqualWithExplanation "true and true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortTrue sortSortTrue) + ) + ) + ) + , testCase "Or truth table" + (do + assertEqualWithExplanation "false or false = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortFalse sortSortFalse) + ) + ) + assertEqualWithExplanation "false or true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortFalse sortSortTrue) + ) + ) + assertEqualWithExplanation "true or false = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortTrue sortSortFalse) + ) + ) + assertEqualWithExplanation "true or true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortTrue sortSortTrue) + ) + ) + ) + , testCase "Implies truth table" + (do + assertEqualWithExplanation "false implies false = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortFalse sortSortFalse) + ) + ) + assertEqualWithExplanation "false implies true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortFalse sortSortTrue) + ) + ) + assertEqualWithExplanation "true implies false = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortTrue sortSortFalse) + ) + ) + assertEqualWithExplanation "true implies true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortTrue sortSortTrue) + ) + ) + ) + , testCase "Iff truth table" + (do + assertEqualWithExplanation "false iff false = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortFalse sortSortFalse) + ) + ) + assertEqualWithExplanation "false iff true = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortFalse sortSortTrue) + ) + ) + assertEqualWithExplanation "true iff false = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortTrue sortSortFalse) + ) + ) + assertEqualWithExplanation "true iff true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortTrue sortSortTrue) + ) + ) + ) + , testCase "Not truth table" + (do + assertEqualWithExplanation "not false = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaNot SortSort sortSortFalse) + ) + ) + assertEqualWithExplanation "not true = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaNot SortSort sortSortTrue) + ) + ) + ) + , let + falseChild = metaNot SortSort sortSortTrue + trueChild = metaNot SortSort sortSortFalse + in + testCase "Evaluates children" + (do + assertEqualWithExplanation "true and = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortTrue trueChild) + ) + ) + assertEqualWithExplanation " and true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort trueChild sortSortTrue) + ) + ) + assertEqualWithExplanation "true and = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaAnd SortSort sortSortTrue falseChild) + ) + ) + assertEqualWithExplanation "false or = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortFalse trueChild) + ) + ) + assertEqualWithExplanation " or false = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort trueChild sortSortFalse) + ) + ) + assertEqualWithExplanation "false or = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaOr SortSort sortSortFalse falseChild) + ) + ) + assertEqualWithExplanation "true implies = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortTrue trueChild) + ) + ) + assertEqualWithExplanation " implies true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort trueChild sortSortTrue) + ) + ) + assertEqualWithExplanation "true implies = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaImplies SortSort sortSortTrue falseChild) + ) + ) + assertEqualWithExplanation "true iff = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortTrue trueChild) + ) + ) + assertEqualWithExplanation " iff true = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort trueChild sortSortTrue) + ) + ) + assertEqualWithExplanation "true iff = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaIff SortSort sortSortTrue falseChild) + ) + ) + assertEqualWithExplanation "not = false" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaNot SortSort trueChild) + ) + ) + assertEqualWithExplanation "not = true" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaNot SortSort falseChild) + ) + ) + ) + , let + fOfX = metaF (x PatternSort) + gOfX = metaG (x PatternSort) + hOfX = metaH (x PatternSort) + in + testCase "Evaluates equals" + (do + assertEqualWithExplanation "f(x) /= g(x)" + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator []) + (ConditionSort sortSort) + (unevaluatedCondition + (metaEquals (ResultSort SortSort) PatternSort + fOfX + gOfX + ) + ) + ) + assertEqualWithExplanation + "f(x) = g(x) if f(x) => h(x) and g(x) => h(x)" + ConditionTrue + (evaluateCondition + (mockFunctionEvaluator + [ ( asPureMetaPattern fOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionTrue + } + , FunctionResultProof + ) + ) + , ( asPureMetaPattern gOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionTrue + } + , FunctionResultProof + ) + ) + ] + ) + (ConditionSort sortSort) + (unevaluatedCondition + (metaEquals (ResultSort SortSort) PatternSort + (metaF (x PatternSort)) + (metaG (x PatternSort)) + ) + ) + ) + assertEqualWithExplanation + ("f(x) /= g(x) if f(x) => h(x) and g(x) => h(x) " + ++ "but incompatible f condition") + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator + [ ( asPureMetaPattern fOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionFalse + } + , FunctionResultProof + ) + ) + , ( asPureMetaPattern gOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionTrue + } + , FunctionResultProof + ) + ) + ] + ) + (ConditionSort sortSort) + (unevaluatedCondition + (metaEquals (ResultSort SortSort) PatternSort + (metaF (x PatternSort)) + (metaG (x PatternSort)) + ) + ) + ) + assertEqualWithExplanation + ("f(x) /= g(x) if f(x) => h(x) and g(x) => h(x) " + ++ "but incompatible g condition") + ConditionFalse + (evaluateCondition + (mockFunctionEvaluator + [ ( asPureMetaPattern fOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionTrue + } + , FunctionResultProof + ) + ) + , ( asPureMetaPattern gOfX + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern hOfX + , functionResultCondition = + ConditionFalse + } + , FunctionResultProof + ) + ) + ] + ) + (ConditionSort sortSort) + (unevaluatedCondition + (metaEquals (ResultSort SortSort) PatternSort + (metaF (x PatternSort)) + (metaG (x PatternSort)) + ) + ) + ) + ) + ] + +x :: MetaSort sort => sort -> MetaVariable sort +x = metaVariable "#x" AstLocationTest + +sortSort :: Sort Meta +sortSort = asAst SortSort + +sortSortTrue :: PatternTop SortSort Meta +sortSortTrue = metaTop SortSort + +sortSortFalse :: PatternBottom SortSort Meta +sortSortFalse = metaBottom SortSort + + +fSymbol :: SymbolOrAlias Meta +fSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#f" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaF p1 = MetaF p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaF p1) + where + asProperPattern (MetaF p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = fSymbol + , applicationChildren = [asAst p1] + } +metaF + :: (MetaPattern PatternSort p1) + => p1 -> MetaF p1 +metaF = MetaF + + +gSymbol :: SymbolOrAlias Meta +gSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#g" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaG p1 = MetaG p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaG p1) + where + asProperPattern (MetaG p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = gSymbol + , applicationChildren = [asAst p1] + } +metaG + :: (MetaPattern PatternSort p1) + => p1 -> MetaG p1 +metaG = MetaG + + +hSymbol :: SymbolOrAlias Meta +hSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#h" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaH p1 = MetaH p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaH p1) + where + asProperPattern (MetaH p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = hSymbol + , applicationChildren = [asAst p1] + } +metaH + :: (MetaPattern PatternSort p1) + => p1 -> MetaH p1 +metaH = MetaH + + +unevaluatedCondition + :: ProperPattern Meta sort patt => patt -> UnevaluatedCondition Meta +unevaluatedCondition patt = + UnevaluatedCondition (asPureMetaPattern patt) + +asPureMetaPattern + :: ProperPattern Meta sort patt => patt -> CommonMetaPattern +asPureMetaPattern patt = + case patternKoreToPure Meta (asAst patt) of + Left err -> error (printError err) + Right pat -> pat + +evaluateCondition + :: CommonPurePatternFunctionEvaluator level + -> ConditionSort level + -> UnevaluatedCondition level + -> EvaluatedCondition level +evaluateCondition + functionEvaluator + conditionSort + condition + = + fst $ fst $ runIntCounter + (evaluateFunctionCondition functionEvaluator conditionSort condition) + 0 diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/Mocks.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/Mocks.hs new file mode 100644 index 0000000000..0b5bd7c08c --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Condition/Mocks.hs @@ -0,0 +1,36 @@ +module Data.Kore.Step.Condition.Mocks (mockConditionEvaluator) where + +import Data.Kore.Step.Condition.Condition (ConditionProof (..), + EvaluatedCondition (..), + UnevaluatedCondition (..)) +import Data.Kore.Step.Function.Data (ConditionEvaluator (..)) +import Data.Kore.Variables.Fresh.IntCounter + +mockConditionEvaluator + :: [ ( UnevaluatedCondition level + , (EvaluatedCondition level, ConditionProof level) + ) + ] + -> ConditionEvaluator level +mockConditionEvaluator values = + ConditionEvaluator (mockConditionEvaluatorHelper values) + +mockConditionEvaluatorHelper + :: [ ( UnevaluatedCondition level + , (EvaluatedCondition level, ConditionProof level) + ) + ] + -> UnevaluatedCondition level + -> IntCounter (EvaluatedCondition level, ConditionProof level) +mockConditionEvaluatorHelper [] (UnevaluatedCondition condition) = + return + ( ConditionUnevaluable condition + , ConditionProof + ) +mockConditionEvaluatorHelper + ((condition, result) : reminder) + unevaluatedCondition + = + if condition == unevaluatedCondition + then return result + else mockConditionEvaluatorHelper reminder unevaluatedCondition diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs index 7019d864b9..50d8e3b4fc 100644 --- a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/IntegrationTest.hs @@ -260,7 +260,8 @@ conditionSort sort = ConditionSort (asAst sort) appliedMockEvaluator :: FunctionResult level -> ApplicationFunctionEvaluator level appliedMockEvaluator result = - ApplicationFunctionEvaluator (mockEvaluator (Applied result)) + ApplicationFunctionEvaluator + (mockEvaluator (AttemptedFunctionResultApplied result)) mockEvaluator :: AttemptedFunctionResult level diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/Mocks.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/Mocks.hs new file mode 100644 index 0000000000..7c967a1d4b --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/Mocks.hs @@ -0,0 +1,42 @@ +module Data.Kore.Step.Function.Mocks (mockFunctionEvaluator) where + +import Data.Kore.AST.PureML (CommonPurePattern) +import Data.Kore.Comparators () +import Data.Kore.Step.Condition.Condition +import Data.Kore.Step.Function.Data (CommonPurePatternFunctionEvaluator (..), + FunctionResult (..), + FunctionResultProof (..)) +import Data.Kore.Variables.Fresh.IntCounter + +mockFunctionEvaluator + :: [ ( CommonPurePattern level + , (FunctionResult level, FunctionResultProof level) + ) + ] + -> CommonPurePatternFunctionEvaluator level +mockFunctionEvaluator values = + CommonPurePatternFunctionEvaluator + (mockFunctionEvaluatorHelper values) + +mockFunctionEvaluatorHelper + :: [ ( CommonPurePattern level + , (FunctionResult level, FunctionResultProof level) + ) + ] + -> CommonPurePattern level + -> IntCounter (FunctionResult level, FunctionResultProof level) +mockFunctionEvaluatorHelper [] patt = + return + ( FunctionResult + { functionResultPattern = patt + , functionResultCondition = ConditionTrue + } + , FunctionResultProof + ) +mockFunctionEvaluatorHelper + ((left, result) : reminder) + patt + = + if patt == left + then return result + else mockFunctionEvaluatorHelper reminder patt diff --git a/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/UserDefinedTest.hs b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/UserDefinedTest.hs new file mode 100644 index 0000000000..6a56cfc4fa --- /dev/null +++ b/src/main/haskell/language-kore/test/parser/Data/Kore/Step/Function/UserDefinedTest.hs @@ -0,0 +1,334 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +module Data.Kore.Step.Function.UserDefinedTest (userDefinedFunctionTests) where + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) + +import Data.Kore.AST.Common (Application (..), + AstLocation (..), + Id (..), Pattern (..), + Sort (..), + SymbolOrAlias (..)) +import Data.Kore.AST.MetaOrObject +import Data.Kore.AST.PureML (CommonPurePattern, + fromPurePattern) +import Data.Kore.AST.PureToKore (patternKoreToPure) +import Data.Kore.Building.AsAst +import Data.Kore.Building.Patterns +import Data.Kore.Building.Sorts +import Data.Kore.Comparators () +import Data.Kore.Error +import Data.Kore.IndexedModule.MetadataTools (MetadataTools (..)) +import Data.Kore.MetaML.AST (CommonMetaPattern) +import Data.Kore.Step.BaseStep (AxiomPattern (..)) +import Data.Kore.Step.Condition.Condition (ConditionProof (..), + ConditionSort (..), + EvaluatedCondition (..), + UnevaluatedCondition (..)) +import Data.Kore.Step.Condition.Mocks (mockConditionEvaluator) +import Data.Kore.Step.Function.Data (AttemptedFunctionResult (..), + CommonPurePatternFunctionEvaluator (..), + ConditionEvaluator (..), + FunctionResult (..), + FunctionResultProof (..)) +import Data.Kore.Step.Function.Mocks (mockFunctionEvaluator) +import Data.Kore.Step.Function.UserDefined (axiomFunctionEvaluator) +import Data.Kore.Variables.Fresh.IntCounter + +import Test.Tasty.HUnit.Extensions + +userDefinedFunctionTests :: TestTree +userDefinedFunctionTests = + testGroup + "User defined functions tests" + [ testCase "Cannot apply function if step fails" + (assertEqualWithExplanation "" + AttemptedFunctionResultNotApplicable + (evaluateWithAxiom + mockMetadataTools + (ConditionSort sortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (x PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (x PatternSort)) + } + (mockConditionEvaluator []) + (mockFunctionEvaluator []) + (asApplication (metaH (x PatternSort))) + ) + ) + , testCase "Applies one step" + (assertEqualWithExplanation "f(x) => g(x)" + (AttemptedFunctionResultApplied FunctionResult + { functionResultPattern = + asPureMetaPattern (metaG (x PatternSort)) + , functionResultCondition = ConditionTrue + } + ) + (evaluateWithAxiom + mockMetadataTools + (ConditionSort sortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (x PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (x PatternSort)) + } + (mockConditionEvaluator + [ ( unevaluatedCondition + (metaAnd SortSort + (metaTop SortSort) + (metaTop SortSort) + ) + , (ConditionTrue, ConditionProof) + ) + ] + ) + (mockFunctionEvaluator []) + (asApplication (metaF (x PatternSort))) + ) + ) + , testCase "Cannot apply step with unsat condition" + (assertEqualWithExplanation "" + AttemptedFunctionResultNotApplicable + (evaluateWithAxiom + mockMetadataTools + (ConditionSort sortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (x PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (x PatternSort)) + } + (mockConditionEvaluator + [ ( unevaluatedCondition + (metaAnd SortSort + (metaTop SortSort) + (metaTop SortSort) + ) + , (ConditionFalse, ConditionProof) + ) + ] + ) + (mockFunctionEvaluator []) + (asApplication (metaF (x PatternSort))) + ) + ) + , testCase "Reevaluates the step application" + (assertEqualWithExplanation "f(x) => g(x) and g(x) => h(x)" + (AttemptedFunctionResultApplied FunctionResult + { functionResultPattern = + asPureMetaPattern (metaH (x PatternSort)) + , functionResultCondition = ConditionTrue + } + ) + (evaluateWithAxiom + mockMetadataTools + (ConditionSort sortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (x PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (x PatternSort)) + } + (mockConditionEvaluator + [ ( unevaluatedCondition + (metaAnd SortSort + (metaTop SortSort) + (metaTop SortSort) + ) + , (ConditionTrue, ConditionProof) + ) + ] + ) + (mockFunctionEvaluator + [ ( asPureMetaPattern (metaG (x PatternSort)) + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern + (metaH (x PatternSort)) + , functionResultCondition = + ConditionTrue + } + , FunctionResultProof + ) + ) + ] + ) + (asApplication (metaF (x PatternSort))) + ) + ) + , testCase "Does not reevaluate the step application with incompatible condition" + (assertEqualWithExplanation "f(x) => g(x) and g(x) => h(x) + false" + (AttemptedFunctionResultApplied FunctionResult + { functionResultPattern = + asPureMetaPattern (metaG (x PatternSort)) + , functionResultCondition = ConditionTrue + } + ) + (evaluateWithAxiom + mockMetadataTools + (ConditionSort sortSort) + AxiomPattern + { axiomPatternLeft = + asPureMetaPattern (metaF (x PatternSort)) + , axiomPatternRight = + asPureMetaPattern (metaG (x PatternSort)) + } + (mockConditionEvaluator + [ ( unevaluatedCondition + (metaAnd SortSort + (metaTop SortSort) + (metaTop SortSort) + ) + , (ConditionTrue, ConditionProof) + ) + ] + ) + (mockFunctionEvaluator + [ ( asPureMetaPattern (metaG (x PatternSort)) + , ( FunctionResult + { functionResultPattern = + asPureMetaPattern + (metaH (x PatternSort)) + , functionResultCondition = + ConditionFalse + } + , FunctionResultProof + ) + ) + ] + ) + (asApplication (metaF (x PatternSort))) + ) + ) + ] + +mockMetadataTools :: MetadataTools Meta +mockMetadataTools = MetadataTools + { isConstructor = const True + , isFunctional = const True + , isFunction = const False + , getArgumentSorts = const [asAst PatternSort, asAst PatternSort] + , getResultSort = const (asAst PatternSort) + } + +x :: MetaSort sort => sort -> MetaVariable sort +x = metaVariable "#x" AstLocationTest + +sortSort :: Sort Meta +sortSort = asAst SortSort + + +fSymbol :: SymbolOrAlias Meta +fSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#f" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaF p1 = MetaF p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaF p1) + where + asProperPattern (MetaF p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = fSymbol + , applicationChildren = [asAst p1] + } +metaF + :: (MetaPattern PatternSort p1) + => p1 -> MetaF p1 +metaF = MetaF + + +gSymbol :: SymbolOrAlias Meta +gSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#g" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaG p1 = MetaG p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaG p1) + where + asProperPattern (MetaG p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = gSymbol + , applicationChildren = [asAst p1] + } +metaG + :: (MetaPattern PatternSort p1) + => p1 -> MetaG p1 +metaG = MetaG + + +hSymbol :: SymbolOrAlias Meta +hSymbol = SymbolOrAlias + { symbolOrAliasConstructor = Id "#h" AstLocationTest + , symbolOrAliasParams = [] + } + +newtype MetaH p1 = MetaH p1 +instance (MetaPattern PatternSort p1) + => ProperPattern Meta PatternSort (MetaH p1) + where + asProperPattern (MetaH p1) = + ApplicationPattern Application + { applicationSymbolOrAlias = hSymbol + , applicationChildren = [asAst p1] + } +metaH + :: (MetaPattern PatternSort p1) + => p1 -> MetaH p1 +metaH = MetaH + +unevaluatedCondition + :: ProperPattern Meta sort patt => patt -> UnevaluatedCondition Meta +unevaluatedCondition patt = + UnevaluatedCondition (asPureMetaPattern patt) + +asPureMetaPattern + :: ProperPattern Meta sort patt => patt -> CommonMetaPattern +asPureMetaPattern patt = + case patternKoreToPure Meta (asAst patt) of + Left err -> error (printError err) + Right pat -> pat + +asApplication + :: ProperPattern Meta sort patt => patt + -> Application Meta (CommonPurePattern Meta) +asApplication patt = + case fromPurePattern (asPureMetaPattern patt) of + ApplicationPattern a -> a + _ -> error "Expected an Application pattern." + +evaluateWithAxiom + :: MetaOrObject level + => MetadataTools level + -> ConditionSort level + -> AxiomPattern level + -> ConditionEvaluator level + -> CommonPurePatternFunctionEvaluator level + -> Application level (CommonPurePattern level) + -> AttemptedFunctionResult level +evaluateWithAxiom + metadataTools + conditionSort + axiom + conditionEvaluator + functionEvaluator + app + = + fst $ fst $ runIntCounter + (axiomFunctionEvaluator + metadataTools + conditionSort + axiom + conditionEvaluator + functionEvaluator + app + ) + 0 From bae3a5234c73889cbdd4cb2b4c558051ba9e3f94 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 4 Jul 2018 20:39:05 +0300 Subject: [PATCH 08/10] Documentation cleanup --- .../language-kore/src/Data/Kore/Step/Condition/Condition.hs | 4 ++-- .../language-kore/src/Data/Kore/Step/Condition/Evaluator.hs | 2 -- .../haskell/language-kore/src/Data/Kore/Step/Function/Data.hs | 4 ++-- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs index 7b38e1499d..ab31f3e935 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Condition.hs @@ -24,8 +24,8 @@ import Data.Kore.AST.Common (And (..), Iff (..), Implies (..), Sort (..)) import Data.Kore.AST.PureML (CommonPurePattern, asPurePattern) -{--| 'ConditionProof' is a placeholder for a proof about a condition's -evaluation. +{--| 'ConditionProof' is a placeholder for a proof showing that a condition +evaluation was correct. --} data ConditionProof level = ConditionProof deriving (Show, Eq) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs index 3076ca36bb..281e0d6cb2 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs @@ -134,8 +134,6 @@ evaluateFunctionConditionInternal } , _ ) = secondValue - -- TODO(virgil): This is more complex than implemented here, e.g. - -- we should evaluate functions on these patterns. if firstPattern == secondPattern -- TODO(virgil): this should probably call evaluateFunctionCondition then return $ diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs index 1cb27d1197..9de18cd549 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Function/Data.hs @@ -23,8 +23,8 @@ import Data.Kore.Step.Condition.Condition (ConditionProof, UnevaluatedCondition) import Data.Kore.Variables.Fresh.IntCounter (IntCounter) -{--| 'FunctionResultProof' is a placeholder for proofs about a Kore function -evaluation's result correctness. +{--| 'FunctionResultProof' is a placeholder for proofs showing that a Kore +function evaluation was correct. --} data FunctionResultProof level = FunctionResultProof deriving (Show, Eq) From e91a3e62121e605f4333adb36650d166f4229379 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 4 Jul 2018 21:59:45 +0300 Subject: [PATCH 09/10] Add TODO to fix equality evaluation for conditions. --- .../language-kore/src/Data/Kore/Step/Condition/Evaluator.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs index 281e0d6cb2..de0a328268 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/Step/Condition/Evaluator.hs @@ -134,6 +134,8 @@ evaluateFunctionConditionInternal } , _ ) = secondValue + -- TODO(virgil): This is wrong, because `variable=pattern` is not + -- necessarily false. Fix this. if firstPattern == secondPattern -- TODO(virgil): this should probably call evaluateFunctionCondition then return $ From 2e43d6562fe76d4fadff9e4143d10c4e96ea8ce4 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Mon, 9 Jul 2018 19:07:19 +0300 Subject: [PATCH 10/10] Code cleanup. --- src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs index 2703541462..f8b833ec1f 100644 --- a/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs +++ b/src/main/haskell/language-kore/src/Data/Kore/AST/PureML.hs @@ -2,7 +2,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeSynonymInstances #-} {-| Module : Data.Kore.AST.PureML @@ -35,7 +34,7 @@ asPurePattern = Fix fromPurePattern :: PureMLPattern level var -> Pattern level var (PureMLPattern level var) -fromPurePattern (Fix p) = p +fromPurePattern = unFix -- |'PureSentenceAxiom' is the pure (fixed-@level@) version of 'SentenceAxiom' type PureSentenceAxiom level =