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
(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)
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))
+-}
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".