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.

Sign up for GitHub

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

Jump to bottom

Struct constructor is difficult to use in generic printer #1294

Open

keks opened this issue Feb 6, 2025 · 0 comments

Labels

engine

Member

keks commented Feb 6, 2025

In SMT-LIB, we don't just use the type name for structs, but also the name of the constructor. The generic printer makes that pretty difficult:

hax/engine/backends/smtlib/smtlib_backend.ml

Lines 184 to 187 in 7ba7c7e

    
           match super.v with 
        
             | Type { variants = [{name = constructor_name;_}]; _ } -> 
        
               let constructor_name = Concrete_ident.DefaultViewAPI.render constructor_name in 
        
               let constructor_name = self#concrete_ident false constructor_name in

Would be nice if it were easier.

keks added the engine label

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment