Edit Files¶

The edit files contain declarations that control the output of hs-to-coq on various Haskell files.

General format of edit files¶

Edit files are plain text files. Empty lines and lines starting with # are ignored. Otherwise, the files are consist of a sequence of edits. Most form of edits are exactly one line long, but some edits can span multiple lines, and must be terminated with a period.

Make sure that your edit file ends with a newline.

Qualified names¶

A qualified_name is the Coq name with module prefix. Names must always be qualified, because edit files are not bound to a specific module (even though you may want to have a separate edit for each Haskell module).

Reserved names have an underscore appended and renames (see below) have already been applied.

More details about how hs-to-coq treats see Section Identifiers and Notation.

Gallina expressions¶

Some edits contain Gallina expressions (i.e. Coq code). The parser is pretty limited. In particular, it does not know anything about operator precedence or associativity, so add plenty of parentheses!

Skipping Haskell¶

Sometimes, hs-to-coq should ignore various Haskell declarations, because they are not translatable, or they are out-of-scope, or for other reasons.

`skip` – skip a function, type, or type class instance¶

Format:

skip qualified_name

Effect:

During translation, ignore the declaration of the function, value, type, or type class instance with the given qualified_name. The name must be the translated Coq name, not the original Haskell name (if those differ).

This does not affect the translation of uses of the given name. This means that you can use other methods, e.g. a preamble, to make it available.

You can skip type class instances, but as they do not have names in Haskell, you must use the name hs-to-coq generates for them. The name generation is systematic, but you might want to first attempt the translation and check the output for the precise name.

To skip data type constructors, see skip constructor; to skip type classes, see skip class; to skip type class methods, see skip methods. They are not unified here because those effects are more powerful. You can also skip whole modules with skip module.

Examples:

skip Data.Function.fix_ # Note the mangled name!
skip GHC.Base.String
skip GHC.Real.Fractional
skip Data.Monoid.Show__Last # an instance

`skip constructor` – skip a constructor of a data type¶

Format:

skip constructor qualified_name

Effect:

During translation, ignore the given data type constructor. Any equation of a function, alternative of a case statement, or pattern guard that pattern-matches on that constructor is also skipped. List comprehensions that bind to that constructor become [].

As with skip, this does not affect the translation of uses of the constructor. This means that you must either make it available in a preamble or elide it with other edits. Additionally, matching against the constructor in do notation will cause a translation failure.

These skipped constructors are not stored in the generated metadata, so you need to include the skip constructor edits in all downstream modules.

Examples:

skip constructor Core.Cast
skip constructor Core.Tick
skip constructor Core.Type_
skip constructor Core.Coercion

`skip class` – skip a type class and all its instances¶

Format:: skip class qualified_class

Effect:

Omit the given type class and all its instances.

These skipped classes are not stored in the generated metadata, so you need to include the skip class edits in all downstream modules.

Examples:

skip class GHC.Base.Alternative
skip class Data.Data.Data

`skip method` – skip a method¶

Format:

skip method qualified_class method

Effect:

Omit the given method from the its class declaration, and also from all instances.

Examples:

skip method GHC.Base.Monad fail

`skip equation` – skip one equation of a function definition¶

Format:

skip equation qualified_function pattern …

Effect:

Skip the equation of the function definition whose arguments are the specified patterns. Guards are not considered, only the patterns themselves.

For example, consider the following (silly) function definition:

redundant :: Maybe Bool -> Maybe Bool -> Bool
redundant (Just True)  _        = False
redundant (Just False) _        = True
redundant _            _        = True
redundant _            (Just b) = b

The last case is redundant, so Coq will reject this definition. However, we can add the following edit:

skip equation ModuleName.redundant _ (Some b)

And the last case will be deleted on the Coq side:

Definition redundant : option bool -> option bool -> bool :=
  fun arg_0__ arg_1__ =>
    match arg_0__, arg_1__ with
    | Some true, _ => false
    | Some false, _ => true
    | _, _ => true
    end.

Note that you have to use the translated name (Some vs. Just), and most constructor names will be fully qualified.

Why would you want this? This edit is most useful in tandem with skip constructor (which see). Suppose we have a function where the final catch-all case can only match skipped constructors, such as

data T = TranslateMe
       | SkipMe

function :: T -> Bool
function TranslateMe = True
function _           = False

Then, on skipping SkipMe, this function’s _ case will be redundant, and Coq would reject it. We can fix this with

skip equation ModuleName.function _

to translate just the TranslateMe case.

See also skip case pattern for the equivalent edit for case and lambda-case expressions.

Examples:

skip equation ModuleName.redundant _ (Some b)
skip equation Core.hasSomeUnfolding _

`skip case pattern` – skip one alternative of a `case` expression¶

Format:

skip case pattern pattern

Effect:

Skip any alternative of a case expression (or a lambda-case expression) which matches against the given pattern. Guards are not considered, only the pattern itself.

For example, consider the following (silly) function definition:

redundant :: Bool -> Bool
redundant b = not (case b of
                     True  -> False
                     False -> True
                     _     -> True)

