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

git.iko.soy/Idris-dev

Add :apc for adding "proof style" declarations

That is, :apc on plus_comm : (m, n : Nat) -> (plus m n = plus n m) will add the caluse (plus m n = plus n m) <== plus_comm = ?plus_comm_rhs where m and n can be case split as normal

commit6adee8048d06b8de15be9a04653412b2e7bf6e09 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 1 Nov 2013, 12:21 (13 years ago) parentc553f6a

6 files changed+52−10

compare with master

unifiedsplit

src/Core/Unify.hs+7−2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CaseSplit.hs+11−1 src/Idris/ElabDecls.hs+9−7 src/Idris/REPL.hs+20 src/Idris/REPLParser.hs+4

src/Core/Unify.hs+7−2

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

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

3535 TC [(Name, TT Name)]

3636match_unify ctxt env topx topy dont holes =

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

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

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

4039 res ->

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

4443 (UI 0 []) of

4544 OK (v, UI _ fails) ->

4645 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

4853 where

4954 un names (P _ x _) tm

5055 | holeIn env x || x `elem` holes

src/Idris/AbsSyntaxTree.hs+1

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

242242 | CaseSplit Name PTerm

243243 | CaseSplitAt Bool Int Name

244244 | AddClauseFrom Bool Int Name

245+ | AddProofClauseFrom Bool Int Name

245246 | AddMissing Bool Int Name

246247 | MakeWith Bool Int Name

247248 | DoProofSearch Bool Int Name [Name]

src/Idris/CaseSplit.hs+11−1

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

11{-# LANGUAGE PatternGuards #-}

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

4− getClause,

4+ getClause, getProofClause,

55 mkWith,

66 getUniq, nameRoot) where

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

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

273273 mkApp _ _ = ""

274274

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+

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

276286-- match clause

277287

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

5353 ctxt <- getContext

5454 i <- getIState

5555

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−

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

6157 ty' <- addUsingConstraints syn fc ty'

6258 ty' <- implicit syn n ty'

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

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

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

8177 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+

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

8384 let corec = case t of

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

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

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

834835

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−

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

839837 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+

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

841843 -- Elaborate where block

842844 ist <- getIState

src/Idris/REPL.hs+20

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

535535process h fn (CaseSplit n t)

536536 = do tms <- split n t

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

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

538539process h fn (CaseSplitAt updatefile l n)

539540 = do src <- runIO $ readFile fn

540541 res <- splitOnLine l n fn

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

567568 getIndent i n [] = 0

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

569570 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

570590process h fn (AddMissing updatefile l n)

571591 = do src <- runIO $ readFile fn

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

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

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

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

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

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

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