f34f0af · Idris-dev · git.iko.soy

contribs/idriscasesplit.vim+1

@@ -7,6 +7,7 @@ function IdrisReload()

77endfunction

88

99function IdrisShowType()

10+ w

1011 let word = expand("<cword>")

1112 let tc = IdrisReload()

1213 if (! (tc is ""))

src/Core/Execute.hs+1−1

@@ -79,7 +79,7 @@ toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

7979 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

8080 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

8181 fixBinder (Hole t) = Hole <$> toTT t

82− fixBinder (GHole t) = GHole <$> toTT t

82+ fixBinder (GHole i t) = GHole i <$> toTT t

8383 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

8484 fixBinder (PVar t) = PVar <$> toTT t

8585 fixBinder (PVTy t) = PVTy <$> toTT t

src/Core/ProofState.hs+2−2

@@ -379,7 +379,7 @@ defer :: Name -> RunTactic

379379defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

380380 do action (\ps -> let hs = holes ps in

381381 ps { holes = hs \\ [x] })

382− return (Bind n (GHole (mkTy (reverse env) t))

382+ return (Bind n (GHole (length env) (mkTy (reverse env) t))

383383 (mkApp (P Ref n ty) (map getP (reverse env))))

384384 where

385385 mkTy [] t = t

@@ -395,7 +395,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

395395 ds = deferred ps in

396396 ps { holes = hs \\ [x],

397397 deferred = n : ds })

398− return (Bind n (GHole fty)

398+ return (Bind n (GHole 0 fty)

399399 (mkApp (P Ref n ty) (map getP args)))

400400 where

401401 getP n = case lookup n env of

src/Core/TT.hs+5−4

@@ -451,7 +451,8 @@ data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}

451451 | NLet { binderTy :: b,

452452 binderVal :: b }

453453 | Hole { binderTy :: b}

454− | GHole { binderTy :: b}

454+ | GHole { envlen :: Int,

455+ binderTy :: b}

455456 | Guess { binderTy :: b,

456457 binderVal :: b }

457458 | PVar { binderTy :: b }

@@ -467,7 +468,7 @@ instance Sized a => Sized (Binder a) where

467468 size (Let ty val) = 1 + size ty + size val

468469 size (NLet ty val) = 1 + size ty + size val

469470 size (Hole ty) = 1 + size ty

470− size (GHole ty) = 1 + size ty

471+ size (GHole _ ty) = 1 + size ty

471472 size (Guess ty val) = 1 + size ty + size val

472473 size (PVar ty) = 1 + size ty

473474 size (PVTy ty) = 1 + size ty

@@ -479,7 +480,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

479480fmapMB f (Lam t) = liftM Lam (f t)

480481fmapMB f (Pi t) = liftM Pi (f t)

481482fmapMB f (Hole t) = liftM Hole (f t)

482−fmapMB f (GHole t) = liftM GHole (f t)

483+fmapMB f (GHole i t) = liftM (GHole i) (f t)

483484fmapMB f (PVar t) = liftM PVar (f t)

484485fmapMB f (PVTy t) = liftM PVTy (f t)

485486

@@ -951,7 +952,7 @@ showEnv' env t dbg = se 10 env t where

951952

952953 sb env n (Lam t) = showb env "\\ " " => " n t

953954 sb env n (Hole t) = showb env "? " ". " n t

954− sb env n (GHole t) = showb env "?defer " ". " n t

955+ sb env n (GHole i t) = showb env "?defer " ". " n t

955956 sb env n (Pi t) = showb env "(" ") -> " n t

956957 sb env n (PVar t) = showb env "pat " ". " n t

957958 sb env n (PVTy t) = showb env "pty " ". " n t

src/Core/Typecheck.hs+4−4

@@ -165,12 +165,12 @@ check' holes ctxt env top = chk env top where

165165 let tt' = normalise ctxt env tt

166166 lift $ isType ctxt env tt'

167167 return (Hole tv)

168− checkBinder (GHole t)

168+ checkBinder (GHole i t)

169169 = do (tv, tt) <- chk env t

170170 let tv' = normalise ctxt env tv

171171 let tt' = normalise ctxt env tt

172172 lift $ isType ctxt env tt'

173− return (GHole tv)

173+ return (GHole i tv)