The last case is redundant, so Coq will reject this definition. However, we can add the following edit:

in ModuleName.redundant skip case pattern _

And the last case will be deleted on the Coq side (reformatted):

Definition redundant : bool -> bool :=
  fun b => negb (match b with
                 | true => false
                 | false => true
                 end).

You can use an arbitrary pattern, not simply _; constructor names must be fully qualified and the names used must be those that appear after renaming.

Why would you want this? This edit is most useful in tandem with skip constructor (which see); see the discussion in skip equation for a worked example (with a named function).

This edit is unusual in that you very likely want to use it with the in meta-edit to scope its effects to within a specific definition. However, this isn’t mandatory; if, for some reason, you want to skip every _ in every case, then skip case pattern _ will do what you want.

See also skip equation for the equivalent edit for named functions.

Examples:

in ModuleName.redundant skip case pattern _

`skip module` – skip a module import¶

Format:

skip module module

Effect:

Do not generate an Require statemnt for module.

This is mostly useful during development: hs-to-coq automatically requires the modules of all names it encounters, in the beginning of the resulting file. If there are names from modules that you do not intent to translate, Coq will already abort there. It is more convenient to have it fail when the name is actually encountered, to then decide how to fix it (e.g. using skip, rename or rewrite).

In the end, all mentions of names in the give module ought to be gone, in which case hs-to-coq would not generate an Require statement anyways. So in complete formalizations, this edit should not be needed.

Examples:

skip module GHC.Show

`axiomatize module` – replace all definitions in a module with axioms¶

Format:

axiomatize module module

Effect:

Replaces all definitions in a module with axioms.

This translates type and type class definitions, and then produces axioms for variable bindings and type class instances which have the translated types. Any types that are redefined are correctly redefined; any bindings or instances that are skipped don’t have axioms generated. If you want to override the axiomatization for a single definition and actually translate it, you can use the unaxiomatize definition edit.

The axiomatize module edit is useful if you want to stub out a dependency of a module you are actually interested in.

`axiomatize original module name` – replace all definitions in a module with axioms, using the pre-renaming module name¶

Format:

axiomatize original module name module

Effect:

You probably do not need to use this edit; it’s only important when using rename module to merge multiple modules into one. If you are doing this, however, and wish you could use axiomatize module on some of the input modules but not others, then axiomatize original module name is the edit for you.

The behavior of axiomatize original module name is the same as that of axiomatize module, except for how it picks which module to axiomatize. While every other edit operates in terms of the Coq name after any renamings from the edits have been applied, axiomatize original module name checks the original, pre-rename module, form of the module name. Most of the time, this would be confusing, and axiomatize module would be preferable.

However, if you have used rename module to merge two (or more) modules into one, but you only want one of them (or some other strict subset) to be axiomatized, then axiomatize original module name is the only way to get this behavior.

Examples:

axiomatize original module name Part1
rename module Part1 Whole
rename module Part2 Whole

`axiomatize definition` – replace a value definition with an axiom¶

Format:

axiomatize definition qualified_name

Effect:

Replaces a single definition with an axiom.

This takes the name of a value-level definition and, when translating it, translates only the type and generates an axiom with that type.

See also axiomatize module, and also redefine Axiom for type-level axiomatization.

Examples:

axiomatize definition GHC.Prim.primitiveFunction

`unaxiomatize definition` – override whole-module axiomatization on a case-by-case basis¶

Format:

unaxiomatize definition qualified_name

Effect:

Translates a single definition, axiomatize module notwithstanding.

If the module containing the given value-level definition is being axiomatized, then this definition will be translated in the usual way.

If a definition is both unaxiomatized and skipped, then it will simply be skipped. But please don’t do this :-)

Examples:

axiomatize module TrieMap
unaxiomatize definition TrieMap.insertTM
unaxiomatize definition TrieMap.deleteTM

Adding Coq Commands¶

`add` – inject a definition¶

Format:

add module coq_definition

Effect:

Add a Coq definition to module. The definition can be a Definition, a Fixpoint, an Inductive, an Instance, an Axiom, or a Theorem (with a Proof).

The name in the definition should be fully qualified. (If it is not, some dependency calculations inside hs-to-coq might go wrong – but this is not always critical.)

Our Coq parser is dramatically incomplete, and you may need to add parentheses or pick a simpler syntactic representation of terms to get them to parse correctly or at all. One example is that hs-to-coq does not understand the associativity of the function arrow when parsing: a -> b -> c will not parse, and needs to be given as a -> (b -> c).

When providing a Theorem – or a Lemma, a Remark, a Fact, a Corollary, a Proposition, or an Example – it must be immediately followed by Proof., some unparsed text (newlines are permitted), and then the word Qed, Defined, or Admitted.

This is a multi-line edit and needs to be terminated by a period (as is natural when writing a coq_definition).

Examples:

add Data.Foldable Definition Data.Foldable.elem {f} `{(Foldable f)} {a} `{(GHC.Base.Eq_ a)} :
  a -> (f a -> bool) :=
  fun x xs => Data.Foldable.any (fun y => x GHC.Base.== y) xs.

