Builtins resolution

[maowtm]

Lots of remaining questions like

• Is this the best way to implement built-in rules?

• Does built-in rules need to return more constraints? i.e. currently in the temporary "rule" constructed the body is always empty.

• Should any built-in rules "leave" any variables ungrounded at all? i.e. currently string_concat always return literal of the form string_concat(C, C, C) where C are constants. Will this be the case for all built in rules? If so then maybe we could just have builtin.apply return a vec of constants, instead of terms (and thus introducing the possibility of variable collision, unless special care is taken to only return aux or input variables).

• How should the application of built-in rules be reflected in the tree? i.e. currently it's just

  Proof {
    clause: Builtin,
    valuation: {},
    children: [],
  }

  (maybe just have every relevant variables in the clause? i.e. clause: Builtin("run", vec![Term::Constant("apt install python")]))

[maowtm]

Also since variables and constants are always generic at the moment, I have placed some C: From<String> (for constructing constants) as well as C: ToString (for getting strings out of C) trait bounds. This can be vastly simplified once we decide on what C and V should be, and apply the concrete type throughout the program... if that's something we are planning to do. Otherwise we might need a better way, like a Constant trait with methods like new_from_str or as_str, etc, and put all the Eq + Hash + ... stuff into the trait bound of that.