6adee80 · Idris-dev · git.iko.soy

src/Core/Unify.hs+7−2

compare with master

unifiedsplit

@@ -34,7 +34,6 @@ data UResult a = UOK a

34match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

35 TC [(Name, TT Name)]

36match_unify ctxt env topx topy dont holes =

37−-- trace ("Matching " ++ show (topx, topy)) $

38 case runStateT (un [] topx topy) (UI 0 []) of

37 case runStateT (un [] topx topy) (UI 0 []) of

39 OK (v, UI _ []) -> return (filter notTrivial v)

38 OK (v, UI _ []) -> return (filter notTrivial v)

40 res ->

39 res ->

@@ -44,7 +43,13 @@ match_unify ctxt env topx topy dont holes =

44 (UI 0 []) of

43 (UI 0 []) of

45 OK (v, UI _ fails) ->

44 OK (v, UI _ fails) ->

46 return (filter notTrivial v)

45 return (filter notTrivial v)

47− Error e -> tfail e

46+ Error e ->

47+ -- just normalise the term we're matching against

48+ case runStateT (un [] topxn topy)

49+ (UI 0 []) of

50+ OK (v, UI _ fails) ->

51+ return (filter notTrivial v)

52+ _ -> tfail e

48 where

53 where

49 un names (P _ x _) tm

54 un names (P _ x _) tm

50 | holeIn env x || x `elem` holes

55 | holeIn env x || x `elem` holes

src/Idris/AbsSyntaxTree.hs+1

@@ -242,6 +242,7 @@ data Command = Quit

242 | CaseSplit Name PTerm

243 | CaseSplitAt Bool Int Name

244 | AddClauseFrom Bool Int Name

245+ | AddProofClauseFrom Bool Int Name

245 | AddMissing Bool Int Name

246 | AddMissing Bool Int Name

246 | MakeWith Bool Int Name

247 | MakeWith Bool Int Name

247 | DoProofSearch Bool Int Name [Name]

248 | DoProofSearch Bool Int Name [Name]

src/Idris/CaseSplit.hs+11−1

@@ -1,7 +1,7 @@

1{-# LANGUAGE PatternGuards #-}

2

3module Idris.CaseSplit(split, splitOnLine, replaceSplits,

4− getClause,

4+ getClause, getProofClause,

5 mkWith,

6 getUniq, nameRoot) where

7

@@ -272,6 +272,16 @@ getClause l fn fp = do ty <- getInternalApp fp l

272 mkApp (PPi _ _ _ sc) ns = mkApp sc ns

273 mkApp _ _ = ""

274

275+getProofClause :: Int -> -- ^ Line type is declared on

276+ Name -> -- ^ Function name

277+ FilePath -> -- ^ Source file name

278+ Idris String

279+getProofClause l fn fp

280+ = do ty <- getInternalApp fp l

281+ return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

282+ where mkApp (PPi _ _ _ sc) = mkApp sc

283+ mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

284+

275-- Purely syntactic - turn a pattern match clause into a with and a new

285-- Purely syntactic - turn a pattern match clause into a with and a new

276-- match clause

286-- match clause

277

287

src/Idris/ElabDecls.hs+9−7

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

53 ctxt <- getContext

54 i <- getIState

55

56− -- Add user one, not implicitsed one

57− addInternalApp (fc_fname fc) (fc_line fc) ty'

58− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) ty')

59−

60 logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

56 logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

61 ty' <- addUsingConstraints syn fc ty'

57 ty' <- addUsingConstraints syn fc ty'

62 ty' <- implicit syn n ty'

58 ty' <- implicit syn n ty'

@@ -79,6 +75,11 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

79 let nty = cty -- normalise ctxt [] cty

75 let nty = cty -- normalise ctxt [] cty

80 -- if the return type is something coinductive, freeze the definition

76 -- if the return type is something coinductive, freeze the definition

81 let nty' = normalise ctxt [] nty

77 let nty' = normalise ctxt [] nty

