@@ -7,6 +7,7 @@ module Idris.Delaborate where
77
88import Idris.AbsSyntax
99import Core.TT
10+import Core.Evaluate
1011
1112import Debug.Trace
1213
@@ -15,30 +16,48 @@ bugaddr = "https://github.com/edwinb/Idris-dev/issues"
1516delab :: IState -> Term -> PTerm
1617delab i tm = delab' i tm False
1718
19+delabTy :: IState -> Name -> PTerm
20+delabTy i n
21+ = case lookupTy Nothing n (tt_ctxt i) of
22+ (ty:_) -> case lookupCtxt Nothing n (idris_implicits i) of
23+ (imps:_) -> delabTy' i imps ty False
24+
1825delab' :: IState -> Term -> Bool -> PTerm
19−delab' ist tm fullname = de [] tm
26+delab' i t f = delabTy' i [] t f
27+
28+delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
29+ -> Term -> Bool -> PTerm
30+delabTy' ist imps tm fullname = de [] imps tm
2031 where
2132 un = FC "(val)" 0
2233
23− de env (App f a) = deFn env f [a]
24− de env (V i) | i < length env = PRef un (snd (env!!i))
25− | otherwise = PRef un (UN ("v" ++ show i ++ ""))
26− de env (P _ n _) | n == unitTy = PTrue un
27− | n == unitCon = PTrue un
28− | n == falseTy = PFalse un
29− | Just n' <- lookup n env = PRef un n'
30− | otherwise = PRef un (dens n)
31− de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de ((n,n):env) sc)
32− de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de ((n,n):env) sc)
33− de env (Bind n (Let ty val) sc)
34− = PLet n (de env ty) (de env val) (de ((n,n):env) sc)
35− de env (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) sc
36− de env (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) sc
37− de env (Bind n _ sc) = de ((n,n):env) sc
38− de env (Constant i) = PConstant i
39− de env Erased = Placeholder
40− de env Impossible = Placeholder
41− de env (TType i) = PType
34+ de env _ (App f a) = deFn env f [a]
35+ de env _ (V i) | i < length env = PRef un (snd (env!!i))
36+ | otherwise = PRef un (UN ("v" ++ show i ++ ""))
37+ de env _ (P _ n _) | n == unitTy = PTrue un
38+ | n == unitCon = PTrue un
39+ | n == falseTy = PFalse un
40+ | Just n' <- lookup n env = PRef un n'
41+ | otherwise = PRef un (dens n)
42+ de env _ (Bind n (Lam ty) sc)
43+ = PLam n (de env [] ty) (de ((n,n):env) [] sc)
44+ de env (PImp _ _ _ _ _:is) (Bind n (Pi ty) sc)
45+ = PPi impl n (de env [] ty) (de ((n,n):env) is sc)
46+ de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)
47+ = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)
48+ de env (PTacImplicit _ _ _ tac _ _:is) (Bind n (Pi ty) sc)
49+ = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)
50+ de env _ (Bind n (Pi ty) sc)
51+ = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)
52+ de env _ (Bind n (Let ty val) sc)
53+ = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)
54+ de env _ (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) [] sc
55+ de env _ (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) [] sc
56+ de env _ (Bind n _ sc) = de ((n,n):env) [] sc
57+ de env _ (Constant i) = PConstant i
58+ de env _ Erased = Placeholder
59+ de env _ Impossible = Placeholder
60+ de env _ (TType i) = PType
4261
4362 dens x | fullname = x
4463 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of
@@ -47,19 +66,21 @@ delab' ist tm fullname = de [] tm
4766 dens n = n
4867
4968 deFn env (App f a) args = deFn env f (a:args)
50− deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)
51− | n == eqCon = PRefl un (de env r)
52− | n == UN "lazy" = de env r
69+ deFn env (P _ n _) [l,r]
70+ | n == pairTy = PPair un (de env [] l) (de env [] r)
71+ | n == eqCon = PRefl un (de env [] r)
72+ | n == UN "lazy" = de env [] r
5373 deFn env (P _ n _) [ty, Bind x (Lam _) r]
54− | n == UN "Exists"
55− = PDPair un (PRef un x) (de env ty)
56− (de ((x,x):env) (instantiate (P Bound x ty) r))
57− deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
58− | n == eqTy = PEq un (de env l) (de env r)
59− | n == UN "Ex_intro" = PDPair un (de env l) Placeholder
60− (de env r)
61− deFn env (P _ n _) args = mkPApp (dens n) (map (de env) args)
62− deFn env f args = PApp un (de env f) (map pexp (map (de env) args))
74+ | n == UN "Exists"
75+ = PDPair un (PRef un x) (de env [] ty)
76+ (de ((x,x):env) [] (instantiate (P Bound x ty) r))
77+ deFn env (P _ n _) [_,_,l,r]
78+ | n == pairCon = PPair un (de env [] l) (de env [] r)
79+ | n == eqTy = PEq un (de env [] l) (de env [] r)
80+ | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder
81+ (de env [] r)
82+ deFn env (P _ n _) args = mkPApp (dens n) (map (de env []) args)
83+ deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
6384
6485 mkPApp n args
6586 | [imps] <- lookupCtxt Nothing n (idris_implicits ist)