add Data.Monoid Instance Unpeel_Last a : GHC.Prim.Unpeel (Last a) (option a) :=
  GHC.Prim.Build_Unpeel _ _ getLast Mk_Last.

`add type` – inject a definition into the type component¶

Format:: add type module coq_definition
Effect:: Add a Coq definition to the type component of a module. The definition can be as above, and need not be a type definition. However, it is inserted before the midamble section and will appear grouped with the type and class definitions.

`import` – inject an `Import` statement¶

Format:

import module module

Effect:

Inject a Import statement into the Coq code, which makes the definitions from the given module available unqualified.

When used to import the hs-to-coq base library, this makes the output look more like standard Haskell.

Note, however, that Coq’s module system lacks the import ... hiding construct so all definitions from the module must be made available.

Examples:

import module Prelude

Renaming and Rewriting¶

`rename type` – rename a type¶

Format:

rename type qualified_name = qualified_name

Effect:

Change the name of a Haskell type, at both definition and use sites.

Examples:

rename type GHC.Types.[] = list
rename type GHC.Natural.Natural = Coq.Numbers.BinNums.N

`rename value` – rename a value¶

Format:: rename value qualified_name = qualified_name
Effect:: Change the name of a Haskell value (function, data constructor), at both definition and use sites.
Note:: When renaming a name in its definition, you should not change the module.

Examples:

rename value Data.Foldable.length = Coq.Lists.List.length     # use Coq primitive
rename value GHC.Base.++          = Coq.Init.Datatypes.app    # operators ok
rename value Data.Monoid.First    = Data.Monoid.Mk_First      # resolve punning

`rename module` – change a module name¶

Format:: rename module module module
Effect:: Change the name of a Haskell module, affecting the filename of the generated Coq module.
Note:: If two modules are renamed to the same name, they will be combined into a single joint module, as long as they are processed during the same execution of hs-to-coq. This feature is useful to translate mutually recursive modules.

Examples:

rename module Type MyType
rename module Data.Semigroup.Internal Data.SemigroupInternal

`alias module` – abbreviate a module name¶

Format:: alias module module module
Effect:: Abbreviate a module name with an alias. All occurrences of the alias in the current edits file are expanded to the original name. Aliases do not affect the generated Coq code.

Examples:

alias module Seq Data.Sequence.Internal
order Seq.Functor__Seq Seq.Applicative__Seq

# Equivalent to
order Data.Sequence.Internal.Functor__Seq Data.Sequence.Internal.Applicative__Seq

`rewrite` – replace Haskell subexpressions¶

Format:

rewrite forall vars, expression = expression

Effect:

Pattern-matches a sub-expression and replaces it with the right-hand side after substituting all variables.

The pattern-matching is unhygienic: if you mention a variable x in the pattern but not in the list of variables (vars), then the rewrite rule will only match if there is actually is a variable named x.

Examples:

## work around laziness
rewrite forall xs x, (GHC.List.zip xs (GHC.List.repeat x)) = (GHC.Base.map (fun y => pair y x) xs)
rewrite forall x, GHC.Magic.lazy x = x

## replace with Coq library function
rewrite forall x y, GHC.List.replicate x y = Coq.Lists.List.repeat y x

## skip debugging code
rewrite forall x, andb Util.debugIsOn x = false

## create dummy strings to ignore particular definitions
## note empty variable list
rewrite forall , Outputable.empty = (GHC.Base.hs_string__ "Outputable.empty")

`redefine` – override a Coq definition¶

Format:

redefine Coq_definition

Effect:

Combines the skip and add edits.

You can use redefine Axiom ... to replace a type-level definition with an axiom; for value-level definitions, please use axiomatize definition instead.

Examples:

redefine Definition GHC.Base.map {A B :Type} (f : A -> B) xs := Coq.Lists.List.map f xs.

`collapse let` – if a definition is just a `let`-expression, inline it¶

Format:

collapse let qualified_name

Effect:

If a converted definition is of the form

Definition outer := let inner := definition in inner.

then convert it to simply

Definition outer := definition.

Both outer and inner can have arguments; inner can have a type annotation, but it’s ignored.

Additionally, if definition is a non-mutual fixpoint fix f args := body, the recursive calls to f in body are rewritten to direct calls to outer.

This is particularly important for mutual recursion: if inner is mutually recursive with another top-level function, then if outer has no arguments, it would otherwise appear not to be a function and would thus cause conversion to fail, as Coq doesn’t support recursion through non-functions.

Examples:

collapse let CoreFVs.freeVars

Extra information¶

`data kinds` – Declare kinds of type arguments to Inductive datatypes¶

Format:: data kinds qualified_name Coq_types

Effect:

Haskell programmers rarely include kind signatures on inductive datatypes. This usually isn’t a problem, but for higher-order parameters, some phantom type parameters, or poly-kinded type parameters, Coq does not necessarily automatically infer the right types. In these cases, the information can be included in an edit.

Examples:

# The edit file's Coq parser needs parentheses
data kinds Control.Applicative.WrappedArrow (Type -> (Type -> Type))

