ffc64e3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add mechanism for simplification and function options

ffc64e3Edwin Brady15 years ago

src/Core/CaseTree.hs+6−1

compare with master

unifiedsplit

@@ -1,5 +1,5 @@

1module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

2− simpleCase) where

2+ simpleCase, small) where

4import Core.TT

@@ -23,6 +23,11 @@ type CaseTree = SC

23type Clause = ([Pat], Term)

24type CS = Int

26+-- simple terms can be inlined trivially - good for primitives in particular

27+small :: SC -> Bool

28+small (STerm t) = True

29+small _ = False

30+

26simpleCase :: Bool -> [(Term, Term)] -> CaseDef

31simpleCase :: Bool -> [(Term, Term)] -> CaseDef

27simpleCase tc [] = CaseDef [] (UnmatchedCase "No pattern clauses")

32simpleCase tc [] = CaseDef [] (UnmatchedCase "No pattern clauses")

28simpleCase tc cs = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

33simpleCase tc cs = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

src/Core/Evaluate.hs+39−22

@@ -1,7 +1,7 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2 PatternGuards #-}

4−module Core.Evaluate(normalise, normaliseC, specialise, hnf,

4+module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5 Fun(..), Def(..), Context,

6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -16,7 +16,7 @@ import Core.CaseTree

16type EvalState = ()

17type Eval a = State EvalState a

19−data EvalOpt = Spec | HNF

19+data EvalOpt = Spec | HNF | Simplify

20 deriving (Show, Eq)

22-- VALUES (as HOAS) ---------------------------------------------------------

@@ -66,6 +66,14 @@ specialise ctxt statics t

66 = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]

67 quote 0 val) ()

69+-- Like normalise, but we only reduce functions that are marked as okay to

70+-- inline (and probably shouldn't reduce lets?)

71+

72+simplify :: Context -> Env -> TT Name -> TT Name

73+simplify ctxt env t

74+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]

75+ quote 0 val) ()

76+

69hnf :: Context -> Env -> TT Name -> TT Name

77hnf :: Context -> Env -> TT Name -> TT Name

70hnf ctxt env t

78hnf ctxt env t

71 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]

79 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]

@@ -92,17 +100,20 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

92eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value

100eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value

93eval ctxt statics genv tm opts = ev True [] tm where

101eval ctxt statics genv tm opts = ev True [] tm where

94 spec = Spec `elem` opts

102 spec = Spec `elem` opts

103+ simpl = Simplify `elem` opts

104

96 ev top env (P _ n ty)

105 ev top env (P _ n ty)

97 | Just (Let t v) <- lookup n genv = ev top env v

106 | Just (Let t v) <- lookup n genv = ev top env v

98 ev top env (P Ref n ty) = case lookupDef n ctxt of

107 ev top env (P Ref n ty) = case lookupDef n ctxt of

99 Just (Function (Fun _ _ _ v)) -> return v

108 Just (Function (Fun _ _ _ v)) -> return v

100 Just (TyDecl nt ty hty) -> return $ VP nt n hty

109 Just (TyDecl nt ty hty) -> return $ VP nt n hty

101− Just (CaseOp _ _ [] tree) ->

110+ Just (CaseOp inl _ _ [] tree) ->

111+ if simpl && (not inl)

112+ then liftM (VP Ref n) (ev top env ty)

102− do c <- evCase top env [] [] tree

113+ else do c <- evCase top env [] [] tree

103− case c of

114+ case c of

104− (Nothing, _) -> liftM (VP Ref n) (ev top env ty)

115+ (Nothing, _) -> liftM (VP Ref n) (ev top env ty)

105− (Just v, _) -> return v

116+ (Just v, _) -> return v

106 _ -> liftM (VP Ref n) (ev top env ty)

117 _ -> liftM (VP Ref n) (ev top env ty)

107 ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)

118 ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)

108 ev top env (V i) | i < length env = return $ env !! i

119 ev top env (V i) | i < length env = return $ env !! i

@@ -137,12 +148,13 @@ eval ctxt statics genv tm opts = ev True [] tm where

137 apply False env f args

148 apply False env f args

138 | spec = return $ unload env f args

149 | spec = return $ unload env f args

139 apply top env (VP Ref n ty) args

150 apply top env (VP Ref n ty) args

140− | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

151+ | Just (CaseOp inl _ _ ns tree) <- lookupDef n ctxt

141 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

152 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

153+ if simpl && (not inl) then return $ unload env (VP Ref n ty) args

142− do c <- evCase top env ns args tree

154+ else do c <- evCase top env ns args tree

