59c1eb1 · Idris-dev · git.iko.soy

miniidris.cabal+2−1

compare with master

unifiedsplit

@@ -23,7 +23,8 @@ Executable miniidris

23 Core.CaseTree,

24

25 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

26− Idris.REPLParser, Idris.ElabDecls, Idris.Error

26+ Idris.REPLParser, Idris.ElabDecls, Idris.Error,

27+ Idris.Delaborate

27

28

28 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

29 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

29 containers, process, transformers

30 containers, process, transformers

src/Idris/AbsSyntax.hs+2−1

@@ -131,6 +131,7 @@ data PTerm = PQuote Raw

131 | PRef Name

132 | PLam Name PTerm PTerm

133 | PPi Plicity Name PTerm PTerm

134+ | PLet Name PTerm PTerm PTerm -- not implemented yet

134 | PApp PTerm [(Name, PTerm)] [PTerm]

135 | PApp PTerm [(Name, PTerm)] [PTerm]

135 | PHidden PTerm -- irrelevant or hidden pattern

136 | PHidden PTerm -- irrelevant or hidden pattern

136 | PSet

137 | PSet

@@ -187,7 +188,7 @@ showImp impl tm = se 10 tm where

187 | not impl = show f

188 | not impl = show f

188 se p (PApp (PRef op@(UN [f:_])) _ [l, r])

189 se p (PApp (PRef op@(UN [f:_])) _ [l, r])

189 | not impl && not (isAlpha f)

190 | not impl && not (isAlpha f)

190− = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r

191+ = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

191 se p (PApp f imps args)

192 se p (PApp f imps args)

192 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

193 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

193 ++ concatMap seArg args

194 ++ concatMap seArg args

src/Idris/Delaborate.hsnew file+32

@@ -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+

src/Idris/REPL.hs+4−1

@@ -6,6 +6,7 @@ import Idris.AbsSyntax

6import Idris.REPLParser

7import Idris.ElabDecls

8import Idris.Error

9+import Idris.Delaborate

9

10

10import Core.Evaluate

11import Core.Evaluate

11import Core.ProofShell

12import Core.ProofShell

@@ -41,8 +42,10 @@ process Help

41 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

42 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

42process (Eval t) = do (tm, ty) <- elabVal t

43process (Eval t) = do (tm, ty) <- elabVal t

43 ctxt <- getContext

44 ctxt <- getContext

45+ ist <- get

44 let tm' = normalise ctxt [] tm

46 let tm' = normalise ctxt [] tm

45− iputStrLn (show tm' ++ " : " ++ show ty)

47+ iputStrLn (show (delab ist tm') ++ " : " ++

48+ show (delab ist ty))

46process TTShell = do ist <- get

49process TTShell = do ist <- get

47 let shst = initState (tt_ctxt ist)

50 let shst = initState (tt_ctxt ist)

48 shst' <- lift $ runShell shst

51 shst' <- lift $ runShell shst