git.iko.soy/Idris-dev
on master help sign in
First attempt at with rule
bf368abEdwin Brady
src/Core/CaseTree.hs+13−5
compare with master
unifiedsplit
@@ -2,9 +2,9 @@ module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,
2 simpleCase) where
2 simpleCase) where
3
3
4import Core.TT
4import Core.TT
5−-- import Core.Evaluate
6
5
7import Control.Monad.State
6import Control.Monad.State
7+import Debug.Trace
8
8
9data CaseDef = CaseDef [Name] SC
9data CaseDef = CaseDef [Name] SC
10 deriving Show
10 deriving Show
@@ -48,17 +48,25 @@ toPats f = reverse (toPat (getArgs f)) where
48toPat :: [Term] -> [Pat]
48toPat :: [Term] -> [Pat]
49toPat tms = evalState (mapM (\x -> toPat' x []) tms) []
49toPat tms = evalState (mapM (\x -> toPat' x []) tms) []
50 where
50 where
51+ toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
51− toPat' (P (DCon t a) n _) args = return $ PCon n t args
52+ return $ PCon n t args'
52 toPat' (P Bound n _) [] = do ns <- get
53 toPat' (P Bound n _) [] = do ns <- get
53 if n `elem` ns
54 if n `elem` ns
54 then return PAny
55 then return PAny
55 else do put (n : ns)
56 else do put (n : ns)
56 return (PV n)
57 return (PV n)
57− toPat' (App f a) args = do a' <- toPat' a []
58+ toPat' (App f a) args = toPat' f (a : args)
58− toPat' f (a' : args)
59− toPat' (Constant c) args = return $ PConst c
59+ toPat' (Constant c) args
60+ | isType c = return PAny
61+ | otherwise = return $ PConst c
60 toPat' _ _ = return PAny
62 toPat' _ _ = return PAny
61
63
64+ isType (I _) = False
65+ isType (Fl _) = False
66+ isType (Str _) = False
67+ isType (Ch _) = False
68+ isType _ = True
69+
62data Partition = Cons [Clause]
70data Partition = Cons [Clause]
63 | Vars [Clause]
71 | Vars [Clause]
64
72
src/Core/CoreParser.hs+1−1
@@ -21,7 +21,7 @@ idrisDef = haskellDef {
21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
22 "do", "dsl", "import",
22 "do", "dsl", "import",
23 "infix", "infixl", "infixr", "prefix",
23 "infix", "infixl", "infixr", "prefix",
24− "where", "forall", "syntax",
24+ "where", "with", "forall", "syntax",
25 "using", "params", "namespace",
25 "using", "params", "namespace",
26 "Int", "Float", "Char", "String", "Ptr"]
26 "Int", "Float", "Char", "String", "Ptr"]
27 }
27 }
src/Core/TT.hs+7
@@ -273,6 +273,13 @@ forget tm = fe [] tm
273 = RConstant c
273 = RConstant c
274 fe env (Set i) = RSet i
274 fe env (Set i) = RSet i
275
275
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+
276type Term = TT Name
283type Term = TT Name
277type Type = Term
284type Type = Term
278
285
src/Core/Typecheck.hs−1
@@ -119,7 +119,6 @@ check ctxt env (RBind n b sc)
119 let tt' = normalise ctxt env tt
119 let tt' = normalise ctxt env tt
120 isSet ctxt env tt'
120 isSet ctxt env tt'
121 return (PVTy tv')
121 return (PVTy tv')
122− checkBinder x = fail (show x)
123
122
124 discharge n (Lam t) scv sct
123 discharge n (Lam t) scv sct
125 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
124 = 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
140 | PSyntax FC Syntax
140 | PSyntax FC Syntax
141 deriving Functor
141 deriving Functor
142
142
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]
144 deriving Functor
145 deriving Functor
145
146
146data PData' t = PDatadecl { d_name :: Name,
147data PData' t = PDatadecl { d_name :: Name,
@@ -231,14 +232,26 @@ instance Show PDecl where
231 show (PData _ d) = show d
232 show (PData _ d) = show d
232
233
233instance Show PClause where
234instance Show PClause where
234− show c = showCImp False c
235+ show c = showCImp True c
235
236
236instance Show PData where
237instance Show PData where
237 show d = showDImp False d
238 show d = showDImp False d
238
239
239showCImp :: Bool -> PClause -> String
240showCImp :: Bool -> PClause -> String
240−showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
241+showCImp impl (PClause n l ws r w)
242+ = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
241− ++ " where " ++ show w
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+
242showDImp :: Bool -> PData -> String
255showDImp :: Bool -> PData -> String
243showDImp impl (PDatadecl n ty cons)
256showDImp impl (PDatadecl n ty cons)
244 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
257 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
@@ -366,7 +379,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
366 [(pairCon, PPi Imp (n "A") PSet (
379 [(pairCon, PPi Imp (n "A") PSet (
367 PPi Imp (n "B") PSet (
380 PPi Imp (n "B") PSet (
368 PPi Exp (n "a") (PRef bi (n "A")) (
381 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"))
370 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),
383 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),
371 PExp (PRef bi (n "B"))])))), bi)]
384 PExp (PRef bi (n "B"))])))), bi)]
372 where n a = MN 0 a
385 where n a = MN 0 a
@@ -426,6 +439,9 @@ addImpl :: IState -> PTerm -> PTerm
426addImpl ist ptm = ai [] ptm
439addImpl ist ptm = ai [] ptm
427 where
440 where
428 ai env (PRef fc f) = aiFn fc env (PRef fc f) []
441 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'
429 ai env (PApp fc (PRef _ f) as)
445 ai env (PApp fc (PRef _ f) as)
430 = let as' = map (fmap (ai env)) as in
446 = let as' = map (fmap (ai env)) as in
431 aiFn fc env (PRef fc f) as'
447 aiFn fc env (PRef fc f) as'
src/Idris/Compiler.hs+8−1
@@ -58,6 +58,10 @@ instance ToEpic (TT Name) where
58 epic' env (Bind n (Lam _) sc)
58 epic' env (Bind n (Lam _) sc)
59 = do sc' <- epic' (aname n : env) sc
59 = do sc' <- epic' (aname n : env) sc
60 return $ term ([aname n], sc')
60 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')
61 epic' env (Bind _ _ _) = return impossible
65 epic' env (Bind _ _ _) = return impossible
62 epic' env (App f a) = do f' <- epic' env f
66 epic' env (App f a) = do f' <- epic' env f
63 a' <- epic' env a
67 a' <- epic' env a
@@ -112,7 +116,10 @@ instance ToEpic SC where
112 return $ con t (map ename args, rhs')
116 return $ con t (map ename args, rhs')
113 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
117 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
114 return $ constcase i rhs'
118 return $ constcase i rhs'
119+ mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
120+ return $ defaultcase rhs'
121+ mkEpicAlt (ConstCase c rhs)
115− mkEpicAlt (ConstCase _ rhs) = fail "Can only pattern match on integer constants"
122+ = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
116 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
123 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
117 return $ defaultcase rhs'
124 return $ defaultcase rhs'
118
125
src/Idris/ElabDecls.hs+107−19
@@ -97,7 +97,7 @@ elabVal info tm
97 tclift $ recheck ctxt [] vtm
97 tclift $ recheck ctxt [] vtm
98
98
99elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)
99elabClause :: 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)
101 = do ctxt <- getContext
101 = do ctxt <- getContext
102 -- Build the LHS as an "Infer", and pull out its type and
102 -- Build the LHS as an "Infer", and pull out its type and
103 -- pattern bindings
103 -- pattern bindings
@@ -116,28 +116,19 @@ elabClause info fc (PClause fname lhs rhs whereblock)
116 -- Now build the RHS, using the type of the LHS as the goal.
116 -- Now build the RHS, using the type of the LHS as the goal.
117 logLvl 2 (showImp True rhs)
117 logLvl 2 (showImp True rhs)
118 ctxt <- getContext -- new context with where block added
118 ctxt <- getContext -- new context with where block added
119+ ((rhs', defer), _) <-
119− ((rhs', defer), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty
120+ tclift $ elaborate ctxt (MN 0 "patRHS") clhsty
120− (do pbinds lhs_tm
121+ (do pbinds lhs_tm
121− (_, d) <- erun fc (build winfo False rhs)
122+ (_, d) <- erun fc (build winfo False rhs)
122− psolve lhs_tm
123+ psolve lhs_tm
123− tt <- get_term
124+ tt <- get_term
124− return (tt, d))
125+ return (tt, d))
125 logLvl 2 $ "---> " ++ show rhs'
126 logLvl 2 $ "---> " ++ show rhs'
126 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
127 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
127 addDeferred defer
128 addDeferred defer
128 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'
129 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'
129 return (clhs, crhs)
130 return (clhs, crhs)
130 where
131 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−
141 pinfo ns ps i
132 pinfo ns ps i
142 = let ds = concatMap declared ps
133 = let ds = concatMap declared ps
143 newps = params info ++ ns
134 newps = params info ++ ns
@@ -151,6 +142,103 @@ elabClause info fc (PClause fname lhs rhs whereblock)
151 _ -> MN i (show n)) . l
142 _ -> MN i (show n)) . l
152 }
143 }
153
144
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+
154-- TODO: Also build a 'binary' version of each declaration for fast reloading
242-- TODO: Also build a 'binary' version of each declaration for fast reloading
155
243
156elabDecl :: ElabInfo -> PDecl -> Idris ()
244elabDecl :: ElabInfo -> PDecl -> Idris ()
@@ -215,8 +303,8 @@ elab info pattern tm = do elab' tm
215 elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)
303 elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)
216 [PExp l,PExp r]))
304 [PExp l,PExp r]))
217 (elab' (PApp fc (PRef fc pairCon)
305 (elab' (PApp fc (PRef fc pairCon)
218− [PImp (MN 0 "a") Placeholder,
306+ [PImp (MN 0 "A") Placeholder,
219− PImp (MN 0 "a") Placeholder,
307+ PImp (MN 0 "B") Placeholder,
220 PExp l, PExp r]))
308 PExp l, PExp r]))
221 elab' (PRef fc n) | pattern && not (inparamBlock n)
309 elab' (PRef fc n) | pattern && not (inparamBlock n)
222 = erun fc $
310 = erun fc $
src/Idris/Parser.hs+54−14
@@ -114,10 +114,18 @@ parseProg syn fname input pos
114
114
115-- Collect PClauses with the same function name
115-- Collect PClauses with the same function name
116collect :: [PDecl] -> [PDecl]
116collect :: [PDecl] -> [PDecl]
117−collect (c@(PClauses fc _ [PClause n l r w]) : ds) = clauses n [] (c:ds)
117+collect (c@(PClauses _ _ _) : ds)
118+ = clauses (cname c) [] (c : ds)
118− where clauses n acc (PClauses fc _ [PClause n' l r w] : ds)
119+ where clauses n acc (PClauses fc _ [PClause n' l ws r w] : ds)
119− | n == n' = clauses n (PClause n' l r (collect w) : acc) 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
120− clauses n acc xs = PClauses fc n (reverse acc) : collect xs
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+
121collect (PParams f ns ps : ds) = PParams f ns (collect ps) : (collect ds)
129collect (PParams f ns ps : ds) = PParams f ns (collect ps) : (collect ds)
122collect (d : ds) = d : collect ds
130collect (d : ds) = d : collect ds
123collect [] = []
131collect [] = []
@@ -480,24 +488,56 @@ pPattern syn = do fc <- pfc
480
488
481pClause :: SyntaxInfo -> IParser PClause
489pClause :: SyntaxInfo -> IParser PClause
482pClause syn
490pClause syn
483− = try (do n <- pfName
491+ = try (do n <- pfName
484− iargs <- many (pImplicitArg syn)
492+ iargs <- many (pImplicitArg syn)
485− fc <- pfc
493+ fc <- pfc
486− args <- many (pHSimpleExpr syn)
494+ args <- many (pHSimpleExpr syn)
495+ wargs <- many (pWExpr syn)
487− lchar '='
496+ lchar '='
488− rhs <- pExpr syn
497+ rhs <- pExpr syn
489− wheres <- choice [pWhereblock syn, do lchar ';'; return []]
498+ wheres <- choice [pWhereblock syn, do lchar ';'; return []]
490− return $ PClause n (PApp fc (PRef fc n)
499+ return $ PClause n (PApp fc (PRef fc n)
491− (iargs ++ map PExp args)) rhs wheres)
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+
492 <|> do l <- pSimpleExpr syn
515 <|> do l <- pSimpleExpr syn
493 op <- operator
516 op <- operator
494 let n = UN [op]
517 let n = UN [op]
495 r <- pSimpleExpr syn
518 r <- pSimpleExpr syn
496 fc <- pfc
519 fc <- pfc
520+ wargs <- many (pWExpr syn)
497 lchar '='
521 lchar '='
498 rhs <- pExpr syn
522 rhs <- pExpr syn
499 wheres <- choice [pWhereblock syn, do lchar ';'; return []]
523 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
501
541
502pWhereblock :: SyntaxInfo -> IParser [PDecl]
542pWhereblock :: SyntaxInfo -> IParser [PDecl]
503pWhereblock syn = do reserved "where"; lchar '{'
543pWhereblock syn = do reserved "where"; lchar '{'