c78fb14 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed errors; partially complete default arg subs

commitc78fb14babc88a2fbb7af52edd70cbf2b7784a50 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 4 Apr 2014, 19:57 (13 years ago) parentd3eb486

7 files changed+83−69

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+41−40 src/Idris/AbsSyntaxTree.hs+16−3 src/Idris/Coverage.hs+3−2 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+1−13 src/Idris/ParseExpr.hs+19−8 src/Idris/Parser.hs+2−2

src/Idris/AbsSyntax.hs+41−40

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

12051205 | otherwise = doAdd cs ns t

12061206

12071207 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)

12091209

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

12111211 = getcapp c ++ getConstraints sc

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

12321232implicit' info syn ignore n ptm

12331233 = do i <- getIState

12341234 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

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

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

12391238 addIBC (IBCImp n)

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

12441243 where

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

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

1247− defaultArgCheck names params = foldM_ names params unknownInDefault

1248−

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

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

1251− = case notFound (namesIn script) ns of

1252− Nothing -> return (n:ns)

1253− Just name -> throwError (NoSuchVariable name)

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

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

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

1257−

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

1259− unknown [] _ = Nothing

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

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

1246+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1247+

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

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

1250+ = do i <- getIState

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

1252+ Nothing -> return (n:kns)

1253+ Just name -> throwError (NoSuchVariable name)

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

1255+

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

1257+ notFound kns [] = Nothing

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

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

12621260

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

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

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

15251523 [(n,t)] -> t

15261524 _ -> Public

15271525

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

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

1528+

15281529 -- TODO WIP substitution into default arg expressions.

15291530 -- - An extra accumulator parameter here?

15301531 -- - Accumulator of what?

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

15341535 -- function?

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

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

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

1538− -> [PArg] -- parameters

1539− -> [PArg] -- arguments

1540− -> [PArg]

1541− insertImpl 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− insertImpl 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− insertImpl pnas (PConstraint p l n ty : ps) given =

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

1539+ -> [PArg] -- parameters

1540+ -> [PArg] -- arguments

1541+ -> [PArg]

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

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

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

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

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

15461547 let rtc = PResolveTC fc in

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

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

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

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

15491550 case find n given [] of

15501551 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'

15521553 Nothing ->

15531554 PImp p True l n Placeholder :

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

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

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

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

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

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

15571558 case find n given [] of

15581559 Just (tm, given') ->

15591560 PTacImplicit p l n sc tm :

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

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

15611562 Nothing ->

15621563 if inpat

15631564 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

15651566 else PTacImplicit p l n sc sc :

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

1567− insertImpl expected [] = []

1568− insertImpl _ given = given

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

1568+ insImpAcc _ expected [] = []

1569+ insImpAcc _ _ given = given

15691570

15701571 find n [] acc = Nothing

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

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

16021603 return $ PApp fc fn args'

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

16041605 return $ PImp p m l n t'

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

1606− return $ PExp p l n t'

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

1607+ return $ PExp p l n t'

16071608 slA (PConstraint p l n t)

16081609 = do t' <- sl t

16091610 return $ PConstraint p l n t'

src/Idris/AbsSyntaxTree.hs+16−3

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

3636

3737import Text.PrettyPrint.Annotated.Leijen

3838

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+

3952data IOption = IOption { opt_logLevel :: Int,

4053 opt_typecase :: Bool,

4154 opt_typeintype :: Bool,

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

15071520 ni env _ = []

15081521

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

1510− niTacImp _ = []

1523+ niTacImp _ _ = []

15111524

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

15131526boundNamesIn :: PTerm -> [Name]

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

15931606 ni env (PNoImplicits tm) = ni env tm

15941607 ni env _ = []

15951608

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

1597− niTacImp _ = []

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

1610+ niTacImp _ _ = []

15981611

src/Idris/Coverage.hs+3−2

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

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

5757 -- suggests)

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

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

60− _ -> repeat (pexp Placeholder)

59+ (p : _) ->

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

61+ _ -> repeat (pexp Placeholder)

6162 let tryclauses = mkClauses parg all_args

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

6364 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

17951795

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

17971797 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

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

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

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

src/Idris/ElabTerm.hs+1−13

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

33module Idris.ElabTerm where

55import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

67import Idris.DSL

78import Idris.Delaborate

89import Idris.Error

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

2627

2728import Debug.Trace

2829

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−

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

4331-- elaborated, typechecked term.

4432--

src/Idris/ParseExpr.hs+19−8

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

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

151151 Just (SynTm t) -> t

152152 _ -> PRef fc n

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

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

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

156− (update (dropn n ns) sc)

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

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

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

153+ update ns (PLam n ty 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)

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

158+ update ns (PLet n ty val sc)

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

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

161+ update ns (PApp fc t args)

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

163+ update ns (PAppBind fc t args)

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

165+ update ns (PCase fc c opts)

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

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

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

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

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

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

163171 update ns (PHidden t) = PHidden (update ns t)

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

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

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

177185 update ns t = t

178186

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

188+ updTacImp _ x = x

189+

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

180191@

181192InternalExpr ::=

src/Idris/Parser.hs+2−2

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

1818

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

2020

21−import Idris.AbsSyntax

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

2222import Idris.DSL

2323import Idris.Imports

2424import Idris.Delaborate

2525import Idris.Error

2626import Idris.ElabDecls

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

27+import Idris.ElabTerm

2828import Idris.Coverage

2929import Idris.IBC

3030import Idris.Unlit