Uniquify all Sprite preterms before elaboartion

This commit α-renames all variables in a separate step prior elaboration
in order to avoid name clashes as demonstrated by `#testAlphaClash`.

This is similar to PR #197 but differ in several ways:

 * perform renaming as a separate step, not as part of [Chk-Lam].
 * renames all lets, not just function parameter binds
 * renames everything in single top-down traversal.

Fixes #139 (well, not quite yet)

Author: janvrany

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/ARef.class.st

@@ -99,6 +99,18 @@ ARef >> tsubstGoA: outerT tVar: outerA [
 			x -> (t rSortToRType tsubstGo: outerT tVar: outerA) rTypeToRSort ])
 ]
 
+{ #category : #'α-renaming' }
+ARef >> uniq2: α [
+	| α′ |
+	
+	α′ := α.
+	arArgs do:[:a|α′ := α′ extMap: a key to: a key uniq]. 
+
+	^self class
+		arArgs: (arArgs collect:[:a|(α′ at: a key) -> (a value uniq2: α′)])
+		arPred: (arPred uniq2: α′)
+]
+
 { #category : #'as yet unclassified' }
 ARef >> ≺+ rhs [
 	| xts1 p1 xts2 p2 su |

src/SpriteLang/Alt.class.st

@@ -59,3 +59,11 @@ Alt >> expr [
 Alt >> expr: anObject [
 	expr := anObject
 ]
+
+{ #category : #'α-renaming' }
+Alt >> uniq2: α [
+	^self class
+		daCon: daCon
+		binds: (binds collect: [ :each | each uniq2: α])
+		expr: (expr uniq2: α)
+]

src/SpriteLang/EAnn.class.st

@@ -72,3 +72,13 @@ EAnn >> synth: Γ [
 	c := expr check: Γ rtype: t.
 	^{ c . t }
 ]
+
+{ #category : #'α-renaming' }
+EAnn >> uniq2: α [
+
+	^self class
+		expr: (expr uniq2: α)
+		ann:  (ann uniq2: α)
+
+
+]

src/SpriteLang/ECase.class.st

@@ -58,6 +58,16 @@ ECase >> goSubsTyExpr: su [
 		])
 ]
 
+{ #category : #'α-renaming' }
+ECase >> uniq2: α [
+	| x′ alts′ |
+	x′ := α at: x ifAbsent:[x].
+	alts′ := alts collect: [ :each | each uniq2: α ].
+	^self class
+		x: x′ alts: alts′
+
+]
+
 { #category : #accessing }
 ECase >> x [
 	^ x

src/SpriteLang/ECon.class.st

@@ -59,3 +59,8 @@ ECon >> synthImm: Γ [
 ECon >> toFX [
 	^self shouldBeImplemented 
 ]
+
+{ #category : #'α-renaming' }
+ECon >> uniq2: α [
+	"Nothing to do"
+]

src/SpriteLang/EFun.class.st

@@ -92,3 +92,16 @@ EFun >> renameTy: ty metric: m [
 	t′′_m′′ := expr renameTy: t′ metric: m′.  t′′ := t′′_m′′ key. m′′ := t′′_m′′ value.
 	^(TFun x: x s: s′ t: t′′) -> m′′
 ]
+
+{ #category : #'α-renaming' }
+EFun >> uniq2: α [
+	| id id′ α′ |
+
+	id  := bind id.
+	id′ := α at: id ifAbsent:[id uniq].
+	α′  := α extMap: id to: id′.
+
+	^self class
+		bind: (bind uniq2: α′)
+		expr: (expr uniq2: α′)
+]

src/SpriteLang/EIf.class.st

@@ -77,3 +77,12 @@ EIf >> trueE [
 EIf >> trueE: anObject [
 	trueE := anObject
 ]
+
+{ #category : #'α-renaming' }
+EIf >> uniq2: α [
+	^self class
+		cond: (cond uniq2: α)
+		trueE: (trueE uniq2: α)
+		falseE: (falseE uniq2: α).
+
+]

src/SpriteLang/EImm.class.st

@@ -51,3 +51,14 @@ EImm >> synth: Γ [
 	t := imm synthImm: Γ.
 	^{ HCstr cTrue . t }
 ]
+
+{ #category : #'as yet unclassified' }
+EImm >> uniq [
+	"Nothing to do. This is only called on 'sentinel' EImm terminating list of ELet decls"
+]
+
+{ #category : #'α-renaming' }
+EImm >> uniq2: α [
+	^self class imm: (imm uniq2: α)
+
+]

src/SpriteLang/ELet.class.st

@@ -79,3 +79,38 @@ ELet >> goSubsTyExpr: su [
 ELet >> gtChildren [
 	^{decl . expr}
 ]
+
+{ #category : #'α-renaming' }
+ELet >> uniq [
+	"α-rename all variables ensuring all have unique names.
+	 Returns a new instance."
+
+	| α decl′ expr′ |
+
+	α := αRenames empty.
+	decl′ := decl class bind: decl bind expr: (decl expr uniq2: α).
+	expr′ := expr uniq.
+
+	^self class
+		decl: decl′
+		expr: expr′
+
+
+
+
+]
+
+{ #category : #'α-renaming' }
+ELet >> uniq2: α [
+	| id id′ α′ decl′ expr′ |
+
+	id := decl bind id.
+	id′:= α at: id ifAbsent:[id uniq].
+	α′ := α extMap: id to: id′.
+
+	decl′ := decl class bind: (decl bind uniq2: α′) expr: (decl expr uniq2: α)."<-- CERTAINLY NOT α!!!"
+	expr′ := expr uniq2: α′.
+
+	^self class decl: decl′ expr: expr′
+
+]

src/SpriteLang/ERApp.class.st

@@ -41,3 +41,10 @@ ERApp >> synth: Γ [
 	s′ := s rinst.
 	^{ c . s′ }
 ]
+
+{ #category : #'α-renaming' }
+ERApp >> uniq2: α [
+	^self class
+		expr: (expr uniq2: α)
+
+]

src/SpriteLang/ETApp.class.st

@@ -55,3 +55,11 @@ ETApp >> synth: Γ [
 	tt := Γ refresh: rtype.
 	^{ ce . te type tsubst: tt tVar: te var }
 ]
+
+{ #category : #'α-renaming' }
+ETApp >> uniq2: α [
+	^self class
+		expr: (expr uniq2: α)
+		rtype: (rtype uniq2: α)
+
+]

src/SpriteLang/ETLam.class.st

@@ -64,3 +64,8 @@ ETLam >> tvar [
 ETLam >> tvar: anObject [
 	tvar := anObject
 ]
+
+{ #category : #'α-renaming' }
+ETLam >> uniq2: α [
+	self shouldBeImplemented
+]

src/SpriteLang/EVar.extension.st

@@ -53,3 +53,12 @@ synthImm :: Env -> SrcImm -> CG RType
 	t := Γ getEnvDamit: sym. 
 	^t singleton: sym
 ]
+
+{ #category : #'*SpriteLang' }
+EVar >> uniq2: α [
+	| sym′ |
+
+	sym′ := α at: sym ifAbsent:[ ^ self ].
+	^self class of: sym′
+
+]

src/SpriteLang/Expr.extension.st

@@ -11,6 +11,21 @@ predRType p = TBase TBool (known $ F.predReft p)
 		r: self "F."predReft known
 ]
 
+{ #category : #'*SpriteLang' }
+Expr >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	| self′ |
+
+	self′ := self.
+	α keysAndValuesDo: [ :orig :uniq |
+		self′ := self′ rename: orig to: uniq.
+	].
+	^ self′
+
+
+]
+
 { #category : #'*SpriteLang' }
 Expr >> ΛpredReft [
 	^self predReft known

src/SpriteLang/HPred.extension.st

@@ -47,3 +47,11 @@ smash p           = [p]
 HPred >> subsAR: p ar: ar [
 	^self "No κ-apps can happen, because those have been refactored to RefVarApps"
 ]
+
+{ #category : #'*SpriteLang' }
+HPred >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self shouldBeImplemented
+
+]

src/SpriteLang/HPredAnd.extension.st

@@ -23,3 +23,9 @@ HPredAnd >> subs: p ar: ar [
 HPredAnd >> subsAR: aString ar: anARef [
 	^HPredAnd of: (ps collect: [ :each | each subsAR: aString ar: anARef ])
 ]
+
+{ #category : #'*SpriteLang' }
+HPredAnd >> uniq2: α [
+	^self class of: (ps collect: [:e|e uniq2: α])
+
+]

src/SpriteLang/HReft.extension.st

@@ -14,3 +14,9 @@ HReft >> predExprsGo [
 HReft >> subs: p ar: ar [
 	^self
 ]
+
+{ #category : #'*SpriteLang' }
+HReft >> uniq2: α [
+	^self class expr: (expr uniq2: α)
+
+]

src/SpriteLang/KnownReft.class.st

@@ -163,3 +163,14 @@ KnownReft >> symbol: anObject [
 KnownReft >> syms [
 	^{symbol}, expr syms
 ]
+
+{ #category : #'α-renaming' }
+KnownReft >> uniq2: α [
+	| symbol′ α′ expr′ |
+
+	symbol′ := α at: symbol ifAbsent:[symbol uniq].
+	α′ := α extMap: symbol to: symbol′.
+	expr′ := expr uniq2: α′.
+
+	^self class symbol: symbol′ expr: expr′
+]

src/SpriteLang/MetricExpression.class.st

@@ -59,6 +59,16 @@ MetricExpression >> subst: su [
 	^self class source: replacement sym
 ]
 
+{ #category : #'α-renaming' }
+MetricExpression >> uniq2: α [
+	| source′ |
+	
+	source′ := α at: source ifAbsent:[^self].
+	^self class source: source′
+	
+
+]
+
 { #category : #'as yet unclassified' }
 MetricExpression >> wfExpr: γ sort: t [
 "

src/SpriteLang/Prog.class.st

@@ -82,11 +82,13 @@ Prog >> solve [
 
 { #category : #verification }
 Prog >> vcgen [
-	| env eL cstr query |
+	| expr′ env expr′′ cstr query |
+
+	expr′ := expr uniq.
 	env := ΓContext empEnv: meas typs: data.
-	eL := expr elaborate: env.
+	expr′′ := expr′ elaborate: env.
 	CGState reset.
-	cstr := eL check: env rtype: TInt instance bTrue.
+	cstr := expr′′ check: env rtype: TInt instance bTrue.
 	query := HornQuery new.
 	cstr addToQuery: query.
 	CGState current cgInfo cgiKVars do: [ :kVar | kVar addToQuery: query ].

src/SpriteLang/RType.class.st

@@ -137,6 +137,17 @@ closeType :: [RVar] -> [(F.Symbol, RType)] -> RType -> RType
 	^rvParams generalize
 ]
 
+{ #category : #'α-renaming' }
+RType >> collectαRenames: α [
+	"Create (but not apply!) all neccessary α-renames
+	 and return updated renames. See SpriteAnn >> #uniq2: why
+	 this is needed."
+	
+	^ self subclassResponsibility 	
+	
+
+]
+
 { #category : #polymorphism }
 RType >> dispatchUnify: t1 [
 	"The 'normal' case where we just fall through to unifyLL:."
@@ -516,6 +527,13 @@ unify :: F.SrcSpan -> RType -> RType -> ElabM RType
 	^t2 dispatchUnify: self
 ]
 
+{ #category : #'α-renaming' }
+RType >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self subclassResponsibility.
+]
+
 { #category : #'as yet unclassified' }
 RType >> ≺ [ t
 	self subclassResponsibility 

src/SpriteLang/RVar.class.st

@@ -122,3 +122,13 @@ RVar >> tsubstGoP: t′ tVar: a [
 		rvArgs: newRvArgs;
 		yourself
 ]
+
+{ #category : #'α-renaming' }
+RVar >> uniq2: α [
+	| rvName′ | 
+	
+	rvName′ := α at: rvName ifAbsent:[^self].
+	^self class
+		rvName: rvName′ 
+		rvArgs: (rvArgs collect:[:e|e uniq2: α])
+]

src/SpriteLang/RefVarApp.extension.st

@@ -27,3 +27,10 @@ go (H.Var k xs) | k == p ...
 	θ := yts zip: xs with: [ :y_☐ :x | y_☐ key -> x ].
 	^pr substs: θ
 ]
+
+{ #category : #'*SpriteLang' }
+RefVarApp >> uniq2: α [
+	^self class
+		var: (α at: var ifAbsent:[var])
+		args: (args collect:[:arg|α at: arg ifAbsent:[arg]])
+]

src/SpriteLang/Refl.class.st

@@ -3,3 +3,10 @@ Class {
 	#superclass : #SpriteAnn,
 	#category : #SpriteLang
 }
+
+{ #category : #'α-renaming' }
+Refl >> uniq2: α [
+
+	self shouldBeImplemented
+
+]