module uexpr import StdEnv import Data.Functor import Data.Functor.Identity import Control.Applicative import Control.Monad => qualified join import Control.Monad.State import Control.Monad.Trans import Control.Monad.Writer import Data.Array import Data.Func import Data.List import Text :: In a b = In infix 0 a b class uexpr v where lit :: a -> v a | toString a (+.) infixl 6 :: (v a) (v a) -> v a | + a class uvar v where var :: (u:(v .a) -> v:(In u:(v .a) u:(v b))) -> u:(v b), [v <= u] class uarr v where arr :: *(arr a) -> v *(arr a) | Array arr a & toString a (++.) infixr 5 :: (v .(arr a)) (v .(arr a)) -> v .(arr a) | Array arr a (!.) infixl 9 :: (v .(arr a)) (v Int) -> v a | Array arr a :: Printer a = P (WriterT [String] (StateT Int Identity) ()) runPrinter (P a) = concat $ snd $ evalState (runWriterT a) 0 instance uexpr Printer where lit a = P $ tell [toString a] +. (P l) (P r) = P $ tell ["("] >>| l >>| tell ["+"] >>| r >>| tell [")"] instance uvar Printer where var def = P ( liftT (getState) >>= \s->liftT (put (s+1)) >>| let (P i In P b) = def $ P $ tell $ varName s [] in tell ["let ":varName s [" = "]] >>| i >>| tell [" in\n"] >>| b ) where varName i c = ["v",toString i:c] instance uarr Printer where arr a = P $ tell ["{",join "," [toString a\\a<-:a],"}"] ++. (P l) (P r) = P $ tell ["("] >>| l >>| tell ["+++"] >>| r >>| tell [")"] !. (P l) (P r) = P $ l >>| tell [".["] >>| r >>| tell ["]"] :: Eval a = E a runEval (E a) = a instance uexpr Eval where lit a = E $ pure a +. (E l) (E r) = E $ l + r //instance uvar Eval where // var def = let (i In b) = def i in b instance uarr Eval where arr a = E a ++. (E l) (E r) = E (appendArr l r) !. (E l) (E r) = E (select l r) appendArr :: .(arr a) .(arr a) -> .arr a | Array arr a appendArr l r = {if (i < size l) l.[i] r.[i rem size l]\\i<-[0..size l + size r - 1]} //Start = both (var \v=arr {!1,2,3} In v ++. arr {!4,5,6}) Start = runPrinter (var \v=arr {!1,2,3} In v ++. arr {!4,5,6}) //both :: (A.v: v a | uexpr, uarr, uvar v) -> (String, a) //both f = (runPrinter f, runEval f) //i :: v Int | uexpr v //i = lit 41 +. lit 1 // //ai :: v {Int} | uexpr, uarr v //ai = arr {1,2,3} // //aip :: v {Int} | uexpr, uarr v //aip = arr {1,2,3} ++. arr {4,5,6} // //aii :: v Int | uexpr, uarr v //aii = ai !. lit 41 // //somearray :: *{Int} //somearray = {1,2,3}