From 0c8396cf41a2b8ac3df9196dd4f828a4e2b95d9d Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Wed, 9 Oct 2024 06:08:11 -0400
Subject: [PATCH] Pass the SymEnv into #sort: indirectly through Reader

Thus, the keyword #smt2: is gone in favor of unary #smt2.
This has the advantage that we don't have to lug the SymEnv as
argument to unFApp, z3sort etc.
---
 src/PLE/Equation.extension.st         |  2 +-
 src/Refinements/BindEnv.class.st      |  4 ++--
 src/Refinements/ECst.class.st         | 10 +++++-----
 src/Refinements/EIte.class.st         |  8 ++++----
 src/Refinements/EMessageSend.class.st |  6 +++---
 src/Refinements/EVar.class.st         |  7 +++++--
 src/Refinements/Expr.class.st         |  6 +++---
 src/Refinements/Integer.extension.st  |  2 +-
 src/Refinements/PAnd.class.st         |  4 ++--
 src/Refinements/PKVar.class.st        |  2 +-
 src/Refinements/PNot.class.st         |  6 ++++++
 src/Refinements/POr.class.st          |  4 ++--
 src/Refinements/Reft.class.st         |  4 ++--
 src/Refinements/SInfo.class.st        | 17 +++++++++++------
 src/Refinements/SimpC.class.st        |  4 ++--
 src/Refinements/Solution.class.st     | 11 +++++++----
 src/Refinements/SortedReft.class.st   |  4 ++--
 src/Refinements/UncurriedApp.class.st | 12 ++++++------
 src/Refinements/Z3AST.extension.st    |  2 +-
 src/Refinements/Z3Node.extension.st   |  2 +-
 20 files changed, 67 insertions(+), 50 deletions(-)

diff --git a/src/PLE/Equation.extension.st b/src/PLE/Equation.extension.st
index 9bbb9fd1d..dae6ec364 100644
--- a/src/PLE/Equation.extension.st
+++ b/src/PLE/Equation.extension.st
@@ -19,7 +19,7 @@ instance Normalizable Equation where
 		x suffixSymbol: (eqName intSymbol: i) ].
 	evalEnv := EvalEnv ofSorts: (SEnv newFromAssociations: eqArgs), sEnv naturalTransformations.
 	body′ := eqBody evaluateIn: evalEnv.
-	body′ := body′ smt2: sEnv.
+	body′ := [ body′ smt2 ] runReader: #symbolEnv initialState: sEnv.
 	su := Dictionary newFromAssociations:  (xs zip: xs′).
 	body′ := body′ renameVariables: su.
 	body′ := body′ normalizeBody: eqName.
