git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into Reader
commit5b1421f002b4f9de6825344daf0d39d901dd565e authorNiklas Larsson <metaniklas@gmail.com> dateSun 25 Jun 2017, 18:00 (9 years ago) parent292fb31c1329d7
13 files changed+146−79
compare with master
unifiedsplit
CHANGELOG.md+16 libs/base/Data/List/Views.idr+15−19 libs/base/Data/Nat/Views.idr+8−12 libs/base/Data/Vect/Views.idr+9−9 libs/contrib/Text/Parser.idr+1−1 libs/prelude/Prelude/WellFounded.idr+54−22 src/Idris/Interactive.hs+9−9 src/Idris/Package/Parser.hs+16−5 src/Util/System.hs+10 stack-shell.nix+1−1 stack.yaml+1−1 test/pkg001/expected+3 test/pkg001/run+3
CHANGELOG.md+16
@@ -9,6 +9,22 @@
99 + Added `MonadTrans` for `RWST`.
1010+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
1111 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
12++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
13+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
14+
15++ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
16+ mapping from `a` to `Nat`. For example, there is an implementation for lists,
17+ where `size = length`.
18+
19+ The function `sizeAccessible` then proves well-foundedness of the relation
20+ `Smaller x y = LT (size x) (size y)`, which allows us to use strong
21+ induction conveniently with any type that implements `Sized`.
22+
23+ In practice, this allows us to write functions that recurse not only on
24+ direct subterms of their arguments but on any value
25+ with a (strictly) smaller `size`.
26+
27+ A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
1228
1329## Tool Updates
1430
libs/base/Data/List/Views.idr+15−19
@@ -61,22 +61,18 @@ data SplitRec : List a -> Type where
6161 (lrec : Lazy (SplitRec lefts)) ->
6262 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
6363
64−total
65−splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
66− SplitRec xs
67−splitRecFix xs srec with (split xs)
68− splitRecFix [] srec | SplitNil = SplitRecNil
69− splitRecFix [x] srec | SplitOne = SplitRecOne
70− splitRecFix (x :: (ys ++ (y :: zs))) srec | SplitPair
71− = let left = srec (x :: ys) (smallerLeft ys y zs)
72− right = srec (y :: zs) (smallerRight ys zs) in
73− SplitRecPair left right
74−
7564||| Covering function for the `SplitRec` view
7665||| Constructs the view in O(n lg n)
7766export total
7867splitRec : (xs : List a) -> SplitRec xs
79−splitRec xs = accInd splitRecFix xs (smallerAcc xs)
68+splitRec xs with (sizeAccessible xs)
69+ splitRec xs | acc with (split xs)
70+ splitRec [] | acc | SplitNil = SplitRecNil
71+ splitRec [x] | acc | SplitOne = SplitRecOne
72+ splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair
73+ = SplitRecPair
74+ (splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
75+ (splitRec (z :: zs) | acc _ (smallerRight ys zs))
8076
8177||| View for traversing a list backwards
8278public export
@@ -105,21 +101,21 @@ data Filtered : (a -> a -> Bool) -> List a -> Type where
105101 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
106102 Filtered p (x :: xs)
107103
108−filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => p y x) xs) (x :: xs)
104+filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => p y x) xs) (x :: xs)
109105filteredLOK p x xs = LTESucc (filterSmaller xs)
110106
111−filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => not (p y x)) xs) (x :: xs)
107+filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => not (p y x)) xs) (x :: xs)
112108filteredROK p x xs = LTESucc (filterSmaller xs)
113109
114110||| Covering function for the `Filtered` view
115111||| Constructs the view in O(n lg n)
116112export
117113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (smallerAcc inp)
119− filtered p [] | with_pat = FNil
120− filtered p (x :: xs) | (Access xsrec)
121− = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
122− (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs))
114+filtered p inp with (sizeAccessible inp)
115+ filtered p [] | _ = FNil
116+ filtered p (x :: xs) | Access acc
117+ = FRec (filtered p (filter (\y => p y x) xs) | acc _ (filteredLOK p x xs))
118+ (filtered p (filter (\y => not (p y x)) xs) | acc _ (filteredROK p x xs))
123119
124120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
125121lenImpossible {n = Z} _ Refl impossible
libs/base/Data/Nat/Views.idr+8−12
@@ -22,17 +22,13 @@ half (S k) with (half k)
2222 HalfEven {n=S n}
2323 half (S (n + n)) | HalfEven = HalfOdd
2424
25−halfRecFix : (n : Nat) -> ((m : Nat) -> LT m n -> HalfRec m) -> HalfRec n
26−halfRecFix Z hrec = HalfRecZ
27−halfRecFix (S k) hrec with (half k)
28− halfRecFix (S (S (n + n))) hrec | HalfOdd
29− = rewrite plusSuccRightSucc (S n) n in
30− HalfRecEven (hrec (S n) (LTESucc (LTESucc (lteAddRight _))))
31− halfRecFix (S (n + n)) hrec | HalfEven
32− = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
33−
34−||| Covering function for the `HalfRec` view
3525export
3626halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAccessible n)
38−
27+halfRec n with (sizeAccessible n)
28+ halfRec Z | acc = HalfRecZ
29+ halfRec (S n) | acc with (half n)
30+ halfRec' (S (S (k + k))) | Access acc | HalfOdd
31+ = rewrite plusSuccRightSucc (S k) k
32+ in HalfRecEven (halfRec' (S k) | acc (S k) (LTESucc (LTESucc (lteAddRight _))))
33+ halfRec' (S (k + k)) | Access acc | HalfEven
34+ = HalfRecOdd (halfRec' k | acc k (LTESucc (lteAddRight _)))
libs/base/Data/Vect/Views.idr+9−9
@@ -61,23 +61,23 @@ data SplitRec : Vect n a -> Type where
6161 (lrec : Lazy (SplitRec xs)) ->
6262 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
6363
64−smallerPlus : LTE (S (S m)) (S (plus m (S k)))
65−smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
64+smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
65+smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
6666 (LTESucc (LTESucc (lteAddRight _)))
6767
68−smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
69−smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
68+smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
69+smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
7070 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
7171
7272||| Covering function for the `SplitRec` view
7373||| Constructs the view in O(n lg n)
7474export
7575splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (ltAccessible n)
76+splitRec {n} input with (sizeAccessible n)
7777 splitRec input | acc with (split input)
7878 splitRec [] | acc | SplitNil = SplitRecNil
7979 splitRec [x] | acc | SplitOne = SplitRecOne
80− splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
81− = let left = splitRec (x :: xs) | rec _ smallerPlus
82− right = splitRec (y :: ys) | rec _ smallerPlus' in
83− SplitRecPair left right
80+ splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
81+ = SplitRecPair
82+ (splitRec (x :: xs) | acc _ smallerPlusL)
83+ (splitRec (y :: ys) | acc _ smallerPlusR)
libs/contrib/Text/Parser.idr+1−1
@@ -113,7 +113,7 @@ shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
113113doParse : {c : Bool} ->
114114 (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
115115 ParseResult xs c ty
116−doParse com xs act with (smallerAcc xs)
116+doParse com xs act with (sizeAccessible xs)
117117 doParse com xs (Empty val) | sml = EmptyRes com val xs
118118 doParse com [] (Fail str) | sml = Failure com str []
119119 doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
libs/prelude/Prelude/WellFounded.idr+54−22
@@ -85,28 +85,60 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8585 (x : a) -> P x
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
88−-- Some basic useful relations
88+||| Interface of types with sized values.
89+||| The size is used for proofs of termination via accessibility.
90+|||
91+||| @ a the type whose elements can be mapped to Nat
92+interface Sized a where
93+ size : a -> Nat
8994
90−||| LT is a well-founded relation on numbers
91−ltAccessible : (n : Nat) -> Accessible LT n
92−ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
93− where
94− ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
95− ltAccessible' Z x = absurd x
96− ltAccessible' (S k) (LTESucc x)
97− = Access (\val, p => ltAccessible' k (lteTransitive p x))
98−
99−-- First list is smaller than the second
100−smaller : List a -> List a -> Type
101−smaller xs ys = LT (length xs) (length ys)
102−
103−||| `smaller` is a well-founded relation on lists
104−smallerAcc : (xs : List a) -> Accessible WellFounded.smaller xs
105−smallerAcc xs = Access (\v, prf => smallerAcc' {xs'=v} xs prf)
106− where
107− smallerAcc' : (ys : List a) -> smaller xs' ys -> Accessible smaller xs'
108− smallerAcc' [] x = absurd x
109− smallerAcc' (y :: ys) (LTESucc x)
110− = Access (\val, p => smallerAcc' ys (lteTransitive p x))
95+Smaller : Sized a => a -> a -> Type
96+Smaller x y = size x `LT` size y
11197
98+SizeAccessible : Sized a => a -> Type
99+SizeAccessible = Accessible Smaller
112100
101+||| Proof of well-foundedness of `Smaller`.
102+||| Constructs accessibility for any given element of `a`, provided `Sized a`.
103+sizeAccessible : Sized a => (x : a) -> SizeAccessible x
104+sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
105+ where
106+ -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107+ f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
108+ -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
109+ f Z acc y pf = absurd pf
110+ f (S n) (Access acc) y (LTESucc yLEx)
111+ = Access (\z, zLTy =>
112+ f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
113+ )
114+
115+ ||| LT is a well-founded relation on numbers
116+ ltAccessible : (n : Nat) -> Accessible LT n
117+ ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
118+ where
119+ ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
120+ ltAccessible' Z x = absurd x
121+ ltAccessible' (S k) (LTESucc x)
122+ = Access (\val, p => ltAccessible' k (lteTransitive p x))
123+
124+||| Strong induction principle for sized types.
125+sizeInd : Sized a
126+ => {P : a -> Type}
127+ -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
128+ -> (z : a)
129+ -> P z
130+sizeInd step z = accInd step z (sizeAccessible z)
131+
132+||| Strong recursion principle for sized types.
133+sizeRec : Sized a
134+ => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
135+ -> (z : a)
136+ -> b
137+sizeRec step z = accRec step z (sizeAccessible z)
138+
139+
140+implementation Sized Nat where
141+ size = \x => x
142+
143+implementation Sized (List a) where
144+ size = length
src/Idris/Interactive.hs+9−9
@@ -37,7 +37,7 @@ import System.IO
3737
3838caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
3939caseSplitAt fn updatefile l n
40− = do src <- runIO $ readSource fn
40+ = do src <- runIO $ readSourceStrict fn
4141 (ok, res) <- splitOnLine l n fn
4242 logLvl 1 (showSep "\n" (map show res))
4343 let (before, (ap : later)) = splitAt (l-1) (lines src)
@@ -61,7 +61,7 @@ addClauseFrom fn updatefile l n = do
6161 case metavars of
6262 Nothing -> addMissing fn updatefile l n
6363 Just _ -> do
64− src <- runIO $ readSource fn
64+ src <- runIO $ readSourceStrict fn
6565 let (before, tyline : later) = splitAt (l-1) (lines src)
6666 let indent = getIndent 0 (show n) tyline
6767 cl <- getClause l fulln n fn
@@ -88,7 +88,7 @@ addClauseFrom fn updatefile l n = do
8888
8989addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
9090addProofClauseFrom fn updatefile l n
91− = do src <- runIO $ readSource fn
91+ = do src <- runIO $ readSourceStrict fn
9292 let (before, tyline : later) = splitAt (l-1) (lines src)
9393 let indent = getIndent 0 (show n) tyline
9494 cl <- getProofClause l n fn
@@ -109,7 +109,7 @@ addProofClauseFrom fn updatefile l n
109109
110110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111111addMissing fn updatefile l n
112− = do src <- runIO $ readSource fn
112+ = do src <- runIO $ readSourceStrict fn
113113 let (before, tyline : later) = splitAt (l-1) (lines src)
114114 let indent = getIndent tyline
115115 i <- getIState
@@ -127,7 +127,7 @@ addMissing fn updatefile l n
127127 ++ extras
128128 ++ (if null extras then "" else "\n")
129129 ++ unlines rest)
130− runIO $ copyFile fb fn
130+ runIO $ (length src `seq` copyFile fb fn)
131131 else iPrintResult extras
132132 where showPat = show . stripNS
133133 stripNS tm = mapPT dens tm where
@@ -160,7 +160,7 @@ addMissing fn updatefile l n
160160
161161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
162162makeWith fn updatefile l n = do
163− src <- runIO $ readSource fn
163+ src <- runIO $ readSourceStrict fn
164164 i <- getIState
165165 indentWith <- getIndentWith
166166 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -184,7 +184,7 @@ makeWith fn updatefile l n = do
184184-- block, using a _ for the scrutinee
185185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
186186makeCase fn updatefile l n
187− = do src <- runIO $ readSource fn
187+ = do src <- runIO $ readSourceStrict fn
188188 let (before, tyline : later) = splitAt (l-1) (lines src)
189189 let newcase = addCaseSkel (show n) tyline
190190
@@ -224,7 +224,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->
224224doProofSearch fn updatefile rec l n hints Nothing
225225 = doProofSearch fn updatefile rec l n hints (Just 20)
226226doProofSearch fn updatefile rec l n hints (Just depth)
227− = do src <- runIO $ readSource fn
227+ = do src <- runIO $ readSourceStrict fn
228228 let (before, tyline : later) = splitAt (l-1) (lines src)
229229 ctxt <- getContext
230230 mn <- case lookupNames n ctxt of
@@ -319,7 +319,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"
319319
320320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
321321makeLemma fn updatefile l n
322− = do src <- runIO $ readSource fn
322+ = do src <- runIO $ readSourceStrict fn
323323 let (before, tyline : later) = splitAt (l-1) (lines src)
324324
325325 -- if the name is in braces, rather than preceded by a ?, treat it
src/Idris/Package/Parser.hs+16−5
@@ -24,7 +24,9 @@ import Control.Applicative
2424import Control.Monad.State.Strict
2525import Data.List (union)
2626import Data.Maybe (fromJust, isNothing)
27−import System.FilePath (isValid, takeFileName)
27+import System.Directory (doesFileExist)
28+import System.Exit
29+import System.FilePath (isValid, takeExtension, takeFileName)
2830import qualified Text.PrettyPrint.ANSI.Leijen as PP
2931import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,
3032 whiteSpace)
@@ -58,10 +60,19 @@ instance TokenParsing PParser where
5860
5961parseDesc :: FilePath -> IO PkgDesc
6062parseDesc fp = do
61− p <- readFile fp
62− case runparser pPkg defaultPkg fp p of
63− Failure (ErrInfo err _) -> fail (show $ PP.plain err)
64− Success x -> return x
63+ when (not $ takeExtension fp == ".ipkg") $ do
64+ putStrLn $ unwords ["The presented iPKG file does not have a '.ipkg' extension:", show fp]
65+ exitWith (ExitFailure 1)
66+ res <- doesFileExist fp
67+ if res
68+ then do
69+ p <- readFile fp
70+ case runparser pPkg defaultPkg fp p of
71+ Failure (ErrInfo err _) -> fail (show $ PP.plain err)
72+ Success x -> return x
73+ else do
74+ putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]
75+ exitWith (ExitFailure 1)
6576
6677pPkg :: PParser PkgDesc
6778pPkg = do
src/Util/System.hs+10
@@ -14,6 +14,7 @@ module Util.System( tempfile
1414 , writeSource
1515 , writeSourceText
1616 , readSource
17+ , readSourceStrict
1718 , setupBundledCC
1819 , isATTY
1920 ) where
@@ -60,6 +61,15 @@ readSource f = do h <- openFile f ReadMode
6061 hSetEncoding h utf8
6162 hGetContents h
6263
64+-- | Read a source file, make sure that the it all has been read before exiting the function.
65+-- | This is useful when we want to write the file again and need it to be closed.
66+readSourceStrict :: FilePath -> IO String
67+readSourceStrict f = withFile f ReadMode $
68+ \h -> do
69+ hSetEncoding h utf8
70+ src <- hGetContents h
71+ length src `seq` return src
72+
6373-- | Write a source file, same as writeFile except the encoding is set to utf-8
6474writeSource :: FilePath -> String -> IO ()
6575writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
22
33let
44 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-8_06.ghc;
5+ resolver = haskell.packages.lts-8_18.ghc;
66
77 native_libs = [
88 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-8.06
1+resolver: lts-8.18
22
33packages:
44 - location: .
test/pkg001/expected+3
@@ -18,3 +18,6 @@ builtin
1818Elaborating type decl Main.main[]
1919Elaborating clause Main.main
2020Rechecking for positivity []
21+The presented iPKG file does not have a '.ipkg' extension: "malformed-package-name"
22+The presented iPKG file does not exist: "non-existent-package.ipkg"
23+The presented iPKG file does not have a '.ipkg' extension: "non-existent-package-with-malformed-name"
test/pkg001/run+3
@@ -3,3 +3,6 @@ ${IDRIS:-idris} $@ --build test-pkg.ipkg
33rm -f *.ibc
44${IDRIS:-idris} $@ --build test-pkg.ipkg --quiet
55${IDRIS:-idris} $@ --build test-pkg.ipkg --logging-categories "elab" --log 1
6+${IDRIS:-idris} $@ --build malformed-package-name
7+${IDRIS:-idris} $@ --build non-existent-package.ipkg
8+${IDRIS:-idris} $@ --build non-existent-package-with-malformed-name