git.iko.soy/Idris-dev
on master help sign in
Parser now fills in implicit arguments
a8768afEdwin Brady
src/Core/TT.hs+1
compare with master
unifiedsplit
@@ -67,6 +67,7 @@ instance Show Name where
67
67
68
68
69-- Contexts allow us to map names to things
69-- Contexts allow us to map names to things
70+-- TODO: Namespaces and ambiguous names
70
71
71type Ctxt a = Map.Map Name a
72type Ctxt a = Map.Map Name a
72emptyContext = Map.empty
73emptyContext = Map.empty
src/Idris/AbsSyntax.hs+71−2
@@ -93,10 +93,79 @@ data PTerm = PQuote Raw
93 | Placeholder
93 | Placeholder
94 deriving Show
94 deriving Show
95
95
96+namesIn :: IState -> PTerm -> [Name]
97+namesIn ist tm = nub $ ni [] tm
98+ where
99+ ni env (PRef n)
100+ | not (n `elem` env)
101+ = case lookupCtxt n (idris_implicits ist) of
102+ Nothing -> [n]
103+ _ -> []
104+ ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
105+ concatMap (ni env) es
106+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
107+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
108+ ni env (PHidden tm) = ni env tm
109+ ni env _ = []
110+
96-- Dealing with implicit arguments
111-- Dealing with implicit arguments
97
112
113+-- Add implicit Pi bindings for any names in the term which appear in an
114+-- argument position.
115+
98implicitise :: IState -> PTerm -> (PTerm, [Name])
116implicitise :: IState -> PTerm -> (PTerm, [Name])
99−implicitise ist tm = (tm, [])
117+implicitise ist tm
118+ = let (declimps, ns) = execState (imps [] tm) ([], []) in
119+ (pibind ns tm, ns ++ reverse declimps)
120+ where
121+ imps env (PApp f is es)
122+ = do (decls, ns) <- get
123+ let isn = concatMap (namesIn ist) (map snd is)
124+ let esn = concatMap (namesIn ist) es
125+ put (decls, nub (ns ++ ((isn ++ esn) \\ env)))
126+ imps env (PPi Imp n ty sc)
127+ = do imps env ty
128+ (decls, ns) <- get
129+ put (n:decls, ns)
130+ imps (n:env) sc
131+ imps env (PPi Exp n ty sc)
132+ = do imps env ty
133+ imps (n:env) sc
134+ imps env (PLam n ty sc)
135+ = do imps env ty
136+ imps (n:env) sc
137+ imps env (PHidden tm) = imps env tm
138+ imps env _ = return ()
139+
140+ pibind [] sc = sc
141+ pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)
100
142
101addImpl :: IState -> PTerm -> PTerm
143addImpl :: IState -> PTerm -> PTerm
102−addImpl ist ptm = ptm
144+addImpl ist ptm = ai [] ptm
145+ where
146+ ai env (PApp f is es) = let f' = ai env f
147+ is' = map (\ (n, tm) -> (n, ai env tm)) is
148+ es' = map (ai env) es in
149+ aiFn env f is' es'
150+ ai env (PLam n ty sc) = let ty' = ai env ty
151+ sc' = ai (n:env) sc in
152+ PLam n ty' sc'
153+ ai env (PPi p n ty sc) = let ty' = ai env ty
154+ sc' = ai (n:env) sc in
155+ PPi p n ty' sc'
156+ ai env (PHidden tm) = PHidden (ai env tm)
157+ ai env tm = tm
158+
159+ aiFn env (PRef f) is es | not (f `elem` env)
160+ = case lookupCtxt f (idris_implicits ist) of
161+ Just ns -> PApp (PRef f) (insertImpl ns is) es
162+ Nothing -> PApp (PRef f) is es
163+ aiFn env f is es = PApp f is es
164+
165+ insertImpl [] given = []
166+ insertImpl (n:ns) given
167+ = case lookup n given of
168+ Just val -> (n, val) : insertImpl ns given
169+ Nothing -> (n, Placeholder) : insertImpl ns given
170+
171+
src/Idris/Parser.hs+11−3
@@ -109,8 +109,14 @@ pHSimpleExpr = try pSimpleExpr
109 return $ PHidden e
109 return $ PHidden e
110
110
111pApp = do f <- pSimpleExpr
111pApp = do f <- pSimpleExpr
112+ iargs <- many pImplicitArg
112 args <- many1 pSimpleExpr
113 args <- many1 pSimpleExpr
113− return (PApp f [] args)
114+ return (PApp f iargs args)
115+
116+pImplicitArg = do lchar '{'; n <- iName
117+ v <- option (PRef n) (do lchar '='; pExpr)
118+ lchar '}'
119+ return (n, v)
114
120
115pTSig = do lchar ':'
121pTSig = do lchar ':'
116 pExpr
122 pExpr
@@ -173,7 +179,8 @@ bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
173pConstructor :: IParser (Name, PTerm)
179pConstructor :: IParser (Name, PTerm)
174pConstructor
180pConstructor
175 = do cn <- pfName; ty <- pTSig
181 = do cn <- pfName; ty <- pTSig
182+ ty' <- implicit cn ty
176− return (cn, ty)
183+ return (cn, ty')
177
184
178pSimpleCon :: IParser (Name, [PTerm])
185pSimpleCon :: IParser (Name, [PTerm])
179pSimpleCon = do cn <- pfName
186pSimpleCon = do cn <- pfName
@@ -184,10 +191,11 @@ pSimpleCon = do cn <- pfName
184
191
185pPattern :: IParser PDecl
192pPattern :: IParser PDecl
186pPattern = try (do n <- pfName
193pPattern = try (do n <- pfName
194+ iargs <- many pImplicitArg
187 args <- many pHSimpleExpr
195 args <- many pHSimpleExpr
188 lchar '='
196 lchar '='
189 rhs <- pExpr
197 rhs <- pExpr
190− return $ PClause (PApp (PRef n) [] args) rhs)
198+ return $ PClause (PApp (PRef n) iargs args) rhs)
191 <|> do l <- pSimpleExpr
199 <|> do l <- pSimpleExpr
192 op <- operator
200 op <- operator
193 r <- pSimpleExpr
201 r <- pSimpleExpr
src/Main.hs+10−1
@@ -42,11 +42,20 @@ runIdris opts =
42loadModule :: FilePath -> Idris ()
42loadModule :: FilePath -> Idris ()
43loadModule f = do iLOG ("Reading " ++ show f)
43loadModule f = do iLOG ("Reading " ++ show f)
44 ds <- parseProg f
44 ds <- parseProg f
45− iLOG (show ds)
45+ iLOG (dumpDecls ds)
46 i <- get
46 i <- get
47 iLOG (show (idris_infixes i))
47 iLOG (show (idris_infixes i))
48 return ()
48 return ()
49
49
50+dumpDecls :: [PDecl] -> String
51+dumpDecls [] = ""
52+dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
53+
54+dumpDecl (PFix f ops) = show f ++ " ==> " ++ show ops
55+dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ show t
56+dumpDecl (PClause l r) = "pat " ++ show l ++ " = " ++ show r
57+dumpDecl (PData d) = "data " ++ show d
58+
50getFile :: Opt -> Maybe String
59getFile :: Opt -> Maybe String
51getFile (Filename str) = Just str
60getFile (Filename str) = Just str
52getFile _ = Nothing
61getFile _ = Nothing