# Multiple kinds are separated with commas
data kinds Data.Functor.Reverse.Reverse   (Type -> Type), Type
data kinds Data.Functor.Constant.Constant Type,           Type

`polykinds` – Declare polymorphic kind variables to Inductive datatypes¶

Format:: polykinds qualified_name name

Effect:

For Haskell programs written with the PolyKind extension, the user can provide the polymorphic kind variables to help hs-to-coq to include those kind variables.

Examples:

polykinds Data.Monoid.Ap k

data kinds Data.Monoid.Ap (k -> Type), k

`class kinds` – Declare kinds of type arguments to type classes¶

Format:: class kinds qualified_name Coq_types

Effect:

Like data kinds, but for classes.

Examples:

class kinds Control.Arrow.Arrow (Type -> (Type -> Type))

`delete unused type variables` – Remove unused type variables from a declaration¶

Format:: delete unused type variables qualified_name

Effect:

Don’t translate binders for any type variables that aren’t visibly used in the specified definition.

An explanation: sometimes, poly-kinded Haskell data types have extra invisible type parameters. For instance, in Data.Functor.Const, we have the type
newtype Const a b = Const { getConst :: a }
which is secretly
newtype Const {k} (a :: Type) (b :: k) = Const { getConst :: a }
Often, such as here, this doesn’t show up in the translated Coq code; we get
Inductive Const a b : Type := Mk_Const (getConst : a) : Const a b.
(And, as in Haskell 2010, b is inferred to have kind Type.) Sometimes it does, in which case we can fix it using data kinds. But either way, we still introduce spurious kind variables in the translation sometimes. For example, the derived Eq instance for Const is translated to
Program Instance Eq___Const {a} {k} {b} `{GHC.Base.Eq_ a}
   : GHC.Base.Eq_ (Const a b : GHC.Prim.TYPE GHC.Types.LiftedRep) :=
  fun _ k =>
    k {| GHC.Base.op_zeze____ := Eq___Const_op_zeze__ ;
         GHC.Base.op_zsze____ := Eq___Const_op_zsze__ |}.
The implicit argument {k} isn’t useful in the Coq code, and causes a type-checking failure when its type cannot be determined. We can avoid this with
delete unused type variables Data.Functor.Const.Eq___Const
which will drop the {k} and leave the definition with just the {a} and {b} it needs:
Program Instance Eq___Const {a} {b} `{GHC.Base.Eq_ a}
   : GHC.Base.Eq_ (Const a b : GHC.Prim.TYPE GHC.Types.LiftedRep) :=
  fun _ k =>
    k {| GHC.Base.op_zeze____ := Eq___Const_op_zeze__ ;
         GHC.Base.op_zsze____ := Eq___Const_op_zsze__ |}.

Examples:

delete unused type variables Data.Functor.Const.Eq___Const

`order` – reorder output¶

Format:

order qualified_name …

Effect:

hs-to-coq topologically sorts definitions so that they appear in dependency order. However, this sorting is not always correct — type classes introduce implicit dependencies that are invisible to hs-to-coq. This edit adds a new ordering constraint into the topological sort so that the output definitions appear in the order indicate in this edit.

You can order more than two definitions at the same time:

order Foo.foo Foo.bar Foo.baz

is equivalent to

order Foo.foo Foo.bar
order Foo.bar Foo.baz

Examples:

order GHC.Base.Functor__arrow GHC.Base.Applicative__arrow_op_ztzg__ GHC.Base.Applicative__arrow GHC.Base.Monad__arrow_return_ GHC.Base.Monad__arrow GHC.Base.Alternative__arrow GHC.Base.MonadPlus__arrow

`promote` – promote a definition from the term level to the type level¶

Format:

promote qualified_name …

Effect:

hs-to-coq divides Haskell definitions into two “levels”: type-level and term-level. Type-level definitions always appear above term-level definitions in the Coq output. The promote edit moves a term-level definition to the type level. It also recursively moves the transitive closure of all definitions on which the specified definition depends.

Examples:

promote MyModule.foo

`polyrec` – Make a function polymorphic recursive¶

Format:

polyrec qualified_name

Effect:

Translates a function which calls itself recursively at a different type.

Examples:

polyrec MyModule.foo

`manual notation` – Indicate presence of manual notation¶

Format:

manual notation name

Effect:

If your preamble includes custom notation (usually for operators), you need to indicate this using this edit. See Section Identifiers and Notation for more information about how hs-to-coq implements custom notation.

Examples:

manual notation GHC.Base

`set type` – Specify a type for a binding¶

Format:

set type qualified_name : Coq_type

set type qualified_name no type

Effect:

Sets the type of the given definition to the given type, or omits the type if no type is specified.

Examples:

set type Example.int_to_int : Z -> Z
set type Example.inferred no type
in CoreUtils.stripTicksE set type go_b : (b * Core.Expr b) -> (b * Core.Expr b)

Termination edits¶

`coinductive` – use a coinductive instead of an inductive datatype¶

Format:: coinductive qualified_name

Effect:

Examples:

`termination` – hints for termination proofs¶