143− case c of

155+ case c of

144− (Nothing, _) -> return $ unload env (VP Ref n ty) args

156+ (Nothing, _) -> return $ unload env (VP Ref n ty) args

145− (Just v, rest) -> evApply top env rest v

157+ (Just v, rest) -> evApply top env rest v

146 | Just (Operator _ i op) <- lookupDef n ctxt

158 | Just (Operator _ i op) <- lookupDef n ctxt

147 = if (i <= length args)

159 = if (i <= length args)

148 then case op (take i args) of

160 then case op (take i args) of

@@ -282,7 +294,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

282 ev env (P Ref n ty) = case lookupDef n ctxt of

294 ev env (P Ref n ty) = case lookupDef n ctxt of

283 Just (Function (Fun _ _ t _)) -> ev env t

295 Just (Function (Fun _ _ t _)) -> ev env t

284 Just (TyDecl nt ty hty) -> return $ HP nt n ty

296 Just (TyDecl nt ty hty) -> return $ HP nt n ty

285− Just (CaseOp _ _ [] tree) ->

297+ Just (CaseOp inl _ _ [] tree) ->

286 do c <- evCase env [] [] tree

298 do c <- evCase env [] [] tree

287 case c of

299 case c of

288 (Nothing, _, _) -> return $ HP Ref n ty

300 (Nothing, _, _) -> return $ HP Ref n ty

@@ -312,7 +324,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

312 app <- apply env sc' as

324 app <- apply env sc' as

313 wknH (-1) app

325 wknH (-1) app

314 apply env (HP Ref n ty) args

326 apply env (HP Ref n ty) args

315− | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

327+ | Just (CaseOp _ _ _ ns tree) <- lookupDef n ctxt

316 = do c <- evCase env ns args tree

328 = do c <- evCase env ns args tree

317 case c of

329 case c of

318 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

330 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -415,13 +427,14 @@ data Fun = Fun Type Value Term Value

415data Def = Function Fun

427data Def = Function Fun

416 | TyDecl NameType Type Value

428 | TyDecl NameType Type Value

417 | Operator Type Int ([Value] -> Maybe Value)

429 | Operator Type Int ([Value] -> Maybe Value)

418− | CaseOp Type [(Term, Term)] [Name] SC

430+ | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

419

431

420instance Show Def where

432instance Show Def where

421 show (Function f) = "Function: " ++ show f

433 show (Function f) = "Function: " ++ show f

422 show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

434 show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

423 show (Operator ty _ _) = "Operator: " ++ show ty

435 show (Operator ty _ _) = "Operator: " ++ show ty

424− show (CaseOp ty _ ns sc) = "Case: " ++ show ns ++ " " ++ show sc

436+ show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

437+ show ns ++ " " ++ show sc

425

438

426-------

439-------

427

440

@@ -448,10 +461,14 @@ addDatatype (Data n tag ty cons) ctxt

