git.iko.soy/Idris-dev
on master help sign in
Parser now fills in implicit arguments
commita8768af71ec3bd8548c2fb8cb156c0335609a88e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 6 Oct 2011, 23:28 (15 years ago) parent596e9aa
4 files changed+93−6
compare with master
unifiedsplit
src/Core/TT.hs+1 src/Idris/AbsSyntax.hs+71−2 src/Idris/Parser.hs+11−3 src/Main.hs+10−1
src/Core/TT.hs+1
@@ -67,6 +67,7 @@ instance Show Name where
6767
6868
6969-- Contexts allow us to map names to things
70+-- TODO: Namespaces and ambiguous names
7071
7172type Ctxt a = Map.Map Name a
7273emptyContext = Map.empty
src/Idris/AbsSyntax.hs+71−2
@@ -93,10 +93,79 @@ data PTerm = PQuote Raw
9393 | Placeholder
9494 deriving Show
9595
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+
96111-- Dealing with implicit arguments
97112
113+-- Add implicit Pi bindings for any names in the term which appear in an
114+-- argument position.
115+
98116implicitise :: 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)
100142
101143addImpl :: 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
109109 return $ PHidden e
110110
111111pApp = do f <- pSimpleExpr
112+ iargs <- many pImplicitArg
112113 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)
114120
115121pTSig = do lchar ':'
116122 pExpr
@@ -173,7 +179,8 @@ bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
173179pConstructor :: IParser (Name, PTerm)
174180pConstructor
175181 = do cn <- pfName; ty <- pTSig
176− return (cn, ty)
182+ ty' <- implicit cn ty
183+ return (cn, ty')
177184
178185pSimpleCon :: IParser (Name, [PTerm])
179186pSimpleCon = do cn <- pfName
@@ -184,10 +191,11 @@ pSimpleCon = do cn <- pfName
184191
185192pPattern :: IParser PDecl
186193pPattern = try (do n <- pfName
194+ iargs <- many pImplicitArg
187195 args <- many pHSimpleExpr
188196 lchar '='
189197 rhs <- pExpr
190− return $ PClause (PApp (PRef n) [] args) rhs)
198+ return $ PClause (PApp (PRef n) iargs args) rhs)
191199 <|> do l <- pSimpleExpr
192200 op <- operator
193201 r <- pSimpleExpr
src/Main.hs+10−1
@@ -42,11 +42,20 @@ runIdris opts =
4242loadModule :: FilePath -> Idris ()
4343loadModule f = do iLOG ("Reading " ++ show f)
4444 ds <- parseProg f
45− iLOG (show ds)
45+ iLOG (dumpDecls ds)
4646 i <- get
4747 iLOG (show (idris_infixes i))
4848 return ()
4949
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+
5059getFile :: Opt -> Maybe String
5160getFile (Filename str) = Just str
5261getFile _ = Nothing