c78fb14 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed errors; partially complete default arg subs

c78fb14Timo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+41−40

compare with master

unifiedsplit

@@ -1205,7 +1205,7 @@ addUsingConstraints syn fc t

1205 | otherwise = doAdd cs ns t

1206

1207 mkConst c args = PApp fc (PRef fc c)

1208− (map (\n -> PExp 0 [] (sMN 0 "carg" (PRef fc n)) args)

1208+ (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)

1209

1210 getConstraints (PPi (Constraint _ _) _ c sc)

1211 = getcapp c ++ getConstraints sc

@@ -1232,8 +1232,7 @@ implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1232implicit' info syn ignore n ptm

1233 = do i <- getIState

1234 let (tm', impdata) = implicitise syn ignore i ptm

1235− -- TODO WIP check impdata for unknown vars in default args

1236− defaultArgCheck (eInfoNames info ++ keys (idris_implicits i)) impdata

1235+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1237-- let (tm'', spos) = findStatics i tm'

1236-- let (tm'', spos) = findStatics i tm'

1238 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1237 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1239 addIBC (IBCImp n)

1238 addIBC (IBCImp n)

@@ -1244,21 +1243,20 @@ implicit' info syn ignore n ptm

1244 where

1243 where

1245 -- Detect unknown names in default arguments and throw error if found.

1244 -- Detect unknown names in default arguments and throw error if found.

1246 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1245 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1247− defaultArgCheck names params = foldM_ names params unknownInDefault

1246+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1248−

1247+

1249− unknownInDefault :: [Name] -> PArg -> Idris [Name]

1248+ notFoundInDefault :: [Name] -> PArg -> Idris [Name]

1250− unknownInDefault ns (PTacImplicit _ _ n script _)

1249+ notFoundInDefault kns (PTacImplicit _ _ n script _)

1250+ = do i <- getIState

1251− = case notFound (namesIn script) ns of

1251+ case notFound kns (namesIn [] i script) of

1252− Nothing -> return (n:ns)

1252+ Nothing -> return (n:kns)

1253− Just name -> throwError (NoSuchVariable name)

1253+ Just name -> throwError (NoSuchVariable name)

1254− -- TODO See if PConstraint in addition to PExp can reasonably have

1254+ notFoundInDefault kns p = return ((pname p):kns)

1255− -- a name. Until then, 'pname p' worksn't.

1255+

1256− unknownInDefault ns p = return (pname p):ns

1257−

1258− unknown :: [Name] -> [Name] -> Maybe Name

1256+ notFound :: [Name] -> [Name] -> Maybe Name

1259− unknown [] _ = Nothing

1257+ notFound kns [] = Nothing

1260− unknown (SN (WhereN _ _ _)):as bs = unknown as bs

1258+ notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1261− unknown a:as bs = if elem a bs then unknown as bs else Just a

1259+ notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1262

1260

1263implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1261implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1264implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1262implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

@@ -1525,6 +1523,9 @@ aiFn inpat expat ist fc f ds as

1525 [(n,t)] -> t

1523 [(n,t)] -> t

1526 _ -> Public

1524 _ -> Public

1527

1525

1526+ insertImpl :: [PArg] -> [PArg] -> [PArg]

1527+ insertImpl ps as = insImpAcc M.empty ps as

1528+

1528 -- TODO WIP substitution into default arg expressions.

1529 -- TODO WIP substitution into default arg expressions.

1529 -- - An extra accumulator parameter here?

1530 -- - An extra accumulator parameter here?

1530 -- - Accumulator of what?

1531 -- - Accumulator of what?

@@ -1534,38 +1535,38 @@ aiFn inpat expat ist fc f ds as

1534 -- function?

1535 -- function?

1535 -- - Check for existing call sites of insertImpl.

1536 -- - Check for existing call sites of insertImpl.

1536 -- - Well, easy: this is in a where block :-).

1537 -- - Well, easy: this is in a where block :-).

1537− insertImpl :: M.Map Name PTerm -- accumulated param names & arg terms

1538+ insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1538− -> [PArg] -- parameters

1539+ -> [PArg] -- parameters

1539− -> [PArg] -- arguments

1540+ -> [PArg] -- arguments

1540− -> [PArg]

1541+ -> [PArg]

1541− insertImpl pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1542+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1542− PExp p l n tm : insertImpl (M.insert n tm pnas) ps given

1543+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

1543− insertImpl pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1544+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1544− PConstraint p l n tm : insertImpl (M.insert n tm pnas) ps given

1545+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given

1545− insertImpl pnas (PConstraint p l n ty : ps) given =

1546+ insImpAcc pnas (PConstraint p l n ty : ps) given =

1546 let rtc = PResolveTC fc in

