diff --git a/src/Refinements/DecidableRefinement.class.st b/src/Refinements/DecidableRefinement.class.st index 1b7610750..7a009cc39 100644 --- a/src/Refinements/DecidableRefinement.class.st +++ b/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" diff --git a/src/Refinements/HReft.class.st b/src/Refinements/HReft.class.st index e9fa04a7a..7e7ca753c 100644 --- a/src/Refinements/HReft.class.st +++ b/src/Refinements/HReft.class.st @@ -98,3 +98,8 @@ HReft >> substf: f [ HReft >> syms [ ^expr syms ] + +{ #category : #private } +HReft >> uniqAbsRefsUsing: aDictionary [ + expr uniqAbsRefsUsing: aDictionary +] diff --git a/src/Refinements/PAnd.class.st b/src/Refinements/PAnd.class.st index 20c26ec18..35e6b5dc3 100644 --- a/src/Refinements/PAnd.class.st +++ b/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 ] diff --git a/src/Refinements/VariableAlphabet.class.st b/src/Refinements/VariableAlphabet.class.st index f68fc033c..8aa29e03b 100644 --- a/src/Refinements/VariableAlphabet.class.st +++ b/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 ] diff --git a/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st b/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st index e4a2f5c96..a8670c728 100644 --- a/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st +++ b/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) => { diff --git a/src/SpriteLang-Tests/L1RTypeParserTest.class.st b/src/SpriteLang-Tests/L1RTypeParserTest.class.st index af4f264d7..5ed71da30 100644 --- a/src/SpriteLang-Tests/L1RTypeParserTest.class.st +++ 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 } diff --git a/src/SpriteLang/KnownReft.class.st b/src/SpriteLang/KnownReft.class.st index 728651464..9440cdd6a 100644 --- a/src/SpriteLang/KnownReft.class.st +++ b/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. + + +] diff --git a/src/SpriteLang/RType.class.st b/src/SpriteLang/RType.class.st index 01119e7d5..e5393943f 100644 --- a/src/SpriteLang/RType.class.st +++ b/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 diff --git a/src/SpriteLang/RVar.class.st b/src/SpriteLang/RVar.class.st index 6bc6fc9d5..9f07774df 100644 --- a/src/SpriteLang/RVar.class.st +++ b/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. +] diff --git a/src/SpriteLang/RefinementParser.class.st b/src/SpriteLang/RefinementParser.class.st index f14716685..2bd640c2d 100644 --- a/src/SpriteLang/RefinementParser.class.st +++ b/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} ] ] diff --git a/src/SpriteLang/TBase.class.st b/src/SpriteLang/TBase.class.st index d2c5a0759..fea2bc076 100644 --- a/src/SpriteLang/TBase.class.st +++ b/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 " diff --git a/src/SpriteLang/TCon.class.st b/src/SpriteLang/TCon.class.st index ccfc24690..f3d9d902b 100644 --- a/src/SpriteLang/TCon.class.st +++ b/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 " diff --git a/src/SpriteLang/TFun.class.st b/src/SpriteLang/TFun.class.st index f42272436..d13ce2f61 100644 --- a/src/SpriteLang/TFun.class.st +++ b/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 diff --git a/src/SpriteLang/TRAll.class.st b/src/SpriteLang/TRAll.class.st index 659bfc2b2..9a1434c1a 100644 --- a/src/SpriteLang/TRAll.class.st +++ b/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 +] diff --git a/src/SpriteLang/UnknownReft.class.st b/src/SpriteLang/UnknownReft.class.st index 366d049fd..8735647ca 100644 --- a/src/SpriteLang/UnknownReft.class.st +++ b/src/SpriteLang/UnknownReft.class.st @@ -69,3 +69,8 @@ UnknownReft >> substf: f [ UnknownReft >> syms [ ^#() ] + +{ #category : #private } +UnknownReft >> uniqAbsRefsUsing: aDictionary [ + "Nothing to do here" +] diff --git "a/src/SpriteLang/\316\233Reft.class.st" "b/src/SpriteLang/\316\233Reft.class.st" index 0602c94b0..9879770f8 100644 --- "a/src/SpriteLang/\316\233Reft.class.st" +++ "b/src/SpriteLang/\316\233Reft.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 +]