diff --git a/src/Refinements/BindEnv.class.st b/src/Refinements/BindEnv.class.st
index 02d146d27..ca4834e4c 100644
--- a/src/Refinements/BindEnv.class.st
+++ b/src/Refinements/BindEnv.class.st
@@ -199,10 +199,10 @@ In Smalltalk we destructively replace the indexDict in-place.
 ]
 
 { #category : #'SMT interface' }
-BindEnv >> smt2: γ [
+BindEnv >> smt2 [
 	self mapBindEnv: [ :i :x_sr |
 		| x sr |  x := x_sr key. sr := x_sr value.
-		x -> (sr smt2: γ) ]
+		x -> sr smt2 ]
 ]
 
 { #category : #accessing }
diff --git a/src/Refinements/ECst.class.st b/src/Refinements/ECst.class.st
index 031433c6f..a4072c3df 100644
--- a/src/Refinements/ECst.class.st
+++ b/src/Refinements/ECst.class.st
@@ -124,17 +124,17 @@ ECst >> printUncastOn: aStream [
 ]
 
 { #category : #'SMT interface' }
-ECst >> smt2: γ [
+ECst >> smt2 [
 	| fxyz f args |
 	(sort isKindOf: FFunc) ifTrue: [
 		| nt uncurriedSort |
 		(expr isKindOf: EVar) ifFalse: [ self error "monkey programmer at work" ].
-		nt := γ naturalTransformationFor: expr sym.
+		nt := (Context readState: #symbolEnv) naturalTransformationFor: expr sym.
 		uncurriedSort := sort uncurry.
 		^nt from: uncurriedSort dom to: uncurriedSort cod
 	].
 
-	(expr isKindOf: EApp) ifFalse: [ ^expr smt2Cast: sort in: γ ].
+	(expr isKindOf: EApp) ifFalse: [ ^expr smt2Cast: sort ].
 
 	"TODO: Investigate why control can reach here.
 	 See Issue#272."
@@ -142,8 +142,8 @@ ECst >> smt2: γ [
 	"(ECst (EApp...)):
 	Possibly need to uncurry."
 	fxyz := self splitArgs.
-	f := fxyz key smt2: γ.
-	args := fxyz value collect: [ :eachArg | eachArg key smt2: γ ].
+	f := fxyz key smt2.
+	args := fxyz value collect: [ :eachArg | eachArg key smt2 ].
 	^f valueWithArguments: args
 ]
 
diff --git a/src/Refinements/EIte.class.st b/src/Refinements/EIte.class.st
index 8ec4d4853..f8d7e5438 100644
--- a/src/Refinements/EIte.class.st
+++ b/src/Refinements/EIte.class.st
@@ -80,10 +80,10 @@ EIte >> evaluateIn: anEvalEnv ifUndeclared: vndBlock [
 ]
 
 { #category : #'SMT interface' }
-EIte >> smt2: γ [
-	^((b smt2: γ)
-		ifThen: (thenE smt2: γ)
-		else: (elseE smt2: γ)
+EIte >> smt2 [
+	^(b smt2
+		ifThen: thenE smt2
+		else: elseE smt2
 		) simplify
 ]
 
diff --git a/src/Refinements/EMessageSend.class.st b/src/Refinements/EMessageSend.class.st
index a54964767..464cdeca4 100644
--- a/src/Refinements/EMessageSend.class.st
+++ b/src/Refinements/EMessageSend.class.st
@@ -50,8 +50,8 @@ EMessageSend >> messageSend: anObject [
 ]
 
 { #category : #'SMT interface' }
-EMessageSend >> smt2: γ [
-	^(messageSend receiver smt2: γ)
+EMessageSend >> smt2 [
+	^messageSend receiver smt2
 		perform: messageSend selector
-		withArguments: (messageSend arguments collect: [ :arg | arg smt2: γ ])
+		withArguments: (messageSend arguments collect: #smt2)
 ]
diff --git a/src/Refinements/EVar.class.st b/src/Refinements/EVar.class.st
index c21f17fb5..0e9e65597 100644
--- a/src/Refinements/EVar.class.st
+++ b/src/Refinements/EVar.class.st
@@ -130,8 +130,11 @@ EVar >> readStream [
 ]
 
 { #category : #'SMT interface' }
-EVar >> smt2: aSymEnv [
-	^(aSymEnv sort at: sym) z3sort mkConst: sym
+EVar >> smt2 [
+	| preSort z3sort |
+	preSort := (Context readState: #symbolEnv) sort at: sym.
+	z3sort := preSort z3sort.
+	^z3sort mkConst: sym
 ]
 
 { #category : #'SMT interface' }
diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st
index 0cd656f19..0e39ddebc 100644
--- a/src/Refinements/Expr.class.st
+++ b/src/Refinements/Expr.class.st
@@ -438,16 +438,16 @@ Expr >> rename: a to: b [
 ]
 
 { #category : #'SMT interface' }
-Expr >> smt2: γ [
+Expr >> smt2 [
 	self shouldNotImplement
 ]
 
 { #category : #'SMT interface' }
-Expr >> smt2Cast: _ in: γ [
+Expr >> smt2Cast: _ [
 "
 smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder
 "
-	^self smt2: γ
+	^self smt2
 ]
 
 { #category : #'as yet unclassified' }
diff --git a/src/Refinements/Integer.extension.st b/src/Refinements/Integer.extension.st
index 389524596..0485df0e0 100644
--- a/src/Refinements/Integer.extension.st
+++ b/src/Refinements/Integer.extension.st
@@ -11,7 +11,7 @@ Integer >> evaluateIn: anEvalEnv ifUndeclared: vndBlock [
 ]
 
 { #category : #'*Refinements' }
-Integer >> smt2: _ [
+Integer >> smt2 [
 	^self toInt
 ]
 
diff --git a/src/Refinements/PAnd.class.st b/src/Refinements/PAnd.class.st
index c1ba10749..157114659 100644
--- a/src/Refinements/PAnd.class.st
+++ b/src/Refinements/PAnd.class.st
@@ -110,9 +110,9 @@ PAnd >> rename: a to: b [
 ]
 
 { #category : #'SMT interface' }
-PAnd >> smt2: γ [
+PAnd >> smt2 [
 	| cs |
-	cs := conjuncts collect: [ :each | each smt2: γ ].
+	cs := conjuncts collect: #smt2.
 	^(cs allSatisfy: #isConc)
 		ifTrue: [ Bool and: cs ]
 		ifFalse: [ ^self class of: cs ]
diff --git a/src/Refinements/PKVar.class.st b/src/Refinements/PKVar.class.st
index 0ed351fbf..4f3cc265e 100644
--- a/src/Refinements/PKVar.class.st
+++ b/src/Refinements/PKVar.class.st
@@ -115,7 +115,7 @@ PKVar >> s: anObject [
 ]
 
 { #category : #'SMT interface' }
-PKVar >> smt2: _ [ 
+PKVar >> smt2 [
 	^self
 ]
 
diff --git a/src/Refinements/PNot.class.st b/src/Refinements/PNot.class.st
index fc766a8e6..3589ad9aa 100644
--- a/src/Refinements/PNot.class.st
+++ b/src/Refinements/PNot.class.st
@@ -43,6 +43,12 @@ PNot >> printOn: aStream [
 	p printOn: aStream 
 ]
 
+{ #category : #'SMT interface' }
+PNot >> smt2 [
+	p isConc ifFalse: [ self shouldBeImplemented ].
+	^p smt2 not
+]
+
 { #category : #'F.Subable' }
 PNot >> subst1: ass [
 	^PNot of: (p subst1: ass)
diff --git a/src/Refinements/POr.class.st b/src/Refinements/POr.class.st
index ee96808dd..9a296ebd0 100644
--- a/src/Refinements/POr.class.st
+++ b/src/Refinements/POr.class.st
@@ -45,9 +45,9 @@ POr >> evaluateIn: aBindEnv ifUndeclared: vndBlock [
 ]
 
 { #category : #'SMT interface' }
-POr >> smt2: γ [ 
+POr >> smt2 [
 	(disjuncts allSatisfy: #isConc) ifFalse: [ self shouldBeImplemented ].
-	^Bool or: (disjuncts collect: [ :each | each smt2: γ ])
+	^Bool or: (disjuncts collect: #smt2)
 ]
 
 { #category : #'F.Subable' }
diff --git a/src/Refinements/Reft.class.st b/src/Refinements/Reft.class.st
index 1add314eb..41fe9f4cf 100644
--- a/src/Refinements/Reft.class.st
+++ b/src/Refinements/Reft.class.st
@@ -175,10 +175,10 @@ Cf. Constraints.hs
 ]
 
 { #category : #'SMT interface' }
-Reft >> smt2: γ [
+Reft >> smt2 [
 	^Reft
 		symbol: symbol
-		expr: (expr smt2: γ)
+		expr: expr smt2
 ]
 
 { #category : #'F.Subable' }
diff --git a/src/Refinements/SInfo.class.st b/src/Refinements/SInfo.class.st
index ad8d069ca..5c168399e 100644
--- a/src/Refinements/SInfo.class.st
+++ b/src/Refinements/SInfo.class.st
@@ -193,6 +193,15 @@ SInfo >> eliminatingSolverInfo [
 
 ]
 
+{ #category : #'SMT interface' }
+SInfo >> emitSMT2 [
+	| γ |
+	γ := self symbolEnv.
+	[ γ naturalTransformations: gLits.
+		γ naturalTransformations freezeNaturalTransformations.
+		self smt2 ] runReader: #symbolEnv initialState: γ
+]
+
 { #category : #'as yet unclassified' }
 SInfo >> getSubC: i [
 "
@@ -400,12 +409,8 @@ SInfo >> sanitize [
 
 { #category : #'SMT interface' }
 SInfo >> smt2 [
-	| γ |
-	γ := self symbolEnv .
-	γ naturalTransformations: gLits.
-	γ naturalTransformations freezeNaturalTransformations.
-	cm do: [ :eachC | eachC smt2: γ ].
-	bs smt2: γ.
+	cm do: #smt2.
+	bs smt2.
 ]
 
 { #category : #logic }
diff --git a/src/Refinements/SimpC.class.st b/src/Refinements/SimpC.class.st
index f1347169c..3daf9f36b 100644
--- a/src/Refinements/SimpC.class.st
+++ b/src/Refinements/SimpC.class.st
@@ -100,9 +100,9 @@ SimpC >> sinfo [
 ]
 
 { #category : #'SMT interface' }
-SimpC >> smt2: aSymEnv [
+SimpC >> smt2 [
 	"Destructively replace RHS with its Z3 AST."
-	rhs := rhs smt2: aSymEnv.
+	rhs := rhs smt2.
 	^self
 	
 ]
diff --git a/src/Refinements/Solution.class.st b/src/Refinements/Solution.class.st
index fea9c3ca5..cc7c9dd3a 100644
--- a/src/Refinements/Solution.class.st
+++ b/src/Refinements/Solution.class.st
@@ -217,9 +217,12 @@ Solution >> qbPreds: aSubst qBind: aQBind [
 qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
 Cf. Types/Solutions.hs
 "
-	| elabPred |
-	elabPred := [ :eq | ((eq pred subst: aSubst) elaborate: sEnv) smt2: sEnv ].
-	^aQBind eQuals collect: [ :eq | { elabPred value: eq . eq } ]
+	^aQBind eQuals collect: [ :eq |
+		| pred smt2 |
+		pred := (eq pred subst: aSubst) elaborate: sEnv.
+		smt2 := [ pred smt2 ] runReader: #symbolEnv initialState: sEnv.
+		{ smt2 . eq }
+	]
 ]
 
 { #category : #'as yet unclassified' }
@@ -357,7 +360,7 @@ Solution >> sScp: anObject [
 Solution >> solve_: fi ks: ks wkl: w [
 "cf. Solver/Solve.hs."
 	| s1 s2 s3 s4 res₀ s3_res0 bindingsInSmt |
-	fi smt2.
+	fi emitSMT2.
 	s1 := fi initialSolution: ks. "cf. Solve.hs"
 	s2 := self, s1.
 	bindingsInSmt := __binds concretePreds.
diff --git a/src/Refinements/SortedReft.class.st b/src/Refinements/SortedReft.class.st
index b3096ad25..c57f3a7cd 100644
--- a/src/Refinements/SortedReft.class.st
+++ b/src/Refinements/SortedReft.class.st
@@ -154,10 +154,10 @@ SortedReft >> shiftSR: i [
 ]
 
 { #category : #'SMT interface' }
-SortedReft >> smt2: γ [
+SortedReft >> smt2 [
 	^SortedReft
 		sort: sr_sort z3sort
-		reft: (sr_reft smt2: γ)
+		reft: sr_reft smt2
 ]
 
 { #category : #accessing }
diff --git a/src/Refinements/UncurriedApp.class.st b/src/Refinements/UncurriedApp.class.st
index 6770fe22c..de132aa43 100644
--- a/src/Refinements/UncurriedApp.class.st
+++ b/src/Refinements/UncurriedApp.class.st
@@ -69,19 +69,19 @@ UncurriedApp >> resultSort: anObject [
 ]
 
 { #category : #'SMT interface' }
-UncurriedApp >> smt2: γ [
+UncurriedApp >> smt2 [
 	| s α D αc |
 	s := f expr sym.
-	α := γ naturalTransformations at: s.
-	D := args collect: [ :eachArg | eachArg sort ].
+	α := (Context readState: #symbolEnv) naturalTransformations at: s.
+	D := args collect: #sort.
 	αc := α from: D to: resultSort.
-	^αc valueWithArguments: (args collect: [ :eachArg | eachArg smt2: γ ])
+	^αc valueWithArguments: (args collect: #smt2 )
 ]
 
 { #category : #'SMT interface' }
-UncurriedApp >> smt2Cast: s in: γ [
+UncurriedApp >> smt2Cast: s [
 	self assert: self resultSort = s.
-	^self smt2: γ
+	^self smt2
 	
 ]
 
diff --git a/src/Refinements/Z3AST.extension.st b/src/Refinements/Z3AST.extension.st
index 13f36cf4f..3ddaee18e 100644
--- a/src/Refinements/Z3AST.extension.st
+++ b/src/Refinements/Z3AST.extension.st
@@ -17,6 +17,6 @@ Z3AST >> evaluateIn: aBindEnv ifUndeclared: vndBlock [
 ]
 
 { #category : #'*Refinements' }
-Z3AST >> smt2: _ [ 
+Z3AST >> smt2 [
 	^self
 ]
diff --git a/src/Refinements/Z3Node.extension.st b/src/Refinements/Z3Node.extension.st
index 84b07506d..b94621eb6 100644
--- a/src/Refinements/Z3Node.extension.st
+++ b/src/Refinements/Z3Node.extension.st
@@ -21,7 +21,7 @@ Z3Node >> kvarsExpr [
 ]
 
 { #category : #'*Refinements' }
-Z3Node >> smt2Cast: aZ3Sort in: _ [
+Z3Node >> smt2Cast: aZ3Sort [
 	aZ3Sort = self sort ifFalse: [ self error ].
 	^self
 ]