Commit 58c4080d authored by Bernd Brassel's avatar Bernd Brassel
Browse files

external definitions for new debugger

parent e15d5d6b
{- Auto generated stubs for external functions and types
Remove this comment to suppress warnings. -}
strict_prim_doesFileExist ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Bool dm))
strict_prim_doesFileExist x0
= hook_strict_prim_doesFileExist x0
(Prelude.error "not implemented")
strict_prim_doesDirectoryExist ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Bool dm))
strict_prim_doesDirectoryExist x0
= hook_strict_prim_doesDirectoryExist x0
(Prelude.error "not implemented")
strict_prim_fileSize ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Int dm))
strict_prim_fileSize x0
= hook_strict_prim_fileSize x0 (Prelude.error "not implemented")
strict_prim_getModificationTime ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (STime.ClockTime dm))
strict_prim_getModificationTime x0
= hook_strict_prim_getModificationTime x0
(Prelude.error "not implemented")
strict_getCurrentDirectory ::
(DebugMonad.DM dm) =>
dm (SPrelude.IO dm (SPrelude.List dm (SPrelude.Char dm)))
strict_getCurrentDirectory
= hook_strict_getCurrentDirectory (Prelude.error "not implemented")
strict_prim_setCurrentDirectory ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_setCurrentDirectory x0
= hook_strict_prim_setCurrentDirectory x0
(Prelude.error "not implemented")
strict_prim_getDirectoryContents ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm
(SPrelude.IO dm
(SPrelude.List dm (SPrelude.List dm (SPrelude.Char dm))))
strict_prim_getDirectoryContents x0
= hook_strict_prim_getDirectoryContents x0
(Prelude.error "not implemented")
strict_prim_createDirectory ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_createDirectory x0
= hook_strict_prim_createDirectory x0
(Prelude.error "not implemented")
strict_prim_removeFile ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_removeFile x0
= hook_strict_prim_removeFile x0 (Prelude.error "not implemented")
strict_prim_removeDirectory ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_removeDirectory x0
= hook_strict_prim_removeDirectory x0
(Prelude.error "not implemented")
strict_prim_renameFile ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_renameFile x0 x1
= hook_strict_prim_renameFile x0 x1
(Prelude.error "not implemented")
strict_prim_renameDirectory ::
(DebugMonad.DM dm) =>
SPrelude.List dm (SPrelude.Char dm) ->
SPrelude.List dm (SPrelude.Char dm) ->
dm (SPrelude.IO dm (SPrelude.Unit dm))
strict_prim_renameDirectory x0 x1
= hook_strict_prim_renameDirectory x0 x1
(Prelude.error "not implemented")
import qualified Char
instance DebugInfo.GenTerm (Float dm) where
underscore = FloatUnderscore
genTerm FloatUnderscore = DebugInfo.TermUnderscore (DebugInfo.SrcID "Prelude" 2)
genTerm (Float f) = DebugInfo.TermFloat f
instance DebugInfo.GenTerm (Char dm) where
underscore = CharUnderscore
genTerm CharUnderscore = DebugInfo.TermUnderscore (DebugInfo.SrcID "Prelude" 0)
genTerm (Char c) = DebugInfo.TermChar c
instance DebugInfo.GenTerm (IO dm a) where
underscore = IOUnderscore
genTerm IOUnderscore = DebugInfo.TermUnderscore (DebugInfo.SrcID "Prelude" Prelude.undefined)
genTerm x0 = Prelude.error "not implemented"
natToHInt :: DebugMonad.DM dm => Nat dm -> Prelude.Integer
natToHInt IHi = 1
natToHInt (O x) = 2 Prelude.* natToHInt x
natToHInt (I x) = 2 Prelude.* natToHInt x Prelude.+ 1
intToHInt :: DebugMonad.DM dm => Int dm -> Prelude.Integer
intToHInt (Neg n) = Prelude.negate (natToHInt n)
intToHInt (Pos n) = natToHInt n
intToHInt Zero = 0
hIntToNat :: (DebugMonad.DM dm,Prelude.Integral n) => n -> Nat dm
hIntToNat 1 = IHi
hIntToNat i = case Prelude.divMod i 2 of
(d,0) -> O (hIntToNat d)
(d,1) -> I (hIntToNat d)
hIntToInt :: (DebugMonad.DM dm,Prelude.Integral n) => n -> Int dm
hIntToInt i | i Prelude.< 0 = Neg (hIntToNat (Prelude.negate i))
| i Prelude.== 0 = Zero
| Prelude.otherwise = Pos (hIntToNat i)
listToHList :: DebugMonad.DM dm => List dm a -> [a]
listToHList Nil = []
listToHList (Cons x xs) = x:listToHList xs
charToHChar :: DebugMonad.DM dm => Char dm -> Prelude.Char
charToHChar (Char c) = c
data (DebugMonad.DM dm) => Float dm = Float Prelude.Float | FloatUnderscore
data (DebugMonad.DM dm) => Char dm = Char Prelude.Char | CharUnderscore
-- data (DebugMonad.DM dm) => IO dm a = IO (Prelude.IO a) | IOUnderscore
-- data (DebugMonad.DM dm) => IO dm a = IO a | IOUnderscore
-- data IO dm a = IO (World -> (a,World))
-- data IO dm a = IO (DebugMonad.Func dm (Unit dm) (a,Unit dm))
data IO dm a = IO ((Unit dm) -> (a,(Unit dm))) | IOUnderscore
return :: DebugMonad.DM dm => a -> dm a
return = Prelude.return
(?) :: DebugMonad.DM dm => a -> a -> dm a
x ? _ = return x
--_ ? y = Prelude.return y
-- implementation just returns () representation
strict_prim_putChar ::
(DebugMonad.DM dm) => Char dm -> dm (IO dm (Unit dm))
strict_prim_putChar x0 = hook_strict_prim_putChar x0 (return (IO Unit))
-- extracts a regular Char from the Virtual I/O information of the oracle
extractChar :: (DebugMonad.DM dm) => dm Prelude.Char
extractChar = DebugMonad.getNextExtVal
strict_getChar :: (DebugMonad.DM dm) => dm (IO dm (Char dm))
strict_getChar =
do c <- extractChar
hook_strict_getChar (return (IO (Char c)))
op_DollarEMark ::
(DebugMonad.DM dm, DebugInfo.GenTerm a, DebugInfo.GenTerm b) =>
DebugMonad.Func dm a b -> a -> dm b
op_DollarEMark x0 x1
= hook_op_DollarEMark x0 x1 (strict_apply x0 x1)
op_DollarEMarkEMark ::
(DebugMonad.DM dm, DebugInfo.GenTerm a, DebugInfo.GenTerm b) =>
DebugMonad.Func dm a b -> a -> dm b
op_DollarEMarkEMark x0 x1
= hook_op_DollarEMarkEMark x0 x1 (strict_apply x0 x1)
op_DollarRhomb ::
(DebugMonad.DM dm, DebugInfo.GenTerm a, DebugInfo.GenTerm b) =>
DebugMonad.Func dm a b -> a -> dm b
op_DollarRhomb x0 x1
= hook_op_DollarRhomb x0 x1 (strict_apply x0 x1)
op_DollarRhombRhomb ::
(DebugMonad.DM dm, DebugInfo.GenTerm a, DebugInfo.GenTerm b) =>
DebugMonad.Func dm a b -> a -> dm b
op_DollarRhombRhomb x0 x1
= hook_op_DollarRhombRhomb x0 x1 (strict_apply x0 x1)
strict_prim_error ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) =>
List dm (Char dm) -> dm a
strict_prim_error x0
= hook_strict_prim_error x0
(DebugMonad.errorHook (Prelude.map charToHChar (listToHList x0)))
strict_failed :: (DebugMonad.DM dm, DebugInfo.GenTerm a) => dm a
strict_failed
= DebugMonad.failedHook
op_EqEq ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) => a -> a -> dm (Bool dm)
op_EqEq x0 x1
= hook_op_EqEq x0 x1 (x0 `eqeq` x1)
eqeq :: (DebugMonad.DM dm, DebugInfo.GenTerm a) => a -> a -> dm (Bool dm)
eqeq x0 x1
| DebugInfo.genTerm x0 Prelude.== DebugInfo.genTerm x1 = Prelude.return True
| Prelude.otherwise = Prelude.return False
strict_prim_ord :: (DebugMonad.DM dm) => Char dm -> dm (Int dm)
strict_prim_ord x0@(Char c)
= hook_strict_prim_ord x0 (Prelude.return (hIntToInt (Char.ord c)))
strict_prim_chr :: (DebugMonad.DM dm) => Int dm -> dm (Char dm)
strict_prim_chr x0
= hook_strict_prim_chr x0 (Prelude.error "not implemented") -- TODO: natToInt
-- = hook_strict_prim_chr x0 (Char $ prim_chr $ natToInt x0)
op_EqEqEq ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) => a -> a -> dm (Bool dm)
op_EqEqEq x0 x1
= hook_op_EqEqEq x0 x1 (x0 `eqeq` x1)
op_And ::
(DebugMonad.DM dm) => Success dm -> Success dm -> dm (Success dm)
op_And x0 x1 = hook_op_And x0 x1 (Prelude.error "not implemented")
-- data IO dm a = IO ((Unit dm) -> (a,(Unit dm)))
op_GtGtEq ::
(DebugMonad.DM dm, DebugInfo.GenTerm a, DebugInfo.GenTerm b) =>
IO dm a -> DebugMonad.Func dm a (IO dm b) -> dm (IO dm b)
op_GtGtEq a k
-- = hook_op_GtGtEq x0 x1 (Prelude.error "not implemented")
= hook_op_GtGtEq a k (IO (\w -> case a w of
(r,w') -> let IO f = k r
in
f w'))
strict_return ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) => a -> dm (IO dm a)
strict_return x
-- = hook_strict_return x (IO dm (FuncRep (\w -> (x,w))))
= hook_strict_return x (IO (\w -> (x,w)))
strict_prim_readFile ::
(DebugMonad.DM dm) =>
List dm (Char dm) -> dm (IO dm (List dm (Char dm)))
strict_prim_readFile x0
= hook_strict_prim_readFile x0 (Prelude.error "not implemented")
-- implementation just returns () representation
strict_prim_writeFile ::
(DebugMonad.DM dm) =>
List dm (Char dm) -> List dm (Char dm) -> dm (IO dm (Unit dm))
strict_prim_writeFile x0 x1
= hook_strict_prim_writeFile x0 x1 (return (IO Unit))
-- implementation just returns () representation
strict_prim_appendFile ::
(DebugMonad.DM dm) =>
List dm (Char dm) -> List dm (Char dm) -> dm (IO dm (Unit dm))
strict_prim_appendFile x0 x1
= hook_strict_prim_appendFile x0 x1 (return (IO Unit))
strict_catchFail ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) =>
IO dm a -> IO dm a -> dm (IO dm a)
strict_catchFail x0 x1
= hook_strict_catchFail x0 x1 (Prelude.error "not implemented")
strict_prim_show ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) =>
a -> dm (List dm (Char dm))
strict_prim_show x0
= hook_strict_prim_show x0 (Prelude.error "not implemented")
strict_getSearchTree ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) =>
a -> dm (IO dm (SearchTree dm a))
strict_getSearchTree x0
= hook_strict_getSearchTree x0 (Prelude.error "not implemented")
strict_apply :: DebugMonad.DM dm => DebugMonad.Func dm a b -> a -> dm b
strict_apply (DebugMonad.FuncRep _ f) x = f x
strict_cond ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) => Success dm -> a -> dm a
strict_cond x0 x1
= hook_strict_cond x0 x1 (Prelude.error "not implemented")
strict_commit ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) => a -> dm a
strict_commit x0
= hook_strict_commit x0 (Prelude.error "not implemented")
op_EqColonLtEq ::
(DebugMonad.DM dm, DebugInfo.GenTerm a) =>
a -> a -> dm (Success dm)
op_EqColonLtEq x0 x1
= hook_op_EqColonLtEq x0 x1 (Prelude.error "not implemented")
{- Auto generated stubs for external functions and types
Remove this comment to suppress warnings. -}
strict_getClockTime ::
(DebugMonad.DM dm) => dm (SPrelude.IO dm (ClockTime dm))
strict_getClockTime
= hook_strict_getClockTime (Prelude.error "not implemented")
strict_prim_toCalendarTime ::
(DebugMonad.DM dm) =>
ClockTime dm -> dm (SPrelude.IO dm (CalendarTime dm))
strict_prim_toCalendarTime x0
= hook_strict_prim_toCalendarTime x0
(Prelude.error "not implemented")
strict_prim_toUTCTime ::
(DebugMonad.DM dm) => ClockTime dm -> dm (CalendarTime dm)
strict_prim_toUTCTime x0
= hook_strict_prim_toUTCTime x0 (Prelude.error "not implemented")
strict_prim_toClockTime ::
(DebugMonad.DM dm) => CalendarTime dm -> dm (ClockTime dm)
strict_prim_toClockTime x0
= hook_strict_prim_toClockTime x0 (Prelude.error "not implemented")
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment