Commit a54cd6d4 authored by Bernd Brassel's avatar Bernd Brassel
Browse files

less dm constraints in debugger

parent a757c015
import qualified Char
instance DI.GenTerm (Float dm) where
instance DI.GenTerm Float where
underscore = FloatUnderscore
genTerm FloatUnderscore = DI.TermUnderscore (DI.SrcID "Prelude" 2)
genTerm (Float f) = DI.TermFloat f
instance DI.GenTerm (Char dm) where
instance DI.GenTerm Char where
underscore = CharUnderscore
genTerm CharUnderscore = DI.TermUnderscore (DI.SrcID "Prelude" 0)
genTerm (Char c) = DI.TermChar c
......@@ -15,46 +15,49 @@ instance DI.GenTerm (IO dm a) where
genTerm IOUnderscore = DI.TermUnderscore (DI.SrcID "Prelude" Prelude.undefined)
genTerm x0 = Prelude.error "not implemented"
natToHInt :: DM.DM dm => Nat dm -> Prelude.Integer
natToHInt :: Nat -> Prelude.Integer
natToHInt IHi = 1
natToHInt (O x) = 2 Prelude.* natToHInt x
natToHInt (I x) = 2 Prelude.* natToHInt x Prelude.+ 1
intToHInt :: DM.DM dm => Int dm -> Prelude.Integer
intToHInt :: Int -> Prelude.Integer
intToHInt (Neg n) = Prelude.negate (natToHInt n)
intToHInt (Pos n) = natToHInt n
intToHInt Zero = 0
hIntToNat :: (DM.DM dm,Prelude.Integral n) => n -> Nat dm
hIntToNat :: Prelude.Integral n => n -> Nat
hIntToNat 1 = IHi
hIntToNat i = case Prelude.divMod i 2 of
(d,0) -> O (hIntToNat d)
(d,1) -> I (hIntToNat d)
hIntToInt :: (DM.DM dm,Prelude.Integral n) => n -> Int dm
hIntToInt :: (Prelude.Integral n) => n -> Int
hIntToInt i | i Prelude.< 0 = Neg (hIntToNat (Prelude.negate i))
| i Prelude.== 0 = Zero
| Prelude.otherwise = Pos (hIntToNat i)
listToHList :: DM.DM dm => List dm a -> [a]
listToHList :: List a -> [a]
listToHList Nil = []
listToHList (Cons x xs) = x:listToHList xs
charToHChar :: DM.DM dm => Char dm -> Prelude.Char
charToHChar :: Char -> Prelude.Char
charToHChar (Char c) = c
data (DM.DM dm) => Float dm = Float Prelude.Float | FloatUnderscore
data Float = Float Prelude.Float | FloatUnderscore deriving (Data.Generics.Typeable, Data.Generics.Data)
data (DM.DM dm) => Char dm = Char Prelude.Char | CharUnderscore
data Char = Char Prelude.Char | CharUnderscore deriving (Data.Generics.Typeable, Data.Generics.Data)
-- data (DM.DM dm) => IO dm a = IO (Prelude.IO a) | IOUnderscore
-- data (DM.DM dm) => IO dm a = IO a | IOUnderscore
-- data IO dm a = IO (World -> (a,World))
-- data IO dm a = IO (DM.Func dm (Unit dm) (a,Unit dm))
-- data (DM.DM dm) => IO a = IO (Prelude.IO a) | IOUnderscore
-- data (DM.DM dm) => IO a = IO a | IOUnderscore
-- data IO a = IO (World -> (a,World))
-- data IO a = IO (DM.Func dm (Unit) (a,Unit))
data World = World
data IO dm a = IO (World -> dm (a,World)) | IOUnderscore
data (DM.DM dm) => IO dm a = IO (World -> dm (a,World)) | IOUnderscore -- (dm :: * -> *)
instance Data.Generics.Typeable (IO dm a)
instance Data.Generics.Data (IO dm a)
return :: DM.DM dm => a -> dm a
return = Prelude.return
......@@ -66,14 +69,14 @@ x ? _ = return x
-- implementation just returns () representation
strict_prim_putChar ::
(DM.DM dm) => Char dm -> dm (IO dm (Unit dm))
(DM.DM dm) => Char -> dm (IO dm (Unit))
strict_prim_putChar x0 = hook_strict_prim_putChar x0 (strict_return Unit)
-- extracts a regular Char from the Virtual I/O information of the oracle
extractChar :: (DM.DM dm) => dm Prelude.Char
extractChar = DM.getNextExtVal
strict_getChar :: (DM.DM dm) => dm (IO dm (Char dm))
strict_getChar :: (DM.DM dm) => dm (IO dm Char)
strict_getChar =
do c <- extractChar
hook_strict_getChar (strict_return (Char c))
......@@ -104,7 +107,7 @@ op_DollarRhombRhomb x0 x1
strict_prim_error ::
(DM.DM dm, DI.GenTerm a) =>
List dm (Char dm) -> dm a
List Char -> dm a
strict_prim_error x0
= hook_strict_prim_error x0
(DM.errorHook (Prelude.map charToHChar (listToHList x0)))
......@@ -116,34 +119,34 @@ strict_failed = return DM.failed
op_EqEq ::
(DM.DM dm, DI.GenTerm a) => a -> a -> dm (Bool dm)
(DM.DM dm, DI.GenTerm a) => a -> a -> dm Bool
op_EqEq x0 x1
= hook_op_EqEq x0 x1 (x0 `eqeq` x1)
eqeq :: (DM.DM dm, DI.GenTerm a) => a -> a -> dm (Bool dm)
eqeq :: (DM.DM dm, DI.GenTerm a) => a -> a -> dm Bool
eqeq x0 x1
| DI.genTerm x0 Prelude.== DI.genTerm x1 = Prelude.return True
| Prelude.otherwise = Prelude.return False
strict_prim_ord :: (DM.DM dm) => Char dm -> dm (Int dm)
strict_prim_ord :: (DM.DM dm) => Char -> dm (Int)
strict_prim_ord x0@(Char c)
= hook_strict_prim_ord x0 (Prelude.return (hIntToInt (Char.ord c)))
strict_prim_chr :: (DM.DM dm) => Int dm -> dm (Char dm)
strict_prim_chr :: (DM.DM dm) => Int -> dm Char
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 ::
(DM.DM dm, DI.GenTerm a) => a -> a -> dm (Bool dm)
(DM.DM dm, DI.GenTerm a) => a -> a -> dm Bool
op_EqEqEq x0 x1
= hook_op_EqEqEq x0 x1 (x0 `eqeq` x1)
op_And ::
(DM.DM dm) => Success dm -> Success dm -> dm (Success dm)
(DM.DM dm) => Success -> Success -> dm Success
op_And x0 x1 = hook_op_And x0 x1 (Prelude.error "not implemented")
-- data IO dm a = IO ((Unit dm) -> (a,(Unit dm)))
-- data IO a = IO ((Unit) -> (a,(Unit)))
op_GtGtEq ::
(DM.DM dm, DI.GenTerm a, DI.GenTerm b) =>
IO dm a -> DM.Func dm a (IO dm b) -> dm (IO dm b)
......@@ -157,26 +160,26 @@ op_GtGtEq a1@(IO a) k
strict_return ::
(DM.DM dm, DI.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 (FuncRep (\w -> (x,w))))
= hook_strict_return x (return (IO (\w -> return (x,w))))
strict_prim_readFile ::
(DM.DM dm) =>
List dm (Char dm) -> dm (IO dm (List dm (Char dm)))
List Char -> dm (IO dm (List Char))
strict_prim_readFile x0
= hook_strict_prim_readFile x0 (Prelude.error "not implemented")
-- implementation just returns () representation
strict_prim_writeFile ::
(DM.DM dm) =>
List dm (Char dm) -> List dm (Char dm) -> dm (IO dm (Unit dm))
List Char -> List Char -> dm (IO dm (Unit))
strict_prim_writeFile x0 x1
= hook_strict_prim_writeFile x0 x1 (strict_return Unit)
-- implementation just returns () representation
strict_prim_appendFile ::
(DM.DM dm) =>
List dm (Char dm) -> List dm (Char dm) -> dm (IO dm (Unit dm))
List Char -> List Char -> dm (IO dm (Unit))
strict_prim_appendFile x0 x1
= hook_strict_prim_appendFile x0 x1 (strict_return Unit)
......@@ -188,13 +191,13 @@ strict_catchFail x0 x1
strict_prim_show ::
(DM.DM dm, DI.GenTerm a) =>
a -> dm (List dm (Char dm))
a -> dm (List Char)
strict_prim_show x0
= hook_strict_prim_show x0 (Prelude.error "not implemented")
strict_getSearchTree ::
(DM.DM dm, DI.GenTerm a) =>
a -> dm (IO dm (SearchTree dm a))
a -> dm (IO dm (SearchTree a))
strict_getSearchTree x0
= hook_strict_getSearchTree x0 (Prelude.error "not implemented")
......@@ -202,7 +205,7 @@ strict_apply :: DM.DM dm => DM.Func dm a b -> a -> dm b
strict_apply (DM.FuncRep _ f) x = f x
strict_cond ::
(DM.DM dm, DI.GenTerm a) => Success dm -> a -> dm a
(DM.DM dm, DI.GenTerm a) => Success -> a -> dm a
strict_cond x0 x1
= hook_strict_cond x0 x1 (Prelude.error "not implemented")
......@@ -213,7 +216,7 @@ strict_commit x0
op_EqColonLtEq ::
(DM.DM dm, DI.GenTerm a) =>
a -> a -> dm (Success dm)
a -> a -> dm Success
op_EqColonLtEq x0 x1
= hook_op_EqColonLtEq x0 x1 (Prelude.error "not implemented")
......@@ -87,7 +87,8 @@ readTerm s = case result of
[(term,tail)]
-> if all isSpace tail then term
else error ("ReadShowTerm.readTerm: no parse, unmatched string after term: "++tail)
[] -> error "ReadShowTerm.readTerm: no parse"
[] -> error $ "ReadShowTerm.readTerm: no parse of string beginning with "
++ take 20 s
_ -> error "ReadShowTerm.readTerm: ambiguous parse"
where result = prim_readsUnqualifiedTerm [] $## s
......
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