8cd093f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed lookup to return a list (preparation for namespaces)

8cd093fEdwin Brady15 years ago

src/Core/Elaborate.hs+1−1

compare with master

unifiedsplit

@@ -134,7 +134,7 @@ unique_hole n = do ES p _ _ <- get

134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name

135uniqueNameCtxt ctxt n hs

136 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

137− | Just _ <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

137+ | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs

138 | otherwise = return n

139

140elog :: String -> Elab ()

src/Core/Evaluate.hs+22−21

@@ -105,10 +105,10 @@ eval ctxt statics genv tm opts = ev True [] tm where

105

106 ev top env (P _ n ty)

107 | Just (Let t v) <- lookup n genv = ev top env v

108− ev top env (P Ref n ty) = case lookupDef n ctxt of

108+ ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

109− Just (Function (Fun _ _ _ v)) -> return v

109+ [Function (Fun _ _ _ v)] -> return v

110− Just (TyDecl nt ty hty) -> return $ VP nt n hty

110+ [TyDecl nt ty hty] -> return $ VP nt n hty

111− Just (CaseOp inl _ _ [] tree) ->

111+ [CaseOp inl _ _ [] tree] ->

112 if simpl && (not inl)

113 then liftM (VP Ref n) (ev top env ty)

114 else do c <- evCase top env [] [] tree

@@ -149,14 +149,14 @@ eval ctxt statics genv tm opts = ev True [] tm where

149 apply False env f args

150 | spec = return $ unload env f args

151 apply top env (VP Ref n ty) args

152− | Just (CaseOp inl _ _ ns tree) <- lookupDef n ctxt

152+ | [CaseOp inl _ _ ns tree] <- lookupDef Nothing n ctxt

153 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

154 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

155 else do c <- evCase top env ns args tree

156 case c of

157 (Nothing, _) -> return $ unload env (VP Ref n ty) args

158 (Just v, rest) -> evApply top env rest v

159− | Just (Operator _ i op) <- lookupDef n ctxt

159+ | [Operator _ i op] <- lookupDef Nothing n ctxt

160 = if (i <= length args)

161 then case op (take i args) of

162 Nothing -> return $ unload env (VP Ref n ty) args

@@ -292,10 +292,10 @@ eval_hnf ctxt statics genv tm = ev [] tm where

292 ev :: [HNF] -> TT Name -> Eval HNF

293 ev env (P _ n ty)

294 | Just (Let t v) <- lookup n genv = ev env v

295− ev env (P Ref n ty) = case lookupDef n ctxt of

295+ ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

296− Just (Function (Fun _ _ t _)) -> ev env t

296+ [Function (Fun _ _ t _)] -> ev env t

297− Just (TyDecl nt ty hty) -> return $ HP nt n ty

297+ [TyDecl nt ty hty] -> return $ HP nt n ty

298− Just (CaseOp inl _ _ [] tree) ->

298+ [CaseOp inl _ _ [] tree] ->

299 do c <- evCase env [] [] tree

300 case c of

301 (Nothing, _, _) -> return $ HP Ref n ty

@@ -325,7 +325,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

325 app <- apply env sc' as

326 wknH (-1) app

327 apply env (HP Ref n ty) args

328− | Just (CaseOp _ _ _ ns tree) <- lookupDef n ctxt

328+ | [CaseOp _ _ _ ns tree] <- lookupDef Nothing n ctxt

329 = do c <- evCase env ns args tree

330 case c of

331 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -494,29 +494,30 @@ addOperator n ty a op uctxt

494 ctxt' = addDef n (Operator ty a op) ctxt in