1547 let rtc = PResolveTC fc in

1547− PConstraint p l n rtc : insertImpl (M.insert n rtc pnas) ps given

1548+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given

1548− insertImpl pnas (PImp p _ l n ty : ps) given =

1549+ insImpAcc pnas (PImp p _ l n ty : ps) given =

1549 case find n given [] of

1550 case find n given [] of

1550 Just (tm, given') ->

1551 Just (tm, given') ->

1551− PImp p False l n tm : insertImpl (M.insert n tm pnas) ps given'

1552+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'

1552 Nothing ->

1553 Nothing ->

1553 PImp p True l n Placeholder :

1554 PImp p True l n Placeholder :

1554− insertImpl (M.insert n Placeholder pnas) ps given

1555+ insImpAcc (M.insert n Placeholder pnas) ps given

1555− insertImpl pnas (PTacImplicit p l n sc' ty : ps) given =

1556+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =

1556− let sc = addImpl ist (substMatches (toList pnas) sc') in

1557+ let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1557 case find n given [] of

1558 case find n given [] of

1558 Just (tm, given') ->

1559 Just (tm, given') ->

1559 PTacImplicit p l n sc tm :

1560 PTacImplicit p l n sc tm :

1560− insertImpl (M.insert n tm pnas) ps given'

1561+ insImpAcc (M.insert n tm pnas) ps given'

1561 Nothing ->

1562 Nothing ->

1562 if inpat

1563 if inpat

1563 then PTacImplicit p l n sc Placeholder :

1564 then PTacImplicit p l n sc Placeholder :

1564− insertImpl (M.insert n Placeholder pnas) ps given

1565+ insImpAcc (M.insert n Placeholder pnas) ps given

1565 else PTacImplicit p l n sc sc :

1566 else PTacImplicit p l n sc sc :

1566− insertImpl (M.insert n sc pnas) ps given

1567+ insImpAcc (M.insert n sc pnas) ps given

1567− insertImpl expected [] = []

1568+ insImpAcc _ expected [] = []

1568− insertImpl _ given = given

1569+ insImpAcc _ _ given = given

1569

1570

1570 find n [] acc = Nothing

1571 find n [] acc = Nothing

1571 find n (PImp _ _ _ n' t : gs) acc

1572 find n (PImp _ _ _ n' t : gs) acc

@@ -1602,8 +1603,8 @@ stripLinear i tm = evalState (sl tm) [] where

1602 return $ PApp fc fn args'

1603 return $ PApp fc fn args'

1603 where slA (PImp p m l n t) = do t' <- sl t

1604 where slA (PImp p m l n t) = do t' <- sl t

1604 return $ PImp p m l n t'

1605 return $ PImp p m l n t'

1605− slA (PExp p l n t) = do t' <- sl t

1606+ slA (PExp p l n t) = do t' <- sl t

1606− return $ PExp p l n t'

1607+ return $ PExp p l n t'

1607 slA (PConstraint p l n t)

1608 slA (PConstraint p l n t)

1608 = do t' <- sl t

1609 = do t' <- sl t

1609 return $ PConstraint p l n t'

1610 return $ PConstraint p l n t'

src/Idris/AbsSyntaxTree.hs+16−3

@@ -36,6 +36,19 @@ import Debug.Trace

37import Text.PrettyPrint.Annotated.Leijen

39+-- Data to pass to recursively called elaborators; e.g. for where blocks,

40+-- paramaterised declarations, etc.

41+

42+data ElabInfo = EInfo { params :: [(Name, PTerm)],

43+ inblock :: Ctxt [Name], -- names in the block, and their params

44+ liftname :: Name -> Name,

45+ namespace :: Maybe [String] }

46+

47+toplevel = EInfo [] emptyContext id Nothing

48+

49+eInfoNames :: ElabInfo -> [Name]

50+eInfoNames info = map fst (params info) ++ M.keys (inblock info)

51+

39data IOption = IOption { opt_logLevel :: Int,

52data IOption = IOption { opt_logLevel :: Int,

40 opt_typecase :: Bool,

53 opt_typecase :: Bool,

41 opt_typeintype :: Bool,

54 opt_typeintype :: Bool,

@@ -1507,7 +1520,7 @@ allNamesIn tm = nub $ ni [] tm

1507 ni env _ = []

1520 ni env _ = []

1508

1521

1509 niTacImp env (TacImp _ _ scr) = ni env scr

1522 niTacImp env (TacImp _ _ scr) = ni env scr

1510− niTacImp _ = []

1523+ niTacImp _ _ = []

1511

1524

1512-- Return all names defined in binders in the given term

1525-- Return all names defined in binders in the given term

1513boundNamesIn :: PTerm -> [Name]

1526boundNamesIn :: PTerm -> [Name]

@@ -1593,6 +1606,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1593 ni env (PNoImplicits tm) = ni env tm

1606 ni env (PNoImplicits tm) = ni env tm

1594 ni env _ = []

1607 ni env _ = []

1595

1608

1596− niTacImp (TacImp _ _ scr) = ni scr

1609+ niTacImp env (TacImp _ _ scr) = ni env scr

1597− niTacImp _ = []

1610+ niTacImp _ _ = []

1598

1611

src/Idris/Coverage.hs+3−2

@@ -56,8 +56,9 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59+ (p : _) ->

59− (p : _) -> p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

60+ p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

60− _ -> repeat (pexp Placeholder)

61+ _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63 logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

64 logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

src/Idris/ElabDecls.hs+1−1

@@ -1795,7 +1795,7 @@ elabClass info syn doc fc constraints tn ps ds

1795

1796 getMName (PTy _ _ _ _ _ n _) = nsroot n

1797 tdecl allmeths (PTy doc _ syn _ o n t)

1798− = do t' <- implicit' syn allmeths n t

1798+ = do t' <- implicit' info syn allmeths n t

1799 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1800 return ( (n, (toExp (map fst ps) Exp t')),

1801 (n, (doc, o, (toExp (map fst ps) Imp t'))),

src/Idris/ElabTerm.hs+1−13

@@ -3,6 +3,7 @@

3module Idris.ElabTerm where

5import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

6import Idris.DSL

7import Idris.DSL

7import Idris.Delaborate

8import Idris.Delaborate

8import Idris.Error

9import Idris.Error

@@ -26,19 +27,6 @@ import qualified Data.Text as T

27import Debug.Trace

28import Debug.Trace

29−-- Data to pass to recursively called elaborators; e.g. for where blocks,

30−-- paramaterised declarations, etc.

31−

32−data ElabInfo = EInfo { params :: [(Name, PTerm)],

33− inblock :: Ctxt [Name], -- names in the block, and their params

34− liftname :: Name -> Name,

35− namespace :: Maybe [String] }

36−

37−toplevel = EInfo [] emptyContext id Nothing

38−

39−eInfoNames :: ElabInfo -> [Name]

40−eInfoNames info = map fst (params info) ++ keys (inblock info)

41−

42-- Using the elaborator, convert a term in raw syntax to a fully

30-- Using the elaborator, convert a term in raw syntax to a fully

43-- elaborated, typechecked term.

31-- elaborated, typechecked term.

44--

32--

src/Idris/ParseExpr.hs+19−8

@@ -150,15 +150,23 @@ extension syn (Rule ssym ptm _)

150 update ns (PRef fc n) = case lookup n ns of

151 Just (SynTm t) -> t

152 _ -> PRef fc n

153+ update ns (PLam n ty sc)

153− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

154+ = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

155+ update ns (PPi p n ty sc)

156+ = PPi (updTacImp ns p) (updateB ns n)

154− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)

157+ (update ns ty) (update (dropn n ns) sc)

158+ update ns (PLet n ty val sc)

155− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)

159+ = PLet (updateB ns n) (update ns ty)

156− (update (dropn n ns) sc)

160+ (update ns val) (update (dropn n ns) sc)

161+ update ns (PApp fc t args)

157− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

162+ = PApp fc (update ns t) (map (fmap (update ns)) args)

163+ update ns (PAppBind fc t args)

158− update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)

164+ = PAppBind fc (update ns t) (map (fmap (update ns)) args)

165+ update ns (PCase fc c opts)

159− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

166+ = PCase fc (update ns c) (map (pmap (update ns)) opts)

160 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

167 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

168+ update ns (PDPair fc p l t r)

161− update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)

169+ = PDPair fc p (update ns l) (update ns t) (update ns r)

162 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

170 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

163 update ns (PHidden t) = PHidden (update ns t)

171 update ns (PHidden t) = PHidden (update ns t)

164 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

172 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -176,6 +184,9 @@ extension syn (Rule ssym ptm _)

176 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

184 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

177 update ns t = t

185 update ns t = t

178

186

187+ updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

188+ updTacImp _ x = x

189+

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

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

180@

191@

181InternalExpr ::=

192InternalExpr ::=

src/Idris/Parser.hs+2−2

@@ -18,13 +18,13 @@ import qualified Text.Parser.Token.Highlight as Hi

19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

21−import Idris.AbsSyntax

21+import Idris.AbsSyntax hiding (namespace, params)

22import Idris.DSL

23import Idris.Imports

24import Idris.Delaborate

25import Idris.Error

26import Idris.ElabDecls

27−import Idris.ElabTerm hiding (namespace, params)

27+import Idris.ElabTerm

28import Idris.Coverage

29import Idris.IBC

30import Idris.Unlit