Smart constructors #137

phillipharr1s · 2018-07-06T18:59:46Z

No description provided.

…ation

ttuegel · 2018-07-06T20:02:26Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+alphaRename = (\case 
+ Forall_ s1 v p -> go Forall_ s1 v p 
+ Exists_ s1 v p -> go Exists_ s1 v p
+ _ -> error "Input must be an Exist or Forall at the top level"


Can we make this function total? For example, if its argument is not a binder, could it just return the argument unmodified? Or, can we encode this restriction in the type?

ttuegel · 2018-07-06T20:05:19Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

@@ -0,0 +1,124 @@
+{-|


Is it necessary to implement substitution ourselves, or could we outsource this to a library like bound?

Hmm. Maybe. There was already a substitution function in Kore/Substitution, but I needed one that substitutes terms for terms and not just terms for variables.

ttuegel · 2018-07-06T20:16:10Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+  -> CommonPurePattern level 
+  -> CommonPurePattern level 
+  -> CommonPurePattern level
+subst a b (Forall_ s1 v p) = handleBinder a b Forall_ s1 v p


It would be better to write this as subst a b = \case ... since the first two variables are always bound the same.

ttuegel · 2018-07-06T20:16:37Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+  -> CommonPurePattern level
+subst a b (Forall_ s1 v p) = handleBinder a b Forall_ s1 v p
+subst a b (Exists_ s1 v p) = handleBinder a b Exists_ s1 v p
+subst a b pat =


The intention here might be clearer using guards rather than if.

ttuegel · 2018-07-06T20:29:20Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+subst a b (Forall_ s1 v p) = handleBinder a b Forall_ s1 v p
+subst a b (Exists_ s1 v p) = handleBinder a b Exists_ s1 v p
+subst a b pat =
+  if pat == a then b else Fix $ fmap (subst a b) $ unFix pat


I think subst could actually be rewritten as a catamorphism using embed. Maybe that's a little tricky if we're doing whole-term substitution instead of only variables. Although, maybe not: I don't see that pat could contain a as a subterm and also be equal to a.

virgil-serbanuta

What's the test coverage for the new code?

virgil-serbanuta · 2018-07-09T13:39:07Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/SmartConstructors.hs

+  Rewrites_  s2   a b -> Rewrites_ <$>          o s2           <*> c a <*> c b
+  Top_       s2       -> Top_      <$>          o s2
+  Var_          v     -> Var_      <$>                   var v
+  other -> error $ "Unknown constructor " ++ show other


Does one still get warnings about not matching all possible cases when using pattern synonyms? If yes, then it may be better to drop the "other" case, because we use --pedantic on Jenkins, which will transform that into an error.

Pattern Synonyms + GADTS = GHC definitely can't tell if it's complete or not, so without the "other" it doesn't compile.

Oh, wow, I was waiting to use these synonyms in my condition-evaluation pull request, but now I'm not so sure anymore.

One of the reasons we chose Haskell is because all of the built-in safety, but it seems to me that Haskell programmers don't usually want it that much.

PatternSynonyms are a big problem for completeness checking. For our case, we really only want to be using the synonyms for construction, not matching. The benefit of using Fix is that we should be able to write algebras that only need to match on the underlying functior!

Actually, in this case the COMPLETE pragma works. So writing a complete list of cases with

Fix ( ApplicationPattern (Application ...
Fix (AndPattern (And ...

is equivalent to

App_ ...
And_ ...

and the compiler will know it's complete.

virgil-serbanuta · 2018-07-09T15:47:14Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/SmartConstructors.hs

+  Var_          v     -> Var_      <$>                   var v
+  other -> error $ "Unknown constructor " ++ show other
+
+inputSort        f = patternLens f    pure pure pure 


Could you add function signatures? Also, could you document all exported functions?

virgil-serbanuta · 2018-07-09T15:54:50Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/SmartConstructors.hs

+pattern Or_           s2   a b = Fix (OrPattern (Or s2 a b))
+pattern Rewrites_     s2   a b = Fix (RewritesPattern (Rewrites s2 a b))
+pattern Top_          s2       = Fix (TopPattern (Top s2))
+pattern Var_             v     = Fix (VariablePattern v)   


Why didn't you add patterns for strings and chars?

… smart-constructors

ehildenb · 2018-07-10T14:19:57Z

@u-- can we use better commit messages? Try to make them useful for code reviewers. Someone somewhere said "given the commit message, the reviewer should be able to re-implement your commit".

Also, I recommend squashing fixup commits into the commit which introduced the feature. The story "I introduced feature A and then " is a lot simpler than "I introduced feature A and then and then a fixup A.1".

phillipharr1s · 2018-07-10T14:47:41Z

@ehildenb what do you mean w/ squashing? Like branch off the original commit that introduced the feature?

phillipharr1s · 2018-07-10T15:02:12Z

Also, I didn't mean for the Hashable instances in Common.hs to be in this branch... but since it relates to the AST I guess it fits.

virgil-serbanuta

I didn't know I was a reviewer! Most of my comments are about understanding what you did and about having a style that's consistent with the existing code.

virgil-serbanuta · 2018-07-10T16:16:33Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/SmartConstructors.hs

+--   -> CommonPurePattern Meta
+
+-- No way to make multiline pragma?
+{-# COMPLETE And_, App_, Bottom_, Ceil_, DV_, Equals_, Exists_, Floor_, Forall_, Iff_, Implies_, In_, Next_, Not_, Or_, Rewrites_, Top_, Var_, StringLiteral_, CharLiteral_ #-}


If this make sense: could you add a comment near Pattern in Common.hs that one should update this list when updating the Pattern case list?

virgil-serbanuta · 2018-07-10T16:18:08Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/SmartConstructors.hs

+  _ -> False
+
+
+-- Flexible patterns are those which can be


Some of these comments do not have a "|". Does haddock produce documentation from them?

virgil-serbanuta · 2018-07-10T16:30:24Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+import           Data.Kore.ASTUtils.SmartConstructors
+
+
+subst


Could you document exported methods?

One-letter variable names don't usually help people reading your code. Sometimes that does not matter much, but, as an example, here, the meaning of "a" and "b" can be sort of inferred only when reaching the line | pat == a -> b .

Not sure what to call the "phi_1" and "phi_2" in something like phi[phi_1/phi_2]

Substituted term? Substituting term?

It's made worse by the fact that some papers write it the opposite way, phi[phi_2/phi_1]

I guess I can call them "old" and "new"

Old and new seems fine. Substituted and subtituting is also fine. Wrapping them in data types so that people calling your method do not mix the arguments is even better, but I can't usually convince others that it's worth doing. Anyway, the issue was that you had three patterns as arguments and it was not obvious which is which.

virgil-serbanuta · 2018-07-10T16:31:27Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+    go binder s1 v p = 
+        binder s1 (replacementVar v p)
+        (subst (Var_ v) (Var_ $ replacementVar v p) p)
+    replacementVar v p = head $ alternatives v \\ (S.toList $ freeVars p)


Just curious, you don't have to fix this: why not filter with ('member' freeVars p)?

The thing about code like filter (member freeVars p) is, if you later change to a situation where asymptotics matter, it's easy to make a linear operation accidentally quadratic that way.

For instance if alternatives were also a Data.Set, set union/intersect/subtraction are O(m+n), but filtering on membership would be O(m log n).

Isn't it O(m*n) right now, where m is the first index that was not already used, and n is the free var count?

Even if my estimate is correct, I guess it may be reasonable if m is likely to be small (which, by default, it should be). I can't tell right now if it would increase when doing many similar substitutions as we execute code and produce proofs.

Whoops, I thought \ assumes sorted. Yeah, it is slower in this case.

But I just noticed: freeVars p is being called over and over in the "filter" case. That's another accident that can't happen when you use operations over whole datastructures like union/intersect/difference.

Thanks. As I said, I was just curious. We're not supposed to optimize things right now, and we should prefer code that is safer/easier to read/whatever.

Yeah I'm just explaining why I think it's a good default. For now I filtered with S.member, in the future maybe substitution could be outsourced to kmett's bound or something.

virgil-serbanuta · 2018-07-10T17:00:18Z

src/main/haskell/language-kore/test/parser/Data/Kore/ASTUtils/ASTUtilsTest.hs

+
+substitutions :: TestTree
+substitutions = testGroup "substitutions" 
+  [ testCase "subTrivial" $ assertEqual "" subTrivial subTrivialSolution


This project uses 4 spaces for indentation almost everywhere, "where" and "=" (only sometimes and only when used in function definitions) are the only exceptions I can think of right now. The main reasons for using 4 spaces are uniformity and the fact that "where" and "=" use half of a normal indentation and it looks bad when they are indented by only one space. Note that function signatures are also indented by 4 spaces instead of 2.

BTW, I think that there are places above where you're using a one-space indentation.

virgil-serbanuta · 2018-07-10T17:02:49Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

@@ -0,0 +1,129 @@
+{-|
+Module      : Data.Kore.ASTUtils.Substitution
+Description : Substitute phi_1 for phi_2, avoiding capture


Could you add a short comment or example saying why this would be useful (as opposed to substituting variables)?

virgil-serbanuta · 2018-07-10T17:11:36Z

src/main/haskell/language-kore/src/Data/Kore/AST/Common.hs

@@ -101,14 +109,16 @@ data Id level = Id
    { getId      :: !String
    , idLocation :: !AstLocation
    }
-    deriving Show
+    deriving (Show, Generic)


Just curious, not asking for a fix: Where is this generic thing used (for any of the instances defined here, not necessarily this one)?

Generic is needed to derive classes like Hashable.

virgil-serbanuta · 2018-07-10T17:14:29Z

src/main/haskell/language-kore/test/parser/Data/Kore/ASTUtils/ASTUtilsTest.hs

@@ -0,0 +1,217 @@
+{-# LANGUAGE MultiParamTypeClasses  #-}


I didn't get an answer to one of my previous questions, so I'll try asking it this way: What's the test coverage for the new code?

Do you mean hpc report ? About 70-80%

We usually use stack test --coverage and look at the html report, I guess that may use hpc behind the scenes.

That number, by itself, does not mean much. We are aiming for 100% coverage. Until now we allowed the coverage to be lower for things like automatic instance derivations and struct getters, but we usually want close to 100% for everything else. So, if the missing 20-30% are things like that, it should be fine.

virgil-serbanuta

Please take a look at the new comments before submitting ans see if they make sense.

virgil-serbanuta · 2018-07-12T12:48:33Z

src/main/haskell/language-kore/src/Data/Kore/ASTUtils/Substitution.hs

+
+-- subst2 a b = cata (\pat -> if Fix pat == a then b else Fix pat)
+
+-- handleBinder


You can leave it if it makes sense, but I'm not a fan of code that's commented out. If you allow time to pass, the code will be more and more out of date, but people will avoid deleting it since they assume it has a purpose.

virgil-serbanuta · 2018-07-12T12:53:11Z

src/main/haskell/language-kore/test/parser/Data/Kore/ASTUtils/ASTUtilsTest.hs

@@ -0,0 +1,217 @@
+{-# LANGUAGE MultiParamTypeClasses  #-}


We usually use stack test --coverage and look at the html report, I guess that may use hpc behind the scenes.

That number, by itself, does not mean much. We are aiming for 100% coverage. Until now we allowed the coverage to be lower for things like automatic instance derivations and struct getters, but we usually want close to 100% for everything else. So, if the missing 20-30% are things like that, it should be fine.

phillipharr1s added 30 commits May 30, 2018 11:36

gave FunctionalProof a proper tree structure

9b00586

mild refactoring

4aa9968

Merge branch 'master' into unification

7eb47b2

.

e7347c6

trying to create skeleton of monadic uni alg

a7471d2

skeleton of unification alg

09f698e

done all i could before introducing AST type

3babf33

need custom ProofMOnad

539676b

.

672f64f

.

0d9006c

ProofSystemWithHypos -- complete?

497f223

basic rules implemented

42550f0

should work aside from a few trivial holes

3f9288c

basic examples work

84ba0c5

cleanup

e5cd004

cleanup

f75d372

cleanup

f272608

more test cases

c9211dc

.

c117a86

.

e67a155

backwards, iff, basic proof pretty printing

39c6b30

nice pretty print output for demo

121654d

.

6d05072

added level param

5eaebcc

type sigs

4cb056e

Merge branch 'master' into unification

050445c

forgot Proof/

63944df

Merge branch 'unification' of https://github.com/u--/kore into unific…

efa63cb

…ation

reverted the original unificationImpl

7cefce6

cleanup

f3e042c

ttuegel reviewed Jul 6, 2018

View reviewed changes

.

b65c62a

virgil-serbanuta reviewed Jul 9, 2018

View reviewed changes

virgil-serbanuta mentioned this pull request Jul 9, 2018

Function evaluation #131

Merged

phillipharr1s added 7 commits July 9, 2018 13:48

.

d392196

Merge branch 'master' into smart-constructors

eb6af8c

.

d75f8e2

Merge branch 'smart-constructors' of https://github.com/u--/kore into…

930953d

… smart-constructors

should pass pedantic

12f4638

should pass --pedantic TEST too

0d08d13

hashable ast

6ebb03f

change ensureSortAgreement to return flexibleSort whenever it can

cf059ee

virgil-serbanuta reviewed Jul 10, 2018

View reviewed changes

phillipharr1s added 6 commits July 10, 2018 14:00

formatting, misc refactoring

28514e0

quick and dirty substitution test generator

226f3fa

remove potentially long tests?

1268e17

.

3238a7c

.

036df29

.

d91cc99

virgil-serbanuta approved these changes Jul 12, 2018

View reviewed changes

phillipharr1s merged commit 55f89f0 into runtimeverification:master Jul 12, 2018

phillipharr1s deleted the smart-constructors branch July 13, 2018 21:17

Stevengre mentioned this pull request Jun 17, 2025

Backend fails to simplify complex shift expressions with bitwise AND operations #4112

Open


		-- subst2 a b = cata (\pat -> if Fix pat == a then b else Fix pat)

		-- handleBinder

		import Data.Kore.ASTUtils.SmartConstructors


		subst

Smart constructors #137

Smart constructors #137

Uh oh!

Conversation

phillipharr1s commented Jul 6, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

virgil-serbanuta left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ehildenb commented Jul 10, 2018

Uh oh!

phillipharr1s commented Jul 10, 2018

Uh oh!

phillipharr1s commented Jul 10, 2018

Uh oh!

virgil-serbanuta left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!