pietrobraione

/* This gist shows how to build an almost zero-assembly template compiler from a threaded 
 * interpreter.
 * See http://eli.thegreenplace.net/2012/07/12/computed-goto-for-efficient-dispatch-tables
 * for the original threaded code interpreter. To illustrate compilation of jumps I added 
 * a couple of jump bytecodes. Works under macOS High Sierra (clang) and Ubuntu 18.04 (gcc), 
 * versions:
 *
 * $ clang --version
 * Apple LLVM version 10.0.0 (clang-1000.11.45.5)
 * Target: x86_64-apple-darwin17.7.0

pietrobraione

From Coq Require Import Strings.String.
From Coq Require Import Init.Nat.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Lists.List.
From Coq Require Import Program.Wf.
From Hammer Require Import Tactics.

(* A simplified version of a symbolic interpreter for an o-o language.
   Expressions are evaluated against heaps. Values can be either