module TTImp.Impossible import Core.Context import Core.Env import Core.Normalise import Core.TT import 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 Bool match 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 ts dropNoMatch (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 clauses export getImpossibleTerm : {auto c : Ref Ctxt Defs} -> Env Term vars -> RawImp -> Core ClosedTerm getImpossibleTerm 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)