Reification in enums

[saucisson]

Didier was trying to get all even naturals. It is possible with the following code, but we had problems.

enum Nat: Term, CustomStringConvertible {
   case zero
   case succ (Term)
   func equals(_ other: Term) -> Bool {
       return (other is Nat) && (other as! Nat == self)
   }
   var description: String {
     get {
       switch (self) {
       case .zero: return "0"
       case let .succ(x): return "s." + String (describing: x)
       }
     }
   }
  static func ==(lhs: Nat, rhs: Nat) -> Bool {
       switch (lhs, rhs) {
       case (let .succ(l), let .succ(r)):
           return l.equals(r)
       case (.zero, .zero):
           return true
       default:
           return false
       }
   }
}

func is_even(what: Term) -> Goal {
   return (what === Nat.zero) ||
          delayed (fresh { x in what === Nat.succ(Nat.succ(x)) && is_even(what:x) })
}

    func replace(term: Term, substitution: Substitution) -> Term {
      switch (term) {
      case Nat.zero:
        return Nat.zero
      case is Variable:
        return replace(term: substitution [term], substitution: substitution)
      case let Nat.succ(x):
        return Nat.succ(replace(term: x, substitution: substitution))
      default:
        return term
      }
    }

    let v = Variable(named:"v")
    let query = is_even(what:v)
    for substitution in query(State()) {
         let reified = substitution.reified()
         let value   = replace (term: reified [v], substitution: reified)
         print (value)
    }

1. The use of delayed is required. Could it be automatic?
2. Printing the result terms is awful, as there is no replacement of the variables within the enum cases. We had to write our own replace function to correctly print the results. Is there a generic solution?

[kyouko-taiga]

I don't know about the use of delayed. I should investigate more about it to give you an answer.

Regarding replace, the problem is that LogicKit has no idea about the structure of your term. Hence it can't automatically apply the substitutions. It would work out-of-the box if you had use the built-in list type rather than a custom Nat enum type.

If that kind of pattern becomes the norm, I could setup a protocol that instructs LogicKit how to unfold the recursion.