α-rename all pvar binders in refined type signatures

This commit renames all variable in refinement predicates to use distinct
names. This is done by `#uniqAbsRefs` at parse time - LH seems to do the
same thing (also at parse time).

The heart of is `#uniqAbsRefsUsing:` defined accordingly in number of
classes - perhaps, some implementation is missing but in that case,
MA should fail early with either DNU or "subclass responsibility".

With this change, all tests are passing, including `#testAlphaClash`.

Fixes #139.

See:

[1]: ucsd-progsys/liquidhaskell#1907
[2]: https://github.com/ucsd-progsys/liquidhaskell/blob/255fb4a1260906

src/Refinements/DecidableRefinement.class.st

@@ -116,6 +116,17 @@ DecidableRefinement >> uniq1: α [
 	^self
 ]
 
+{ #category : #private }
+DecidableRefinement >> uniqAbsRefsUsing: aDictionary [
+	self tree variableNodes do:[:node|
+		| name |
+
+		name := node name.
+		name := aDictionary at: name ifAbsent:[name].
+		node name: name.
+	]
+]
+
 { #category : #'well-formedness' }
 DecidableRefinement >> wfIn: gamma [
 self shouldBeImplemented "true if self is a bool-(unrefined-)typed formula"

src/Refinements/HReft.class.st

@@ -98,3 +98,8 @@ HReft >> substf: f [
 HReft >> syms [
 	^expr syms
 ]
+
+{ #category : #private }
+HReft >> uniqAbsRefsUsing: aDictionary [
+	expr uniqAbsRefsUsing: aDictionary
+]

src/Refinements/PAnd.class.st

@@ -138,6 +138,11 @@ PAnd >> substf: f [
 	^self class of: (conjuncts collect: [ :each | each substf: f ])
 ]
 
+{ #category : #private }
+PAnd >> uniqAbsRefsUsing: aDictionary [
+	conjuncts do:[:e|e uniqAbsRefsUsing: aDictionary]
+]
+
 { #category : #'well-formedness' }
 PAnd >> wfIn: gamma [ 
 	^self conjuncts allSatisfy: [ :c | c wfIn: gamma ]

src/Refinements/VariableAlphabet.class.st

@@ -9,7 +9,12 @@ Class {
 
 { #category : #API }
 VariableAlphabet class >> freshVariableName [
+	^self freshVariableName:'VV'
+]
+
+{ #category : #API }
+VariableAlphabet class >> freshVariableName: prefix [
 	j isNil ifTrue: [ j:= 0 ].
 	j := j + 1.
-	^'VV', j printString 
+	^prefix, j printString
 ]

src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st

@@ -93,7 +93,6 @@ BoolGaloisConnectionTest >> testAlphaClash [
 	 so must end up in the same UNSAFE result.
 	 However, this breaks, see issue #139.
 	"
-	self skip. "Remove this skip after #139 is resolved."
 	self proveUnsafe: '
 ⟦val b2i : b:bool => int[i | ((i===0) not <=> b) & ((i===0)|(i===1)) ] ⟧
 let b2i = (b) => {

src/SpriteLang-Tests/L1RTypeParserTest.class.st

@@ -19,7 +19,7 @@ L1RTypeParserTest >> testAnn [
 	ann := RTypeParser new end parse: '⟦val x : int [v|v=42]⟧'.
 	self assert: ann symbol equals: 'x'.
 	self assert: ann rtype b == TInt instance.
-	self assert: ann rtype r symbol equals: 'v'.
+	self assert: (ann rtype r symbol beginsWith: 'v_').
 ]
 
 { #category : #tests }
@@ -37,7 +37,7 @@ L1RTypeParserTest >> testAnnot [
 	ann := RTypeParser new annot end parse: 'val x : int [v|v=42]'.
 	self assert: ann symbol equals: 'x'.
 	self assert: ann rtype b == TInt instance.
-	self assert: ann rtype r symbol equals: 'v'.
+	self assert: (ann rtype r symbol beginsWith: 'v_').
 ]
 
 { #category : #tests }

src/SpriteLang/KnownReft.class.st

@@ -163,3 +163,22 @@ KnownReft >> symbol: anObject [
 KnownReft >> syms [
 	^{symbol}, expr syms
 ]
+
+{ #category : #private }
+KnownReft >> uniqAbsRefsUsing: aDictionary [
+	| oldSymbol newSymbol |
+
+	self assert: (aDictionary includesKey: oldSymbol) not. "???"
+
+	oldSymbol := symbol.
+	newSymbol := VariableAlphabet freshVariableName: symbol , '_'.
+
+	aDictionary at: oldSymbol put: newSymbol.
+
+	symbol := newSymbol.
+	expr uniqAbsRefsUsing: aDictionary.
+
+	aDictionary removeKey: oldSymbol.
+
+
+]

src/SpriteLang/RType.class.st

@@ -516,6 +516,26 @@ unify :: F.SrcSpan -> RType -> RType -> ElabM RType
 	^t2 dispatchUnify: self
 ]
 
+{ #category : #private }
+RType >> uniqAbsRefs [
+	"
+	α-rename all pvar binders. See [1], [2] and [3] why this is
+	needed.
+
+	[1]: https://github.com/shingarov/MachineArithmetic/issues/139
+	[2]: https://github.com/ucsd-progsys/liquidhaskell/issues/1907
+	[3]: https://github.com/ucsd-progsys/liquidhaskell/blob/255fb4a126090618c1e646c31fb10291710b367b/src/Language/Haskell/Liquid/Parse.hs#L568
+	"
+	^self uniqAbsRefsUsing: Dictionary new.
+]
+
+{ #category : #private }
+RType >> uniqAbsRefsUsing: renames [
+	"See #uniqAbsRefs"
+
+	^self subclassResponsibility
+]
+
 { #category : #'as yet unclassified' }
 RType >> ≺ [ t
 	self subclassResponsibility 

src/SpriteLang/RVar.class.st

@@ -122,3 +122,8 @@ RVar >> tsubstGoP: t′ tVar: a [
 		rvArgs: newRvArgs;
 		yourself
 ]
+
+{ #category : #'as yet unclassified' }
+RVar >> uniqAbsRefsUsing: aCollection [
+	self shouldBeImplemented.
+]

src/SpriteLang/RefinementParser.class.st

@@ -186,7 +186,7 @@ here Sig is just type-alias for (F.Symbol, RType, Maybe Metric)
 	$: asParser trim,
 	rtype trim,
 	self metricP optional
-	==> [ :x | {x third . x fifth . x sixth} ]
+	==> [ :x | {x third . x fifth uniqAbsRefs . x sixth} ]
 
 ]
 

src/SpriteLang/TBase.class.st

@@ -214,6 +214,11 @@ TBase >> unifyLL: t [
 	self error: 'Cant unify'
 ]
 
+{ #category : #private }
+TBase >> uniqAbsRefsUsing: renames [
+	r uniqAbsRefsUsing: renames
+]
+
 { #category : #'as yet unclassified' }
 TBase >> ≺ [ t
 "

src/SpriteLang/TCon.class.st

@@ -250,6 +250,11 @@ TCon >> unifyLL: tcon2 [
 	^TCon c: c ts: newTs ars: #() r: ΛReft new
 ]
 
+{ #category : #private }
+TCon >> uniqAbsRefsUsing: aDictionary [
+	r uniqAbsRefsUsing: aDictionary
+]
+
 { #category : #'as yet unclassified' }
 TCon >> ≺ [ tcon2
 "

src/SpriteLang/TFun.class.st

@@ -238,6 +238,12 @@ TFun >> unifyLL: tfun2 [
 	^TFun x: x_ s: s_ t: t_
 ]
 
+{ #category : #private }
+TFun >> uniqAbsRefsUsing: renames [
+	s uniqAbsRefsUsing: renames.
+	t uniqAbsRefsUsing: renames.
+]
+
 { #category : #accessing }
 TFun >> x [
 	^ x

src/SpriteLang/TRAll.class.st

@@ -139,3 +139,10 @@ go (TRAll p t)      = TRAll  (goP p) (go t)
 		r: (r tsubstGoP: t′ tVar: a)
 		t: (t tsubstGo: t′ tVar: a)
 ]
+
+{ #category : #private }
+TRAll >> uniqAbsRefsUsing: aDictionary [
+	"FIXME: shall we recurse into r (RVar) here?"
+	"r uniqAbsRefsUsing: aDictionary."
+	t uniqAbsRefsUsing: aDictionary
+]

src/SpriteLang/UnknownReft.class.st

@@ -69,3 +69,8 @@ UnknownReft >> substf: f [
 UnknownReft >> syms [
 	^#()
 ]
+
+{ #category : #private }
+UnknownReft >> uniqAbsRefsUsing: aDictionary [
+	"Nothing to do here"
+]

src/SpriteLang/ΛReft.class.st

@@ -75,3 +75,10 @@ freshR :: F.SrcSpan -> Env -> F.Sort -> Reft -> CG Reft
 	"instance F.Subable Reft where..."
 	self subclassResponsibility
 ]
+
+{ #category : #private }
+ΛReft >> uniqAbsRefsUsing: aDictionary [
+	"See RType >> #uniqAbsRefs"
+
+	self subclassResponsibility
+]