From 01bad43f6e31dfb1ff59371ed264e94397745df9 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 18 Feb 2019 15:26:02 +0100
Subject: [PATCH] update

---
 afp/a11/a11.icl         |  28 ++++++----
 afp/a12/cashModel.dcl   |  26 +++++++++
 afp/a12/cashModel.icl   |  42 +++++++++++++++
 afp/a12/gastyStart.dcl  |  37 +++++++++++++
 afp/a12/gastyStart.icl  | 115 ++++++++++++++++++++++++++++++++++++++++
 afp/a12/testCash.icl    |  48 +++++++++++++++++
 conj-semantics/Makefile |   4 ++
 conj-semantics/test.icl |  17 ++++++
 8 files changed, 308 insertions(+), 9 deletions(-)
 create mode 100644 afp/a12/cashModel.dcl
 create mode 100644 afp/a12/cashModel.icl
 create mode 100644 afp/a12/gastyStart.dcl
 create mode 100644 afp/a12/gastyStart.icl
 create mode 100644 afp/a12/testCash.icl
 create mode 100644 conj-semantics/Makefile
 create mode 100644 conj-semantics/test.icl

diff --git a/afp/a11/a11.icl b/afp/a11/a11.icl
index 8c1600c..f586122 100644
--- a/afp/a11/a11.icl
+++ b/afp/a11/a11.icl
@@ -85,7 +85,7 @@ fail s = liftT (Left s)
 runEval = runStateT
 instance action (StateT SemState (Either String))
 where
-	moveToShip = cast $ modify (\s->{s & craneOnQuay=False})
+	moveToShip = 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})
@@ -141,15 +141,12 @@ state0 =
 	, variables = []
 	}
 
+/*
 //Optimization
 :: BM a b =
-	{ t  :: a -> b
-	, f  :: b -> a
-	, t2 :: A.v: (v a) -> v b
+	{ t2 :: A.v: (v a) -> v b
 	, f2 :: A.v: (v b) -> v a
 	}
-bm :: BM a a
-bm = {t=id,f=id,t2=id,f2=id}
 :: Opt a
 	//Actions
 	= OMoveToShip (BM a (Step High High))
@@ -180,7 +177,7 @@ where
 	moveDown = OMoveDown bm
 	lock = OLock bm
 	unlock = OUnlock bm
-	wait = OWait bm
+	wait = OWait bm sbm
 	(:.) a b = OSeq bm a b
 	While a b = OWhile bm bm a b
 
@@ -206,10 +203,19 @@ opti (OMoveDown bm) = bm.f2 moveDown
 opti (OMoveUp bm) = bm.f2 moveUp
 opti (OLock bm) = bm.f2 lock
 opti (OUnlock bm) = bm.f2 unlock
-opti (OWait bm) = bm.f2 wait
+opti (OWait bm sbm) = bm.f2 wait
 opti (OWhile bm1 bm2 p a) = bm2.f2 (While (opti (bm1.t2 p)) (opti (bm2.t2 a)))
 //opti (OSeq bm1 (OWait bm2) r) =
-//opti (OSeq bm1 l (OWait bm2)) =
+/*
+l :: (Step pre inter)
+| E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
+bm2 :: BM (Step pre inter)
+| E.e: OWait (BM (Step inter post) (Step post post)) (SBM inter post)
+
+need:
+:: BM (Step pre inter) (Step pre post)
+*/
+opti (OSeq bm1 l (OWait bm2 sbm)) = bm.f2 (opti (sbm.st2 l))
 opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
 //Expr
 opti (OContainersBelow bm) = bm.f2 containersBelow
@@ -221,9 +227,13 @@ opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
 opti (OVar bm v) = bm.f2 (var (opti v))
 opti (OAssign bm a b) = bm.f2 (opti a =. opti b)
 //opti (ODef bm a b) = bm.f2 (def (opti a) \v->opti (b (OVar bm v))
+//
 
 Start :: [String]
 Start = runPrinter (opti (loadShip)) []
