Commit 1440f95d authored by Michael Hanus 's avatar Michael Hanus

Interpreter prints computed results immediately in order to deal with infinitely many results

parent f95850db
......@@ -56,6 +56,10 @@ In the following, we describe various uses of the `icurry` tool.
compiled program in a file), invokes the ICurry interpreter
(see `ICurry.Interpreter`), and shows the results of evaluating `mymain`.
With option `--interactive`, the ICurry interpreter stops after
each result and ask for a confirmation to proceed, which is useful
if their might be infinitely many results.
The ICurry interpreter can also visualize the term graph manipulated
during execution as a PDF generated by `dot`. If `icurry` is invoked by
......@@ -64,12 +68,26 @@ In the following, we describe various uses of the `icurry` tool.
the graph after each step is shown by `evince` (see parameter `--viewer`)
and each step is executed in one second.
To see more output information and perform individual steps,
add the option `--interactive`, e.g.,
The option `--interactive` in combination with `--graph` shows more
more details about the state of the interpreter and asks for
a confirmation to proceed after each step of the interpreter:
> icurry -m mymain --graph --interactive Prog
More executions options are available by invoking the interpreter
manually via the operation `ICurry.Interpreter.execProg`.
Some remarks about the ICurry interpreter:
------------------------------------------
The interpreter evaluates expressions up to head normal form.
In order to evaluate the main expression to normal form,
one can wrap it with the function `normalForm`, e.g.,
mymain = normalForm (reverse [1,2,3])
The current version of the interpreter supports only the prelude
operations `normalForm` and `$!`.
----------------------------------------------------------------------------
-- Testing infinitely many results
aBool = False
aBool = True
aBoolList = []
aBoolList = aBool : aBoolList
main = normalForm aBoolList
......@@ -309,51 +309,56 @@ m14 o = execIProg o exampleProg "notBool"
------------------------------------------------------------------------------
-- Testing with CurryCheck.
-- Like evalFun but returns results non-deterministically in order to
-- abstract from the evaluation strategy.
evalFunND :: IProg -> String -> String
evalFunND prog fs = anyOf (evalFun prog fs)
testCoin :: Prop
testCoin = evalFun exampleProg "coin" <~> ("1" ? "2")
testCoin = evalFunND exampleProg "coin" <~> ("1" ? "2")
testHeadEmpty :: Prop
testHeadEmpty = failing (evalFun exampleProg "headempty")
testHeadEmpty = failing (evalFunND exampleProg "headempty")
testHead1 :: Prop
testHead1 = evalFun exampleProg "head1" <~> "1"
testHead1 = evalFunND exampleProg "head1" <~> "1"
testHead12 :: Prop
testHead12 = evalFun exampleProg "head12" <~> ("1" ? "2")
testHead12 = evalFunND exampleProg "head12" <~> ("1" ? "2")
testHeadOneTwo :: Prop
testHeadOneTwo = evalFun exampleProg "headOneTwo" <~> "1"
testHeadOneTwo = evalFunND exampleProg "headOneTwo" <~> "1"
testXorSelfBool :: Prop
testXorSelfBool = evalFun exampleProg "xorSelfBool" <~> "False"
testXorSelfBool = evalFunND exampleProg "xorSelfBool" <~> "False"
testXorSelfDollarBangBool :: Prop
testXorSelfDollarBangBool =
evalFun exampleProg "xorSelfDollarBangBool" <~> "False"
evalFunND exampleProg "xorSelfDollarBangBool" <~> "False"
testXorSelfSeqBool :: Prop
testXorSelfSeqBool = evalFun exampleProg "xorSelfSeqBool" <~> "False"
testXorSelfSeqBool = evalFunND exampleProg "xorSelfSeqBool" <~> "False"
testAndNotFalse :: Prop
testAndNotFalse = evalFun exampleProg "andNotFalse" <~> "True"
testAndNotFalse = evalFunND exampleProg "andNotFalse" <~> "True"
testNotBool :: Prop
testNotBool = evalFun exampleProg "notBool" <~> ("True" ? "False")
testNotBool = evalFunND exampleProg "notBool" <~> ("True" ? "False")
testIdTrue :: Prop
testIdTrue = evalFun exampleProg "idTrue" <~> "True"
testIdTrue = evalFunND exampleProg "idTrue" <~> "True"
testCoinList :: Prop
testCoinList = evalFun exampleProg "coinList" <~> ("(: 1 [])" ? "(: 2 [])")
testCoinList = evalFunND exampleProg "coinList" <~> ("(: 1 [])" ? "(: 2 [])")
testCoinCoinList :: Prop
testCoinCoinList =
evalFun exampleProg "coinCoinList" <~>
evalFunND exampleProg "coinCoinList" <~>
("(: 1 (: 1 []))" ? "(: 2 (: 1 []))" ? "(: 1 (: 2 []))" ? "(: 2 (: 2 []))")
testPerm123 :: Prop
testPerm123 =
evalFun exampleProg "perm123" <~>
evalFunND exampleProg "perm123" <~>
("(: 1 (: 2 (: 3 [])))" ? "(: 1 (: 3 (: 2 [])))" ? "(: 2 (: 1 (: 3 [])))" ?
"(: 2 (: 3 (: 1 [])))" ? "(: 3 (: 1 (: 2 [])))" ? "(: 3 (: 2 (: 1 [])))")
......
......@@ -10,7 +10,7 @@
module ICurry.Interpreter
where
import List ( init, last, replace )
import List ( init, isPrefixOf, last, replace )
import System ( sleep, system )
import ICurry.Types
......@@ -77,16 +77,20 @@ currentNodeOfTask (Task (CNode nid) _ _) = nid
currentNodeOfTask (Task (IBlockEnv _ env) _ _) = lookupInEnv 0 env
------------------------------------------------------------------------------
-- The state of an ICurry program under evaluation.
-- The state of an ICurry program under evaluation as described in the
-- WFLP'19 paper.
-- The auxiliary component `currResult` is set in a step when a new result
-- has been computed.
data State = State { program :: [IFunction]
, graph :: Graph
, tasks :: [Task]
, results :: [NodeID]
, currResult :: Maybe NodeID
}
-- Initial state for a program, graph, and root node id.
initState :: [IFunction] -> Graph -> NodeID -> State
initState prog graph nid = State prog graph [Task (CNode nid) [] []] []
initState prog graph nid = State prog graph [Task (CNode nid) [] []] [] Nothing
-- Returns the root nodes of all results and all expressions.
rootsOfState :: State -> [NodeID]
......@@ -96,6 +100,10 @@ rootsOfState st = results st ++ map rootOfTask (tasks st)
showResults :: State -> String
showResults st = unlines (map (showGraphExp (graph st)) (results st))
-- Adds a result to a program state.
addResult :: NodeID -> State -> State
addResult nid st = st { results = results st ++ [nid], currResult = Just nid }
-- Print the current state of the interpreter according to the given options.
printState :: IOptions -> State -> IO ()
printState opts st = do
......@@ -116,10 +124,7 @@ printState opts st = do
, "FINGER PRINT: " ++ show fp ]
else []
when (withGraph opts || makePDF opts) $ showStateGraph
if interactive opts
then putStr "Type <RET> to proceed: " >> getLine >> done
else when (waitTime opts > 0) (sleep (waitTime opts))
when (waitTime opts > 0 && not (interactive opts)) $ sleep (waitTime opts)
when (verb>0) $ putStrLn ""
where
verb = verbosity opts
......@@ -158,6 +163,18 @@ The following coloring is used in the graph:
-}
askProceed :: IOptions -> IO Bool
askProceed opts =
if interactive opts
then do putStr "Proceed (<RET>) or abort (a)? "
ans <- getLine
if null ans
then return True
else if ans `isPrefixOf` "abort"
then putStrLn "Execution aborted!" >> return False
else askProceed opts
else return True
------------------------------------------------------------------------------
-- An interpreter for a single Curry program based on translating
-- them into ICurry.
......@@ -196,26 +213,41 @@ runWith :: IOptions -> State -> IO IOptions
runWith opts st
| null (tasks st)
= do printState opts st
putStr $ "RESULTS:\n" ++ showResults st
return opts
| otherwise
= do printState opts st
let num = stepNum opts
nopts = if num==0 then opts else opts { stepNum = num + 1 }
runWith nopts (step st)
-- Evaluates a 0-ary function w.r.t. an ICurry program and return any result
-- formatted as a string.
procstep <- if verbosity opts > 0 then askProceed opts else return True
if not procstep
then return opts
else do
let num = stepNum opts
nopts = if num==0 then opts else opts { stepNum = num + 1 }
nst = step st
maybe (runWith nopts nst)
(\nid -> do putStrLn $ "RESULT: " ++
showGraphExp (graph nst) nid
proceed <- askProceed opts
if proceed
then runWith nopts nst {currResult = Nothing}
else return opts)
(currResult nst)
-- Evaluates a 0-ary function w.r.t. an ICurry program and returns
-- the list of all results formatted as strings.
-- Used for testing.
evalFun :: IProg -> String -> String
evalFun :: IProg -> String -> [String]
evalFun (IProg _ _ _ ifuns) f =
let (g,ni) = addNode (FuncNode f []) emptyGraph
final = evaluate (initState ifuns g ni)
in anyOf (map (showGraphExp (graph final)) (results final))
in evaluate (initState ifuns g ni)
where
evaluate st
| null (tasks st) = st
| otherwise = evaluate (step st)
| null (tasks st) = []
| otherwise
= let st' = step st
in maybe (evaluate st')
(\nid -> showGraphExp (graph st') nid :
evaluate st' {currResult = Nothing})
(currResult st')
------------------------------------------------------------------------------
-- Implementation of the small-step semantics.
......@@ -230,14 +262,14 @@ evalFirstTask _ [] = error "step: empty tasks"
evalFirstTask st (Task (CNode nid) stk fp : tsks) =
case lookupNode nid (graph st) of
ConsNode _ _ -> case stk of
[] -> st { tasks = tsks, results = results st ++ [nid] }
[] -> addResult nid (st { tasks = tsks })
((fnid,_) : rstk) ->
let st1 = st { tasks = Task (CNode fnid) rstk fp : tsks }
in invokeFunction st1 (tasks st1)
-- partial calls are treated as constructors:
PartNode _ _ _ -> case stk of
[] -> st { tasks = tsks, results = results st ++ [nid] }
[] -> addResult nid (st { tasks = tsks })
((fnid,_) : rstk) ->
let st1 = st { tasks = Task (CNode fnid) rstk fp : tsks }
in invokeFunction st1 (tasks st1)
......
......@@ -50,7 +50,9 @@ mainProg opts p = do
, withViewer = optViewPDF opts }
else defOpts
opts2 = if optInteractive opts
then opts1 { interactive = True, verbosity = 2 }
then if optShowGraph opts
then opts1 { interactive = True, verbosity = 2 }
else opts1 { interactive = True }
else opts1
execIProg opts2 iprog imain
......@@ -95,7 +97,7 @@ options =
"command to view PDF files (default: 'evince')"
, Option "i" ["interactive"]
(NoArg (\opts -> opts { optInteractive = True }))
"interactive execution (wait after each step)"
"interactive execution (ask after each result or step)"
]
where
safeReadNat opttrans s opts =
......
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