01ceead · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Names

01ceeadEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+13−2

compare with master

unifiedsplit

@@ -16,11 +16,12 @@ import Debug.Trace

16import qualified Epic.Epic as E

18data IOption = IOption { opt_logLevel :: Int,

19− opt_typecase :: Bool

19+ opt_typecase :: Bool,

20+ opt_showimp :: Bool

20 }

21 }

21 deriving (Show, Eq)

22 deriving (Show, Eq)

23−defaultOpts = IOption 0 False

24+defaultOpts = IOption 0 False False

25-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

26-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

26-- without typechecking).

27-- without typechecking).

@@ -139,6 +140,16 @@ logLevel :: Idris Int

139logLevel = do i <- get

140logLevel = do i <- get

140 return (opt_logLevel (idris_options i))

141 return (opt_logLevel (idris_options i))

141

142

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+

142logLvl :: Int -> String -> Idris ()

153logLvl :: Int -> String -> Idris ()

143logLvl l str = do i <- get

154logLvl l str = do i <- get

144 let lvl = opt_logLevel (idris_options i)

155 let lvl = opt_logLevel (idris_options i)

src/Idris/Parser.hs+2−2

@@ -510,7 +510,7 @@ pPi syn =

510 t <- pExpr' syn

511 symbol "->"

512 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)

514

515pConstList :: SyntaxInfo -> IParser [PTerm]

516pConstList syn = try (do lchar '('

@@ -577,7 +577,7 @@ table fixes

577 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

578 ++ toTable (reverse fixes) ++

579 [[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]]

581

582toTable fs = map (map toBin)

583 (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

92 let tm' = normaliseC ctxt [] tm

93 let ty' = normaliseC ctxt [] ty

94 logLvl 3 $ "Raw: " ++ show (tm', ty')

95+ imp <- impShow

95− iputStrLn (show (delab ist tm') ++ " : " ++

96+ iputStrLn (showImp imp (delab ist tm') ++ " : " ++

96− show (delab ist ty'))

97+ showImp imp (delab ist ty'))

97process (Check (PRef _ n))

98process (Check (PRef _ n))

98 = do ctxt <- getContext

99 = do ctxt <- getContext

99 ist <- get

100 ist <- get

101+ imp <- impShow

100 case lookupTy n ctxt of

102 case lookupTy n ctxt of

101 Just t -> iputStrLn $ show n ++ " : " ++

103 Just t -> iputStrLn $ show n ++ " : " ++

102− show (delab ist t)

104+ showImp imp (delab ist t)

103 _ -> iputStrLn $ "No such variable " ++ show n

105 _ -> iputStrLn $ "No such variable " ++ show n

104process (Check t) = do (tm, ty) <- elabVal toplevel False t

106process (Check t) = do (tm, ty) <- elabVal toplevel False t

105 ctxt <- getContext

107 ctxt <- getContext

106 ist <- get

108 ist <- get

109+ imp <- impShow

107 let ty' = normaliseC ctxt [] ty

110 let ty' = normaliseC ctxt [] ty

108− iputStrLn (show (delab ist tm) ++ " : " ++

111+ iputStrLn (showImp imp (delab ist tm) ++ " : " ++

109− show (delab ist ty))

112+ showImp imp (delab ist ty))

110process (Defn n) = do ctxt <- getContext

113process (Defn n) = do ctxt <- getContext

111 lift $ print (lookupDef n ctxt)

114 lift $ print (lookupDef n ctxt)

112process (Spec t) = do (tm, ty) <- elabVal toplevel False t

115process (Spec t) = do (tm, ty) <- elabVal toplevel False t