Hook up poulet4 interpreter to bin/main.ml

[hackedy]

Blocked on #346, since the extracted interpreter has to use the same datatypes as the typechecker. Right now the ppx_imported types in the typechecker are technically different, so things won't play nicely.

[hackedy]

Rough roadmap here

• [ ] fix error reporting in checker.ml
• [x] call interp from main.ml
• [x] do something about the fuel parameter

[hackedy]

Having trouble extracting the v1model target right now due to a mismatch between coq polymorphism and extracted ocaml polymorphism. Turning it into an axiom makes it possible to extract something, but it's an axiom and not runnable code. Going to axiomatize it for now so that I can get things sorted out on the ocaml side and I'll deal with the extraction problem later.

Error message:

File "extraction/V1ModelTarget.ml", line 1:
Error: The implementation extraction/V1ModelTarget.ml
       does not match the interface extraction/.poulet4.objs/byte/poulet4__V1ModelTarget.cmi:
        Values do not match:
          val coq_V1ModelExternSem :
            ('_weak1, '_weak2) Poulet4.Target.coq_ExternSem
        is not included in
          val coq_V1ModelExternSem : ('a1, 'a2) Poulet4.Target.coq_ExternSem
        The type ('_weak1, '_weak2) Poulet4.Target.coq_ExternSem
        is not compatible with the type ('a, 'b) Poulet4.Target.coq_ExternSem
        Type '_weak1 is not compatible with type 'a
        File "extraction/V1ModelTarget.mli", line 199, characters 0-51:
          Expected declaration
        File "extraction/V1ModelTarget.ml", line 632, characters 4-24:
          Actual declaration

Appears to be an instance of coq/coq#6614.

[hackedy]

Current STF failure messages (sorted and deduplicated.. literally every test is failing right now)

          [failure] Expected SReturn (ValBaseNull) but got something different (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] Tried to find the global variable <global: <empty path>> in a Semantics.state. Global variables are stored in the genv.
          [failure] Tried to find the global variable <global: > in a Semantics.state. Global variables are stored in the genv.
          [failure] Tried to find the global variable <global: f1.x> in a Semantics.state. Global variables are stored in the genv.
          [failure] Tried to find the global variable <global: g.hdr> in a Semantics.state. Global variables are stored in the genv.
          [failure] Tried to find the global variable <global: swapped.x> in a Semantics.state. Global variables are stored in the genv.
          [failure] architecture unsupported
          [failure] couldn't find loc in const env (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_expr: failure in eval_cast (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_func (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_func: error in interp_extern (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_stmt: lookup_func could not find main.p.<global: <empty path>>.advance (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_stmt: lookup_func could not find main.p.<global: <empty path>>.extract (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] interp_stmt: lookup_func could not find main.p.<global: <empty path>>.lookahead (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] set_member called on value that is not struct-like (You may want to break this error out into its own variant in Semantics.Exn.t instead of using Exn.Other)
          [failure] unimplemented stf statement: Add

[hackedy]

Rough roadmap here

• [ ] fix error reporting in checker.ml
• [x] call interp from main.ml
• [x] do something about the fuel parameter

Going to give up on improving error reporting in checker.ml since we are about to refactor it anyway and just try to merge this.