Cleaned up spec creation

examples/contracts/dev.contract

@@ -455,6 +455,6 @@ keeps_distance_raw = compose over car:
 keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE,
     MIN_DIST,
     max_brake=MAX_BRAKE,
-    max_accel=MAX_ACCEL) using LeanProof("KeepsDistanceRefinement")
+    max_accel=MAX_ACCEL) using LeanRefinementProof("KeepsDistanceRefinement")
 
 verify keeps_distance

src/scenic/contracts/contracts.py

@@ -1,7 +1,9 @@
 from abc import ABC, abstractmethod
+from copy import deepcopy
 from functools import cached_property
 
-from scenic.contracts.specifications import SpecNode
+from scenic.contracts.specifications import ASTSpecTransformer, SpecNode
+from scenic.syntax.compiler import NameConstantTransformer
 
 
 class Contract:
@@ -13,16 +15,40 @@ def __init__(self, **kwargs):
         self.definitions = props[0]
         self.assumptions_props = props[1]
         self.guarantees_props = props[2]
-        self.assumptions = [
-            SpecNode.propToSpec(a, contract_veneer._syntaxTrees)
-            for a in self.assumptions_props
+
+        offset = self.def_id_offset
+        def_names = list(self.definitions.keys())
+        self.def_syntaxTrees = {
+            def_names[i]: deepcopy(contract_veneer._syntaxTrees[offset + i])
+            for i in range(len(self.definitions))
+        }
+        offset += len(self.definitions)
+        self.assumption_syntaxTrees = [
+            deepcopy(contract_veneer._syntaxTrees[offset + i])
+            for i in range(len(self.assumptions_props))
         ]
-        self.guarantees = [
-            SpecNode.propToSpec(g, contract_veneer._syntaxTrees)
-            for g in self.guarantees_props
+        offset += len(self.assumptions_props)
+        self.guarantee_syntaxTrees = [
+            deepcopy(contract_veneer._syntaxTrees[offset + i])
+            for i in range(len(self.guarantees_props))
         ]
 
         self.kwargs = kwargs
+        constant_transformer = NameConstantTransformer(self.kwargs)
+        for tree in (
+            list(self.def_syntaxTrees.values())
+            + self.assumption_syntaxTrees
+            + self.guarantee_syntaxTrees
+        ):
+            constant_transformer.visit(tree)
+
+        spec_transformer = ASTSpecTransformer(self.def_syntaxTrees)
+        self.assumptions = [
+            spec_transformer.convert(a) for a in self.assumption_syntaxTrees
+        ]
+        self.guarantees = [
+            spec_transformer.convert(g) for g in self.guarantee_syntaxTrees
+        ]
 
         # TODO: Handle contracts w/ more than one object
         assert len(self.objects) <= 1

src/scenic/contracts/refinement.py

@@ -9,7 +9,7 @@ def __init__(self, stmt, contract, method):
         self.contract = contract
         self.method = method
 
-        self.method.check()
+        self.method.check(self.stmt, self.contract)
 
     @cached_property
     def assumptions(self):
@@ -51,11 +51,13 @@ def evidenceSummary(self):
         return string
 
 
-class LeanProof:
+class LeanRefinementProof:
     def __init__(self, proof_loc):
         self.proof_loc = proof_loc
 
-    def check(self):
+    def check(self, stmt, contract):
+        # breakpoint()
+        #
         pass
 
     def __str__(self):