a11

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index 77445a6..fabad8c 100644 (file)
--- a/afp/a10/a10.icl
+++ b/afp/a10/a10.icl
@@ -77,4 +77,11 @@ eval (WhileContainerBelow _ action) s
                = eval (action :. whileContainerBelow action) s
        = pure s
 
-Start = moveToShip :. moveDown
+opt :: (Action a b) -> Action a b
+opt (WhileContainerBelow b a) = WhileContainerBelow b (opt a)
+opt (Wait bm :. b) = opt (bm.f2 b)
+opt (a :. Wait bm) = opt (bm.t2 a)
+opt (a :. b) = opt a :. opt b
+opt x = x
+
+Start = opt (moveToShip :. wait :. moveDown)

diff --git a/afp/a11/a10.icl b/afp/a11/a10.icl
new file mode 100644 (file)
index 0000000..0344721
--- /dev/null
+++ b/afp/a11/a10.icl
@@ -0,0 +1,181 @@
+module a10
+
+import StdEnv
+
+import Data.Functor
+import Control.Applicative
+import Control.Monad => qualified join
+import Control.Monad.Trans
+import Control.Monad.State
+import Data.Maybe
+import Data.Error
+import Data.Either
+import Data.Func
+import Text
+
+:: Step pre post = Step
+:: High = High
+:: Low = Low
+
+class action v
+where
+       moveToShip :: v (Step High High)
+       moveToQuay :: v (Step High High)
+       moveUp :: v (Step Low High)
+       moveDown :: v (Step High Low)
+       lock :: v (Step Low Low)
+       unlock :: v (Step Low Low)
+       wait :: v (Step a a)
+       (:.) infixl 1 :: (v (Step a b)) (v (Step b c)) -> v (Step a c)
+       While :: (v Bool) (v (Step a a)) -> v (Step a a)
+
+class expr v
+where
+       containersBelow :: v Int
+       lit :: t -> v t | toString t
+       (<.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
+       (>.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
+       (+.) infix 4 :: (v t) (v t) -> (v t) | + t
+
+:: Var a = Var Int
+class var v
+where
+       def :: (v t) ((v (Var t)) -> (v (Step a b))) -> v (Step a b) | TC t
+       var :: (v (Var t)) -> v t | TC t
+       (=.) infixr 2 :: (v (Var t)) (v t) -> v (Step a a) | TC t
+
+//Printing
+:: Printer a = P (Int Int [String] -> [String])
+runPrinter (P a) = a 0 0
+
+word :: String -> Printer a
+word s = P \v i c->[createArray i '\t',s:c]
+
+instance action Printer
+where
+       moveToShip = word "moveToShip"
+       moveToQuay = word "moveToQuay"
+       moveUp = word "moveUp"
+       moveDown = word "moveDown"
+       lock = word "lock"
+       unlock = word "unlock"
+       wait = word "wait"
+       (:.) (P a) (P b) = P \v i c->a v i [":.\n":b v i c]
+       While (P b) (P a) = P \v i c->["while (":b v 0 [")\n":a v (i+1) ["\n)":c]]]
+
+instance expr Printer
+where
+       containersBelow = P \v i c->["containerBelow":c]
+       lit x = P \v i c->[toString x:c]
+       (<.) (P x) (P y) = P \v i c->x v i [" < ":y v i c]
+       (>.) (P x) (P y) = P \v i c->x v i [" > ":y v i c]
+       (+.) (P x) (P y) = P \v i c->x v i [" + ":y v i c]
+
+varname i = "v" +++ toString i
+instance var Printer
+where
+       def (P e) fun = P \v i c->[createArray i '\t',"def ":e v i [" \\",varname v,".\n":let (P f) = fun (P \_ i c->[varname v:c]) in f (inc v) i c]]
+       var (P e) = P e
+       (=.) (P a) (P b) = P \v i c->[createArray i '\t':a v i [" = ":b v i c]]
+
+//Evaluating
+:: Eval a :== StateT SemState (Either String) a
+cast f = f >>| pure Step
+fail s = liftT (Left s)
+runEval = runStateT
+instance action (StateT SemState (Either String))
+where
+       moveToShip = cast $ modify (\s->{s & craneOnQuay=False})
+       moveToQuay = cast $ modify (\s->{s & craneOnQuay=True})
+       moveUp     = cast $ modify (\s->{s & craneUp=True})
+       moveDown   = cast $ modify (\s->{s & craneUp=False})
+       lock       = cast $ getState >>= \s->case s of
+               {locked=Just _}                   = fail "Already locked"
+               {craneOnQuay=True,onQuay=[]}      = fail "No container to lock to"
+               {craneOnQuay=False,onShip=[]}     = fail "No container to lock to"
+               {craneOnQuay=True,onQuay=[x:xs]}  = put {s & onQuay=xs,locked=Just x}
+               {craneOnQuay=False,onShip=[x:xs]} = put {s & onShip=xs,locked=Just x}
+               _                                 = fail "Shouldn't happen"
+       unlock       = cast $ getState >>= \s->case s of
+               {locked=Nothing}                  = fail "Already unlocked"
+               {craneOnQuay=True,locked=Just x}  = put {s & onQuay=[x:s.onQuay],locked=Nothing}
+               {craneOnQuay=False,locked=Just x} = put {s & onShip=[x:s.onShip],locked=Nothing}
+               _                                 = fail "Shouldn't happen"
+       wait = pure Step
+       (:.) x y = cast $ x >>| y
+       While x y = x >>= \b->if b (y :. (While x y)) (pure Step)
+
+instance expr (StateT SemState (Either String))
+where
+       containersBelow = gets (\s->length if s.craneOnQuay s.onQuay s.onShip)
+       lit x = pure x
+       (<.) x y = (<) <$> x <*> y
+       (>.) x y = (>) <$> x <*> y
+       (+.) x y = (+) <$> x <*> y
+
+instance var (StateT SemState (Either String))
+where
+       def d fun = d >>= \v->gets (\s->length s.variables) >>= \i->modify (\s->{s & variables=s.variables ++ [dynamic v]}) >>| fun (pure (Var i))
+       var a = a >>= \(Var i)->gets (\s->s.variables !! i) >>= cast
+       where
+               cast :: Dynamic -> StateT SemState (Either String) a | TC a
+               cast (a :: a^) = pure a
+               cast_ =  fail "Something went horribly wrong"
+       (=.) a b = cast $ a >>= \(Var i)->b >>= \v->modify (\s->{s & variables=updateAt i (dynamic v) s.variables})
+
+:: SemState =
+       { onShip      :: [String]
+       , onQuay      :: [String]
+       , craneUp     :: Bool
+       , craneOnQuay :: Bool
+       , locked      :: Maybe String
+       , variables   :: [Dynamic]
+       }
+
+state0 =
+       { onShip = []
+       , onQuay = ["apples","beer","camera's"]
+       , craneUp = True
+       , craneOnQuay = True
+       , locked = Nothing
+       , variables = []
+       }
+
+Start :: (String, Either String SemState, String, Either String SemState)
+Start =
+       ( concat $ runPrinter loadShip []
+       , execStateT loadShip state0
+       , concat $ runPrinter loadShip2 []
+       , execStateT loadShip2 state0
+       )
+       
+loadShip =
+       While (containersBelow >. lit 0) (
+               moveDown:.
+               lock:.
+               moveUp:.
+               moveToShip:.
+               wait:.
+               moveDown:.
+               wait:.
+               unlock:.
+               moveUp:.
+               moveToQuay
+       )
+
+loadShip2 =
+       def containersBelow \n.
+       def (lit 0) \m.
+       While (var n >. lit 0) (
+               moveDown:.
+               lock:.
+               moveUp:.
+               moveToShip:.
+               wait:.
+               moveDown:.
+               wait:.
+               unlock:.
+               moveUp:.
+               moveToQuay:.
+               n =. var n +. lit (-1)
+       )

diff --git a/contparse/test.icl b/contparse/test.icl
new file mode 100644 (file)
index 0000000..720c68d
--- /dev/null
+++ b/contparse/test.icl
@@ -0,0 +1,21 @@
+module test
+
+import StdEnv
+
+import Data.Tuple
+import Data.Functor
+import Control.Applicative
+import Control.Monad
+
+instance Functor ((,,) a b) where fmap f (x, y, z) = (x, y, f z)
+
+:: Parser t s m a = Parser (s [t] -> m (s, [t], a))
+
+runParser (Parser t) = t
+
+instance Functor (Parser t s m) | Functor m where fmap f fa = Parser \s t->fmap f <$> runParser fa s t
+instance pure (Parser t s m) | Applicative m where pure a = Parser \s t->pure (s, t, a)
+instance <*> (Parser t s m) | Monad m where (<*>) fab fa = ap fab fa
+instance Monad (Parser t s m) | Monad m where bind ma a2mb = Parser \s t->runParser ma s t >>= \(s, t, a)->runParser (a2mb a) s t
+
+Start = 42

diff --git a/ext/test.dcl b/ext/test.dcl
new file mode 100644 (file)
index 0000000..8af22f7
--- /dev/null
+++ b/ext/test.dcl
@@ -0,0 +1,3 @@
+definition module test
+
+

diff --git a/ext/test.icl b/ext/test.icl
new file mode 100644 (file)
index 0000000..5d31f2f
--- /dev/null
+++ b/ext/test.icl
@@ -0,0 +1,22 @@
+implementation module test
+
+import StdEnv
+import iTasks
+
+:: Test = E.s: T (R s) & iTask s
+:: R s =
+       { state :: s
+       , transform :: s -> s
+       }
+
+transf :: Test -> Test
+transf (T rec=:{state, transform})
+# state = transform state
+= T {R | rec & state = state}
+
+test :: Test
+test = T {R | state = True, transform = not}
+
+Start :: Bool
+Start
+= let (T {R|state}) = transf test in gEq{|*|} state state

diff --git a/funcdeps/test.icl b/funcdeps/test.icl
index 5a03545..f9ef764 100644 (file)
--- a/funcdeps/test.icl
+++ b/funcdeps/test.icl
@@ -3,16 +3,20 @@ module test
 import StdMisc
 
 :: Zero = Zero
-:: Succ a = Succ
-
+:: Succ a = Succ a
 :: Ar3 a b c :== (a -> b -> c)
 
-class C m :: (m b)
-
-instance C ((->) a) where C = \x->undef
+class succ a ~b :: a -> b
+instance succ Zero (Succ Zero) where succ Zero = Succ Zero
+instance succ a (Succ a) where succ a = Succ a
 
-Start :: (a -> b -> c)
-Start = t
+class plus a b | succ a b :: a b
+instance plus Zero a a
+where
+       plus a b = b
+instance plus (Succ a) b c | plus a (Succ b) c
+where
+       plus (Succ a) b = plus a (Succ b)
 
-t :: (Ar3 a b c)
-t = C
+Start :: Int
+Start = 42