composeM is no longer skipped by the Coq translator

GaloisInc · Mar 15, 2021 · a2d632c · a2d632c
1 parent 9fa8e4f
commit a2d632c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -1027,7 +1027,8 @@ Definition foldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), foral
 
 (* Prelude.bindM was skipped *)
 
-(* Prelude.composeM was skipped *)
+Definition composeM : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> (b -> CompM c) -> a -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (g : b -> CompM c) (x : a) => @bindM CompM _ b c (f x) g.
 
 Definition tupleCompMFunBoth : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> prod c a -> CompM (prod c b) :=
   fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (x : prod c a) => @bindM CompM _ b (prod c b) (f (SAWCoreScaffolding.snd x)) (fun (y : b) => @returnM CompM _ (prod c b) (pair (SAWCoreScaffolding.fst x) y)).

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -446,12 +446,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("List__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
   ]
 
-  -- Definitions that depend on axioms currently skipped
-  ++
-  [ ("composeM",   skip)
-  , ("letRecFuns", skip)
-  ]
-
 constantsRenamingMap :: [(String, String)] -> Map.Map String String
 constantsRenamingMap notations = Map.fromList notations