Skip to content

GitLab

Commit dc2ef5b8 authored by bbr's avatar bbr
Browse files

intermediate state

parent 0f64bbbe
Hide whitespace changes
Inline Side-by-side
src/lib/All_Libraries.curry
View file @ dc2ef5b8
......@@ -38,7 +38,7 @@ module All_Libraries (
module Array,
module Dequeue,
module FiniteMap,
module GraphInductive,
--module GraphInductive,
--module IArray,
module Random,
module RedBlackTree,
......@@ -74,12 +74,12 @@ module All_Libraries (
module FlatCurryTools,
--module FlatCurryXML,
module FlexRigid,
module Generic,
--module Generic,
module Meta,
--internal libraries
module Interactive,
module Oracle) where
module Oracle, test) where
--import AllSolutions
......@@ -119,7 +119,7 @@ import Unsafe(trace)
import Array hiding ((!))
import Dequeue
import FiniteMap
import GraphInductive(Graph)
--import GraphInductive(Graph)
--import IArray ((!))
import Random
import RedBlackTree(RedBlackTree)
......@@ -154,8 +154,10 @@ import FlatCurryShow hiding (showCurryId)
import FlatCurryTools(showCurryId)
--import FlatCurryXML
import FlexRigid
import Generic
--import Generic
import Meta hiding (isFree)
import Interactive
import Oracle
\ No newline at end of file
import Oracle
test = putStrLn "okay"
\ No newline at end of file
src/oracle/PrettyStrict.curry
View file @ dc2ef5b8
......@@ -88,7 +88,9 @@ identifier' b fun n
| otherwise = consname (snd (consId n))
funId :: QName -> QName
funId (m,n) = (m,toLower (head n) : tail n)
funId mn@(m,n@(h:_))
| isUpper h = (m,'_':n)
| otherwise = mn
consId :: QName -> QName
consId (m,n) = (m,toUpper (head n) : tail n)
......
src/oracle/StrictSteps.hs
View file @ dc2ef5b8
......@@ -15,19 +15,21 @@ module StrictSteps (
addReadFile,addWrittenFile,addAppendedFile,
getNextExtVal,
pc1,pc2,pc3,pc4,pc5,pc6,pc7,pc8,pc9,pc10,pc11
module PartCalls
) where
import Prelude hiding (catch,interact)
import System.IO.Unsafe
import DebuggerMonad
import Control.Monad.Error
import Control.Monad.State
import Data.IORef
import System.IO hiding (interact)
import System.IO.Unsafe
import Control.Exception
import System.Process
import Term
import Data.IORef
import System.Process
import PartCalls
hello= " ____ ____ _____ \n\
\( _ \\ (_ _) ( _ ) Believe\n\
......@@ -35,164 +37,6 @@ hello= " ____ ____ _____ \n\
\(____/()(____)()(_____)() Oracles\n\
\--------type ? for help----------"
---------------------------------------------------------
-- BoolStack - a List of boolean values is efficiently
-- coded as a list of Integers (arbitrary size).
-- Assumption is that there will not be many Falses in
-- sequence.
-- If this assumption is wrong, we could alternatively
-- change to no. of Trues,no. of False, no of Trues...
-- Another alternativ could be a fraction of which
-- the slist is the representation as a fractional chain,
-- cf. jan christiansen.
-- Nice for these alternatives: keep implementation
-- abstract by push/pop/empty.
-----------------------------------------------------------
type BoolStack = [Integer]
emptyBoolStack :: BoolStack
emptyBoolStack = [0]
--- implementation of push/pop
--- makes sure that this is an infinite list of Trues:
allTrue :: BoolStack
allTrue = []
--- popping from a BoolStack
pop :: BoolStack -> (BoolStack, Bool)
pop [] = ([],True)
pop [0] = error "pop: Stack underflow"
pop (0:os) = (os, False)
pop (n:os) = (n-1 : os, True)
--- pushing to a BoolStack
push :: BoolStack -> Bool -> BoolStack
push [] True = []
push (b:bs) True = b+1 : bs
push bs False = 0 : bs
-----------------------------------------------------------
-- Term - Representation of observable data
-- (from module Term)
--
-- ShowTerm - Class to obtain Term representation
----------------------------------------------------------- -}
-- consTerm, consUnderscore - werden anstelle der
-- Konstruktoren exportiert (good for what?)
consTerm :: String -> [Term] -> Term
consTerm = Term
consUnderscore :: Term
consUnderscore = Underscore
consFailed :: String -> Term
consFailed = Fail
instance Show Term where
show t = showsTerm t ""
-- The class to obtain Term representation.
-- showCons is monadic in order to
-- catch the underscore exception.
class (Show a,Eq a) => ShowTerm a where
showCons :: a -> Debug Term
showCons x = return (Term (show x) [])
underscore :: a
underscore = throw NonTermination
failure :: String -> a
failure s = throw (ErrorCall s)
showTerm :: ShowTerm a => a -> Debug Term
showTerm x =
liftIO (catch (x `seq` return Nothing) (return . Just)) >>=
maybe (showCons x)
(\ e -> case e of
NonTermination -> return Underscore
ErrorCall s -> return (Fail s))
($$) :: ShowTerm a => Debug [Term] -> a -> Debug [Term]
getxs $$ x = do
xs <- getxs
x <- showTerm x
return (x:xs)
---------------------------------------------------------
-- Debugstate - the intrnal state of the debugger
---------------------------------------------------------
-- The Orakel is a list of boolean values encoded as a
-- BoolStack.
type Oracle = BoolStack
-- Display mode of the debugger
data DisplayMode = DisplayMode
{ verbose :: Bool, -- verbose status information
optionalResult:: Bool, -- do not inspect results
depth :: Maybe Int -- show terms up to certain depth
}
-- The working modes of the debugger:
--
-- The debugger is either interactive, asking the user
-- for his opinion of the next step or silent.
-- In silent mode there are two kinds of information:
-- a) are we in the main thread or do we inspect a result
-- b) is the current subcomputation correct or yet unrated
--
-- The combinations mean:
--
-- Main+Unrated
-- the user skipped. We may perform io in this subcomputation.
-- Old ratings are kept.
-- Main+Correct
-- the user decided the current sub computation to be correct.
-- We may perform io.
-- Inspect+Skipped
-- The user wants to know a result of a currently future
-- subcomputation. Old ratings are kept. No io.
-- Inspect+Unrated
-- The user wants to know a result of a currently future
-- subcomputation. No io.
data StepMode = StepInteractive
| StepSilent Bool Bool
-- the internal state of the debugger
data DebugState = DebugState {
stepmode :: StepMode, -- several debug modes, see below
oracle :: Oracle, -- the current oracle
displayMode :: IORef DisplayMode, -- why is this an ioref?
past, future :: BoolStack, -- Both stacks:
-- True: no rating yet, False rated.
-- past: computation up to current point
-- future: remaining computation
gui :: Maybe (Handle,ProcessHandle),
-- our link to the biotope
extValues :: [String] -- the values from external io functions
}
------------------------------------------
......@@ -233,51 +77,6 @@ shift = do
past = push (past state) entry}
return entry
-- a BugReport is the left hand side + result
data BugReport = BugReport
{ lhs :: Term,
rhs :: Term }
-- BugReport is treated as an error in the error monad
instance Error (Maybe a) where
noMsg = Nothing
{-
Ein Berechnungsschritt ordnet einem Debugger-Zustand
entweder den Nachfolgezustand und das Ergebnis der
Auswertung oder den bei der interaktiven
Auswertung gefundenen Bug zu.
Bei der Berechnung werden
- Orakeleinträge konsumiert,
- eventuell das verbose-Flag geändert,
- Einträge zu past hinzugefügt und
- Einträge von future konsumiert
-}
type Debug a = StateT DebugState (ErrorT (Maybe BugReport) IO) a
{- ---------------------------------------------------------
Debugger - Monade
Kombiniert das Debugging von Argument und Funktion zu
einem Berechnungsschritt.
- Das Orakel steuert, ob das Argument ausgewertet oder
durch den Platzhalter underscore ersetzt wird.
- wenn im Argument ein Bug gefunden wurde, wird die
Auswertung abgebrochen
--------------------------------------------------------- -}
eval :: ShowTerm a => Debug a -> Debug a
eval act = do
state <- get
......@@ -552,27 +351,9 @@ showResult result = do
liftIO $ putStr (" ~> " ++ show r)
type IO' a = Prim (Debug a)
---------------------------------------------------------------
-- representation of external data types
---------------------------------------------------------------
data Prim a = Prim Term a | PrimUnderscore | PrimFailed String
instance ShowTerm (Prim a) where
showCons PrimUnderscore = return consUnderscore
showCons (PrimFailed s) = return (consFailed s)
showCons (Prim a _) = return a
instance Eq (Prim a) where
Prim x _ == Prim y _ = x Prelude.== y
instance Show (Prim a) where
show (Prim a _) = show a
type IO' a = Prim (Debug a)
type DebugPrim a = Debug (Prim a)
---------------------------------------------------------------
-- saved values of external functions and their representation
......@@ -653,266 +434,3 @@ getNextExtVal = do
put (st{extValues=tail vals})
return (read (head vals))
------------------------------------------------------------
-- very bad thing but there seems to be no more elegant way
------------------------------------------------------------
pc1 :: Term -> (a -> Debug res) -> Prim (a -> Debug res)
pc1 (Term n xs) f = Prim (Term n []) f
pc2 :: ShowTerm a => Term -> (a -> b -> Debug res) -> Prim (a -> DebugPrim (b -> Debug res))
pc2 (Term n xs) f =
Prim (c []) (\ x -> do
sx <- showTerm x
return (Prim (c [sx]) (f x))
)
where
c = Term n . (xs++)
pc3 :: (ShowTerm a,ShowTerm b) =>
Term -> (a -> b -> c -> Debug res) ->
Prim (a -> DebugPrim (b -> DebugPrim (c -> Debug res)))
pc3 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 ->
f x1 x2 x3)))))
where
c = Term n . (xs++)
pc4 :: (ShowTerm a,ShowTerm b,ShowTerm c) =>
Term -> (a -> b -> c -> d -> Debug res) ->
Prim (a -> DebugPrim (b -> DebugPrim (c -> DebugPrim (d -> Debug res))))
pc4 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 ->
f x1 x2 x3 x4)))))))
where
c = Term n . (xs++)
pc5 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d) =>
Term -> (a -> b -> c -> d -> e -> Debug res) ->
Prim (a -> DebugPrim (b -> DebugPrim (c -> DebugPrim (d -> DebugPrim (e -> Debug res)))))
pc5 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 ->
f x1 x2 x3 x4 x5)))))))))
where
c = Term n . (xs++)
pc6 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e) =>
Term -> (a -> b -> c -> d -> e -> f -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f -> Debug res))))))
pc6 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 ->
f x1 x2 x3 x4 x5 x6)))))))))))
where
c = Term n . (xs++)
pc7 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e,ShowTerm f) =>
Term -> (a -> b -> c -> d -> e -> f -> g -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f ->
DebugPrim (g ->
Debug res)))))))
pc7 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 -> do
sx6 <- showTerm x6
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6]) (\ x7 ->
f x1 x2 x3 x4 x5 x6 x7)))))))))))))
where
c = Term n . (xs++)
pc8 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e,ShowTerm f,ShowTerm g) =>
Term -> (a -> b -> c -> d -> e -> f -> g -> h -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f ->
DebugPrim (g ->
DebugPrim (h ->
Debug res))))))))
pc8 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 -> do
sx6 <- showTerm x6
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6]) (\ x7 -> do
sx7 <- showTerm x7
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7]) (\ x8 ->
f x1 x2 x3 x4 x5 x6 x7 x8)))))))))))))))
where
c = Term n . (xs++)
pc9 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e,ShowTerm f,
ShowTerm g,ShowTerm h) =>
Term -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f ->
DebugPrim (g ->
DebugPrim (h ->
DebugPrim (i ->
Debug res)))))))))
pc9 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 -> do
sx6 <- showTerm x6
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6]) (\ x7 -> do
sx7 <- showTerm x7
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7]) (\ x8 -> do
sx8 <- showTerm x8
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8]) (\ x9 ->
f x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))))))))))
where
c = Term n . (xs++)
pc10 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e,ShowTerm f,
ShowTerm g,ShowTerm h,ShowTerm i) =>
Term -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f ->
DebugPrim (g ->
DebugPrim (h ->
DebugPrim (i ->
DebugPrim (j ->
Debug res))))))))))
pc10 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 -> do
sx6 <- showTerm x6
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6]) (\ x7 -> do
sx7 <- showTerm x7
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7]) (\ x8 -> do
sx8 <- showTerm x8
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8]) (\ x9 -> do
sx9 <- showTerm x9
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8,sx9]) (\ x10 ->
f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)))))))))))))))))))
where
c = Term n . (xs++)
pc11 :: (ShowTerm a,ShowTerm b,ShowTerm c,ShowTerm d,ShowTerm e,ShowTerm f,
ShowTerm g,ShowTerm h,ShowTerm i,ShowTerm j) =>
Term -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> Debug res) ->
Prim (a ->
DebugPrim (b ->
DebugPrim (c ->
DebugPrim (d ->
DebugPrim (e ->
DebugPrim (f ->
DebugPrim (g ->
DebugPrim (h ->
DebugPrim (i ->
DebugPrim (j ->
DebugPrim (k ->
Debug res)))))))))))
pc11 (Term n xs) f =
Prim (c []) (\ x1 -> do
sx1 <- showTerm x1
return (Prim (c [sx1]) (\ x2 -> do
sx2 <- showTerm x2
return (Prim (c [sx1,sx2]) (\ x3 -> do
sx3 <- showTerm x3
return (Prim (c [sx1,sx2,sx3]) (\ x4 -> do
sx4 <- showTerm x4
return (Prim (c [sx1,sx2,sx3,sx4]) (\ x5 -> do
sx5 <- showTerm x5
return (Prim (c [sx1,sx2,sx3,sx4,sx5]) (\ x6 -> do
sx6 <- showTerm x6
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6]) (\ x7 -> do
sx7 <- showTerm x7
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7]) (\ x8 -> do
sx8 <- showTerm x8
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8]) (\ x9 -> do
sx9 <- showTerm x9
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8,sx9]) (\ x10 -> do
sx10 <- showTerm x10
return (Prim (c [sx1,sx2,sx3,sx4,sx5,sx6,sx7,sx8,sx9,sx10]) (\ x11 ->
f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)))))))))))))))))))))
where
c = Term n . (xs++)
src/oracle/Transform.curry
View file @ dc2ef5b8
......@@ -15,6 +15,7 @@ import FlatCurryGoodies
import Wrapper
import Make
import ReadShowTerm
applyFuncs = ("Meta","headNormalFormIO") :
......@@ -44,8 +45,11 @@ transform force _ mod = make mod tester writeTrans
where
tester = if force then (\ fn _ -> readTypes fn >>= return . Just)
else obsolete addFcy (addFcy . addOrc) readTypes
readTypes fn = readFlatCurryFile fn >>=
return . filter hasHOTypeArg . progTypes