{-# LANGUAGE
  UndecidableInstances,
  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) (t→r)
       ⇒ 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)
     where
      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)
    where
      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
  
instance
  (ExtendEnv env rest ret env' fun,
   ListToFun pt t)
  ⇒ ExtendEnv env (pt :*: rest) ret ((TypeToTermT pt t) :*: env') (t → fun)
   where 
 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