add orM and add more mapsToExpls to SpecialTreatment.hs

GaloisInc · Mar 8, 2022 · f182756 · f182756
1 parent 3929005
commit f182756
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -1195,8 +1195,7 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
 
 (* Prelude.existsM was skipped *)
 
-Definition orM : forall (a : Type), CompM a -> CompM a -> CompM a :=
-  fun (a : Type) (m1 : CompM a) (m2 : CompM a) => @CompM.existsM SAWCoreScaffolding.Bool a (fun (b : SAWCoreScaffolding.Bool) => if b then m1 else m2).
+(* Prelude.orM was skipped *)
 
 (* Prelude.forallM was skipped *)
 

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -451,11 +451,11 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("errorM",               replace (Coq.App (Coq.ExplVar "errorM")
                                        [Coq.Var "CompM", Coq.Var "_"]))
   , ("catchM",               skip)
-  , ("existsM",              mapsTo compMModule "existsM")
-  , ("forallM",              mapsTo compMModule "forallM")
+  , ("existsM",              mapsToExpl compMModule "existsM")
+  , ("forallM",              mapsToExpl compMModule "forallM")
+  , ("orM",                  mapsToExpl compMModule "orM")
   , ("fixM",                 replace (Coq.App (Coq.ExplVar "fixM")
                                        [Coq.Var "CompM", Coq.Var "_"]))
-  , ("existsM",              mapsToExpl compMModule "existsM")
   , ("LetRecType",           mapsTo compMModule "LetRecType")
   , ("LRT_Ret",              mapsTo compMModule "LRT_Ret")
   , ("LRT_Fun",              mapsTo compMModule "LRT_Fun")