bf368ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

First attempt at with rule

commitbf368ab3fe6308a845644b406bbef115bdc31fc9 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 00:48 (15 years ago) parentcc4eb28

8 files changed+211−46

compare with master

unifiedsplit

src/Core/CaseTree.hs+13−5 src/Core/CoreParser.hs+1−1 src/Core/TT.hs+7 src/Core/Typecheck.hs−1 src/Idris/AbsSyntax.hs+21−5 src/Idris/Compiler.hs+8−1 src/Idris/ElabDecls.hs+107−19 src/Idris/Parser.hs+54−14

src/Core/CaseTree.hs+13−5

@@ -2,9 +2,9 @@ module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

22 simpleCase) where

44import Core.TT

5−-- import Core.Evaluate

76import Control.Monad.State

7+import Debug.Trace

99data CaseDef = CaseDef [Name] SC

1010 deriving Show

@@ -48,17 +48,25 @@ toPats f = reverse (toPat (getArgs f)) where

4848toPat :: [Term] -> [Pat]

4949toPat tms = evalState (mapM (\x -> toPat' x []) tms) []

5050 where

51− toPat' (P (DCon t a) n _) args = return $ PCon n t args

51+ toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

52+ return $ PCon n t args'

5253 toPat' (P Bound n _) [] = do ns <- get

5354 if n `elem` ns

5455 then return PAny

5556 else do put (n : ns)

5657 return (PV n)

57− toPat' (App f a) args = do a' <- toPat' a []

58− toPat' f (a' : args)

59− toPat' (Constant c) args = return $ PConst c

58+ toPat' (App f a) args = toPat' f (a : args)

59+ toPat' (Constant c) args

60+ | isType c = return PAny

61+ | otherwise = return $ PConst c

6062 toPat' _ _ = return PAny

6163

64+ isType (I _) = False

65+ isType (Fl _) = False

66+ isType (Str _) = False

67+ isType (Ch _) = False

68+ isType _ = True

69+

6270data Partition = Cons [Clause]

6371 | Vars [Clause]

6472

src/Core/CoreParser.hs+1−1

@@ -21,7 +21,7 @@ idrisDef = haskellDef {

2121 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

2222 "do", "dsl", "import",

2323 "infix", "infixl", "infixr", "prefix",

24− "where", "forall", "syntax",

24+ "where", "with", "forall", "syntax",

2525 "using", "params", "namespace",

2626 "Int", "Float", "Char", "String", "Ptr"]

2727 }

src/Core/TT.hs+7

@@ -273,6 +273,13 @@ forget tm = fe [] tm

273273 = RConstant c

274274 fe env (Set i) = RSet i

275275

276+bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

277+bindAll [] t =t

278+bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)

279+

280+bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n

281+bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

282+

276283type Term = TT Name

277284type Type = Term

278285

src/Core/Typecheck.hs−1

@@ -119,7 +119,6 @@ check ctxt env (RBind n b sc)

119119 let tt' = normalise ctxt env tt

120120 isSet ctxt env tt'

121121 return (PVTy tv')

122− checkBinder x = fail (show x)

123122

124123 discharge n (Lam t) scv sct

125124 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

src/Idris/AbsSyntax.hs+21−5

@@ -140,7 +140,8 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

140140 | PSyntax FC Syntax

141141 deriving Functor

142142

143−data PClause' t = PClause Name t t [PDecl]

143+data PClause' t = PClause Name t [t] t [PDecl]

144+ | PWith Name t [t] t [PDecl]

144145 deriving Functor

145146

146147data PData' t = PDatadecl { d_name :: Name,

@@ -231,14 +232,26 @@ instance Show PDecl where

231232 show (PData _ d) = show d

232233

233234instance Show PClause where

234− show c = showCImp False c

235+ show c = showCImp True c

235236

236237instance Show PData where

237238 show d = showDImp False d

238239

239240showCImp :: Bool -> PClause -> String

240−showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r

241− ++ " where " ++ show w

241+showCImp impl (PClause n l ws r w)

242+ = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r

243+ ++ " where " ++ show w

244+ where

245+ showWs [] = ""

246+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs

247+showCImp impl (PWith n l ws r w)

248+ = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r

249+ ++ " { " ++ show w ++ " } "

250+ where

251+ showWs [] = ""

252+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs

253+

254+

242255showDImp :: Bool -> PData -> String

243256showDImp impl (PDatadecl n ty cons)

244257 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

@@ -366,7 +379,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

366379 [(pairCon, PPi Imp (n "A") PSet (

367380 PPi Imp (n "B") PSet (

368381 PPi Exp (n "a") (PRef bi (n "A")) (

369− PPi Exp (n "c") (PRef bi (n "B"))

382+ PPi Exp (n "b") (PRef bi (n "B"))

370383 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),

371384 PExp (PRef bi (n "B"))])))), bi)]

