5fbca2a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix with so that clauses are checked for matches against top level defn

commit5fbca2aba2a39b3568dd1c72c50f6f009211d9b8 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 14:44 (15 years ago) parent39b934c

4 files changed+79−20

compare with master

unifiedsplit

src/Core/TT.hs+1−1 src/Idris/AbsSyntax.hs+53−2 src/Idris/ElabDecls.hs+23−16 src/Idris/Parser.hs+2−1

src/Core/TT.hs+1−1

@@ -121,7 +121,7 @@ data Raw = Var Name

121121 | RApp Raw Raw

122122 | RSet Int

123123 | RConstant Const

124− deriving Show

124+ deriving (Show, Eq)

125125

126126data Binder b = Lam { binderTy :: b }

127127 | Pi { binderTy :: b }

src/Idris/AbsSyntax.hs+53−2

@@ -130,7 +130,7 @@ data FixDecl = Fix Fixity String

130130instance Ord FixDecl where

131131 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

132132

133−data Plicity = Imp | Exp deriving Show

133+data Plicity = Imp | Exp deriving (Show, Eq)

134134

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

136136 | PTy FC Name t -- type declaration

@@ -187,14 +187,16 @@ data PTerm = PQuote Raw

187187 | PReturn FC

188188 | PMetavar Name

189189 | PElabError String -- error to report on elaboration

190+ deriving Eq

190191

191192data PDo = DoExp FC PTerm

192193 | DoBind FC Name PTerm

193194 | DoLet FC Name PTerm

195+ deriving Eq

194196

195197data PArg' t = PImp { pname :: Name, getTm :: t }

196198 | PExp { getTm :: t }

197− deriving (Show, Functor)

199+ deriving (Show, Eq, Functor)

198200

199201type PArg = PArg' PTerm

200202

@@ -525,3 +527,52 @@ dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}

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

526528-- dumpDecl (PImport i) = "import " ++ i

527529

530+-- syntactic match of a against b, returning pair of variables in a

531+-- and what they match. Returns 'Nothing' if not a match.

532+

533+matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]

534+matchClause x y = match x y where

535+ matchArg x y = match (getTm x) (getTm y)

536+

537+ match (PApp _ f args) (PApp _ f' args')

538+ | length args == length args'

539+ = do mf <- match f f'

540+ ms <- zipWithM matchArg args args'

541+ return (mf ++ concat ms)

542+ match (PRef _ n) (PRef _ n') | n == n' = return []

543+ | otherwise = Nothing

544+ match (PRef _ n) tm = return [(n, tm)]

545+ match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'

546+ mr <- match r r'

547+ return (ml ++ mr)

548+ match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'

549+ mr <- match r r'

550+ return (ml ++ mr)

551+ match (PTrue _) (PTrue _) = return []

552+ match (PFalse _) (PFalse _) = return []

553+ match (PReturn _) (PReturn _) = return []

554+ match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'

555+ ms <- match s s'

556+ return (mt ++ ms)

557+ match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'

558+ ms <- match s s'

559+ return (mt ++ ms)

560+ match (PHidden x) (PHidden y) = match x y

561+ match a b | a == b = return []

562+ | otherwise = Nothing

563+

564+substMatches :: [(Name, PTerm)] -> PTerm -> PTerm

565+substMatches [] t = t

566+substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)

567+

568+substMatch :: Name -> PTerm -> PTerm -> PTerm

569+substMatch n tm t = sm t where

570+ sm (PRef _ n') | n == n' = tm

571+ sm (PLam x t sc) = PLam x (sm t) (sm sc)

572+ sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

573+ sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

574+ sm (PPair f x y) = PPair f (sm x) (sm y)

575+ sm (PDPair f x y) = PDPair f (sm x) (sm y)

576+ sm (PHidden x) = PHidden (sm x)

577+ sm x = x

578+

src/Idris/ElabDecls.hs+23−16

@@ -179,8 +179,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

179179

180180 -- in the subdecls, lhs becomes:

181181 -- fname pats | wpat [rest]

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

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

182+ -- ==> fname' ps wpat [rest], match pats against toplevel for ps

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

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

185185 mapM_ (elabDecl info) wb

186186

@@ -200,23 +200,30 @@ elabClause info fc (PWith fname lhs withs wval withblock)

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

201201 return (clhs, crhs)

202202 where

203− mkAuxC wname ns (PClauses fc n cs)

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

203+ mkAuxC wname lhs ns (PClauses fc n cs)

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

205205 return $ PClauses fc wname cs'

206206 | 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

207+ mkAuxC wname lhs ns d = return $ d

208+

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

210+ = do logLvl 2 ("Matching " ++ show tm ++ " against " ++ show toplhs)

211+ case matchClause toplhs tm of

212+ Nothing -> fail "with clause does not match top level"

213+ Just mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

214+ lhs <- updateLHS n wname mvars ns tm w

215+ return $ PClause wname lhs ws rhs wheres

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

217+ = do logLvl 2 ("Matching " ++ show tm ++ " against " ++ show toplhs)

218+ case matchClause toplhs tm of

219+ Nothing -> fail "with clause does not match top level"

220+ Just mvars -> do lhs <- updateLHS n wname mvars ns tm w

221+ return $ PWith wname lhs ws wval wheres

215222

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

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

224+ = return $ substMatches mvars $

225+ PApp fc (PRef fc' wname) (map (PExp . (PRef fc')) ns ++ [PExp w])

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

220227

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

222229 pbinds sc

src/Idris/Parser.hs+2−1

@@ -517,7 +517,7 @@ pClause syn

517517 args <- many (pHSimpleExpr syn)

518518 wargs <- many (pWExpr syn)

519519 reserved "with"

520− wval <- pExpr' syn

520+ wval <- pExpr syn

521521 lchar '{'

522522 ds <- many1 $ pFunDecl syn

523523 let withs = concat ds

@@ -542,6 +542,7 @@ pClause syn

542542 r <- pSimpleExpr syn

543543 fc <- pfc

544544 wargs <- many (pWExpr syn)

545+ reserved "with"

545546 wval <- pExpr syn

546547 lchar '{'

547548 ds <- many1 $ pFunDecl syn