func NewCallExpr(name string, args ...Expr) CallExpr {
	if len(args) == 0 {
		args = []Expr{Tt}
	}
	return CallExpr{MethodName: name, Args: args}
}
NewCallExpr is a convenience to construct a CallExpr statically, especially
for a fixed number of arguments.
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
}