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

src/Core/Elaborate.hs+1−1

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

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

135135uniqueNameCtxt ctxt n hs

136136 | 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

138138 | otherwise = return n

139139

140140elog :: String -> Elab ()

src/Core/Evaluate.hs+22−21

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

105105

106106 ev top env (P _ n ty)

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

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

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

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

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

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

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

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

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

112112 if simpl && (not inl)

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

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

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

149149 apply False env f args

150150 | spec = return $ unload env f args

151151 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

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

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

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

156156 case c of

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

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

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

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

160160 = if (i <= length args)

161161 then case op (take i args) of

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

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

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

293293 ev env (P _ n ty)

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

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

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

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

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

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

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

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

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

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

300300 case c of

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

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

325325 app <- apply env sc' as

326326 wknH (-1) app

327327 apply env (HP Ref n ty) args

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

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

329329 = do c <- evCase env ns args tree

330330 case c of

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

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

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

495495 uctxt { definitions = ctxt' }

496496

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

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

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

498+lookupTy root n ctxt

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

499500 case def of

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

501502 (TyDecl _ ty _) -> return ty

502503 (Operator ty _ _) -> return ty

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

504505

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

506−lookupP n ctxt

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

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

507+lookupP root n ctxt

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

508509 case def of

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

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

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

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

513514

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

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

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

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

516517

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

518−lookupVal n ctxt

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

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

519+lookupVal root n ctxt

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

520521 case def of

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

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

src/Core/ProofShell.hs+3−3

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

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

3838 err -> (state, show err)

3939processCommand (Print n) state =

40− case lookupDef n (ctxt state) of

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

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

40+ case lookupDef Nothing n (ctxt state) of

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

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

4343processCommand (Tac e) state

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

4545 OK (ES ps' resp _) ->

src/Core/TT.hs+16−2

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

110110addDef :: Name -> a -> Ctxt a -> Ctxt a

111111addDef = Map.insert

112112

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

114−lookupCtxt = Map.lookup

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+

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

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

127+ Just x -> [x]

128+ Nothing -> []

115129

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

117131toAlist = Map.toList

src/Core/Typecheck.hs+1−1

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

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

5252 chk env (Var n)

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

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

5656 chk env (RApp f a)

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

src/Idris/AbsSyntax.hs+14−12

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

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

102102checkUndefined fc n

103103 = do i <- getContext

104− case lookupTy n i of

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

104+ case lookupTy Nothing n i of

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

106106 show n ++ " already defined"

107107 _ -> return ()

108108

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

560560 where

561561 ni env (PRef _ n)

562562 | not (n `elem` env)

563− = case lookupTy n (tt_ctxt ist) of

564− Nothing -> [n]

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

564+ [] -> [n]

565565 _ -> []

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

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

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

714714getPriority i tm = pri tm

715715 where

716716 pri (PRef _ n) =

717− case lookupP n (tt_ctxt i) of

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

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

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

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

717+ case lookupP Nothing n (tt_ctxt i) of

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

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

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

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

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

723723 pri (PTrue _) = 0

724724 pri (PFalse _) = 0

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

866866aiFn ist fc f as

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

868868aiFn ist fc f as

869− = case lookupCtxt f (idris_implicits ist) of

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

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

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

870+ -- PAlternative

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

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

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

872874 where

873875 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

src/Idris/Delaborate.hs+1−1

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

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

4040

4141 mkPApp n args

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

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

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

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

4545

src/Idris/ElabDecls.hs+6−6

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

9696 let tree = simpleCase tcase (map debind pats)

9797 logLvl 3 (show tree)

9898 ctxt <- getContext

99− case lookupTy n ctxt of

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

99+ case lookupTy Nothing n ctxt of

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

101101 tcase (map debind pats) ty)

102− Nothing -> return ()

102+ [] -> return ()

103103 where

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

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

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

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

377377elabInstance info syn fc cs n ps t ds

378378 = do i <- get

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

380− Just c -> return c

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

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

380+ [c] -> return c

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

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

383383 elabType info syn fc iname t

384384 let ips = zip (class_params ci) ps

src/Idris/ElabTerm.hs+11−10

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

100100

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

102102 = do ctxt <- get_context

103− let sc = case lookupTy n ctxt of

104− Nothing -> True

103+ let sc = case lookupTy Nothing n ctxt of

104+ [] -> True

105105 _ -> False

106106 if sc

107107 then erun fc $

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

109109 (patvar n)

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

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

112− Nothing -> False

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

112+ [] -> False

113113 _ -> True

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

115115 elab' (PLam n Placeholder sc)

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

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

237237 | otherwise

238238 = do t <- goal

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

240− Nothing -> []

241− Just args -> map isImp args

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

240+ [] -> []

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

242242 args <- apply (Var n) imps

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

244244 resolveTC (depth - 1) ist)

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

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

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

277277 when autoSolve solveAll

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

279− Nothing -> envArgs fn

280− Just args -> return $ map isImp args

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

279+ [] -> envArgs fn

280+ -- FIXME: resolve ambiguities

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

281282 ns <- apply (Var fn) imps

282283 when autoSolve solveAll

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

src/Idris/Prover.hs+2−2

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

1919prover :: Name -> Idris ()

2020prover x = do ctxt <- getContext

2121 i <- get

22− case lookupTy x ctxt of

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

22+ case lookupTy Nothing x ctxt of

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

2424 then prove ctxt x t

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

2626 _ -> fail "No such metavariable"

src/Idris/REPL.hs+3−3

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

100100 = do ctxt <- getContext

101101 ist <- get

102102 imp <- impShow

103− case lookupTy n ctxt of

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

103+ case lookupTy Nothing n ctxt of

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

105105 showImp imp (delab ist t)

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

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

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

117117 lift $ print (map fst cs)

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

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

120− lift $ print (lookupDef n ctxt)

120+ lift $ print (lookupDef Nothing n ctxt)

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

122122 ctxt <- getContext

123123 ist <- get