NotElem.idr

module NotElem

import Language.Reflection.Elab
import Language.Reflection.Utils

import Data.List


emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible

emptyNotHere : {x,y : a} -> {ys : List a} -> (hy1 : Elem x (y :: ys)) -> (notThis : Not (x = y)) -> (notMore : Not (Elem x ys)) -> Void
emptyNotHere Here x1 x2 = x1 Refl
emptyNotHere (There x) x1 x2 = x2 x


||| Attempt to create a witness that two canonical things are not equal, or else fail
mkNotEq : Raw -> Raw -> Raw -> Elab TTName
mkNotEq ty x y = do let fn = UN $ show x ++ show y ++ "nope"
                    ty <- lookupTy fn
                    case ty of
                      [] => do let argTy : Raw = `((=) {A=~ty} {B=~ty} ~x ~y)
                               declareType $ Declare fn [Explicit (UN "h") NotErased argTy] `(Void)
                               defineFunction $ DefineFun fn []
                               -- Note: this is passing the totality checker even when it shouldn't!
                               -- Investigate. Also, DefineFun needs a field to say "fail if not total".
                               return fn
                      _ => return fn

autoNotElt : TT -> Elab ()
autoNotElt `(Elem {a=~t} ~x [] -> Void) =
  do h <- gensym "h"
     attack; intro (Just h)
     fill [| (Var `{emptyNotElem}) !(forgetTypes t) !(forgetTypes x) (Var h)|]
     solve; solve
autoNotElt `(Elem {a=~t} ~x (~y :: ~xs) -> Void) =
  do h <- gensym "h"
     attack; intro (Just h)
     noteq <- mkNotEq !(forgetTypes t) !(forgetTypes x) !(forgetTypes y)

     holes <- map snd <$>
              apply [| (Var `{emptyNotHere}) !(forgetTypes t) !(forgetTypes x) !(forgetTypes y)
                                             !(forgetTypes xs) (Var h) (Var noteq)
                     |] [(False, 0)]


     solve;
     traverse_ {b=()}
        (\h => do focus h
                  compute
                  autoNotElt (snd !getGoal))
        holes
     solve
autoNotElt _ = fail [TextPart "nope"]

autoNotHere : Elab ()
autoNotHere = do compute
                 g <- snd <$> getGoal
                 autoNotElt g

%default total

test1 : Not (Elem Z [1])
test1 = %runElab autoNotHere

test2 : Not (Elem Z [])
test2 = %runElab autoNotHere

test3 : Not (Elem "foo" ["fnord"])
test3 = %runElab autoNotHere

test4 : Not (Elem "foo" ["foo"])
test4 = %runElab autoNotHere