f34f0af · Idris-dev · git.iko.soy

contribs/idriscasesplit.vim+1

compare with master

unifiedsplit

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

7endfunction

8

9function IdrisShowType()

10+ w

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

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

11 let tc = IdrisReload()

12 let tc = IdrisReload()

12 if (! (tc is ""))

13 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

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

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

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

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

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

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

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

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

src/Core/ProofState.hs+2−2

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

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

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

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

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

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

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

384 where

385 mkTy [] t = t

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

395 ds = deferred ps in

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

397 deferred = n : ds })

398− return (Bind n (GHole fty)

398+ return (Bind n (GHole 0 fty)

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

400 where

401 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-}}

451 | NLet { binderTy :: b,

452 binderVal :: b }

453 | Hole { binderTy :: b}

454+ | GHole { envlen :: Int,

454− | GHole { binderTy :: b}

455+ binderTy :: b}

455 | Guess { binderTy :: b,

456 | Guess { binderTy :: b,

456 binderVal :: b }

457 binderVal :: b }

457 | PVar { binderTy :: b }

458 | PVar { binderTy :: b }

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

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

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

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

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

469 size (Hole ty) = 1 + size ty

470 size (Hole ty) = 1 + size ty

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

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

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

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

472 size (PVar ty) = 1 + size ty

473 size (PVar ty) = 1 + size ty

473 size (PVTy ty) = 1 + size ty

474 size (PVTy ty) = 1 + size ty

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

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

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

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

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

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

482fmapMB 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)

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

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

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

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

485

486

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

951

952

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

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

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

954 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

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

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

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

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

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

958 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

165 let tt' = normalise ctxt env tt

166 lift $ isType ctxt env tt'

167 return (Hole tv)

168− checkBinder (GHole t)

168+ checkBinder (GHole i t)

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

170 let tv' = normalise ctxt env tv

171 let tt' = normalise ctxt env tt

172 lift $ isType ctxt env tt'

173− return (GHole tv)

173+ return (GHole i tv)

174 checkBinder (Guess t v)

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

176 | otherwise

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

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

205 discharge n (Hole t) scv sct

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

207− discharge n (GHole t) scv sct

207+ discharge n (GHole i t) scv sct

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

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

209 discharge n (Guess t v) scv sct

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

211 discharge n (PVar t) scv sct

src/IRTS/Compiler.hs+1−1

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

93 Bytecode -> dumpBC c f

94 Error e -> ierror e

95 where checkMVs = do i <- getIState

96− case idris_metavars i \\ primDefs of

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

97 [] -> return ()

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

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

src/Idris/AbsSyntax.hs+8−5

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

281addDeferred = addDeferred' Ref

282addDeferredTyCon = addDeferred' (TCon 0 0)

283

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

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

285addDeferred' 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

287 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 }

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

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

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

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

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

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

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

296

297

297solveDeferred :: Name -> Idris ()

298solveDeferred :: Name -> Idris ()

298solveDeferred n = do i <- getIState

299solveDeferred 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) }

300

303

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

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

302ihPrintResult h s = do i <- getIState

305ihPrintResult h s = do i <- getIState

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

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

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

1180 = case lookupCtxtName f (idris_implicits ist) of

1183 = case lookupCtxtName f (idris_implicits ist) of

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

1184 [(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))

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

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

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

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

1185 alts -> Right $

1188 alts -> Right $

src/Idris/AbsSyntaxTree.hs+1−1

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

102 idris_name :: Int,

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

104 -- ^ 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

106 idris_coercions :: [Name],

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

108 syntax_rules :: [Syntax],

src/Idris/Completion.hs+1−1

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

71

72metavars :: Idris [String]

73metavars = do i <- get

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

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

75

76

77modules :: Idris [String]

src/Idris/ElabDecls.hs+4−4

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

41 return (tm, ty)

42

43checkDef fc ns = do ctxt <- getContext

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

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

