From d78f9b74d648ec4279d904dcff48b562a138ff7d Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Mon, 16 Aug 2021 15:36:30 -0700 Subject: [PATCH] saw-core-coq: fix and document the local translation state (#1328) 5a37203a2c5d0f78faf1faa3ebc8ab3cbeacae2d introduced a subtle bug in the translation of Cryptol modules to Coq. In this commit, it was decided that all 'TranslationState' should be restored when calling `withLocalLocalEnvironment'. Historically, 'withLocalLocalEnvironment' was only supposed to restore the value of the 'localEnvironment' field of the translation state, hence its name. The translation state has grown since, and includes many fields that ought to be restored after a local (sub-)term translation. Unfortunately, the translation state also contains fields that are meant to monotonically accumulate global data through the translation. Those fields are thus being erased incorrectly due to the changes made. This commit revert those changes, making it painfully explicit which fields of the state are to be restored or preserved so that future refactorings will have to make a decision. In the process, I also renamed the confusing 'localDeclarations' into 'topLevelDeclarations', since it captures declarations that appear in the processed file (so more local than the "global", "ambient" standard library declarations), but the name made it sound like these were more local. --- .../CryptolPrimitivesForSAWCore.v | 7 +- .../generated/CryptolToCoq/SAWCorePrelude.v | 44 ++---- .../src/Verifier/SAW/Translation/Coq.hs | 12 +- .../SAW/Translation/Coq/CryptolModule.hs | 33 +++-- .../src/Verifier/SAW/Translation/Coq/Monad.hs | 26 +++- .../Verifier/SAW/Translation/Coq/SAWModule.hs | 34 ++--- .../SAW/Translation/Coq/SpecialTreatment.hs | 6 +- .../src/Verifier/SAW/Translation/Coq/Term.hs | 139 +++++++++++------- 8 files changed, 177 insertions(+), 124 deletions(-) diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v index cf2950a91f..28b94c7cd2 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v @@ -583,8 +583,11 @@ Definition ecRotR : forall (m : @Num), forall (ix : Type), forall (a : Type), @P Definition ecCat : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a := @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @seq n a -> @seq (@tcAdd (@TCNum m) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.append m n a) (fun (a : Type) => @SAWCorePrelude.streamAppend a m)). -Definition ecSplitAt : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a) := - @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a)) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> prod (@SAWCoreVectorsAsCoqVectors.Vec m a) (@seq n a)) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => pair (@SAWCorePrelude.take a m n xs) (@SAWCorePrelude.drop a m n xs)) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => pair (@SAWCorePrelude.streamTake a m xs) (@SAWCorePrelude.streamDrop a m xs))). +Definition ecTake : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a := + @CryptolPrimitivesForSAWCore.Num_rect (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.take a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamTake a m xs)) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCInf) n) a -> @SAWCorePrelude.Stream a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCorePrelude.Stream a) => xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => xs)). + +Definition ecDrop : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a := + @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @seq n a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.drop a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamDrop a m xs)). Definition ecJoin : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m (@seq n a) -> @seq (@tcMul m n) a := fun (m : @Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : @Num) => forall (n : @Num), forall (a : Type), @seq m1 (@seq n a) -> @seq (@tcMul m1 n) a) (fun (m1 : @SAWCoreScaffolding.Nat) => @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m1 (@seq n a) -> @seq (@tcMul (@TCNum m1) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.join m1 n a)) (@finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Stream (@seq n a) -> @seq (@tcMul (@TCInf) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.natCase (fun (n' : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec n' a) -> @seq (@SAWCorePrelude.if0Nat (@Num) n' (@TCNum 0) (@TCInf)) a) (fun (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec 0 a)) => @SAWCoreVectorsAsCoqVectors.EmptyVec a) (fun (n' : @SAWCoreScaffolding.Nat) (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n') a)) => @SAWCorePrelude.streamJoin a n' s) n)) m. diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v index c088de3a04..428d2342ba 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v @@ -182,8 +182,7 @@ Definition not_True : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCor Definition not_False : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) := @trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (if @SAWCoreScaffolding.false then @SAWCoreScaffolding.false else @SAWCoreScaffolding.true) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not__eq (@SAWCoreScaffolding.false)) (@ite_false (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.true)). -Definition not_not : forall (x : @SAWCoreScaffolding.Bool), let var__0 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not x)) x := +Definition not_not : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not x)) x := fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not b)) b) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_False) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_True). Definition and_True1 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) x) x := @@ -198,8 +197,7 @@ Definition and_True2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffoldin Definition and_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) := fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and b (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false)) x (@and_True1 (@SAWCoreScaffolding.false)) (@and_False1 (@SAWCoreScaffolding.false)). -Definition and_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), let var__0 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y z)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) z) := +Definition and_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y z)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) z) := fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y b)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) b)) z (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.and x y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.true)) y (@and_True2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x)) (@and_True2 (@SAWCoreScaffolding.and x y))) (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@and_False2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x)) (@and_False2 x)) (@and_False2 (@SAWCoreScaffolding.and x y))). Definition and_idem : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x x) x := @@ -217,8 +215,7 @@ Definition or_True2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding Definition or_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.false)) x := fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or b (@SAWCoreScaffolding.false)) b) x (@or_True1 (@SAWCoreScaffolding.false)) (@or_False1 (@SAWCoreScaffolding.false)). -Definition or_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), let var__0 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y z)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) z) := +Definition or_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y z)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) z) := fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y b)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) b)) z (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@or_True2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x)) (@or_True2 x)) (@or_True2 (@SAWCoreScaffolding.or x y))) (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.or x y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.false)) y (@or_False2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x)) (@or_False2 (@SAWCoreScaffolding.or x y))). Definition or_idem : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x x) x := @@ -263,26 +260,19 @@ Definition boolEq_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffo Definition boolEq_same : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq x x) (@SAWCoreScaffolding.true) := fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq b b) (@SAWCoreScaffolding.true)) x (@boolEq_True1 (@SAWCoreScaffolding.true)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@boolEq_False1 (@SAWCoreScaffolding.false)) not_False). -Definition not_or : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), let var__0 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - let var__1 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or x y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) := +Definition not_or : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or x y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) := fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or b y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not b) (@SAWCoreScaffolding.not y))) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y) (@SAWCoreScaffolding.true) (@or_True1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_True) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.false) (@and_False1 (@SAWCoreScaffolding.not y))) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True) (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.and z (@SAWCoreScaffolding.not y))))) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.not y) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) y) y (@or_False1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.and z (@SAWCoreScaffolding.not y))) (@and_True1 (@SAWCoreScaffolding.not y))))). -Definition not_and : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), let var__0 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - let var__1 := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in - @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and x y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) := +Definition not_and : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and x y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) := fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and b y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not b) (@SAWCoreScaffolding.not y))) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.not y) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) y) y (@and_True1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.or z (@SAWCoreScaffolding.not y))) (@or_False1 (@SAWCoreScaffolding.not y))))) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y) (@SAWCoreScaffolding.false) (@and_False1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_False) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.true) (@or_True1 (@SAWCoreScaffolding.not y))) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False) (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.or z (@SAWCoreScaffolding.not y))))). -Definition ite_not : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), let var__0 := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in - @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b then x else y) (if b then y else x) := +Definition ite_not : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b then x else y) (if b then y else x) := fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b' then x else y) (if b' then y else x)) b (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.true) then x else y) y (if @SAWCoreScaffolding.true then y else x) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.true) then x else y) (if @SAWCoreScaffolding.false then x else y) y (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True a (fun (z : @SAWCoreScaffolding.Bool) => if z then x else y)) (@ite_false a x y)) (@sym a (if @SAWCoreScaffolding.true then y else x) y (@ite_true a y x))) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.false) then x else y) x (if @SAWCoreScaffolding.false then y else x) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.false) then x else y) (if @SAWCoreScaffolding.true then x else y) x (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False a (fun (z : @SAWCoreScaffolding.Bool) => if z then x else y)) (@ite_true a x y)) (@sym a (if @SAWCoreScaffolding.false then y else x) x (@ite_false a y x))). -Definition ite_nest1 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), let var__0 := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in - @SAWCoreScaffolding.Eq a (if b then if b then x else y else z) (if b then x else z) := +Definition ite_nest1 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), @SAWCoreScaffolding.Eq a (if b then if b then x else y else z) (if b then x else z) := fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) (z : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if b' then if b' then x else y else z) (if b' then x else z)) b (@trans a (if @SAWCoreScaffolding.true then if @SAWCoreScaffolding.true then x else y else z) x (if @SAWCoreScaffolding.true then x else z) (@trans a (if @SAWCoreScaffolding.true then if @SAWCoreScaffolding.true then x else y else z) (if @SAWCoreScaffolding.true then x else y) x (@ite_true a (if @SAWCoreScaffolding.true then x else y) z) (@ite_true a x y)) (@sym a (if @SAWCoreScaffolding.true then x else z) x (@ite_true a x z))) (@trans a (if @SAWCoreScaffolding.false then if @SAWCoreScaffolding.false then x else y else z) z (if @SAWCoreScaffolding.false then x else z) (@ite_false a (if @SAWCoreScaffolding.false then x else y) z) (@sym a (if @SAWCoreScaffolding.false then x else z) z (@ite_false a x z))). -Definition ite_nest2 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), let var__0 := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in - @SAWCoreScaffolding.Eq a (if b then x else if b then y else z) (if b then x else z) := +Definition ite_nest2 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), @SAWCoreScaffolding.Eq a (if b then x else if b then y else z) (if b then x else z) := fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) (z : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if b' then x else if b' then y else z) (if b' then x else z)) b (@trans a (if @SAWCoreScaffolding.true then x else if @SAWCoreScaffolding.true then y else z) x (if @SAWCoreScaffolding.true then x else z) (@ite_true a x (if @SAWCoreScaffolding.true then y else z)) (@sym a (if @SAWCoreScaffolding.true then x else z) x (@ite_true a x z))) (@trans a (if @SAWCoreScaffolding.false then x else if @SAWCoreScaffolding.false then y else z) z (if @SAWCoreScaffolding.false then x else z) (@trans a (if @SAWCoreScaffolding.false then x else if @SAWCoreScaffolding.false then y else z) (if @SAWCoreScaffolding.false then y else z) z (@ite_false a x (if @SAWCoreScaffolding.false then y else z)) (@ite_false a y z)) (@sym a (if @SAWCoreScaffolding.false then x else z) z (@ite_false a x z))). (* Prelude.ite_bit was skipped *) @@ -510,8 +500,7 @@ Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b) Definition reverse : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec n a := fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec n a) => @SAWCoreVectorsAsCoqVectors.gen n a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a xs (@subNat (@subNat n 1) i)). -Definition transpose : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> let var__0 := @SAWCoreScaffolding.Nat -> Type -> Type in - @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreVectorsAsCoqVectors.Vec m a) := +Definition transpose : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreVectorsAsCoqVectors.Vec m a) := fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (xss : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @SAWCoreVectorsAsCoqVectors.gen n (@SAWCoreVectorsAsCoqVectors.Vec m a) (fun (j : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.gen m a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a (@SAWCorePrelude.sawAt m (@SAWCoreVectorsAsCoqVectors.Vec n a) xss i) j)). Definition vecEq : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (a -> a -> @SAWCoreScaffolding.Bool) -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreScaffolding.Bool := @@ -520,8 +509,7 @@ Definition vecEq : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (a - Definition take : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a := fun (a : Type) (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (v : @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a) => @SAWCoreVectorsAsCoqVectors.gen m a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt (@addNat m n) a v i). -Definition vecCong : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n -> let var__0 := @SAWCoreScaffolding.Nat -> Type -> Type in - @SAWCoreScaffolding.Eq Type (@SAWCoreVectorsAsCoqVectors.Vec m a) (@SAWCoreVectorsAsCoqVectors.Vec n a) := +Definition vecCong : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n -> @SAWCoreScaffolding.Eq Type (@SAWCoreVectorsAsCoqVectors.Vec m a) (@SAWCoreVectorsAsCoqVectors.Vec n a) := fun (a : Type) (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (eq : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n) => @eq_cong (@SAWCoreScaffolding.Nat) m n eq Type (fun (i : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.Vec i a). (* Prelude.coerceVec was skipped *) @@ -539,8 +527,7 @@ Definition slice : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), fora Definition join : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a := fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @SAWCoreVectorsAsCoqVectors.gen (@mulNat m n) a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a (@SAWCorePrelude.sawAt m (@SAWCoreVectorsAsCoqVectors.Vec n a) v (@divNat i n)) (@modNat i n)). -Definition split : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> let var__0 := @SAWCoreScaffolding.Nat -> Type -> Type in - @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) := +Definition split : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) := fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a) => @SAWCoreVectorsAsCoqVectors.gen m (@SAWCoreVectorsAsCoqVectors.Vec n a) (fun (i : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.gen n a (fun (j : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt (@mulNat m n) a v (@addNat (@mulNat i n) j))). Definition append : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a := @@ -557,8 +544,7 @@ Definition append : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreSc Definition joinLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a := fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @join m n a (@reverse m (@SAWCoreVectorsAsCoqVectors.Vec n a) v). -Definition splitLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> let var__0 := @SAWCoreScaffolding.Nat -> Type -> Type in - @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) := +Definition splitLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) := fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a) => @reverse m (@SAWCoreVectorsAsCoqVectors.Vec n a) (@split m n a v). Definition msb : forall (n : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Bool := @@ -874,11 +860,9 @@ Definition bvultWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @ Definition bvuleWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvule n v1 v2) (@SAWCoreScaffolding.true)) := fun (n : @SAWCoreScaffolding.Nat) (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) b (@SAWCoreScaffolding.true))) (@SAWCoreVectorsAsCoqVectors.bvule n v1 v2) (@Just (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.Refl (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true))) (@Nothing (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.true))). -Axiom bvEqToEqNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) v1 v2 -> let var__0 := forall (n1 : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Nat in - @eqNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) . +Axiom bvEqToEqNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) v1 v2 -> @eqNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) . -Axiom bvultToIsLtNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n v1 v2) (@SAWCoreScaffolding.true) -> let var__0 := forall (n1 : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Nat in - @IsLtNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) . +Axiom bvultToIsLtNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n v1 v2) (@SAWCoreScaffolding.true) -> @IsLtNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) . Axiom genWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (forall (i : @SAWCoreScaffolding.Nat), @IsLtNat i n -> a) -> @SAWCoreVectorsAsCoqVectors.Vec n a . diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs index e14bcefbe3..34dfc2d7b6 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs @@ -113,7 +113,11 @@ Import ListNotations. translateTermAsDeclImports :: TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann) translateTermAsDeclImports configuration name t = do - doc <- TermTranslation.translateDefDoc configuration Nothing [] name t + doc <- + TermTranslation.translateDefDoc + configuration + (TermTranslation.TranslationReader Nothing) + [] name t return $ vcat [preamble configuration, hardline <> doc] translateSAWModule :: TranslationConfiguration -> Module -> Doc ann @@ -131,7 +135,11 @@ translateSAWModule configuration m = ] translateCryptolModule :: - TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann) + TranslationConfiguration -> + -- | List of already translated global declarations + [String] -> + CryptolModule -> + Either (TranslationError Term) (Doc ann) translateCryptolModule configuration globalDecls m = let decls = CryptolModuleTranslation.translateCryptolModule configuration diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs index 8f47a8c931..4ce29b872b 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs @@ -8,10 +8,10 @@ import Control.Monad (forM) import Control.Monad.State (modify) import qualified Data.Map as Map -import Cryptol.ModuleSystem.Name -import Cryptol.Utils.Ident +import Cryptol.ModuleSystem.Name (Name, nameIdent) +import Cryptol.Utils.Ident (unpackIdent) import qualified Language.Coq.AST as Coq -import Verifier.SAW.Term.Functor +import Verifier.SAW.Term.Functor (Term) import Verifier.SAW.Translation.Coq.Monad import qualified Verifier.SAW.Translation.Coq.Term as TermTranslation import Verifier.SAW.TypedTerm @@ -23,21 +23,28 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry translateAndRegisterEntry (name, symbol) = do let t = ttTerm symbol let nameStr = unpackIdent (nameIdent name) - term <- TermTranslation.withLocalLocalEnvironment $ do + term <- TermTranslation.withLocalTranslationState $ do modify $ set TermTranslation.localEnvironment [nameStr] TermTranslation.translateTerm t let decl = TermTranslation.mkDefinition nameStr term modify $ over TermTranslation.globalDeclarations (nameStr :) return decl +-- | Translates a Cryptol Module into a list of Coq declarations. This is done +-- by going through the term map corresponding to the module, translating all +-- terms, and accumulating the translated declarations of all top-level +-- declarations encountered. translateCryptolModule :: - TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl] + TranslationConfiguration -> + -- | List of already translated global declarations + [String] -> + CryptolModule -> + Either (TranslationError Term) [Coq.Decl] translateCryptolModule configuration globalDecls (CryptolModule _ tm) = - case TermTranslation.runTermTranslationMonad - configuration - Nothing - globalDecls - [] - (translateTypedTermMap tm) of - Left e -> Left e - Right (_, st) -> Right (reverse (view TermTranslation.localDeclarations st)) + reverse . view TermTranslation.topLevelDeclarations . snd + <$> TermTranslation.runTermTranslationMonad + configuration + (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no? + globalDecls + [] + (translateTypedTermMap tm) diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs index f2a441a037..21d69675f4 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs @@ -17,6 +17,7 @@ module Verifier.SAW.Translation.Coq.Monad , TranslationConfigurationMonad , TranslationMonad , TranslationError(..) + , WithTranslationConfiguration(..) , runTranslationMonad ) where @@ -77,19 +78,32 @@ data TranslationConfiguration = TranslationConfiguration -- - SAWCoreVectorsAsSSReflectSeqs } -type TranslationConfigurationMonad m = - ( MonadReader TranslationConfiguration m +-- | The functional dependency of 'MonadReader' makes it not compositional, so +-- we have to jam together different structures that want to be in the 'Reader' +-- into a single datatype. This type allows adding extra configuration on top +-- of the translation configuration. +data WithTranslationConfiguration r = WithTranslationConfiguration + { translationConfiguration :: TranslationConfiguration + , otherConfiguration :: r + } + +-- | Some computations will rely solely on access to the configuration, so we +-- provide it separately. +type TranslationConfigurationMonad r m = + ( MonadReader (WithTranslationConfiguration r) m ) -type TranslationMonad s m = +type TranslationMonad r s m = ( Except.MonadError (TranslationError Term) m - , TranslationConfigurationMonad m + , TranslationConfigurationMonad r m , MonadState s m ) runTranslationMonad :: TranslationConfiguration -> + r -> s -> - (forall m. TranslationMonad s m => m a) -> + (forall m. TranslationMonad r s m => m a) -> Either (TranslationError Term) (a, s) -runTranslationMonad configuration state m = runStateT (runReaderT m configuration) state +runTranslationMonad configuration r s m = + runStateT (runReaderT m (WithTranslationConfiguration configuration r)) s diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs index 23dfb81774..67ba2b0d40 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs @@ -24,10 +24,8 @@ Portability : portable module Verifier.SAW.Translation.Coq.SAWModule where -import Control.Lens (makeLenses, view) import qualified Control.Monad.Except as Except import Control.Monad.Reader hiding (fail) -import Control.Monad.State hiding (fail) import Prelude hiding (fail) import Prettyprinter (Doc) @@ -36,26 +34,22 @@ import qualified Language.Coq.Pretty as Coq import Verifier.SAW.Module import Verifier.SAW.SharedTerm import Verifier.SAW.Term.Functor -import Verifier.SAW.Translation.Coq.Monad +import qualified Verifier.SAW.Translation.Coq.Monad as M import Verifier.SAW.Translation.Coq.SpecialTreatment import qualified Verifier.SAW.Translation.Coq.Term as TermTranslation +import Verifier.SAW.Translation.Coq.Monad -- import Debug.Trace -data ModuleTranslationState = ModuleTranslationState - { _currentModule :: Maybe ModuleName - } - deriving (Show) -makeLenses ''ModuleTranslationState - -type ModuleTranslationMonad m = TranslationMonad ModuleTranslationState m +type ModuleTranslationMonad m = + M.TranslationMonad TermTranslation.TranslationReader () m runModuleTranslationMonad :: - TranslationConfiguration -> Maybe ModuleName -> + M.TranslationConfiguration -> Maybe ModuleName -> (forall m. ModuleTranslationMonad m => m a) -> - Either (TranslationError Term) (a, ModuleTranslationState) -runModuleTranslationMonad configuration modname = - runTranslationMonad configuration (ModuleTranslationState modname) + Either (M.TranslationError Term) (a, ()) +runModuleTranslationMonad configuration modName = + M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) () dropPi :: Coq.Term -> Coq.Term dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r @@ -162,15 +156,19 @@ liftTermTranslationMonad :: (forall n. TermTranslation.TermTranslationMonad n => n a) -> (forall m. ModuleTranslationMonad m => m a) liftTermTranslationMonad n = do - configuration <- ask - cur_mod <- view currentModule <$> get - let r = TermTranslation.runTermTranslationMonad configuration cur_mod [] [] n + configuration <- asks translationConfiguration + configReader <- asks otherConfiguration + let r = TermTranslation.runTermTranslationMonad configuration configReader [] [] n case r of Left e -> Except.throwError e Right (a, _) -> do return a -translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc ann +translateDecl :: + M.TranslationConfiguration -> + Maybe ModuleName -> + ModuleDecl -> + Doc ann translateDecl configuration modname decl = case decl of TypeDecl td -> do diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs index 0a54491e0c..92e83624ba 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs @@ -25,7 +25,7 @@ Portability : portable module Verifier.SAW.Translation.Coq.SpecialTreatment where import Control.Lens (_1, _2, over) -import Control.Monad.Reader (ask) +import Control.Monad.Reader (asks) import qualified Data.Map as Map import Data.String.Interpolate (i) import qualified Data.Text as Text @@ -70,10 +70,10 @@ translateModuleName mn = Map.findWithDefault mn mn moduleRenamingMap findSpecialTreatment :: - TranslationConfigurationMonad m => + TranslationConfigurationMonad r m => Ident -> m IdentSpecialTreatment findSpecialTreatment ident = do - configuration <- ask + configuration <- asks translationConfiguration let moduleMap = Map.findWithDefault Map.empty (identModule ident) (specialTreatmentMap configuration) let defaultTreatment = diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs index d51d405819..ec1548c9aa 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs @@ -62,6 +62,13 @@ traceTerm :: String -> Term -> a -> a traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a -} +newtype TranslationReader = TranslationReader + { _currentModule :: Maybe ModuleName + } + deriving (Show) + +makeLenses ''TranslationReader + data TranslationState = TranslationState { _globalDeclarations :: [String] @@ -70,7 +77,7 @@ data TranslationState = TranslationState -- same file). We want to translate those exactly once, so we need to keep -- track of which ones have already been translated. - , _localDeclarations :: [Coq.Decl] + , _topLevelDeclarations :: [Coq.Decl] -- ^ Because some terms capture their dependencies, translating one term may -- result in multiple declarations: one for the term itself, but also zero or -- many for its dependencies. We store all of those in this, so that a caller @@ -95,12 +102,14 @@ data TranslationState = TranslationState -- ^ The next available name to be used for a let-bound shared -- sub-expression. - , _currentModule :: Maybe ModuleName } deriving (Show) makeLenses ''TranslationState +type TermTranslationMonad m = + TranslationMonad TranslationReader TranslationState m + -- | The set of reserved identifiers in Coq, obtained from section -- "Gallina Specification Language" of the Coq reference manual. -- @@ -134,52 +143,61 @@ getNamesOfAllDeclarations :: getNamesOfAllDeclarations = view allDeclarations <$> get where allDeclarations = - to (\ (TranslationState {..}) -> namedDecls _localDeclarations ++ _globalDeclarations) - -type TermTranslationMonad m = TranslationMonad TranslationState m + to (\ (TranslationState {..}) -> namedDecls _topLevelDeclarations ++ _globalDeclarations) runTermTranslationMonad :: TranslationConfiguration -> - Maybe ModuleName -> + TranslationReader -> [String] -> [Coq.Ident] -> (forall m. TermTranslationMonad m => m a) -> Either (TranslationError Term) (a, TranslationState) -runTermTranslationMonad configuration modname globalDecls localEnv = - runTranslationMonad configuration +runTermTranslationMonad configuration r globalDecls localEnv = + runTranslationMonad configuration r (TranslationState { _globalDeclarations = globalDecls - , _localDeclarations = [] + , _topLevelDeclarations = [] , _localEnvironment = localEnv , _unavailableIdents = Set.union reservedIdents (Set.fromList localEnv) , _sharedNames = IntMap.empty , _nextSharedName = "var__0" - , _currentModule = modname }) errorTermM :: TermTranslationMonad m => String -> m Coq.Term errorTermM str = return $ Coq.App (Coq.Var "error") [Coq.StringLit str] translateIdentWithArgs :: TermTranslationMonad m => Ident -> [Term] -> m Coq.Term -translateIdentWithArgs i args = - (view currentModule <$> get) >>= \cur_modname -> +translateIdentWithArgs i args = do + currentModuleName <- asks (view currentModule . otherConfiguration) let identToCoq ident = - if Just (identModule ident) == cur_modname then identName ident else - show (translateModuleName (identModule ident)) - ++ "." ++ identName ident in + if Just (identModule ident) == currentModuleName + then identName ident + else + show (translateModuleName (identModule ident)) + ++ "." ++ identName ident + specialTreatment <- findSpecialTreatment i + applySpecialTreatment identToCoq (atUseSite specialTreatment) - (atUseSite <$> findSpecialTreatment i) >>= \case - UsePreserve -> Coq.App (Coq.ExplVar $ identToCoq i) <$> mapM translateTerm args - UseRename targetModule targetName -> - Coq.App (Coq.ExplVar $ identToCoq $ - mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule) - (Text.pack targetName)) <$> - mapM translateTerm args - UseReplaceDropArgs n replacement - | length args >= n -> Coq.App replacement <$> mapM translateTerm (drop n args) - UseReplaceDropArgs n _ -> - errorTermM ("Identifier " ++ show i - ++ " not applied to required number of args," - ++ " which is " ++ show n) + where + + applySpecialTreatment identToCoq UsePreserve = + Coq.App (Coq.ExplVar $ identToCoq i) <$> mapM translateTerm args + applySpecialTreatment identToCoq (UseRename targetModule targetName) = + Coq.App + (Coq.ExplVar $ identToCoq $ + mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule) + (Text.pack targetName)) + <$> mapM translateTerm args + applySpecialTreatment _identToCoq (UseReplaceDropArgs n replacement) + | length args >= n = + Coq.App replacement <$> mapM translateTerm (drop n args) + applySpecialTreatment _identToCoq (UseReplaceDropArgs n _) = + errorTermM (unwords + [ "Identifier" + , show i + , "not applied to required number of args, which is" + , show n + ] + ) translateIdent :: TermTranslationMonad m => Ident -> m Coq.Term translateIdent i = translateIdentWithArgs i [] @@ -318,13 +336,34 @@ asApplyAllRecognizer :: Recognizer Term (Term, [Term]) asApplyAllRecognizer t = do _ <- asApp t return $ asApplyAll t --- | Run a translation, but keep changes to the environment local to it, --- restoring the current environment before returning. -withLocalLocalEnvironment :: TermTranslationMonad m => m a -> m a -withLocalLocalEnvironment action = do - s <- get +-- | Run a translation, but keep some changes to the translation state local to +-- that computation, restoring parts of the original translation state before +-- returning. +withLocalTranslationState :: TermTranslationMonad m => m a -> m a +withLocalTranslationState action = do + before <- get result <- action - put s + after <- get + put (TranslationState + -- globalDeclarations is **not** restored, because we want to translate each + -- global declaration exactly once! + { _globalDeclarations = view globalDeclarations after + -- topLevelDeclarations is **not** restored, because it accumulates the + -- declarations witnessed in a given module so that we can extract it. + , _topLevelDeclarations = view topLevelDeclarations after + -- localEnvironment **is** restored, because the identifiers added to it + -- during translation are local to the term that was being translated. + , _localEnvironment = view localEnvironment before + -- unavailableIdents **is** restored, because the extra identifiers + -- unavailable in the term that was translated are local to it. + , _unavailableIdents = view unavailableIdents before + -- sharedNames **is** restored, because we are leaving the scope of the + -- locally shared names. + , _sharedNames = view sharedNames before + -- nextSharedName **is** restored, because we are leaving the scope of the + -- last names used. + , _nextSharedName = view nextSharedName before + }) return result mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Decl @@ -354,7 +393,7 @@ translateParams ((n, ty):ps) = do return (Coq.Binder n' (Just ty') : ps') translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term -translatePi binders body = withLocalLocalEnvironment $ do +translatePi binders body = withLocalTranslationState $ do bindersT <- forM binders $ \ (b, bType) -> do bTypeT <- translateTerm bType b' <- freshenAndBindName b @@ -389,7 +428,7 @@ nextVariant = reverse . go . reverse translateTermLet :: TermTranslationMonad m => Term -> m Coq.Term translateTermLet t = - withLocalLocalEnvironment $ + withLocalTranslationState $ do let counts = scTermCount False t let locals = fmap fst $ IntMap.filter keep counts names <- traverse (const nextName) locals @@ -419,7 +458,7 @@ translateTerm t = Just x -> pure (Coq.Var x) translateTermUnshared :: TermTranslationMonad m => Term -> m Coq.Term -translateTermUnshared t = withLocalLocalEnvironment $ do +translateTermUnshared t = withLocalTranslationState $ do -- traceTerm "translateTerm" t $ -- NOTE: env is in innermost-first order env <- view localEnvironment <$> get @@ -487,7 +526,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do do len <- translateTerm n (x', expr) <- - withLocalLocalEnvironment $ + withLocalTranslationState $ do x' <- freshenAndBindName x expr <- translateTerm body pure (x', expr) @@ -514,7 +553,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do case lambda of (asLambdaList -> ((recFn, _) : binders, body)) -> do let (_binderPis, otherPis) = splitAt (length binders) pis - (recFn', bindersT, typeT, bodyT) <- withLocalLocalEnvironment $ do + (recFn', bindersT, typeT, bodyT) <- withLocalTranslationState $ do -- this is very ugly... recFn' <- freshenAndBindName recFn bindersT <- mapM @@ -543,7 +582,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do -- Constants come with a body Constant n body -> do - configuration <- ask + configuration <- asks translationConfiguration let renamed = translateConstant (notations configuration) n alreadyTranslatedDecls <- getNamesOfAllDeclarations let definitionsToSkip = skipDefinitions configuration @@ -552,13 +591,13 @@ translateTermUnshared t = withLocalLocalEnvironment $ do else do b <- -- Translate body in a top-level name scope - withLocalLocalEnvironment $ + withLocalTranslationState $ do modify $ set localEnvironment [] modify $ set unavailableIdents reservedIdents modify $ set sharedNames IntMap.empty modify $ set nextSharedName "var__0" translateTermLet body - modify $ over localDeclarations $ (mkDefinition renamed b :) + modify $ over topLevelDeclarations $ (mkDefinition renamed b :) Coq.Var <$> pure renamed where @@ -590,16 +629,16 @@ defaultTermForType typ = do translateTermToDocWith :: TranslationConfiguration -> - Maybe ModuleName -> + TranslationReader -> [String] -> [String] -> (Coq.Term -> Doc ann) -> Term -> Either (TranslationError Term) (Doc ann) -translateTermToDocWith configuration mn globalDecls localEnv f t = do +translateTermToDocWith configuration r globalDecls localEnv f t = do (term, state) <- - runTermTranslationMonad configuration mn globalDecls localEnv (translateTermLet t) - let decls = view localDeclarations state + runTermTranslationMonad configuration r globalDecls localEnv (translateTermLet t) + let decls = view topLevelDeclarations state return $ vcat $ [ (vcat . intersperse hardline . map Coq.ppDecl . reverse) decls @@ -609,10 +648,10 @@ translateTermToDocWith configuration mn globalDecls localEnv f t = do translateDefDoc :: TranslationConfiguration -> - Maybe ModuleName -> + TranslationReader -> [String] -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann) -translateDefDoc configuration mn globalDecls name = - translateTermToDocWith configuration mn globalDecls [name] - (\ term -> Coq.ppDecl (mkDefinition name term)) +translateDefDoc configuration r globalDecls name = + translateTermToDocWith configuration r globalDecls [name] + (Coq.ppDecl . mkDefinition name)