on master help sign in
Fix compilation of unqualified constructor names
9cdf03aEdwin Brady
src/Core/TT.hs+3
@@ -309,6 +309,9 @@ lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
309lookupCtxt :: Name -> Ctxt a -> [a]
309lookupCtxt :: Name -> Ctxt a -> [a]
310lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
310lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
311
311
312+lookupCtxtExact :: Name -> Ctxt a -> [a]
313+lookupCtxtExact n ctxt = [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
314+
312updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
315updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
313updateDef n f ctxt
316updateDef n f ctxt
314 = let ds = lookupCtxtName n ctxt in
317 = let ds = lookupCtxtName n ctxt in
src/IRTS/Simplified.hs+7−7
@@ -46,7 +46,7 @@ simplify :: Bool -> DExp -> State (DDefs, Int) SExp
46simplify tl (DV (Loc i)) = return (SV (Loc i))
46simplify tl (DV (Loc i)) = return (SV (Loc i))
47simplify tl (DV (Glob x))
47simplify tl (DV (Glob x))
48 = do ctxt <- ldefs
48 = do ctxt <- ldefs
49− case lookupCtxt x ctxt of
49+ case lookupCtxtExact x ctxt of
50 [DConstructor _ t 0] -> return $ SCon t x []
50 [DConstructor _ t 0] -> return $ SCon t x []
51 _ -> return $ SV (Glob x)
51 _ -> return $ SV (Glob x)
52simplify tl (DApp tc n args) = do args' <- mapM sVar args
52simplify tl (DApp tc n args) = do args' <- mapM sVar args
@@ -88,7 +88,7 @@ simplify tl (DError str) = return $ SError str
88
88
89sVar (DV (Glob x))
89sVar (DV (Glob x))
90 = do ctxt <- ldefs
90 = do ctxt <- ldefs
91− case lookupCtxt x ctxt of
91+ case lookupCtxtExact x ctxt of
92 [DConstructor _ t 0] -> sVar (DC t x [])
92 [DConstructor _ t 0] -> sVar (DC t x [])
93 _ -> return (Glob x, Nothing)
93 _ -> return (Glob x, Nothing)
94sVar (DV x) = return (x, Nothing)
94sVar (DV x) = return (x, Nothing)
@@ -136,7 +136,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
136 sc env (SV (Glob n)) =
136 sc env (SV (Glob n)) =
137 case lookup n (reverse env) of -- most recent first
137 case lookup n (reverse env) of -- most recent first
138 Just i -> do lvar i; return (SV (Loc i))
138 Just i -> do lvar i; return (SV (Loc i))
139− Nothing -> case lookupCtxt n ctxt of
139+ Nothing -> case lookupCtxtExact n ctxt of
140 [DConstructor _ i ar] ->
140 [DConstructor _ i ar] ->
141 if True -- ar == 0
141 if True -- ar == 0
142 then return (SCon i n [])
142 then return (SCon i n [])
@@ -146,7 +146,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
146 [] -> fail $ "Codegen error: No such variable " ++ show n
146 [] -> fail $ "Codegen error: No such variable " ++ show n
147 sc env (SApp tc f args)
147 sc env (SApp tc f args)
148 = do args' <- mapM (scVar env) args
148 = do args' <- mapM (scVar env) args
149− case lookupCtxt f ctxt of
149+ case lookupCtxtExact f ctxt of
150 [DConstructor n tag ar] ->
150 [DConstructor n tag ar] ->
151 if True -- (ar == length args)
151 if True -- (ar == length args)
152 then return $ SCon tag n args'
152 then return $ SCon tag n args'
@@ -160,7 +160,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
160 return $ SForeign l ty f args'
160 return $ SForeign l ty f args'
161 sc env (SCon tag f args)
161 sc env (SCon tag f args)
162 = do args' <- mapM (scVar env) args
162 = do args' <- mapM (scVar env) args
163− case lookupCtxt f ctxt of
163+ case lookupCtxtExact f ctxt of
164 [DConstructor n tag ar] ->
164 [DConstructor n tag ar] ->
165 if True -- (ar == length args)
165 if True -- (ar == length args)
166 then return $ SCon tag n args'
166 then return $ SCon tag n args'
@@ -197,7 +197,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
197 scVar env (Glob n) =
197 scVar env (Glob n) =
198 case lookup n (reverse env) of -- most recent first
198 case lookup n (reverse env) of -- most recent first
199 Just i -> do lvar i; return (Loc i)
199 Just i -> do lvar i; return (Loc i)
200− Nothing -> case lookupCtxt n ctxt of
200+ Nothing -> case lookupCtxtExact n ctxt of
201 [DConstructor _ i ar] ->
201 [DConstructor _ i ar] ->
202 fail $ "Codegen error : can't pass constructor here"
202 fail $ "Codegen error : can't pass constructor here"
203 [_] -> return (Glob n)
203 [_] -> return (Glob n)
@@ -207,7 +207,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
207
207
208 scalt env (SConCase _ i n args e)
208 scalt env (SConCase _ i n args e)
209 = do let env' = env ++ zip args [length env..]
209 = do let env' = env ++ zip args [length env..]
210− tag <- case lookupCtxt n ctxt of
210+ tag <- case lookupCtxtExact n ctxt of
211 [DConstructor _ i ar] ->
211 [DConstructor _ i ar] ->
212 if True -- (length args == ar)
212 if True -- (length args == ar)
213 then return i
213 then return i
test/reg007/expected+12
@@ -1 +1,13 @@
1reg007.lidr:8:A.n is already defined
1reg007.lidr:8:A.n is already defined
2+reg007.lidr:12:When elaborating right hand side of hurrah:
3+Can't unify
4+ n = A.lala
5+with
6+ 0 = 1
7+
8+Specifically:
9+ Can't unify
10+ 1
11+ with
12+ 0
13+
test/reg007/reg007.lidr+3−3
@@ -5,8 +5,8 @@
5> isSame : A.n = A.lala
5> isSame : A.n = A.lala
6> isSame = refl
6> isSame = refl
7
7
8−> A.n = O -- This is where it's at!
8+> A.n = Z -- This is where it's at!
9−> A.lala = S O
9+> A.lala = S Z
10
10
11−> hurrah : O = S O
11+> hurrah : Z = S Z
12> hurrah = isSame
12> hurrah = isSame
test/test030/Reflect.idr+1
@@ -1,6 +1,7 @@
1module Reflect
1module Reflect
2
2
3import Decidable.Equality
3import Decidable.Equality
4+%default total
4
5
5using (xs : List a, ys : List a, G : List (List a))
6using (xs : List a, ys : List a, G : List (List a))
6
7