174174 checkBinder (Guess t v)

175175 | not holes = lift $ tfail (IncompleteTerm undefined)

176176 | otherwise

@@ -204,8 +204,8 @@ check' holes ctxt env top = chk env top where

204204 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

205205 discharge n (Hole t) scv sct

206206 = return (Bind n (Hole t) scv, sct)

207− discharge n (GHole t) scv sct

208− = return (Bind n (GHole t) scv, sct)

207+ discharge n (GHole i t) scv sct

208+ = return (Bind n (GHole i t) scv, sct)

209209 discharge n (Guess t v) scv sct

210210 = return (Bind n (Guess t v) scv, sct)

211211 discharge n (PVar t) scv sct

src/IRTS/Compiler.hs+1−1

@@ -93,7 +93,7 @@ compile codegen f tm

9393 Bytecode -> dumpBC c f

9494 Error e -> ierror e

9595 where checkMVs = do i <- getIState

96− case idris_metavars i \\ primDefs of

96+ case map fst (idris_metavars i) \\ primDefs of

9797 [] -> return ()

9898 ms -> ifail $ "There are undefined metavariables: " ++ show ms

9999 inDir d h = do let f = d </> h

src/Idris/AbsSyntax.hs+8−5

@@ -281,11 +281,12 @@ addConstraints fc (v, cs)

281281addDeferred = addDeferred' Ref

282282addDeferredTyCon = addDeferred' (TCon 0 0)

283283

284−addDeferred' :: NameType -> [(Name, Type)] -> Idris ()

284+addDeferred' :: NameType -> [(Name, (Int, Type))] -> Idris ()

285285addDeferred' nt ns

286− = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

