{-# 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 forall aux. Elab' aux ()
attack
PTerm
sc <- case Maybe PTerm
newg of
Maybe PTerm
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
sc_in
Just PTerm
t -> do
Name
letn <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rewrite_result")
forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rty")
forall aux. Name -> Raw -> Elab' aux ()
claim Name
tyn Raw
RType
Name
valn <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"rval")
forall aux. Name -> Raw -> Elab' aux ()
claim Name
valn (Name -> Raw
Var Name
tyn)
Name
letn <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"_rewrite_rule")
forall aux. Name -> RigCount -> Raw -> Raw -> Elab' aux ()
letbind Name
letn RigCount
RigW (Name -> Raw
Var Name
tyn) (Name -> Raw
Var Name
valn)
forall aux. Name -> Elab' aux ()
focus Name
valn
PTerm -> ElabD ()
elab PTerm
rule
forall aux. Elab' aux ()
compute
Type
g <- forall aux. Elab' aux Type
goal
(Type
tmv, Type
rule_in) <- forall aux. Raw -> Elab' aux (Type, Type)
get_type_val (Name -> Raw
Var Name
letn)
Env
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 <- forall aux. Name -> Elab' aux Name
unique_hole (Int -> String -> Name
sMN Int
0 String
"replaced")
case 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 forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
do Name
substfn <- Maybe Name -> IState -> Type -> Type -> ElabD Name
findSubstFn Maybe Name
substfn_in IState
ist Type
lt Type
rt
let pred_tt :: Type
pred_tt = Type -> Type -> Type -> Type -> Type
mkP (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
rname Type
rt) Type
l Type
r Type
g
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
g forall a. Eq a => a -> a -> Bool
== Type
pred_tt) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (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 (forall a b. (a -> b) -> [a] -> [b]
map 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)
[forall {t}. t -> PArg' t
pexp (PTerm -> PTerm
stripImpls PTerm
pred),
forall {t}. t -> PArg' t
pexp (PTerm -> PTerm
stripImpls PTerm
rule), forall {t}. t -> PArg' t
pexp PTerm
sc])
PTerm -> ElabD ()
elab PTerm
rewrite
forall aux. Elab' aux ()
solve
(Type, [Type])
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (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 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 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 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
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 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
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 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 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
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Type
t' Type
v'
mkPB Binder Type
b = let ty :: Type
ty = forall b. Binder b -> b
binderTy Binder Type
b
ty' :: Type
ty' = if (Type
r 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 :: Type
binderTy = Type
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 (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 :: PTerm
getTm = PTerm
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 -> ElabD Name
findSubstFn Maybe Name
Nothing IState
ist Type
lt Type
rt
| Type
lt forall a. Eq a => a -> a -> Bool
== Type
rt = forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
sUN String
"rewrite__impl")
| (P NameType
_ Name
lcon Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
lt,
(P NameType
_ Name
rcon Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
rt,
Name
lcon 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Name
rewrite_name Name
lcon)
Maybe Type
Nothing -> forall {t :: (* -> *) -> * -> *} {a}.
MonadTrans t =>
Type -> Type -> t TC a
rewriteFail Type
lt Type
rt
| Bool
otherwise = 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Can't rewrite heterogeneous equality on types " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (IState -> Type -> PTerm
delab IState
ist Type
lt) forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ 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)] -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
[] -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Name -> Err' t
NoSuchVariable forall a b. (a -> b) -> a -> b
$ Name
substfn_in
[(Name, Type)]
more -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. [Name] -> Err' t
CantResolveAlts forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"_rewrite_lemma")
data ParamInfo = Index
| Param
| ImplicitIndex
| ImplicitParam
deriving Int -> ParamInfo -> ShowS
[ParamInfo] -> ShowS
ParamInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ParamInfo] -> ShowS
$cshowList :: [ParamInfo] -> ShowS
show :: ParamInfo -> String
$cshow :: ParamInfo -> String
showsPrec :: Int -> ParamInfo -> ShowS
$cshowsPrec :: Int -> ParamInfo -> ShowS
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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = ParamInfo
Param forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
| Bool
otherwise = ParamInfo
Index forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = ParamInfo
ImplicitParam forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i forall a. Num a => a -> a -> a
+ Int
1) [Int]
ps
| Bool
otherwise = ParamInfo
ImplicitIndex forall a. a -> [a] -> [a]
: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
getParamInfo Type
sc [PArg]
is (Int
i 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 forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
Maybe TypeInfo
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't happen, elabRewriteLemma for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
Just TypeInfo
ti -> do
let imps :: [PArg]
imps = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
Maybe [PArg]
Nothing -> forall a. a -> [a]
repeat (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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ParamInfo -> Bool
isParam [ParamInfo]
pinfo
then forall (m :: * -> *) a. Monad m => a -> m a
return ()
else 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
_ -> 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) 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 forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
yarg FC
fc PTerm
rightty forall a b. (a -> b) -> a -> b
$
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
parg FC
fc PTerm
predty 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
"="))
[forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
xarg),
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
yarg)]) 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)
[forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
yarg)]) forall a b. (a -> b) -> a -> b
$
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
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)
[forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
parg),
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Refl")),
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
(forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy 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
(forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] Name
lemma [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 forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i) forall a. a -> [a] -> [a]
: String -> Int -> [Name]
namesFrom String
x (Int
i 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
= forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
p) 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)
= forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
i) 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 (forall n. TT n -> TT n -> TT n
instantiate (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 (forall n. TT n -> TT n -> TT n
instantiate (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 (forall n. TT n -> TT n -> TT n
instantiate (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 (forall n. TT n -> TT n -> TT n
instantiate (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