From d51e5dc2fcc6b6c7d40aa45397925dc3444c3dbb Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 27 Mar 2011 13:32:20 -0700 Subject: [PATCH] change name of string-extraction placeholder --- src/Extraction-prefix.hs | 16 ++++++++-------- src/ExtractionMain.v | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 3179cdb..041ca7e 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -35,13 +35,6 @@ import qualified GHC.Base import qualified System.IO import qualified System.IO.Unsafe -{- -- used for extracting strings WITHOUT the patch for Coq -bin2ascii = - (\ b0 b1 b2 b3 b4 b5 b6 b7 -> - let f b i = if b then 1 `shiftL` i else 0 - in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) --} - getTyConTyVars :: TyCon.TyCon -> [Var.TyVar] getTyConTyVars tc = if TyCon.isFunTyCon tc @@ -159,7 +152,7 @@ coreCoercionToWeakCoercion c = (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1" (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1" (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1" --- (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)" + (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)" _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c)) _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c)) -- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t) @@ -191,3 +184,10 @@ trace msg x = System.IO.Unsafe.unsafePerformIO $ trace msg x = System.IO.Unsafe.unsafePerformIO $ (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x) -} + +{- -- used for extracting strings WITHOUT the patch for Coq +bin2ascii = + (\ b0 b1 b2 b3 b4 b5 b6 b7 -> + let f b i = if b then 1 `shiftL` i else 0 + in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) +-} diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index dbeb3cc..2f0856f 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -62,7 +62,7 @@ Extract Inlined Constant string_dec => "(==)". Extract Inlined Constant ascii_dec => "(==)". (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". +Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq". Extract Constant zero => "'\000'". Extract Constant one => "'\001'". Extract Constant shift => "shiftAscii". -- 1.7.10.4