git.iko.soy/Idris-dev
on master help sign in
Names
commit01ceeada092046b3c29f13958b3e07a6ff575d68 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 15:20 (15 years ago) parent03d7d5e
3 files changed+23−9
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+13−2 src/Idris/Parser.hs+2−2 src/Idris/REPL.hs+8−5
src/Idris/AbsSyntax.hs+13−2
@@ -16,11 +16,12 @@ import Debug.Trace
1616import qualified Epic.Epic as E
1717
1818data IOption = IOption { opt_logLevel :: Int,
19− opt_typecase :: Bool
19+ opt_typecase :: Bool,
20+ opt_showimp :: Bool
2021 }
2122 deriving (Show, Eq)
2223
23−defaultOpts = IOption 0 False
24+defaultOpts = IOption 0 False False
2425
2526-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
2627-- without typechecking).
@@ -139,6 +140,16 @@ logLevel :: Idris Int
139140logLevel = do i <- get
140141 return (opt_logLevel (idris_options i))
141142
143+impShow :: Idris Bool
144+impShow = do i <- get
145+ return (opt_showimp (idris_options i))
146+
147+setImpShow :: Bool -> Idris ()
148+setImpShow t = do i <- get
149+ let opts = idris_options i
150+ let opt' = opts { opt_showimp = t }
151+ put (i { idris_options = opt' })
152+
142153logLvl :: Int -> String -> Idris ()
143154logLvl l str = do i <- get
144155 let lvl = opt_logLevel (idris_options i)
src/Idris/Parser.hs+2−2
@@ -510,7 +510,7 @@ pPi syn =
510510 t <- pExpr' syn
511511 symbol "->"
512512 sc <- pExpr syn
513− return (PPi (Exp False Static) (MN 0 "X") t sc)
513+ return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)
514514
515515pConstList :: SyntaxInfo -> IParser [PTerm]
516516pConstList syn = try (do lchar '('
@@ -577,7 +577,7 @@ table fixes
577577 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
578578 ++ toTable (reverse fixes) ++
579579 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
580− [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]
580+ [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
581581
582582toTable fs = map (map toBin)
583583 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
src/Idris/REPL.hs+8−5
@@ -92,21 +92,24 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel False t
9292 let tm' = normaliseC ctxt [] tm
9393 let ty' = normaliseC ctxt [] ty
9494 logLvl 3 $ "Raw: " ++ show (tm', ty')
95− iputStrLn (show (delab ist tm') ++ " : " ++
96− show (delab ist ty'))
95+ imp <- impShow
96+ iputStrLn (showImp imp (delab ist tm') ++ " : " ++
97+ showImp imp (delab ist ty'))
9798process (Check (PRef _ n))
9899 = do ctxt <- getContext
99100 ist <- get
101+ imp <- impShow
100102 case lookupTy n ctxt of
101103 Just t -> iputStrLn $ show n ++ " : " ++
102− show (delab ist t)
104+ showImp imp (delab ist t)
103105 _ -> iputStrLn $ "No such variable " ++ show n
104106process (Check t) = do (tm, ty) <- elabVal toplevel False t
105107 ctxt <- getContext
106108 ist <- get
109+ imp <- impShow
107110 let ty' = normaliseC ctxt [] ty
108− iputStrLn (show (delab ist tm) ++ " : " ++
109− show (delab ist ty))
111+ iputStrLn (showImp imp (delab ist tm) ++ " : " ++
112+ showImp imp (delab ist ty))
110113process (Defn n) = do ctxt <- getContext
111114 lift $ print (lookupDef n ctxt)
112115process (Spec t) = do (tm, ty) <- elabVal toplevel False t