func (d FuncDecl) CoqDecl() string {
	var pp buffer
	pp.AddComment(d.Comment)
	pp.Add("Definition %s: val :=", d.Name)
	func() {
		pp.Indent(2)
		defer pp.Indent(-2)
		pp.Add("rec: \"%s\" %s :=", d.Name, d.Signature())
		pp.Indent(2)
		defer pp.Indent(-2)
		pp.AddLine(d.Body.Coq() + ".")
	}()
	if d.AddTypes {
		pp.Add("Theorem %s_t: ⊢ %s : (%s).", d.Name, d.Name, d.Type())
		pp.AddLine("Proof. typecheck. Qed.")
		pp.Add("Hint Resolve %s_t : types.", d.Name)
	}
	return pp.Build()
}
CoqDecl implements the Decl interface

For FuncDecl this emits the Coq vernacular Definition that defines the whole
function.
package coq
import (
	"fmt"
	"io"
	"path"
	"path/filepath"
	"sort"
	"strings"
)
func isWellBalanced(s string, lDelim string, rDelim string) bool {
	if strings.HasPrefix(s, lDelim) && strings.HasSuffix(s, rDelim) {
		return true
	}
	return false
}
type buffer struct {
	lines       []string
	indentLevel int
}
func (pp buffer) indentation() string {
	b := make([]byte, pp.indentLevel)
	for i := range b {
		b[i] = ' '
	}
	return string(b)
}
func (pp *buffer) appendLine(line string) {
	pp.lines = append(pp.lines, line)
}
func (pp *buffer) AddLine(line string) {
	if line == "" {
		pp.appendLine("")
	} else {
		pp.appendLine(pp.indentation() + indent(pp.indentLevel, line))
	}
}
func (pp *buffer) Add(format string, args ...interface{}) {
	pp.AddLine(fmt.Sprintf(format, args...))
}
func (pp *buffer) Indent(spaces int) {
	pp.indentLevel += spaces
}
func (pp *buffer) Block(prefix string, format string, args ...interface{}) int {
	pp.AddLine(prefix + indent(len(prefix), fmt.Sprintf(format, args...)))
	pp.Indent(len(prefix))
	return len(prefix)
}
func (pp buffer) Build() string {
	return strings.Join(pp.lines, "\n")
}
func addParens(s string) string {
	if !strings.Contains(s, " ") ||
		isWellBalanced(s, "(", ")") ||
		isWellBalanced(s, "{|", "|}") {
		return s
	}
	return fmt.Sprintf("(%s)", s)
}
func indent(spaces int, s string) string {
	lines := strings.Split(s, "\n")
	indentation := strings.Repeat(" ", spaces)
	for i, line := range lines {
		if i == 0 || line == "" {
			continue
		}
		lines[i] = indentation + line
	}
	return strings.Join(lines, "\n")
}
func (pp *buffer) AddComment(c string) {
	if c == "" {
		return
	}
	c = strings.ReplaceAll(c, "(*", "( *")
	c = strings.ReplaceAll(c, "*)", "* )")
	indent := pp.Block("(* ", "%s *)", c)
	pp.Indent(-indent)
}
func quote(s string) string {
	return `"` + s + `"`
}
func binder(s string) string {
	if s == "_" {
		return "<>"
	}
	return quote(s)
}
type FieldDecl struct {
	Name string
	Type Type
}
func (d FieldDecl) CoqBinder() string {
	return binder(d.Name)
}
func (d FieldDecl) Coq() string {
	return binder(d.Name)
}
type StructDecl struct {
	Name    string
	Fields  []FieldDecl
	Comment string
}
func (d StructDecl) CoqDecl() string {
	var pp buffer
	pp.AddComment(d.Comment)
	pp.Add("Definition %s := struct.decl [", d.Name)
	pp.Indent(2)
	for i, fd := range d.Fields {
		sep := ";"
		if i == len(d.Fields)-1 {
			sep = ""
		}
		pp.Add("%s :: %s%s", quote(fd.Name), fd.Type.Coq(), sep)
	}
	pp.Indent(-2)
	pp.AddLine("].")
	return pp.Build()
}
type InterfaceDecl struct {
	Name    string
	Methods []FieldDecl
	Comment string
}
func (d InterfaceDecl) CoqDecl() string {
	var pp buffer
	pp.AddComment(d.Comment)
	pp.Add("Definition %s := struct.decl [", d.Name)
	pp.Indent(2)
	for i, fd := range d.Methods {
		sep := ";"
		if i == len(d.Methods)-1 {
			sep = ""
		}
		pp.Add("%s :: %s%s", quote(fd.Name), fd.Type.Coq(), sep)
	}
	pp.Indent(-2)
	pp.AddLine("].")
	return pp.Build()
}
func (d InterfaceDecl) Coq() string {
	var pp buffer
	pp.AddComment(d.Comment)
	pp.Add("Definition %s := struct.decl [", d.Name)
	pp.Indent(2)
	for i, fd := range d.Methods {
		sep := ";"
		if i == len(d.Methods)-1 {
			sep = ""
		}
		pp.Add("%s :: %s%s", quote(fd.Name), fd.Type.Coq(), sep)
	}
	pp.Indent(-2)
	pp.AddLine("].")
	return pp.Build()
}
type StructToInterface struct {
	Struct    string
	Interface string
	Methods   []string
}
func (d StructToInterface) Coq() string {
	var pp buffer
	if len(d.Struct) > 0 && len(d.Interface) > 0 {
		pp.Add("Definition %s__to__%s: val :=", d.Struct, d.Interface)
		pp.Indent(2)
		pp.Add("rec: \"%s_to_%s\" \"t\" :=", d.Struct, d.Interface)
		pp.Indent(2)
		if len(d.Methods) == 1 {
			pp.Add("struct.mk %s [\"%s\" ::= %s__%s \"t\"].", d.Interface, d.Methods[0], d.Struct, d.Methods[0])
		} else {
			pp.Add("struct.mk %s [", d.Interface)
			pp.Indent(2)
			for i, method := range d.Methods {
				if i == len(d.Methods)-1 {
					pp.Add("\"%s\" ::= %s__%s \"t\"", method, d.Struct, method)
				} else {
					pp.Add("\"%s\" ::= %s__%s \"t\";", method, d.Struct, method)
				}
			}
			pp.Indent(-2)
			pp.Add("].")
		}
	}
	return pp.Build()
}
func (d StructToInterface) MethodList() []string {
	return d.Methods
}
func (d StructToInterface) Name() string {
	var pp buffer
	pp.Add("%s__to__%s", d.Struct, d.Interface)
	return pp.Build()
}
func (d StructToInterface) CoqDecl() string {
	var pp buffer
	if len(d.Struct) > 0 && len(d.Interface) > 0 {
		pp.Add("Definition %s__to__%s: val :=", d.Struct, d.Interface)
		pp.Indent(2)
		pp.Add("rec: \"%s_to_%s\" \"t\" :=", d.Struct, d.Interface)
		pp.Indent(2)
		if len(d.Methods) == 1 {
			pp.Add("struct.mk %s [\"%s\" ::= %s__%s \"t\"].", d.Interface, d.Methods[0], d.Struct, d.Methods[0])
		} else {
			pp.Add("struct.mk %s [", d.Interface)
			pp.Indent(2)
			for i, method := range d.Methods {
				if i == len(d.Methods)-1 {
					pp.Add("\"%s\" ::= %s__%s \"t\"", method, d.Struct, method)
				} else {
					pp.Add("\"%s\" ::= %s__%s \"t\";", method, d.Struct, method)
				}
			}
			pp.Indent(-2)
			pp.Add("].")
		}
	}
	return pp.Build()
}
type StructToInterfaceDecl struct {
	Fun       string
	Struct    string
	Interface string
	Arg       string
}
func (d StructToInterfaceDecl) Coq() string {
	var pp buffer
	pp.Add("%s (%s__to__%s %s)", d.Fun[1:len(d.Fun)-1], d.Struct, d.Interface, d.Arg)
	return pp.Build()
}
type TypeDecl struct {
	Name string
	Body Type
}
func (d TypeDecl) CoqDecl() string {
	var pp buffer
	pp.Add("Definition %s: ty := %s.", d.Name, d.Body.Coq())
	return pp.Build()
}
type Type interface {
	Coq() string
}
type TypeIdent string
func (t TypeIdent) Coq() string {
	return string(t)
}
type StructName string
func (t StructName) Coq() string {
	return NewCallExpr("struct.t", StructDesc(string(t))).Coq()
}
type MapType struct {
	Value Type
}
func (t MapType) Coq() string {
	return NewCallExpr("mapT", t.Value).Coq()
}
type FuncType struct {
	Params  []string
	Results []string
}
func (t FuncType) Coq() string {
	var args []string
	for _, a := range t.Params {
		args = append(args, a)
	}
	if len(t.Params) == 0 {
		args = []string{"unitT"}
	}
	for _, a := range t.Results {
		args = append(args, a)
	}
	if len(args) == 0 {
		args = []string{"<>"}
	}
	return fmt.Sprintf("arrowT %s", strings.Join(args, " "))
}
type SliceType struct {
	Value Type
}
func (t SliceType) Coq() string {
	return fmt.Sprintf("slice.T %s", addParens(t.Value.Coq()))
}
type ArrayType struct {
	Len uint64
	Elt Type
}
func (t ArrayType) Coq() string {
	return fmt.Sprintf("arrayT %s", t.Elt.Coq())
}
type ArrowType struct {
	ArgTypes   []Type  
	ReturnType Type
}
func (t ArrowType) Coq() string {
	types := []string{}
	for _, a := range t.ArgTypes {
		types = append(types, a.Coq())
	}
	types = append(types, t.ReturnType.Coq())
	return "(" + strings.Join(types, " -> ") + ")%ht"
}
type Expr interface {
	Coq() string
}
type GallinaIdent string
func (e GallinaIdent) Coq() string {
	return string(e)
}
type PackageIdent struct {
	Package string
	Ident   string
}
func (e PackageIdent) Coq() string {
	return fmt.Sprintf("%s.%s", e.Package, e.Ident)
}
var Skip Expr = GallinaIdent("Skip")
type LoggingStmt struct {
	GoCall string
}
func (s LoggingStmt) Coq() string {
	var pp buffer
	pp.AddComment(s.GoCall)
	return pp.Build()
}
type IdentExpr string
func (e IdentExpr) Coq() string {
	return quote(string(e))
}
type GallinaString string
func (s GallinaString) Coq() string {
	return quote(string(s))
}
type CallExpr struct {
	MethodName string
	Args       []Expr
}
func NewCallExpr(name string, args ...Expr) CallExpr {
	if len(args) == 0 {
		args = []Expr{Tt}
	}
	return CallExpr{MethodName: name, Args: args}
}
func (s CallExpr) Coq() string {
	comps := []string{s.MethodName}
	for _, a := range s.Args {
		comps = append(comps, addParens(a.Coq()))
	}
	return strings.Join(comps, " ")
}
type StructFieldAccessExpr struct {
	Struct string
	Field  string
	X      Expr
	ThroughPointer bool
}
func StructDesc(name string) Expr {
	return GallinaIdent(name)
}
func (e StructFieldAccessExpr) Coq() string {
	if e.ThroughPointer {
		return NewCallExpr("struct.loadF",
			StructDesc(e.Struct), GallinaString(e.Field), e.X).Coq()
	}
	return NewCallExpr("struct.get", StructDesc(e.Struct),
		GallinaString(e.Field), e.X).Coq()
}
type ReturnExpr struct {
	Value Expr
}
func (e ReturnExpr) Coq() string {
	return e.Value.Coq()
}
type Binding struct {
	Names []string
	Expr  Expr
}
func NewAnon(e Expr) Binding {
	return Binding{Expr: e}
}
func (b Binding) isAnonymous() bool {
	return len(b.Names) == 0
}
type fieldVal struct {
	Field string
	Value Expr
}
type StructLiteral struct {
	StructName string
	elts       []fieldVal
	Allocation bool  
}
func NewStructLiteral(structName string) StructLiteral {
	return StructLiteral{StructName: structName}
}
func (sl *StructLiteral) AddField(field string, value Expr) {
	sl.elts = append(sl.elts, fieldVal{field, value})
}
func (sl StructLiteral) Coq() string {
	var pp buffer
	method := "struct.mk"
	if sl.Allocation {
		method = "struct.new"
	}
	pp.Add("%s %s [", method, StructDesc(sl.StructName).Coq())
	pp.Indent(2)
	for i, f := range sl.elts {
		terminator := ";"
		if i == len(sl.elts)-1 {
			terminator = ""
		}
		pp.Add("%s ::= %s%s", quote(f.Field), f.Value.Coq(), terminator)
	}
	pp.Indent(-2)
	pp.Add("]")
	return pp.Build()
}
type BoolLiteral bool
var (
	False BoolLiteral = false
	True  BoolLiteral = true
)
func (b BoolLiteral) Coq() string {
	if b {
		return "#true"
	} else {
		return "#false"
	}
}
type UnitLiteral struct{}
var Tt UnitLiteral = struct{}{}
func (tt UnitLiteral) Coq() string {
	return "#()"
}
type IntLiteral struct {
	Value uint64
}
func (l IntLiteral) Coq() string {
	return fmt.Sprintf("#%d", l.Value)
}
type Int32Literal struct {
	Value uint32
}
func (l Int32Literal) Coq() string {
	return fmt.Sprintf("#(U32 %d)", l.Value)
}
type ByteLiteral struct {
	Value uint8
}
func (l ByteLiteral) Coq() string {
	return fmt.Sprintf("#(U8 %v)", l.Value)
}
type StringLiteral struct {
	Value string
}
func (l StringLiteral) Coq() string {
	return fmt.Sprintf(`#(str"%s")`, l.Value)
}
type nullLiteral struct{}
func (l nullLiteral) Coq() string {
	return "#null"
}
var Null = nullLiteral{}
type BinOp int
const (
	OpPlus BinOp = iota
	OpMinus
	OpEquals
	OpNotEquals
	OpLessThan
	OpGreaterThan
	OpLessEq
	OpGreaterEq
	OpAppend
	OpMul
	OpQuot
	OpRem
	OpAnd
	OpOr
	OpXor
	OpLAnd
	OpLOr
	OpShl
	OpShr
)
type BinaryExpr struct {
	X  Expr
	Op BinOp
	Y  Expr
}
func (be BinaryExpr) Coq() string {
	coqBinOp := map[BinOp]string{
		OpPlus:        "+",
		OpMinus:       "-",
		OpEquals:      "=",
		OpNotEquals:   "≠",
		OpAppend:      "+",
		OpMul:         "*",
		OpQuot:        "`quot`",
		OpRem:         "`rem`",
		OpLessThan:    "<",
		OpGreaterThan: ">",
		OpLessEq:      "≤",
		OpGreaterEq:   "≥",
		OpAnd:         "`and`",
		OpOr:          "`or`",
		OpXor:         "`xor`",
		OpLAnd:        "&&",
		OpLOr:         "||",
		OpShl:         "≪",
		OpShr:         "≫",
	}
	if binop, ok := coqBinOp[be.Op]; ok {
		badPrecedence := map[BinOp]bool{
			OpQuot: true,
			OpRem:  true,
			OpLOr:  true,
			OpLAnd: true,
			OpShl:  true,
			OpShr:  true,
		}
		if badPrecedence[be.Op] {
			return fmt.Sprintf("%s %s %s",
				addParens(be.X.Coq()), binop, addParens(be.Y.Coq()))
		}
		s := fmt.Sprintf("%s %s %s", be.X.Coq(), binop, be.Y.Coq())
		if be.Op == OpEquals || be.Op == OpAnd {
			s = addParens(s)
		}
		return s
	}
	panic(fmt.Sprintf("unknown binop %d", be.Op))
}
type NotExpr struct {
	X Expr
}
func (e NotExpr) Coq() string {
	return fmt.Sprintf("~ %s", addParens(e.X.Coq()))
}
type TupleExpr []Expr
func (te TupleExpr) Coq() string {
	var comps []string
	for _, t := range te {
		comps = append(comps, t.Coq())
	}
	return fmt.Sprintf("(%s)",
		indent(1, strings.Join(comps, ", ")))
}
func NewTuple(es []Expr) Expr {
	if len(es) == 1 {
		return es[0]
	}
	return TupleExpr(es)
}
type BlockExpr struct {
	Bindings []Binding
}
func (b Binding) AddTo(pp *buffer) {
	if e, ok := b.Expr.(LoggingStmt); ok {
		pp.Add("%s", e.Coq())
		return
	}
	if b.isAnonymous() {
		pp.Add("%s;;", b.Expr.Coq())
	} else if len(b.Names) == 1 {
		pp.Add("let: %s := %s in", binder(b.Names[0]), b.Expr.Coq())
	} else if len(b.Names) == 2 {
		pp.Add("let: (%s, %s) := %s in",
			binder(b.Names[0]),
			binder(b.Names[1]),
			b.Expr.Coq())
	} else if len(b.Names) == 3 {
		pp.Add("let: ((%s, %s), %s) := %s in",
			binder(b.Names[0]),
			binder(b.Names[1]),
			binder(b.Names[2]),
			b.Expr.Coq())
	} else if len(b.Names) == 4 {
		pp.Add("let: (((%s, %s), %s), %s) := %s in",
			binder(b.Names[0]),
			binder(b.Names[1]),
			binder(b.Names[2]),
			binder(b.Names[3]),
			b.Expr.Coq())
	} else {
		panic("no support for destructuring more than 4 return values")
	}
}
func (be BlockExpr) Coq() string {
	var pp buffer
	for n, b := range be.Bindings {
		if n == len(be.Bindings)-1 {
			if _, ok := b.Expr.(LoggingStmt); ok {
				pp.AddLine(b.Expr.Coq())
				pp.AddLine(UnitLiteral{}.Coq())
			} else {
				pp.AddLine(b.Expr.Coq())
			}
			continue
		}
		b.AddTo(&pp)
	}
	return pp.Build()
}
type DerefExpr struct {
	X  Expr
	Ty Expr
}
func (e DerefExpr) Coq() string {
	return fmt.Sprintf("![%s] %s", e.Ty.Coq(), addParens(e.X.Coq()))
}
type RefExpr struct {
	X  Expr
	Ty Expr
}
func (e RefExpr) Coq() string {
	return NewCallExpr("ref_to", e.Ty, e.X).Coq()
}
type StoreStmt struct {
	Dst Expr
	Ty  Expr
	X   Expr
}
func (e StoreStmt) Coq() string {
	return fmt.Sprintf("%s <-[%s] %s", e.Dst.Coq(), e.Ty.Coq(), e.X.Coq())
}
type IfExpr struct {
	Cond Expr
	Then Expr
	Else Expr
}
func flowBranch(pp *buffer, prefix string, e Expr, suffix string) {
	code := e.Coq() + suffix
	if !strings.ContainsRune(code, '\n') {
		indent := pp.Block(prefix+" ", "%s", code)
		pp.Indent(-indent)
		return
	}
	pp.AddLine(prefix)
	pp.Indent(2)
	pp.AddLine(code)
	pp.Indent(-2)
}
func (ife IfExpr) Coq() string {
	var pp buffer
	pp.Add("(if: %s", ife.Cond.Coq())
	flowBranch(&pp, "then", ife.Then, "")
	flowBranch(&pp, "else", ife.Else, ")")
	return pp.Build()
}
func (b Binding) Unwrap() (e Expr, ok bool) {
	if b.isAnonymous() {
		return b.Expr, true
	}
	return nil, false
}
type HashTableInsert struct {
	Value Expr
}
func (e HashTableInsert) Coq() string {
	return fmt.Sprintf("(fun _ => Some %s)", addParens(e.Value.Coq()))
}
var LoopContinue = GallinaIdent("Continue")
var LoopBreak = GallinaIdent("Break")
type ForLoopExpr struct {
	Init Binding
	Cond Expr
	Post Expr
	Body BlockExpr
}
func (e ForLoopExpr) Coq() string {
	var pp buffer
	e.Init.AddTo(&pp)
	pp.Add("(for: (λ: <>, %s); (λ: <>, %s) := λ: <>,", e.Cond.Coq(), e.Post.Coq())
	pp.Indent(2)
	pp.Add("%s)", e.Body.Coq())
	return pp.Build()
}
type Binder *IdentExpr
func binderToCoq(b Binder) string {
	if b == nil {
		return "<>"
	}
	return binder(string(*b))
}
type SliceLoopExpr struct {
	Key   Binder
	Val   Binder
	Ty    Expr
	Slice Expr
	Body  BlockExpr
}
func (e SliceLoopExpr) Coq() string {
	var pp buffer
	pp.Add("ForSlice %v %s %s %s",
		addParens(e.Ty.Coq()),
		binderToCoq(e.Key), binderToCoq(e.Val),
		addParens(e.Slice.Coq()))
	pp.Indent(2)
	pp.Add("%s", addParens(e.Body.Coq()))
	return pp.Build()
}
type MapIterExpr struct {
	KeyIdent, ValueIdent string
	Map Expr
	Body BlockExpr
}
func (e MapIterExpr) Coq() string {
	var pp buffer
	pp.Add("MapIter %s (λ: %s %s,",
		addParens(e.Map.Coq()),
		binder(e.KeyIdent), binder(e.ValueIdent))
	pp.Indent(2)
	pp.Add("%s)", e.Body.Coq())
	return pp.Build()
}
type SpawnExpr struct {
	Body BlockExpr
}
func (e SpawnExpr) Coq() string {
	var pp buffer
	pp.Block("Fork (", "%s)", e.Body.Coq())
	return pp.Build()
}
type FuncLit struct {
	Args []FieldDecl
	Body Expr
}
func (e FuncLit) Coq() string {
	var pp buffer
	var args []string
	for _, a := range e.Args {
		args = append(args, a.CoqBinder())
	}
	if len(args) == 0 {
		args = []string{"<>"}
	}
	sig := strings.Join(args, " ")
	pp.Add("(λ: %s,", sig)
	pp.Indent(2)
	defer pp.Indent(-2)
	pp.AddLine(e.Body.Coq())
	pp.Add(")")
	return pp.Build()
}
type FuncDecl struct {
	Name       string
	Args       []FieldDecl
	ReturnType Type
	Body       Expr
	Comment    string
	AddTypes   bool
}
func (d FuncDecl) Signature() string {
	var args []string
	for _, a := range d.Args {
		args = append(args, a.CoqBinder())
	}
	if len(args) == 0 {
		args = []string{"<>"}
	}
	return strings.Join(args, " ")
}
func (d FuncDecl) Type() string {
	types := []string{}
	for _, a := range d.Args {
		types = append(types, a.Type.Coq())
	}
	if len(d.Args) == 0 {
		types = append(types, TypeIdent("unitT").Coq())
	}
	types = append(types, d.ReturnType.Coq())
	return strings.Join(types, " -> ")
}