afp/a10/setGADT.icl

   1 module a10
   2
   3 /*
   4   Advanced Progrmming 2018, Assignment 8
   5   Pieter Koopman, pieter@cs.ru.nl
   6 */
   7 import StdEnv
   8
   9 import iTasks => qualified return, >>=, >>|, sequence, forever, :: Set
  10
  11 import Control.Applicative
  12 import Control.Monad
  13 import Control.Monad.State
  14 import Control.Monad.Trans
  15 import Data.Func
  16 import Data.List
  17 import Data.Functor
  18 import Data.Either
  19 import Data.Maybe
  20
  21 import Text => qualified join
  22
  23 import qualified Data.List as List
  24 import qualified Data.Map as Map
  25
  26 ::  BM a b = { t :: a -> b, f :: b -> a, t2 :: A.t: (t a) -> (t b), f2 :: A.t: (t b) -> (t a)}
  27
  28 bm :: BM a a
  29 bm = {t = id, f = id, t2 = id, f2 = id}
  30
  31 :: Expr a
  32   = E.e: New        (BM a [e])   [e]                             & Eq, Ord, toString e
  33   | E.e: Lit        (BM a e)     e                               & toString e
  34   | E.e: Variable   (BM a e)     Ident                           & TC e
  35   | E.e: Size       (BM a Int)   (Expr [e])                      & toString e
  36   | E.e: Plus       (BM a e)     (Expr e)   (Expr e)             & + e
  37   | E.e: Minus      (BM a e)     (Expr e)   (Expr e)             & - e
  38   | E.e: Times      (BM a e)     (Expr e)   (Expr e)             & * e
  39   | E.e: Union      (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
  40   | E.e: Difference (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
  41   | E.e: Intersect  (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
  42   | E.e: Remove     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
  43   | E.e: Insert     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
  44   | E.e: Scale      (BM a [e])   (Expr e)   (Expr [e])           & * e
  45   | E.e: Assign     (BM a e)     Ident (Expr e)                  & TC e
  46   |      Not        (BM a Bool)  (Expr Bool)
  47   |      And        (BM a Bool)  (Expr Bool)(Expr Bool)
  48   |      Or         (BM a Bool)  (Expr Bool)(Expr Bool)
  49   | E.e: ElemOf     (BM a Bool)  (Expr e)   (Expr [e])           & Eq e
  50   | E.e: Equals     (BM a Bool)  (Expr e)   (Expr e)             & Eq e
  51   | E.e: LesEquals  (BM a Bool)  (Expr e)   (Expr e)             & Ord e
  52   | E.e: Expr       (BM a ())    (Expr e)
  53   | E.e: For        (BM a ())    String (Expr [e]) (Expr ())     & TC e
  54   | E.e: If         (BM a ())    (Expr Bool) (Expr ()) (Expr ())
  55   |      Seq        (BM a ())    (Expr ()) (Expr ())
  56
  57 // === Smart constructors
  58 new e = New bm e
  59 lit e = Lit bm e
  60 var e = Variable bm e
  61 size e = Size bm e
  62 (+.) infixl 6
  63 (+.) a b = Plus bm a b
  64 (-.) infixl 6
  65 (-.) a b = Minus bm a b
  66 (*.) infixl 6
  67 (*.) a b = Times bm a b
  68 union a b = Union bm a b
  69 difference a b = Difference bm a b
  70 intersect a b = Intersect bm a b
  71 remove a b = Remove bm a b
  72 insert a b = Insert bm a b
  73 scale a b = Scale bm a b
  74 (=.) infixl 2
  75 (=.) a b = Assign bm a b
  76 instance ~ (Expr Bool) where ~ a = Not bm a
  77 (&&.) infixr 2
  78 (&&.) a b = And bm a b
  79 (||.) infixr 2
  80 (||.) a b = Or bm a b
  81 (In) infix 4
  82 (In) a b = ElemOf bm a b
  83 (==.) infix 4
  84 (==.) a b = Equals bm a b
  85 (<=.) infix 4
  86 (<=.) a b = LesEquals bm a b
  87 expr a = Expr bm a
  88 for a b c = For bm a b c
  89 iff a b c = If bm a b c
  90 (:.) infixl 1
  91 (:.) a b = Seq bm a b
  92
  93 :: Ident  :== String
  94
  95 // === State
  96 :: Val :== Either Int [Int]
  97 :: SemState :== 'Map'.Map String Dynamic
  98 :: Sem a :== StateT SemState (Either String) a
  99
 100 store :: Ident a -> Sem a | TC a
 101 store k v = modify ('Map'.put k (dynamic v)) *> pure v
 102
 103 read :: Ident -> Sem a | TC a
 104 read k = gets ('Map'.get k) >>= \v->case v of
 105         (Just (a :: a^)) = pure a
 106         (Just a) = fail
 107                 (   "Type mismatch... expected: "
 108                 +++ toString (undef :: a^)
 109                 +++ " got: "
 110                 +++ printType a
 111                 )
 112         Nothing = fail ("No variable with ident " +++ k)
 113 where
 114         printType :: Dynamic -> String
 115         printType a = toString (typeCodeOfDynamic a)
 116
 117 fail :: String -> Sem a
 118 fail s = liftT (Left s)
 119
 120 eval :: (Expr e) -> Sem e
 121 eval (New {f,f2} s)        = f2 $ pure ('List'.nub s)
 122 eval (Lit {f2} i)          = f2 $ pure i
 123 eval (Variable {f2} i)     = f2 $ read i
 124 eval (Size {f2} s)         = f2 $ length <$> eval s
 125 eval (Plus {f2} a b)       = f2 $ (+) <$> eval a <*> eval b
 126 eval (Minus {f2} a b)      = f2 $ (-) <$> eval a <*> eval b
 127 eval (Times {f2} a b)      = f2 $ (*) <$> eval a <*> eval b
 128 eval (Union {f2} a b)      = f2 $ 'List'.union <$> eval a <*> eval b
 129 eval (Difference {f2} a b) = f2 $ 'List'.difference <$> eval a <*> eval b
 130 eval (Intersect {f2} a b)  = f2 $ 'List'.intersect <$> eval a <*> eval b
 131 eval (Remove {f2} a b)     = f2 $ 'List'.delete <$> eval a <*> eval b
 132 eval (Insert {f2} a b)     = f2 $ 'List'.union <$> (pure <$> eval a) <*> eval b
 133 eval (Scale {f2} a b)      = f2 $ (map o (*)) <$> eval a <*> eval b
 134 eval (Assign {f2} v b)     = f2 $ eval b >>= store v
 135 eval (Not {f2} b)          = f2 $ not <$> eval b
 136 eval (And {f2} b1 b2)      = f2 $ (&&) <$> eval b1 <*> eval b2
 137 eval (Or {f2} b1 b2)       = f2 $ (||) <$> eval b1 <*> eval b2
 138 eval (ElemOf {f2} e s)     = f2 $ 'List'.elem <$> eval e <*> eval s
 139 eval (Equals {f2} e1 e2)   = f2 $ (==) <$> eval e1 <*> eval e2
 140 eval (LesEquals {f2} e1 e2)= f2 $ (<=) <$> eval e2 <*> eval e2
 141 eval (Expr {f2} e)         = f2 $ eval e *> pure ()
 142 eval (For {f2} i bag b)    = f2 $ eval bag >>= foldr proc (pure ())
 143 where
 144         //Needed to convince the compiler that there is a TC of e
 145         proc :: e (Sem ()) -> Sem () | TC e
 146         proc e m = store i e *> eval b *> m
 147 eval (If {f2} p t e)       = f2 $ eval p >>= \v->eval if v t e
 148 eval (Seq {f2} l r)        = f2 $ eval l *> eval r *> pure ()
 149
 150 print :: (Expr e) [String] -> [String]
 151 print (New _ s)          c = ["[":'List'.intersperse "," $ map toString s] ++ ["]":c]
 152 print (Lit _ i)          c = [toString i:c]
 153 print (Variable _ i)     c = [i:c]
 154 print (Size _ s)         c = ["size(":print s [")":c]]
 155 print (Plus _ a b)       c = print a ["+":print b c]
 156 print (Minus _ a b)      c = print a ["-":print b c]
 157 print (Times _ a b)      c = print a ["*":print b c]
 158 print (Union _ a b)      c = print a ["+":print b c]
 159 print (Difference _ a b) c = print a ["-":print b c]
 160 print (Intersect _ a b)  c = print a ["*":print b c]
 161 print (Remove _ a b)     c = print a ["-":print b c]
 162 print (Insert _ a b)     c = print a ["+":print b c]
 163 print (Scale _ a b)      c = print a ["*":print b c]
 164 print (Assign _ v b)     c = [v,"=":print b c]
 165 print (Not _ b)          c = ["not":print b c]
 166 print (And _ a b)        c = print a ["&&":print b c]
 167 print (Or _ a b)         c = print a ["||":print b c]
 168 print (ElemOf _ a b)     c = print a ["in":print b c]
 169 print (Equals _ a b)     c = print a ["==":print b c]
 170 print (LesEquals _ a b)  c = print a ["<=":print b c]
 171 print (Expr _ e)         c = print e c
 172 print (For _ i bag b)    c = ["For",i,"in":print bag ["do":print b c]]
 173 print (If _ p t e)       c = ["If":print p ["then":print t ["else":print e c]]]
 174 print (Seq _ l r)        c = print l ["\n":print r c]
 175
 176 Start :: (Either String (), String)
 177 Start =
 178         (evalStateT (eval stmt) 'Map'.newMap
 179         ,"\n" +++ 'Text'.join " " (print stmt [])
 180         )
 181 where
 182         stmt = expr ("x" =. new [42]) :. expr (lit 42 +. var "x")