Implement F.DataDecl on top of Z3 Datatypes

src/Refinements-Parsing/FQParser.class.st

@@ -29,6 +29,7 @@ FQParser >> def [
 	^ self fixpoint
 	/ self constraint
 	/ self iBind
+	/ data
 	/ 'everything else' asParser
 ]
 

src/Refinements-Parsing/FixpointParser.class.st

@@ -5,7 +5,8 @@ Class {
 		'sort',
 		'sortArg',
 		'funcSort',
-		'pred'
+		'pred',
+		'data'
 	],
 	#category : #'Refinements-Parsing'
 }
@@ -20,6 +21,34 @@ FixpointParser class >> upperId [
 	^(#uppercase asParser, (#word asParser / $_ asParser) star) flatten
 ]
 
+{ #category : #grammar }
+FixpointParser >> data [
+	^'data' asParser trim,
+	self fTyCon trim,
+	PPParser decimalNat trim,
+	$= asParser trim,
+	($| asParser trim, self dataCtor trim ==> #second) star brackets
+		==> [ :x | DataDecl
+			ddTyCon: x second
+			ddVars: x third
+			ddCtors: x fifth ]
+]
+
+{ #category : #grammar }
+FixpointParser >> dataCtor [
+	^FixpointParser upperId trim,
+	(self dataField commaSeparated optional ==> [ :x | x ifNil: [#()] ifNotNil: [x] ]) braces
+	==> [ :x | DataCtor dcName: x first dcFields: x second ]
+]
+
+{ #category : #grammar }
+FixpointParser >> dataField [
+	^ FixpointParser upperId trim,
+	$: asParser trim,
+	sort
+	==> [ :x | DataField dfName: x first dfSort: x last ]
+]
+
 { #category : #grammar }
 FixpointParser >> fTyCon [
 	^ ('Int' asParser ==> [ :x | Int tyCon ])

src/Refinements-Parsing/NNFParser.class.st

@@ -78,7 +78,7 @@ NNFParser >> hThing [
 		/ self fixpoint
 		/ define
 		" / match"
-		" / data"
+		/ data
 	) parens
 ]
 

src/Refinements-Tests/FQPosTest.class.st

@@ -31,3 +31,24 @@ constraint:
   tag [1]
 '
 ]
+
+{ #category : #tests }
+FQPosTest >> testEqConstr1 [
+	self provePos: '
+data Thing 0 = [
+  | Cons {Head : int}
+]
+
+bind 0 a : {v: Thing | Bool true }
+bind 1 x : {v: Thing | Bool true }
+bind 2 y : {v: `a    | Bool true }
+
+constraint:
+  env [0; 1; 2]
+  lhs {v:int | x === y }
+  rhs {v:int | y === x }
+  id 1 tag []
+'.
+
+
+]

src/Refinements/DataCtor.class.st

@@ -0,0 +1,75 @@
+"
+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 : #'SMT interface' }
+DataCtor >> apply: ts [ 
+	^DataCtor
+		dcName: dcName
+		dcFields: (dcFields collect: [ :field | field apply: ts ])
+]
+
+{ #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 : #'SMT interface' }
+DataCtor >> declare: aMonomorphizedDataDecl in: γ [
+	aMonomorphizedDataDecl
+			declare: dcName
+			accessors: (dcFields collect: [ :field | field declarationAssociation: aMonomorphizedDataDecl in: γ ])
+]
+
+{ #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 : #Symbolic }
+DataCtor >> symbol [
+	^dcName
+]

src/Refinements/DataDecl.class.st

@@ -0,0 +1,124 @@
+"
+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 : #'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
+]
+
+{ #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 interface' }
+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 }
+DataDecl >> printOn: aStream [
+	aStream nextPutAll: 'data '.
+	aStream nextPutAll: self ddTyCon symbol
+]
+
+{ #category : #Symbolic }
+DataDecl >> symbol [
+"
+instance Symbolic DataDecl where
+  symbol = symbol . ddTyCon
+"
+	^ddTyCon symbol
+]
+
+{ #category : #'SMT interface' }
+DataDecl >> z3sort: γ [
+	ddVars = 0 ifFalse: [ self error ].
+	^PreSort hotel
+		at: ddTyCon symbol
+		ifAbsentPut: [ (self monomorphicDeclIn: γ) create ]
+]

src/Refinements/DataField.class.st

@@ -0,0 +1,61 @@
+"
+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 : #'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
+]
+
+{ #category : #accessing }
+DataField >> dfName: anObject [
+	dfName := anObject
+]
+
+{ #category : #accessing }
+DataField >> dfSort [
+	^ dfSort
+]
+
+{ #category : #accessing }
+DataField >> dfSort: anObject [
+	dfSort := anObject
+]

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
 ]

src/Refinements/FApp.class.st

@@ -72,6 +72,26 @@ FApp >> hash [
 	^s hash
 ]
 
+{ #category : #hotel }
+FApp >> monomorphicDeclIn: γ [
+	"Like fappSmtSort but don't go all the way to Z3.
+	 Do we want to keep this layer?"
+	(s isKindOf: FTC) ifFalse: [ self error ].
+	s isSetCon ifTrue: [ self error ].
+	s isMapCon ifTrue: [ self shouldBeImplemented ].
+	s isBitVec ifTrue: [ self shouldBeImplemented ].
+
+	^(s maybeDataIn: γ)
+		ifNil: [ self error]
+		ifNotNil: [ :d |
+			| instance ct_ts ct ts |
+			ct_ts := self unFApp.  ct := ct_ts first.  ts := ct_ts allButFirst.
+			instance := d apply: (ts collect: [ :each | each z3sort: γ ]).
+			instance monomorphicDeclIn: γ
+
+		]
+]
+
 { #category : #printing }
 FApp >> printOn: aStream [
 	aStream nextPutAll: '(FApp '.

src/Refinements/FInfo.class.st

@@ -41,7 +41,7 @@ but at least textually consistent with LF.
 	quals := OrderedCollection new.
 	gLits := SEnv new.
 	kuts := Kuts new.
-	ddecls := OrderedCollection new.
+	ddecls := defs select: [ :def | def isKindOf: DataDecl ].
 	ae := AxiomEnv new.
 	options := QueryOptions new.
 ]