module Agda.Auto.Convert where import Control.Monad.Except import Control.Monad.State import Data.Bifunctor (first) import Data.IORef import Data.Maybe (catMaybes) import Data.Map (Map) import qualified Data.Map as Map import Agda.Syntax.Common (Hiding(..), getHiding, Arg) import Agda.Syntax.Concrete (exprFieldA) import qualified Agda.Syntax.Internal as I import Agda.Syntax.Internal (Dom'(..),domInfo,unDom) import qualified Agda.Syntax.Internal.Pattern as IP import qualified Agda.Syntax.Common as Cm import qualified Agda.Syntax.Abstract.Name as AN import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Position as SP import qualified Agda.TypeChecking.Monad.Base as MB import Agda.TypeChecking.Monad.Signature (getConstInfo, getDefFreeVars, ignoreAbstractMode) import Agda.TypeChecking.Level (reallyUnLevelView) import Agda.TypeChecking.Monad.Base (mvJudgement, mvPermutation, getMetaInfo, envContext, clEnv) import Agda.TypeChecking.Monad.MetaVars (lookupMeta, withMetaInfo, lookupInteractionPoint) import Agda.TypeChecking.Monad.Context (getContextArgs) import Agda.TypeChecking.Monad.Constraints (getAllConstraints) import Agda.TypeChecking.Substitute (applySubst, renamingR) import Agda.TypeChecking.Telescope (piApplyM) import qualified Agda.TypeChecking.Substitute as I (absBody) import Agda.TypeChecking.Reduce (normalise, instantiate) import Agda.TypeChecking.EtaContract (etaContract) import Agda.TypeChecking.Monad.Builtin (constructorForm) import Agda.TypeChecking.Free as Free (freeIn) import Agda.Interaction.MakeCase (getClauseZipperForIP) import Agda.Auto.NarrowingSearch import Agda.Auto.Syntax hiding (getConst) import Agda.Auto.CaseSplit hiding (lift) import Agda.Utils.Either import Agda.Utils.Lens import Agda.Utils.Monad ( forMaybeMM ) import Agda.Utils.Permutation ( Permutation(Perm), permute, takeP, compactP ) import Agda.Utils.Pretty ( prettyShow ) import Agda.Utils.Impossible data Hint = Hint { hintIsConstructor :: Bool , hintQName :: I.QName } type O = (Maybe (Int, [Arg AN.QName]),AN.QName) -- Nothing - Def -- Just npar - Con with npar parameters which don't appear in Agda data TMode = TMAll -- can be extended to distinguish between different modes (all, only def) deriving Eq type MapS a b = (Map a b, [a]) initMapS :: MapS a b initMapS = (Map.empty, []) popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b) popMapS r w = do (m, xs) <- gets r case xs of [] -> return Nothing (x:xs) -> do modify (w (m, xs)) return $ Just x data S = S {sConsts :: MapS AN.QName (TMode, ConstRef O), sMetas :: MapS I.MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [I.MetaId]), sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O)), sCurMeta :: Maybe I.MetaId, sMainMeta :: I.MetaId } type TOM = StateT S MB.TCM type MOT = ExceptT String IO tomy :: I.MetaId -> [Hint] -> [I.Type] -> MB.TCM ([ConstRef O] , [MExp O] , Map I.MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [I.MetaId]) , [(Bool, MExp O, MExp O)] , Map AN.QName (TMode, ConstRef O)) tomy imi icns typs = do eqs <- getEqs let r :: [AN.QName] -> TOM [AN.QName] r projfcns = do nxt <- popMapS sConsts (\x y -> y {sConsts = x}) case nxt of Just cn -> do cmap <- gets (fst . sConsts) let (mode, c) = cmap Map.! cn def <- lift $ getConstInfo cn let typ = MB.defType def defn = MB.theDef def typ <- lift $ normalise typ typ' <- convert typ let clausesToDef clauses = do clauses' <- convert clauses let narg = case clauses of [] -> 0 I.Clause {I.namedClausePats = xs} : _ -> length xs return (Def narg clauses' Nothing Nothing, []) (cont, projfcns2) <- case defn of MB.Axiom {} -> return (Postulate, []) MB.DataOrRecSig{} -> return (Postulate, []) MB.GeneralizableVar{} -> __IMPOSSIBLE__ MB.AbstractDefn{} -> return (Postulate, []) MB.Function {MB.funClauses = clauses} -> clausesToDef clauses -- MB.Primitive {MB.primClauses = []} -> throwError $ strMsg "Auto: Primitive functions are not supported" -- Andreas, 2013-06-17 breaks interaction/AutoMisc MB.Primitive {MB.primClauses = clauses} -> clausesToDef clauses MB.PrimitiveSort{} -> __IMPOSSIBLE__ MB.Datatype {MB.dataCons = cons} -> do cons2 <- mapM (\con -> getConst True con TMAll) cons return (Datatype cons2 [], []) MB.Record {MB.recFields = fields, MB.recTel = tel} -> do -- the value of recPars seems unreliable or don't know what it signifies let pars n (I.El _ (I.Pi it typ)) = Cm.Arg (I.domInfo it) (I.var n) : pars (n - 1) (I.unAbs typ) pars _ (I.El _ _) = [] contyp npar I.EmptyTel = I.El (I.mkType 0 {- arbitrary -}) $ I.Def cn $ map I.Apply $ pars (npar - 1) typ contyp npar (I.ExtendTel it (I.Abs v tel)) = I.El (I.mkType 0 {- arbitrary -}) (I.Pi it (I.Abs v (contyp (npar + 1) tel))) contyp npar (I.ExtendTel it I.NoAbs{}) = __IMPOSSIBLE__ contyp' <- convert $ contyp 0 tel cc <- lift $ liftIO $ readIORef c let Datatype [con] [] = cdcont cc lift $ liftIO $ modifyIORef con (\cdef -> cdef {cdtype = contyp'}) projfcns <- mapM (\ dom -> getConst False (I.unDom dom) TMAll) fields -- Equivalently projfcns <- mapM (($ TMAll) . getConst False . I.unDom) fields return (Datatype [con] projfcns, []{-map snd fields-}) MB.Constructor {MB.conData = dt} -> do _ <- getConst False dt TMAll -- make sure that datatype is included cc <- lift $ liftIO $ readIORef c let (Just (nomi,_), _) = cdorigin cc return (Constructor (nomi - cddeffreevars cc), []) lift $ liftIO $ modifyIORef c (\cdef -> cdef {cdtype = typ', cdcont = cont}) r $ projfcns2 ++ projfcns Nothing -> do nxt <- popMapS sMetas (\x y -> y {sMetas = x}) case nxt of Just mi -> do mapM_ (\((_, e, i), eqi) -> do when (fmExp mi e || fmExp mi i) $ do (eqsm, eqsl) <- gets sEqs when (Map.notMember eqi eqsm) $ do modify $ \s -> s {sEqs = (Map.insert eqi Nothing eqsm, eqi : eqsl)} ) (zip eqs [0..]) mv <- lift $ lookupMeta mi msol <- case MB.mvInstantiation mv of MB.InstV{} -> lift $ withMetaInfo (getMetaInfo mv) $ do args <- getContextArgs --sol <- norm (I.MetaV mi args) sol <- instantiate $ I.MetaV mi $ map I.Apply $ permute (takeP (length args) $ mvPermutation mv) args return $ Just sol _ -> return Nothing case msol of Nothing -> return () Just sol -> do m <- getMeta mi sol' <- convert sol modify $ \s -> s {sEqs = first (Map.insert (Map.size (fst $ sEqs s)) (Just (False, Meta m, sol'))) (sEqs s)} let tt = MB.jMetaType $ mvJudgement mv minfo = getMetaInfo mv localVars = map (snd . I.unDom) . envContext . clEnv $ minfo (targettype, localVars) <- lift $ withMetaInfo minfo $ do vs <- getContextArgs targettype <- tt `piApplyM` permute (takeP (length vs) $ mvPermutation mv) vs targettype <- normalise targettype localVars <- mapM normalise localVars return (targettype, localVars) modify (\s -> s {sCurMeta = Just mi}) typ' <- convert targettype ctx' <- mapM convert localVars modify (\s -> s {sCurMeta = Nothing}) modify (\s -> s {sMetas = first (Map.adjust (\(m, _, deps) -> (m, Just (typ', ctx'), deps)) mi) (sMetas s)}) r projfcns Nothing -> do nxt <- popMapS sEqs (\x y -> y {sEqs = x}) case nxt of Just eqi -> do let (ineq, e, i) = eqs !! eqi e' <- convert e i' <- convert i modify (\s -> s {sEqs = first (Map.adjust (\_ -> Just (ineq, e', i')) eqi) (sEqs s)}) r projfcns Nothing -> return projfcns ((icns', typs'), s) <- runStateT (do _ <- getMeta imi icns' <- mapM (\ (Hint iscon name) -> getConst iscon name TMAll) icns typs' <- mapM convert typs projfcns <- r [] projfcns' <- mapM (\name -> getConst False name TMAll) projfcns [] <- r [] return (projfcns' ++ icns', typs') ) (S {sConsts = initMapS, sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = imi}) lift $ liftIO $ mapM_ categorizedecl icns' return (icns', typs', Map.map flatten (fst (sMetas s)), map fromJust $ Map.elems (fst (sEqs s)), fst (sConsts s)) where flatten (x, Just (y, z), w) = (x, y, z, w) flatten (x, Nothing, w) = __IMPOSSIBLE__ fromJust (Just x) = x fromJust Nothing = __IMPOSSIBLE__ getConst :: Bool -> AN.QName -> TMode -> TOM (ConstRef O) getConst iscon name mode = do def <- lift $ getConstInfo name case MB.theDef def of MB.Record {MB.recConHead = con} -> do let conname = I.conName con conflds = I.conFields con cmap <- gets (fst . sConsts) case Map.lookup name cmap of Just (mode', c) -> if iscon then do cd <- lift $ liftIO $ readIORef c let Datatype [con] _ = cdcont cd return con else return c Nothing -> do mainm <- gets sMainMeta dfv <- lift $ getdfv mainm name let nomi = I.arity (MB.defType def) ccon <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name ++ ".CONS", cdorigin = (Just (nomi,conflds), conname), cdtype = __IMPOSSIBLE__, cdcont = Constructor (nomi - dfv), cddeffreevars = dfv}) -- ?? correct value of deffreevars for records? c <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name, cdorigin = (Nothing, name), cdtype = __IMPOSSIBLE__, cdcont = Datatype [ccon] [], cddeffreevars = dfv}) -- ?? correct value of deffreevars for records? modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))}) return $ if iscon then ccon else c _ -> do cmap <- gets (fst . sConsts) case Map.lookup name cmap of Just (mode', c) -> return c Nothing -> do (miscon, sname) <- if iscon then do let MB.Constructor {MB.conPars = npar, MB.conData = dname, MB.conSrcCon = ch} = MB.theDef def return (Just (npar,I.conFields ch), prettyShow dname ++ "." ++ prettyShow (I.qnameName name)) else return (Nothing, prettyShow name) mainm <- gets sMainMeta dfv <- lift $ getdfv mainm name c <- lift $ liftIO $ newIORef (ConstDef {cdname = sname, cdorigin = (miscon, name), cdtype = __IMPOSSIBLE__, cdcont = __IMPOSSIBLE__, cddeffreevars = dfv}) modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))}) return c getdfv :: I.MetaId -> A.QName -> MB.TCM Cm.Nat getdfv mainm name = do mv <- lookupMeta mainm withMetaInfo (getMetaInfo mv) $ getDefFreeVars name getMeta :: I.MetaId -> TOM (Metavar (Exp O) (RefInfo O)) getMeta name = do mmap <- gets (fst . sMetas) case Map.lookup name mmap of Just (m, _, _) -> return m Nothing -> do m <- lift $ liftIO initMeta modify $ \ s -> s { sMetas = (Map.insert name (m, Nothing, []) mmap, name : snd (sMetas s)) } return m getEqs :: MB.TCM [(Bool, I.Term, I.Term)] getEqs = forMaybeMM getAllConstraints $ \ eqc -> do neqc <- normalise eqc case MB.clValue $ MB.theConstraint neqc of MB.ValueCmp ineq _ i e -> do ei <- etaContract i ee <- etaContract e return $ Just (tomyIneq ineq, ee, ei) _ -> return Nothing copatternsNotImplemented :: MB.TCM a copatternsNotImplemented = MB.typeError $ MB.NotImplemented $ "The Agda synthesizer (Agsy) does not support copatterns yet" literalsNotImplemented :: MB.TCM a literalsNotImplemented = MB.typeError $ MB.NotImplemented $ "The Agda synthesizer (Agsy) does not support literals yet" hitsNotImplemented :: MB.TCM a hitsNotImplemented = MB.typeError $ MB.NotImplemented $ "The Agda synthesizer (Agsy) does not support HITs yet" class Conversion m a b where convert :: a -> m b instance Conversion TOM [I.Clause] [([Pat O], MExp O)] where convert = fmap catMaybes . mapM convert instance Conversion TOM I.Clause (Maybe ([Pat O], MExp O)) where convert cl = do let -- Jesper, 2016-07-28: -- I can't figure out if this should be the old or new -- clause body (i.e. relative to the positions of pattern variables or -- relative to the clauseTel). Both options pass the test suite, so I -- have the impression it doesn't actually matter. -- ALTERNATIVE CODE: -- perm = fromMaybe __IMPOSSIBLE__ $ IP.clausePerm cl -- body = applySubst (renamingR perm) $ I.clauseBody cl body = I.clauseBody cl pats = I.clausePats cl pats' <- mapM convert (IP.unnumberPatVars pats :: [Cm.Arg I.Pattern]) body' <- traverse convert =<< lift (normalise body) return $ (pats',) <$> body' instance Conversion TOM (Cm.Arg I.Pattern) (Pat O) where convert p = case Cm.unArg p of I.IApplyP _ _ _ n -> return $ PatVar (prettyShow n) I.VarP _ n -> return $ PatVar (prettyShow n) I.DotP _ _ -> return $ PatVar "_" -- because Agda includes these when referring to variables in the body I.ConP con _ pats -> do let n = I.conName con c <- getConst True n TMAll pats' <- mapM (convert . fmap Cm.namedThing) pats def <- lift $ getConstInfo n cc <- lift $ liftIO $ readIORef c let Just (npar,_) = fst $ cdorigin cc return $ PatConApp c (replicate npar PatExp ++ pats') -- UNSUPPORTED CASES I.ProjP{} -> lift copatternsNotImplemented I.LitP{} -> lift literalsNotImplemented I.DefP{} -> lift hitsNotImplemented instance Conversion TOM I.Type (MExp O) where convert (I.El _ t) = convert t -- sort info is thrown away instance Conversion TOM I.Term (MExp O) where convert v0 = case I.unSpine v0 of I.Var v es -> do let Just as = I.allApplyElims es as' <- convert as return $ NotM $ App Nothing (NotM OKVal) (Var v) as' I.Lam info b -> do b' <- convert (I.absBody b) return $ NotM $ Lam (getHiding info) (Abs (Id $ I.absName b) b') t@I.Lit{} -> do t <- lift $ constructorForm t case t of I.Lit{} -> lift literalsNotImplemented _ -> convert t I.Level l -> convert =<< lift (reallyUnLevelView l) I.Def name es -> do let Just as = I.allApplyElims es c <- getConst False name TMAll as' <- convert as return $ NotM $ App Nothing (NotM OKVal) (Const c) as' I.Con con ci es -> do let Just as = I.allApplyElims es let name = I.conName con c <- getConst True name TMAll as' <- convert as def <- lift $ getConstInfo name cc <- lift $ liftIO $ readIORef c let Just (npar,_) = fst $ cdorigin cc return $ NotM $ App Nothing (NotM OKVal) (Const c) (foldl (\x _ -> NotM $ ALConPar x) as' [1..npar]) I.Pi (I.Dom{domInfo = info, unDom = x}) b -> do let y = I.absBody b name = I.absName b x' <- convert x y' <- convert y return $ NotM $ Pi Nothing (getHiding info) (Free.freeIn 0 y) x' (Abs (Id name) y') I.Sort (I.Type (I.ClosedLevel l)) -> return $ NotM $ Sort $ Set $ fromIntegral l I.Sort _ -> return $ NotM $ Sort UnknownSort I.Dummy{}-> return $ NotM $ Sort UnknownSort t@I.MetaV{} -> do t <- lift $ instantiate t case t of I.MetaV mid _ -> do mcurmeta <- gets sCurMeta case mcurmeta of Nothing -> return () Just curmeta -> modify $ \ s -> s { sMetas = first (Map.adjust (\(m, x, deps) -> (m, x, mid : deps)) curmeta) (sMetas s) } m <- getMeta mid return $ Meta m _ -> convert t I.DontCare _ -> return $ NotM dontCare instance Conversion TOM a b => Conversion TOM (Cm.Arg a) (Hiding, b) where convert (Cm.Arg info a) = (getHiding info,) <$> convert a instance Conversion TOM I.Args (MM (ArgList O) (RefInfo O)) where convert as = NotM . foldr (\ (hid,t) -> ALCons hid t . NotM) ALNil <$> mapM convert as tomyIneq :: MB.Comparison -> Bool tomyIneq MB.CmpEq = False tomyIneq MB.CmpLeq = True -- --------------------------------------------- fmType :: I.MetaId -> I.Type -> Bool fmType m (I.El _ t) = fmExp m t fmExp :: I.MetaId -> I.Term -> Bool fmExp m (I.Var _ as) = fmExps m $ I.argsFromElims as fmExp m (I.Lam _ b) = fmExp m (I.unAbs b) fmExp m (I.Lit _) = False fmExp m (I.Level (I.Max _ as)) = any (fmLevel m) as fmExp m (I.Def _ as) = fmExps m $ I.argsFromElims as fmExp m (I.Con _ ci as) = fmExps m $ I.argsFromElims as fmExp m (I.Pi x y) = fmType m (I.unDom x) || fmType m (I.unAbs y) fmExp m (I.Sort _) = False fmExp m (I.MetaV mid _) = mid == m fmExp m (I.DontCare _) = False fmExp _ I.Dummy{} = False fmExps :: I.MetaId -> I.Args -> Bool fmExps m as = any (fmExp m . Cm.unArg) as fmLevel :: I.MetaId -> I.PlusLevel -> Bool fmLevel m (I.Plus _ l) = fmExp m l -- --------------------------------------------- icnvh :: Hiding -> Cm.ArgInfo icnvh h = Cm.setHiding h $ Cm.setOrigin o $ Cm.defaultArgInfo where -- Andreas, 2017-01-18, issue #819. -- Visible arguments are made UserWritten, -- otherwise they might not be printed in patterns. o = case h of NotHidden -> Cm.UserWritten Instance{} -> Cm.Inserted Hidden -> Cm.Inserted -- --------------------------------------------- instance Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b where convert meta = case meta of NotM a -> convert a Meta m -> do ma <- lift $ readIORef $ mbind m case ma of Nothing -> throwError "meta not bound" Just a -> convert a instance Conversion MOT a b => Conversion MOT (Abs a) (I.Abs b) where convert (Abs mid t) = I.Abs id <$> convert t where id = case mid of NoId -> "x" Id id -> id instance Conversion MOT (Exp O) I.Type where convert e = I.El (I.mkType 0) <$> convert e -- 0 is arbitrary, sort not read by Agda when reifying instance Conversion MOT (Exp O) I.Term where convert = \case App _ _ (Var v) as -> frommyExps 0 as (I.Var v []) App _ _ (Const c) as -> do cdef <- lift $ readIORef c let (iscon, name) = cdorigin cdef {- case iscon of Just n -> do v <- getConTerm name -- We are not in TCM frommyExps n as v -} (ndrop, h) = case iscon of Just (n,fs) -> (n, \ q -> I.Con (I.ConHead q I.IsData Cm.Inductive fs) Cm.ConOSystem) Nothing -> (0, \ f vs -> I.Def f vs) frommyExps ndrop as (h name []) Lam hid t -> I.Lam (icnvh hid) <$> convert t Pi _ hid _ x y -> do x' <- convert x let dom = (I.defaultDom x') {domInfo = icnvh hid} I.Pi dom <$> convert y -- maybe have case for Pi where possdep is False which produces Fun (and has to unweaken y), return $ I.Fun (Cm.Arg (icnvh hid) x') y' Sort (Set l) -> return $ I.Sort (I.mkType (fromIntegral l)) Sort Type -> __IMPOSSIBLE__ Sort UnknownSort -> return $ I.Sort (I.mkType 0) -- hoping it's thrown away AbsurdLambda hid -> return $ I.Lam (icnvh hid) $ I.Abs abslamvarname (I.Var 0 []) frommyExps :: Nat -> MArgList O -> I.Term -> ExceptT String IO I.Term frommyExps ndrop (Meta m) trm = do bind <- lift $ readIORef $ mbind m case bind of Nothing -> throwError "meta not bound" Just e -> frommyExps ndrop (NotM e) trm frommyExps ndrop (NotM as) trm = case as of ALNil -> return trm ALCons _ _ xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm ALCons hid x xs -> do x' <- convert x frommyExps ndrop xs (addend (Cm.Arg (icnvh hid) x') trm) -- Andreas, 2013-10-19 TODO: restore postfix projections ALProj eas idx hid xs -> do idx <- lift $ expandbind idx c <- case idx of NotM c -> return c Meta{} -> throwError "meta not bound" cdef <- lift $ readIORef c let name = snd $ cdorigin cdef trm2 <- frommyExps 0 eas (I.Def name []) frommyExps 0 xs (addend (Cm.Arg (icnvh hid) trm) trm2) ALConPar xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm ALConPar _ -> __IMPOSSIBLE__ where addend x (I.Var h xs) = I.Var h (xs ++ [I.Apply x]) addend x (I.Con h ci xs) = I.Con h ci (xs ++ [I.Apply x]) addend x (I.Def h xs) = I.Def h (xs ++ [I.Apply x]) addend _ _ = __IMPOSSIBLE__ -- -------------------------------- abslamvarname :: String abslamvarname = "\0absurdlambda" modifyAbstractExpr :: A.Expr -> A.Expr modifyAbstractExpr = f where f (A.App i e1 (Cm.Arg info (Cm.Named n e2))) = A.App i (f e1) (Cm.Arg info (Cm.Named n (f e2))) f (A.Lam i (A.DomainFree _ x) _) | A.Binder _ (A.BindName{unBind = n}) <- Cm.namedArg x , prettyShow (A.nameConcrete n) == abslamvarname = A.AbsurdLam i $ Cm.getHiding x f (A.Lam i b e) = A.Lam i b (f e) f (A.Rec i xs) = A.Rec i (map (mapLeft (over exprFieldA f)) xs) f (A.RecUpdate i e xs) = A.RecUpdate i (f e) (map (over exprFieldA f) xs) f (A.ScopedExpr i e) = A.ScopedExpr i (f e) f e = e modifyAbstractClause :: A.Clause -> A.Clause modifyAbstractClause (A.Clause lhs spats (A.RHS e mc) decls catchall) = A.Clause lhs spats (A.RHS (modifyAbstractExpr e) mc) decls catchall modifyAbstractClause cl = cl -- --------------------------------- constructPats :: Map AN.QName (TMode, ConstRef O) -> I.MetaId -> I.Clause -> MB.TCM ([(Hiding, MId)], [CSPat O]) constructPats cmap mainm clause = do let cnvps ns [] = return (ns, []) cnvps ns (p : ps) = do (ns', ps') <- cnvps ns ps (ns'', p') <- cnvp ns' p return (ns'', p' : ps') cnvp ns p = let hid = getHiding $ Cm.argInfo p in case Cm.namedArg p of I.VarP _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns)) I.IApplyP _ _ _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns)) I.ConP con _ ps -> do let c = I.conName con (c2, _) <- runStateT (getConst True c TMAll) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm}) (ns', ps') <- cnvps ns ps cc <- liftIO $ readIORef c2 let Just (npar,_) = fst $ cdorigin cc return (ns', HI hid (CSPatConApp c2 (replicate npar (HI Hidden CSOmittedArg) ++ ps'))) I.DotP _ t -> do (t2, _) <- runStateT (convert t) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm}) return (ns, HI hid (CSPatExp t2)) I.ProjP{} -> copatternsNotImplemented I.LitP{} -> literalsNotImplemented I.DefP{} -> hitsNotImplemented (names, pats) <- cnvps [] (IP.unnumberPatVars $ I.namedClausePats clause) return (reverse names, pats) frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO I.Clause frommyClause (ids, pats, mrhs) = do let ctel [] = return I.EmptyTel ctel (HI hid (mid, t) : ctx) = do let Id id = mid tel <- ctel ctx t' <- convert t let dom = (I.defaultDom t') {domInfo = icnvh hid} return $ I.ExtendTel dom (I.Abs id tel) tel <- ctel $ reverse ids let getperms 0 [] perm nv = return (perm, nv) getperms n [] _ _ = __IMPOSSIBLE__ getperms 0 (p : ps) perm nv = do (perm, nv) <- getperm p perm nv getperms 0 ps perm nv getperms n (HI _ CSPatExp{} : ps) perm nv = getperms (n - 1) ps perm nv getperms n (HI _ CSOmittedArg{} : ps) perm nv = getperms (n - 1) ps perm nv getperms n (_ : _) _ _ = __IMPOSSIBLE__ getperm (HI _ p) perm nv = case p of --CSPatVar v -> return (length ids + nv - 1 - v : perm, nv) CSPatVar v -> return ((length ids - 1 - v, nv) : perm, nv + 1) CSPatConApp c ps -> do cdef <- lift $ readIORef c let (Just (ndrop,_), _) = cdorigin cdef getperms ndrop ps perm nv CSPatExp e -> return (perm, nv + 1) _ -> __IMPOSSIBLE__ (rperm, nv) <- getperms 0 pats [] 0 let --perm = reverse rperm perm = map (\i -> let Just x = lookup i rperm in x) [0..length ids - 1] --renperm = map (\i -> length ids + nv - 1 - i) rperm --renm = rename (\i -> renperm !! i) cnvps 0 [] = return [] cnvps n [] = __IMPOSSIBLE__ cnvps 0 (p : ps) = do p' <- cnvp p ps' <- cnvps 0 ps return (p' : ps') cnvps n (HI _ CSPatExp{} : ps) = cnvps (n - 1) ps cnvps n (HI _ CSOmittedArg{} : ps) = cnvps (n - 1) ps cnvps n (_ : _) = __IMPOSSIBLE__ cnvp (HI hid p) = do p' <- case p of CSPatVar v -> return (I.varP $ let HI _ (Id n, _) = ids !! v in n) CSPatConApp c ps -> do cdef <- lift $ readIORef c let (Just (ndrop,_), name) = cdorigin cdef ps' <- cnvps ndrop ps let con = I.ConHead name I.IsData Cm.Inductive [] -- TODO: restore DataOrRecord and record fields! return (I.ConP con I.noConPatternInfo ps') CSPatExp e -> do e' <- convert e {- renm e -} -- renaming before adding to clause below return (I.dotP e') CSAbsurd -> __IMPOSSIBLE__ -- CSAbsurd not used _ -> __IMPOSSIBLE__ return $ Cm.Arg (icnvh hid) $ Cm.unnamed p' -- TODO: recover names ps <- cnvps 0 pats body <- case mrhs of Nothing -> return $ Nothing Just e -> Just <$> convert e let cperm = Perm nv perm return $ I.Clause { I.clauseLHSRange = SP.noRange , I.clauseFullRange = SP.noRange , I.clauseTel = tel , I.namedClausePats = IP.numberPatVars __IMPOSSIBLE__ cperm $ applySubst (renamingR $ compactP cperm) ps , I.clauseBody = body , I.clauseType = Nothing -- TODO: compute clause type , I.clauseCatchall = False , I.clauseExact = Nothing -- TODO , I.clauseRecursive = Nothing -- TODO: Don't know here whether recursive or not !? , I.clauseUnreachable = Nothing -- TODO: Don't know here whether reachable or not !? , I.clauseEllipsis = Cm.NoEllipsis } contains_constructor :: [CSPat O] -> Bool contains_constructor = any f where f (HI _ p) = case p of CSPatConApp{} -> True _ -> False -- --------------------------------- freeIn :: Nat -> MExp o -> Bool freeIn = f where mr x = let NotM x' = x in x' f v e = case mr e of App _ _ elr args -> case elr of Var v' | v' == v -> False _ -> fs v args Lam _ (Abs _ b) -> f (v + 1) b Pi _ _ _ it (Abs _ ot) -> f v it && f (v + 1) ot Sort{} -> True AbsurdLambda{} -> True fs v es = case mr es of ALNil -> True ALCons _ a as -> f v a && fs v as ALProj{} -> __IMPOSSIBLE__ ALConPar as -> fs v as negtype :: ConstRef o -> MExp o -> MExp o negtype ee = f (0 :: Int) where mr x = let NotM x' = x in x' f n e = case mr e of Pi uid hid possdep it (Abs id ot) -> NotM $ Pi uid hid possdep it (Abs id (f (n + 1) ot)) _ -> NotM $ Pi Nothing NotHidden False (NotM $ Pi Nothing NotHidden False e (Abs NoId (NotM $ Pi Nothing NotHidden True (NotM $ Sort (Set 0)) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)))))) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Const ee) (NotM ALNil))) -- --------------------------------------- findClauseDeep :: Cm.InteractionId -> MB.TCM (Maybe (AN.QName, I.Clause, Bool)) findClauseDeep ii = ignoreAbstractMode $ do -- Andreas, 2016-09-04, issue #2162 MB.InteractionPoint { MB.ipClause = ipCl} <- lookupInteractionPoint ii case ipCl of MB.IPNoClause -> return Nothing MB.IPClause f clauseNo _ _ _ _ _ -> do (_, (_, c, _)) <- getClauseZipperForIP f clauseNo return $ Just (f, c, maybe __IMPOSSIBLE__ toplevel $ I.clauseBody c) where toplevel e = case e of I.MetaV{} -> True _ -> False -- --------------------------------------- matchType :: Int -> Int -> I.Type -> I.Type -> Maybe (Nat, Nat) -- Nat is deffreevars of const, Nat is ctx length of target type, left arg is const type, right is target type matchType cdfv tctx ctyp ttyp = trmodps cdfv ctyp where trmodps 0 ctyp = tr 0 0 ctyp trmodps n ctyp = case I.unEl ctyp of I.Pi _ ot -> trmodps (n - 1) (I.absBody ot) _ -> __IMPOSSIBLE__ tr narg na ctyp = case ft 0 0 Just ctyp ttyp of Just n -> Just (n, narg) Nothing -> case I.unEl ctyp of I.Pi _ (I.Abs _ ot) -> tr (narg + 1) (na + 1) ot I.Pi _ (I.NoAbs _ ot) -> tr (narg + 1) na ot _ -> Nothing where ft nl n c (I.El _ e1) (I.El _ e2) = f nl n c e1 e2 f nl n c e1 e2 = case e1 of I.Var v1 as1 | v1 < nl -> case e2 of I.Var v2 as2 | v1 == v2 -> fes nl (n + 1) c as1 as2 _ -> Nothing I.Var v1 _ | v1 < nl + na -> c n -- unify vars with no args? I.Var v1 as1 -> case e2 of I.Var v2 as2 | cdfv + na + nl - v1 == tctx + nl - v2 -> fes nl (n + 1) c as1 as2 _ -> Nothing _ -> case (e1, e2) of (I.MetaV{}, _) -> c n (_, I.MetaV{}) -> c n (I.Lam hid1 b1, I.Lam hid2 b2) | hid1 == hid2 -> f (nl + 1) n c (I.absBody b1) (I.absBody b2) (I.Lit lit1, I.Lit lit2) | lit1 == lit2 -> c (n + 1) (I.Def n1 as1, I.Def n2 as2) | n1 == n2 -> fes nl (n + 1) c as1 as2 (I.Con n1 _ as1, I.Con n2 _ as2) | n1 == n2 -> fs nl (n + 1) c as1 as2 (I.Pi (I.Dom{domInfo = info1, unDom = it1}) ot1, I.Pi (I.Dom{domInfo = info2, unDom = it2}) ot2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> ft nl n (\n -> ft (nl + 1) n c (I.absBody ot1) (I.absBody ot2)) it1 it2 (I.Sort{}, I.Sort{}) -> c n -- sloppy _ -> Nothing fs nl n c es1 es2 = case (es1, es2) of ([], []) -> c n (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fs nl n c es1 es2) e1 e2 _ -> Nothing fes nl n c es1 es2 = case (es1, es2) of ([], []) -> c n (I.Proj _ f : es1, I.Proj _ f' : es2) | f == f' -> fes nl n c es1 es2 (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fes nl n c es1 es2) e1 e2 _ -> Nothing