module TTImp.Impossible import Core.Contextimport Core.Envimport Core.Normaliseimport Core.TTimport Core.Value import TTImp.TTImp -- This file contains support for building a guess at the term on the LHS of an -- 'impossible' case, in order to help build a tree of covered cases for-- coverage checking. Since the LHS by definition won't be well typed, we are-- only guessing! But we can still do some type-directed disambiguation of-- names.-- Constants (fromInteger/fromString etc) won't be supported, because in general-- they involve resoling interfaces - they'll just become unmatchable patterns. match : {auto c : Ref Ctxt Defs} ->        NF [] -> (Name, Int, ClosedTerm) -> Core Boolmatch nty (n, i, rty)    = do defs <- get Ctxt         rtynf <- nf defs [] rty         sameRet nty rtynf  where    sameRet : NF [] -> NF [] -> Core Bool    sameRet _ (NApp _ _ _) = pure True    sameRet _ (NErased _ _) = pure True    sameRet (NApp _ _ _) _ = pure True    sameRet (NErased _ _) _ = pure True    sameRet (NTCon _ n _ _ _) (NTCon _ n' _ _ _) = pure (n == n')    sameRet (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')    sameRet (NType _) (NType _) = pure True    sameRet nf (NBind fc _ (Pi _ _ _) sc)        = do defs <- get Ctxt             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))             sameRet nf sc'    sameRet _ _ = pure False dropNoMatch : {auto c : Ref Ctxt Defs} ->              Maybe (NF []) -> List (Name, Int, ClosedTerm) ->              Core (List (Name, Int, ClosedTerm))dropNoMatch _ [t] = pure [t]dropNoMatch Nothing ts = pure tsdropNoMatch (Just nty) ts    = -- if the return type of a thing in ts doesn't match nty, drop it      filterM (match nty) ts nextVar : {auto q : Ref QVar Int} ->          FC -> Core (Term [])nextVar fc    = do i <- get QVar         put QVar (i + 1)         pure (Ref fc Bound (MN "imp" i)) mutual  processArgs : {auto c : Ref Ctxt Defs} ->                {auto q : Ref QVar Int} ->                Term [] -> NF [] ->                (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->                Core ClosedTerm  processArgs fn (NBind fc x (Pi r Explicit ty) sc) (e :: exp) imp     = do e' <- mkTerm e (Just ty) [] []          defs <- get Ctxt          processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))                      exp imp  processArgs fn (NBind fc x (Pi r Implicit ty) sc) exp imp     = do defs <- get Ctxt          case useImp [] imp of            Nothing => do e' <- nextVar fc                          processArgs (App fc fn e')                                      !(sc defs (toClosure defaultOpts [] e'))                                      exp imp            Just (e, impargs') =>               do e' <- mkTerm e (Just ty) [] []                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))                              exp impargs'    where      useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->               Maybe (RawImp, List (Maybe Name, RawImp))      useImp acc [] = Nothing      useImp acc ((Just x', xtm) :: rest)          = if x == x'               then Just (xtm, reverse acc ++ rest)               else useImp ((Just x', xtm) :: acc) rest      useImp acc (ximp :: rest)          = useImp (ximp :: acc) rest  processArgs fn (NBind fc x (Pi r AutoImplicit ty) sc) exp imp     = do defs <- get Ctxt          case useAutoImp [] imp of            Nothing => do e' <- nextVar fc                          processArgs (App fc fn e')                                      !(sc defs (toClosure defaultOpts [] e'))                                      exp imp            Just (e, impargs') =>               do e' <- mkTerm e (Just ty) [] []                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))                              exp impargs'    where      useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->                   Maybe (RawImp, List (Maybe Name, RawImp))      useAutoImp acc [] = Nothing      useAutoImp acc ((Nothing, xtm) :: rest)          = Just (xtm, reverse acc ++ rest)      useAutoImp acc ((Just x', xtm) :: rest)          = if x == x'               then Just (xtm, reverse acc ++ rest)               else useAutoImp ((Just x', xtm) :: acc) rest      useAutoImp acc (ximp :: rest)          = useAutoImp (ximp :: acc) rest  processArgs fn ty [] [] = pure fn  processArgs fn ty exp imp     = throw (GenericMsg (getLoc fn)                 ("Badly formed impossible clause "                     ++ show (fn, exp, imp)))   buildApp : {auto c : Ref Ctxt Defs} ->             {auto q : Ref QVar Int} ->             FC -> Name -> Maybe (NF []) ->             (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->             Core ClosedTerm  buildApp fc n mty exp imp      = do defs <- get Ctxt           fi <- fromIntegerName           si <- fromStringName           ci <- fromCharName           when (Just n `elem` [fi, si,ci]) $               throw (InternalError "Can't deal with constants here yet")            tys <- lookupTyName n (gamma defs)           [(n', _, ty)] <- dropNoMatch mty tys              | [] => throw (UndefinedName fc n)              | ts => throw (AmbiguousName fc (map fst ts))           tynf <- nf defs [] ty           processArgs (Ref fc Func n') tynf exp imp   mkTerm : {auto c : Ref Ctxt Defs} ->            {auto q : Ref QVar Int} ->           RawImp -> Maybe (NF []) ->           (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->           Core ClosedTerm  mkTerm (IVar fc n) mty exp imp     = buildApp fc n mty exp imp  mkTerm (IApp fc fn arg) mty exp imp     = mkTerm fn mty (arg :: exp) imp  mkTerm (IImplicitApp fc fn nm arg) mty exp imp     = mkTerm fn mty exp ((nm, arg) :: imp)  mkTerm (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)  mkTerm tm _ _ _ = nextVar (getFC tm) -- Given an LHS that is declared 'impossible', build a term to match from,-- so that when we build the case tree for checking coverage, we take into-- account the impossible clausesexportgetImpossibleTerm : {auto c : Ref Ctxt Defs} ->                    Env Term vars -> RawImp -> Core ClosedTermgetImpossibleTerm env tm    = do q <- newRef QVar (the Int 0)         mkTerm (applyEnv tm) Nothing [] []  where    isLet : Binder (Term vars) -> Bool    isLet (Let _ _ _) = True    isLet _ = False     addEnv : FC -> Env Term vars -> List RawImp    addEnv fc [] = []    addEnv fc (b :: env) =       if isLet b          then addEnv fc env          else Implicit fc False :: addEnv fc env     -- Need to apply the function to the surrounding environment    applyEnv : RawImp -> RawImp    applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg    applyEnv (IImplicitApp fc fn n arg)        = IImplicitApp fc (applyEnv fn) n arg    applyEnv tm = apply tm (addEnv (getFC tm) env)