Revise the type inference part

[izgzhen]

Esp. the higher order structures like Map, Set. Interestingly, currently we don't need to infer function type because there is a SMTContext::_funcContext which should include everything you need.

[izgzhen]

I am trying to embed the small language directly inside Haskell. See embed branch for details.

[izgzhen]

Looks like the easiest solution to embed qualifier would be make variable not embedded at all...I should make a demo lang for this.

[izgzhen]

@zjhmale Ok, I am finally comfortable with its current status now（强迫症终于缓和一点了，赶紧滚去复习期末考）, although it has several problems:

First, Assertion is not type-safe, for example forall v1 v2. (Z3Encoded v1, Z3Encoded v2) => v1 -> v2 -> Assertion, it doesn't require v1 and v2 to be the same Eq v => v. We can make stronger requirements here, but that would render the naive term language (rather than a real eDSL in Haskell) in Z3.Demo invalid.

Second, pretty lame is that the qualifier still needs a String binder and a concrete Type. By using Template Haskell, we might be able to resolve this (though it can be difficult IMO).

[zjhmale]

it seems difficult to make HeteroList deriving Eq so as to derive Eq for Term 😂 , i will try later.

it doesn't require v1 and v2 to be the same Eq v => v.

agreed. binder here is a little bit redundent.

Second, pretty lame is that the qualifier still needs a String binder and a concrete Type. By using Template Haskell, we might be able to resolve this (though it can be difficult IMO).

[izgzhen]

You are right, HeteroList is a bad idea. Originally we have manually typed term, so it is possible to bake the Eq logic into our Infer part

[izgzhen]

Looks like TH would be the only way out, unless we manually manage the the Inference etc. It works good, just not that extensible and elegant

[zjhmale]

writing Macro is eggache 😂

Looks like TH would be the only way out, unless we manually manage the the Inference etc. It works good, just not that extensible and elegant

[izgzhen]

I agree

On 8 Jun 2016, at 8:46 PM, (λ . λ) notifications@github.com wrote:

writing Macro is eggache 😂

Looks like TH would be the only way out, unless we manually manage the the Inference etc. It works good, just not that extensible and elegant

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/izgzhen/z3-encoding/issues/3#issuecomment-224577782, or mute the thread https://github.com/notifications/unsubscribe/AG1hxj0EM1EDgVsTZeyx3G8rC8vi4IEBks5qJrmjgaJpZM4Iv5i8.

[zjhmale]

sorry, i work on #6 before i see this comment, and do you mean hard code the Eq logic? maybe i'm misunderstanding with this comment.

You are right, HeteroList is a bad idea. Originally we have manually typed term, so it is possible to bake the Eq logic into our Infer part

[zjhmale]

actually i can not figure out the infer part for now, maybe i should play with z3-haskell first, i used to play with z3 use smtlib2 format scripts.

[izgzhen]

@zjhmale I originally mean to write something like forall v. (Eq v, Z3Encoded v) => v -> v -> Assertion, but it will require us to inject everything that can appear at that place to be embedded into Haskell type system.

6 is cool anyway, better than no constraint at all :P

[izgzhen]

@zjhmale no hurry. The z3-haskell's interface is not type-safe anyway, so we are not worse at least. I think it is an interesting topic to work on though.

[zjhmale]

ok. so... (那我先去复习啦 😂 )

[izgzhen]

I am planning to re-introduce type checking to Z3Pred

[izgzhen]

Now it is checked by Haskell compiler