+*/
+
+Start = 42
 	
 loadShip =
 	While (containersBelow >. lit 0) (
diff --git a/afp/a12/cashModel.dcl b/afp/a12/cashModel.dcl
new file mode 100644
index 0000000..9811e6a
--- /dev/null
+++ b/afp/a12/cashModel.dcl
@@ -0,0 +1,26 @@
+definition module cashModel
+/*
+	Pieter Koopman, Radboud University, 2017 -2018
+	pieter@cs.ru.nl
+	Advanced programming
+	
+	A simple state model for an automated cash register
+*/
+
+import StdEnv, Data.GenEq
+
+:: Euro = {euro :: Int, cent :: Int}
+:: Product = Pizza | Beer | Cola
+:: Action = Add Product | Rem Product | Pay
+
+class euro a :: a -> Euro
+instance euro Product, Euro
+instance euro Int, (Int, Int), [e] | euro e
+instance + Euro
+instance - Euro
+instance zero Euro
+derive gEq Euro
+instance ~ Euro
+instance == Euro, Product
+
+model :: [Product] Action -> ([Product],[Euro])
diff --git a/afp/a12/cashModel.icl b/afp/a12/cashModel.icl
new file mode 100644
index 0000000..9f7f1f9
--- /dev/null
+++ b/afp/a12/cashModel.icl
@@ -0,0 +1,42 @@
+implementation module cashModel
+/*
+	Pieter Koopman, Radboud University, 2017 - 2018
+	pieter@cs.ru.nl
+	Advanced programming
+	
+	A simple state model for an automated cash register
+*/
+
+import StdEnv, Data.GenEq
+
+class euro a :: a -> Euro
+instance euro Product where
+	euro Pizza = euro (4,99)
+	euro Beer  = euro (0,65)
+	euro _     = euro 1
+
+instance euro Int where euro e = {euro = e, cent = 0}
+instance euro (Int, Int) where euro (e,c) = {euro = e, cent = c}
+instance euro [e] | euro e where euro l = sum (map euro l)
+instance euro Euro where euro e = e
+instance + Euro where + x y = fromCents (toCents x + toCents y)
+instance - Euro where - x y = fromCents (toCents x - toCents y)
+instance zero Euro where zero = {euro = 0, cent = 0}
+derive gEq Euro, Product
+instance == Product where (==) p q = p === q
+instance == Euro where (==) p q = p === q
+
+instance ~ Euro where ~ e = {euro = ~e.euro, cent = ~e.cent}
+
+toCents :: Euro -> Int
+toCents e = if (e.euro < 0 || e.cent < 0) (~) id (abs e.euro*100 + abs e.cent)
+
+fromCents :: Int -> Euro
+fromCents c = if (c < 0) (~) id {euro=abs c / 100, cent=abs c rem 100}
+
+model :: [Product] Action -> ([Product],[Euro])
+model list (Add p) = ([p:list],[euro p])
+model list (Rem p) | isMember p list
+ = (removeMember p list,[~ (euro p)])
+ = (list,[])
+model list Pay = ([],[euro list])
diff --git a/afp/a12/gastyStart.dcl b/afp/a12/gastyStart.dcl
new file mode 100644
index 0000000..053ac97
--- /dev/null
+++ b/afp/a12/gastyStart.dcl
@@ -0,0 +1,37 @@
+definition module gastyStart
+
+/*
+	Pieter Koopman, Radboud University, 2016 - 2018
+	pieter@cs.ru.nl
+	Advanced programming
+	A simplified MBT tool based on logical properties
+	
+	Use the iTask environment!
+	Execute with "Basic values only" option
+*/
+
+import StdEnv, StdGeneric, Data.GenEq
+
+test :: p -> [String] | prop p
+class prop a where holds :: a Prop -> [Prop]
+
+:: Prop
+
+instance prop Bool
+instance prop (a->b) | prop b & testArg a
+class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
+
+generic gen a :: [a]
+derive gen Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS, OBJECT, RECORD, FIELD
+
+generic string a :: a -> String
+derive string Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT, RECORD of grd, FIELD of gfd
+
+:: For = E.a b: (For) infix 0 (a -> b) [a] & prop b & string{|*|} a
+instance prop For
+
+:: Select = E.p: (==>) infixl 0 Bool p & prop p
+instance prop Select
+
+:: Equ = E.a: (=.=) infix 4 a a & testArg a
+instance prop Equ
diff --git a/afp/a12/gastyStart.icl b/afp/a12/gastyStart.icl
new file mode 100644
index 0000000..2ea539b
--- /dev/null
+++ b/afp/a12/gastyStart.icl
@@ -0,0 +1,115 @@
+implementation module gastyStart
+
+/*
+	Pieter Koopman, Radboud University, 2016, 2017
+	pieter@cs.ru.nl
+	Advanced programming
+	A simplified MBT tool based on logical properties
+	
+	Use the iTask environment!
+	Execute with "Basic values only" option
+*/
+
+import StdEnv, StdGeneric, Data.GenEq
+
+test :: p -> [String] | prop p
+test p = check 1000 (holds p prop0)
+
+check :: Int [Prop] -> [String]
+check n [] = ["Proof\n"]
+check 0 l  = ["Passed\n"]
+check n [p:x] | p.bool
+	= check (n-1) x
+	= ["Fail for: ":reverse ["\n":p.info]]
+
+class prop a where holds :: a Prop -> [Prop]
+instance prop Bool where holds b p = [{p & bool = b}]
+instance prop (a->b) | prop b & testArg a 
+where
+	holds f p = diagonal [holds (f a) {p & info = [" ",string{|*|} a:p.info]} \\ a <- gen{|*|}]
+
+class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a 
+
+:: Prop =
+	{ bool :: Bool
+	, info :: [String]
+	}
+prop0 = {bool = True, info = []}
+
+generic gen a :: [ a ]
+gen{|Int|}  = [0,1,-1,maxint,minint,maxint-1,minint+1:[j\\i<-[2..], j<-[i,~i]]]
+gen{|Real|} = [0.0, 1.0, -1.0: reals]
+where
+	reals = [r \\ (x,y) <- diag2 ints ints | x <> y, r <- let c = toReal x / toReal y in [c, ~c]]
+	ints = [1: sieve [2..]]
+	sieve [p:xs] = [p: sieve [x \\ x <- xs | x rem p <> 0]]
+gen{|Bool|} = [True,False]
+gen{|Char|} = [' '..'~'] ++ ['\t\n\b']
+gen{|UNIT|} = [UNIT]
+gen{|PAIR|}   f g	= map (\(a,b)=PAIR a b) (diag2 f g)
+gen{|EITHER|} f g = merge (map RIGHT g) (map LEFT f)
+where
+  merge [a:x] ys = [a: merge ys x]
+  merge []    ys = ys
+gen{|CONS|}   f  = map CONS f
+gen{|OBJECT|} f  = map (\x->OBJECT x) f 
+gen{|RECORD|} f  = map RECORD f
+gen{|FIELD|}  f  = map (\x->FIELD x) f
+
+generic string a :: a -> String
+string{|Int|}  i = toString i
+string{|Real|} x = toString x
+string{|Bool|} b = toString b
+string{|Char|} c = toString ['\'',c,'\'']
+string{|UNIT|} _ = ""
+string{|PAIR|} f g (PAIR x y) = f x + " " + g y
+string{|EITHER|} f g (LEFT x) = f x
+string{|EITHER|} f g (RIGHT y) = g y
+string{|CONS of gcd|} f (CONS x) | gcd.gcd_arity > 0
+	= "(" + gcd.gcd_name + " " + f x + ")"
+	= gcd.gcd_name
+string{|OBJECT|} f (OBJECT x) = f x
+string{|RECORD of grd|} f (RECORD x) = "{" + grd.grd_name + "|" + f x + "}"
+string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + " = " + f x + " "
+
+maxint :: Int
+maxint =: IF_INT_64_OR_32 (2^63-1) (2^31-1) //2147483647
+
+minint :: Int
+minint =: IF_INT_64_OR_32 (2^63) (2^31) //-2147483648
+
+instance + String where + s t = s +++ t
+
+diagonal :: [[a]] -> [a]
+diagonal list = f 1 2 list []
+where
+	f n m [] [] = []
+	f 0 m xs ys = f m (m+1) (rev ys xs) []
+	f n m [] ys = f m (m+1) (rev ys []) []
+	f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
+	f n m [[]:xs] ys = f (n-1) m xs ys
+	
+	rev []    accu = accu
+	rev [x:r] accu = rev r [x:accu]
+
+pUpper :: Char -> Bool
+pUpper c = c <> toUpper c
+
+:: For = E.a b: (For) infix 0 (a -> b) [a] & prop b & string{|*|} a
+instance prop For
+where
+	holds (f For l) p = diagonal [holds (f a) {p & info = [" ",string{|*|} a:p.info]}\\a<-l]
+//Start = ["pUpper: ":test (pUpper For ['a'..'z'])]
+
+:: Select = E.p: (==>) infixl 0 Bool p & prop p
+instance prop Select
+where
+	holds (c ==> b) p = if c (holds b p) [{p & bool = True, info = ["rejected ":p.info]}]
+
+//Start = ["pUpper lower:": test (\c. isLower c ==> pUpper c)]
+
+:: Equ = E.a: (=.=) infix 4 a a & testArg a
+instance prop Equ
+where
+	holds (x =.= y) p = [{p & bool = x === y, info = [string{|*|} y," found: ",string{|*|} x," expected: ":p.info]}]
+//Start = test (\i->i =.= hd [i,0])
diff --git a/afp/a12/testCash.icl b/afp/a12/testCash.icl
new file mode 100644
index 0000000..e234bfa
--- /dev/null
+++ b/afp/a12/testCash.icl
@@ -0,0 +1,48 @@
+module testCash
+
+import cashModel
+import gastyStart
+
+//gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- [0..99], f<-[id,(~)]]
+gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- merge [0..50] [51..99], f<-[id,(~)]]
+where
+	merge [a:x] ys = [a:merge ys x]
+	merge [] ys =ys
+derive string Euro, Product, []
+derive gen Product, []
+derive bimap []
+derive gEq Product
+
+pPlusAssociative :: Euro Euro Euro -> Equ
+pPlusAssociative a b c = a + (b + c) =.= (a + b) + c
+
+pPlusCommutative :: Euro Euro -> Equ
+pPlusCommutative a b = a + b =.= b + a
+
+pPlusIdentity :: Euro -> Equ
+pPlusIdentity i = i + zero =.= i
+
+pNegSub :: Euro -> Equ
+pNegSub i = zero - i =.= ~i
+
+pNegNegId :: Euro -> Equ
+pNegNegId i = ~ (~i) =.= i
+
+//model :: [Product] Action -> ([Product],[Euro])
+pFair :: [Product] Product -> Equ
+pFair state p = euro state =.= euro t - euro o
+where
+	(t,o) = model state (Rem p)
+//
+//pFair2 :: [Product] Action -> Equ //Euro
+//pFair2 state action = euro state =.= euro t - euro o
+//where (t,o) = model state action
+
+Start = flatten
+	[ ["pPlusAssociative: ":test pPlusAssociative]
+	, ["pPlusCommutative: ":test pPlusCommutative]
+	, ["pPlusIdentity: ":test pPlusIdentity]
+	, ["pNegSub: ":test pNegSub]
+	, ["pNegNegId: ":test pNegNegId]
+//	, ["pFair: ":test pFair]
+	]
diff --git a/conj-semantics/Makefile b/conj-semantics/Makefile
new file mode 100644
index 0000000..83f7745
--- /dev/null
+++ b/conj-semantics/Makefile
@@ -0,0 +1,4 @@
+all:
+	mkdir -p Clean\ System\ Files
+	gcc -c test.c -o test.o
+	clm -l test.o -dynamics -IL Dynamics test -o test
diff --git a/conj-semantics/test.icl b/conj-semantics/test.icl
new file mode 100644
index 0000000..1746082
--- /dev/null
+++ b/conj-semantics/test.icl
@@ -0,0 +1,17 @@
+module test
+
+
+import Data.Either
+import iTasks
+
+Start w = doTasks viewer w
+
+viewer = parallel
+	[(Embedded, \stl->appendTask Embedded (\_->t <<@ ArrangeHorizontal) stl
+		>>= \tid->viewSharedInformation "Task Value" []
+			(sdsFocus (Right tid) (taskListItemValue stl)) @! 42)
+	] []
+
+t =    updateInformation "Left" [] 42
+  -||- (enterInformation "Right" [] -||- chooseAction [(Action "Fire", 42)])
+
-- 
2.20.1