From f97a5bd0b5f76a04c484555f7ff16b0f3ba152bb Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 5 Dec 2018 13:14:09 +0100
Subject: [PATCH] a11

---
 afp/a10/a10.icl    |   9 ++-
 afp/a11/a10.icl    | 181 +++++++++++++++++++++++++++++++++++++++++++++
 contparse/test.icl |  21 ++++++
 ext/test.dcl       |   3 +
 ext/test.icl       |  22 ++++++
 funcdeps/test.icl  |  22 +++---
 6 files changed, 248 insertions(+), 10 deletions(-)
 create mode 100644 afp/a11/a10.icl
 create mode 100644 contparse/test.icl
 create mode 100644 ext/test.dcl
 create mode 100644 ext/test.icl

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index 77445a6..fabad8c 100644
--- 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
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
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
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
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
--- 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
-- 
2.20.1