448 addCons (tag+1) cons (addDef n

461 addCons (tag+1) cons (addDef n

449 (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)

462 (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)

450

463

451−addCasedef :: Name -> Bool -> [(Term, Term)] -> Type -> Context -> Context

464+addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

452−addCasedef n tcase ps ty ctxt

465+addCasedef n alwaysInline tcase ps ty ctxt

466+ = let ps' = simpl ps in

453− = case simpleCase tcase ps of

467+ case simpleCase tcase ps' of

468+ CaseDef args sc -> let inl = alwaysInline in

454− CaseDef args sc -> addDef n (CaseOp ty ps args sc) ctxt

469+ addDef n (CaseOp inl ty ps args sc) ctxt

470+ where simpl [] = []

471+ simpl ((l,r) : xs) = (l, simplify ctxt [] r) : simpl xs

455

472

456addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

473addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

457addOperator n ty a op ctxt

474addOperator n ty a op ctxt

@@ -463,7 +480,7 @@ lookupTy n ctxt = do def <- lookupCtxt n ctxt

463 (Function (Fun ty _ _ _)) -> return ty

480 (Function (Fun ty _ _ _)) -> return ty

464 (TyDecl _ ty _) -> return ty

481 (TyDecl _ ty _) -> return ty

465 (Operator ty _ _) -> return ty

482 (Operator ty _ _) -> return ty

466− (CaseOp ty _ _ _) -> return ty

483+ (CaseOp _ ty _ _ _) -> return ty

467

484

468lookupP :: Name -> Context -> Maybe Term

485lookupP :: Name -> Context -> Maybe Term

469lookupP n ctxt

486lookupP n ctxt

@@ -471,7 +488,7 @@ lookupP n ctxt

471 case def of

488 case def of

472 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

489 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

473 (TyDecl nt ty hty) -> return (P nt n ty)

490 (TyDecl nt ty hty) -> return (P nt n ty)

474− (CaseOp ty _ _ _) -> return (P Ref n ty)

491+ (CaseOp _ ty _ _ _) -> return (P Ref n ty)

475 (Operator ty _ _) -> return (P Ref n ty)

492 (Operator ty _ _) -> return (P Ref n ty)

476

493

477lookupDef :: Name -> Context -> Maybe Def

494lookupDef :: Name -> Context -> Maybe Def

src/Idris/AbsSyntax.hs+12−7

146 | Compile String | Execute String

147 | Metavars | Prove Name

148 | TTShell

149− | LogLvl Int | Spec PTerm | HNF PTerm

149+ | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

150 | NOP

151

152-- Parsed declarations

@@ -186,9 +186,14 @@ impl = Imp False Dynamic

186expl = Exp False Dynamic

187constraint = Constraint False Static

188

189+type FnOpts = Bool -- just inlinable, for now

190+

191+inlinable :: FnOpts -> Bool

192+inlinable x = x

193+

189data PDecl' t = PFix FC Fixity [String] -- fixity declaration

194data PDecl' t = PFix FC Fixity [String] -- fixity declaration

190 | PTy SyntaxInfo FC Name t -- type declaration

195 | PTy SyntaxInfo FC Name t -- type declaration

191− | PClauses FC Name [PClause' t] -- pattern clause

196+ | PClauses FC FnOpts Name [PClause' t] -- pattern clause

192 | PData SyntaxInfo FC (PData' t) -- data declaration

197 | PData SyntaxInfo FC (PData' t) -- data declaration

193 | PParams FC [(Name, t)] [PDecl' t] -- params block

198 | PParams FC [(Name, t)] [PDecl' t] -- params block

194 | PClass SyntaxInfo FC

199 | PClass SyntaxInfo FC

@@ -225,7 +230,7 @@ type PClause = PClause' PTerm

225declared :: PDecl -> [Name]

230declared :: PDecl -> [Name]

226declared (PFix _ _ _) = []

231declared (PFix _ _ _) = []

227declared (PTy _ _ n t) = [n]

232declared (PTy _ _ n t) = [n]

228−declared (PClauses _ n _) = [] -- not a declaration

233+declared (PClauses _ _ n _) = [] -- not a declaration

229declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

234declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

230 where fstt (a, _, _) = a

235 where fstt (a, _, _) = a

231declared (PParams _ _ ds) = concatMap declared ds

236declared (PParams _ _ ds) = concatMap declared ds

@@ -369,7 +374,7 @@ instance Show PTerm where

369instance Show PDecl where

374instance Show PDecl where

370 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

375 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

371 show (PTy _ _ n ty) = show n ++ " : " ++ show ty

376 show (PTy _ _ n ty) = show n ++ " : " ++ show ty

372− show (PClauses _ n c) = showSep "\n" (map show c)

377+ show (PClauses _ _ n c) = showSep "\n" (map show c)

373 show (PData _ _ d) = show d

378 show (PData _ _ d) = show d

374

379

375instance Show PClause where

380instance Show PClause where

@@ -611,9 +616,9 @@ expandParamsD ist dec ps ns (PTy syn fc n ty)

611 = if n `elem` ns

616 = if n `elem` ns

612 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

617 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

613 else PTy syn fc n (expandParams dec ps ns ty)

618 else PTy syn fc n (expandParams dec ps ns ty)

614−expandParamsD ist dec ps ns (PClauses fc n cs)

619+expandParamsD ist dec ps ns (PClauses fc opts n cs)

615 = let n' = if n `elem` ns then dec n else n in

620 = let n' = if n `elem` ns then dec n else n in

616− PClauses fc n' (map expandParamsC cs)

621+ PClauses fc opts n' (map expandParamsC cs)

617 where

622 where

618 expandParamsC (PClause n lhs ws rhs ds)

623 expandParamsC (PClause n lhs ws rhs ds)

619 = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])

624 = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])

@@ -859,7 +864,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

859

864

860dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

865dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

861dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

866dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

862−dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

867+dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

863dumpDecl (PData _ _ d) = showDImp True d

868dumpDecl (PData _ _ d) = showDImp True d

864dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

869dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

865dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

870dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

src/Idris/Compiler.hs+1−1

@@ -46,7 +46,7 @@ impossible = int 42424242

47instance ToEpic Def where

48 epic (Function (Fun _ _ tm _)) = epic tm

49− epic (CaseOp _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

49+ epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

50 epic _ = return impossible

52instance ToEpic (TT Name) where

src/Idris/ElabDecls.hs+12−11

@@ -85,8 +85,8 @@ elabCon info syn (n, t_in, fc)

85 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

86 return (n, cty)

88−elabClauses :: ElabInfo -> FC -> Name -> [PClause] -> Idris ()

88+elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

89−elabClauses info fc n_in cs = let n = liftname info n_in in

89+elabClauses info fc opts n_in cs = let n = liftname info n_in in

90 do solveDeferred n

91 pats <- mapM (elabClause info fc) cs

92 logLvl 3 (showSep "\n" (map (\ (l,r) ->

@@ -98,7 +98,8 @@ elabClauses info fc n_in cs = let n = liftname info n_in in

98 logLvl 3 (show tree)

99 ctxt <- getContext

100 case lookupTy n ctxt of

101− Just ty -> updateContext (addCasedef n tcase (map debind pats) ty)

101+ Just ty -> updateContext (addCasedef n (inlinable opts)

102+ tcase (map debind pats) ty)

102 Nothing -> return ()

103 Nothing -> return ()

103 where

104 where

104 debind (x, y) = (depat x, depat y)

105 debind (x, y) = (depat x, depat y)

@@ -249,9 +250,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

249 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

250 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

250 getImps _ = []

251 getImps _ = []

251

252

252− mkAuxC wname lhs ns (PClauses fc n cs)

253+ mkAuxC wname lhs ns (PClauses fc o n cs)

253 | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

254 | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

254− return $ PClauses fc wname cs'

255+ return $ PClauses fc o wname cs'

255 | otherwise = fail $ "with clause uses wrong function name " ++ show n

256 | otherwise = fail $ "with clause uses wrong function name " ++ show n

256 mkAuxC wname lhs ns d = return $ d

257 mkAuxC wname lhs ns d = return $ d

257

258

@@ -313,7 +314,7 @@ elabClass info syn fc constraints tn ps ds

313 tdecl (PTy syn _ n t) = do t' <- implicit syn n t

314 tdecl (PTy syn _ n t) = do t' <- implicit syn n t

314 return ( (n, (toExp (map fst ps) Exp t')),

315 return ( (n, (toExp (map fst ps) Exp t')),

315 (n, (toExp (map fst ps) Imp t')) )

316 (n, (toExp (map fst ps) Imp t')) )

316− tdecl (PClauses _ _ _) = fail "No default definitions allowed yet"

317+ tdecl (PClauses _ _ _ _) = fail "No default definitions allowed yet"

317 tdecl _ = fail "Not allowed in a class declaration"

318 tdecl _ = fail "Not allowed in a class declaration"

318

319

319 tfun cn c syn all (m, ty)

320 tfun cn c syn all (m, ty)

@@ -328,7 +329,7 @@ elabClass info syn fc constraints tn ps ds

328 iLOG (show (m, ty', capp, margs))

329 iLOG (show (m, ty', capp, margs))

329 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

330 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

330 return [PTy syn fc m ty',

331 return [PTy syn fc m ty',

331− PClauses fc m [PClause m lhs [] rhs []]]

332+ PClauses fc True m [PClause m lhs [] rhs []]]

332

333

333 getMArgs (PPi (Imp _ _) n ty sc) = False : getMArgs sc

334 getMArgs (PPi (Imp _ _) n ty sc) = False : getMArgs sc

334 getMArgs (PPi (Exp _ _) n ty sc) = True : getMArgs sc

335 getMArgs (PPi (Exp _ _) n ty sc) = True : getMArgs sc

@@ -374,7 +375,7 @@ elabInstance info syn fc cs n ps t ds

374 let lhs = PRef fc iname

375 let lhs = PRef fc iname

375 let rhs = PApp fc (PRef fc (instanceName ci))

376 let rhs = PApp fc (PRef fc (instanceName ci))

376 (map (pexp . mkMethApp) mtys)

377 (map (pexp . mkMethApp) mtys)

377− let idecl = PClauses fc iname [PClause iname lhs [] rhs wb]

378+ let idecl = PClauses fc True iname [PClause iname lhs [] rhs wb]

378 iLOG (show idecl)

379 iLOG (show idecl)

379 elabDecl info idecl

380 elabDecl info idecl

380 where

381 where

@@ -394,7 +395,7 @@ elabInstance info syn fc cs n ps t ds

394 papp fc f as = PApp fc f as

395 papp fc f as = PApp fc f as

395 decorate (UN (n:ns)) = UN (('!':n) : ns)

396 decorate (UN (n:ns)) = UN (('!':n) : ns)

396 decorateid (PTy s f n t) = PTy s f (decorate n) t

397 decorateid (PTy s f n t) = PTy s f (decorate n) t

397− decorateid (PClauses f n cs) = PClauses f (decorate n) (map dc cs)

398+ decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)

398 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

399 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

399 dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w ds

400 dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w ds

400 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

401 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

@@ -442,8 +443,8 @@ elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n

442 elabType info s f n ty

443 elabType info s f n ty

443elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

444elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

444 elabData info s f d

445 elabData info s f d

445−elabDecl' info d@(PClauses f n ps) = do iLOG $ "Elaborating clause " ++ show n

446+elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

446− elabClauses info f n ps

447+ elabClauses info f o n ps

447elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

448elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

448 where

449 where

449 pinfo = let ds = concatMap declared ps

450 pinfo = let ds = concatMap declared ps

src/Idris/Parser.hs+8−8

@@ -132,17 +132,17 @@ parseProg syn fname input pos

132-- Collect PClauses with the same function name

133

134collect :: [PDecl] -> [PDecl]

135−collect (c@(PClauses _ _ _) : ds)

135+collect (c@(PClauses _ o _ _) : ds)

136 = clauses (cname c) [] (c : ds)

137− where clauses n acc (PClauses fc _ [PClause n' l ws r w] : ds)

137+ where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds)

138 | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds

139− clauses n acc (PClauses fc _ [PWith n' l ws r w] : ds)

139+ clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)

140 | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds

141− clauses n acc xs = PClauses (getfc c) n (reverse acc) : collect xs

141+ clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs

142

143− cname (PClauses fc _ [PClause n _ _ _ _]) = n

143+ cname (PClauses fc _ _ [PClause n _ _ _ _]) = n

144− cname (PClauses fc _ [PWith n _ _ _ _]) = n

144+ cname (PClauses fc _ _ [PWith n _ _ _ _]) = n

145− getfc (PClauses fc _ _) = fc

145+ getfc (PClauses fc _ _ _) = fc

146

147collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

148collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

@@ -591,7 +591,7 @@ pSimpleCon syn

591pPattern :: SyntaxInfo -> IParser PDecl

592pPattern syn = do clause <- pClause syn

593 fc <- pfc

594− return (PClauses fc (MN 2 "_") [clause]) -- collect together later

594+ return (PClauses fc False (MN 2 "_") [clause]) -- collect together later

595

596whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

597whereSyn n syn args = let ns = concatMap allNamesIn args

src/Idris/Prover.hs+1−1

@@ -38,7 +38,7 @@ prove ctxt n ty

38 let tree = simpleCase False [(P Ref n ty, tm)]

39 logLvl 3 (show tree)

40 (ptm, pty) <- tclift $ recheck ctxt [] tm

41− updateContext (addCasedef n False [(P Ref n ty, ptm)] ty)

41+ updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

42 solveDeferred n

44elabStep :: ElabState -> Elab a -> Idris (a, ElabState)

src/Idris/REPL.hs+3−1

@@ -92,6 +92,8 @@ process _ (Check t) = do (tm, ty) <- elabVal toplevel False t

92 let ty' = normaliseC ctxt [] ty

93 iputStrLn (show (delab ist tm) ++ " : " ++

94 show (delab ist ty'))

95+process _ (Defn n) = do ctxt <- getContext

96+ lift $ print (lookupDef n ctxt)

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

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

96 ctxt <- getContext

98 ctxt <- getContext

97 ist <- get

99 ist <- get

@@ -101,7 +103,7 @@ process _ (Prove n) = prover n

101process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t

103process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t

102 ctxt <- getContext

104 ctxt <- getContext

103 ist <- get

105 ist <- get

104− let tm' = hnf ctxt [] tm

106+ let tm' = simplify ctxt [] tm

105 iputStrLn (show (delab ist tm'))

107 iputStrLn (show (delab ist tm'))

106process _ TTShell = do ist <- get

108process _ TTShell = do ist <- get

107 let shst = initState (tt_ctxt ist)

109 let shst = initState (tt_ctxt ist)

src/Idris/REPLParser.hs+1

@@ -32,6 +32,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

32 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

33 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

34 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

35+ <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

35 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

36 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

36 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

37 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

37 <|> do eof; return NOP

38 <|> do eof; return NOP