495 uctxt { definitions = ctxt' }

496

497−lookupTy :: Name -> Context -> Maybe Type

497+lookupTy :: Maybe Name -> Name -> Context -> [Type]

498+lookupTy root n ctxt

498−lookupTy n ctxt = do def <- lookupCtxt n (definitions ctxt)

499+ = do def <- lookupCtxt root n (definitions ctxt)

499 case def of

500 case def of

500 (Function (Fun ty _ _ _)) -> return ty

501 (Function (Fun ty _ _ _)) -> return ty

501 (TyDecl _ ty _) -> return ty

502 (TyDecl _ ty _) -> return ty

502 (Operator ty _ _) -> return ty

503 (Operator ty _ _) -> return ty

503 (CaseOp _ ty _ _ _) -> return ty

504 (CaseOp _ ty _ _ _) -> return ty

504

505

505−lookupP :: Name -> Context -> Maybe Term

506+lookupP :: Maybe Name -> Name -> Context -> [Term]

506−lookupP n ctxt

507+lookupP root n ctxt

507− = do def <- lookupCtxt n (definitions ctxt)

508+ = do def <- lookupCtxt root n (definitions ctxt)

508 case def of

509 case def of

509 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

510 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

510 (TyDecl nt ty hty) -> return (P nt n ty)

511 (TyDecl nt ty hty) -> return (P nt n ty)

511 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

512 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

512 (Operator ty _ _) -> return (P Ref n ty)

513 (Operator ty _ _) -> return (P Ref n ty)

513

514

514−lookupDef :: Name -> Context -> Maybe Def

515+lookupDef :: Maybe Name -> Name -> Context -> [Def]

515−lookupDef n ctxt = lookupCtxt n (definitions ctxt)

516+lookupDef root n ctxt = lookupCtxt root n (definitions ctxt)

516

517

517−lookupVal :: Name -> Context -> Maybe Value

518+lookupVal :: Maybe Name -> Name -> Context -> [Value]

518−lookupVal n ctxt

519+lookupVal root n ctxt

519− = do def <- lookupCtxt n (definitions ctxt)

520+ = do def <- lookupCtxt root n (definitions ctxt)

520 case def of

521 case def of

521 (Function (Fun _ _ _ htm)) -> return htm

522 (Function (Fun _ _ _ htm)) -> return htm

522 (TyDecl nt ty hty) -> return (VP nt n hty)

523 (TyDecl nt ty hty) -> return (VP nt n hty)

src/Core/ProofShell.hs+3−3

@@ -37,9 +37,9 @@ processCommand (Eval t) state =

37 (state, show nf ++ " : " ++ show ty)

38 err -> (state, show err)

39processCommand (Print n) state =

40− case lookupDef n (ctxt state) of

40+ case lookupDef Nothing n (ctxt state) of

41− Just tm -> (state, show tm)

41+ [tm] -> (state, show tm)

42− Nothing -> (state, "No such name")

42+ _ -> (state, "No such name")

43processCommand (Tac e) state

44 | Just ps <- prf state = case execElab e ps of

45 OK (ES ps' resp _) ->

src/Core/TT.hs+16−2

@@ -110,8 +110,22 @@ emptyContext = Map.empty

110addDef :: Name -> a -> Ctxt a -> Ctxt a

111addDef = Map.insert

112

113+{- lookup a name in the context, given an optional namespace.

114+ The name (n) may itself have a (partial) namespace given.

115+

116+ Rules for resolution:

117+ - if an explicit namespace is given, return the names which match it. If none

118+ match, return all names.

119+ - if the name has has explicit namespace given, return the names which match it

120+ and ignore the given namespace.

121+ - otherwise, return all names.

122+

123+-}

124+

113−lookupCtxt :: Name -> Ctxt a -> Maybe a

125+lookupCtxt :: Maybe Name -> Name -> Ctxt a -> [a]

114−lookupCtxt = Map.lookup

126+lookupCtxt nspace n ctxt = case Map.lookup n ctxt of

127+ Just x -> [x]

128+ Nothing -> []

115

129

116toAlist :: Ctxt a -> [(Name, a)]

130toAlist :: Ctxt a -> [(Name, a)]

117toAlist = Map.toList

131toAlist = Map.toList

src/Core/Typecheck.hs+1−1

@@ -51,7 +51,7 @@ check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

51check' holes ctxt env top = chk env top where

52 chk env (Var n)

53 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

54− | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)

54+ | [P nt n' ty] <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

55 | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)

56 chk env (RApp f a)

57 = do (fv, fty) <- chk env f

src/Idris/AbsSyntax.hs+14−12

@@ -101,8 +101,8 @@ getName = do i <- get;

101checkUndefined :: FC -> Name -> Idris ()

102checkUndefined fc n

103 = do i <- getContext

104− case lookupTy n i of

104+ case lookupTy Nothing n i of

105− Just _ -> fail $ show fc ++ ":" ++

105+ (_:_) -> fail $ show fc ++ ":" ++

106 show n ++ " already defined"

107 _ -> return ()

108

@@ -560,8 +560,8 @@ namesIn ist tm = nub $ ni [] tm

560 where

561 ni env (PRef _ n)

562 | not (n `elem` env)

563− = case lookupTy n (tt_ctxt ist) of

563+ = case lookupTy Nothing n (tt_ctxt ist) of

564− Nothing -> [n]

564+ [] -> [n]

565 _ -> []

566 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

567 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

@@ -714,11 +714,11 @@ getPriority :: IState -> PTerm -> Int

714getPriority i tm = pri tm

715 where

716 pri (PRef _ n) =

717− case lookupP n (tt_ctxt i) of

717+ case lookupP Nothing n (tt_ctxt i) of

718− Just (P (DCon _ _) _ _) -> 1

718+ ((P (DCon _ _) _ _):_) -> 1

719− Just (P (TCon _ _) _ _) -> 1

719+ ((P (TCon _ _) _ _):_) -> 1

720− Just (P Ref _ _) -> 3

720+ ((P Ref _ _):_) -> 3

721− Nothing -> 0 -- must be locally bound, if it's not an error...

721+ [] -> 0 -- must be locally bound, if it's not an error...

722 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))

