@@ -0,0 +1,32 @@
1+module Idris.Delaborate where
2+
3+-- Convert core TT back into high level syntax, primarily for display
4+-- purposes.
5+
6+import Idris.AbsSyntax
7+import Core.TT
8+
9+import Debug.Trace
10+
11+delab :: IState -> Term -> PTerm
12+delab ist tm = de [] tm
13+ where
14+ de env (App f a) = deFn env f [a]
15+ de env (V i) = PRef (env!!i)
16+ de env (P _ n _) = PRef n
17+ de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)
18+ de env (Bind n (Pi ty) sc) = PPi Exp n (de env ty) (de (n:env) sc)
19+ de env (Bind n (Let ty val) sc)
20+ = PLet n (de env ty) (de env val) (de (n:env) sc)
21+ de env (Bind n _ sc) = de (n:env) sc
22+ de env (Set i) = PSet
23+
24+ deFn env (App f a) args = deFn env f (a:args)
25+ deFn env (P _ n _) args = mkPApp n (map (de env) args)
26+ deFn env f args = PApp (de env f) [] (map (de env) args)
27+
28+ mkPApp n args
29+ | Just (ns, i) <- lookupCtxt n (idris_implicits ist)
30+ = PApp (PRef n) (zip ns args) (drop (length ns) args)
31+ | otherwise = PApp (PRef n) [] args
32+