Generic Printer: ~constructor argument to expr'_Construct_inductive is wrong for structs

[keks]

When processing these assignments

hax/examples/validation-example/src/lib.rs

Lines 120 to 121 in 7ba7c7e

	self.pl_value = msg.vm_value;
	self.pl_last_changed = msg.vm_timestamp;

this function in the generic printer implementation

hax/engine/backends/smtlib/smtlib_backend.ml

Lines 257 to 265 in 7ba7c7e

	method expr'_Construct_inductive ~super ~constructor ~is_record:_
	~is_struct ~fields ~base:_ =
	let constructor = if is_struct
	then constructor#p
	else constructor#p in
	let constructor = sexprlist [string "as" ; constructor; self#print_ty AstPos_expr__e super.typ] in
	if (List.is_empty fields)
	then constructor
	else sexprlist (constructor :: ps (List.map ~f:(fun (name, expr) -> expr ) fields))

(please ignore the pointless if-then-else 🙈 )

produces this code

(let
      (
        (self
          (
            (as validation_example/t_ProtocolLibrary validation_example/t_ProtocolLibrary)
            (get/validation_example/f_vm_value msg))))
      (let
        (
          (self
            (
              (as validation_example/t_ProtocolLibrary validation_example/t_ProtocolLibrary)
              (get/validation_example/f_vm_timestamp msg))))
        (let
          (
            (hax_temp_output
              (
                (as
                  core/result/Result_Ok
                  (core/result/t_Result Tuple0 validation_example/t_Error))
                (mk-tuple0))))
          (mk-tuple2 self hax_temp_output))))

Specifically, look at the type coercion that the ocaml code above builds:

(as validation_example/t_ProtocolLibrary validation_example/t_ProtocolLibrary)

This should be

(as <constructor_name> <type_name>

I think this is because the constructor and type name are not properly separated in some parts of the engine.