Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Investigate smt2Cast and the as x T pattern #272

Open
shingarov opened this issue May 3, 2024 · 0 comments
Open

Investigate smt2Cast and the as x T pattern #272

shingarov opened this issue May 3, 2024 · 0 comments

Comments

@shingarov
Copy link
Owner

The comment in ECst>>smt2: calls to investigate why it can happen that the receiver wraps around an EApp. However, after having invested some time into this investigation, I am realizing that the heart of smt2Cast has to do with the Z3 datatypes, which we don't have use right now, so we should come back to this subject then, and pay attention to the following comment in Serialize.hs:

-- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors
--   like Nil, see `tests/pos/adt_list_1.fq` 
  
smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder
smt2Cast env (EVar x) t = smt2Var env x t
smt2Cast env e        _ = smt2    env e
shingarov added a commit that referenced this issue May 3, 2024
shingarov added a commit that referenced this issue May 3, 2024
shingarov added a commit that referenced this issue May 3, 2024
shingarov added a commit that referenced this issue May 3, 2024
shingarov added a commit that referenced this issue May 3, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 5, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
shingarov added a commit that referenced this issue May 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant