Refactor Prog>>vcgen

src/Refinements/HornQuery.class.st

@@ -54,7 +54,7 @@ Cf. Info.hs
 { #category : #'instance creation' }
 HornQuery class >> fromThings: things [ 
 	| q |
-	q := self new.
+	q := self basicNew.
 	things do: [ :x | x addToQuery: q ].
 	^q
 ]
@@ -101,10 +101,23 @@ HornQuery class >> hornVariables: ks smalltalkBlock: aBlockClosure [
 	^self fromThings: {cstr}, ks
 ]
 
-{ #category : #'as yet unclassified' }
-HornQuery >> addPapp: j [ 
-	(HCon papp: j) addToQuery: self.
-	(Qualifier pappQual: j) addToQuery: self
+{ #category : #'instance creation' }
+HornQuery class >> mkQuery_qs: qs ks: ks cstr: c syms: syms defs: defs ddecls: ddecls [
+"
+mkQuery :: [F.Qualifier]
+        -> [H.Var a]
+        -> H.Cstr a
+        -> M.HashMap F.Symbol F.Sort
+        -> [F.Equation]
+        -> [F.DataDecl]
+        -> H.Query a
+"
+	^self basicNew qs: qs ks: ks cstr: c syms: syms defs: defs ddecls: ddecls
+]
+
+{ #category : #'instance creation' }
+HornQuery class >> new [
+	self shouldNotImplement
 ]
 
 { #category : #accessing }
@@ -288,6 +301,22 @@ HornQuery >> qMats: anObject [
 	qMats := anObject
 ]
 
+{ #category : #'private - initialization' }
+HornQuery >> qs: qs ks: ks cstr: c syms: syms defs: defs ddecls: ddecls [
+	qualifiers := qs.
+	vars := ks.
+	qCstr := {c}.
+	qCon := syms.
+	qDis := Dictionary new.
+	qEqns := defs.
+	qMats := #().
+	qData := ddecls.
+
+	defs isEmpty ifFalse: [ HOpt rewrite addToQuery: self ].
+
+	^self
+]
+
 { #category : #accessing }
 HornQuery >> qualifiers [
 	"qualifiers over which to solve cstrs"
@@ -304,7 +333,7 @@ HornQuery >> solve [
 				solve
 ]
 
-{ #category : #private }
+{ #category : #accessing }
 HornQuery >> vars [
 	"κ-vars, with parameter-sorts"
 	vars isNil ifTrue: [ vars := OrderedCollection new ].

src/SpriteLang/CGInfo.class.st

@@ -32,7 +32,7 @@ CGInfo >> addReflectVar: f rtype: t xts: xts outputSort: ot expr: e [
 		expr: e
 		sort: ot.
 	self cgiDefs add: fDef.
-	self cgiConsts add: (HCon symbol: f sort: t rtypeSort)
+	self cgiConsts add: f -> t rtypeSort
 ]
 
 { #category : #API }

src/SpriteLang/HCstr.extension.st

@@ -23,6 +23,11 @@ mkHead :: F.SrcSpan -> H.Pred -> SrcCstr
 	^CstrAnd of: (smashed collect: #cHead)
 ]
 
+{ #category : #'*SpriteLang' }
+HCstr >> strengthenInv: aΓContext [
+	^self
+]
+
 { #category : #'*SpriteLang' }
 HCstr class >> subPs: coll1 _: coll2 [
 	| p1 p1s p2 p2s |	

src/SpriteLang/Prog.class.st

@@ -93,22 +93,26 @@ Prog >> solve [
 
 { #category : #verification }
 Prog >> vcgen [
-	| expr′ env expr′′ c_cgi c cgi query |
+	| expr′ env eL ps pqs c_cgi c cgi rfls syms c′ query |
 	expr′ := expr uniq2.
 	env := ΓContext empEnv: meas typs: data.
-	expr′′ := expr′ elaborate: env.
-	c_cgi := [ expr′′ check: env rtype: TInt instance bTrue ] runCG.
-	c := c_cgi key. cgi := c_cgi value.
-	query := HornQuery new.
-	c addToQuery: query.
-	cgi cgiKVars do: [ :kVar | kVar addToQuery: query ].
-	quals do: [ :q | q addToQuery: query ].
-	query qCon: (Dictionary newFromAssociations: meas).	
-	#(1 2 3) do: [ :j | query addPapp: j ].
-	cgi cgiDefs   do: [ :equ  | equ  addToQuery: query ].
-	cgi cgiConsts do: [ :con  | con  addToQuery: query ].
-	cgi cgiDefs isEmpty ifFalse: [
-		HOpt rewrite addToQuery: query
+	eL := expr′ elaborate: env.
+	ps := #(1 2 3) collect: [ :j |
+		| hcon |
+		hcon := HCon papp: j.
+		hcon symbol -> hcon sort
 	].
-	^query
+	pqs := #(1 2 3) collect: [ :j | Qualifier pappQual: j ].
+	c_cgi := [ eL check: env rtype: TInt instance bTrue ] runCG.
+	c := c_cgi key. cgi := c_cgi value.
+	rfls := cgi cgiConsts.
+	syms := Dictionary newFromAssociations: ps, meas, rfls.
+	c′ := c strengthenInv: env.
+	^HornQuery
+		mkQuery_qs: quals, pqs
+		ks: cgi cgiKVars
+		cstr: "cI &" c′
+		syms: syms
+		defs: cgi cgiDefs
+		ddecls: #()
 ]