Coq translator incorrectly handles let-bindings in argument types

[eddywestbrook]

The following SAW core definition generates an Coq type-checking error when translated to Coq:

test : Nat -> Sigma Nat (\ (n:Nat) -> (m:Nat) -> IsLeNat n (Succ m) -> Nat);
test x =
  exists Nat (\ (n:Nat) -> (m:Nat) -> IsLeNat n (Succ m) -> Nat)
         (addNat (Succ x) (Succ x))
         (\ (m:Nat) (pf:IsLeNat (addNat (Succ x) (Succ x)) (Succ m)) -> m);

The resulting Coq generated by the Coq translator is:

Definition test : Coq.Init.Datatypes.nat -> @sigT Coq.Init.Datatypes.nat (fun (n : Coq.Init.Datatypes.nat) => forall (m : Coq.Init.Datatypes.nat), SAWCoreScaffolding.IsLeNat n (SAWCoreScaffolding.Succ m) -> Coq.Init.Datatypes.nat) :=
  fun (x : Coq.Init.Datatypes.nat) => let var__0   := SAWCoreScaffolding.Succ x in
  @existT Coq.Init.Datatypes.nat (fun (n : Coq.Init.Datatypes.nat) => forall (m : Coq.Init.Datatypes.nat), SAWCoreScaffolding.IsLeNat n (SAWCoreScaffolding.Succ m) -> Coq.Init.Datatypes.nat) (SAWCorePrelude.addNat var__0 var__0) (fun (m : Coq.Init.Datatypes.nat) (pf : SAWCoreScaffolding.IsLeNat (SAWCorePrelude.addNat (SAWCoreScaffolding.Succ x) (SAWCoreScaffolding.Succ x)) var__0) => m).

The difficulty is that var__0 is bound to Succ x in the body of test, but is then used for the Succ m term in the type of pf. The issue is that, in both places, the Coq translator is recognizing that the term being translated to var__0 is the Succ constructor applied to deBruijn index 0, but deBruijn index 0 refers to x in the body of test and it refers to m in the type of pf.

The simplest way to reproduce this is to use Heapster to generate the Coq. This can be done by supplying any arbitrary LLVM bitcode file XXX.bc and executing the following SAW script file:

enable_experimental;
env <- heapster_init_env_from_file "test.sawcore" "XXX.bc";
heapster_export_coq env "test.v";

This expects the test.sawcore file to look like this:

module linked_list where

import Prelude;

// include the above definition of test

[eddywestbrook]

My recommendation (which I am already working on) is to reorganize some of how the Coq translator handles variable bindings in general. The current approach is a little confusing, because it uses a monadic action freshenAndBindName to bind a variable, which implicitly runs the rest of the translation following it in the extended context with the new name, up to the nearest enclosing withLocalTranslationState. In some places, freshenAndBindName is multiple functions deep, which can make it hard to read and follow the code. It's also a little unclear where to put the calls to withLocalTranslationState, and that function is sometimes used where variables are not even bound, but the docs in that function read as if it's expecting variable binding.

Instead, it would be easier to understand if we had a withBoundVar operation, that would run a translation computation with the variable context locally extended with a new variable. The current functions for translating binders would have to be replaced by functions that take in computations for the body, which would make them higher-order, but I think that would still be easier to understand than the implicit state changing approach as it is now.