45− return (n, t')) ns

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

46

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

48elabType :: ElabInfo -> SyntaxInfo -> String ->

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

86 _ -> False

87 _ -> False

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

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

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

90 addIBC (IBCDef n)

91 addDeferred ds

92 setFlags n opts'

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

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

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

1027 addIBC (IBCDef wname)

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

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

1029 addDeferred def'

1030

1031 -- in the subdecls, lhs becomes:

src/Idris/ElabTerm.hs+7−7

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

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

38

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

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

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

41build ist info pattern fn tm

42 = do elab ist info pattern False fn tm

43 ivs <- get_instances

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

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

76

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

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

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

79buildTC ist info pattern tcgen fn tm

80 = do elab ist info pattern tcgen fn tm

81 probs <- get_probs

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

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

752 isImp arg = (False, priority arg)

753

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

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

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

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

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

758 collectDeferred app

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

760 t' <- collectDeferred t

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

1123reifyTTBinderApp reif f [t]

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

1125reifyTTBinderApp reif f [t]

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

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

1127reifyTTBinderApp reif f [x, y]

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

1129reifyTTBinderApp reif f [t]

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

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

1238reflectBinder (Hole t)

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

1240−reflectBinder (GHole t)

1240+reflectBinder (GHole _ t)

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

1242reflectBinder (Guess x y)

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

src/Idris/IBC.hs+6−4

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

70writeIBC src f

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

72 i <- getIState

73− case idris_metavars i \\ primDefs of

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

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

75 [] -> return ()

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

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

561 put x2

562 Hole x1 -> do putWord8 4

563 put x1

564− GHole x1 -> do putWord8 5

564+ GHole x1 x2 -> do putWord8 5

565− put x1

565+ put x1

566+ put x2

566 Guess x1 x2 -> do putWord8 6

567 Guess x1 x2 -> do putWord8 6

567 put x1

568 put x1

568 put x2

569 put x2

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

586 4 -> do x1 <- get

587 4 -> do x1 <- get

587 return (Hole x1)

588 return (Hole x1)

588 5 -> do x1 <- get

589 5 -> do x1 <- get

590+ x2 <- get

589− return (GHole x1)

591+ return (GHole x1 x2)

590 6 -> do x1 <- get

592 6 -> do x1 <- get

591 x2 <- get

593 x2 <- get

592 return (Guess x1 x2)

594 return (Guess x1 x2)

src/Idris/Prover.hs+1−1

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

30 do ctxt <- getContext

31 i <- getIState

32 case lookupTy x ctxt of

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

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

34 then prove ctxt lit x t

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

36 _ -> fail "No such metavariable"

src/Idris/REPL.hs+33−9

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

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2− PatternGuards, CPP #-}

2+ PatternGuards, ScopedTypeVariables, CPP #-}

3

4module Idris.REPL where

5

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

110 return ()

111 where serverLoop :: IO ()

112 -- TODO: option for port number

113+ serverLoop = withSocketsDo $

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

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

114 i <- readMVar stvar

115 i <- readMVar stvar

115− loop i sock

116+ loop i sock)

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

118+ -- TODO: allow multiple instances somehow

116

119

117 fn = case fn_in of

120 fn = case fn_in of

118 (f:_) -> f

121 (f:_) -> f

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

418 imp <- impShow

421 imp <- impShow

419 c <- colourise

422 c <- colourise

420 case lookupNames n ctxt of

423 case lookupNames n ctxt of

424+ ts@(t:_) ->

425+ case lookup t (idris_metavars ist) of

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

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

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

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

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

423− ihPrintResult h ""

429+ ihPrintResult h ""

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

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+

425process h fn (Check t)

449process h fn (Check t)

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

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

427 ctxt <- getContext

451 ctxt <- getContext

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

568 insertMetavar n =

592 insertMetavar n =

569 do i <- getIState

593 do i <- getIState

570 let ms = idris_metavars i

594 let ms = idris_metavars i

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

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

572

596

573process h fn' (AddProof prf)

597process h fn' (AddProof prf)

574 = do fn <- do

598 = do fn <- do

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

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

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

694process h fn Metavars

718process h fn Metavars

695 = do ist <- getIState

719 = do ist <- getIState

696− let mvs = idris_metavars ist \\ primDefs

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

697 case mvs of

721 case mvs of

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

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

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

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