Test PR to kick CI on FxData3

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.

src/Refinements-Parsing/NNFParser.class.st

@@ -25,7 +25,8 @@ Class {
 		'cstrPred',
 		'funcSort',
 		'sortArg',
-		'define'
+		'define',
+		'data'
 	],
 	#category : #'Refinements-Parsing'
 }
@@ -79,6 +80,35 @@ NNFParser >> cstrPred [
 	^pred parens ==> [ :x | CstrHead pred: x ]
 ]
 
+{ #category : #grammar }
+NNFParser >> data [
+	^'data' asParser trim,
+	self fTyCon trim,
+	(#digit asParser plus flatten trim ==> #asInteger),
+	$= asParser trim,
+	($| asParser trim, self dataCtor trim ==> #second) star brackets
+	==> [ :x | DataDecl
+			ddTyCon: x second
+			ddVars: x third
+			ddCtors: x fifth ]
+
+]
+
+{ #category : #grammar }
+NNFParser >> dataCtor [
+	^NNFParser upperId trim,
+	(self dataField commaSeparated optional ==> [ :x | x ifNil: [#()] ifNotNil: [x] ]) braces
+	==> [ :x | DataCtor dcName: x first dcFields: x second ]
+]
+
+{ #category : #grammar }
+NNFParser >> dataField [
+	^ NNFParser upperId trim,
+	$: asParser trim,
+	sort
+	==> [ :x | DataField dfName: x first dfSort: x last ]
+]
+
 { #category : #grammar }
 NNFParser >> decidablePred [
 	^matchedParen
@@ -234,7 +264,7 @@ NNFParser >> symSort [
 
 { #category : #grammar }
 NNFParser >> thing [
-	^(constraint / var / qualif / constant / fixpoint / define "match data") parens
+	^(constraint / var / qualif / constant / fixpoint / define "/ match" / data) parens
 ]
 
 { #category : #'grammar - util' }

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 }

src/Refinements/DataCtor.class.st

@@ -0,0 +1,72 @@
+"
+data DataCtor = DCtor
+  { dcName   :: !LocSymbol        -- ^ Ctor Name
+  , dcFields :: ![DataField]      -- ^ Ctor Fields
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+"
+Class {
+	#name : #DataCtor,
+	#superclass : #Object,
+	#instVars : [
+		'dcName',
+		'dcFields'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataCtor class >> dcName: dcName dcFields: dcFields [
+	^self basicNew
+		dcName: dcName;
+		dcFields: dcFields;
+		yourself
+]
+
+{ #category : #accessing }
+DataCtor >> dcFields [
+	^ dcFields
+]
+
+{ #category : #accessing }
+DataCtor >> dcFields: anObject [
+	dcFields := anObject
+]
+
+{ #category : #accessing }
+DataCtor >> dcName [
+	^ dcName
+]
+
+{ #category : #accessing }
+DataCtor >> dcName: anObject [
+	dcName := anObject
+]
+
+{ #category : #printing }
+DataCtor >> printOn: aStream [
+	aStream
+		nextPutAll: '↪';
+		nextPutAll: dcName;
+		nextPutAll: '('.
+	dcFields do:
+		[ :df | aStream nextPutAll: df dfName; nextPutAll: '::'. df dfSort printOn: aStream ]
+		separatedBy: [ aStream nextPutAll: ',' ].
+	aStream
+		nextPutAll: ')'
+]
+
+{ #category : #'as yet unclassified' }
+DataCtor >> smt2ctor: ts [
+	| instantiatedFields |
+	instantiatedFields := dcFields collect: [ :field | field dfName -> (field smt2field: ts) ].
+	^Z3Constructor
+		name: self symbol
+		recognizer: 'is-', self symbol
+		fields: instantiatedFields
+		referencing: (Array new: dcFields size withAll: 0)  "BOGUS, implement mutually-recursive ADTs!"	
+]
+
+{ #category : #Symbolic }
+DataCtor >> symbol [
+	^dcName
+]

src/Refinements/DataDecl.class.st

@@ -0,0 +1,99 @@
+"
+data DataDecl = DDecl
+  { ddTyCon :: !FTycon            -- ^ Name of defined datatype
+  , ddVars  :: !Int               -- ^ Number of type variables
+  , ddCtors :: [DataCtor]         -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+"
+Class {
+	#name : #DataDecl,
+	#superclass : #Object,
+	#instVars : [
+		'ddTyCon',
+		'ddVars',
+		'ddCtors'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataDecl class >> ddTyCon: ddTyCon ddVars: ddVars ddCtors: ddCtors [
+	^self basicNew
+		ddTyCon: ddTyCon;
+		ddVars: ddVars;
+		ddCtors: ddCtors;
+		yourself 
+
+]
+
+{ #category : #construction }
+DataDecl >> addToQuery: aNNFQuery [ 
+	aNNFQuery qData add: self
+]
+
+{ #category : #accessing }
+DataDecl >> ddCtors [
+	^ ddCtors
+]
+
+{ #category : #accessing }
+DataDecl >> ddCtors: anObject [
+	ddCtors := anObject
+]
+
+{ #category : #accessing }
+DataDecl >> ddTyCon [
+	^ ddTyCon
+]
+
+{ #category : #accessing }
+DataDecl >> ddTyCon: anObject [
+	ddTyCon := anObject
+]
+
+{ #category : #accessing }
+DataDecl >> ddVars [
+	^ ddVars
+]
+
+{ #category : #accessing }
+DataDecl >> ddVars: anObject [
+	ddVars := anObject
+]
+
+{ #category : #GT }
+DataDecl >> gtInspectorConstructorsIn: composite [
+	<gtInspectorPresentationOrder: 40>
+	^ composite fastList
+		title: 'Constructors';
+		display: [ ddCtors ]
+]
+
+{ #category : #'SMT monomorphisation' }
+DataDecl >> instantiateZ3Sort: ts [
+	| ctors z3datatypeSort |
+	ctors := self smt2datactors: ts.
+	z3datatypeSort := Z3DatatypeSort name: self symbol  constructors: ctors.
+	ctors do: #delete.
+	^z3datatypeSort
+]
+
+{ #category : #printing }
+DataDecl >> printOn: aStream [
+	aStream nextPutAll: 'data '.
+	aStream nextPutAll: self ddTyCon symbol
+]
+
+{ #category : #'as yet unclassified' }
+DataDecl >> smt2datactors: ts [
+	^ddCtors collect: [ :ctor | ctor smt2ctor: ts ]
+]
+
+{ #category : #Symbolic }
+DataDecl >> symbol [
+"
+instance Symbolic DataDecl where
+  symbol = symbol . ddTyCon
+"
+	^ddTyCon symbol
+]

src/Refinements/DataField.class.st

@@ -0,0 +1,53 @@
+"
+data DataField = DField
+  { dfName :: !LocSymbol          -- ^ Field Name
+  , dfSort :: !Sort               -- ^ Field Sort
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+
+"
+Class {
+	#name : #DataField,
+	#superclass : #Object,
+	#instVars : [
+		'dfName',
+		'dfSort'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataField class >> dfName: dfName dfSort: dfSort [
+	^self basicNew
+		dfName: dfName;
+		dfSort: dfSort;
+		yourself
+]
+
+{ #category : #accessing }
+DataField >> dfName [
+	^ dfName
+]
+
+{ #category : #accessing }
+DataField >> dfName: anObject [
+	dfName := anObject
+]
+
+{ #category : #accessing }
+DataField >> dfSort [
+	^ dfSort
+]
+
+{ #category : #accessing }
+DataField >> dfSort: anObject [
+	dfSort := anObject
+]
+
+{ #category : #'as yet unclassified' }
+DataField >> smt2field: ts [
+	| θ monomorphicSort |
+	θ := Dictionary newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]).
+	monomorphicSort := dfSort apply: θ.
+	^monomorphicSort z3sort
+]

src/Refinements/ECst.class.st

@@ -124,26 +124,26 @@ 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."
 
 	"(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
 ]
 

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
 ]
 

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)
 ]

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' }

src/Refinements/Equation.class.st

@@ -38,7 +38,7 @@ mkEquation f xts e out = Equ f xts e out (f `elem` syms e)
 		yourself
 ]
 
-{ #category : #adding }
+{ #category : #construction }
 Equation >> addToQuery: aHornQuery [ 
 	aHornQuery qEqns add: self
 ]