INCOMPLETE, still can't compile

core/src/main/scala/shapesafe/core/Const.scala

@@ -1,11 +1,9 @@
 package shapesafe.core
 
-import shapeless.Witness
-
 object Const {
 
   type NoName = ""
-  lazy val NoNameW: Witness.Aux[NoName] = Witness[NoName]
+  lazy val NoNameW: "" = ""
 
   object True // TODO: should already exists in scala library
   type True = True.type

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

@@ -19,7 +19,7 @@ trait SymbolicTuples[VB] extends Tuples {
   class Eye extends Backbone.Eye with Tuple {
 
     final override type _ConsExpr[T <: HasNotation] = T#Notation
-    final override type Notation = EYE.T
+    final override type Notation = EYE.type
   }
   override val Eye = new Eye
 

core/src/main/scala/shapesafe/core/arity/Arity.scala

@@ -1,12 +1,13 @@
 package shapesafe.core.arity
 
-import shapeless.{Nat, Witness}
+import ai.acyclic.prover.commons.refl.XInt
+import shapeless.Nat
 import shapesafe.core.arity.ConstArity.{Derived, Literal}
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.arity.ops.ArityOpsLike
 import shapesafe.core.axis.Axis
 import shapesafe.core.debugging.CanReason
-import shapesafe.core.{arity, Const, XInt}
+import shapesafe.core.{arity, Const}
 
 import scala.language.implicitConversions
 
@@ -57,7 +58,7 @@ trait Arity extends CanReason with ArityOpsLike with Axis {
       prove: ReasonTo[O]
   ): ^[O] = eval(prove)
 
-  final override val nameW: Witness.Aux[Const.NoName] = Const.NoNameW
+  final override val nameW: Const.NoName = Const.NoNameW
 }
 
 object Arity {
@@ -80,8 +81,8 @@ object Arity {
 
   val Unchecked: ^[arity.Unchecked.type] = arity.Unchecked.^
 
-  def apply(w: Witness.Lt[XInt]): ^[Literal[w.T]] = {
-    ^(Literal.shapeless(w))
+  def apply[S <: XInt](w: S): ^[Literal[S]] = {
+    ^(Literal(w))
   }
 
   object FromNat {

core/src/main/scala/shapesafe/core/arity/ConstArity.scala

@@ -1,8 +1,7 @@
 package shapesafe.core.arity
 
+import ai.acyclic.prover.commons.refl.XInt
 import ai.acyclic.prover.commons.same.Same
-import shapeless.Witness
-import shapesafe.core.XInt
 import shapesafe.core.arity.Utils.Op
 import singleton.ops.{==, Require}
 
@@ -20,20 +19,18 @@ trait ConstArity[S] extends LeafArity with Same.ByEquality.IWrapper {
       proof: S =:= N2
   ): Unit = {}
 
-  def proveEqualType[N2](
+  def proveEqualType[N2 <: XInt](
       implicit
       proof: Require[S == N2]
   ): Unit = {}
 
   // TODO: should be named proofEqual, require should do everything in runtime?
-  def proveEqual(w: Witness.Lt[Int])(
+  def proveEqual[N2 <: XInt](n2: N2)(
       implicit
-      proof: Require[S == w.T]
+      proof: Require[S == N2]
   ): Unit = {
 
-    proveEqualType[w.T]
-
-    require(w.value == runtimeValue)
+    require(n2 == runtimeValue)
   }
 }
 
@@ -63,14 +60,10 @@ object ConstArity {
 
     implicit def summon[S <: XInt](
         implicit
-        w: Witness.Aux[S]
+        w: ValueOf[S]
     ): Literal[S] = {
       new Literal[S](w.value)
     }
 
-    def shapeless(w: Witness.Lt[XInt]): Literal[w.T] = {
-
-      Literal.summon[w.T](w)
-    }
   }
 }

core/src/main/scala/shapesafe/core/arity/binary/Op2.scala

@@ -38,7 +38,7 @@ object Op2 extends Op2_Imp0 {
       // TODO: can this be VerifiedArity?
 
       override type _RefuteTxt =
-        DebugConst.REFUTE.T + DebugConst.ILLEGAL_OP.T + A1#SymbolTxt + SS[
+        DebugConst.REFUTE.type + DebugConst.ILLEGAL_OP.type + A1#SymbolTxt + SS[
           Unit,
           Unit
         ]#SymbolTxt + A2#SymbolTxt

core/src/main/scala/shapesafe/core/arity/binary/Require2.scala

@@ -43,7 +43,7 @@ object Require2 extends Require2_Imp0 {
     ) extends Conjecture2[A1, A2] {
 
       override type _RefuteTxt =
-        DebugConst.REFUTE.T + A1#SymbolTxt + SS[Unit, Unit]#Negation#SymbolTxt + A2#SymbolTxt
+        DebugConst.REFUTE.type + A1#SymbolTxt + SS[Unit, Unit]#Negation#SymbolTxt + A2#SymbolTxt
 
       override lazy val runtimeValue: Int = {
         val v1 = a1.runtimeValue

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

@@ -1,11 +1,10 @@
 package shapesafe.core.axis
 
+import ai.acyclic.prover.commons.refl.{XInt, XString}
 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.{HasNotation, Notations}
-import shapesafe.core.{XInt, XString}
 
 import scala.language.implicitConversions
 
@@ -32,15 +31,15 @@ object Axis {
       N <: XString
   ](
       val arityType: A,
-      val nameW: Witness.Aux[N]
+      val nameW: N
   ) extends Axis
       //      with KeyTag[N, D :<<- N]
       // TODO: remove? FieldType[] has some black magic written in macro
       {
 
     type _ArityType = A
 
-    type _Axis = _ArityType :<<- Name
+    type _Axis = _ArityType :<<- N
 
     trait NameAsNotation extends HasNotation {
 
@@ -55,19 +54,16 @@ object Axis {
     }
   }
 
-  def apply(
+  def apply[N <: XString](
       value: Arity,
-      name: Witness.Lt[XString]
-  ): :<<-[value._ArityType, name.T] = {
+      name: N
+  ): :<<-[value._ArityType, N] = {
 
     new :<<-(value.arityType, name)
   }
 
-  implicit def fromXInt[V <: XInt](v: V)(
-      implicit
-      toW: Witness.Aux[V]
-  ): Arity.^[ConstArity.Literal[V]] = {
+  implicit def fromXInt[V <: XInt](v: V): Arity.^[ConstArity.Literal[V]] = {
 
-    Arity(toW)
+    Arity(v)
   }
 }

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

@@ -1,29 +1,28 @@
 package shapesafe.core.axis
 
-import shapesafe.core.XString
+import ai.acyclic.prover.commons.refl.XString
 import shapesafe.core.arity.Arity
 import shapesafe.core.arity.ops.HasArity
 import shapesafe.core.axis.Axis.:<<-
-import shapeless.Witness
 
 trait AxisLike extends HasArity {
 
-  val nameW: Witness.Lt[XString]
-  final type Name = nameW.T
+  val nameW: XString
+  final type Name = nameW.type
 
-  final def name: Name = nameW.value
+  final def name: Name = nameW
 
   def nameless: Arity.^[_ArityType] = arityType.^
 
   def namedT[S <: XString](
       implicit
-      name: Witness.Aux[S]
+      name: S
   ): _ArityType :<<- S = Axis(nameless, name)
 
-  def named(name: Witness.Lt[XString]): _ArityType :<<- name.T = {
+  def named[S <: XString](name: S): _ArityType :<<- S = {
 
     namedT(name)
   }
 
-  def :<<-(name: Witness.Lt[XString]): _ArityType :<<- name.T = namedT(name)
+  def :<<-[S <: XString](name: S): _ArityType :<<- S = namedT(name)
 }

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

@@ -1,10 +1,11 @@
 package shapesafe.core.axis
 
+import ai.acyclic.prover.commons.refl.XString
 import shapesafe.core.arity.binary.Op2Like
 import shapesafe.core.arity.{ArityType, LeafArity}
 import shapesafe.core.axis.Axis.->>
 import shapeless.ops.record.{Modifier, Selector}
-import shapeless.{::, HList, Witness}
+import shapeless.{::, HList}
 
 class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
@@ -16,13 +17,13 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
     implicit def ifOldName[
         OLD <: HList,
-        N <: String,
+        N <: XString,
         A1 <: ArityType,
         A2 <: ArityType,
         O <: LeafArity
     ](
         implicit
-        name: Witness.Aux[N],
+        name: ValueOf[N],
         selector: Selector.Aux[OLD, N, A1],
         lemma: op.On[A1, A2] |- O
     ): (OLD, N ->> A2) =>> ((N ->> O) :: OLD) = {
@@ -32,7 +33,7 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
         case (old, field) =>
           import shapeless.record._
 
-          val d1 = old.apply(name)
+          val d1 = selector.apply(old)
           val d2 = field: A2
 
           val oped = op.on(d1.^, d2.^)
@@ -52,13 +53,13 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
     implicit def ifOldName[
         OLD <: HList,
-        N <: String,
+        N <: XString,
         A1 <: ArityType,
         A2 <: ArityType,
         O <: LeafArity
     ](
         implicit
-        name: Witness.Aux[N],
+        name: N,
         selector: Selector.Aux[OLD, N, A1], // TODO: how to remove this? should be implied in modifier
         lemma: op.On[A1, A2] |- O,
         modifier: Modifier[OLD, N, A1, O]

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

@@ -1,6 +1,5 @@
 package shapesafe.core.debugging
 
-import shapeless.Witness
 import singleton.ops.{+, ITE, IsString}
 
 object DebugConst {
@@ -19,37 +18,37 @@ object DebugConst {
   //    TypeToLiteral.Type.Case[T1]
   //  ]
 
-  val SPACE4 = Witness("    ")
-  val shades_+ = Witness(" ░▒▓")
-  val shades_- = Witness("▓▒░ ")
+  final val SPACE4 = "    "
+  final val shades_+ = " ░▒▓"
+  final val shades_- = "▓▒░ "
 
-  type Stripe[T] = SPACE4.T + shades_-.T + T + shades_+.T + "\n\n"
+  type Stripe[T] = SPACE4.type + shades_-.type + T + shades_+.type + "\n\n"
 
   // TODO: add another instance that shows reasoning process?
 
-//  val LF = Witness("\n")
+//  val LF = ("\n")
 
-  val EMPTY = Witness("")
+  val EMPTY = ""
 
-  val REFUTE =
-    Witness("""¯\_(ツ)_/¯ """)
-  val PEEK =
-    Witness("""      """)
-  val EQUIV =
-    Witness("""  :=  """)
+  final val REFUTE =
+    """¯\_(ツ)_/¯ """
+  final val PEEK =
+    """      """
+  final val EQUIV =
+    """  :=  """
 
-  type EquivLF = "\n" + EQUIV.T
+  type EquivLF = "\n" + EQUIV.type
 
   type CannotEval = Stripe["cannot evaluate"]
 
-  val ILLEGAL_OP = Witness("""(Illegal Operation) """)
+  final val ILLEGAL_OP = """(Illegal Operation) """
 
-  val IMPOSSIBLE = Witness("IMPOSSIBLE!")
+  final val IMPOSSIBLE = "IMPOSSIBLE!"
 
   type Br[T] = "(" + T + ")"
 
-  val FROM1 = Witness("\n\n... with 1 prior >\n\n")
-  val FROM2 = Witness("\n\n... with 2 priors >\n\n")
+  final val FROM1 = "\n\n... with 1 prior >\n\n"
+  final val FROM2 = "\n\n... with 2 priors >\n\n"
 
   val INTERNAL_ERROR = "[INTERNAL ERROR] Please submit a bug report using the following expression ..."
 }

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

@@ -42,7 +42,7 @@ trait Reporters extends HasTheory {
           lemma: A |- S,
           vizA: PeekCTAux[A#Notation, VA],
           vizS: PeekCTAux[ExprOf[S], VS],
-          mk: (PEEK.T + VS + EquivLF + VA + "\n") { type Out <: XString }
+          mk: (PEEK.type + VS + EquivLF + VA + "\n") { type Out <: XString }
       ): A =>> mk.Out =
         at[A].defining(_ => mk.value)
     }
@@ -55,7 +55,7 @@ trait Reporters extends HasTheory {
       ](
           implicit
           vizS: PeekCTAux[ExprOf[S], VS],
-          op: (PEEK.T + VS + "\n") { type Out <: XString }
+          op: (PEEK.type + VS + "\n") { type Out <: XString }
       ): S =>> op.Out =
         at[S].defining(_ => op.value)
     }

core/src/main/scala/shapesafe/core/logic/binary/RingAxioms.scala

@@ -14,7 +14,7 @@ trait RingAxioms[D, :+[A <: D, B <: D] <: D, :*[A <: D, B <: D] <: D, _0 <: D, _
         A <: D,
         B <: D,
         C <: D
-    ] = forAll[A :* (B :+ C)].=>> { v =>
+    ]: theory.Theorem[A :* (B :+ C) |- (A :* B :+ (A :* C))] = forAll[A :* (B :+ C)].=>> { v =>
       val (l, r) = deconstruct(v)
       val (rl, rr) = group_+.deconstruct(r)
 
@@ -28,7 +28,7 @@ trait RingAxioms[D, :+[A <: D, B <: D] <: D, :*[A <: D, B <: D] <: D, _0 <: D, _
         A <: D,
         B <: D,
         C <: D
-    ] = forAll[(A :+ B) :* C].=>> { v =>
+    ]: theory.Theorem[A :+ B :* C |- (A :* C :+ (B :* C))] = forAll[(A :+ B) :* C].=>> { v =>
       val (l, r) = deconstruct(v)
       val (ll, lr) = group_+.deconstruct(l)
 

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

@@ -4,8 +4,5 @@ import ai.acyclic.prover.commons.function.PreDef
 
 package object core {
 
-  type XInt = Int with Singleton
-  type XString = String with Singleton
-
   type AdHocPoly1 = PreDef.Poly
 }