723 pri (PTrue _) = 0

724 pri (PFalse _) = 0

@@ -866,9 +866,11 @@ aiFn :: IState -> FC -> Name -> [PArg] -> PTerm

866aiFn ist fc f as

867 | f `elem` primNames = PApp fc (PRef fc f) as

868aiFn ist fc f as

869+ -- TODO: This is where namespaces get resolved by adding

870+ -- PAlternative

869− = case lookupCtxt f (idris_implicits ist) of

871+ = case lookupCtxt Nothing f (idris_implicits ist) of

870− Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)

872+ [ns] -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)

871− Nothing -> mkPApp fc 1 (PRef fc f) as

873+ [] -> mkPApp fc 1 (PRef fc f) as

872 where

874 where

873 insertImpl :: [PArg] -> [PArg] -> [PArg]

875 insertImpl :: [PArg] -> [PArg] -> [PArg]

874 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

876 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

src/Idris/Delaborate.hs+1−1

@@ -39,7 +39,7 @@ delab ist tm = de [] tm

39 deFn env f args = PApp un (de env f) (map pexp (map (de env) args))

41 mkPApp n args

42− | Just imps <- lookupCtxt n (idris_implicits ist)

42+ | [imps] <- lookupCtxt Nothing n (idris_implicits ist)

43 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

44 | otherwise = PApp un (PRef un n) (map pexp args)

src/Idris/ElabDecls.hs+6−6

@@ -96,10 +96,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

96 let tree = simpleCase tcase (map debind pats)

97 logLvl 3 (show tree)

98 ctxt <- getContext

99− case lookupTy n ctxt of

99+ case lookupTy Nothing n ctxt of

