{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
             IncoherentInstances, RankNTypes, ScopedTypeVariables,
             FlexibleContexts,UndecidableInstances #-}
--
-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
--

module SizedExp  where

import Lambda as L
import Constraints
import Data.Supply
import Control.Arrow
import Control.Monad

class TS b => (Unify se a b)  where
    unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) ->
        (b -> Size se b -> (Size se b, d)) ->
        a -> (Size se b, d)

instance (SizedExp se, Unify se a b, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1->a) (c2->b) where
    unify f g = f undefined

instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where
    unify f g = g undefined

class SizedExp (se :: * -> *) where
    data Size se :: * -> *
    true  :: Size se x
    known  :: L -> Size se x
    match :: Size se [l] -> Size se r -> (Size se l -> Size se [l] -> Size se r) ->  Size se r
    bind  :: (Unify se a b) => L.L -> a -> Size se b
    app   :: Size se (a->b) -> Size se a -> Size se b
    iff   :: Bool -> Size se a -> Size se a -> Size se a
    num   :: Integer -> Size se Int

instance Show (Size se a) where
    show (==) = error "no show on Size!"
instance Eq (Size se a) where
    (==) = undefined
instance (SizedExp se) => Num (Size se Int) where
    fromInteger = num
    x + y = num 0
    x * y = num 0
    abs = undefined
    signum = undefined
instance (SizedExp se) => Ord(Size se Int) where

{-
 - Implementation of constraints
 -}
sizeof :: Size Q a -> IO [SExp]
sizeof (QSynt s)       = s
sizeof (QProvable l _) = return [([], l)]

fresh :: TypeKind -> Supply Int -> L
fresh sig var = fresh' sig [] var
    where
    fresh' U _ _ = Unsized
    fresh' V l var = appall (supplyValue var) l
    fresh' (F _ b) l var = Abs i $ fresh' b (Var i:l) v2
        where
        (v1,v2) = split2 var
        i = supplyValue v1
    fresh' (L a) l var = List (appall i l) (Abs j $ fresh' a (Var j:l) v3)
        where
        (v1,v2,v3) = split3 var
        i = supplyValue v1
        j = supplyValue v2


freshvars2 :: (TS b, Unify Q (Size Q a) a) => Supply Int -> b -> Size Q a -> (Size Q a, L -> L)
freshvars2 supply q exp = (exp , id)

freshvars :: (TS c, Unify Q a b) => Supply Int -> c -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2))
    where
    (s1, s2, s3) = split3 supply
    freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
    freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv)
        where
        (x, f) = u $ exp $ QSynt $ do
            return [([], fv)]
        fv = fresh (tk q) s3

addConstraint :: Constraint -> [SExp] -> [SExp]
addConstraint nc = map (first ((:) nc))

concatMapM :: (a -> IO [b]) -> [a] -> IO [b]
concatMapM f l = liftM concat $ mapM f l

type SExp = ([Constraint], L)
newtype Q a = Q { unQ :: () }
instance SizedExp Q where
    data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition])
    known l = QSynt $return [([], l)]
    true = QSynt $ return []
    match l nil cons = let
            match1 (cond, ltype) = do
                    x <- sizeof l
                    let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
                    nils <- sizeof nil
                    let nilc = foldr addConstraint nils $ Zero lt:cond
                    let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype
                    let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype
                    conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
                    let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond
                    return $ nilc ++ consc
        in QSynt $ sizeof l >>= concatMapM match1

    iff _ l1 l2 = QSynt $ do
        ll1 <- sizeof l1
        ll2 <- sizeof l2
        return $ ll1 ++ ll2

    app l1 l2 = QSynt $ do
            ll1 <- sizeof l1
            ll2 <- sizeof l2
            return  [ (c1 ++ c2,  App e1 e2) | (c1,e1) <- ll1, (c2,e2) <- ll2]

    bind l exp = z $ \supply -> let (s1,s2) = split2 supply in unify (freshvars s1) (freshvars2 s2) exp
        where
        z :: (Supply Int -> (Size Q c, L -> L)) -> Size Q c
        z x = QProvable l $ \supply -> let
                (sexp, f) = x supply
                ll = rall $ f l
                rr (Zero a) = Zero $ rall a
                rr (GEC a b) = rall a `GEC` rall b
                rr (LTC a b) = rall a `LTC` rall b
            in do
                l3 <- sizeof sexp
                return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3

    num n = QSynt $return [([], Unsized)]

instance Num (Size Q Int) where
    (+) = undefined
    (*) = undefined
    abs = undefined
    signum = undefined
    fromInteger = num

conditions :: Size Q b -> IO ()
conditions (QProvable l x) = do
    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1)
    c <- x s1
    print c

prove :: Size Q b -> IO Bool
prove (QProvable l x) = do
    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1)
    c <- x s1
    putStrLn ""
    putStrLn "------------"
    putStrLn "Conditions: "
    print c
    putStrLn ""
    putStrLn "------------"
    putStrLn "Equations: "
    x <- checkCond s2 c
    print x
    putStrLn ""
    putStrLn "------------"
    putStrLn "Solving: "
    y <- solve x s3
    putStrLn ""
    if null y then do
        putStrLn "QED"
        return True
      else do
        putStrLn "------------"
        putStrLn "Cannot prove: "
        print y
        return False