git.iko.soy/Idris-dev
on master help sign in
Added provisional definitions
commit1c492199949b13ca948fb458f32284751d3254af authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 09:20 (15 years ago) parentd496a9c
2 files changed+12−6
compare with master
unifiedsplit
src/Core/Elaborate.hs+2−2 src/Idris/Parser.hs+10−4
src/Core/Elaborate.hs+2−2
@@ -133,8 +133,8 @@ unique_hole n = do ES p _ _ <- get
133133
134134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
135135uniqueNameCtxt ctxt n hs
136− | n `elem` hs = return $ uniqueName (nextName n) hs
137− | Just _ <- lookupCtxt n ctxt = return $ uniqueName (nextName n) hs
136+ | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
137+ | Just _ <- lookupCtxt n ctxt = uniqueNameCtxt ctxt (nextName n) hs
138138 | otherwise = return n
139139
140140elog :: String -> Elab ()
src/Idris/Parser.hs+10−4
@@ -641,6 +641,14 @@ whereSyn n syn args = let ns = concatMap allNamesIn args
641641pArgExpr syn = let syn' = syn { inPattern = True } in
642642 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
643643
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+
644652pClause :: SyntaxInfo -> IParser PClause
645653pClause syn
646654 = try (do n <- pfName
@@ -649,8 +657,7 @@ pClause syn
649657 fc <- pfc
650658 args <- many (pArgExpr syn)
651659 wargs <- many (pWExpr syn)
652− lchar '='
653− rhs <- pExpr syn
660+ rhs <- pRHS syn n
654661 ist <- getState
655662 let ctxt = tt_ctxt ist
656663 let wsyn = whereSyn n syn (map getTm iargs ++
@@ -681,8 +688,7 @@ pClause syn
681688 r <- pArgExpr syn
682689 fc <- pfc
683690 wargs <- many (pWExpr syn)
684− lchar '='
685− rhs <- pExpr syn
691+ rhs <- pRHS syn n
686692 let wsyn = whereSyn n syn []
687693 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
688694 return ([], [])]