git.iko.soy/Idris-dev
on master help sign in
Added provisional definitions
1c49219Edwin Brady
src/Core/Elaborate.hs+2−2
compare with master
unifiedsplit
@@ -133,8 +133,8 @@ unique_hole n = do ES p _ _ <- get
133
133
134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
135uniqueNameCtxt ctxt n hs
135uniqueNameCtxt ctxt n hs
136− | n `elem` hs = return $ uniqueName (nextName n) hs
136+ | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
137− | Just _ <- lookupCtxt n ctxt = return $ uniqueName (nextName n) hs
137+ | Just _ <- lookupCtxt n ctxt = uniqueNameCtxt ctxt (nextName n) hs
138 | otherwise = return n
138 | otherwise = return n
139
139
140elog :: String -> Elab ()
140elog :: String -> Elab ()
src/Idris/Parser.hs+10−4
@@ -641,6 +641,14 @@ whereSyn n syn args = let ns = concatMap allNamesIn args
641pArgExpr syn = let syn' = syn { inPattern = True } in
641pArgExpr syn = let syn' = syn { inPattern = True } in
642 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
642 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
643
643
644+pRHS :: SyntaxInfo -> Name -> IParser PTerm
645+pRHS syn n = do lchar '='; pExpr syn
646+ <|> do symbol "?="; rhs <- pExpr syn;
647+ return (PLet (UN ["value"]) Placeholder rhs (PMetavar n'))
648+ where n' = case n of
649+ UN [x] -> UN [x++"_lemma_1"]
650+ x -> x
651+
644pClause :: SyntaxInfo -> IParser PClause
652pClause :: SyntaxInfo -> IParser PClause
645pClause syn
653pClause syn
646 = try (do n <- pfName
654 = try (do n <- pfName
@@ -649,8 +657,7 @@ pClause syn
649 fc <- pfc
657 fc <- pfc
650 args <- many (pArgExpr syn)
658 args <- many (pArgExpr syn)
651 wargs <- many (pWExpr syn)
659 wargs <- many (pWExpr syn)
652− lchar '='
653− rhs <- pExpr syn
660+ rhs <- pRHS syn n
654 ist <- getState
661 ist <- getState
655 let ctxt = tt_ctxt ist
662 let ctxt = tt_ctxt ist
656 let wsyn = whereSyn n syn (map getTm iargs ++
663 let wsyn = whereSyn n syn (map getTm iargs ++
@@ -681,8 +688,7 @@ pClause syn
681 r <- pArgExpr syn
688 r <- pArgExpr syn
682 fc <- pfc
689 fc <- pfc
683 wargs <- many (pWExpr syn)
690 wargs <- many (pWExpr syn)
684− lchar '='
685− rhs <- pExpr syn
691+ rhs <- pRHS syn n
686 let wsyn = whereSyn n syn []
692 let wsyn = whereSyn n syn []
687 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
693 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
688 return ([], [])]
694 return ([], [])]