Tuple moved to prover-commons

minor cleanup

core/src/main/scala/shapesafe/core/SymbolicTuples.scala

@@ -0,0 +1,43 @@
+package shapesafe.core
+
+import ai.acyclic.prover.commons.tuple.{ProductTuples, Tuples}
+import shapesafe.core.debugging.{HasNotation, Notations}
+import ai.acyclic.prover.commons.tuple.ProductTuples.EYE
+
+trait SymbolicTuples[VB] extends Tuples {
+
+  final type VBound = VB
+
+  object Backbone extends ProductTuples[VB]
+
+  trait Tuple extends Backbone.Tuple with HasNotation {
+
+//    final type Cons[HH <: VB] = BoneNotation.this.><[this.type, VB]
+    type _ConsExpr[PEEK <: HasNotation]
+  }
+
+  class Eye extends Backbone.Eye with Tuple {
+
+    final override type _ConsExpr[T <: HasNotation] = T#Notation
+    final override type Notation = EYE.T
+  }
+  override val Eye = new Eye
+
+  class ><[
+      TAIL <: Tuple,
+      HEAD <: VB
+  ](
+      tail: TAIL,
+      head: HEAD
+  ) extends Backbone.><[TAIL, HEAD](tail, head)
+      with Tuple {
+
+    type PeekHead <: HasNotation
+
+    final override type _ConsExpr[PEEK <: HasNotation] = Notations.><[this.Notation, PEEK#Notation]
+    final override type Notation = TAIL#_ConsExpr[PeekHead]
+  }
+
+  final override def cons[TAIL <: Tuple, HEAD <: VBound](tail: TAIL, head: HEAD): TAIL >< HEAD =
+    new ><(tail, head)
+}

core/src/main/scala/shapesafe/core/axis/Axis.scala

@@ -4,12 +4,12 @@ import ai.acyclic.prover.commons.same.Same
 import shapeless.Witness
 import shapeless.labelled.FieldType
 import shapesafe.core.arity.{Arity, ArityType, ConstArity}
-import shapesafe.core.debugging.{CanPeek, Notations}
+import shapesafe.core.debugging.{HasNotation, Notations}
 import shapesafe.core.{XInt, XString}
 
 import scala.language.implicitConversions
 
-trait Axis extends AxisLike with Same.ByEquality.IWrapper with CanPeek {
+trait Axis extends AxisLike with Same.ByEquality.IWrapper with HasNotation {
   // TODO:; can be a subclass of shapeless KeyTag
 
   final type Field = FieldType[Name, _ArityType]
@@ -42,12 +42,12 @@ object Axis {
 
     type _Axis = _ArityType :<<- Name
 
-    trait CanPeekName extends CanPeek {
+    trait NameAsNotation extends HasNotation {
 
       override type Notation = Name
     }
 
-    override type Notation = Notations.:<<-[A#Notation, CanPeekName#Notation]
+    override type Notation = Notations.:<<-[A#Notation, NameAsNotation#Notation]
 
     override lazy val toString: String = {
       if (name.isEmpty) s"$arityType"

core/src/main/scala/shapesafe/core/debugging/CanRefute.scala

@@ -1,6 +1,6 @@
 package shapesafe.core.debugging
 
-trait CanRefute extends CanPeek {
+trait CanRefute extends HasNotation {
 
   type _RefuteTxt
 

core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala

@@ -3,7 +3,7 @@ package shapesafe.core.debugging
 import ai.acyclic.prover.commons.graph.local.Local
 import ai.acyclic.prover.commons.meta.ProductDiscovery
 
-trait ExpressionType extends CanPeek {}
+trait ExpressionType extends HasNotation {}
 
 object ExpressionType {
 

core/src/main/scala/shapesafe/core/debugging/CanPeek.scala → core/src/main/scala/shapesafe/core/debugging/HasNotation.scala

@@ -1,6 +1,6 @@
 package shapesafe.core.debugging
 
-trait CanPeek {
+trait HasNotation {
 
   type Notation
   // use TypeVizCT macro

core/src/main/scala/shapesafe/core/debugging/NotationsLike.scala

@@ -43,13 +43,13 @@ object NotationsLike {
 
     trait On[A] {}
 
-    type Apply[AA <: CanPeek] = On[AA#Notation]
+    type Apply[AA <: HasNotation] = On[AA#Notation]
   }
   trait Proto2 {
 
     trait On[A, B] {}
 
-    type Apply[AA <: CanPeek, BB <: CanPeek] = On[AA#Notation, BB#Notation]
+    type Apply[AA <: HasNotation, BB <: HasNotation] = On[AA#Notation, BB#Notation]
   }
 
 }

core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala

@@ -9,23 +9,23 @@ trait ProofWithReasoning extends ProofSystem with Reporters {
 
   trait Reasoner {
 
-    type Goal <: CanPeek
+    type Goal <: HasNotation
 
-    object Peek extends PeekReporter[CanPeek, Goal]
-    type Peek[I <: CanPeek] = Peek.CaseFrom[I]
+    object Peek extends PeekReporter[HasNotation, Goal]
+    type Peek[I <: HasNotation] = Peek.CaseFrom[I]
 
-    object Interrupt extends InterruptReporter[CanPeek, Goal]
-    type Interrupt[I <: CanPeek] = Interrupt.CaseFrom[I]
+    object Interrupt extends InterruptReporter[HasNotation, Goal]
+    type Interrupt[I <: HasNotation] = Interrupt.CaseFrom[I]
 
     trait ReasoningMixin {
       self: Proof[_, _] =>
     }
 
-    type |-@-[I <: CanPeek, O <: Goal] = (I |- O) with ReasoningMixin
+    type |-@-[I <: HasNotation, O <: Goal] = (I |- O) with ReasoningMixin
 
     object ReasoningMixin {
 
-      implicit def reason[I <: CanPeek, P <: Consequent](
+      implicit def reason[I <: HasNotation, P <: Consequent](
           implicit
           reporter: Peek.CaseFrom[I],
           prove: Proof[I, P]

core/src/main/scala/shapesafe/core/debugging/Reporters.scala

@@ -13,16 +13,16 @@ trait Reporters extends HasTheory {
 
   import Reporters._
 
-  trait ProofReporter[IUB <: CanPeek, TGT <: CanPeek] extends Reporter {
+  trait ProofReporter[IUB <: HasNotation, TGT <: HasNotation] extends Reporter {
 
     import shapesafe.core.debugging.DebugConst._
     import theory._
 
-    type ExprOf[T <: CanPeek] = T#Notation
+    type ExprOf[T <: HasNotation] = T#Notation
 
     trait Step1_Imp3 extends AdHocPoly1 {
 
-      implicit def raw[A <: CanPeek, VA <: XString](
+      implicit def raw[A <: HasNotation, VA <: XString](
           implicit
           vizA: PeekCTAux[A#Notation, VA],
           mk: (CannotEval + VA + "\n") { type Out <: XString }
@@ -33,7 +33,7 @@ trait Reporters extends HasTheory {
     trait Step1_Imp2 extends Step1_Imp3 {
 
       implicit def eval[
-          A <: CanPeek,
+          A <: HasNotation,
           S <: TGT,
           VA <: XString,
           VS <: XString
@@ -50,7 +50,7 @@ trait Reporters extends HasTheory {
     trait Step1_Imp1 extends Step1_Imp2 {
 
       implicit def alreadyEvaled[
-          S <: TGT with CanPeek,
+          S <: TGT with HasNotation,
           VS <: XString
       ](
           implicit
@@ -63,12 +63,12 @@ trait Reporters extends HasTheory {
     override object Step1 extends Step1_Imp1
   }
 
-  trait PeekReporter[IUB <: CanPeek, TGT <: CanPeek] extends ProofReporter[IUB, TGT] {
+  trait PeekReporter[IUB <: HasNotation, TGT <: HasNotation] extends ProofReporter[IUB, TGT] {
 
     override type EmitMsg[T] = Emit.Info[T]
   }
 
-  trait InterruptReporter[IUB <: CanPeek, TGT <: CanPeek] extends ProofReporter[IUB, TGT] {
+  trait InterruptReporter[IUB <: HasNotation, TGT <: HasNotation] extends ProofReporter[IUB, TGT] {
 
     override type EmitMsg[T] = Emit.Error[T]
   }

core/src/main/scala/shapesafe/core/package.scala

@@ -1,7 +1,11 @@
 package shapesafe
 
+import ai.acyclic.prover.commons.function.PreDef
+
 package object core {
 
   type XInt = Int with Singleton
   type XString = String with Singleton
+
+  type AdHocPoly1 = PreDef.Poly
 }

core/src/main/scala/shapesafe/core/shape/Dimensions.scala

@@ -1,7 +1,8 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.tuple.ProductTuples
+import shapesafe.core.SymbolicTuples
 import shapesafe.core.arity.ArityType
-import shapesafe.core.tuple.Bone
 
 // should it be "Arities"?
-object Dimensions extends Bone[ArityType] {}
+object Dimensions extends SymbolicTuples[ArityType] {}

core/src/main/scala/shapesafe/core/shape/Index.scala

@@ -1,11 +1,11 @@
 package shapesafe.core.shape
 
 import shapesafe.core.arity.Utils.NatAsOp
-import shapesafe.core.debugging.CanPeek
+import shapesafe.core.debugging.HasNotation
 import ai.acyclic.prover.commons.same.Same
 import shapeless.{Nat, Witness}
 
-trait Index extends Same.ByEquality.IWrapper with CanPeek {
+trait Index extends Same.ByEquality.IWrapper with HasNotation {
 
   def value: Any
   final override protected def samenessDelegatedTo = value

core/src/main/scala/shapesafe/core/shape/Indices.scala

@@ -1,6 +1,7 @@
 package shapesafe.core.shape
 
-import shapesafe.core.tuple.{Bone, Tuples}
+import ai.acyclic.prover.commons.tuple.Tuples
+import shapesafe.core.SymbolicTuples
 
 trait Indices extends IndicesMagnet with Indices.Backbone.Tuple {
 
@@ -13,7 +14,7 @@ object Indices extends Tuples {
 
   type VBound = Index
 
-  object Backbone extends Bone[VBound] {}
+  object Backbone extends SymbolicTuples[VBound] {}
 
   type Tuple = Indices
 

core/src/main/scala/shapesafe/core/shape/Names.scala

@@ -1,24 +1,24 @@
 package shapesafe.core.shape
 
-import shapesafe.core.XString
-import shapesafe.core.debugging.CanPeek
-import shapesafe.core.shape.args.ApplyLiterals
-import shapesafe.core.tuple._
+import ai.acyclic.prover.commons.tuple._
 import shapeless.Witness
+import shapesafe.core.debugging.HasNotation
+import shapesafe.core.shape.args.ApplyLiterals
+import shapesafe.core.{SymbolicTuples, XString}
 
 import scala.language.implicitConversions
 
-trait Names extends IndicesMagnet with Names.Proto.Tuple {}
+trait Names extends IndicesMagnet with Names.Backbone.Tuple {}
 
 object Names extends Tuples with ApplyLiterals.ToNames {
 
   type VBound = XString // expand to take all String for gradual typing?
 
-  object Proto extends Bone[VBound] {}
+  object Backbone extends SymbolicTuples[VBound] {}
 
   type Tuple = Names
 
-  class Eye extends Proto.Eye with Names {
+  class Eye extends Backbone.Eye with Names {
     override type AsIndices = Indices.Eye
 
     override def asIndices: Indices.Eye = Indices.Eye
@@ -31,17 +31,19 @@ object Names extends Tuples with ApplyLiterals.ToNames {
   ](
       override val tail: TAIL,
       override val head: HEAD
-  ) extends Proto.><[TAIL, HEAD](tail, head)
+  ) extends Backbone.><[TAIL, HEAD](tail, head)
       with Tuple {
 
     val headW: Witness.Aux[HEAD] = Witness[HEAD](head).asInstanceOf[Witness.Aux[HEAD]]
 
     override type AsIndices = Indices.><[tail.AsIndices, Index.Name[HEAD]]
 
-    override def asIndices: AsIndices =
+    override def asIndices: AsIndices = {
+      import Indices._
       tail.asIndices >< Index.Name(headW)
+    }
 
-    trait PeekHead extends CanPeek {
+    trait PeekHead extends HasNotation {
       override type Notation = Head
     }
   }

core/src/main/scala/shapesafe/core/shape/StaticShape.scala

@@ -1,13 +1,13 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.tuple.Tuples
 import shapeless.{::, HList, HNil, Nat, Succ, Witness}
+import shapesafe.core.Const.NoName
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.arity.{Arity, ArityType, ConstArity}
 import shapesafe.core.axis.Axis
 import shapesafe.core.axis.Axis.{->>, :<<-}
-import shapesafe.core.Const.NoName
-import shapesafe.core.tuple.{Bone, Tuples}
-import shapesafe.core.{XInt, XString}
+import shapesafe.core.{SymbolicTuples, XInt, XString}
 
 /**
   * a thin wrapper of HList that has all proofs of constraints included this saves compiler burden and reduces error
@@ -32,7 +32,7 @@ object StaticShape extends Tuples {
 
   final type VBound = Axis
 
-  object Backbone extends Bone[VBound]
+  object Backbone extends SymbolicTuples[VBound]
   type Proto = Backbone.Tuple
 
   final type Tuple = StaticShape