@@ -7,6 +7,7 @@ module Idris.Delaborate where
8import Idris.AbsSyntax
8import Idris.AbsSyntax
9import Core.TT
9import Core.TT
11import Debug.Trace
12import Debug.Trace
@@ -15,30 +16,48 @@ bugaddr = "https://github.com/edwinb/Idris-dev/issues"
15delab :: IState -> Term -> PTerm
16delab :: IState -> Term -> PTerm
16delab i tm = delab' i tm False
17delab i tm = delab' i tm False
19+delabTy :: IState -> Name -> PTerm
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
18delab' :: IState -> Term -> Bool -> PTerm
25delab' :: IState -> Term -> Bool -> PTerm
26+delab' i t f = delabTy' i [] t f
28+delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
29+ -> Term -> Bool -> PTerm
19−delab' ist tm fullname = de [] tm
30+delabTy' ist imps tm fullname = de [] imps tm
21 un = FC "(val)" 0
32 un = FC "(val)" 0
23− de env (App f a) = deFn env f [a]
34+ de env _ (App f a) = deFn env f [a]
24− de env (V i) | i < length env = PRef un (snd (env!!i))
35+ de env _ (V i) | i < length env = PRef un (snd (env!!i))
25− | otherwise = PRef un (UN ("v" ++ show i ++ ""))
36+ | otherwise = PRef un (UN ("v" ++ show i ++ ""))
26− de env (P _ n _) | n == unitTy = PTrue un
37+ de env _ (P _ n _) | n == unitTy = PTrue un
27− | n == unitCon = PTrue un
38+ | n == unitCon = PTrue un
28− | n == falseTy = PFalse un
39+ | n == falseTy = PFalse un
29− | Just n' <- lookup n env = PRef un n'
40+ | Just n' <- lookup n env = PRef un n'
30− | otherwise = PRef un (dens n)
41+ | otherwise = PRef un (dens n)
31− de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de ((n,n):env) sc)
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)
32− de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de ((n,n):env) sc)
51+ = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)
33− de env (Bind n (Let ty val) sc)
52+ de env _ (Bind n (Let ty val) sc)
34− = PLet n (de env ty) (de env val) (de ((n,n):env) sc)
53+ = 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
54+ 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
55+ de env _ (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) [] sc
37− de env (Bind n _ sc) = de ((n,n):env) sc
56+ de env _ (Bind n _ sc) = de ((n,n):env) [] sc
38− de env (Constant i) = PConstant i
57+ de env _ (Constant i) = PConstant i
39− de env Erased = Placeholder
58+ de env _ Erased = Placeholder
40− de env Impossible = Placeholder
59+ de env _ Impossible = Placeholder
41− de env (TType i) = PType
60+ de env _ (TType i) = PType
43 dens x | fullname = x
62 dens x | fullname = x
44 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of
63 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of
@@ -47,19 +66,21 @@ delab' ist tm fullname = de [] tm
47 dens n = n
66 dens n = n
49 deFn env (App f a) args = deFn env f (a:args)
68 deFn env (App f a) args = deFn env f (a:args)
69+ deFn env (P _ n _) [l,r]
50− deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)
70+ | n == pairTy = PPair un (de env [] l) (de env [] r)
51− | n == eqCon = PRefl un (de env r)
71+ | n == eqCon = PRefl un (de env [] r)
52− | n == UN "lazy" = de env r
72+ | n == UN "lazy" = de env [] r
53 deFn env (P _ n _) [ty, Bind x (Lam _) r]
73 deFn env (P _ n _) [ty, Bind x (Lam _) r]
54− | n == UN "Exists"
74+ | n == UN "Exists"
55− = PDPair un (PRef un x) (de env ty)
75+ = PDPair un (PRef un x) (de env [] ty)
56− (de ((x,x):env) (instantiate (P Bound x ty) r))
76+ (de ((x,x):env) [] (instantiate (P Bound x ty) r))
77+ deFn env (P _ n _) [_,_,l,r]
57− deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
78+ | n == pairCon = PPair un (de env [] l) (de env [] r)
58− | n == eqTy = PEq un (de env l) (de env r)
79+ | n == eqTy = PEq un (de env [] l) (de env [] r)
59− | n == UN "Ex_intro" = PDPair un (de env l) Placeholder
80+ | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder
60− (de env r)
81+ (de env [] r)
61− deFn env (P _ n _) args = mkPApp (dens n) (map (de env) args)
82+ 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))
83+ deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
64 mkPApp n args
85 mkPApp n args
65 | [imps] <- lookupCtxt Nothing n (idris_implicits ist)
86 | [imps] <- lookupCtxt Nothing n (idris_implicits ist)