From fd376e92d5a7b48933f2fa267c2b3c8f4808b1bf Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Tue, 29 Oct 2024 19:32:12 -0400
Subject: [PATCH] Implement beginnigs of Z3 interface for DataDecl

NB: Still no datatype recursion!!!  See e.g. Horn L5cons00data.
---
 src/Refinements/DataCtor.class.st  | 11 +++++++++++
 src/Refinements/DataDecl.class.st  | 14 ++++++++++++++
 src/Refinements/DataField.class.st |  8 ++++++++
 3 files changed, 33 insertions(+)

diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st
index f9b4be481..3df1d081a 100644
--- a/src/Refinements/DataCtor.class.st
+++ b/src/Refinements/DataCtor.class.st
@@ -55,6 +55,17 @@ 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
index d4996668d..ca2e903e6 100644
--- a/src/Refinements/DataDecl.class.st
+++ b/src/Refinements/DataDecl.class.st
@@ -69,12 +69,26 @@ DataDecl >> gtInspectorConstructorsIn: composite [
 		display: [ ddCtors ]
 ]
 
+{ #category : #'SMT interface' }
+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 : #'SMT interface' }
+DataDecl >> smt2datactors: ts [
+	^ddCtors collect: [ :ctor | ctor smt2ctor: ts ]
+]
+
 { #category : #Symbolic }
 DataDecl >> symbol [
 "
diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st
index f7aff16cc..d56fb8617 100644
--- a/src/Refinements/DataField.class.st
+++ b/src/Refinements/DataField.class.st
@@ -43,3 +43,11 @@ 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"
+]