Commit 06e07e81 authored by bbr's avatar bbr
Browse files

unification seems functionable now

parent 23c521c1
......@@ -4,6 +4,8 @@ import Store
import Data.IORef
import System.IO.Unsafe
trace' s x = unsafePerformIO (putStrLn s >> return x)
-- On the top level io monad of each program we manage a store.
-- Because there is unsafe io and because some operations on
-- stores start out without one, a state might be without store.
......@@ -94,27 +96,28 @@ bind v val res = unsafePerformIO $ do
-- This function controls all kinds of evaluations to (head) normal forms
-- IMPORTANT: if you change anything here, also update ExternalPrelude.prim_do
ctcStore :: (BaseCurry a,BaseCurry b) => HNFMode -> (a -> Result b) -> a -> Result b
ctcStore mode cont x state =
ctcStore mode cont x state = --trace' "ctc" $
case consKind x of
-- cases solvable without store
Val -> cont x state
Failed -> addException
(curryError ("Prelude."++if mode then "$#" else "$!"))
x
Failed -> addException err x
Branching -> let ref = orRef x
bs = branches x
in case state of
Nothing -> if mode || not (isGenerator ref)
Nothing -> error "nostore" $ if mode || not (isGenerator ref)
then mapOr (ctcStore mode cont) ref bs state
else cont x state
Just store -> case fromStore store ref of
Nothing -> if mode || not (isGenerator ref)
then branching (narrowOrRef ref)
(zipWith (ctcBranch contCTC ref store)
[0..] bs)
else cont x state
Just i -> ctcStore mode cont (bs!!i) state
NoBinding i -> if mode || not (isGenerator ref)
then branching (narrowOrRef ref)
(zipWith (ctcBranch contCTC ref store)
[0..] bs)
else cont (branching (mkRef i) bs) state
Found i -> ctcStore mode cont (bs!!i) state
Redirect to from -> branching ref
[maybe (failed err)
(ctcStore mode cont (head bs) . Just)
(chainInStore store to from)]
Free -> let ref = freeVarRef x in
case binding x of
Left x' -> if mode
......@@ -132,6 +135,7 @@ ctcStore mode cont x state =
where
contCTC x st = ctcStore mode cont x (Just st)
susp = ctcStore mode cont
err = curryError ("Prelude."++if mode then "$#" else "$!")
{-
-- It can happen that computations suspend twice in a row, e.g.:
......@@ -201,17 +205,20 @@ fetchState cont = suspend True (cont . Just)
ctcBranch :: (BaseCurry a, BaseCurry b) =>
(b -> Result' a) -> OrRef -> Store -> Int -> b -> a
ctcBranch cont orRef store nr x =
let newStore = addToStore store orRef nr in
cont x newStore
maybe (failed (curryError "ctcBranch")) (cont x) (addToStore store orRef nr)
-- pull continuations into branches without modifying a store
-- TODO: add right number to state!
mapOr :: (BaseCurry a,BaseCurry b) => (a -> Result b) -> OrRef -> Branches a -> Result b
mapOr f ref bs Nothing = mapOr f ref bs (Just emptyStore)
mapOr f ref bs st@(Just store) = case fromStore store ref of
Nothing -> branching (narrowOrRef ref)
(zipWith (ctcBranch (\ x st -> f x (Just st)) ref store) [0..] bs)
Just i -> f (bs!!i) st
mapOr f ref bs st@(Just store) = trace' "mapOr" $ case fromStore store ref of
NoBinding _ -> branching (narrowOrRef ref)
(zipWith (ctcBranch (\ x st -> f x (Just st)) ref store) [0..] bs)
Found i -> f (bs!!i) st
Redirect i j -> branching ref
[maybe (failed (curryError "mapOr"))
(f (head bs) . Just)
(chainInStore store i j)]
addException :: (BaseCurry a,BaseCurry b) => Exception -> a -> b
addException _ x = failed (exceptions x)
......
......@@ -63,7 +63,7 @@ freeIORef x = freeVar (nextFreeRef x)
-- the global state of references
storeRefCounter :: IORef (Int,Int)
storeRefCounter = unsafePerformIO (newIORef (0,0))
storeRefCounter = unsafePerformIO (newIORef (1,1))
-- generate a new reference
nextRef :: Bool -> OrRefKind -> OrRef
......@@ -137,7 +137,7 @@ freeCTC :: (BaseCurry b, BaseCurry a) => (b -> a) -> a
freeCTC f = let x=freeIORef () in f x
orCTC :: BaseCurry a => a -> a -> a
orCTC x y = branching (nextOrRef Other) [x,y]
orCTC x y = branching (nextOrRef Narrowed) [x,y]
orBased :: RunTimeOptions
orBased = withFree {freeFunc = freeOrBased}
......
module Store
(Store,
module Store
(Store,
emptyStore,addToStore,fromStore, storeSize,
emptyStore,addToStore,fromStore, storeSize,chainInStore,
trace,vtrace,vtrace',
OrRef,OrRefKind(Generator,Other),
OrRef,OrRefKind(..),FromStore(..),
deref,cover,uncover,mkRef,isCovered,
mkRefWithGenInfo, isGenerator, chainedTo, chainTo,
......@@ -17,19 +16,22 @@ import Data.IntMap
import Prelude hiding (lookup)
import System.IO.Unsafe
trace s x = unsafePerformIO (putStrLn s >> return x)
----------------------------
-- or references
----------------------------
data OrRefKind = Generator | Chain Int | Other
data OrRefKind = Generator | Narrowed
deriving (Eq,Show,Read)
data OrRef = OrRef OrRefKind Int
| Layer OrRef deriving (Eq,Show,Read)
| Layer OrRef
| Chain Int Int deriving (Eq,Show,Read)
uncover :: OrRef -> OrRef
uncover x@(OrRef _ _) = x
uncover (Layer x) = x
uncover x = x
-- constructors
cover :: OrRef -> OrRef
......@@ -43,62 +45,47 @@ mkRefWithGenInfo = OrRef
-- selectors
deref :: OrRef -> Int
deref r = (\ (OrRef _ x) -> x) (uncover r)
deref r = case uncover r of
OrRef _ i -> i
Chain i j -> i
refKind :: OrRef -> OrRefKind
refKind r = (\ (OrRef x _) -> x) (uncover r)
--refKind :: OrRef -> OrRefKind
--refKind r = (\ (OrRef x _) -> x) (uncover r)
-- tester
isCovered :: OrRef -> Bool
isCovered (OrRef _ _) = False
isCovered (Layer _) = True
isCovered _ = False
isGenerator :: OrRef -> Bool
isGenerator o = case refKind o of
Generator -> True
_ -> False
isGenerator r = case uncover r of
OrRef Generator _ -> True
_ -> False
isOther :: OrRef -> Bool
isOther o = case refKind o of
Other -> True
_ -> False
isNarrowed :: OrRef -> Bool
isNarrowed r = case uncover r of
OrRef Narrowed _ -> True
_ -> False
chainedTo :: OrRef -> Maybe Int
chainedTo o = case refKind o of
Chain i -> Just i
_ -> Nothing
chainedTo :: OrRef -> Maybe (Int,Int)
chainedTo r = case uncover r of
Chain i j -> Just (i,j)
_ -> Nothing
--operations
updKind :: (OrRefKind -> OrRefKind) -> OrRef -> OrRef
updKind f (Layer r) = Layer (updKind f r)
updKind f (OrRef k i) = OrRef (f k) i
updKind f (Chain i j) = Chain i j
narrowOrRef :: OrRef -> OrRef
narrowOrRef = updKind narrow
where narrow o@Other = o
narrow o@(Chain _) = o
narrow Generator = Other
chainTo :: OrRef -> Int -> OrRef
chainTo r v = updKind chain r
where
chain Generator = Chain v
chain _ = error "Store.chainTo applied to unexpected argument"
----------------------------------
-- tracing
----------------------------------
where narrow o@Narrowed = o
narrow Generator = Narrowed
--trace s x = unsafePerformIO (putStrLn s >> return x)
trace _ x = x
-- sometimes you want to see values
vtrace x = x
--vtrace x = trace (show x) x
--vtrace' = trace
vtrace' _ x = x
chainTo :: Int -> Int -> OrRef
chainTo = Chain
-------------------------------------------------------
-- finally: the store
......@@ -111,24 +98,55 @@ newtype Store = Store (IntMap Int) deriving (Show)
emptyStore :: Store
emptyStore = Store empty
addToStore :: Store -> OrRef -> Int -> Store
addToStore (Store st) r i = Store (add st (deref r) i)
where
add store ref choice =
case insertLookupWithKey (\ _ new _ -> new) ref i st of
(Nothing, newStore) -> newStore
(Just ref',newStore) -> add newStore (-ref') choice
fromStore :: Store -> OrRef -> Maybe Int
fromStore (Store store) r = from (deref r)
addToStore :: Store -> OrRef -> Int -> Maybe Store
addToStore st r i = trace (show (st,r,i)) $
case uncover r of
OrRef _ r' -> let st' = insertAndCutChains r' i st
in trace (show st') st'
_ -> error "add applied to bad arguments"
data FromStore = NoBinding Int
| Found Int
| Redirect Int Int deriving Show
fromStore :: Store -> OrRef -> FromStore
fromStore st@(Store store) r = trace (show (r,store)) $ case uncover r of
OrRef _ i -> let r=from i in trace (show r) r
Chain i j -> trace (show (i,j)) Redirect i j
where
from ref = maybe Nothing follow (lookup ref store)
from ref = maybe (NoBinding ref) follow (lookup ref store)
follow i | i<0 = from (negate i)
| otherwise = Just i
| otherwise = Found i
chainInStore :: Store -> Int -> Int -> Maybe Store
chainInStore st@(Store store) from to = trace "chain" $
case lookupAndCutChains to st of
Nothing -> insertAndCutChains from (negate to) st
Just (b,newSt) -> insertAndCutChains from b newSt
lookupAndCutChains :: Int -> Store -> Maybe (Int,Store)
lookupAndCutChains i st@(Store store) = case lookup i store of
Nothing -> Nothing
Just j -> if j<0
then case lookupAndCutChains (negate j) st of
Nothing -> Just (j,st)
Just (j',Store store') -> Just (j',Store (insert i j' store'))
else Just (j,st)
insertAndCutChains :: Int -> Int -> Store -> Maybe Store
insertAndCutChains key val st@(Store store) =
case insertLookupWithKey (\ _ new _ -> new) key val store of
(Nothing,newStore) -> Just (Store newStore)
(Just b,newStore) -> if b==val
then Just st
else if b<0
then insertAndCutChains (negate b) val (Store newStore)
else if val>0
then Nothing
else Just (Store (insert (negate val) b store))
chainInStore :: Store -> OrRef -> OrRef -> Store
chainInStore (Store st) from to =
Store (insert (deref from) (negate (deref to)) st)
storeSize :: Store -> Int
storeSize (Store st) = size st
\ No newline at end of file
module ExternalFunctionsMeta where
import Curry hiding ( trace )
import Curry
import CurryPrelude hiding ( (==) , return , (>>=))
import CurryArray
import InstancesMeta
......
......@@ -33,8 +33,11 @@ ioStart :: Curry a => Store -> C_IO a -> IO a
ioStart st (C_IO act) = act (Just st) Prelude.>>= curryDo st
ioStart _ (C_IOFail es) = printExceptions es
ioStart st (C_IOOr ref bs) = case fromStore st ref of
Nothing -> searchValC_IO [] (zipWith (mkChoice st ref) [0..] bs)
Just i -> ioStart st (bs !! i)
NoBinding _ -> searchValC_IO [] (zipWith (mkChoice st ref) [0..] bs)
Found i -> ioStart st (bs !! i)
Redirect i j -> maybe (printExceptions (curryError "ioStart"))
(\st -> ioStart st (head bs))
(chainInStore st i j)
ioStart st (C_IOSusp _ contRef) = do
cont <- readIORef contRef
case cont () of
......@@ -45,16 +48,21 @@ curryDo :: Curry a => Store -> IOVal a -> IO a
curryDo _ (IOVal x) = Prelude.return x
curryDo _ (IOValFail es) = printExceptions es
curryDo st (IOValOr ref bs) = case fromStore st ref of
Nothing -> searchIOVal [] (zipWith (mkChoice st ref) [0..] bs)
Just i -> (bs !! i) Prelude.>>= curryDo st
NoBinding _ -> searchIOVal [] (zipWith (mkChoice st ref) [0..] bs)
Found i -> (bs !! i) Prelude.>>= curryDo st
Redirect i j -> maybe (printExceptions (curryError "curryDo"))
(\ st -> head bs Prelude.>>= curryDo st)
(chainInStore st i j)
curryDo st (IOValSusp _ cont) = do
mVal <- cont
case mVal of
Nothing -> error "top io action is suspension"
Just v -> curryDo st v
mkChoice :: Store -> OrRef -> Int -> a -> (Store,a)
mkChoice st ref i x = (addToStore st ref i,x)
mkChoice :: BaseCurry a => Store -> OrRef -> Int -> a -> (Store,a)
mkChoice st ref i x = maybe (st,Curry.failed $ curryError "mkChoice")
(\st -> (st,x))
(addToStore st ref i)
searchValC_IO :: Curry a => [C_Exceptions] -> [(Store,C_IO a)] -> IO a
searchValC_IO es [] =
......@@ -89,11 +97,6 @@ searchIOVal es ((st,act) : stacts) = do
Nothing -> searchIOVal es stacts
Just v -> searchIOVal es ((st,Prelude.return v) : stacts)
firstVal :: (Store -> a -> b) -> Store -> OrRef -> Branches a -> b
firstVal cont store ref bs = case fromStore store ref of
Nothing -> searchVal cont store ref bs
Just i -> searchVal cont store ref [trace "firstVal" (bs !! i)]
-- this is the place to change for implicit breadth first search
searchVal :: (Store -> a -> b) -> Store -> OrRef -> Branches a -> b
searchVal cont store ref [] = error "top io failed"
......@@ -278,13 +281,19 @@ prim_do f x state = case x of
IOValFail es -> Prelude.return (IOValFail es)
IOValOr ref bs ->
case state of
Nothing -> mapOr (\ x st -> x Prelude.>>= \ x' -> prim_do f x' st) ref bs state
Nothing -> mapOr (\ x st -> x Prelude.>>= \ x' -> prim_do f x' st)
ref bs state
Just store ->
case fromStore store ref of
Nothing ->
NoBinding _ ->
Prelude.return (IOValOr ref
(zipWith (ctcBranch (\ x st -> x Prelude.>>= \ x' -> cont x' st) ref store) [0..] bs))
Just i -> (bs!!i) Prelude.>>= \ x' -> prim_do f x' state
(zipWith (ctcBranch (\ x st -> x Prelude.>>= \ x' -> cont x' st)
ref store) [0..] bs))
Found i -> (bs!!i) Prelude.>>= \ x' -> prim_do f x' state
Redirect i j -> maybe
(Prelude.return (IOValFail (curryError "prim_do")))
(\ st -> head bs Prelude.>>= \ x' -> prim_do f x' (Just st))
(chainInStore store i j)
IOValFreeVar ref -> case binding x of
--Left i -> IOValSusp True (findBindIO cont i)
Right v -> prim_do f v state --hnfCTC exec2 state (apply f v)
......@@ -331,8 +340,12 @@ catchFail (C_IO act) err _ =
C_IO (\ st -> catch (act st) (const (hnfCTC exec2 err st)))
catchFail (C_IOFail _) err _ = err
catchFail (C_IOOr ref bs) err (Just st) = case fromStore st ref of
Nothing -> searchValCatch (zipWith (mkChoice st ref) [0..] bs) err
Just i -> catchFail (bs !! i) err (Just st)
NoBinding _ -> searchValCatch (zipWith (mkChoice st ref) [0..] bs) err
Found i -> catchFail (bs !! i) err (Just st)
Redirect i j -> maybe
err
(catchFail (head bs) err . Just)
(chainInStore st i j)
catchFail (C_IOSusp _ contRef) err _ = C_IO (\ st -> do
cont <- readIORef contRef
case cont () of
......
......@@ -10,7 +10,7 @@ import System.IO.Unsafe
import Data.IORef
import AutoGenerated2
strace s x = unsafePerformIO (putStrLn s >> return x)
trace s x = unsafePerformIO (putStrLn s >> return x)
-----------------------------------------------------------------
-- type classes to extend BaseCurry to full Curry
-----------------------------------------------------------------
......@@ -623,11 +623,16 @@ onLists _ _ (C_False:_) = C_False
onLists st ors (C_True:xs) = onLists st ors xs
onLists st ors (C_BoolAnd xs:ys) = onLists st ors (xs++ys)
onLists st ors (C_BoolOr ref xs:ys) = case fromStore st ref of
Nothing -> onLists st (insertOr ref xs ors) ys
Just i -> onLists st ors (xs!!i : ys)
NoBinding i -> onLists st (insertOr (mkRef i) xs ors) ys
Found i -> onLists st ors (xs!!i : ys)
Redirect i j -> maybe (failed $ curryError "onLists")
(\st -> onLists st ors (head xs:ys))
(chainInStore st i j)
onLists st (C_BoolOr ref xs:ors) [] =
let res = map (\ (i,x) -> onLists (addToStore st ref i) ors [x]) (zip [0..] xs)
in C_BoolOr ref res
let inBranch i x = maybe (failed $ curryError "onLists")
(\st -> onLists st ors [x])
(addToStore st ref i)
in C_BoolOr ref (zipWith inBranch [0..] xs)
insertOr ref xs [] = [C_BoolOr ref xs]
insertOr ref xs (o@(C_BoolOr ref2 xs2):ys)
......@@ -677,32 +682,32 @@ genStrEq a b = (\ a' -> (onceMore a') `hnfCTC` b) `hnfCTC` a
where
checkFree Free Free
| freeVarRef x Prelude.== freeVarRef y
= C_True
| otherwise = bind (freeVarRef x) y C_True
= trace "a" C_True
| otherwise = trace "b" bind (freeVarRef x) y C_True
-- maybe create new var to be symmetric?
checkFree Free _ = let p=pattern () in
bind (freeVarRef x) p (hnfCTC (\ x' -> unify x' y) p st)
trace "c" bind (freeVarRef x) p (hnfCTC (\ x' -> unify x' y) p st)
checkFree _ Free = let p=pattern () in
bind (freeVarRef y) p (hnfCTC (unify x) p st)
trace "d" bind (freeVarRef y) p (hnfCTC (unify x) p st)
checkFree Val Val = strEq x y st
checkFree Val Val = trace "e" strEq x y st
checkFree Branching Branching
| deref rx Prelude.== dry
= C_True
| otherwise = branching (chainTo rx dry) [C_True]
where rx=orRef x
| drx Prelude.== dry
= trace "f" C_True
| otherwise = trace "g" branching (chainTo drx dry) [C_True]
where drx=deref (orRef x)
dry=deref (orRef y)
checkFree Branching _ =
checkFree Branching _ = trace ("h "++show (orRef x,branches x))
hnfCTC (\ x' -> unify x' y)
(branching (narrowOrRef (orRef x)) (branches x)) st
checkFree _ Branching =
checkFree _ Branching = trace "i"
hnfCTC (unify x)
(branching (narrowOrRef (orRef y)) (branches y)) st
checkFree x y = error $ "checkFree " ++ show (x,y)
checkFree x y = trace "j" error $ "checkFree " ++ show (x,y)
strEqFail :: String -> StrEqResult
strEqFail s = C_False --C_SuccessFail (ErrorCall ("(=:=) for type "++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