Permalink
Browse files

Pretty printing of TT terms as PTerms

  • Loading branch information...
1 parent d3adb11 commit 59c1eb18cdc14c86e4d95e5eb7427fab8fbd7d15 Edwin Brady committed Oct 10, 2011
Showing with 40 additions and 3 deletions.
  1. +2 −1 miniidris.cabal
  2. +2 −1 src/Idris/AbsSyntax.hs
  3. +32 −0 src/Idris/Delaborate.hs
  4. +4 −1 src/Idris/REPL.hs
View
@@ -23,7 +23,8 @@ Executable miniidris
Core.CaseTree,
Idris.AbsSyntax, Idris.Parser, Idris.REPL,
- Idris.REPLParser, Idris.ElabDecls, Idris.Error
+ Idris.REPLParser, Idris.ElabDecls, Idris.Error,
+ Idris.Delaborate
Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
containers, process, transformers
View
@@ -131,6 +131,7 @@ data PTerm = PQuote Raw
| PRef Name
| PLam Name PTerm PTerm
| PPi Plicity Name PTerm PTerm
+ | PLet Name PTerm PTerm PTerm -- not implemented yet
| PApp PTerm [(Name, PTerm)] [PTerm]
| PHidden PTerm -- irrelevant or hidden pattern
| PSet
@@ -187,7 +188,7 @@ showImp impl tm = se 10 tm where
| not impl = show f
se p (PApp (PRef op@(UN [f:_])) _ [l, r])
| not impl && not (isAlpha f)
- = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
+ = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
se p (PApp f imps args)
= bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
++ concatMap seArg args
View
@@ -0,0 +1,32 @@
+module Idris.Delaborate where
+
+-- Convert core TT back into high level syntax, primarily for display
+-- purposes.
+
+import Idris.AbsSyntax
+import Core.TT
+
+import Debug.Trace
+
+delab :: IState -> Term -> PTerm
+delab ist tm = de [] tm
+ where
+ de env (App f a) = deFn env f [a]
+ de env (V i) = PRef (env!!i)
+ de env (P _ n _) = PRef n
+ de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)
+ de env (Bind n (Pi ty) sc) = PPi Exp n (de env ty) (de (n:env) sc)
+ de env (Bind n (Let ty val) sc)
+ = PLet n (de env ty) (de env val) (de (n:env) sc)
+ de env (Bind n _ sc) = de (n:env) sc
+ de env (Set i) = PSet
+
+ deFn env (App f a) args = deFn env f (a:args)
+ deFn env (P _ n _) args = mkPApp n (map (de env) args)
+ deFn env f args = PApp (de env f) [] (map (de env) args)
+
+ mkPApp n args
+ | Just (ns, i) <- lookupCtxt n (idris_implicits ist)
+ = PApp (PRef n) (zip ns args) (drop (length ns) args)
+ | otherwise = PApp (PRef n) [] args
+
View
@@ -6,6 +6,7 @@ import Idris.AbsSyntax
import Idris.REPLParser
import Idris.ElabDecls
import Idris.Error
+import Idris.Delaborate
import Core.Evaluate
import Core.ProofShell
@@ -41,8 +42,10 @@ process Help
= iputStrLn "At some point I'll write some help text. Thanks for asking though."
process (Eval t) = do (tm, ty) <- elabVal t
ctxt <- getContext
+ ist <- get
let tm' = normalise ctxt [] tm
- iputStrLn (show tm' ++ " : " ++ show ty)
+ iputStrLn (show (delab ist tm') ++ " : " ++
+ show (delab ist ty))
process TTShell = do ist <- get
let shst = initState (tt_ctxt ist)
shst' <- lift $ runShell shst

0 comments on commit 59c1eb1

Please sign in to comment.