78+

79+ -- Add normalised type to internals

80+ addInternalApp (fc_fname fc) (fc_line fc) (delab i nty')

81+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i nty'))

82+

82 let (t, _) = unApply (getRetTy nty')

83 let (t, _) = unApply (getRetTy nty')

83 let corec = case t of

84 let corec = case t of

84 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

85 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

@@ -832,11 +833,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

832 logLvl 3 ("Elaborated: " ++ show lhs_tm)

833 logLvl 3 ("Elaborated: " ++ show lhs_tm)

833 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

834 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

834

835

835− addInternalApp (fc_fname fc) (fc_line fc) (delab i lhs_tm)

836− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i lhs_tm))

837−

838 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

836 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

839 let clhs = normalise ctxt [] clhs_c

837 let clhs = normalise ctxt [] clhs_c

838+

839+ addInternalApp (fc_fname fc) (fc_line fc) (delab i clhs)

840+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i clhs))

841+

840 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

842 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

841 -- Elaborate where block

843 -- Elaborate where block

842 ist <- getIState

844 ist <- getIState

src/Idris/REPL.hs+20

@@ -535,6 +535,7 @@ process h fn (Search t) = iPrintError "Not implemented"

535process h fn (CaseSplit n t)

536 = do tms <- split n t

537 iputStrLn (showSep "\n" (map show tms))

538+-- FIXME: There is far too much repetition in the cases below!

538process h fn (CaseSplitAt updatefile l n)

539process h fn (CaseSplitAt updatefile l n)

539 = do src <- runIO $ readFile fn

540 = do src <- runIO $ readFile fn

540 res <- splitOnLine l n fn

541 res <- splitOnLine l n fn

@@ -567,6 +568,25 @@ process h fn (AddClauseFrom updatefile l n)

567 getIndent i n [] = 0

568 getIndent i n [] = 0

568 getIndent i n xs | take (length n) xs == n = i

569 getIndent i n xs | take (length n) xs == n = i

569 getIndent i n (x : xs) = getIndent (i + 1) n xs

570 getIndent i n (x : xs) = getIndent (i + 1) n xs

571+process h fn (AddProofClauseFrom updatefile l n)

572+ = do src <- runIO $ readFile fn

573+ let (before, tyline : later) = splitAt (l-1) (lines src)

574+ let indent = getIndent 0 (show n) tyline

575+ cl <- getProofClause l n fn

576+ -- add clause before first blank line in 'later'

577+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

578+ if updatefile then

579+ do let fb = fn ++ "~"

580+ runIO $ writeFile fb (unlines (before ++ nonblank)

581+ ++ replicate indent ' ' ++

582+ cl ++ "\n" ++

583+ unlines rest)

584+ runIO $ copyFile fb fn

585+ else ihputStrLn h cl

586+ where

587+ getIndent i n [] = 0

588+ getIndent i n xs | take (length n) xs == n = i

589+ getIndent i n (x : xs) = getIndent (i + 1) n xs

570process h fn (AddMissing updatefile l n)

590process h fn (AddMissing updatefile l n)

571 = do src <- runIO $ readFile fn

591 = do src <- runIO $ readFile fn

572 let (before, tyline : later) = splitAt (l-1) (lines src)

592 let (before, tyline : later) = splitAt (l-1) (lines src)

src/Idris/REPLParser.hs+4

@@ -69,6 +69,10 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

69 upd <- option False (do P.lchar '!'; return True)

70 l <- P.natural; n <- P.name;

71 return (CaseSplitAt upd (fromInteger l) n))

72+ <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;

73+ upd <- option False (do P.lchar '!'; return True)

74+ l <- P.natural; n <- P.name;

75+ return (AddProofClauseFrom upd (fromInteger l) n))

72 <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

76 <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

73 upd <- option False (do P.lchar '!'; return True)

77 upd <- option False (do P.lchar '!'; return True)

74 l <- P.natural; n <- P.name;

78 l <- P.natural; n <- P.name;