Format:

termination qualified_name termination_argument

Examples:

termination MyModule.foo {struct arg_33__}
termination MyModule.foo {struct 3}
termination MyModule.foo {measure myExpr}
termination MyModule.foo {wf myRel myExpr}
termination MyModule.foo {corecursive}
termination MyModule.foo {deferred}

Effect:

By default, hs-to-coq translates recursive definitions using Coq’s fix operator, which requires that the recursion is obviously structurally recursive. This is not always the right choice, and a termination edit tells hs-to-coq to construct the recursive definition differently, where termination_argument is one of the following:

corecursive

This causes hs-to-coq to use cofix instead of fix.

{ struct qualified_name }

Coq’s fix operator usually determines the recursive argument automatically, but also supports the user to specify it explicitly. This termination_argument is just passed along to Coq’s fix.

{ struct number }

This variant specifies the position of the recursive argument, counting from 1 and ignoring type arguments. (Note: this variant is not actually valid Coq syntax, it is only allowed in edits files.)

{ measure expr }

{ measure expr ( relation ) }

{ wf relation expr }

With one of these forms for termination_argument, hs-to-coq uses Program Fixpoint to declare the function, passing these termination arguments along. See the documentation of Program Fixpoint for their precise meaning.

The expr is a Coq expression that mentions the parameters of the current functions. These often have names generated by hs-to-coq – look at the generated Coq code to see what they are.

Program Fixpoint only supports top-level declaration. When these termination edits are applied to local definitions, hs-to-coq therefore uses the fixed-point operator wfFix1 defined in GHC.Wf in our base library.

A side effect of these edits is that the definition (or the enclosing definition) is defines using Program, which leaves proof obligations to the user. These should be discharged using the obligations edit (see below).

deferred

This causes hs-to-coq to use the axiom deferredFix from the module GHC.DeferredFix to translate the recursive definition. This defers the termination proof until the verification stage, where the axiom deferredFix_eq_on is needed to learn anything about the recursive function, and this axion requires an (extensional) termination proof.

See the file GHC/DeferredFix.v for more details.

Examples:

termination Memo.mkTrie corecursive

termination Memo.lookupTrie { measure arg_1__ (Coq.NArith.BinNat.N.lt) }
obligations Memo.lookupTrie solve_lookupTrie

termination Data.Set.Internal.link {measure (Nat.add (set_size arg_1__) (set_size arg_2__))}
obligations Data.Set.Internal.link termination_by_omega

in Data.IntSet.Internal.foldlBits  termination go  {measure (Coq.NArith.BinNat.N.to_nat arg_0__)}
obligations Data.IntSet.Internal.foldlBits BitTerminationProofs.termination_foldl


termination QuickSort.quicksort deferred

`obligations` – Proof obligations in `Program` mode¶

Format:

obligations qualified_name tactic

Effect:

The specified definition is now defined using Program, and is followed by

Solve Obligations with (tactic).

with the specified tactic.

This is most commonly used with with the termination hint, but can be useful on its own: For example, Program mode automatically applies or unwraps sigma types, which may leave proof obligations.

The { measure … } termination argument of the termination edit always causes Program to be used. If no obligations edit is specified, then all obligations are solved with Admit Obligations..

The tactic is drawn from a very simple subset of Ltac, featuring identifiers, identifiers with @, application, numbers, underscore, ;, and ||. Anything richer should go in the preamble or midamble.

Mutual recursion edits¶

`inline mutual` – Move mutually-recursive functions into `let`-bindings¶

Format:

inline mutual qualified_name

Effect:

The specified definition must be part of a mutually recursive set of definitions. Instead of being defined as another mutual fixpoint, it will be inlined into each of the other mutual fixpoints that needs it with a let-binding; additionally, a top-level Coq definition is generated for each let-bound function that simply calls into the predefined recursive functions.

This facility is useful when translating groups of mutually recursive functions that contain “preprocessing” or “postprocessing” functions, where the group is otherwise structurally recursive. These functions are not “truly” mutual recursive, as they just hand along values of the type being recursed, and so if Coq could only see through them, everything would work fine. And indeed, as let-bindings, Coq can see through them.

As an example, consider the following pair of mutually recursive data types, which represent a Forest of nonempty Trees. Each Branch of a Tree holds an extra boolean flag, which we can extract with isOK. In Haskell:

data Forest a = Empty
              | WithTree (Tree a) (Forest a)

data Tree a = Branch Bool a (Forest a)

isOK :: Tree a -> Bool
isOK (Branch ok _ _) = ok

And in cleaned-up Coq:

Inductive Forest a : Type
  := Empty    : Forest a
  |  WithTree : Tree a -> Forest a -> Forest a
with Tree a : Type
  := Branch : bool -> a -> Forest a -> Tree a.

Arguments Empty    {_}.
Arguments WithTree {_} _ _.
Arguments Branch   {_} _ _ _.

Definition isOK {a} : Tree a -> bool :=
  fun '(Branch ok _ _) => ok.

Now we can define a pair of mapping functions that only apply a function inside subtrees where the boolean flag is true. The Haskell code is simple:

