Change TV ranking to select src vars as a representative during unification; Nit: cleanup dot() emitting code; Nit: fix small bug in verify_semantics() - make an internal copy of src rtl to avoid clobbering of typevars re-used in multiple definitions

lib/cretonne/meta/semantics/__init__.py

@@ -31,6 +31,7 @@ def verify_semantics(inst, src, xforms):
 
     # 2) Any possible typing for the instruction should be covered by
     #    exactly ONE semantic XForm
+    src = src.copy({})
     typenv = get_type_env(ti_rtl(src, TypeEnv()))
     typenv.normalize()
     typenv = typenv.extract()

lib/cretonne/meta/semantics/primitives.py

@@ -9,7 +9,6 @@ from __future__ import absolute_import
 from cdsl.operands import Operand
 from cdsl.typevar import TypeVar
 from cdsl.instructions import Instruction, InstructionGroup
-from cdsl.ti import SameWidth
 import base.formats # noqa
 
 GROUP = InstructionGroup("primitive", "Primitive instruction set")
@@ -39,8 +38,7 @@ prim_from_bv = Instruction(
         'prim_from_bv', r"""
         Convert a flat bitvector to a real SSA Value.
         """,
-        ins=(x), outs=(real),
-        constraints=SameWidth(BV, Real))
+        ins=(fromReal), outs=(real))
 
 xh = Operand('xh', BV.half_width(),
              doc="A semantic value representing the upper half of X")

lib/cretonne/meta/semantics/test_elaborate.py

@@ -205,8 +205,8 @@ class TestElaborate(TestCase):
         assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl(
             bvx << prim_to_bv.i32x4(x),
             (bvlo, bvhi) << bvsplit.bv128(bvx),
-            lo << prim_from_bv.i32x2.bv64(bvlo),
-            hi << prim_from_bv.i32x2.bv64(bvhi))))
+            lo << prim_from_bv.i32x2(bvlo),
+            hi << prim_from_bv.i32x2(bvhi))))
 
     def test_elaborate_vconcat(self):
         # type: () -> None
@@ -227,7 +227,7 @@ class TestElaborate(TestCase):
             bvlo << prim_to_bv.i32x2(lo),
             bvhi << prim_to_bv.i32x2(hi),
             bvx << bvconcat.bv64(bvlo, bvhi),
-            x << prim_from_bv.i32x4.bv128(bvx))))
+            x << prim_from_bv.i32x4(bvx))))
 
     def test_elaborate_iadd_simple(self):
         # type: () -> None
@@ -247,7 +247,7 @@ class TestElaborate(TestCase):
             bvx << prim_to_bv.i32(x),
             bvy << prim_to_bv.i32(y),
             bva << bvadd.bv32(bvx, bvy),
-            a << prim_from_bv.i32.bv32(bva))))
+            a << prim_from_bv.i32(bva))))
 
     def test_elaborate_iadd_elaborate_1(self):
         # type: () -> None
@@ -279,7 +279,7 @@ class TestElaborate(TestCase):
             bva_3 << bvadd.bv32(bvlo_1, bvlo_2),
             bva_4 << bvadd.bv32(bvhi_1, bvhi_2),
             bvx_5 << bvconcat.bv32(bva_3, bva_4),
-            a << prim_from_bv.i32x2.bv64(bvx_5))))
+            a << prim_from_bv.i32x2(bvx_5))))
 
     def test_elaborate_iadd_elaborate_2(self):
         # type: () -> None
@@ -334,4 +334,4 @@ class TestElaborate(TestCase):
             bva_14 << bvadd.bv8(bvhi_11, bvhi_12),
             bvx_15 << bvconcat.bv8(bva_13, bva_14),
             bvx_5 << bvconcat.bv16(bvx_10, bvx_15),
-            a << prim_from_bv.i8x4.bv32(bvx_5))))
+            a << prim_from_bv.i8x4(bvx_5))))