{-# LANGUAGE CPP #-}
module Agda.Auto.Convert where
import Control.Applicative hiding (getConst, Const(..))
import Data.IORef
import Data.Maybe (catMaybes)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable (traverse)
import Control.Monad.State
import Agda.Syntax.Common (Hiding(..), getHiding)
import Agda.Syntax.Concrete (exprFieldA)
import qualified Agda.Syntax.Internal as I
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.Utils.Permutation (Permutation(Perm), permute, takeP, compactP)
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.TypeChecking.Errors ( stringTCErr )
import Agda.Interaction.MakeCase (getClauseForIP)
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax hiding (getConst)
import Agda.Auto.CaseSplit hiding (lift)
import Agda.Utils.Either
import Agda.Utils.Except ( ExceptT , MonadError(throwError) )
import Agda.Utils.Lens
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Impossible
#include "undefined.h"
data Hint = Hint
{ hintIsConstructor :: Bool
, hintQName :: I.QName
}
type O = (Maybe Int, AN.QName)
data TMode = TMAll
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 <- fst `liftM` gets 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.AbstractDefn{} -> return (Postulate, [])
MB.Function {MB.funClauses = clauses} -> clausesToDef clauses
MB.Primitive {MB.primClauses = clauses} -> clausesToDef clauses
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
let pars n (I.El _ (I.Pi it typ)) = Cm.Arg (Cm.domInfo it) (I.var n) :
pars (n - 1) (I.unAbs typ)
pars _ (I.El _ _) = []
contyp npar I.EmptyTel = I.El (I.mkType 0 ) $
I.Def cn $ map I.Apply $ pars (npar - 1) typ
contyp npar (I.ExtendTel it (I.Abs v tel)) = I.El (I.mkType 0 ) (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 (\name -> getConst False name TMAll) (map Cm.unArg fields)
return (Datatype [con] projfcns, [])
MB.Constructor {MB.conData = dt} -> do
_ <- getConst False dt TMAll
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 <- 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 = (Map.insert (Map.size (fst $ sEqs s)) (Just (False, Meta m, sol')) (fst $ sEqs s), snd $ sEqs s)}
let tt = MB.jMetaType $ mvJudgement mv
minfo = getMetaInfo mv
localVars = map (snd . Cm.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 = (Map.adjust (\(m, _, deps) -> (m, Just (typ', ctx'), deps)) mi (fst $ sMetas s), snd $ 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 = (Map.adjust (\_ -> Just (ineq, e', i')) eqi (fst $ sEqs s), snd $ 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
cmap <- fst `liftM` gets 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, conname), cdtype = __IMPOSSIBLE__, cdcont = Constructor (nomi - dfv), cddeffreevars = dfv})
c <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name, cdorigin = (Nothing, name), cdtype = __IMPOSSIBLE__, cdcont = Datatype [ccon] [], cddeffreevars = dfv})
modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))})
return $ if iscon then ccon else c
_ -> do
cmap <- fst `liftM` gets 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.theDef def
return (Just npar, 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 <- fst `liftM` gets 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 = do
eqs <- getAllConstraints
let r = mapM (\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 [(tomyIneq ineq, ee, ei)]
MB.TypeCmp ineq i e -> do
I.El _ ei <- etaContract i
I.El _ ee <- etaContract e
return [(tomyIneq ineq, ee, ei)]
MB.Guarded (MB.UnBlock _) pid -> return []
_ -> return []
)
eqs' <- r eqs
return $ concat eqs'
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"
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
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.VarP _ n -> return $ PatVar (show n)
I.DotP _ _ -> return $ PatVar "_"
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')
I.ProjP{} -> lift copatternsNotImplemented
I.LitP _ -> lift literalsNotImplemented
instance Conversion TOM I.Type (MExp O) where
convert (I.El _ t) = convert t
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 (Cm.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.Max [I.ClosedLevel l])) -> return $ NotM $ Sort $ Set $ fromIntegral l
I.Sort _ -> 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 = ( Map.adjust (\(m, x, deps) -> (m, x, mid : deps)) curmeta (fst $ sMetas s)
, snd $ 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 (Cm.unDom x) || fmType m (I.unAbs y)
fmExp m (I.Sort _) = False
fmExp m (I.MetaV mid _) = mid == m
fmExp m (I.DontCare _) = False
fmExps :: I.MetaId -> I.Args -> Bool
fmExps m [] = False
fmExps m (a : as) = fmExp m (Cm.unArg a) || fmExps m as
fmLevel :: I.MetaId -> I.PlusLevel -> Bool
fmLevel m I.ClosedLevel{} = False
fmLevel m (I.Plus _ l) = case l of
I.MetaLevel m' _ -> m == m'
I.NeutralLevel _ v -> fmExp m v
I.BlockedLevel _ v -> fmExp m v
I.UnreducedLevel v -> fmExp m v
icnvh :: Hiding -> Cm.ArgInfo
icnvh h = Cm.setHiding h $
Cm.setOrigin o $
Cm.defaultArgInfo
where
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
instance Conversion MOT (Exp O) I.Term where
convert e = case e of
App _ _ (Var v) as -> frommyExps 0 as (I.Var v [])
App _ _ (Const c) as -> do
cdef <- lift $ readIORef c
let (iscon, name) = cdorigin cdef
(ndrop, h) = case iscon of
Just n -> (n, \ q -> I.Con (I.ConHead q Cm.Inductive []) 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 -> I.Pi . Cm.Dom (icnvh hid) <$> convert x <*> convert y
Sort (Set l) -> return $ I.Sort (I.mkType (fromIntegral l))
Sort Type -> __IMPOSSIBLE__
Sort UnknownSort -> return $ I.Sort (I.mkType 0)
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)
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 info (A.BindName n)) _)
| prettyShow (A.nameConcrete n) == abslamvarname =
A.AbsurdLam i $ Cm.argInfoHiding info
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.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
(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
return $ I.ExtendTel (Cm.Dom (icnvh hid) t') (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 - 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 = map (\i -> let Just x = lookup i rperm in x) [0..length ids - 1]
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 Cm.Inductive []
return (I.ConP con I.noConPatternInfo ps')
CSPatExp e -> do
e' <- convert e
return (I.dotP e')
CSAbsurd -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
return $ Cm.Arg (icnvh hid) $ Cm.unnamed p'
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
, I.clauseCatchall = False
, I.clauseUnreachable = Nothing
}
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
MB.InteractionPoint { MB.ipClause = ipCl} <- lookupInteractionPoint ii
case ipCl of
MB.IPNoClause -> return Nothing
MB.IPClause f clauseNo _ -> do
(_, c, _) <- getClauseForIP 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)
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
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 (Cm.Dom{domInfo = info1, unDom = it1}) ot1, I.Pi (Cm.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
_ -> 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