mapForest :: (a -> a) -> Forest a -> Forest a
mapForest f Empty           = Empty
mapForest f (WithTree t ts) = WithTree (mapTree f t) (mapForest f ts)

mapTree :: (a -> a) -> Tree a -> Tree a
mapTree f t | isOK t    = mapOKTree f t
            | otherwise = t

mapOKTree :: (a -> a) -> Tree a -> Tree a
mapOKTree f (Branch ok x ts) = Branch ok (f x) (mapForest f ts)

However, the (cleaned-up) Coq translation fails:

Fail Fixpoint mapForest {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree f t) (mapForest f ts)
  end
with mapTree {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree f t
  else t
with mapOKTree {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest f ts)
  end.

The issue is that mapTree calls mapOKTree on the same term, and not a subterm. But this just a preprocessing/postprocessing split – there’s nothing actually recursive going on.

But with

inline mutual mapOKTree

we instead get working Coq code (again, cleaned up):

Fixpoint mapForest {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree f t) (mapForest f ts)
  end
with mapTree {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  let mapOKTree {a} (f : a -> a) (t : Tree a) : Tree a :=
        match t with
        | Branch ok x ts => Branch ok (f x) (mapForest f ts)
        end in
  if isOK t
  then mapOKTree f t
  else t.

Definition mapOKTree {a} (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest f ts)
  end.

This is the idea. However, to be completely fair, we never produce Fixpoint commands; both in the failing case and in the successful case, we generate fix terms. In this example, this looks like (reindented)

Definition mapForest {a} : (a -> a) -> Forest a -> Forest a :=
  fix mapTree f t :=
    let mapOKTree arg_0__ arg_1__ :=
          match arg_0__, arg_1__ with
          | f, Branch ok x ts => Branch ok (f x) (mapForest f ts)
          end in
    if isOK t : bool
    then mapOKTree f t
    else t
  with mapForest arg_0__ arg_1__ :=
    match arg_0__, arg_1__ with
    | f, Empty => Empty
    | f, WithTree t ts => WithTree (mapTree f t) (mapForest f ts)
    end
  for mapForest.

Definition mapOKTree {a} : (a -> a) -> Tree a -> Tree a :=
  fun arg_0__ arg_1__ =>
    match arg_0__, arg_1__ with
    | f, Branch ok x ts => Branch ok (f x) (mapForest f ts)
    end.

Definition mapTree {a} : (a -> a) -> Tree a -> Tree a :=
  fix mapTree f t :=
    let mapOKTree arg_0__ arg_1__ :=
          match arg_0__, arg_1__ with
          | f, Branch ok x ts => Branch ok (f x) (mapForest f ts)
          end in
    if isOK t : bool
    then mapOKTree f t
    else t
  with mapForest arg_0__ arg_1__ :=
    match arg_0__, arg_1__ with
    | f, Empty => Empty
    | f, WithTree t ts => WithTree (mapTree f t) (mapForest f ts)
    end
  for mapTree.

Invariant Edit¶

`add invariant` – Specify an invariant that a datatype should satisfy¶

NOTE: Currently only applies to datatypes with a single constructor!

Format:

add invariant {

module = module,

qid = qualified_name,

tyVars = [ type_variables ],

constructor = qualified_name,

useSigmaType = [ names ],

invariant = coq_definition

}

Note: Currently, you cannot leave any of the parameters out, and they must appear in the order above.

Meaning of each parameter:

module denotes the name of the module to which the invariant applies.
qid is a qualified name that denotes the type to which the invariant applies.
tyVars is a list of the type variable arguments of the type passed to qid. For example, if the type passed to qid was declared in Haskell as
```
data Foo a b where
...
```
then tyVars should be set to [a, b].
constructor is a qualified name referring to the constructor of the type to which the invariant applies.
useSigmaType is a list of unqualified names of the definitions that should preserve the invariant. The Program keyword will be added in front of these definitions, so that Coq generates the needed proof obligations (see below under “Effect”). You must supply the proofs (see the edits file of the extended example below).
invariant is a Coq definition encoding the invariant. Note that the type of the definition passed to invariant should be a function type, where the argument type is the name of the type passed to qid, prefixed by “Raw”, and the return type is Type. For instance, if the type passed to qid is MyModule.Foo, the type of the definition passed to invariant should be MyModule.RawFoo -> Type.

Effect:

Inserts Coq code to support a datatype invariant for the type passed as qid, which we will henceforth refer to here as <ty_qid>.

In particular, creates a sigma type that pairs a value of type <ty_qid> with a proof that it satisfies the invariant. In the translated Coq file, the type <ty_qid> will now denote this sigma type. The original type (which was denoted by <ty_qid>) will be renamed by prefixing “Raw” in front of the original unqualified name (e.g. MyModule.Foo becomes MyModule.RawFoo).

Also creates notation that acts as a constructor for this new sigma type. Internally, this notation uses existT. Note that the last argument to existT is the proof part of the sigma type. Thus, wherever this notation is used to construct a value of the sigma type, the corresponding proof must be provided. Coq’s Program mode automatically unwarps sigma types and generates the necessary proof obligations (see below).

The original constructor will be renamed by adding the suffix _Raw.

The definitions specified in useSigmaType will use the sigma type instead of the original type. Thus, we need a way to provide the proof part of the sigma type. To this end, hs-to-coq will re-define these definitions using the Program keyword. As a result, when Coq encounters these definitions, it will enter Program mode. Program mode automatically applies or unwraps sigma types, which may generate proof obligations for the user.

You MUST use an obligations edit to supply the proofs; see the example below.

Example:

Suppose we create a Haskell module representing a counter, as shown below. We say that a Counter is valid if its internal integer is non-negative.

Below is the Haskell code:

module Counter(Counter, zeroCounter, inc, dec, isZero) where

data Counter = MkC Int
    deriving Show

zeroCounter :: Counter
zeroCounter = MkC 0

inc :: Counter -> Counter
inc (MkC x) = MkC (x+1)

dec :: Counter -> Counter
dec (MkC x) = if x > 0 then MkC (x - 1) else MkC 0

isZero :: Counter -> Bool
isZero (MkC x) = x == 0

valid :: Counter -> Bool
valid (MkC x) = x >= 0

Notice that any Counter created using the public API has the property that it is non-negative: zeroCounter is non-negative, and given a non-negative Counter, the public functions defined on Counter type preserve the fact that the counter is non-negative.

In Coq, we can formalize the invariant that the counter is non-negative with the help of an invariant edit.

Here is the edits file:

add invariant {
  module = Counter,
  qid = Counter.Counter,
  tyVars = [],
  constructor = MkC,
  useSigmaType = [Counter.zeroCounter, Counter.inc, Counter.dec],
  invariant = Definition Counter.NonNegInv : (Counter.RawCounter -> Type)
    := fun x => valid x = true.
  }

  promote Counter.valid  # promote valid from the term-level to the type-level

  obligations Counter.zeroCounter admit
  obligations Counter.inc admit
  obligations Counter.dec admit

Note that we have used a promote edit to lift the definition of valid from the term level to the type level. We need to do this because NonNegInv, which is in the type level, references valid. We have also provided (trivial) proof obligations for the definitions in the list passed to useSigmaType.

Here is the Coq output (relevant parts, cleaned up and with added comments):

(* Converted type declarations: *)

(* The original Counter datatype, now renamed to RawCounter.
   Notice that the constructor MkC has been renamed to MkC_Raw. *)
Inductive RawCounter : Type := | MkC_Raw : GHC.Num.Int -> RawCounter.

(* The definition of validity. Note that this came directly
   from the Haskell source. It is not suitable as an invariant,
   because the return type is not Type. *)
Definition valid : RawCounter -> bool :=
  fun '(MkC_Raw x) => x GHC.Base.>= #0.

(* The invariant. Notice the input has type RawCounter. *)
Definition NonNegInv : RawCounter -> Type :=
  fun x => valid x = true.

(* The sigma type. *)
Definition Counter : Type :=
  { x : RawCounter & NonNegInv x }.

(* The "constructor" for the sigma type. The last argument
   to @existT is the proof part of the sigma type. *)
Local Notation MkC y :=
  (@existT _ _ (MkC_Raw y) _).

(* Converted value declarations: *)

Program Definition zeroCounter : Counter :=
          MkC #0.
Admit Obligations.

Program Definition inc : Counter -> Counter :=
          fun '(MkC x) => MkC (x GHC.Num.+ #1).
Admit Obligations.

Program Definition dec : Counter -> Counter :=
          fun '(MkC x) =>
            if Bool.Sumbool.sumbool_of_bool (x GHC.Base.> #0)
            then MkC (x GHC.Num.- #1)
            else MkC #0.
Admit Obligations.

Definition isZero : RawCounter -> bool :=
  fun '(MkC_Raw x) => x GHC.Base.== #0.

Notice that some renaming has occurred: Counter has been renamed to RawCounter and MkC has been renamed MkC_Raw.

Note also that valid has been promoted to the type level. This is necessary, because NonNegInv refers to valid.

Finally, note the use of Program before the definitions of zeroCounter, inc, and dec, and observe that these definitions use Counter and MkC, while isZero uses RawCounter and MkC_Raw.

Meta-edits¶

`in` edit - restrict scope of an edit to a single definition¶

Format:: in qualified_name edit

Effect:

This is a meta-edit: The given edit is only applied during the translation of the given definition. This is most useful to rename or rewrite only within a specific function, or to give termination arguments to local functions.

While all edits are allowed, not all edits are useful when localized.

Examples:

in SrcLoc.Ord__RealSrcLoc_op_zl__ rewrite forall, SrcLoc.Ord__RealSrcLoc_compare = GHC.Base.compare
in Util.exactLog2 termination pow2 deferred

`except in` edit - exclude definitions from an edit¶

Format:: except in qualified_names edit

Effect:

This is essentially the opposite of an in edit. The given edit is applied as normal, except during the translation of the given definition(s). This is most useful to rename or rewrite a definition everywhere except within one or more functions. In addition, it can be used when there is a local function with the same name in multiple definitions, in order to give termination arguments to all occurrences of that local function except those in the specified definitions.

As with in edits, while all edits are allowed, for many edits it doesn’t make sense to apply except in.

Examples:

except in SrcLoc.Ord__RealSrcLoc_op_zl__ rewrite forall, SrcLoc.Ord__RealSrcLoc_compare = GHC.Base.compare
except in Util.exactLog2 termination pow2 deferred
except in ModuleName.def_1 skip case pattern _

# Multiple qualified names are separated with commas
except in ModuleName.def_1, ModuleName.def_2 rename type GHC.Types.[] = list

Caveats:

This edit does not currently work with data type definitions.

Deprecated edits¶

`add scope`¶

Format:: add scope scope for place qualified_name

Effect:

Examples:

`type synonym`¶

Format:: type synonym name :-> name

Effect:

Examples:

Edit Files¶

General format of edit files¶

Qualified names¶

Gallina expressions¶

Skipping Haskell¶

skip – skip a function, type, or type class instance¶

skip constructor – skip a constructor of a data type¶

skip class – skip a type class and all its instances¶

skip method – skip a method¶

skip equation – skip one equation of a function definition¶

skip case pattern – skip one alternative of a case expression¶

skip module – skip a module import¶

axiomatize module – replace all definitions in a module with axioms¶

axiomatize original module name – replace all definitions in a module with axioms, using the pre-renaming module name¶

axiomatize definition – replace a value definition with an axiom¶

unaxiomatize definition – override whole-module axiomatization on a case-by-case basis¶

Adding Coq Commands¶

add – inject a definition¶

add type – inject a definition into the type component¶

import – inject an Import statement¶

Renaming and Rewriting¶

rename type – rename a type¶

rename value – rename a value¶

rename module – change a module name¶

alias module – abbreviate a module name¶

rewrite – replace Haskell subexpressions¶

redefine – override a Coq definition¶

collapse let – if a definition is just a let-expression, inline it¶

Extra information¶

data kinds – Declare kinds of type arguments to Inductive datatypes¶

polykinds – Declare polymorphic kind variables to Inductive datatypes¶

class kinds – Declare kinds of type arguments to type classes¶

delete unused type variables – Remove unused type variables from a declaration¶

order – reorder output¶

promote – promote a definition from the term level to the type level¶

polyrec – Make a function polymorphic recursive¶

manual notation – Indicate presence of manual notation¶

set type – Specify a type for a binding¶

Termination edits¶

coinductive – use a coinductive instead of an inductive datatype¶

termination – hints for termination proofs¶

obligations – Proof obligations in Program mode¶

Mutual recursion edits¶

inline mutual – Move mutually-recursive functions into let-bindings¶

Invariant Edit¶

add invariant – Specify an invariant that a datatype should satisfy¶

Meta-edits¶

in edit - restrict scope of an edit to a single definition¶

except in edit - exclude definitions from an edit¶

Deprecated edits¶

add scope¶

type synonym¶

`skip` – skip a function, type, or type class instance¶

`skip constructor` – skip a constructor of a data type¶

`skip class` – skip a type class and all its instances¶

`skip method` – skip a method¶

`skip equation` – skip one equation of a function definition¶

`skip case pattern` – skip one alternative of a `case` expression¶

`skip module` – skip a module import¶

`axiomatize module` – replace all definitions in a module with axioms¶

`axiomatize original module name` – replace all definitions in a module with axioms, using the pre-renaming module name¶

`axiomatize definition` – replace a value definition with an axiom¶

`unaxiomatize definition` – override whole-module axiomatization on a case-by-case basis¶

`add` – inject a definition¶

`add type` – inject a definition into the type component¶

`import` – inject an `Import` statement¶

`rename type` – rename a type¶

`rename value` – rename a value¶

`rename module` – change a module name¶

`alias module` – abbreviate a module name¶

`rewrite` – replace Haskell subexpressions¶

`redefine` – override a Coq definition¶

`collapse let` – if a definition is just a `let`-expression, inline it¶

`data kinds` – Declare kinds of type arguments to Inductive datatypes¶

`polykinds` – Declare polymorphic kind variables to Inductive datatypes¶

`class kinds` – Declare kinds of type arguments to type classes¶

`delete unused type variables` – Remove unused type variables from a declaration¶

`order` – reorder output¶

`promote` – promote a definition from the term level to the type level¶

`polyrec` – Make a function polymorphic recursive¶

`manual notation` – Indicate presence of manual notation¶

`set type` – Specify a type for a binding¶

`coinductive` – use a coinductive instead of an inductive datatype¶

`termination` – hints for termination proofs¶

`obligations` – Proof obligations in `Program` mode¶

`inline mutual` – Move mutually-recursive functions into `let`-bindings¶

`add invariant` – Specify an invariant that a datatype should satisfy¶

`in` edit - restrict scope of an edit to a single definition¶

`except in` edit - exclude definitions from an edit¶

`add scope`¶

`type synonym`¶