372385 where n a = MN 0 a

@@ -426,6 +439,9 @@ addImpl :: IState -> PTerm -> PTerm

426439addImpl ist ptm = ai [] ptm

427440 where

428441 ai env (PRef fc f) = aiFn fc env (PRef fc f) []

442+ ai env (PPair fc l r) = let l' = ai env l

443+ r' = ai env r in

444+ PPair fc l' r'

429445 ai env (PApp fc (PRef _ f) as)

430446 = let as' = map (fmap (ai env)) as in

431447 aiFn fc env (PRef fc f) as'

src/Idris/Compiler.hs+8−1

@@ -58,6 +58,10 @@ instance ToEpic (TT Name) where

5858 epic' env (Bind n (Lam _) sc)

5959 = do sc' <- epic' (aname n : env) sc

6060 return $ term ([aname n], sc')

61+ epic' env (Bind n (Let _ v) sc)

62+ = do sc' <- epic' (aname n : env) sc

63+ v' <- epic' env v

64+ return $ let_ v' (aname n, sc')

6165 epic' env (Bind _ _ _) = return impossible

6266 epic' env (App f a) = do f' <- epic' env f

6367 a' <- epic' env a

@@ -112,7 +116,10 @@ instance ToEpic SC where

112116 return $ con t (map ename args, rhs')

113117 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs

114118 return $ constcase i rhs'

115− mkEpicAlt (ConstCase _ rhs) = fail "Can only pattern match on integer constants"

119+ mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs

120+ return $ defaultcase rhs'

121+ mkEpicAlt (ConstCase c rhs)

122+ = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"

116123 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs

117124 return $ defaultcase rhs'

118125

src/Idris/ElabDecls.hs+107−19

@@ -97,7 +97,7 @@ elabVal info tm

9797 tclift $ recheck ctxt [] vtm

9898

9999elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

100−elabClause info fc (PClause fname lhs rhs whereblock)

100+elabClause info fc (PClause fname lhs withs rhs whereblock)

101101 = do ctxt <- getContext

102102 -- Build the LHS as an "Infer", and pull out its type and

103103 -- pattern bindings

@@ -116,28 +116,19 @@ elabClause info fc (PClause fname lhs rhs whereblock)

116116 -- Now build the RHS, using the type of the LHS as the goal.

117117 logLvl 2 (showImp True rhs)

118118 ctxt <- getContext -- new context with where block added

119− ((rhs', defer), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

120− (do pbinds lhs_tm

121− (_, d) <- erun fc (build winfo False rhs)

122− psolve lhs_tm

123− tt <- get_term

124− return (tt, d))

119+ ((rhs', defer), _) <-

120+ tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

121+ (do pbinds lhs_tm

122+ (_, d) <- erun fc (build winfo False rhs)

123+ psolve lhs_tm

124+ tt <- get_term

125+ return (tt, d))

125126 logLvl 2 $ "---> " ++ show rhs'

126127 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

127128 addDeferred defer

128129 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

129130 return (clhs, crhs)

130131 where

131− pbinds (Bind n (PVar t) sc) = do attack; patbind n

132− pbinds sc

133− pbinds tm = return ()

134−

135− psolve (Bind n (PVar t) sc) = do solve; psolve sc

136− psolve tm = return ()

137−

138− pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

139− pvars ist _ = []

140−

141132 pinfo ns ps i

142133 = let ds = concatMap declared ps

143134 newps = params info ++ ns

@@ -151,6 +142,103 @@ elabClause info fc (PClause fname lhs rhs whereblock)

151142 _ -> MN i (show n)) . l

152143 }

153144

145+elabClause info fc (PWith fname lhs withs wval withblock)

146+ = do ctxt <- getContext

147+ -- Build the LHS as an "Infer", and pull out its type and

148+ -- pattern bindings

149+ ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

150+ (erun fc (build info True (infTerm lhs)))

151+ let lhs_tm = getInferTerm lhs'

152+ let lhs_ty = getInferType lhs'

153+ let ret_ty = getRetTy lhs_ty

154+ logLvl 3 (show lhs_tm)

155+ (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

156+ logLvl 5 ("Checked " ++ show clhs)

157+ logLvl 5 ("Checking " ++ show wval)

158+ let bargs = getPBtys lhs_tm

159+ -- Elaborate wval in this context

160+ ((wval', defer), _) <-

161+ tclift $ elaborate ctxt (MN 0 "withRHS")

162+ (bindTyArgs PVTy bargs infP)

163+ (do pbinds lhs_tm

164+ -- TODO: may want where here - see winfo abpve

165+ (_', d) <- erun fc (build info False (infTerm wval))

166+ psolve lhs_tm

167+ tt <- get_term

168+ return (tt, d))

169+ addDeferred defer

170+ (cwval, cwvalty) <- tclift $ recheck ctxt [] (getInferTerm wval')

171+ logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

172+ windex <- getName

173+ -- build a type declaration for the new function:

174+ -- (ps : Xs) -> (withval : cwvalty) -> ret_ty

175+ let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

176+ logLvl 3 ("New function type " ++ show wtype)

177+ let wname = MN windex (show fname)

178+ addDeferred [(wname, wtype)]

179+

180+ -- in the subdecls, lhs becomes:

181+ -- fname pats | wpat [rest]

182+ -- ==> fname' ps wpat [rest]

183+ wb <- mapM (mkAuxC wname (map fst bargs)) withblock

184+ logLvl 5 ("with block " ++ show wb)

185+ mapM_ (elabDecl info) wb

186+

187+ -- rhs becomes: fname' ps wval

188+ let rhs = PApp fc (PRef fc wname) (map (PExp . (PRef fc) . fst) bargs ++

189+ [PExp wval])

190+ logLvl 3 ("New RHS " ++ show rhs)

191+ ctxt <- getContext -- New context with block added

192+ ((rhs', defer), _) <-

193+ tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty

194+ (do pbinds lhs_tm

195+ (_, d) <- erun fc (build info False rhs)

196+ psolve lhs_tm

197+ tt <- get_term

198+ return (tt, d))

199+ addDeferred defer

200+ (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

201+ return (clhs, crhs)

202+ where

203+ mkAuxC wname ns (PClauses fc n cs)

204+ | n == fname = do cs' <- mapM (mkAux wname ns) cs

205+ return $ PClauses fc wname cs'

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

207+ mkAuxC wname ns d = return $ d

208+

209+ mkAux wname ns (PClause n tm (w:ws) rhs wheres)

210+ = do lhs <- updateLHS n wname ns tm w

211+ return $ PClause wname lhs ws rhs wheres

212+ mkAux wname ns (PWith n tm (w:ws) wval wheres)

213+ = do lhs <- updateLHS n wname ns tm w

214+ return $ PWith wname lhs ws wval wheres

215+

216+ updateLHS n wname ns (PApp fc (PRef fc' n') args) w

217+ = return $ PApp fc (PRef fc' wname)

218+ (map (PExp . (PRef fc')) ns ++ [PExp w])

219+ updateLHS n wname ns tm w = fail $ "Not implemented " ++ show tm

220+

221+pbinds (Bind n (PVar t) sc) = do attack; patbind n

222+ pbinds sc

223+pbinds tm = return ()

224+

225+pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)

226+pbty _ tm = tm

227+

228+getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

229+getPBtys _ = []

230+

231+getRetTy (Bind n (PVar _) sc) = getRetTy sc

232+getRetTy (Bind n (PVTy _) sc) = getRetTy sc

233+getRetTy (Bind n (Pi _) sc) = getRetTy sc

234+getRetTy sc = sc

235+

236+psolve (Bind n (PVar t) sc) = do solve; psolve sc

237+psolve tm = return ()

238+

239+pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

240+pvars ist _ = []

241+

154242-- TODO: Also build a 'binary' version of each declaration for fast reloading

155243

156244elabDecl :: ElabInfo -> PDecl -> Idris ()

@@ -215,8 +303,8 @@ elab info pattern tm = do elab' tm

215303 elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)

216304 [PExp l,PExp r]))

217305 (elab' (PApp fc (PRef fc pairCon)

218− [PImp (MN 0 "a") Placeholder,

219− PImp (MN 0 "a") Placeholder,

306+ [PImp (MN 0 "A") Placeholder,

307+ PImp (MN 0 "B") Placeholder,

220308 PExp l, PExp r]))

221309 elab' (PRef fc n) | pattern && not (inparamBlock n)

222310 = erun fc $

src/Idris/Parser.hs+54−14

@@ -114,10 +114,18 @@ parseProg syn fname input pos

114114

115115-- Collect PClauses with the same function name

116116collect :: [PDecl] -> [PDecl]

117−collect (c@(PClauses fc _ [PClause n l r w]) : ds) = clauses n [] (c:ds)

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

119− | n == n' = clauses n (PClause n' l r (collect w) : acc) ds

120− clauses n acc xs = PClauses fc n (reverse acc) : collect xs

117+collect (c@(PClauses _ _ _) : ds)

118+ = clauses (cname c) [] (c : ds)

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

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

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

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

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

124+

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

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

127+ getfc (PClauses fc _ _) = fc

128+

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

122130collect (d : ds) = d : collect ds

123131collect [] = []

@@ -480,24 +488,56 @@ pPattern syn = do fc <- pfc

480488

481489pClause :: SyntaxInfo -> IParser PClause

482490pClause syn

483− = try (do n <- pfName

484− iargs <- many (pImplicitArg syn)

485− fc <- pfc

486− args <- many (pHSimpleExpr syn)

487− lchar '='

488− rhs <- pExpr syn

489− wheres <- choice [pWhereblock syn, do lchar ';'; return []]

490− return $ PClause n (PApp fc (PRef fc n)

491− (iargs ++ map PExp args)) rhs wheres)

491+ = try (do n <- pfName

492+ iargs <- many (pImplicitArg syn)

493+ fc <- pfc

494+ args <- many (pHSimpleExpr syn)

495+ wargs <- many (pWExpr syn)

496+ lchar '='

497+ rhs <- pExpr syn

498+ wheres <- choice [pWhereblock syn, do lchar ';'; return []]

499+ return $ PClause n (PApp fc (PRef fc n)

500+ (iargs ++ map PExp args)) wargs rhs wheres)

501+ <|> try (do n <- pfName

502+ iargs <- many (pImplicitArg syn)

503+ fc <- pfc

504+ args <- many (pHSimpleExpr syn)

505+ wargs <- many (pWExpr syn)

506+ reserved "with"

507+ wval <- pSimpleExpr syn

508+ lchar '{'

509+ ds <- many1 $ pFunDecl syn

510+ let withs = concat ds

511+ lchar '}'

512+ return $ PWith n (PApp fc (PRef fc n)

513+ (iargs ++ map PExp args)) wargs wval withs)

514+

492515 <|> do l <- pSimpleExpr syn

493516 op <- operator

494517 let n = UN [op]

495518 r <- pSimpleExpr syn

496519 fc <- pfc

520+ wargs <- many (pWExpr syn)

497521 lchar '='

498522 rhs <- pExpr syn

499523 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

500− return $ PClause n (PApp fc (PRef fc n) [PExp l,PExp r]) rhs wheres

524+ return $ PClause n (PApp fc (PRef fc n) [PExp l,PExp r]) wargs rhs wheres

525+

526+ <|> do l <- pSimpleExpr syn

527+ op <- operator

528+ let n = UN [op]

529+ r <- pSimpleExpr syn

530+ fc <- pfc

531+ wargs <- many (pWExpr syn)

532+ wval <- pExpr syn

533+ lchar '{'

534+ ds <- many1 $ pFunDecl syn

535+ let withs = concat ds

536+ lchar '}'

537+ return $ PWith n (PApp fc (PRef fc n) [PExp l, PExp r]) wargs wval withs

538+

539+pWExpr :: SyntaxInfo -> IParser PTerm

540+pWExpr syn = do lchar '|'; pExpr' syn

501541

502542pWhereblock :: SyntaxInfo -> IParser [PDecl]

503543pWhereblock syn = do reserved "where"; lchar '{'