Fix DataDecl, DataCtor, DataField - squash with their introduction

shingarov · Nov 12, 2024 · a7d5ab7 · a7d5ab7
1 parent a516b70
commit a7d5ab7
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 30 deletions.
diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st
@@ -22,6 +22,13 @@ DataCtor class >> dcName: dcName dcFields: dcFields [
 		yourself
 ]
 
+{ #category : #'SMT interface' }
+DataCtor >> apply: ts [ 
+	^DataCtor
+		dcName: dcName
+		dcFields: (dcFields collect: [ :field | field apply: ts ])
+]
+
 { #category : #accessing }
 DataCtor >> dcFields [
 	^ dcFields
@@ -42,6 +49,13 @@ DataCtor >> dcName: anObject [
 	dcName := anObject
 ]
 
+{ #category : #'SMT interface' }
+DataCtor >> declare: aMonomorphizedDataDecl in: γ [
+	aMonomorphizedDataDecl
+			declare: dcName
+			accessors: (dcFields collect: [ :field | field declarationAssociation: aMonomorphizedDataDecl in: γ ])
+]
+
 { #category : #printing }
 DataCtor >> printOn: aStream [
 	aStream
@@ -55,17 +69,6 @@ DataCtor >> printOn: aStream [
 		nextPutAll: ')'
 ]
 
-{ #category : #'SMT interface' }
-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

diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st
@@ -31,6 +31,17 @@ DataDecl >> addToQuery: aNNFQuery [
 	aNNFQuery qData add: self
 ]
 
+{ #category : #'SMT interface' }
+DataDecl >> apply: ts [
+	"Given type-parametrized receiver ...@(0)...@(1)...,
+	 and actual type parameters t₀, t₁, …, answer a DataDecl with
+	 all formal type parameters substituted: ...t₀...t₁... ." 
+	^DataDecl
+		ddTyCon: (ddTyCon apply: ts)
+		ddVars: 0
+		ddCtors: (ddCtors collect: [ :ctor | ctor apply: ts])
+]
+
 { #category : #accessing }
 DataDecl >> ddCtors [
 	^ ddCtors
@@ -70,12 +81,23 @@ DataDecl >> gtInspectorConstructorsIn: composite [
 ]
 
 { #category : #'SMT interface' }
-DataDecl >> instantiateZ3Sort: ts [
-	| ctors z3datatypeSort |
-	ctors := self smt2datactors: ts.
-	z3datatypeSort := Z3DatatypeSort name: self symbol  constructors: ctors.
-	ctors do: #delete.
-	^z3datatypeSort
+DataDecl >> monomorphicDeclIn: γ [
+	| known |
+	known := [ Context readState: #knownMonomorphizedDecls ]
+		on: NoAnswer
+		do: [ :_ex | [ ^self monomorphicDeclIn: γ ] runReader: #knownMonomorphizedDecls initialState: Dictionary new ].
+	^known
+		at: ddTyCon symbol
+		ifAbsentPut: [
+			| mdd |
+			mdd := MonomorphizedDataDecl named: ddTyCon symbol encodeUnsafe.
+			known at: ddTyCon symbol put: mdd.
+			ddCtors do: [ :ctor | ctor declare: mdd in: γ ].
+			mdd
+		]
+
+
+
 ]
 
 { #category : #printing }
@@ -84,11 +106,6 @@ DataDecl >> printOn: aStream [
 	aStream nextPutAll: self ddTyCon symbol
 ]
 
-{ #category : #'SMT interface' }
-DataDecl >> smt2datactors: ts [
-	^ddCtors collect: [ :ctor | ctor smt2ctor: ts ]
-]
-
 { #category : #Symbolic }
 DataDecl >> symbol [
 "
@@ -97,3 +114,11 @@ instance Symbolic DataDecl where
 "
 	^ddTyCon symbol
 ]
+
+{ #category : #'SMT interface' }
+DataDecl >> z3sort: γ [
+	ddVars = 0 ifFalse: [ self error ].
+	^PreSort hotel
+		at: ddTyCon symbol
+		ifAbsentPut: [ (self monomorphicDeclIn: γ) create ]
+]
diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st
@@ -24,6 +24,22 @@ DataField class >> dfName: dfName dfSort: dfSort [
 		yourself
 ]
 
+{ #category : #'SMT interface' }
+DataField >> apply: ts [ 
+	| θ |
+	θ := Dictionary
+		newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]).
+	^DataField
+		dfName: dfName
+		dfSort: (dfSort apply: θ)
+]
+
+{ #category : #'SMT interface' }
+DataField >> declarationAssociation: aMonomorphizedDataDecl in: γ [
+
+	^dfName -> (dfSort monomorphicDeclIn: γ)
+]
+
 { #category : #accessing }
 DataField >> dfName [
 	^ dfName
@@ -43,11 +59,3 @@ DataField >> dfSort [
 DataField >> dfSort: anObject [
 	dfSort := anObject
 ]
-
-{ #category : #'SMT interface' }
-DataField >> smt2field: ts [
-	| θ monomorphicSort |
-	θ := Dictionary newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]).
-	monomorphicSort := dfSort apply: θ.
-	^monomorphicSort "z3sort"
-]