100− Just ty -> updateContext (addCasedef n (inlinable opts)

100+ [ty] -> updateContext (addCasedef n (inlinable opts)

101 tcase (map debind pats) ty)

102− Nothing -> return ()

102+ [] -> return ()

103 where

104 debind (x, y) = (depat x, depat y)

105 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

@@ -376,9 +376,9 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

376 [PTerm] -> PTerm -> [PDecl] -> Idris ()

377elabInstance info syn fc cs n ps t ds

378 = do i <- get

379− ci <- case lookupCtxt n (idris_classes i) of

379+ ci <- case lookupCtxt Nothing n (idris_classes i) of

380− Just c -> return c

380+ [c] -> return c

381− Nothing -> fail $ show n ++ " is not a type class"

381+ _ -> fail $ show n ++ " is not a type class"

382 let iname = UN ('@':show n ++ "$" ++ show ps)

383 elabType info syn fc iname t

384 let ips = zip (class_params ci) ps

src/Idris/ElabTerm.hs+11−10

@@ -100,16 +100,16 @@ elab ist info pattern tm

100

101 elab' (PRef fc n) | pattern && not (inparamBlock n)

102 = do ctxt <- get_context

103− let sc = case lookupTy n ctxt of

103+ let sc = case lookupTy Nothing n ctxt of

104− Nothing -> True

104+ [] -> True

105 _ -> False

106 if sc

107 then erun fc $

108 try (do apply (Var n) []; solve)

109 (patvar n)

110 else do apply (Var n) []; solve

111− where inparamBlock n = case lookupCtxt n (inblock info) of

111+ where inparamBlock n = case lookupCtxt Nothing n (inblock info) of

112− Nothing -> False

112+ [] -> False

113 _ -> True

114 elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

115 elab' (PLam n Placeholder sc)

@@ -236,9 +236,9 @@ resolveTC depth ist

236 | depth == 0 = fail $ "Can't resolve type class"

237 | otherwise

238 = do t <- goal

239− let imps = case lookupCtxt n (idris_implicits ist) of

239+ let imps = case lookupCtxt Nothing n (idris_implicits ist) of

240− Nothing -> []

240+ [] -> []

241− Just args -> map isImp args

241+ [args] -> map isImp args -- won't be overloaded!

242 args <- apply (Var n) imps

243 mapM_ (\ (_,n) -> do focus n

244 resolveTC (depth - 1) ist)

@@ -275,9 +275,10 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

275 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

276 runT (Exact tm) = do elab ist toplevel False tm

277 when autoSolve solveAll

278− runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of

278+ runT (Refine fn []) = do imps <- case lookupCtxt Nothing fn (idris_implicits ist) of

279− Nothing -> envArgs fn

279+ [] -> envArgs fn

280+ -- FIXME: resolve ambiguities

280− Just args -> return $ map isImp args

281+ [args] -> return $ map isImp args

281 ns <- apply (Var fn) imps

282 ns <- apply (Var fn) imps

282 when autoSolve solveAll

283 when autoSolve solveAll

283 where isImp (PImp _ _ _ _) = True

284 where isImp (PImp _ _ _ _) = True

src/Idris/Prover.hs+2−2

@@ -19,8 +19,8 @@ import Control.Monad.State

19prover :: Name -> Idris ()

20prover x = do ctxt <- getContext

21 i <- get

22− case lookupTy x ctxt of

22+ case lookupTy Nothing x ctxt of

23− Just t -> if elem x (idris_metavars i)

23+ [t] -> if elem x (idris_metavars i)

24 then prove ctxt x t

25 else fail $ show x ++ " is not a metavariable"

26 _ -> fail "No such metavariable"

src/Idris/REPL.hs+3−3

@@ -100,8 +100,8 @@ process (Check (PRef _ n))

100 = do ctxt <- getContext

101 ist <- get

102 imp <- impShow

103− case lookupTy n ctxt of

103+ case lookupTy Nothing n ctxt of

104− Just t -> iputStrLn $ show n ++ " : " ++

104+ [t] -> iputStrLn $ show n ++ " : " ++

105 showImp imp (delab ist t)

106 _ -> iputStrLn $ "No such variable " ++ show n

107process (Check t) = do (tm, ty) <- elabVal toplevel False t

@@ -117,7 +117,7 @@ process Universes = do i <- get

117 lift $ print (map fst cs)

118 iputStrLn $ "(" ++ show (length cs) ++ " constraints)"

119process (Defn n) = do ctxt <- getContext

120− lift $ print (lookupDef n ctxt)

120+ lift $ print (lookupDef Nothing n ctxt)

121process (Spec t) = do (tm, ty) <- elabVal toplevel False t

122 ctxt <- getContext

123 ist <- get