{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
import Idris.AbsSyntax
import Idris.Core.Elaborate
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
import Idris.Error
import Control.Monad
import Control.Monad.State.Strict
elabRewrite :: (PTerm -> ElabD ()) -> IState ->
FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()
elabRewrite :: (PTerm -> ElabD ())
-> IState
-> FC
-> Maybe Name
-> PTerm
-> PTerm
-> Maybe PTerm
-> ElabD ()
elabRewrite PTerm -> ElabD ()
elab IState
ist FC
fc Maybe Name
substfn_in PTerm
rule PTerm
sc_in Maybe PTerm
newg
= do ElabD ()
forall aux. Elab' aux ()
attack
PTerm
sc <- case Maybe PTerm
newg of
Maybe PTerm
Nothing -> PTerm -> StateT (ElabState EState) TC PTerm
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
sc_in
Just PTerm
t -> do
Name
letn <- Name -> Elab' EState Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rewrite_result")
PTerm -> StateT (ElabState EState) TC PTerm
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> StateT (ElabState EState) TC PTerm)
-> PTerm -> StateT (ElabState EState) TC PTerm
forall a b. (a -> b) -> a -> b
$ FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW Name
letn FC
fc PTerm
t PTerm
sc_in
(FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
letn)
Name
tyn <- Name -> Elab' EState Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rty")
Name -> Raw -> ElabD ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
tyn Raw
RType
Name
valn <- Name -> Elab' EState Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rval")
Name -> Raw -> ElabD ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
valn (Name -> Raw
Var Name
tyn)
Name
letn <- Name -> Elab' EState Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"_rewrite_rule")
Name -> RigCount -> Raw -> Raw -> ElabD ()
forall aux. Name -> RigCount -> Raw -> Raw -> Elab' aux ()
letbind Name
letn RigCount
RigW (Name -> Raw
Var Name
tyn) (Name -> Raw
Var Name
valn)
Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
valn
PTerm -> ElabD ()
elab PTerm
rule
ElabD ()
forall aux. Elab' aux ()
compute
Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
(Type
tmv, Type
rule_in) <- Raw -> Elab' EState (Type, Type)
forall aux. Raw -> Elab' aux (Type, Type)
get_type_val (Name -> Raw
Var Name
letn)
Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
let ttrule :: Type
ttrule = Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) Env
env Type
rule_in
Name
rname <- Name -> Elab' EState Name
forall aux. Name -> Elab' aux Name
unique_hole (Int -> String -> Name
sMN Int
0 String
"replaced")
case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ttrule of
(P NameType
_ (UN Text
q) Type
_, [Type
lt, Type
rt, Type
l, Type
r]) | Text
q Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
do Name
substfn <- Maybe Name -> IState -> Type -> Type -> Elab' EState Name
findSubstFn Maybe Name
substfn_in IState
ist Type
lt Type
rt
let pred_tt :: Type
pred_tt = Type -> Type -> Type -> Type -> Type
mkP (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
rname Type
rt) Type
l Type
r Type
g
Bool -> ElabD () -> ElabD ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
g Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
pred_tt) (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ TC () -> ElabD ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> ElabD ()) -> TC () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Type -> Type -> Type -> Err
forall t. t -> t -> t -> Err' t
NoRewriting Type
l Type
r Type
g)
let pred :: PTerm
pred = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
rname FC
fc PTerm
Placeholder
(IState -> Type -> PTerm
delab IState
ist Type
pred_tt)
let rewrite :: PTerm
rewrite = IState -> [Name] -> PTerm -> PTerm
addImplBound IState
ist (((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
substfn)
[PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PTerm
stripImpls PTerm
pred),
PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PTerm
stripImpls PTerm
rule), PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
sc])
PTerm -> ElabD ()
elab PTerm
rewrite
ElabD ()
forall aux. Elab' aux ()
solve
(Type, [Type])
_ -> TC () -> ElabD ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> ElabD ()) -> TC () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Type -> Type -> Err
forall t. t -> t -> Err' t
NotEquality Type
tmv Type
ttrule)
where
mkP :: TT Name ->
TT Name -> TT Name -> TT Name -> TT Name
mkP :: Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
ty | Type
l Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty = Type
lt
mkP Type
lt Type
l Type
r (App AppStatus Name
s Type
f Type
a)
= let f' :: Type
f' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
f) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
f else Type
f
a' :: Type
a' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
a) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
a else Type
a in
AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f' Type
a'
mkP Type
lt Type
l Type
r (Bind Name
n Binder Type
b Type
sc)
= let b' :: Binder Type
b' = Binder Type -> Binder Type
mkPB Binder Type
b
sc' :: Type
sc' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
sc) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
sc else Type
sc in
Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Type
b' Type
sc'
where mkPB :: Binder Type -> Binder Type
mkPB (Let RigCount
rig Type
t Type
v)
= let t' :: Type
t' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
t else Type
t
v' :: Type
v' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
v) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
v else Type
v in
RigCount -> Type -> Type -> Binder Type
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Type
t' Type
v'
mkPB Binder Type
b = let ty :: Type
ty = Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b
ty' :: Type
ty' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ty) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
ty else Type
ty in
Binder Type
b { binderTy = ty' }
mkP Type
lt Type
l Type
r Type
x = Type
x
stripImpls :: PTerm -> PTerm
stripImpls PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
phApps PTerm
tm
phApps :: PTerm -> PTerm
phApps (PApp FC
fc PTerm
f [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
removeImp [PArg]
args)
where removeImp :: PArg -> PArg
removeImp tm :: PArg
tm@(PImp{}) = PArg
tm { getTm = Placeholder }
removeImp PArg
t = PArg
t
phApps PTerm
tm = PTerm
tm
findSubstFn :: Maybe Name -> IState -> Type -> Type -> ElabD Name
findSubstFn :: Maybe Name -> IState -> Type -> Type -> Elab' EState Name
findSubstFn Maybe Name
Nothing IState
ist Type
lt Type
rt
| Type
lt Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
rt = Name -> Elab' EState Name
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
sUN String
"rewrite__impl")
| (P NameType
_ Name
lcon Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
lt,
(P NameType
_ Name
rcon Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
rt,
Name
lcon Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rcon
= case Name -> Context -> Maybe Type
lookupTyExact (Name -> Name
rewrite_name Name
lcon) (IState -> Context
tt_ctxt IState
ist) of
Just Type
_ -> Name -> Elab' EState Name
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Name
rewrite_name Name
lcon)
Maybe Type
Nothing -> Type -> Type -> Elab' EState Name
forall {t :: (* -> *) -> * -> *} {a}.
MonadTrans t =>
Type -> Type -> t TC a
rewriteFail Type
lt Type
rt
| Bool
otherwise = Type -> Type -> Elab' EState Name
forall {t :: (* -> *) -> * -> *} {a}.
MonadTrans t =>
Type -> Type -> t TC a
rewriteFail Type
lt Type
rt
where rewriteFail :: Type -> Type -> t TC a
rewriteFail Type
lt Type
rt = TC a -> t TC a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> t TC a) -> (String -> TC a) -> String -> t TC a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC a
forall a. Err -> TC a
tfail (Err -> TC a) -> (String -> Err) -> String -> TC a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> Err
forall t. String -> Err' t
Msg (String -> t TC a) -> String -> t TC a
forall a b. (a -> b) -> a -> b
$ String
"Can't rewrite heterogeneous equality on types " String -> String -> String
forall a. [a] -> [a] -> [a]
++
PTerm -> String
forall a. Show a => a -> String
show (IState -> Type -> PTerm
delab IState
ist Type
lt) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show (IState -> Type -> PTerm
delab IState
ist Type
rt)
findSubstFn (Just Name
substfn_in) IState
ist Type
lt Type
rt
= case Name -> Context -> [(Name, Type)]
lookupTyName Name
substfn_in (IState -> Context
tt_ctxt IState
ist) of
[(Name
n, Type
t)] -> Name -> Elab' EState Name
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
[] -> TC Name -> Elab' EState Name
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Name -> Elab' EState Name)
-> (Name -> TC Name) -> Name -> Elab' EState Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC Name
forall a. Err -> TC a
tfail (Err -> TC Name) -> (Name -> Err) -> Name -> TC Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Err
forall t. Name -> Err' t
NoSuchVariable (Name -> Elab' EState Name) -> Name -> Elab' EState Name
forall a b. (a -> b) -> a -> b
$ Name
substfn_in
[(Name, Type)]
more -> TC Name -> Elab' EState Name
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Name -> Elab' EState Name)
-> ([Name] -> TC Name) -> [Name] -> Elab' EState Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC Name
forall a. Err -> TC a
tfail (Err -> TC Name) -> ([Name] -> Err) -> [Name] -> TC Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts ([Name] -> Elab' EState Name) -> [Name] -> Elab' EState Name
forall a b. (a -> b) -> a -> b
$ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
more
rewrite_name :: Name -> Name
rewrite_name :: Name -> Name
rewrite_name Name
n = Int -> String -> Name
sMN Int
0 (Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_rewrite_lemma")
data ParamInfo = Index
| Param
| ImplicitIndex
| ImplicitParam
deriving Int -> ParamInfo -> String -> String
[ParamInfo] -> String -> String
ParamInfo -> String
(Int -> ParamInfo -> String -> String)
-> (ParamInfo -> String)
-> ([ParamInfo] -> String -> String)
-> Show ParamInfo
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ParamInfo -> String -> String
showsPrec :: Int -> ParamInfo -> String -> String
$cshow :: ParamInfo -> String
show :: ParamInfo -> String
$cshowList :: [ParamInfo] -> String -> String
showList :: [ParamInfo] -> String -> String
Show
getParamInfo :: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo :: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) (PExp{} : [PArg]
is) Int
i [Int]
ps
| Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = ParamInfo
Param ParamInfo -> [ParamInfo] -> [ParamInfo]
forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
| Bool
otherwise = ParamInfo
Index ParamInfo -> [ParamInfo] -> [ParamInfo]
forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
getParamInfo (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) (PArg
_ : [PArg]
is) Int
i [Int]
ps
| Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = ParamInfo
ImplicitParam ParamInfo -> [ParamInfo] -> [ParamInfo]
forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
| Bool
otherwise = ParamInfo
ImplicitIndex ParamInfo -> [ParamInfo] -> [ParamInfo]
forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
getParamInfo Type
_ [PArg]
_ Int
_ [Int]
_ = []
isParam :: ParamInfo -> Bool
isParam ParamInfo
Index = Bool
False
isParam ParamInfo
Param = Bool
True
isParam ParamInfo
ImplicitIndex = Bool
False
isParam ParamInfo
ImplicitParam = Bool
True
elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()
elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()
elabRewriteLemma ElabInfo
info Name
n Type
cty_in =
do IState
ist <- Idris IState
getIState
let cty :: Type
cty = Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
cty_in
let rewrite_lem :: Name
rewrite_lem = Name -> Name
rewrite_name Name
n
case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
Maybe TypeInfo
Nothing -> String -> Idris ()
forall a. String -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Can't happen, elabRewriteLemma for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
Just TypeInfo
ti -> do
let imps :: [PArg]
imps = case Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
Maybe [PArg]
Nothing -> PArg -> [PArg]
forall a. a -> [a]
repeat (PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
Placeholder)
Just [PArg]
is -> [PArg]
is
let pinfo :: [ParamInfo]
pinfo = Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
cty [PArg]
imps Int
0 (TypeInfo -> [Int]
param_pos TypeInfo
ti)
if (ParamInfo -> Bool) -> [ParamInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ParamInfo -> Bool
isParam [ParamInfo]
pinfo
then () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (ElabInfo -> Name -> Name -> [ParamInfo] -> Type -> Idris ()
mkLemma ElabInfo
info Name
rewrite_lem Name
n [ParamInfo]
pinfo Type
cty)
(\Err
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
mkLemma :: ElabInfo -> Name -> Name -> [ParamInfo] -> Type -> Idris ()
mkLemma :: ElabInfo -> Name -> Name -> [ParamInfo] -> Type -> Idris ()
mkLemma ElabInfo
info Name
lemma Name
tcon [ParamInfo]
ps Type
ty =
do IState
ist <- Idris IState
getIState
let leftty :: PTerm
leftty = Name -> [ParamInfo] -> [Name] -> [Name] -> PTerm
mkTy Name
tcon [ParamInfo]
ps (String -> Int -> [Name]
namesFrom String
"p" Int
0) (String -> Int -> [Name]
namesFrom String
"left" Int
0)
rightty :: PTerm
rightty = Name -> [ParamInfo] -> [Name] -> [Name] -> PTerm
mkTy Name
tcon [ParamInfo]
ps (String -> Int -> [Name]
namesFrom String
"p" Int
0) (String -> Int -> [Name]
namesFrom String
"right" Int
0)
predty :: PTerm
predty = IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [ParamInfo]
ps Type
ty (String -> Int -> [Name]
namesFrom String
"pred" Int
0) (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl (Int -> String -> Name
sMN Int
0 String
"rep") FC
fc
(Name -> [ParamInfo] -> [Name] -> [Name] -> PTerm
mkTy Name
tcon [ParamInfo]
ps (String -> Int -> [Name]
namesFrom String
"p" Int
0) (String -> Int -> [Name]
namesFrom String
"pred" Int
0))
(FC -> PTerm
PType FC
fc)
let xarg :: Name
xarg = Int -> String -> Name
sMN Int
0 String
"x"
let yarg :: Name
yarg = Int -> String -> Name
sMN Int
0 String
"y"
let parg :: Name
parg = Int -> String -> Name
sMN Int
0 String
"P"
let eq :: Name
eq = Int -> String -> Name
sMN Int
0 String
"eq"
let prop :: Name
prop = Int -> String -> Name
sMN Int
0 String
"prop"
let lemTy :: PTerm
lemTy = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
xarg FC
fc PTerm
leftty (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
yarg FC
fc PTerm
rightty (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
parg FC
fc PTerm
predty (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
eq FC
fc (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"="))
[PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
xarg),
PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
yarg)]) (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
prop FC
fc (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
parg)
[PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
yarg)]) (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
parg) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
xarg)]
let lemLHS :: PTerm
lemLHS = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
lemma)
[PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
parg),
PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Refl")),
PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
prop)]
let lemRHS :: PTerm
lemRHS = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
prop
ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info
(Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
forall a. Docstring a
emptyDocstring [] SyntaxInfo
defaultSyntax FC
fc [] Name
lemma FC
fc PTerm
lemTy)
ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info
(FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] Name
lemma [FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
lemma PTerm
lemLHS [] PTerm
lemRHS []])
where
fc :: FC
fc = FC
emptyFC
namesFrom :: String -> Int -> [Name]
namesFrom String
x Int
i = Int -> String -> Name
sMN Int
i (String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: String -> Int -> [Name]
namesFrom String
x (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
mkTy :: Name -> [ParamInfo] -> [Name] -> [Name] -> PTerm
mkTy Name
fn [ParamInfo]
pinfo [Name]
ps [Name]
is
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
fn) ([ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [ParamInfo]
pinfo [Name]
ps [Name]
is)
mkArgs :: [ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [] [Name]
ps [Name]
is = []
mkArgs (ParamInfo
Param : [ParamInfo]
pinfo) (Name
p : [Name]
ps) [Name]
is
= PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
p) PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [ParamInfo]
pinfo [Name]
ps [Name]
is
mkArgs (ParamInfo
Index : [ParamInfo]
pinfo) [Name]
ps (Name
i : [Name]
is)
= PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
i) PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [ParamInfo]
pinfo [Name]
ps [Name]
is
mkArgs (ParamInfo
ImplicitParam : [ParamInfo]
pinfo) (Name
p : [Name]
ps) [Name]
is
= [ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [ParamInfo]
pinfo [Name]
ps [Name]
is
mkArgs (ParamInfo
ImplicitIndex : [ParamInfo]
pinfo) [Name]
ps (Name
i : [Name]
is)
= [ParamInfo] -> [Name] -> [Name] -> [PArg]
mkArgs [ParamInfo]
pinfo [Name]
ps [Name]
is
mkArgs [ParamInfo]
_ [Name]
_ [Name]
_ = []
bindIdxs :: IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [] Type
ty [Name]
is PTerm
tm = PTerm
tm
bindIdxs IState
ist (ParamInfo
Param : [ParamInfo]
pinfo) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
ty Type
_) Type
sc) [Name]
is PTerm
tm
= IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [ParamInfo]
pinfo (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
ty) Type
sc) [Name]
is PTerm
tm
bindIdxs IState
ist (ParamInfo
Index : [ParamInfo]
pinfo) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
ty Type
_) Type
sc) (Name
i : [Name]
is) PTerm
tm
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
forall_imp Name
i FC
fc (IState -> Type -> PTerm
delab IState
ist Type
ty)
(IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [ParamInfo]
pinfo (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
ty) Type
sc) [Name]
is PTerm
tm)
bindIdxs IState
ist (ParamInfo
ImplicitParam : [ParamInfo]
pinfo) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
ty Type
_) Type
sc) [Name]
is PTerm
tm
= IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [ParamInfo]
pinfo (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
ty) Type
sc) [Name]
is PTerm
tm
bindIdxs IState
ist (ParamInfo
ImplicitIndex : [ParamInfo]
pinfo) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
ty Type
_) Type
sc) (Name
i : [Name]
is) PTerm
tm
= IState -> [ParamInfo] -> Type -> [Name] -> PTerm -> PTerm
bindIdxs IState
ist [ParamInfo]
pinfo (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
ty) Type
sc) [Name]
is PTerm
tm
bindIdxs IState
_ [ParamInfo]
_ Type
_ [Name]
_ PTerm
tm = PTerm
tm