UnicodeSyntax, TypeOperators, ScopedTypeVariables, MultiParamTypeClasses,
  FunctionalDependencies, TypeSynonymInstances, FlexibleInstances, 
  FlexibleContexts, NoMonomorphismRestriction #-}

-- | Guess a value for a combinator
-- Based on De-typechecker: converting from a type to a term
-- by <oleg at pobox.com>
-- http://www.haskell.org/pipermail/haskell/2005-March/015423.html

module Guess.Combinator (combinator) where

import Guess.Combinator.Lib

-- | Guess a combinator given its type
-- Example:
-- >>> let f = combinator :: (b -> c) -> (a -> b) -> a -> c
-- >>> f (:[]) ((,) True) 10
-- [(True, 10)]

combinator  GuessCombinator t HNil  t
combinator = combinatorWith emptyEnv

-- | Tests
test =
  ((combinator  a  (a  b)  b) 'O' (:"K"), "OK")
  .*. (combinator 'O' (:"K") :: String, "OK")
  .*. ((combinator  a  (a  b)  b) 1 (+2), 3)
  .*. ((combinator  (b  c)  (a  b)  a  c) Just Right True, Just (Right True))
  .*. ((combinator  a  b  a) 'a' 'b', 'a')
  .*. ((combinator  (t  t1)  t  t2  t1) Just 1 'c', Just 1)
  .*. ((combinator  (b  c)  (a  b)  a  c) (:[]) ((,) True) 10, [(True, 10)])
  .*. ((combinator  (((a  b  c)  (a  b)  a  c) (t3  t1  t2  t3)  t)  t) (\f g  f (g 1) (:[]) 2), 1)
  .*. ((combinator  ((a  b)  c)  (a  b)  c) ($2) (+3), 5)
  .*. (combinator 'a' True  Bool, True) 
  .*. HNil

-- | A type/value pair
-- The list representation of the type is also kept.

newtype TypeToTermT tl t = TypeToTermT t deriving Show

-- | GuessCombinator +type +env
-- Guess a combinator given its type and an environment

class GuessCombinator t env where
    combinatorWith  env  t

instance (IsFunction t flag,
          GuessWith' flag t env)
        GuessCombinator t env where
    combinatorWith = guessWith' (Proxy  Proxy flag)

class GuessWith' flag t env where
    guessWith'  (Proxy flag)  env  t

-- | If its a function, add the argument to the environment and guess the result
instance (IsFunction x flagx,
          FunToList' flagx x tlx, 
          IsFunction y flagy,
          GuessWith' flagy y ((TypeToTermT tlx x) :*: env))
        GuessWith' HTrue (x  y) env where
  guessWith' _ env = \(v  x) 
             guessWith' (Proxy  Proxy flagy) (((TypeToTermT v)  TypeToTermT tlx x) .*. env)

-- | If it's not a function, let RResolve find a suitable value
instance (RResolve env ((t :*: HNil) :*: HNil) HNil t)
        GuessWith' HFalse t env where
    guessWith' _ env = rresolve env (Proxy  Proxy ((t :*: HNil) :*: HNil)) HNil

-- | RResolve +env +goals +retlist -ret
-- Type-level SLD resolution algorithm
-- env: a list of TypeToTermT
-- goals: the tail of a flattened type
-- retlist: a function and arguments, reversed, such as any one of tails [a, b, b -> a -> ret]
-- ret: resulting type/value (a collapsed retlist)

class RResolve env goals tl t | env goals tl  t where
    rresolve  env  (Proxy goals)  tl  t

-- | When there are no goals left and the retlist is a singleton, return it

instance RResolve env HNil (t :*: HNil) t where
    rresolve _ _ (HCons t HNil) = t

-- | When there are no goals left and the retlist is not a singleton, collapse the retlist

instance RResolve env HNil (t1 :*: tr) (tr)
        RResolve env HNil (t :*: t1 :*: tr) r where
    rresolve g _ (HCons t r) = (rresolve g (Proxy  Proxy HNil) r) t

-- | When the type we want is not a function, look it up in the environment.
-- If we have a function that returns it, save the function and guess its arguments.

instance (RHLookup g env (TypeToTermT (g :*: assum) g'),
          HReverse assum assum',
          RResolve env assum' (g' :*: HNil) ra,
          RResolve env gr (ra :*: pt) t)
        RResolve env ((g :*: HNil) :*: gr) pt t where
    rresolve env _ pt = rresolve env (Proxy  Proxy gr) (ra .*. pt)
      TypeToTermT t1 = rhlookup (Proxy  Proxy g) env
      ra  ra = rresolve env (Proxy  Proxy assum') (t1 .*. HNil)

-- | The instance for improper combinators was left as an exercise.
-- When we need a function, build the function, add its arguments to the
-- environment and guess the result.

instance (HReverse (gc :*: gcr) revr,
          ExtendEnv env revr ra env' f,
          RResolve env' ((g :*: HNil) :*: HNil) HNil ra,
          RResolve env gr (f :*: pt) t)
          RResolve env ((g :*: gc :*: gcr) :*: gr) pt t where
  rresolve (env  env) _ (pt  pt) = rresolve env (Proxy  Proxy gr) (f .*. pt)
      f  f
      f = extendEnv env (Proxy  Proxy revr) $ \(env'  env') 
          rresolve env' (Proxy  Proxy ((g :*: HNil) :*: HNil)) HNil

-- | Extend an environment with the arguments of a function.
-- The argument list must be the reverse of the tail of the flattened
-- function type.
-- Given a continutation, return a function that builds the environment.
-- For example: 
-- extendEnv [] [[a] [b]] k = \a b -> k env'

class ExtendEnv env vs ret env' fun | env vs ret  env' fun where
  extendEnv  env  (Proxy vs)  (env'  ret)  fun

instance ExtendEnv env HNil ret env ret where
  extendEnv env _ k = k env
  (ExtendEnv env rest ret env' fun,
   ListToFun pt t)
   ExtendEnv env (pt :*: rest) ret ((TypeToTermT pt t) :*: env') (t  fun)
 extendEnv env _ f = \(t  t) 
   extendEnv env (Proxy  Proxy rest) $ \env' 
   f ((TypeToTermT t  TypeToTermT pt t) .*. env')

-- | Lookup in the `associative' type-indexed list

class RHLookup t l w | t l  w where
    rhlookup  (Proxy t)  l  w

instance (TypeEq t t' flag, RHLookup' flag t ((TypeToTermT (t' :*: at) tt') :*: r) w)
     RHLookup t ((TypeToTermT (t' :*: at) tt') :*: r) w where
    rhlookup = rhlookup' (Proxy  Proxy flag)

class RHLookup' flag t l w | flag t l  w where
    rhlookup'  (Proxy flag)  (Proxy t)  l  w

instance RHLookup' HTrue t ((TypeToTermT (t :*: at) tt) :*: r) 
                            (TypeToTermT (t :*: at) tt) where
    rhlookup' _ _ (HCons t _) = t

instance RHLookup t r w  RHLookup' HFalse t ((TypeToTermT tl' t') :*: r) w where
    rhlookup' _ t (HCons _ r) = rhlookup t r

-- | An empty environment.
emptyEnv = HNil

-- | Add a type/value to the environment
consEnv  FunToList t tl  t  env  TypeToTermT tl t :*: env
consEnv x env = TypeToTermT x .*. env