286+ = do mapM_ (\(n, (i, t)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

287287 i <- getIState

288− putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

288+ putIState $ i { idris_metavars = map (\(n, (i, _)) -> (n, i)) ns ++

289+ idris_metavars i }

289290 where tidyNames used (Bind (MN i x) b sc)

290291 = let n' = uniqueName (UN x) used in

291292 Bind n' b $ tidyNames (n':used) sc

@@ -296,7 +297,9 @@ addDeferred' nt ns

296297

297298solveDeferred :: Name -> Idris ()

298299solveDeferred n = do i <- getIState

299− putIState $ i { idris_metavars = idris_metavars i \\ [n] }

300+ putIState $ i { idris_metavars =

301+ filter (\(n', _) -> n/=n')

302+ (idris_metavars i) }

300303

301304ihPrintResult :: Handle -> String -> Idris ()

302305ihPrintResult h s = do i <- getIState

@@ -1179,7 +1182,7 @@ aiFn inpat expat ist fc f as

11791182 -- This is where namespaces get resolved by adding PAlternative

11801183 = case lookupCtxtName f (idris_implicits ist) of

11811184 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1182− [] -> if f `elem` idris_metavars ist

1185+ [] -> if f `elem` (map fst (idris_metavars ist))

11831186 then Right $ PApp fc (PRef fc f) as

11841187 else Right $ mkPApp fc (length as) (PRef fc f) as

11851188 alts -> Right $

src/Idris/AbsSyntaxTree.hs+1−1

@@ -102,7 +102,7 @@ data IState = IState {

102102 idris_name :: Int,

103103 idris_lineapps :: [((FilePath, Int), PTerm)],

104104 -- ^ Full application LHS on source line

105− idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

105+ idris_metavars :: [(Name, Int)], -- ^ The currently defined but not proven metavariables

106106 idris_coercions :: [Name],

107107 idris_transforms :: [(Term, Term)],

108108 syntax_rules :: [Syntax],

src/Idris/Completion.hs+1−1

@@ -71,7 +71,7 @@ names = do i <- get

7171

7272metavars :: Idris [String]

7373metavars = do i <- get

74− return . map (show . nsroot) $ idris_metavars i \\ primDefs

74+ return . map (show . nsroot) $ map fst (idris_metavars i) \\ primDefs

7575

7676

7777modules :: Idris [String]

src/Idris/ElabDecls.hs+4−4

@@ -41,8 +41,8 @@ recheckC fc env t

4141 return (tm, ty)

4242

4343checkDef fc ns = do ctxt <- getContext

44− mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

45− return (n, t')) ns

44+ mapM (\(n, (i, t)) -> do (t', _) <- recheckC fc [] t

45+ return (n, (i, t'))) ns

4646

4747-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

4848elabType :: ElabInfo -> SyntaxInfo -> String ->

@@ -86,7 +86,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

8686 _ -> False

8787 _ -> False

8888 let opts' = if corec then (Coinductive : opts) else opts

89− ds <- checkDef fc [(n, nty)]

89+ ds <- checkDef fc [(n, (0, nty))]

9090 addIBC (IBCDef n)

9191 addDeferred ds

9292 setFlags n opts'

@@ -1025,7 +1025,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10251025 let imps = getImps wtype -- add to implicits context

10261026 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

10271027 addIBC (IBCDef wname)

1028− def' <- checkDef fc [(wname, wtype)]

1028+ def' <- checkDef fc [(wname, (0, wtype))]

10291029 addDeferred def'

10301030

10311031 -- in the subdecls, lhs becomes:

src/Idris/ElabTerm.hs+7−7

@@ -37,7 +37,7 @@ type ElabD a = Elab' [PDecl] a

3737-- Also find deferred names in the term and their types

3838

3939build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

40− ElabD (Term, [(Name, Type)], [PDecl])

40+ ElabD (Term, [(Name, (Int, Type))], [PDecl])

4141build ist info pattern fn tm

4242 = do elab ist info pattern False fn tm

4343 ivs <- get_instances

@@ -75,7 +75,7 @@ build ist info pattern fn tm

7575-- know about yet on the LHS of a pattern def)

7676

7777buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

78− ElabD (Term, [(Name, Type)], [PDecl])

78+ ElabD (Term, [(Name, (Int, Type))], [PDecl])

7979buildTC ist info pattern tcgen fn tm

8080 = do elab ist info pattern tcgen fn tm

8181 probs <- get_probs

@@ -751,10 +751,10 @@ resolveTC depth fn ist

751751 where isImp (PImp p _ _ _ _ _) = (True, p)

752752 isImp arg = (False, priority arg)

753753

754−collectDeferred :: Term -> State [(Name, Type)] Term

755−collectDeferred (Bind n (GHole t) app) =

754+collectDeferred :: Term -> State [(Name, (Int, Type))] Term

755+collectDeferred (Bind n (GHole i t) app) =

756756 do ds <- get

757− when (not (n `elem` map fst ds)) $ put ((n, t) : ds)

757+ when (not (n `elem` map fst ds)) $ put ((n, (i, t)) : ds)

758758 collectDeferred app

759759collectDeferred (Bind n b t) = do b' <- cdb b

760760 t' <- collectDeferred t

@@ -1123,7 +1123,7 @@ reifyTTBinderApp reif f [x, y]

11231123reifyTTBinderApp reif f [t]

11241124 | f == reflm "Hole" = liftM Hole (reif t)

11251125reifyTTBinderApp reif f [t]

1126− | f == reflm "GHole" = liftM GHole (reif t)

1126+ | f == reflm "GHole" = liftM (GHole 0) (reif t)

11271127reifyTTBinderApp reif f [x, y]

11281128 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

11291129reifyTTBinderApp reif f [t]

@@ -1237,7 +1237,7 @@ reflectBinder (NLet x y)

12371237 = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]

12381238reflectBinder (Hole t)

12391239 = reflCall "Hole" [Var (reflm "TT"), reflect t]

1240−reflectBinder (GHole t)

1240+reflectBinder (GHole _ t)

12411241 = reflCall "GHole" [Var (reflm "TT"), reflect t]

12421242reflectBinder (Guess x y)

12431243 = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]

src/Idris/IBC.hs+6−4

@@ -70,7 +70,7 @@ writeIBC :: FilePath -> FilePath -> Idris ()

7070writeIBC src f

7171 = do iLOG $ "Writing ibc " ++ show f

7272 i <- getIState

73− case idris_metavars i \\ primDefs of

73+ case (Data.List.map fst (idris_metavars i)) \\ primDefs of

7474 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

7575 [] -> return ()

7676 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

@@ -561,8 +561,9 @@ instance (Binary b) => Binary (Binder b) where

561561 put x2

562562 Hole x1 -> do putWord8 4

563563 put x1

564− GHole x1 -> do putWord8 5

565− put x1

564+ GHole x1 x2 -> do putWord8 5

565+ put x1

566+ put x2

566567 Guess x1 x2 -> do putWord8 6

567568 put x1

568569 put x2

@@ -586,7 +587,8 @@ instance (Binary b) => Binary (Binder b) where

586587 4 -> do x1 <- get

587588 return (Hole x1)

588589 5 -> do x1 <- get

589− return (GHole x1)

590+ x2 <- get

591+ return (GHole x1 x2)

590592 6 -> do x1 <- get

591593 x2 <- get

592594 return (Guess x1 x2)

src/Idris/Prover.hs+1−1

@@ -30,7 +30,7 @@ prover lit x =

3030 do ctxt <- getContext

3131 i <- getIState

3232 case lookupTy x ctxt of

33− [t] -> if elem x (idris_metavars i)

33+ [t] -> if elem x (map fst (idris_metavars i))

3434 then prove ctxt lit x t

3535 else ifail $ show x ++ " is not a metavariable"

3636 _ -> fail "No such metavariable"

src/Idris/REPL.hs+33−9

@@ -1,5 +1,5 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2− PatternGuards, CPP #-}

2+ PatternGuards, ScopedTypeVariables, CPP #-}

33

44module Idris.REPL where

55

@@ -110,9 +110,12 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

110110 return ()

111111 where serverLoop :: IO ()

112112 -- TODO: option for port number

113− serverLoop = withSocketsDo $ do sock <- listenOn $ PortNumber 4294

113+ serverLoop = withSocketsDo $

114+ catch (do sock <- listenOn $ PortNumber 4294

114115 i <- readMVar stvar

115− loop i sock

116+ loop i sock)

117+ (\(e :: IOException) -> return ()) -- silently fail

118+ -- TODO: allow multiple instances somehow

116119

117120 fn = case fn_in of

118121 (f:_) -> f

@@ -418,10 +421,31 @@ process h fn (Check (PRef _ n))

418421 imp <- impShow

419422 c <- colourise

420423 case lookupNames n ctxt of

421− ts@(_:_) -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

422− showImp (Just ist) imp c (delabTy ist n)) ts

423− ihPrintResult h ""

424− [] -> ihPrintError h $ "No such variable " ++ show n

424+ ts@(t:_) ->

425+ case lookup t (idris_metavars ist) of

426+ Just i -> showMetavarInfo c imp ist n i

427+ Nothing -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

428+ showImp (Just ist) imp c (delabTy ist n)) ts

429+ ihPrintResult h ""

430+ [] -> ihPrintError h $ "No such variable " ++ show n

431+ where

432+ showMetavarInfo c imp ist n i

433+ = case lookupTy n (tt_ctxt ist) of

434+ (ty:_) -> putTy c imp ist i (delab ist ty)

435+ putTy c imp ist 0 sc

436+ = do ihputStrLn h $ "--------------------------------------"

437+ ihputStrLn h $ showName (Just ist) [] False c n ++ " : "

438+ ++ showImp (Just ist) imp c sc

439+ putTy c imp ist i (PPi _ n t sc)

440+ = do ihputStrLn h $ " " ++

441+ (case n of

442+ MN _ _ -> "_"

443+ UN ('_':'_':_) -> "_"

444+ _ -> showName (Just ist) [] False c n) ++

445+ " : " ++ showImp (Just ist) imp c t

446+ putTy c imp ist (i-1) sc

447+

448+

425449process h fn (Check t)

426450 = do (tm, ty) <- elabVal toplevel False t

427451 ctxt <- getContext

@@ -568,7 +592,7 @@ process h fn (RmProof n')

568592 insertMetavar n =

569593 do i <- getIState

570594 let ms = idris_metavars i

571− putIState $ i { idris_metavars = n : ms }

595+ putIState $ i { idris_metavars = (n, 0) : ms }

572596

573597process h fn' (AddProof prf)

574598 = do fn <- do

@@ -693,7 +717,7 @@ process h fn ListDynamic

693717 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

694718process h fn Metavars

695719 = do ist <- getIState

696− let mvs = idris_metavars ist \\ primDefs

720+ let mvs = map fst (idris_metavars ist) \\ primDefs

697721 case mvs of

698722 [] -> iPrintError "No global metavariables to solve"

699723 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs