9e8a976 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master' into wip/tactical

commit9e8a976383bf660e19b9af03da069b20d574e189 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 22 Aug 2015, 14:49 (11 years ago) parent766b73a 0655d3d

19 files changed+519−223

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+7 src/Idris/AbsSyntaxTree.hs+5 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Coverage.hs+3−3 src/Idris/DeepSeq.hs+1 src/Idris/Elab/Term.hs+8−182 src/Idris/IBC.hs+17−6 src/Idris/Interactive.hs+22−11 src/Idris/ParseExpr.hs+12−6 src/Idris/Parser.hs+137−2 src/Idris/ProofSearch.hs+245−12 test/interactive009/expected+1 test/interactive009/input+1 test/interactive009/interactive009.idr+27 test/interactive009/run+3 test/syntax002/expected+2 test/syntax002/run+4 test/syntax002/syntax002.idr+22

CHANGELOG+1

@@ -29,6 +29,7 @@ New in 0.9.19:

2929* Moved System.Interactive, along with getArgs to the Prelude.

3030* Major improvements to reflected elaboration scripts, including the ability to run

3131 them in a declaration context and many bug fixes.

32+* "decl syntax" rules to allow syntax extensions at the declaration level

3233

3334New in 0.9.18:

3435--------------

idris.cabal+7

@@ -540,6 +540,10 @@ Extra-source-files:

540540 test/interactive008/run

541541 test/interactive008/input

542542 test/interactive008/expected

543+ test/interactive009/run

544+ test/interactive009/input

545+ test/interactive009/*.idr

546+ test/interactive009/expected

543547

544548 test/io001/run

545549 test/io001/*.idr

@@ -655,6 +659,9 @@ Extra-source-files:

655659 test/syntax001/run

656660 test/syntax001/*.idr

657661 test/syntax001/expected

662+ test/syntax002/run

663+ test/syntax002/*.idr

664+ test/syntax002/expected

658665

659666 test/tactics001/run

660667 test/tactics001/*.idr

src/Idris/AbsSyntaxTree.hs+5

@@ -1246,15 +1246,20 @@ deriving instance NFData SynContext

12461246!-}

12471247

12481248data Syntax = Rule [SSymbol] PTerm SynContext

1249+ | DeclRule [SSymbol] [PDecl]

12491250 deriving Show

12501251

12511252syntaxNames :: Syntax -> [Name]

12521253syntaxNames (Rule syms _ _) = mapMaybe ename syms

12531254 where ename (Keyword n) = Just n

12541255 ename _ = Nothing

1256+syntaxNames (DeclRule syms _) = mapMaybe ename syms

1257+ where ename (Keyword n) = Just n

1258+ ename _ = Nothing

12551259

12561260syntaxSymbols :: Syntax -> [SSymbol]

12571261syntaxSymbols (Rule ss _ _) = ss

1262+syntaxSymbols (DeclRule ss _) = ss

12581263{-!

12591264deriving instance Binary Syntax

12601265deriving instance NFData Syntax

src/Idris/Core/Elaborate.hs+1−1

@@ -730,7 +730,7 @@ simple_app infer fun arg str =

730730 s <- getNameFrom (sMN 0 "s")

731731 claim a RType

732732 claim b RType

733− claim f (RBind (sMN 0 "aX") (Pi Nothing (Var a) RType) (Var b))

733+ claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))

734734 tm <- get_term

735735 start_unify s

736736 -- if 'infer' is set, we're assuming it's a simply typed application

src/Idris/Coverage.hs+3−3

@@ -222,7 +222,7 @@ genAll i args

222222 pimp (sUN "B") Placeholder True] ++

223223 [pexp l, pexp r]) o

224224 otherPats o@(PDPair fc hls p t _ v)

225− = ops fc (sUN "Ex_intro")

225+ = ops fc sigmaCon

226226 ([pimp (sUN "a") Placeholder True,

227227 pimp (sUN "P") Placeholder True] ++

228228 [pexp t,pexp v]) o

@@ -243,8 +243,8 @@ genAll i args

243243 getExpTm t = getTm t

244244

245245 -- put it back to its original form

246− resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v])

247− | ei == txt "Ex_intro"

246+ resugar (PApp _ (PRef fc hl n) [_,_,t,v])

247+ | n == sigmaCon

248248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)

249249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])

250250 | n == pairCon

src/Idris/DeepSeq.hs+1

@@ -369,6 +369,7 @@ instance NFData SynContext where

369369

370370instance NFData Syntax where

371371 rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

372+ rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

372373

373374instance NFData SSymbol where

374375 rnf (Keyword x1) = rnf x1 `seq` ()

src/Idris/Elab/Term.hs+8−182

@@ -82,7 +82,7 @@ build ist info emode opts fn tm

8282 mapM_ (\n -> when (n `elem` hs) $

8383 do focus n

8484 g <- goal

85− try (resolveTC True False 10 g fn ist)

85+ try (resolveTC' True False 10 g fn ist)

8686 (movelast n)) ivs

8787 ivs <- get_instances

8888 hs <- get_holes

@@ -91,7 +91,7 @@ build ist info emode opts fn tm

9191 do focus n

9292 g <- goal

9393 ptm <- get_term

94− resolveTC True True 10 g fn ist) ivs

94+ resolveTC' True True 10 g fn ist) ivs

9595 tm <- get_term

9696 ctxt <- get_context

9797 probs <- get_probs

@@ -355,7 +355,7 @@ elab ist info emode opts fn tm

355355 UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

356356 _ -> elab' ina (Just fc) (PRef fc [] unitCon)

357357 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

358− = do g <- goal; resolveTC False False 5 g fn ist

358+ = do g <- goal; resolveTC' False False 5 g fn ist

359359 elab' ina fc (PResolveTC fc')

360360 = do c <- getNameFrom (sMN 0 "class")

361361 instanceArg c

@@ -699,7 +699,7 @@ elab ist info emode opts fn tm

699699 g <- goal

700700 hs <- get_holes

701701 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

702− then try (resolveTC True False 10 g fn ist)

702+ then try (resolveTC' True False 10 g fn ist)

703703 (movelast n)

704704 else movelast n)

705705 (ivs' \\ ivs)

@@ -871,7 +871,7 @@ elab ist info emode opts fn tm

871871 env <- get_env

872872 hs <- get_holes

873873 if all (\n -> not (n `elem` hs)) (freeNames g)

874− then try (resolveTC False False 10 g fn ist)

874+ then try (resolveTC' False False 10 g fn ist)

875875 (movelast n)

876876 else movelast n)

877877 (ivs' \\ ivs)

@@ -1603,20 +1603,6 @@ findHighlight n = do ctxt <- get_context

16031603 Nothing -> lift . tfail . InternalMsg $

16041604 "Can't find name" ++ show n

16051605

1606−-- | Find the names of instances that have been designeated for

1607−-- searching (i.e. non-named instances or instances from Elab scripts)

1608−findInstances :: IState -> Term -> [Name]

1609−findInstances ist t

1610− | (P _ n _, _) <- unApply (getRetTy t)

1611− = case lookupCtxt n (idris_classes ist) of

1612− [CI _ _ _ _ _ ins _] ->

1613− [n | (n, True) <- ins, accessible n]

1614− _ -> []

1615− | otherwise = []

1616− where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1617− Just (_, Hidden) -> False

1618− _ -> True

1619−

16201606-- Try again to solve auto implicits

16211607solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

16221608solveAuto ist fn ambigok n

@@ -1642,168 +1628,8 @@ proofSearch' ist rec ambigok depth prv top n psns hints

16421628 = do unifyProblems

16431629 proofSearch rec prv ambigok (not prv) depth

16441630 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

1645−

1646−-- | Resolve type classes. This will only pick up 'normal' instances, never

1647−-- named instances (which is enforced by 'findInstances').

1648−resolveTC :: Bool -- ^ using default Int

1649− -> Bool -- ^ allow metavariables in the goal

1650− -> Int -- ^ depth

1651− -> Term -- ^ top level goal, for error messages

1652− -> Name -- ^ top level function name, to prevent loops

1653− -> IState -> ElabD ()

1654−resolveTC def mvok depth top fn ist

1655− = do hs <- get_holes

1656− resTC' [] def hs depth top fn ist

1657−

1658−resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1659−resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1660−resTC' tcs defaultOn topholes depth topg fn ist

1661− = do compute

1662− g <- goal

1663− -- Resolution can proceed only if there is something concrete in the

1664− -- determining argument positions. Keep track of the holes in the

1665− -- non-determining position, because it's okay for 'trivial' to solve

1666− -- those holes and no others.

1667− let (argsok, okholePos) = case tcArgsOK g topholes of

1668− Nothing -> (False, [])

1669− Just hs -> (True, hs)

1670− if not argsok -- && not mvok)

1671− then lift $ tfail $ CantResolve True topg

1672− else do

1673− ptm <- get_term

1674− ulog <- getUnifyLog

1675− hs <- get_holes

1676− env <- get_env

1677− t <- goal

1678− let (tc, ttypes) = unApply (getRetTy t)

1679− let okholes = case tc of

1680− P _ n _ -> zip (repeat n) okholePos

1681− _ -> []

1682−

1683− traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1684− try' (trivialHoles' [] okholes ist)

1685− (do addDefault t tc ttypes

1686− let stk = map fst (filter snd $ elab_stack ist)

1687− let insts = findInstances ist t

1688− blunderbuss t depth stk (stk ++ insts)) True

1689− where

1690− -- returns Just hs if okay, where hs are holes which are okay in the

1691− -- goal, or Nothing if not okay to proceed

1692− tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

1693− = Just []

1694− tcArgsOK ty hs -- if any determining arguments are metavariables, postpone

1695− = let (f, as) = unApply (getRetTy ty) in

1696− case f of

1697− P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1698− Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1699− Nothing -> if any (isMeta hs) as

1700− then Nothing

1701− else Just []

1702− _ -> if any (isMeta hs) as

1703− then Nothing

1704− else Just []

1705−

1706− -- return the list of argument positions which can safely be a hole

1707− -- or Nothing if one of the determining arguments is a hole

1708− tcDetArgsOK i ds hs (x : xs)

1709− | i `elem` ds = if isMeta hs x

1710− then Nothing

1711− else tcDetArgsOK (i + 1) ds hs xs

1712− | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs

1713− case x of

1714− P _ n _ -> Just (i : rs)

1715− _ -> Just rs

1716− tcDetArgsOK _ _ _ [] = Just []

1717−

1718− isMeta :: [Name] -> Term -> Bool

1719− isMeta ns (P _ n _) = n `elem` ns

1720− isMeta _ _ = False

1721−

1722− notHole hs (P _ n _, c)

1723− | (P _ cn _, _) <- unApply (getRetTy c),

1724− n `elem` hs && isConName cn (tt_ctxt ist) = False

1725− | Constant _ <- c = not (n `elem` hs)

1726− notHole _ _ = True

1727−

1728− -- HACK! Rather than giving a special name, better to have some kind

1729− -- of flag in ClassInfo structure

1730− chaser (UN nm)

1731− | ('@':'@':_) <- str nm = True -- old way

1732− chaser (SN (ParentN _ _)) = True

1733− chaser (NS n _) = chaser n

1734− chaser _ = False

1735−

1736− numclass = sNS (sUN "Num") ["Classes","Prelude"]

1737−

1738− addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

1739− = do focus a

1740− fill (RConstant (AType (ATInt ITBig))) -- default Integer

1741− solve

1742− addDefault t f as

1743− | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t

1744− addDefault t f a = return () -- trace (show t) $ return ()

1745−

1746− boundVar (P Bound _ _) = True

1747− boundVar _ = False

1748−

1749− blunderbuss t d stk [] = do -- c <- get_env

1750− -- ps <- get_probs

1751− lift $ tfail $ CantResolve False topg

1752− blunderbuss t d stk (n:ns)

1753− | n /= fn -- && (n `elem` stk)

1754− = tryCatch (resolve n d)

1755− (\e -> case e of

1756− CantResolve True _ -> lift $ tfail e

1757− _ -> blunderbuss t d stk ns)

1758− | otherwise = blunderbuss t d stk ns

1759−

1760− introImps = do g <- goal

1761− case g of

1762− (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

1763− num <- introImps

1764− return (num + 1)

1765− _ -> return 0

1766−

1767− solven 0 = return ()

1768− solven n = do solve; solven (n - 1)

1769−

1770− resolve n depth

1771− | depth == 0 = fail $ "Can't resolve type class"

1772− | otherwise

1773− = do lams <- introImps

1774− t <- goal

1775− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

1776−-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

1777−-- else do

1778− -- if there's a hole in the goal, don't even try

1779− let imps = case lookupCtxtName n (idris_implicits ist) of

1780− [] -> []

1781− [args] -> map isImp (snd args) -- won't be overloaded!

1782− xs -> error "The impossible happened - overloading is not expected here!"

1783− ps <- get_probs

1784− tm <- get_term

1785− args <- map snd <$> try' (apply (Var n) imps)

1786− (match_apply (Var n) imps) True

1787− solven lams -- close any implicit lambdas we introduced

1788− ps' <- get_probs

1789− when (length ps < length ps' || unrecoverable ps') $

1790− fail "Can't apply type class"

1791−-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1792− mapM_ (\ (_,n) -> do focus n

1793− t' <- goal

1794− let (tc', ttype) = unApply (getRetTy t')

1795− let got = fst (unApply (getRetTy t))

1796− let depth' = if tc' `elem` tcs

1797− then depth - 1 else depth

1798− resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

1799− (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1800− -- if there's any arguments left, we've failed to resolve

1801− hs <- get_holes

1802− ulog <- getUnifyLog

1803− solve

1804− traceWhen ulog ("Got " ++ show n) $ return ()

1805− where isImp (PImp p _ _ _ _) = (True, p)

1806− isImp arg = (False, priority arg)

1631+resolveTC' di mv depth tm n ist

1632+ = resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

18071633

18081634collectDeferred :: Maybe Name -> [Name] -> Context ->

18091635 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

@@ -2131,7 +1957,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

21311957 | n == tacN "prim__ResolveTC", [fn] <- args

21321958 = do g <- goal

21331959 fn <- reifyTTName fn

2134− resolveTC False True 100 g fn ist

1960+ resolveTC' False True 100 g fn ist

21351961 returnUnit

21361962 | n == tacN "prim__Search", [depth, hints] <- args

21371963 = do d <- eval depth

src/Idris/IBC.hs+17−6

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 117

43+ibcVersion = 118

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -2174,14 +2174,25 @@ instance Binary SynContext where

21742174

21752175instance Binary Syntax where

21762176 put (Rule x1 x2 x3)

2177− = do put x1

2177+ = do putWord8 0

2178+ put x1

21782179 put x2

21792180 put x3

2181+ put (DeclRule x1 x2)

2182+ = do putWord8 1

2183+ put x1

2184+ put x2

21802185 get

2181− = do x1 <- get

2182− x2 <- get

2183− x3 <- get

2184− return (Rule x1 x2 x3)

2186+ = do i <- getWord8

2187+ case i of

2188+ 0 -> do x1 <- get

2189+ x2 <- get

2190+ x3 <- get

2191+ return (Rule x1 x2 x3)

2192+ 1 -> do x1 <- get

2193+ x2 <- get

2194+ return (DeclRule x1 x2)

2195+ _ -> error "Corrupted binary data for Syntax"

21852196

21862197instance (Binary t) => Binary (DSL' t) where

21872198 put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

src/Idris/Interactive.hs+22−11

@@ -292,12 +292,12 @@ makeLemma fn updatefile l n

292292 let isProv = checkProv tyline (show n)

293293

294294 ctxt <- getContext

295− mty <- case lookupTyName n ctxt of

296− [(_,t)] -> return t

297− [] -> ierror (NoSuchVariable n)

298− ns -> ierror (CantResolveAlts (map fst ns))

295+ (fname, mty) <- case lookupTyName n ctxt of

296+ [t] -> return t

297+ [] -> ierror (NoSuchVariable n)

298+ ns -> ierror (CantResolveAlts (map fst ns))

299299 i <- getIState

300− margs <- case lookup n (idris_metavars i) of

300+ margs <- case lookup fname (idris_metavars i) of

301301 Just (_, arity, _, _) -> return arity

302302 _ -> return (-1)

303303

@@ -308,7 +308,7 @@ makeLemma fn updatefile l n

308308 let lem = show n ++ " : " ++

309309 constraints i classes mty ++

310310 showTmOpts (defaultPPOption { ppopt_pinames = True })

311− (stripMNBind skip (delab i mty))

311+ (stripMNBind skip margs (delab i mty))

312312 let lem_app = show n ++ appArgs skip margs mty

313313

314314 if updatefile then

@@ -351,12 +351,13 @@ makeLemma fn updatefile l n

351351 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

352352 appArgs skip i _ = ""

353353

354− stripMNBind skip (PPi b n@(UN c) _ ty sc)

355− | (thead c /= '_' && n `notElem` skip) ||

354+ stripMNBind _ args t | args <= 0 = t

355+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)

356+ | n `notElem` skip ||

356357 take 4 (str c) == "__pi" -- keep in type, but not in app

357− = PPi b n NoFC ty (stripMNBind skip sc)

358− stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

359− stripMNBind skip t = t

358+ = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)

359+ stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc

360+ stripMNBind skip args t = t

360361

361362 constraints :: IState -> [Name] -> Type -> String

362363 constraints i [] ty = ""

@@ -374,13 +375,23 @@ makeLemma fn updatefile l n

374375 -- or at the top level themselves.

375376 -- Also, make type class instances implicit

376377 guessImps :: IState -> Context -> Term -> [Name]

378+ -- machine names aren't lifted

379+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

380+ = n : guessImps ist ctxt sc

377381 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

378382 | guarded ctxt n (substV (P Bound n Erased) sc)

379383 = n : guessImps ist ctxt sc

380384 | isClass ist ty

381385 = n : guessImps ist ctxt sc

386+ | TType _ <- ty = n : guessImps ist ctxt sc

387+ | ignoreName n = n : guessImps ist ctxt sc

382388 | otherwise = guessImps ist ctxt sc

383389 guessImps ist ctxt _ = []

390+

391+ -- TMP HACK unusable name so don't lift

392+ ignoreName n = case show n of

393+ "_aX" -> True

394+ _ -> False

384395

385396 guessClasses :: IState -> Context -> Term -> [Name]

386397 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)

src/Idris/ParseExpr.hs+12−6

@@ -128,8 +128,10 @@ extensions syn rules = extension syn [] (filter isValid rules)

128128 isValid (Rule _ _ AnySyntax) = True

129129 isValid (Rule _ _ PatternSyntax) = inPattern syn

130130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

131+ isValid (DeclRule _ _) = False

131132

132133data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

134+ deriving Show

133135

134136extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

135137extension syn ns rules =

@@ -140,7 +142,7 @@ extension syn ns rules =

140142 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

141143 -- If we have more than one Rule in this bucket, our grammar is

142144 -- nondeterministic.

143− Rule [] ptm _ -> return (flatten (update (mapMaybe id ns) ptm))

145+ Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))

144146 where

145147 ruleGroup [] [] = True

146148 ruleGroup (s1:_) (s2:_) = s1 == s2

@@ -159,15 +161,13 @@ extension syn ns rules =

159161 extensionSymbol (Symbol s) = do fc <- symbolFC s

160162 highlightP fc AnnKeyword

161163 return Nothing

162− dropn :: Name -> [(Name, a)] -> [(Name, a)]

163− dropn n [] = []

164− dropn n ((x,t) : xs) | n == x = xs

165− | otherwise = (x,t):dropn n xs

166−

164+

167165 flatten :: PTerm -> PTerm -- flatten application

168166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

169167 flatten t = t

170168

169+updateSynMatch = update

170+ where

171171 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)

172172 updateB ns (n, fc) = case lookup n ns of

173173 Just (SynBind tfc t) -> (t, tfc)

@@ -251,6 +251,12 @@ extension syn ns rules =

251251

252252 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

253253 updTacImp _ x = x

254+

255+ dropn :: Name -> [(Name, a)] -> [(Name, a)]

256+ dropn n [] = []

257+ dropn n ((x,t) : xs) | n == x = xs

258+ | otherwise = (x,t):dropn n xs

259+

254260

255261{- | Parses a (normal) built-in expression

256262@

src/Idris/Parser.hs+137−2

@@ -184,7 +184,13 @@ Decl ::=

184184@

185185-}

186186decl :: SyntaxInfo -> IdrisParser [PDecl]

187−decl syn = do fc <- getFC

187+decl syn = try (externalDecl syn)

188+ <|> internalDecl syn

189+ <?> "declaration"

190+

191+internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192+internalDecl syn

193+ = do fc <- getFC

188194 -- if we're after maxline, stop here

189195 let continue = case maxline syn of

190196 Nothing -> True

@@ -235,6 +241,124 @@ decl' syn = fixity

235241 <|> runElabDecl syn

236242 <?> "declaration"

237243

244+externalDecl :: SyntaxInfo -> IdrisParser [PDecl]

245+externalDecl syn = do i <- get

246+ notEndBlock

247+ FC fn start _ <- getFC

248+ decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)

249+ FC _ _ end <- getFC

250+ let outerFC = FC fn start end

251+ return decls

252+

253+declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]

254+declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

255+ <?> "user-defined declaration"

256+ where

257+ isDeclRule (DeclRule _ _) = True

258+ isDeclRule _ = False

259+

260+declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

261+ -> IdrisParser [PDecl]

262+declExtension syn ns rules =

263+ choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

264+ case head rs of -- can never be []

265+ DeclRule (symb:_) _ -> try $ do

266+ n <- extSymbol symb

267+ declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

268+ -- If we have more than one Rule in this bucket, our grammar is

269+ -- nondeterministic.

270+ DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in

271+ return r

272+

273+ where

274+ update :: [(Name, SynMatch)] -> PDecl -> PDecl

275+ update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)

276+

277+ updateRefs ns = mapPT newref

278+ where

279+ newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)

280+ newref t = t

281+

282+ -- Below is a lot of tedious boilerplate which updates any top level

283+ -- names in the declaration. It will only change names which are bound in

284+ -- the declaration (including method names in classes and field names in

285+ -- record declarations, not including pattern variables)

286+ updateB :: [(Name, SynMatch)] -> Name -> Name

287+ updateB ns (NS n mods) = NS (updateB ns n) mods

288+ updateB ns n = case lookup n ns of

289+ Just (SynBind tfc t) -> t

290+ _ -> n

291+

292+ updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl

293+ updateNs ns (PTy doc argdoc s fc o n fc' t)

294+ = PTy doc argdoc s fc o (updateB ns n) fc' t

295+ updateNs ns (PClauses fc o n cs)

296+ = PClauses fc o (updateB ns n) (map (updateClause ns) cs)

297+ updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t

298+ updateNs ns (PData ds cds s fc o dat)

299+ = PData ds cds s fc o (updateData ns dat)

300+ updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)

301+ updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)

302+ updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)

303+ = PRecord doc syn fc o (updateB ns n) fc' ps pdocs

304+ (map (updateField ns) fields)

305+ (updateRecCon ns cname)

306+ cdoc

307+ s

308+ updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

309+ = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets

310+ (map (updateNs ns) ds)

311+ (updateRecCon ns cname)

312+ cdocs

313+ updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)

314+ = PInstance docs pdocs s fc cs (updateB ns cn) fc'

315+ ps ity (fmap (updateB ns) ni)

316+ (map (updateNs ns) ds)

317+ updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

318+ updateNs ns (PProvider docs s fc fc' pw n)

319+ = PProvider docs s fc fc' pw (updateB ns n)

320+ updateNs ns d = d

321+

322+ updateRecCon ns Nothing = Nothing

323+ updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)

324+

325+ updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)

326+

327+ updateClause ns (PClause fc n t ts t' ds)

328+ = PClause fc (updateB ns n) t ts t' (map (update ns) ds)

329+ updateClause ns (PWith fc n t ts t' m ds)

330+ = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)

331+ updateClause ns (PClauseR fc ts t ds)

332+ = PClauseR fc ts t (map (update ns) ds)

333+ updateClause ns (PWithR fc ts t m ds)

334+ = PWithR fc ts t m (map (update ns) ds)

335+

336+ updateData ns (PDatadecl n fc t cs)

337+ = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)

338+ updateData ns (PLaterdecl n fc t)

339+ = PLaterdecl (updateB ns n) fc t

340+

341+ updateCon ns (cd, ads, cn, fc, ty, fc', fns)

342+ = (cd, ads, updateB ns cn, fc, ty, fc', fns)

343+

344+ ruleGroup [] [] = True

345+ ruleGroup (s1:_) (s2:_) = s1 == s2

346+ ruleGroup _ _ = False

347+

348+ extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

349+ extSymbol (Keyword n) = do fc <- reservedFC (show n)

350+ highlightP fc AnnKeyword

351+ return Nothing

352+ extSymbol (Expr n) = do tm <- expr syn

353+ return $ Just (n, SynTm tm)

354+ extSymbol (SimpleExpr n) = do tm <- simpleExpr syn

355+ return $ Just (n, SynTm tm)

356+ extSymbol (Binding n) = do (b, fc) <- name

357+ return $ Just (n, SynBind fc b)

358+ extSymbol (Symbol s) = do fc <- symbolFC s

359+ highlightP fc AnnKeyword

360+ return Nothing

361+

238362{- | Parses a syntax extension declaration (and adds the rule to parser state)

239363

240364@

@@ -303,6 +427,17 @@ syntaxRule syn

303427 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

304428 terminator

305429 return (Rule (mkSimple syms) tm sty)

430+ <|> do reservedHL "decl"; reservedHL "syntax"

431+ syms <- some syntaxSym

432+ when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

433+ let ns = mapMaybe getName syms

434+ when (length ns /= length (nub ns))

435+ $ unexpected "repeated variable in syntax rule"

436+ lchar '='

437+ openBlock

438+ dec <- some (decl syn)

439+ closeBlock

440+ return (DeclRule (mkSimple syms) (concat dec))

306441 where

307442 isExpr (Expr _) = True

308443 isExpr _ = False

@@ -317,7 +452,7 @@ syntaxRule syn

317452 mkSimple es

318453 -- Can't parse a full expression followed by operator like characters due to ambiguity

319454 mkSimple' (Expr e : Symbol s : es)

320− | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

455+ | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es

321456 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

322457 mkSimple' (e : es) = e : mkSimple' es

323458 mkSimple' [] = []

src/Idris/ProofSearch.hs+245−12

@@ -1,9 +1,10 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.ProofSearch(trivial, trivialHoles, proofSearch) where

3+module Idris.ProofSearch(trivial, trivialHoles, proofSearch, resolveTC) where

55import Idris.Core.Elaborate hiding (Tactic(..))

66import Idris.Core.TT

7+import Idris.Core.Unify

78import Idris.Core.Evaluate

89import Idris.Core.CaseTree

910import Idris.Core.Typecheck

@@ -24,14 +25,16 @@ import Debug.Trace

2425trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

2526trivial = trivialHoles [] []

2627

27−trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28+trivialHoles :: [Name] -> -- user visible names, when working

29+ -- in interactive mode

30+ [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

2831trivialHoles psnames ok elab ist

29− = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

30− return ())

31− (do env <- get_env

32− g <- goal

33− tryAll env

34− return ()) True

32+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

33+ return ())

34+ (do env <- get_env

35+ g <- goal

36+ tryAll env

37+ return ()) True

3538 where

3639 tryAll [] = fail "No trivial solution"

3740 tryAll ((x, b):xs)

@@ -41,7 +44,7 @@ trivialHoles psnames ok elab ist

4144 g <- goal

4245 -- anywhere but the top is okay for a hole, if holesOK set

4346 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

44− holesOK hs (binderTy b) && (null psnames || x `elem` psnames)

47+ (holesOK hs (binderTy b) && (null psnames || x `elem` psnames))

4548 then try' (elab (PRef (fileFC "prf") [] x))

4649 (tryAll xs) True

4750 else tryAll xs

@@ -60,6 +63,50 @@ trivialHoles psnames ok elab ist

6063 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as

6164 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as

6265

66+trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

67+trivialTCs ok elab ist

68+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

69+ return ())

70+ (do env <- get_env

71+ g <- goal

72+ tryAll env

73+ return ()) True

74+ where

75+ tryAll [] = fail "No trivial solution"

76+ tryAll ((x, b):xs)

77+ = do -- if type of x has any holes in it, move on

78+ hs <- get_holes

79+ let badhs = hs -- filter (flip notElem holesOK) hs

80+ g <- goal

81+ env <- get_env

82+ -- anywhere but the top is okay for a hole, if holesOK set

83+ if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

84+ (holesOK hs (binderTy b) && tcArg env (binderTy b))

85+ then try' (elab (PRef (fileFC "prf") [] x))

86+ (tryAll xs) True

87+ else tryAll xs

88+

89+ tcArg env ty

90+ | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))

91+ = case lookupCtxtExact n (idris_classes ist) of

92+ Just _ -> True

93+ _ -> False

94+ | otherwise = False

95+

96+ holesOK hs ap@(App _ _ _)

97+ | (P _ n _, args) <- unApply ap

98+ = holeArgsOK hs n 0 args

99+ holesOK hs (App _ f a) = holesOK hs f && holesOK hs a

100+ holesOK hs (P _ n _) = not (n `elem` hs)

101+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&

102+ holesOK hs sc

103+ holesOK hs _ = True

104+

105+ holeArgsOK hs n p [] = True

106+ holeArgsOK hs n p (a : as)

107+ | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as

108+ | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as

109+

63110cantSolveGoal :: ElabD a

64111cantSolveGoal = do g <- goal

65112 env <- get_env

@@ -179,7 +226,9 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

179226 ty <- goal

180227 when (S.member ty tys) $ fail "Been here before"

181228 let tys' = S.insert ty tys

182− try' (trivialHoles psnames [] elab ist)

229+ try' (try' (trivialHoles psnames [] elab ist)

230+ (resolveTC False False 20 ty nroot elab ist)

231+ True)

183232 (try' (try' (resolveByCon (d - 1) locs tys')

184233 (resolveByLocals (d - 1) locs tys')

185234 True)

@@ -188,9 +237,14 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

188237 then fail "cantSolveGoal"

189238 else do attack; defer [] nroot; solve) True) True

190239

191− getFn d Nothing = []

192− getFn d (Just f) | d < maxDepth-1 = [f]

240+ -- get recursive function name. Only user given names make sense.

241+ getFn d (Just f) | d < maxDepth-1 && usersname f = [f]

193242 | otherwise = []

243+ getFn d _ = []

244+

245+ usersname (UN _) = True

246+ usersname (NS n _) = usersname n

247+ usersname _ = False

194248

195249 resolveByCon d locs tys

196250 = do t <- goal

@@ -273,3 +327,182 @@ checkConstructor ist (n : ns) =

273327 any conHead args

274328 conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)

275329 | otherwise = False

330+

331+-- | Resolve type classes. This will only pick up 'normal' instances, never

332+-- named instances (which is enforced by 'findInstances').

333+resolveTC :: Bool -- ^ using default Int

334+ -> Bool -- ^ allow metavariables in the goal

335+ -> Int -- ^ depth

336+ -> Term -- ^ top level goal, for error messages

337+ -> Name -- ^ top level function name, to prevent loops

338+ -> (PTerm -> ElabD ()) -- ^ top level elaborator

339+ -> IState -> ElabD ()

340+resolveTC def mvok depth top fn elab ist

341+ = do hs <- get_holes

342+ resTC' [] def hs depth top fn elab ist

343+

344+resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve type class"

345+resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

346+resTC' tcs defaultOn topholes depth topg fn elab ist

347+ = do compute

348+ g <- goal

349+ -- Resolution can proceed only if there is something concrete in the

350+ -- determining argument positions. Keep track of the holes in the

351+ -- non-determining position, because it's okay for 'trivial' to solve

352+ -- those holes and no others.

353+ let (argsok, okholePos) = case tcArgsOK g topholes of

354+ Nothing -> (False, [])

355+ Just hs -> (True, hs)

356+ if not argsok -- && not mvok)

357+ then lift $ tfail $ CantResolve True topg

358+ else do

359+ ptm <- get_term

360+ ulog <- getUnifyLog

361+ hs <- get_holes

362+ env <- get_env

363+ t <- goal

364+ let (tc, ttypes) = unApply (getRetTy t)

365+ let okholes = case tc of

366+ P _ n _ -> zip (repeat n) okholePos

367+ _ -> []

368+

369+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

370+ try' (trivialTCs okholes elab ist)

371+ (do addDefault t tc ttypes

372+ let stk = map fst (filter snd $ elab_stack ist)

373+ let insts = findInstances ist t

374+ blunderbuss t depth stk (stk ++ insts)) True

375+ where

376+ -- returns Just hs if okay, where hs are holes which are okay in the

377+ -- goal, or Nothing if not okay to proceed

378+ tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

379+ = Just []

380+ tcArgsOK ty hs -- if any determining arguments are metavariables, postpone

381+ = let (f, as) = unApply (getRetTy ty) in

382+ case f of

383+ P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

384+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

385+ Nothing -> if any (isMeta hs) as

386+ then Nothing

387+ else Just []

388+ _ -> if any (isMeta hs) as

389+ then Nothing

390+ else Just []

391+

392+ -- return the list of argument positions which can safely be a hole

393+ -- or Nothing if one of the determining arguments is a hole

394+ tcDetArgsOK i ds hs (x : xs)

395+ | i `elem` ds = if isMeta hs x

396+ then Nothing

397+ else tcDetArgsOK (i + 1) ds hs xs

398+ | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs

399+ case x of

400+ P _ n _ -> Just (i : rs)

401+ _ -> Just rs

402+ tcDetArgsOK _ _ _ [] = Just []

403+

404+ isMeta :: [Name] -> Term -> Bool

405+ isMeta ns (P _ n _) = n `elem` ns

406+ isMeta _ _ = False

407+

408+ notHole hs (P _ n _, c)

409+ | (P _ cn _, _) <- unApply (getRetTy c),

410+ n `elem` hs && isConName cn (tt_ctxt ist) = False

411+ | Constant _ <- c = not (n `elem` hs)

412+ notHole _ _ = True

413+

414+ -- HACK! Rather than giving a special name, better to have some kind

415+ -- of flag in ClassInfo structure

416+ chaser (UN nm)

417+ | ('@':'@':_) <- str nm = True -- old way

418+ chaser (SN (ParentN _ _)) = True

419+ chaser (NS n _) = chaser n

420+ chaser _ = False

421+

422+ numclass = sNS (sUN "Num") ["Classes","Prelude"]

423+

424+ addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

425+ = do focus a

426+ fill (RConstant (AType (ATInt ITBig))) -- default Integer

427+ solve

428+ addDefault t f as

429+ | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t

430+ addDefault t f a = return () -- trace (show t) $ return ()

431+

432+ boundVar (P Bound _ _) = True

433+ boundVar _ = False

434+

435+ blunderbuss t d stk [] = do -- c <- get_env

436+ -- ps <- get_probs

437+ lift $ tfail $ CantResolve False topg

438+ blunderbuss t d stk (n:ns)

439+ | n /= fn -- && (n `elem` stk)

440+ = tryCatch (resolve n d)

441+ (\e -> case e of

442+ CantResolve True _ -> lift $ tfail e

443+ _ -> blunderbuss t d stk ns)

444+ | otherwise = blunderbuss t d stk ns

445+

446+ introImps = do g <- goal

447+ case g of

448+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

449+ num <- introImps

450+ return (num + 1)

451+ _ -> return 0

452+

453+ solven 0 = return ()

454+ solven n = do solve; solven (n - 1)

455+

456+ resolve n depth

457+ | depth == 0 = fail $ "Can't resolve type class"

458+ | otherwise

459+ = do lams <- introImps

460+ t <- goal

461+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

462+-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

463+-- else do

464+ -- if there's a hole in the goal, don't even try

465+ let imps = case lookupCtxtName n (idris_implicits ist) of

466+ [] -> []

467+ [args] -> map isImp (snd args) -- won't be overloaded!

468+ xs -> error "The impossible happened - overloading is not expected here!"

469+ ps <- get_probs

470+ tm <- get_term

471+ args <- map snd <$> try' (apply (Var n) imps)

472+ (match_apply (Var n) imps) True

473+ solven lams -- close any implicit lambdas we introduced

474+ ps' <- get_probs

475+ when (length ps < length ps' || unrecoverable ps') $

476+ fail "Can't apply type class"

477+-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

478+ mapM_ (\ (_,n) -> do focus n

479+ t' <- goal

480+ let (tc', ttype) = unApply (getRetTy t')

481+ let got = fst (unApply (getRetTy t))

482+ let depth' = if tc' `elem` tcs

483+ then depth - 1 else depth

484+ resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)

485+ (filter (\ (x, y) -> not x) (zip (map fst imps) args))

486+ -- if there's any arguments left, we've failed to resolve

487+ hs <- get_holes

488+ ulog <- getUnifyLog

489+ solve

490+ traceWhen ulog ("Got " ++ show n) $ return ()

491+ where isImp (PImp p _ _ _ _) = (True, p)

492+ isImp arg = (False, priority arg)

493+

494+-- | Find the names of instances that have been designeated for

495+-- searching (i.e. non-named instances or instances from Elab scripts)

496+findInstances :: IState -> Term -> [Name]

497+findInstances ist t

498+ | (P _ n _, _) <- unApply (getRetTy t)

499+ = case lookupCtxt n (idris_classes ist) of

500+ [CI _ _ _ _ _ ins _] ->

501+ [n | (n, True) <- ins, accessible n]

502+ _ -> []

503+ | otherwise = []

504+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

505+ Just (_, Hidden) -> False

506+ _ -> True

507+

508+

test/interactive009/expectednew file+1

@@ -0,0 +1 @@

1+IsSetCons pf prfRec

test/interactive009/inputnew file+1

@@ -0,0 +1 @@

1+:ps 26 rec

test/interactive009/interactive009.idrnew file+27

@@ -0,0 +1,27 @@

1+import Data.Vect

3+%default total

5+data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where

6+ ElemBoolNil : Eq t => ElemBool {t=t} a [] False

7+ ElemBoolCons : Eq t => ElemBool {t=t} x1 xs b -> ElemBool x1 (x2 :: xs) ((x1 == x2) || b)

9+data IsSet : Eq t => Vect n t -> Type where

10+ IsSetNil : Eq t => IsSet {t=t} []

11+ IsSetCons : Eq t => ElemBool {t=t} x xs False -> IsSet xs -> IsSet (x :: xs)

12+

13+fun_1 : Eq t => (x : t) -> (xs : Vect n t) -> (b : Bool ** ElemBool x xs b)

14+fun_1 x [] = (False ** ElemBoolNil)

15+fun_1 x1 (x2 :: xs) =

16+ let (b ** prfRec) = fun_1 x1 xs

17+ in (((x1 == x2) || b) ** (ElemBoolCons prfRec))

18+

19+fun_2 : Eq t => (xs : Vect n t) -> Maybe (IsSet xs)

20+fun_2 [] = Just IsSetNil

21+fun_2 (x :: xs) with (fun_1 x xs)

22+ fun_2 (x :: xs) | (True ** pf) = Nothing

23+ fun_2 (x :: xs) | (False ** pf) with (fun_2 xs)

24+ fun_2 (x :: xs) | (False ** pf) | Nothing = Nothing

25+ fun_2 (x :: xs) | (False ** pf) | (Just prfRec)

26+ = Just ?rec

27+

test/interactive009/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive009.idr < input

3+rm -f *.ibc

test/syntax002/expectednew file+2

@@ -0,0 +1,2 @@

1+Nothing

2+7

test/syntax002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ syntax002.idr -o syntax002

3+./syntax002

4+rm -f syntax002 *.ibc

test/syntax002/syntax002.idrnew file+22

@@ -0,0 +1,22 @@

2+decl syntax fun {n} ":" [ty] "=" [def]

3+ = n : ty

4+ n = def

6+decl syntax newtype {tname} "=" {conname} [tysyn]

7+ = data tname = conname tysyn

9+decl syntax EmptyShow {n} =

10+ instance Show n where

11+ show x = "Nothing"

12+

13+fun add : (Int -> Int -> Int) = \x, y => x + y

14+

15+newtype Foo = MkFoo Int

16+

17+EmptyShow Foo

18+

19+main : IO ()

20+main = do printLn (MkFoo 42)

21+ printLn (add 3 4)

22+