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)

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/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

@@ -90,3 +90,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′ := 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′:= 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′ := symbol uniq.
+	α′ := α extMap: symbol to: symbol′.
+	expr′ := expr uniq2: α′.
+
+	^self class symbol: symbol′ expr: expr′
+]

src/SpriteLang/MetricExpression.class.st

@@ -59,6 +59,13 @@ MetricExpression >> subst: su [
 	^self class source: replacement sym
 ]
 
+{ #category : #'α-renaming' }
+MetricExpression >> uniq2: α [
+
+	self shouldBeImplemented
+
+]
+
 { #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

@@ -516,6 +516,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/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 shouldBeImplemented
+
+]

src/SpriteLang/Refl.class.st

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

src/SpriteLang/SpriteAnn.class.st

@@ -92,3 +92,15 @@ SpriteAnn >> symbol [
 SpriteAnn >> symbol: anObject [
 	symbol := anObject
 ]
+
+{ #category : #'α-renaming' }
+SpriteAnn >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	^self class
+		symbol: symbol
+		rtype: (rtype uniq2: α)
+		metric: (metric ifNotNil:[metric uniq2: α])
+
+
+]

src/SpriteLang/SpriteBind.class.st

@@ -7,6 +7,11 @@ Class {
 	#category : #SpriteLang
 }
 
+{ #category : #accessing }
+SpriteBind class >> id: id [
+	^self basicNew id: id; yourself
+]
+
 { #category : #accessing }
 SpriteBind class >> identifier: id [
 	^self basicNew id: id; yourself
@@ -29,3 +34,8 @@ SpriteBind >> printOn: aStream [
 		nextPutAll: id;
 		nextPutAll: '"'
 ]
+
+{ #category : #'α-renaming' }
+SpriteBind >> uniq2: α [
+	^self class id: (α at: id ifAbsent:[id])
+]

src/SpriteLang/String.extension.st

@@ -43,3 +43,10 @@ rVar :: F.Symbol -> RType
 String >> unifyX: anotherString [ 
 	^self
 ]
+
+{ #category : #'*SpriteLang' }
+String >> uniq [
+	"Return new unique variable name suitable for
+	 α-renaming."
+	^self, '__ß', VariableAlphabet nextJ printString
+]

src/SpriteLang/TAll.class.st

@@ -154,6 +154,17 @@ TAll >> type: anObject [
 	type := anObject
 ]
 
+{ #category : #'α-renaming' }
+TAll >> uniq2: α [
+	| α′ var′ type′ |
+
+	var′ := var uniq.
+	α′ := α extMap: var to: var′.
+	type′ := type uniq2: α′.
+
+	^self class var: var′ type: type′
+]
+
 { #category : #accessing }
 TAll >> var [
 	^ var