idris 0.9.1 → 0.9.2
raw patch · 31 files changed
+1610/−481 lines, 31 filesdep ~epicsetup-changed
Dependency ranges changed: epic
Files
- Setup.hs +37/−26
- idris.cabal +2/−2
- lib/Makefile +1/−1
- lib/builtins.idr +10/−3
- lib/checkall.idr +2/−0
- lib/prelude.idr +12/−1
- lib/prelude/algebra.idr +246/−21
- lib/prelude/complex.idr +65/−0
- lib/prelude/heap.idr +183/−0
- lib/prelude/list.idr +116/−45
- lib/prelude/nat.idr +200/−115
- lib/prelude/tactics.idr +4/−0
- lib/prelude/vect.idr +276/−30
- src/Core/CaseTree.hs +3/−3
- src/Core/Constraints.hs +6/−3
- src/Core/Elaborate.hs +15/−1
- src/Core/Evaluate.hs +163/−89
- src/Core/ProofState.hs +1/−1
- src/Core/TT.hs +10/−0
- src/Idris/AbsSyntax.hs +59/−16
- src/Idris/Compiler.hs +7/−0
- src/Idris/Coverage.hs +1/−54
- src/Idris/DSL.hs +3/−0
- src/Idris/ElabDecls.hs +46/−26
- src/Idris/ElabTerm.hs +75/−21
- src/Idris/IBC.hs +31/−7
- src/Idris/Parser.hs +23/−13
- src/Idris/Primitives.hs +5/−0
- src/Idris/Prover.hs +1/−1
- src/Idris/REPL.hs +4/−2
- tutorial/examples/interp.idr +3/−0
Setup.hs view
@@ -1,42 +1,53 @@ import Distribution.Simple import Distribution.Simple.InstallDirs as I import Distribution.Simple.LocalBuildInfo as L+import qualified Distribution.Simple.Setup as S+import qualified Distribution.Simple.Program as P import Distribution.PackageDescription import System.Exit+import System.FilePath ((</>)) import System.Process -- After Idris is built, we need to check and install the prelude and other libs -system' cmd = do - exit <- system cmd- case exit of- ExitSuccess -> return ()- ExitFailure _ -> exitWith exit--postCleanLib args flags desc _- = system' "make -C lib clean"+make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make" -addPrefix pfx var c = "export " ++ var ++ "=" ++ show pfx ++ "/" ++ c ++ ":$" ++ var+cleanStdLib verbosity+ = make verbosity [ "-C", "lib", "clean" ] -postInstLib args flags desc local- = do let pkg = localPkgDescr local- let penv = packageTemplateEnv (package pkg)- let cenv = compilerTemplateEnv (compilerId (compiler local))- let dirs_pkg = substituteInstallDirTemplates penv (installDirTemplates local)- let dirs = substituteInstallDirTemplates cenv dirs_pkg- let bind = fromPathTemplate (bindir dirs)- let progPart t = L.substPathTemplate (packageId desc) local (t local)- let progpfx = progPart progPrefix- let progsfx = progPart progSuffix- let PackageName pkgname = (packageName desc)- let icmd = bind ++ "/" ++ progpfx ++ pkgname ++ progsfx- let idir = fromPathTemplate (datadir dirs) ++ "/" ++ - fromPathTemplate (datasubdir dirs)+installStdLib pkg local verbosity copy+ = do let dirs = L.absoluteInstallDirs pkg local copy+ let idir = datadir dirs+ let icmd = ".." </> buildDir local </> "idris" </> "idris" putStrLn $ "Installing libraries in " ++ idir- system' $ "make -C lib install TARGET=" ++ idir ++ " IDRIS=" ++ icmd + make verbosity+ [ "-C", "lib", "install"+ , "TARGET=" ++ idir+ , "IDRIS=" ++ icmd+ ] -main = defaultMainWithHooks (simpleUserHooks { postInst = postInstLib,- postClean = postCleanLib })+checkStdLib local verbosity+ = do let icmd = ".." </> buildDir local </> "idris" </> "idris"+ putStrLn $ "Building libraries..."+ make verbosity+ [ "-C", "lib", "check"+ , "IDRIS=" ++ icmd+ ]++-- Install libraries during both copy and install+-- See http://hackage.haskell.org/trac/hackage/ticket/718+main = defaultMainWithHooks $ simpleUserHooks+ { postCopy = \ _ flags pkg lbi -> do+ installStdLib pkg lbi (S.fromFlag $ S.copyVerbosity flags)+ (S.fromFlag $ S.copyDest flags)+ , postInst = \ _ flags pkg lbi -> do+ installStdLib pkg lbi (S.fromFlag $ S.installVerbosity flags)+ NoCopyDest+ , postClean = \ _ flags _ _ -> do+ cleanStdLib (S.fromFlag $ S.cleanVerbosity flags)+ , postBuild = \ _ flags _ lbi -> do+ checkStdLib lbi (S.fromFlag $ S.buildVerbosity flags)+ }
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.1+Version: 0.9.2 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -67,7 +67,7 @@ Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline, containers, process, transformers, filepath, directory,- binary, bytestring, epic>=0.9.2+ binary, bytestring, epic>=0.9.3 Extensions: MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TemplateHaskell
lib/Makefile view
@@ -20,6 +20,6 @@ rm -f control/monad/*.ibc linecount: .PHONY- wc -l *.idr network/*.idr prelude/*.idr+ wc -l *.idr network/*.idr prelude/*.idr control/monad/*.idr .PHONY:
lib/builtins.idr view
@@ -21,6 +21,12 @@ lazy : a -> a lazy x = x -- compiled specially +malloc : Int -> a -> a+malloc size x = x -- compiled specially++trace_malloc : a -> a+trace_malloc x = x -- compiled specially+ believe_me : a -> b -- compiled specially as id, use with care! believe_me x = prim__believe_me _ _ x @@ -186,14 +192,12 @@ else compare xr yr -class (Eq a, Ord a) => Num a where +class Eq a => Num a where (+) : a -> a -> a (-) : a -> a -> a (*) : a -> a -> a abs : a -> a- abs x = if (x < 0) then (-x) else x- fromInteger : Int -> a @@ -204,6 +208,7 @@ (*) = prim__mulInt fromInteger = id+ abs x = if x<0 then -x else x instance Num Integer where @@ -211,6 +216,7 @@ (-) = prim__subBigInt (*) = prim__mulBigInt + abs x = if x<0 then -x else x fromInteger = prim__intToBigInt @@ -219,6 +225,7 @@ (-) = prim__subFloat (*) = prim__mulFloat + abs x = if x<0 then -x else x fromInteger = prim__intToFloat
lib/checkall.idr view
@@ -20,6 +20,8 @@ import prelude.vect import prelude.strings import prelude.char+import prelude.heap+import prelude.complex import network.cgi
lib/prelude.idr view
@@ -143,6 +143,9 @@ atan : Float -> Float atan x = prim__floatATan x +atan2 : Float -> Float -> Float+atan2 y x = atan (y/x)+ sqrt : Float -> Float sqrt x = prim__floatSqrt x @@ -154,14 +157,22 @@ ---- Ranges -count : Num a => a -> a -> a -> List a+count : (Ord a, Num a) => a -> a -> a -> List a count a inc b = if a <= b then a :: count (a + inc) inc b else [] +countFrom : (Ord a, Num a) => a -> a -> List a+countFrom a inc = a :: lazy (countFrom (a + inc) inc)+ syntax "[" [start] ".." [end] "]" = count start 1 end syntax "[" [start] "," [next] ".." [end] "]" = count start (next - start) end ++syntax "[" [start] "..]" + = countFrom start 1+syntax "[" [start] "," [next] "..]" + = countFrom start (next - start) ---- More utilities
lib/prelude/algebra.idr view
@@ -1,32 +1,257 @@-module algebra+module prelude.algebra import builtins --- Sets with an associative binary operation--- Must satisfy:--- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c+-- XXX: change?+infixl 6 <->+infixl 6 <+>+infixl 6 <*>++%access public++--------------------------------------------------------------------------------+-- A modest class hierarchy+--------------------------------------------------------------------------------++-- Sets equipped with a single binary operation that is associative. Must+-- satisfy the following laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c class Semigroup a where- (<*>) : a -> a -> a+ (<+>) : a -> a -> a --- Sets with an associative binary operation and a neutral element--- Must satisfy:--- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c--- forall a. neutral <*> a = a <*> neutral = a+class Semigroup a => VerifiedSemigroup a where+ semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r++-- Sets equipped with a single binary operation that is associative, along with+-- a neutral element for that binary operation. Must satisfy the following+-- laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+-- Neutral for <+>:+-- forall a, a <+> neutral == a+-- forall a, neutral <+> a == a class Semigroup a => Monoid a where neutral : a --- Sets with an associative binary operation, a neutral element, as well as--- inverses--- Must satisfy:--- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c--- forall a. neutral <*> a = a <*> neutral = a--- forall a. inverse a <*> a = a <*> inverse = neutral--- forall a. inverse (inverse a) = a+class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where+ monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l+ monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r++-- Sets equipped with a single binary operation that is associative, along with+-- a neutral element for that binary operation and inverses for all elements.+-- Must satisfy the following laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+-- Neutral for <+>:+-- forall a, a <+> neutral == a+-- forall a, neutral <+> a == a+-- Inverse for <+>:+-- forall a, a <+> inverse a == neutral+-- forall a, inverse a <+> a == neutral class Monoid a => Group a where inverse : a -> a- (<->) : a -> a -> a --- XXX: to add:--- ring, field, euclidean domain, abelian group, vector spaces, etc.?--- do we want proofs of properties in the type classes?--- derived classes, some mechanism for multiple e.g. monoids on same type+class (VerifiedMonoid a, Group a) => VerifiedGroup a where+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral++(<->) : Group a => a -> a -> a+(<->) left right = left <+> (inverse right)++-- Sets equipped with a single binary operation that is associative and+-- commutative, along with a neutral element for that binary operation and+-- inverses for all elements. Must satisfy the following laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+-- Commutativity of <+>:+-- forall a b, a <+> b == b <+> a+-- Neutral for <+>:+-- forall a, a <+> neutral == a+-- forall a, neutral <+> a == a+-- Inverse for <+>:+-- forall a, a <+> inverse a == neutral+-- forall a, inverse a <+> a == neutral+class Group a => AbelianGroup a where { }++class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where+ abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l++-- Sets equipped with two binary operations, one associative and commutative+-- supplied with a neutral element, and the other associative, with+-- distributivity laws relating the two operations. Must satisfy the following+-- laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+-- Commutativity of <+>:+-- forall a b, a <+> b == b <+> a+-- Neutral for <+>:+-- forall a, a <+> neutral == a+-- forall a, neutral <+> a == a+-- Inverse for <+>:+-- forall a, a <+> inverse a == neutral+-- forall a, inverse a <+> a == neutral+-- Associativity of <*>:+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c+-- Distributivity of <*> and <->:+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)+class AbelianGroup a => Ring a where+ (<*>) : a -> a -> a++class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where+ ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r+ ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)++-- Sets equipped with two binary operations, one associative and commutative+-- supplied with a neutral element, and the other associative supplied with a+-- neutral element, with distributivity laws relating the two operations. Must+-- satisfy the following laws:+-- Associativity of <+>:+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+-- Commutativity of <+>:+-- forall a b, a <+> b == b <+> a+-- Neutral for <+>:+-- forall a, a <+> neutral == a+-- forall a, neutral <+> a == a+-- Inverse for <+>:+-- forall a, a <+> inverse a == neutral+-- forall a, inverse a <+> a == neutral+-- Associativity of <*>:+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c+-- Neutral for <*>:+-- forall a, a <*> unity == a+-- forall a, unity <*> a == a+-- Distributivity of <*> and <->:+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)+class Ring a => RingWithUnity a where+ unity : a++class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where+ ringWithUnityIsUnityL : (l : a) -> l <*> unity = l+ ringWithUnityIsUnityR : (r : a) -> unity <*> r = r++-- Sets equipped with a binary operation that is commutative, associative and+-- idempotent. Must satisfy the following laws:+-- Associativity of join:+-- forall a b c, join a (join b c) == join (join a b) c+-- Commutativity of join:+-- forall a b, join a b == join b a+-- Idempotency of join:+-- forall a, join a a == a+-- Join semilattices capture the notion of sets with a "least upper bound".+class JoinSemilattice a where+ join : a -> a -> a++class JoinSemilattice a => VerifiedJoinSemilattice a where+ joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e++-- Sets equipped with a binary operation that is commutative, associative and+-- idempotent. Must satisfy the following laws:+-- Associativity of meet:+-- forall a b c, meet a (meet b c) == meet (meet a b) c+-- Commutativity of meet:+-- forall a b, meet a b == meet b a+-- Idempotency of meet:+-- forall a, meet a a == a+-- Meet semilattices capture the notion of sets with a "greatest lower bound".+class MeetSemilattice a where+ meet : a -> a -> a++class MeetSemilattice a => VerifiedMeetSemilattice a where+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e++-- Sets equipped with a binary operation that is commutative, associative and+-- idempotent and supplied with a neutral element. Must satisfy the following+-- laws:+-- Associativity of join:+-- forall a b c, join a (join b c) == join (join a b) c+-- Commutativity of join:+-- forall a b, join a b == join b a+-- Idempotency of join:+-- forall a, join a a == a+-- Bottom:+-- forall a, join a bottom == bottom+-- Join semilattices capture the notion of sets with a "least upper bound"+-- equipped with a "bottom" element.+class JoinSemilattice a => BoundedJoinSemilattice a where+ bottom : a++class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where+ boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom++-- Sets equipped with a binary operation that is commutative, associative and+-- idempotent and supplied with a neutral element. Must satisfy the following+-- laws:+-- Associativity of meet:+-- forall a b c, meet a (meet b c) == meet (meet a b) c+-- Commutativity of meet:+-- forall a b, meet a b == meet b a+-- Idempotency of meet:+-- forall a, meet a a == a+-- Top:+-- forall a, meet a top == top+-- Meet semilattices capture the notion of sets with a "greatest lower bound"+-- equipped with a "top" element.+class MeetSemilattice a => BoundedMeetSemilattice a where+ top : a++class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where+ boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top++-- Sets equipped with two binary operations that are both commutative,+-- associative and idempotent, along with absorbtion laws for relating the two+-- binary operations. Must satisfy the following:+-- Associativity of meet and join:+-- forall a b c, meet a (meet b c) == meet (meet a b) c+-- forall a b c, join a (join b c) == join (join a b) c+-- Commutativity of meet and join:+-- forall a b, meet a b == meet b a+-- forall a b, join a b == join b a+-- Idempotency of meet and join:+-- forall a, meet a a == a+-- forall a, join a a == a+-- Absorbtion laws for meet and join:+-- forall a b, meet a (join a b) == a+-- forall a b, join a (meet a b) == a+class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }++class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where+ latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l+ latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l++-- Sets equipped with two binary operations that are both commutative,+-- associative and idempotent and supplied with neutral elements, along with+-- absorbtion laws for relating the two binary operations. Must satisfy the+-- following:+-- Associativity of meet and join:+-- forall a b c, meet a (meet b c) == meet (meet a b) c+-- forall a b c, join a (join b c) == join (join a b) c+-- Commutativity of meet and join:+-- forall a b, meet a b == meet b a+-- forall a b, join a b == join b a+-- Idempotency of meet and join:+-- forall a, meet a a == a+-- forall a, join a a == a+-- Absorbtion laws for meet and join:+-- forall a b, meet a (join a b) == a+-- forall a b, join a (meet a b) == a+-- Neutral for meet and join:+-- forall a, meet a top == top+-- forall a, join a bottom == bottom+class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }++class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }+ + +-- XXX todo:+-- Fields and vector spaces.+-- Structures where "abs" make sense.+-- Euclidean domains, etc.+-- Where to put fromInteger and fromRational?
+ lib/prelude/complex.idr view
@@ -0,0 +1,65 @@+module prelude.complex++import builtins+++------------------------------ Rectangular form ++infix 6 :++data Complex a = (:+) a a++realPart : Complex a -> a+realPart (r:+i) = r++imagPart : Complex a -> a+imagPart (r:+i) = i++instance Eq a => Eq (Complex a) where+ (==) a b = realPart a == realPart b && imagPart a == imagPart b++instance Show a => Show (Complex a) where+ show (r:+i) = "("++show r++":+"++show i++")"++++-- when we have a type class 'Fractional' (which contains Float and Double),+-- we can do:+{-+instance Fractional a => Fractional (Complex a) where+ (/) (a:+b) (c:+d) = let+ real = (a*c+b*d)/(c*c+d*d)+ imag = (b*c-a*d)/(c*c+d*d)+ in+ (real:+imag)+-}++++------------------------------ Polarform++mkPolar : Float -> Float -> Complex Float+mkPolar radius angle = radius * cos angle :+ radius * sin angle++cis : Float -> Complex Float+cis angle = cos angle :+ sin angle++magnitude : Complex Float -> Float+magnitude (r:+i) = sqrt (r*r+i*i)++phase : Complex Float -> Float+phase (x:+y) = atan2 y x+++------------------------------ Conjugate++conjugate : Num a => Complex a -> Complex a+conjugate (r:+i) = (r :+ (0-i))++-- We can't do "instance Num a => Num (Complex a)" because+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float+instance Num (Complex Float) where+ (+) (a:+b) (c:+d) = ((a+b):+(c+d))+ (-) (a:+b) (c:+d) = ((a-b):+(c-d))+ (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))+ fromInteger x = (fromInteger x:+0)+ abs (a:+b) = (magnitude (a:+b):+0)
+ lib/prelude/heap.idr view
@@ -0,0 +1,183 @@+--------------------------------------------------------------------------------+-- Okasaki-style maxiphobic heaps. See the paper:+-- ``Fun with binary heap trees'', Chris Okasaki, Fun of programming, 2003.+--------------------------------------------------------------------------------++module prelude.heap++import builtins++import prelude+import prelude.algebra+import prelude.list+import prelude.nat++%access public++abstract data MaxiphobicHeap : Set -> Set where+ Empty : MaxiphobicHeap a+ Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a++----------------------------------------- ---------------------------------------+-- Syntactic tests+--------------------------------------------------------------------------------++total isEmpty : MaxiphobicHeap a -> Bool+isEmpty Empty = True+isEmpty _ = False++total size : MaxiphobicHeap a -> Nat+size Empty = O+size (Node s l e r) = s++--------------------------------------------------------------------------------+-- Basic heaps+--------------------------------------------------------------------------------++total empty : MaxiphobicHeap a+empty = Empty++total singleton : a -> MaxiphobicHeap a+singleton e = Node 1 Empty e Empty++--------------------------------------------------------------------------------+-- Inserting items and merging heaps+--------------------------------------------------------------------------------++private orderBySize : MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a ->+ (MaxiphobicHeap a, MaxiphobicHeap a, MaxiphobicHeap a)+orderBySize left centre right =+ if size left == largest then+ (left, centre, right)+ else if size centre == largest then+ (centre, left, right)+ else+ (right, left, centre)+ where+ largest : Nat+ largest = maximum (size left) $ maximum (size centre) (size right)++merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a+merge Empty right = right+merge left Empty = left+merge (Node ls ll le lr) (Node rs rl re rr) =+ if le < re then+ let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in+ Node mergedSize largest le (merge b c)+ else+ let (largest, b, c) = orderBySize rl rr (Node ls ll le lr) in+ Node mergedSize largest re (merge b c)+ where+ mergedSize : Nat+ mergedSize = ls + rs++insert : Ord a => a -> MaxiphobicHeap a -> MaxiphobicHeap a+insert e = merge $ singleton e++--------------------------------------------------------------------------------+-- Heap operations+--------------------------------------------------------------------------------++findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a+findMinimum Empty p = ?findMinimumEmptyAbsurd+findMinimum (Node s l e r) p = e++deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a+deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd+deleteMinimum (Node s l e r) p = merge l r++--------------------------------------------------------------------------------+-- Conversions to and from lists (and a derived heap sorting algorithm)+--------------------------------------------------------------------------------++toList : Ord a => MaxiphobicHeap a -> List a+toList Empty = []+toList (Node s l e r) = toList' (Node s l e r) refl+ where+ toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a+ toList' heap p = findMinimum heap p :: (toList $ deleteMinimum heap p)++fromList : Ord a => List a -> MaxiphobicHeap a+fromList = foldr insert empty++sort : Ord a => List a -> List a+sort = prelude.heap.toList . prelude.heap.fromList++--------------------------------------------------------------------------------+-- Class instances+--------------------------------------------------------------------------------++instance Show a => Show (MaxiphobicHeap a) where+ show Empty = "Empty"+ show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"++instance Eq a => Eq (MaxiphobicHeap a) where+ Empty == Empty = True+ (Node ls ll le lr) == (Node rs rl re rr) =+ ls == rs && ll == rl && le == re && lr == rr+ _ == _ = False+ +instance Ord a => Semigroup (MaxiphobicHeap a) where+ (<+>) = merge++instance Ord a => Monoid (MaxiphobicHeap a) where+ neutral = empty++instance Ord a => JoinSemilattice (MaxiphobicHeap a) where+ join = merge++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++total absurdBoolDischarge : False = True -> _|_+absurdBoolDischarge p = replace {P = disjointTy} p ()+ where+ total disjointTy : Bool -> Set+ disjointTy False = ()+ disjointTy True = _|_++total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O+isEmptySizeZero Empty p = refl+isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd++--------------------------------------------------------------------------------+-- Proofs+--------------------------------------------------------------------------------++isEmptySizeZeroNodeAbsurd = proof {+ intros;+ refine FalseElim;+ refine absurdBoolDischarge;+ exact p;+}++findMinimumEmptyAbsurd = proof {+ intros;+ refine FalseElim;+ refine absurdBoolDischarge;+ rewrite p;+ trivial;+}++deleteMinimumEmptyAbsurd = proof {+ intros;+ refine FalseElim;+ refine absurdBoolDischarge;+ rewrite p;+ trivial;+}++--------------------------------------------------------------------------------+-- Debug+--------------------------------------------------------------------------------++{- XXX: poor performance when compiled, diverges when used in the REPL, but it+ does seem to work correctly!+main : IO ()+main = do+ _ <- print $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]+ _ <- print $ main.sort ["orange", "apple", "pear", "lime", "durian"]+ _ <- print $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]+ return ()+-}
lib/prelude/list.idr view
@@ -2,6 +2,7 @@ import builtins +import prelude.algebra import prelude.maybe import prelude.nat @@ -78,12 +79,12 @@ -------------------------------------------------------------------------------- take : Nat -> List a -> List a-take Z xs = []+take O xs = [] take (S n) [] = [] take (S n) (x::xs) = x :: take n xs drop : Nat -> List a -> List a-drop Z xs = xs+drop O xs = xs drop (S n) [] = [] drop (S n) (x::xs) = drop n xs @@ -108,6 +109,72 @@ (++) (x::xs) right = x :: (xs ++ right) --------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------++instance (Eq a) => Eq (List a) where+ (==) [] [] = True+ (==) (x::xs) (y::ys) =+ if x == y then+ xs == ys+ else+ False+ (==) _ _ = False+++instance Ord a => Ord (List a) where+ compare [] [] = EQ+ compare [] _ = LT+ compare _ [] = GT+ compare (x::xs) (y::ys) =+ if x /= y then+ compare x y+ else+ compare xs ys++instance Semigroup (List a) where+ (<+>) = (++)++instance Monoid (List a) where+ neutral = []++-- XXX: unification failure+-- instance VerifiedSemigroup (List a) where+-- semigroupOpIsAssociative = appendAssociative++--------------------------------------------------------------------------------+-- Zips and unzips+--------------------------------------------------------------------------------++zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->+ (length l = length r) -> List c+zipWith f [] [] p = []+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)++zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->+ (z : List c) -> (length x = length y) -> (length y = length z) -> List d+zipWith3 f [] [] [] p q = []+zipWith3 f (x::xs) (y::ys) (z::zs) p q =+ f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')++zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)+zip = zipWith (\x => \y => (x, y))++zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->+ (length y = length z) -> List (a, b, c)+zip3 = zipWith3 (\x => \y => \z => (x, y, z))++unzip : List (a, b) -> (List a, List b)+unzip [] = ([], [])+unzip ((l, r)::xs) with (unzip xs)+ | (lefts, rights) = (l::lefts, r::rights)++unzip3 : List (a, b, c) -> (List a, List b, List c)+unzip3 [] = ([], [], [])+unzip3 ((l, c, r)::xs) with (unzip3 xs)+ | (lefts, centres, rights) = (l::lefts, c::centres, r::rights)++-------------------------------------------------------------------------------- -- Maps -------------------------------------------------------------------------------- @@ -138,8 +205,12 @@ -- Special folds -------------------------------------------------------------------------------- +mconcat : Monoid a => List a -> a+mconcat = foldr (<+>) neutral+ concat : List (List a) -> List a-concat = foldr (++) []+concat [] = []+concat (x::xs) = x ++ concat xs concatMap : (a -> List b) -> List a -> List b concatMap f [] = []@@ -403,31 +474,33 @@ Just j => j :: catMaybes xs ----------------------------------------------------------------------------------- Instances+-- Properties -------------------------------------------------------------------------------- -instance (Eq a) => Eq (List a) where- (==) [] [] = True- (==) (a::restA) (b::restB) =- if a == b- then restA == restB- else False- (==) _ _ = False-+-- append+appendNilRightNeutral : (l : List a) ->+ l ++ [] = l+appendNilRightNeutral [] = refl+appendNilRightNeutral (x::xs) =+ let inductiveHypothesis = appendNilRightNeutral xs in+ ?appendNilRightNeutralStepCase -instance Ord a => Ord (List a) where- compare [] [] = EQ- compare [] _ = LT- compare _ [] = GT- compare (a::restA) (b::restB) =- if a /= b- then compare a b- else compare restA restB+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->+ l ++ (c ++ r) = (l ++ c) ++ r+appendAssociative [] c r = refl+appendAssociative (x::xs) c r =+ let inductiveHypothesis = appendAssociative xs c r in+ ?appendAssociativeStepCase ------------------------------------------------------------------------------------ Properties---------------------------------------------------------------------------------+-- length+lengthAppend : (left : List a) -> (right : List a) ->+ length (left ++ right) = length left + length right+lengthAppend [] right = refl+lengthAppend (x::xs) right =+ let inductiveHypothesis = lengthAppend xs right in+ ?lengthAppendStepCase +-- map mapPreservesLength : (f : a -> b) -> (l : List a) -> length (map f l) = length l mapPreservesLength f [] = refl@@ -449,20 +522,7 @@ let inductiveHypothesis = mapFusion f g xs in ?mapFusionStepCase -appendNilRightNeutral : (l : List a) ->- l ++ [] = l-appendNilRightNeutral [] = refl-appendNilRightNeutral (x::xs) =- let inductiveHypothesis = appendNilRightNeutral xs in- ?appendNilRightNeutralStepCase--appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->- (l ++ c) ++ r = l ++ (c ++ r)-appendAssociative [] c r = refl-appendAssociative (x::xs) c r =- let inductiveHypothesis = appendAssociative xs c r in- ?appendAssociativeStepCase-+-- hasAny hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) -> hasAnyBy p [] l = False hasAnyByNilFalse p [] = refl@@ -470,16 +530,9 @@ let inductiveHypothesis = hasAnyByNilFalse p xs in ?hasAnyByNilFalseStepCase -lengthAppend : (left : List a) -> (right : List a) ->- length (left ++ right) = length left + length right-lengthAppend [] right = refl-lengthAppend (x::xs) right =- let inductiveHypothesis = lengthAppend xs right in- ?lengthAppendStepCase- hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False hasAnyNilFalse l = ?hasAnyNilFalseBody-+ -------------------------------------------------------------------------------- -- Proofs --------------------------------------------------------------------------------@@ -539,6 +592,24 @@ mapPreservesLengthStepCase = proof { intros; rewrite inductiveHypothesis;+ trivial;+}++zipWithTailProof = proof {+ intros;+ rewrite (succInjective (length xs) (length ys) p);+ trivial;+}++zipWith3TailProof = proof {+ intros;+ rewrite (succInjective (length xs) (length ys) p);+ trivial;+}++zipWith3TailProof' = proof {+ intros;+ rewrite (succInjective (length ys) (length zs) q); trivial; }
lib/prelude/nat.idr view
@@ -15,11 +15,11 @@ -- Syntactic tests -------------------------------------------------------------------------------- -isZero : Nat -> Bool+total isZero : Nat -> Bool isZero O = True isZero (S n) = False -isSucc : Nat -> Bool+total isSucc : Nat -> Bool isSucc O = False isSucc (S n) = True @@ -27,24 +27,69 @@ -- Basic arithmetic functions -------------------------------------------------------------------------------- -plus : Nat -> Nat -> Nat+total plus : Nat -> Nat -> Nat plus O right = right plus (S left) right = S (plus left right) -mult : Nat -> Nat -> Nat+total mult : Nat -> Nat -> Nat mult O right = O mult (S left) right = plus right $ mult left right -minus : Nat -> Nat -> Nat+total minus : Nat -> Nat -> Nat minus O right = O minus left O = left minus (S left) (S right) = minus left right -power : Nat -> Nat -> Nat+total power : Nat -> Nat -> Nat power base O = S O power base (S exp) = mult base $ power base exp --------------------------------------------------------------------------------+-- Comparisons+--------------------------------------------------------------------------------++data LTE : Nat -> Nat -> Set where+ lteZero : LTE O right+ lteSucc : LTE left right -> LTE (S left) (S right)++total GTE : Nat -> Nat -> Set+GTE left right = LTE right left++total LT : Nat -> Nat -> Set+LT left right = LTE (S left) right++total GT : Nat -> Nat -> Set+GT left right = LT right left++total lte : Nat -> Nat -> Bool+lte O right = True+lte left O = False+lte (S left) (S right) = lte left right++total gte : Nat -> Nat -> Bool+gte left right = lte right left++total lt : Nat -> Nat -> Bool+lt left right = lte (S left) right++total gt : Nat -> Nat -> Bool+gt left right = lt right left++total minimum : Nat -> Nat -> Nat+minimum left right =+ if lte left right then+ left+ else+ right++total maximum : Nat -> Nat -> Nat+maximum left right =+ if lte left right then+ right+ else+ left++-------------------------------------------------------------------------------- -- Type class instances -------------------------------------------------------------------------------- @@ -68,21 +113,73 @@ (-) = minus (*) = mult - fromInteger = intToNat where+ abs x = x++ fromInteger = fromInteger'+ where %assert_total- intToNat : Int -> Nat- intToNat 0 = O- intToNat n = if (n > 0) then S (fromInteger (n-1)) else O+ fromInteger' : Int -> Nat+ fromInteger' 0 = O+ fromInteger' n =+ if (n > 0) then+ S (fromInteger' (n - 1))+ else+ O ------------------------------------------------------------------------------------ Division and modulus---------------------------------------------------------------------------------+record Multiplicative : Set where+ getMultiplicative : Nat -> Multiplicative +record Additive : Set where+ getAdditive : Nat -> Additive++instance Semigroup Multiplicative where+ (<+>) left right = getMultiplicative $ left' * right'+ where+ left' : Nat+ left' =+ case left of+ getMultiplicative m => m++ right' : Nat+ right' =+ case right of+ getMultiplicative m => m++instance Semigroup Additive where+ left <+> right = getAdditive $ left' + right'+ where+ left' : Nat+ left' =+ case left of+ getAdditive m => m++ right' : Nat+ right' =+ case right of+ getAdditive m => m++instance Monoid Multiplicative where+ neutral = getMultiplicative $ S O++instance Monoid Additive where+ neutral = getAdditive O++instance MeetSemilattice Nat where+ meet = minimum++instance JoinSemilattice Nat where+ join = maximum++instance Lattice Nat where { }++instance BoundedJoinSemilattice Nat where+ bottom = O+ -------------------------------------------------------------------------------- -- Auxilliary notions -------------------------------------------------------------------------------- -pred : Nat -> Nat+total pred : Nat -> Nat pred O = O pred (S n) = n @@ -90,9 +187,9 @@ -- Fibonacci and factorial -------------------------------------------------------------------------------- -fib : Nat -> Nat-fib O = 0-fib (S O) = 1+total fib : Nat -> Nat+fib O = O+fib (S O) = S O fib (S (S n)) = fib (S n) + fib n --------------------------------------------------------------------------------@@ -100,120 +197,103 @@ -------------------------------------------------------------------------------- ----------------------------------------------------------------------------------- Comparisons+-- Division and modulus -------------------------------------------------------------------------------- -data LTE : Nat -> Nat -> Set where- lteZero : LTE O right- lteSucc : LTE left right -> LTE (S left) (S right)--GTE : Nat -> Nat -> Set-GTE left right = LTE right left--LT : Nat -> Nat -> Set-LT left right = LTE (S left) right--GT : Nat -> Nat -> Set-GT left right = LT right left--lte : Nat -> Nat -> Bool-lte O right = True-lte left O = False-lte (S left) (S right) = lte left right--gte : Nat -> Nat -> Bool-gte left right = lte right left--lt : Nat -> Nat -> Bool-lt left right = lte (S left) right--gt : Nat -> Nat -> Bool-gt left right = lt right left--minimum : Nat -> Nat -> Nat-minimum left right =- if lte left right then- left- else- right+total mod : Nat -> Nat -> Nat+mod left O = left+mod left (S right) = mod' left left right+ where+ total mod' : Nat -> Nat -> Nat -> Nat+ mod' O centre right = centre+ mod' (S left) centre right =+ if lte centre right then+ centre+ else+ mod' left (centre - (S right)) right -maximum : Nat -> Nat -> Nat-maximum left right =- if lte left right then- right- else- left+total div : Nat -> Nat -> Nat+div left O = S left -- div by zero+div left (S right) = div' left left right+ where+ total div' : Nat -> Nat -> Nat -> Nat+ div' O centre right = O+ div' (S left) centre right =+ if lte centre right then+ O+ else+ S (div' left (centre - (S right)) right) -------------------------------------------------------------------------------- -- Properties -------------------------------------------------------------------------------- -- Succ-eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->+total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) -> S left = S right eqSucc left right refl = refl -succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->+total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) -> left = right succInjective left right refl = refl -- Plus-plusZeroLeftNeutral : (right : Nat) -> 0 + right = right+total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right plusZeroLeftNeutral right = refl -plusZeroRightNeutral : (left : Nat) -> left + 0 = left+total plusZeroRightNeutral : (left : Nat) -> left + 0 = left plusZeroRightNeutral O = refl plusZeroRightNeutral (S n) = let inductiveHypothesis = plusZeroRightNeutral n in ?plusZeroRightNeutralStepCase -plusSuccRightSucc : (left : Nat) -> (right : Nat) ->+total plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right) plusSuccRightSucc O right = refl plusSuccRightSucc (S left) right = let inductiveHypothesis = plusSuccRightSucc left right in ?plusSuccRightSuccStepCase -plusCommutative : (left : Nat) -> (right : Nat) ->+total plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left plusCommutative O right = ?plusCommutativeBaseCase plusCommutative (S left) right = let inductiveHypothesis = plusCommutative left right in ?plusCommutativeStepCase -plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left + (centre + right) = (left + centre) + right plusAssociative O centre right = refl plusAssociative (S left) centre right = let inductiveHypothesis = plusAssociative left centre right in ?plusAssociativeStepCase -plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->+total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) -> (p : left = right) -> left + c = right + c plusConstantRight left right c refl = refl -plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->+total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) -> (p : left = right) -> c + left = c + right plusConstantLeft left right c refl = refl -plusOneSucc : (right : Nat) -> 1 + right = S right+total plusOneSucc : (right : Nat) -> 1 + right = S right plusOneSucc n = refl -plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->+total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (p : left + right = left + right') -> right = right' plusLeftCancel O right right' p = ?plusLeftCancelBaseCase plusLeftCancel (S left) right right' p = let inductiveHypothesis = plusLeftCancel left right right' in ?plusLeftCancelStepCase -plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->+total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> (p : left + right = left' + right) -> left = left' plusRightCancel left left' O p = ?plusRightCancelBaseCase plusRightCancel left left' (S right) p = let inductiveHypothesis = plusRightCancel left left' right in ?plusRightCancelStepCase -plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->+total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> (p : left + right = left) -> right = O plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase plusLeftLeftRightZero (S left) right p =@@ -221,95 +301,95 @@ ?plusLeftLeftRightZeroStepCase -- Mult-multZeroLeftZero : (right : Nat) -> O * right = O+total multZeroLeftZero : (right : Nat) -> O * right = O multZeroLeftZero right = refl -multZeroRightZero : (left : Nat) -> left * O = O+total multZeroRightZero : (left : Nat) -> left * O = O multZeroRightZero O = refl multZeroRightZero (S left) = let inductiveHypothesis = multZeroRightZero left in ?multZeroRightZeroStepCase -multRightSuccPlus : (left : Nat) -> (right : Nat) ->+total multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * (S right) = left + (left * right) multRightSuccPlus O right = refl multRightSuccPlus (S left) right = let inductiveHypothesis = multRightSuccPlus left right in ?multRightSuccPlusStepCase -multLeftSuccPlus : (left : Nat) -> (right : Nat) ->+total multLeftSuccPlus : (left : Nat) -> (right : Nat) -> (S left) * right = right + (left * right) multLeftSuccPlus left right = refl -multCommutative : (left : Nat) -> (right : Nat) ->+total multCommutative : (left : Nat) -> (right : Nat) -> left * right = right * left multCommutative O right = ?multCommutativeBaseCase multCommutative (S left) right = let inductiveHypothesis = multCommutative left right in ?multCommutativeStepCase -multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre + right) = (left * centre) + (left * right) multDistributesOverPlusRight O centre right = refl multDistributesOverPlusRight (S left) centre right = let inductiveHypothesis = multDistributesOverPlusRight left centre right in ?multDistributesOverPlusRightStepCase -multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left + centre) * right = (left * right) + (centre * right) multDistributesOverPlusLeft O centre right = refl multDistributesOverPlusLeft (S left) centre right = let inductiveHypothesis = multDistributesOverPlusLeft left centre right in ?multDistributesOverPlusLeftStepCase -multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre * right) = (left * centre) * right multAssociative O centre right = refl multAssociative (S left) centre right = let inductiveHypothesis = multAssociative left centre right in ?multAssociativeStepCase -multOneLeftNeutral : (right : Nat) -> 1 * right = right+total multOneLeftNeutral : (right : Nat) -> 1 * right = right multOneLeftNeutral O = refl multOneLeftNeutral (S right) = let inductiveHypothesis = multOneLeftNeutral right in ?multOneLeftNeutralStepCase -multOneRightNeutral : (left : Nat) -> left * 1 = left+total multOneRightNeutral : (left : Nat) -> left * 1 = left multOneRightNeutral O = refl multOneRightNeutral (S left) = let inductiveHypothesis = multOneRightNeutral left in ?multOneRightNeutralStepCase -- Minus-minusSuccSucc : (left : Nat) -> (right : Nat) ->+total minusSuccSucc : (left : Nat) -> (right : Nat) -> (S left) - (S right) = left - right minusSuccSucc left right = refl -minusZeroLeft : (right : Nat) -> 0 - right = O+total minusZeroLeft : (right : Nat) -> 0 - right = O minusZeroLeft right = refl -minusZeroRight : (left : Nat) -> left - 0 = left+total minusZeroRight : (left : Nat) -> left - 0 = left minusZeroRight O = refl minusZeroRight (S left) = refl -minusZeroN : (n : Nat) -> O = n - n+total minusZeroN : (n : Nat) -> O = n - n minusZeroN O = refl minusZeroN (S n) = minusZeroN n -minusOneSuccN : (n : Nat) -> S O = (S n) - n+total minusOneSuccN : (n : Nat) -> S O = (S n) - n minusOneSuccN O = refl minusOneSuccN (S n) = minusOneSuccN n -minusSuccOne : (n : Nat) -> S n - 1 = n+total minusSuccOne : (n : Nat) -> S n - 1 = n minusSuccOne O = refl minusSuccOne (S n) = refl -minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O+total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O minusPlusZero O m = refl minusPlusZero (S n) m = minusPlusZero n m -minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left - centre - right = left - (centre + right) minusMinusMinusPlus O O right = refl minusMinusMinusPlus (S left) O right = refl@@ -318,14 +398,14 @@ let inductiveHypothesis = minusMinusMinusPlus left centre right in ?minusMinusMinusPlusStepCase -plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->+total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (left + right) - (left + right') = right - right' plusMinusLeftCancel O right right' = refl plusMinusLeftCancel (S left) right right' = let inductiveHypothesis = plusMinusLeftCancel left right right' in ?plusMinusLeftCancelStepCase -multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left - centre) * right = (left * right) - (centre * right) multDistributesOverMinusLeft O O right = refl multDistributesOverMinusLeft (S left) O right =@@ -335,45 +415,45 @@ let inductiveHypothesis = multDistributesOverMinusLeft left centre right in ?multDistributesOverMinusLeftStepCase -multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->+total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre - right) = (left * centre) - (left * right) multDistributesOverMinusRight left centre right = ?multDistributesOverMinusRightBody -- Power-powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =+total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) = base * (power base exp) powerSuccPowerLeft base exp = refl -multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->+total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> (power base exp) * (power base exp') = power base (exp + exp') multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase multPowerPowerPlus base (S exp) exp' = let inductiveHypothesis = multPowerPowerPlus base exp exp' in ?multPowerPowerPlusStepCase -powerZeroOne : (base : Nat) -> power base 0 = S O+total powerZeroOne : (base : Nat) -> power base 0 = S O powerZeroOne base = refl -powerOneNeutral : (base : Nat) -> power base 1 = base+total powerOneNeutral : (base : Nat) -> power base 1 = base powerOneNeutral O = refl powerOneNeutral (S base) = let inductiveHypothesis = powerOneNeutral base in ?powerOneNeutralStepCase -powerOneSuccOne : (exp : Nat) -> power 1 exp = S O+total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O powerOneSuccOne O = refl powerOneSuccOne (S exp) = let inductiveHypothesis = powerOneSuccOne exp in ?powerOneSuccOneStepCase -powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base+total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base powerSuccSuccMult O = refl powerSuccSuccMult (S base) = let inductiveHypothesis = powerSuccSuccMult base in ?powerSuccSuccMultStepCase -powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->+total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> power (power base exp) exp' = power base (exp * exp') powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase powerPowerMultPower base exp (S exp') =@@ -381,10 +461,10 @@ ?powerPowerMultPowerStepCase -- Pred-predSucc : (n : Nat) -> pred (S n) = n+total predSucc : (n : Nat) -> pred (S n) = n predSucc n = refl -minusSuccPred : (left : Nat) -> (right : Nat) ->+total minusSuccPred : (left : Nat) -> (right : Nat) -> left - (S right) = pred (left - right) minusSuccPred O right = refl minusSuccPred (S left) O =@@ -395,50 +475,50 @@ ?minusSuccPredStepCase' -- boolElim-boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->+total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) -> S (boolElim cond t f) = boolElim cond (S t) (S f) boolElimSuccSucc True t f = refl boolElimSuccSucc False t f = refl -boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->+total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) -> left + (boolElim cond t f) = boolElim cond (left + t) (left + f) boolElimPlusPlusLeft True left t f = refl boolElimPlusPlusLeft False left t f = refl -boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->+total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) -> (boolElim cond t f) + right = boolElim cond (t + right) (f + right) boolElimPlusPlusRight True right t f = refl boolElimPlusPlusRight False right t f = refl -boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->+total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) -> left * (boolElim cond t f) = boolElim cond (left * t) (left * f) boolElimMultMultLeft True left t f = refl boolElimMultMultLeft False left t f = refl -boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->+total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) -> (boolElim cond t f) * right = boolElim cond (t * right) (f * right) boolElimMultMultRight True right t f = refl boolElimMultMultRight False right t f = refl -- Orders-lteNTrue : (n : Nat) -> lte n n = True+total lteNTrue : (n : Nat) -> lte n n = True lteNTrue O = refl lteNTrue (S n) = lteNTrue n -lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False+total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False lteSuccZeroFalse O = refl lteSuccZeroFalse (S n) = refl -- Minimum and maximum-minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O+total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O minimumZeroZeroRight O = refl minimumZeroZeroRight (S right) = minimumZeroZeroRight right -minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O+total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O minimumZeroZeroLeft O = refl minimumZeroZeroLeft (S left) = refl -minimumSuccSucc : (left : Nat) -> (right : Nat) ->+total minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (S left) (S right) = S (minimum left right) minimumSuccSucc O O = refl minimumSuccSucc (S left) O = refl@@ -447,7 +527,7 @@ let inductiveHypothesis = minimumSuccSucc left right in ?minimumSuccSuccStepCase -minimumCommutative : (left : Nat) -> (right : Nat) ->+total minimumCommutative : (left : Nat) -> (right : Nat) -> minimum left right = minimum right left minimumCommutative O O = refl minimumCommutative O (S right) = refl@@ -456,15 +536,15 @@ let inductiveHypothesis = minimumCommutative left right in ?minimumCommutativeStepCase -maximumZeroNRight : (right : Nat) -> maximum O right = right+total maximumZeroNRight : (right : Nat) -> maximum O right = right maximumZeroNRight O = refl maximumZeroNRight (S right) = refl -maximumZeroNLeft : (left : Nat) -> maximum left O = left+total maximumZeroNLeft : (left : Nat) -> maximum left O = left maximumZeroNLeft O = refl maximumZeroNLeft (S left) = refl -maximumSuccSucc : (left : Nat) -> (right : Nat) ->+total maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximum left right) = maximum (S left) (S right) maximumSuccSucc O O = refl maximumSuccSucc (S left) O = refl@@ -473,7 +553,7 @@ let inductiveHypothesis = maximumSuccSucc left right in ?maximumSuccSuccStepCase -maximumCommutative : (left : Nat) -> (right : Nat) ->+total maximumCommutative : (left : Nat) -> (right : Nat) -> maximum left right = maximum right left maximumCommutative O O = refl maximumCommutative (S left) O = refl@@ -481,6 +561,11 @@ maximumCommutative (S left) (S right) = let inductiveHypothesis = maximumCommutative left right in ?maximumCommutativeStepCase++-- div and mod+total modZeroZero : (n : Nat) -> mod 0 n = O+modZeroZero O = refl+modZeroZero (S n) = refl -------------------------------------------------------------------------------- -- Proofs
+ lib/prelude/tactics.idr view
@@ -0,0 +1,4 @@+module prelude.tactics++data Tactic = Intro (List IdrisName)+ | Refine IdrisName
lib/prelude/vect.idr view
@@ -1,56 +1,302 @@ module prelude.vect -import prelude.nat import prelude.fin+import prelude.list+import prelude.nat %access public infixr 10 :: data Vect : Set -> Nat -> Set where- Nil : Vect a O- (::) : a -> Vect a k -> Vect a (S k) + Nil : Vect a O+ (::) : a -> Vect a n -> Vect a (S n) +--------------------------------------------------------------------------------+-- Indexing into vectors+--------------------------------------------------------------------------------+ tail : Vect a (S n) -> Vect a n-tail (x :: xs) = xs+tail (x::xs) = xs -lookup : Fin n -> Vect a n -> a-lookup fO (x :: xs) = x-lookup (fS k) (x :: xs) = lookup k xs-lookup fO [] impossible-lookup (fS _) [] impossible- -(++) : Vect a n -> Vect a m -> Vect a (n + m)-(++) [] ys = ys-(++) (x :: xs) ys = x :: xs ++ ys+head : Vect a (S n) -> a+head (x::xs) = x -filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)+last : Vect a (S n) -> a+last (x::[]) = x+last (x::y::ys) = last $ y::ys++init : Vect a (S n) -> Vect a n+init (x::[]) = []+init (x::y::ys) = x :: init (y::ys)++index : Fin n -> Vect a n -> a+index fO (x::xs) = x+index (fS k) (x::xs) = index k xs+index fO [] impossible+index (fS _) [] impossible++--------------------------------------------------------------------------------+-- Subvectors+--------------------------------------------------------------------------------++take : Fin n -> Vect a n -> (p ** Vect a p)+take fO xs = (_ ** [])+take (fS k) [] impossible+take (fS k) (x::xs) with (take k xs)+ | (_ ** tail) = (_ ** x::tail)++drop : Fin n -> Vect a n -> (p ** Vect a p)+drop fO xs = (_ ** xs)+drop (fS k) [] impossible+drop (fS k) (x::xs) = drop k xs++--------------------------------------------------------------------------------+-- Conversions to and from list+--------------------------------------------------------------------------------++total toList : Vect a n -> List a+toList [] = []+toList (x::xs) = x :: toList xs++total fromList : (l : List a) -> Vect a (length l)+fromList [] = []+fromList (x::xs) = x :: fromList xs++--------------------------------------------------------------------------------+-- Building bigger vectors+--------------------------------------------------------------------------------++(++) : Vect a m -> Vect a n -> Vect a (m + n)+(++) [] ys = ys+(++) (x::xs) ys = x :: xs ++ ys++--------------------------------------------------------------------------------+-- Maps+--------------------------------------------------------------------------------++total map : (a -> b) -> Vect a n -> Vect b n+map f [] = []+map f (x::xs) = f x :: map f xs++-- XXX: causes Idris to enter an infinite loop when type checking in the REPL+--mapMaybe : (a -> Maybe b) -> Vect a n -> (p ** Vect b p)+--mapMaybe f [] = (_ ** [])+--mapMaybe f (x::xs) = mapMaybe' (f x) +-- XXX: working around the type restrictions on case statements+-- where+-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)+-- mapMaybe' Nothing (n ** tail) = (n ** tail)+-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)++--------------------------------------------------------------------------------+-- Folds+--------------------------------------------------------------------------------++total foldl : (a -> b -> a) -> a -> Vect b m -> a+foldl f e [] = e+foldl f e (x::xs) = foldl f (f e x) xs++total foldr : (a -> b -> b) -> b -> Vect a m -> b+foldr f e [] = e+foldr f e (x::xs) = f x (foldr f e xs)++--------------------------------------------------------------------------------+-- Special folds+--------------------------------------------------------------------------------++total and : Vect Bool m -> Bool+and = foldr (&&) True++total or : Vect Bool m -> Bool+or = foldr (||) False++total any : (a -> Bool) -> Vect a m -> Bool+any p = or . map p++total all : (a -> Bool) -> Vect a m -> Bool+all p = and . map p++--------------------------------------------------------------------------------+-- Transformations+--------------------------------------------------------------------------------++total reverse : Vect a n -> Vect a n+reverse = reverse' []+ where+ total reverse' : Vect a m -> Vect a n -> Vect a (m + n)+ reverse' acc [] ?= acc+ reverse' acc (x::xs) ?= reverse' (x::acc) xs++total intersperse' : a -> Vect a m -> (p ** Vect a p)+intersperse' sep [] = (_ ** [])+intersperse' sep (y::ys) with (intersperse' sep ys)+ | (_ ** tail) = (_ ** sep::y::tail)++total intersperse : a -> Vect a m -> (p ** Vect a p)+intersperse sep [] = (_ ** [])+intersperse sep (x::xs) with (intersperse' sep xs)+ | (_ ** tail) = (_ ** x::tail)++--------------------------------------------------------------------------------+-- Membership tests+--------------------------------------------------------------------------------++elemBy : (a -> a -> Bool) -> a -> Vect a n -> Bool+elemBy p e [] = False+elemBy p e (x::xs) with (p e x)+ | True = True+ | False = elemBy p e xs++elem : Eq a => a -> Vect a n -> Bool+elem = elemBy (==)++lookupBy : (a -> a -> Bool) -> a -> Vect (a, b) n -> Maybe b+lookupBy p e [] = Nothing+lookupBy p e ((l, r)::xs) with (p e l)+ | True = Just r+ | False = lookupBy p e xs++lookup : Eq a => a -> Vect (a, b) n -> Maybe b+lookup = lookupBy (==)++hasAnyBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool+hasAnyBy p elems [] = False+hasAnyBy p elems (x::xs) with (elemBy p x elems)+ | True = True+ | False = hasAnyBy p elems xs++hasAny : Eq a => Vect a m -> Vect a n -> Bool+hasAny = hasAnyBy (==)++--------------------------------------------------------------------------------+-- Searching with a predicate+--------------------------------------------------------------------------------++find : (a -> Bool) -> Vect a n -> Maybe a+find p [] = Nothing+find p (x::xs) with (p x)+ | True = Just x+ | False = find p xs++findIndex : (a -> Bool) -> Vect a n -> Maybe Nat+findIndex = findIndex' 0+ where+ findIndex' : Nat -> (a -> Bool) -> Vect a n -> Maybe Nat+ findIndex' cnt p [] = Nothing+ findIndex' cnt p (x::xs) with (p x)+ | True = Just cnt+ | False = findIndex' (S cnt) p xs++total findIndices : (a -> Bool) -> Vect a m -> (p ** Vect Nat p)+findIndices = findIndices' 0+ where+ total findIndices' : Nat -> (a -> Bool) -> Vect a m -> (p ** Vect Nat p)+ findIndices' cnt p [] = (_ ** [])+ findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)+ | (_ ** tail) =+ if p x then+ (_ ** cnt::tail)+ else+ (_ ** tail)++elemIndexBy : (a -> a -> Bool) -> a -> Vect a m -> Maybe Nat+elemIndexBy p e = findIndex $ p e++elemIndex : Eq a => a -> Vect a m -> Maybe Nat+elemIndex = elemIndexBy (==)++total elemIndicesBy : (a -> a -> Bool) -> a -> Vect a m -> (p ** Vect Nat p)+elemIndicesBy p e = findIndices $ p e++total elemIndices : Eq a => a -> Vect a m -> (p ** Vect Nat p)+elemIndices = elemIndicesBy (==)++--------------------------------------------------------------------------------+-- Filters+--------------------------------------------------------------------------------++total filter : (a -> Bool) -> Vect a n -> (p ** Vect a p) filter p [] = ( _ ** [] )-filter p (x :: xs) - = let (_ ** xs') = filter p xs in- if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )+filter p (x::xs) with (filter p xs)+ | (_ ** tail) =+ if p x then+ (_ ** x::tail)+ else+ (_ ** tail) -map : (a -> b) -> Vect a n -> Vect b n-map f [] = []-map f (x :: xs) = f x :: map f xs+nubBy : (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)+nubBy = nubBy' []+ where+ nubBy' : Vect a m -> (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)+ nubBy' acc p [] = (_ ** [])+ nubBy' acc p (x::xs) with (elemBy p x acc)+ | True = nubBy' acc p xs+ | False with (nubBy' (x::acc) p xs)+ | (_ ** tail) = (_ ** x::tail) -reverse : Vect a n -> Vect a n-reverse xs = revAcc [] xs where- revAcc : Vect a n -> Vect a m -> Vect a (n + m)- revAcc acc [] ?= acc- revAcc acc (x :: xs) ?= revAcc (x :: acc) xs+nub : Eq a => Vect a n -> (p ** Vect a p)+nub = nubBy (==) ----------- Proofs ----------+--------------------------------------------------------------------------------+-- Splitting and breaking lists+-------------------------------------------------------------------------------- -revAcc_lemma_2 = proof {+--------------------------------------------------------------------------------+-- Predicates+--------------------------------------------------------------------------------++isPrefixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool+isPrefixOfBy p [] right = True+isPrefixOfBy p left [] = False+isPrefixOfBy p (x::xs) (y::ys) with (p x y)+ | True = isPrefixOfBy p xs ys+ | False = False++isPrefixOf : Eq a => Vect a m -> Vect a n -> Bool+isPrefixOf = isPrefixOfBy (==)++isSuffixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)++isSuffixOf : Eq a => Vect a m -> Vect a n -> Bool+isSuffixOf = isSuffixOfBy (==)++--------------------------------------------------------------------------------+-- Conversions+--------------------------------------------------------------------------------++total maybeToVect : Maybe a -> (p ** Vect a p)+maybeToVect Nothing = (_ ** [])+maybeToVect (Just j) = (_ ** [j])++total vectToMaybe : Vect a n -> Maybe a+vectToMaybe [] = Nothing+vectToMaybe (x::xs) = Just x++--------------------------------------------------------------------------------+-- Misc+--------------------------------------------------------------------------------++catMaybes : Vect (Maybe a) n -> (p ** Vect a p)+catMaybes [] = (_ ** [])+catMaybes (Nothing::xs) = catMaybes xs+catMaybes ((Just j)::xs) with (catMaybes xs)+ | (_ ** tail) = (_ ** j::tail)++--------------------------------------------------------------------------------+-- Proofs+--------------------------------------------------------------------------------++prelude.vect.reverse'_lemma_2 = proof { intros;- rewrite plusSuccRightSucc n k;+ rewrite (plusSuccRightSucc m n1); exact value; } -revAcc_lemma_1 = proof {+prelude.vect.reverse'_lemma_1 = proof { intros;- rewrite sym (plusZeroRightNeutral n);+ rewrite sym (plusZeroRightNeutral m); exact value; }
src/Core/CaseTree.hs view
@@ -38,11 +38,11 @@ namesUsed :: SC -> [Name] namesUsed sc = nub $ nu' [] sc where- nu' ps (Case n alts) = concatMap (nua ps) alts- nu' ps (STerm t) = nut ps t+ nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]+ nu' ps (STerm t) = nub $ nut ps t nu' ps _ = [] - nua ps (ConCase n i args sc) = nu' (ps ++ args) sc+ nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args nua ps (ConstCase _ sc) = nu' ps sc nua ps (DefaultCase sc) = nu' ps sc
src/Core/Constraints.hs view
@@ -32,7 +32,7 @@ acyclic :: Relations -> [UExp] -> TC () acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs where - checkCycle :: FC -> Relations -> [UExp] -> Int -> [UExp] -> TC () + checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC () checkCycle fc r path inc [] = return () checkCycle fc r path inc (c : cs) = do check fc path inc c @@ -42,10 +42,13 @@ check fc path inc (UVar x) | x < 0 = return () check fc path inc cv - | inc > 0 && cv `elem` path = Error $ At fc UniverseError + | inc > 0 && cv `elem` map fst path + = Error $ At fc UniverseError + -- FIXME: Make informative + -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path)) | otherwise = case M.lookup cv r of Nothing -> return () - Just cs -> mapM_ (next (cv:path) inc) cs + Just cs -> mapM_ (next ((cv, fc):path) inc) cs next path inc (ULT l r, fc) = check fc path (inc + 1) r next path inc (ULE l r, fc) = check fc path inc r
src/Core/Elaborate.hs view
@@ -108,6 +108,14 @@ b <- lift $ goalAtFocus (fst p) return (binderTy b) +-- Get the guess at the current hole, if there is one+get_guess :: Elab' aux Type+get_guess = do ES p _ _ <- get+ b <- lift $ goalAtFocus (fst p)+ case b of+ Guess t v -> return v+ _ -> fail "Not a guess"+ -- typecheck locally get_type :: Raw -> Elab' aux Type get_type tm = do ctxt <- get_context@@ -278,7 +286,13 @@ when i (movelast n) mkClaims sc' is (n : claims) mkClaims t [] claims = return (reverse claims)- mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn+ mkClaims _ _ _ + | Var n <- fn+ = do ctxt <- get_context+ case lookupTy Nothing n ctxt of+ [] -> lift $ tfail $ NoSuchVariable n + _ -> fail $ "Too many arguments for " ++ show fn+ | otherwise = fail $ "Too many arguments for " ++ show fn doClaim ((i, _), n, t) = do claim n t when i (movelast n)
src/Core/Evaluate.hs view
@@ -8,7 +8,7 @@ addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype, addCasedef, addOperator, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,- lookupTyEnv, isConName,+ lookupTyEnv, isConName, isFnName, Value(..)) where import Debug.Trace@@ -19,12 +19,30 @@ import Core.TT import Core.CaseTree -type EvalState = ()+data EvalState = ES { limited :: [(Name, Int)],+ steps :: Int -- number of applications/let reductions+ }++-- Evaluation fails if we hit a boredom threshold - in which case, just return+-- the original (capture the failure in a Maybe)+ type Eval a = State EvalState a data EvalOpt = Spec | HNF | Simplify | AtREPL deriving (Show, Eq) +initEval = ES [] 0++step :: Int -> Eval ()+step max = do e <- get+ put (e { steps = steps e + 1 })+ if steps e > max then fail "Threshold exceeded"+ else return () ++getSteps :: Eval Int+getSteps = do e <- get+ return (steps e)+ -- VALUES (as HOAS) --------------------------------------------------------- data Value = VP NameType Name Value@@ -34,6 +52,7 @@ | VSet UExp | VErased | VConstant Const+-- | VLazy Env [Value] Term | VTmp Int data HNF = HP NameType Name (TT Name)@@ -46,7 +65,7 @@ deriving Show instance Show Value where- show x = show $ evalState (quote 10 x) ()+ show x = show $ evalState (quote 100 x) initEval instance Show (a -> b) where show x = "<<fn>>"@@ -58,38 +77,42 @@ -- i.e. it's an intermediate environment that we have while type checking or -- while building a proof. +threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking+ -- in fact it's a maximum recursion depth+ normaliseC :: Context -> Env -> TT Name -> TT Name normaliseC ctxt env t - = evalState (do val <- eval ctxt emptyContext env t []- quote 0 val) ()+ = evalState (do val <- eval ctxt threshold [] env t []+ quote 0 val) initEval normaliseAll :: Context -> Env -> TT Name -> TT Name normaliseAll ctxt env t - = evalState (do val <- eval ctxt emptyContext env t [AtREPL]- quote 0 val) ()+ = evalState (do val <- eval ctxt threshold [] env t [AtREPL]+ quote 0 val) initEval normalise :: Context -> Env -> TT Name -> TT Name normalise ctxt env t - = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []- quote 0 val) ()+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []+ quote 0 val) initEval -specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name-specialise ctxt statics t - = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]- quote 0 val) ()+specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name+specialise ctxt env limits t + = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []+ quote 0 val) (initEval { limited = limits }) -- Like normalise, but we only reduce functions that are marked as okay to -- inline (and probably shouldn't reduce lets?) simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t - = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]- quote 0 val) ()+ = evalState (do val <- eval ctxt threshold [] + (map finalEntry env) (finalise t) [Simplify]+ quote 0 val) initEval hnf :: Context -> Env -> TT Name -> TT Name hnf ctxt env t - = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]- quote 0 val) ()+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]+ quote 0 val) initEval -- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))@@ -106,111 +129,153 @@ unbindEnv [] tm = tm unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc +usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])+usable n [] = (True, [])+usable n ns = case lookup n ns of+ Just 0 -> (False, ns)+ Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)+ _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)++reduction :: Eval ()+reduction = do ES ns s <- get+ put (ES ns (s+1))+ -- Evaluate in a context of locally named things (i.e. not de Bruijn indexed, -- such as we might have during construction of a proof) -eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value-eval ctxt statics genv tm opts = ev [] True [] tm where+eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value+eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where spec = Spec `elem` opts simpl = Simplify `elem` opts atRepl = AtREPL `elem` opts - ev stk top env (P _ n ty)- | Just (Let t v) <- lookup n genv = ev stk top env v - ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of- [(Function _ tm, Public)] -> - ev (n:stk) True env tm- [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty- return $ VP nt n vty- [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version- if simpl && (not inl || elem n stk) - then liftM (VP Ref n) (ev stk top env ty)- else do c <- evCase (n:stk) top env [] [] tree - case c of- (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)- (Just v, _) -> return v- _ -> liftM (VP Ref n) (ev stk top env ty)- ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)- ev stk top env (V i) | i < length env = return $ env !! i+ ev ntimes stk top env (P _ n ty)+ | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred+ ev ntimes stk top env v + ev ntimes_in stk top env (P Ref n ty) + | (True, ntimes) <- usable n ntimes_in+ = do let val = lookupDefAcc Nothing n atRepl ctxt + when (not atRepl) $ step maxred+ case val of+ [(Function _ tm, Public)] -> + ev ntimes (n:stk) True env tm+ [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty+ return $ VP nt n vty+ [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version+ if simpl && (not inl || elem n stk) + then liftM (VP Ref n) (ev ntimes stk top env ty)+ else do c <- evCase ntimes (n:stk) top env [] [] tree + case c of+ (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)+ (Just v, _) -> return v+ _ -> liftM (VP Ref n) (ev ntimes stk top env ty)+ ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)+ ev ntimes stk top env (V i) | i < length env = return $ env !! i | otherwise = return $ VV i - ev stk top env (Bind n (Let t v) sc)- = do v' <- ev stk top env v --(finalise v)- sc' <- ev stk top (v' : env) sc+ ev ntimes stk top env (Bind n (Let t v) sc)+ = do v' <- ev ntimes stk top env v --(finalise v)+ when (not atRepl) $ step maxred+ sc' <- ev ntimes stk top (v' : env) sc wknV (-1) sc'- ev stk top env (Bind n (NLet t v) sc)- = do t' <- ev stk top env (finalise t)- v' <- ev stk top env (finalise v)- sc' <- ev stk top (v' : env) sc+ ev ntimes stk top env (Bind n (NLet t v) sc)+ = do t' <- ev ntimes stk top env (finalise t)+ v' <- ev ntimes stk top env (finalise v)+ when (not atRepl) $ step maxred+ sc' <- ev ntimes stk top (v' : env) sc return $ VBind n (Let t' v') (\x -> return sc')- ev stk top env (Bind n b sc) + ev ntimes stk top env (Bind n b sc) = do b' <- vbind env b- return $ VBind n b' (\x -> ev stk top (x:env) sc)- where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t- ev stk top env (App f a) = do f' <- ev stk top env f- a' <- ev stk False env a- evApply stk top env [a'] f'- ev stk top env (Constant c) = return $ VConstant c- ev stk top env Erased = return VErased- ev stk top env (Set i) = return $ VSet i+ when (not atRepl) $ step maxred+ return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)+ where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t+-- ev ntimes stk top env (App (App (P _ laz _) _) a)+-- | laz == UN "lazy"+-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a+ ev ntimes stk top env (App f a) + = do f' <- ev ntimes stk top env f+ a' <- ev ntimes stk False env a+ when (not atRepl) $ step maxred+ evApply ntimes stk top env [a'] f'+ ev ntimes stk top env (Constant c) = return $ VConstant c+ ev ntimes stk top env Erased = return VErased+ ev ntimes stk top env (Set i) = return $ VSet i - evApply stk top env args (VApp f a) = - evApply stk top env (a:args) f- evApply stk top env args f = apply stk top env f args+ evApply ntimes stk top env args (VApp f a) = + evApply ntimes stk top env (a:args) f+ evApply ntimes stk top env args f = do when (not atRepl) $ step maxred+ apply ntimes stk top env f args - apply stk top env (VBind n (Lam t) sc) (a:as) + apply ntimes stk top env f as + | length stk > threshold = return $ unload env f as+ apply ntimes stk top env (VBind n (Lam t) sc) (a:as) = do a' <- sc a- app <- apply stk top env a' as + app <- apply ntimes stk top env a' as wknV (-1) app- apply stk False env f args- | spec = return $ unload env f args- apply stk top env (VP Ref n ty) args- | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt- = -- traceWhen (n == UN ["interp"]) (show (n, args)) $- if simpl && (not inl || elem n stk) - then return $ unload env (VP Ref n ty) args- else do c <- evCase (n:stk) top env ns args tree- case c of- (Nothing, _) -> return $ unload env (VP Ref n ty) args- (Just v, rest) -> evApply stk top env rest v- | [Operator _ i op] <- lookupDef Nothing n ctxt- = if (i <= length args)- then case op (take i args) of- Nothing -> return $ unload env (VP Ref n ty) args- Just v -> evApply stk top env (drop i args) v- else return $ unload env (VP Ref n ty) args- apply stk top env f (a:as) = return $ unload env f (a:as)- apply stk top env f [] = return f+-- apply ntimes stk False env f args+-- | spec = specApply ntimes stk env f args + apply ntimes_in stk top env f@(VP Ref n ty) args+ | (True, ntimes) <- usable n ntimes_in+ = do let val = lookupDefAcc Nothing n atRepl ctxt+ case val of+ [(CaseOp inl _ _ ns tree _ _, Public)] ->+ if simpl && (not inl || elem n stk) + then return $ unload env (VP Ref n ty) args+ else do c <- evCase ntimes (n:stk) top env ns args tree+ case c of+ (Nothing, _) -> return $ unload env (VP Ref n ty) args+ (Just v, rest) -> evApply ntimes stk top env rest v+ [(Operator _ i op, _)] ->+ if (i <= length args)+ then case op (take i args) of+ Nothing -> return $ unload env (VP Ref n ty) args+ Just v -> evApply ntimes stk top env (drop i args) v+ else return $ unload env (VP Ref n ty) args+ _ -> case args of+ [] -> return f+ _ -> return $ unload env f args+ apply ntimes stk top env f (a:as) = return $ unload env f (a:as)+ apply ntimes stk top env f [] = return f +-- specApply stk env f@(VP Ref n ty) args+-- = case lookupCtxt Nothing n statics of+-- [as] -> if or as +-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $ +-- return $ unload env f args+-- else return $ unload env f args+-- _ -> return $ unload env f args+-- specApply stk env f args = return $ unload env f args+ unload env f [] = f unload env f (a:as) = unload env (VApp f a) as - evCase stk top env ns args tree+ evCase ntimes stk top env ns args tree | length ns <= length args = do let args' = take (length ns) args let rest = drop (length ns) args- t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree+ t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree return (t, rest) | otherwise = return (Nothing, args) - evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)- evTree stk top env amap (UnmatchedCase str) = return Nothing- evTree stk top env amap (STerm tm) + evTree :: [(Name, Int)] -> [Name] -> Bool -> + [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)+ evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing+ evTree ntimes stk top env amap (STerm tm) = do let etm = pToVs (map fst amap) tm- etm' <- ev stk top (map snd amap ++ env) etm+ etm' <- ev ntimes stk top (map snd amap ++ env) etm return $ Just etm'- evTree stk top env amap (Case n alts)+ evTree ntimes stk top env amap (Case n alts) = case lookup n amap of Just v -> do c <- chooseAlt env v (getValArgs v) alts amap case c of- Just (altmap, sc) -> evTree stk top env altmap sc- _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap case c' of- Just (altmap, sc) -> evTree stk top env altmap sc+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc _ -> return Nothing _ -> return Nothing - chooseAlt' stk env _ (f, args) alts amap- = do f' <- apply stk True env f args+ chooseAlt' ntimes stk env _ (f, args) alts amap+ = do f' <- apply ntimes stk True env f args chooseAlt env f' (getValArgs f') alts amap chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->@@ -562,7 +627,7 @@ ctxtAlist :: Context -> [(Name, Def)] ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt) -veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()+veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt @@ -645,6 +710,15 @@ case tfst def of (TyDecl (DCon _ _) _) -> return True (TyDecl (TCon _ _) _) -> return True+ _ -> return False++isFnName :: Maybe [String] -> Name -> Context -> Bool+isFnName root n ctxt + = or $ do def <- lookupCtxt root n (definitions ctxt)+ case tfst def of+ (Function _ _) -> return True+ (Operator _ _ _) -> return True+ (CaseOp _ _ _ _ _ _ _) -> return True _ -> return False lookupP :: Maybe [String] -> Name -> Context -> [Term]
src/Core/ProofState.hs view
@@ -284,7 +284,7 @@ prep_fill :: Name -> [Name] -> RunTactic prep_fill f as ctxt env (Bind x (Hole ty) sc) =- do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)+ do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as) return $ Bind x (Guess ty val) sc prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
src/Core/TT.hs view
@@ -395,6 +395,16 @@ no' i (App f a) = no' i f && no' i a no' i _ = True +-- Returns all names used free in the term++freeNames :: Eq n => TT n -> [n]+freeNames (P _ n _) = [n]+freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])+ ++ freeNames t+freeNames (Bind n b sc) = nub $ freeNames (binderTy b) ++ (freeNames sc \\ [n])+freeNames (App f a) = nub $ freeNames f ++ freeNames a+freeNames _ = []+ -- Return the arity of a (normalised) type arity :: TT n -> Int
src/Idris/AbsSyntax.hs view
@@ -74,7 +74,7 @@ | IBCImp Name | IBCStatic Name | IBCClass Name- | IBCInstance Name Name+ | IBCInstance Bool Name Name | IBCDSL Name | IBCData Name | IBCOpt Name@@ -148,15 +148,20 @@ addToCG n ns = do i <- get put (i { idris_callgraph = addDef n ns (idris_callgraph i) }) -addInstance :: Name -> Name -> Idris ()-addInstance n i +-- Add a class instance function. Dodgy hack: Put integer instances first in the+-- list so they are resolved by default.++addInstance :: Bool -> Name -> Name -> Idris ()+addInstance int n i = do ist <- get case lookupCtxt Nothing n (idris_classes ist) of [CI a b c d ins] ->- do let cs = addDef n (CI a b c d (i : ins)) (idris_classes ist)+ do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist) put (ist { idris_classes = cs }) _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist) put (ist { idris_classes = cs })+ where addI i ins | int = i : ins+ | otherwise = ins ++ [i] addClass :: Name -> ClassInfo -> Idris () addClass n i @@ -400,10 +405,11 @@ impl = Imp False Dynamic expl = Exp False Dynamic-constraint = Constraint False Static+constraint = Constraint False Dynamic tacimpl = TacImp False Dynamic data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen+ | Specialise [Name] -- specialise it, freeze these names deriving (Show, Eq) {-! deriving instance Binary FnOpt@@ -466,6 +472,16 @@ declared (PNamespace _ ds) = concatMap declared ds -- declared (PImport _) = [] +defined :: PDecl -> [Name]+defined (PFix _ _ _) = []+defined (PTy _ _ _ n t) = []+defined (PClauses _ _ n _) = [n] -- not a declaration+defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts+ where fstt (a, _, _) = a+defined (PParams _ _ ds) = concatMap defined ds+defined (PNamespace _ ds) = concatMap defined ds+-- declared (PImport _) = []+ updateN :: [(Name, Name)] -> Name -> Name updateN ns n | Just n' <- lookup n ns = n' updateN _ n = n@@ -752,7 +768,7 @@ showImp :: Bool -> PTerm -> String showImp impl tm = se 10 tm where se p (PQuote r) = "![" ++ show r ++ "]"- se p (PRef fc n) = if impl then show n ++ "[" ++ show fc ++ "]"+ se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]" else showbasic n where showbasic n@(UN _) = show n showbasic (MN _ s) = s@@ -781,6 +797,8 @@ _ -> "" se p (PPi (Constraint _ _) n ty sc) = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc+ se p (PPi (TacImp _ _ s) n ty sc)+ = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc se p (PApp _ (PRef _ f) []) | not impl = show f se p (PApp _ (PRef _ op@(UN (f:_))) args)@@ -1055,6 +1073,30 @@ pri Placeholder = 1 pri _ = 3 +addStatics :: Name -> Term -> PTerm -> Idris ()+addStatics n tm ptm =+ do let (statics, dynamics) = initStatics tm ptm+ let stnames = nub $ concatMap freeNames (map snd statics)+ let dnames = nub $ concatMap freeNames (map snd dynamics)+ when (not (null statics)) $+ logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics+ ++ "\n" ++ show stnames ++ "\n" ++ show dnames+ let statics' = nub $ map fst statics ++ + filter (\x -> not (elem x dnames)) stnames+ let stpos = staticList statics' tm+ i <- get+ put (i { idris_statics = addDef n stpos (idris_statics i) })+ addIBC (IBCStatic n)+ where+ initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)+ = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in+ if pstatic p == Static then ((n, ty) : static, dynamic)+ else (static, (n, ty) : dynamic)+ initStatics t pt = ([], [])++ staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc+ staticList _ _ = []+ -- Dealing with implicit arguments -- Add implicit Pi bindings for any names in the term which appear in an@@ -1066,14 +1108,13 @@ implicit syn n ptm = do i <- get let (tm', impdata) = implicitise syn i ptm- let (tm'', spos) = findStatics i tm'+-- let (tm'', spos) = findStatics i tm' put (i { idris_implicits = addDef n impdata (idris_implicits i) }) addIBC (IBCImp n) logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)- i <- get- put (i { idris_statics = addDef n spos (idris_statics i) })- addIBC (IBCStatic n)- return tm''+-- i <- get+-- put (i { idris_statics = addDef n spos (idris_statics i) })+ return tm' implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg]) implicitise syn ist tm@@ -1286,21 +1327,21 @@ -- FIXME: It's possible that this really has to happen after elaboration findStatics :: IState -> PTerm -> (PTerm, [Bool])-findStatics ist tm = let (ns, ss) = fs tm in+findStatics ist tm = trace (showImp True tm) $+ let (ns, ss) = fs tm in runState (pos ns ss tm) [] where fs (PPi p n t sc) | Static <- pstatic p = let (ns, ss) = fs sc in- (namesIn [] ist t : ns, namesIn [] ist t ++ n : ss)+ (namesIn [] ist t : ns, n : ss) | otherwise = let (ns, ss) = fs sc in- (namesIn [] ist t : ns, ss)+ (ns, ss) fs _ = ([], []) inOne n ns = length (filter id (map (elem n) ns)) == 1 pos ns ss (PPi p n t sc) - | n `inOne` ns && elem n ss- = do sc' <- pos ns ss sc+ | elem n ss = do sc' <- pos ns ss sc spos <- get put (True : spos) return (PPi (p { pstatic = Static }) n t sc')@@ -1360,6 +1401,8 @@ | PConstant (I _) <- getTm x = match (getTm x) x' match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) | PConstant (I _) <- getTm x = match (getTm x) x'+ match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'+ match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x') match (PApp _ f args) (PApp _ f' args') | length args == length args' = do mf <- match' f f'
src/Idris/Compiler.hs view
@@ -102,6 +102,13 @@ = do v' <- epic' env v k' <- epic' env k return (k' @@ (effect_ v'))+ | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm+ = do size' <- epic' env size+ t' <- epic' env t+ return $ malloc_ size' t'+ | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm+ = do t' <- epic' env t+ return $ mallocTrace_ t' | (P (DCon t a) n _, args) <- unApply tm = epicCon env t a n args epic' env (P (DCon t a) n _) = return $ con_ t
src/Idris/Coverage.hs view
@@ -113,59 +113,6 @@ upd p' p = p { getTm = p' } --- recursive calls are well-founded if one of their argument positions is--- always decreasing. Return a list of arguments which are either not used--- recursively, or always decreasing recursively---- If we encounter a non-total name, we'll fail--wellFounded :: IState -> Name -> SC -> Totality-wellFounded i n sc = case wff [] sc of- RightOK smaller_args -> - -- is there a number in every list?- -- trace (show (n, smaller_args)) $- case smaller_args of- [] -> Total []- (x : xs) -> let args = foldl intersect x xs in- if (null args) then Partial Itself- else Total args- LeftErr x -> Partial (Other x)- where- wff :: [Name] -> SC -> EitherErr [Name] [[Int]]- wff ns (Case n as) = do is <- mapM (wffC ns) as- return $ concat is- where wffC ns (ConCase n i ns' sc) = do checkOK n- wff (ns ++ ns') sc- wffC ns (ConstCase _ sc) = wff ns sc- wffC ns (DefaultCase sc) = wff ns sc- wff ns (STerm t) = argPos ns t- wff ns _ = return []-- checkOK n' = case lookupTotal n' (tt_ctxt i) of- [Partial _] -> LeftErr [n']- [Total _] -> RightOK ()- x -> RightOK ()-- argPos ns ap@(App f' a')- | (P _ f _, args) <- unApply ap - = if f == n then- do aa <- argPos ns a' - return $ chkArgs 0 ns args : aa- else do checkOK f- argPos ns a'- argPos ns (App f a) = do f' <- argPos ns f- a' <- argPos ns a- return (f' ++ a')- argPos ns (Bind n (Let t v) sc) = do v' <- argPos ns v- sc' <- argPos ns sc- return (v' ++ sc')- argPos ns (Bind n _ sc) = argPos ns sc- argPos ns _ = return []-- chkArgs i ns [] = []- chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs- chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs- -- Check if, in a given type n, the constructor cn : ty is strictly positive, -- and update the context accordingly @@ -280,7 +227,7 @@ i <- getIState let opts = case lookupCtxt Nothing n (idris_flags i) of [fs] -> fs- [] -> []+ _ -> [] t' <- case t of Unchecked -> case lookupDef Nothing n ctxt of
src/Idris/DSL.hs view
@@ -9,6 +9,8 @@ import Core.TT import Core.Evaluate +import Debug.Trace+ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm desugar syn i t = let t' = expandDo (dsl_info syn) t in t' -- addImpl i t'@@ -82,6 +84,7 @@ v' i (PAlternative as) = PAlternative $ map (v' i) as v' i (PHidden t) = PHidden (v' i t) v' i (PIdiom f t) = PIdiom f (v' i t)+ v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds) v' i t = t mkVar fc 0 = case index_first dsl of
src/Idris/ElabDecls.hs view
@@ -26,8 +26,9 @@ import Debug.Trace -recheckC ctxt fc env t +recheckC fc env t = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)+ ctxt <- getContext (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of Error e -> tfail (At fc e) OK x -> return x@@ -35,7 +36,7 @@ return (tm, ty) checkDef fc ns = do ctxt <- getContext- mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t+ mapM (\(n, t) -> do (t', _) <- recheckC fc [] t return (n, t')) ns elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()@@ -48,17 +49,21 @@ let ty = addImpl i ty' logLvl 3 $ show n ++ " pre-type " ++ showImp True ty' logLvl 2 $ show n ++ " type " ++ showImp True ty- ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []+ ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) [] (erun fc (build i info False n ty))- (cty, _) <- recheckC ctxt fc [] ty'+ ds <- checkDef fc defer+ addDeferred ds+ mapM_ (elabCaseBlock info) is + ctxt <- getContext+ (cty, _) <- recheckC fc [] tyT+ addStatics n cty ty' logLvl 2 $ "---> " ++ show cty let nty = normalise ctxt [] cty- ds <- checkDef fc ((n, nty):defer)+ ds <- checkDef fc [(n, nty)] addIBC (IBCDef n) addDeferred ds setFlags n opts addIBC (IBCFlags n opts)- mapM_ (elabCaseBlock info) is elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris () elabData info syn fc (PDatadecl n t_in dcons)@@ -73,7 +78,7 @@ def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is- (cty, _) <- recheckC ctxt fc [] t'+ (cty, _) <- recheckC fc [] t' logLvl 2 $ "---> " ++ show cty updateContext (addTyDecl n cty) -- temporary, to check cons cons <- mapM (elabCon info syn n) dcons@@ -137,15 +142,15 @@ rec = MN 0 "rec" mkp (UN n) = MN 0 ("p_" ++ n)- mkp (MN 0 n) = MN 0 ("p_" ++ n)+ mkp (MN i n) = MN i ("p_" ++ n) mkp (NS n s) = NS (mkp n) s mkImp (UN n) = UN ("implicit_" ++ n)- mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)+ mkImp (MN i n) = MN i ("implicit_" ++ n) mkImp (NS n s) = NS (mkImp n) s mkSet (UN n) = UN ("set_" ++ n)- mkSet (MN 0 n) = MN 0 ("set_" ++ n)+ mkSet (MN i n) = MN i ("set_" ++ n) mkSet (NS n s) = NS (mkSet n) s mkProj recty substs cimp ((pn_in, pty), pos)@@ -201,7 +206,7 @@ addDeferred def' mapM_ (elabCaseBlock info) is ctxt <- getContext- (cty, _) <- recheckC ctxt fc [] t'+ (cty, _) <- recheckC fc [] t' tyIs cty logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty addIBC (IBCDef n)@@ -289,8 +294,8 @@ when (tot /= Unchecked) $ addIBC (IBCTotal n tot) i <- get case lookupDef Nothing n (tt_ctxt i) of- (CaseOp _ _ _ _ sc _ _ : _) ->- do let ns = namesUsed sc+ (CaseOp _ _ _ scargs sc _ _ : _) ->+ do let ns = namesUsed sc \\ scargs logLvl 2 $ "Called names: " ++ show ns addToCG n ns addIBC (IBCCG n)@@ -322,7 +327,7 @@ logLvl 3 ("Value: " ++ show tm') let vtm = getInferTerm tm' logLvl 2 (show vtm)- recheckC ctxt (FC "(input)" 0) [] vtm+ recheckC (FC "(input)" 0) [] vtm -- checks if the clause is a possible left hand side. Returns the term if -- possible, otherwise Nothing.@@ -361,7 +366,7 @@ let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' logLvl 3 (show lhs_tm)- (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm+ (clhs, clhsty) <- recheckC fc [] lhs_tm logLvl 5 ("Checked " ++ show clhs) -- Elaborate where block ist <- getIState@@ -394,7 +399,7 @@ mapM_ (elabCaseBlock info) is ctxt <- getContext logLvl 5 $ "Rechecking"- (crhs, crhsty) <- recheckC ctxt fc [] rhs'+ (crhs, crhsty) <- recheckC fc [] rhs' i <- get checkInferred fc (delab' i crhs True) rhs return $ Just (clhs, crhs)@@ -426,7 +431,7 @@ let lhs_ty = getInferType lhs' let ret_ty = getRetTy lhs_ty logLvl 3 (show lhs_tm)- (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm+ (clhs, clhsty) <- recheckC fc [] lhs_tm logLvl 5 ("Checked " ++ show clhs) let bargs = getPBtys lhs_tm let wval = addImplBound i (map fst bargs) wval_in@@ -444,7 +449,7 @@ def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is- (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')+ (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval') logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty) windex <- getName -- build a type declaration for the new function:@@ -481,7 +486,7 @@ def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is- (crhs, crhsty) <- recheckC ctxt fc [] rhs'+ (crhs, crhsty) <- recheckC fc [] rhs' return $ Just (clhs, crhs) where getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t@@ -604,9 +609,9 @@ let conn' = case lookupCtxtName Nothing conn (idris_classes i) of [(n, _)] -> n _ -> conn- addInstance conn' cfn- addIBC (IBCInstance conn' cfn)--- iputStrLn ("Added " ++ show (conn, cfn))+ addInstance False conn' cfn+ addIBC (IBCInstance False conn' cfn)+-- iputStrLn ("Added " ++ show (conn, cfn, ty)) return [PTy syn fc [] cfn ty, PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]] @@ -654,8 +659,11 @@ toExp ns e sc = sc elabInstance :: ElabInfo -> SyntaxInfo -> - FC -> [PTerm] -> Name -> - [PTerm] -> PTerm -> [PDecl] -> Idris ()+ FC -> [PTerm] -> -- constraints+ Name -> -- the class + [PTerm] -> -- class parameters (i.e. instance) + PTerm -> -- full instance type+ [PDecl] -> Idris () elabInstance info syn fc cs n ps t ds = do i <- get (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of@@ -665,7 +673,7 @@ -- if the instance type matches any of the instances we have already, -- then it's overlapping, so report an error mapM_ (checkNotOverlapping i t) (class_instances ci) - addInstance n iname+ addInstance intInst n iname elabType info syn fc [] iname t let ips = zip (class_params ci) ps let ns = case n of@@ -679,6 +687,7 @@ let ds' = insertDefaults (class_defaults ci) ns ds iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci) mapM_ (warnMissing ds' ns) (map fst (class_methods ci))+ mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds') let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds' logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys) -- get the implicit parameters that need passing through to the where block@@ -696,8 +705,12 @@ [PClause fc iname lhs [] rhs wb] iLOG (show idecl) elabDecl info idecl- addIBC (IBCInstance n iname)+ addIBC (IBCInstance intInst n iname) where+ intInst = case ps of+ [PConstant IType] -> True+ _ -> False+ checkNotOverlapping i t n | take 2 (show n) == "@@" = return () | otherwise@@ -768,6 +781,13 @@ | null $ filter (clauseFor meth ns) decls = iWarn fc $ "method " ++ show meth ++ " not defined" | otherwise = return ()++ checkInClass ns meth+ | not (null (filter (eqRoot meth) ns)) = return ()+ | otherwise = tclift $ tfail (At fc (Msg $ + show meth ++ " not a method of class " ++ show n))++ eqRoot x y = nsroot x == nsroot y clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m' clauseFor m ns _ = False
src/Idris/ElabTerm.hs view
@@ -101,10 +101,7 @@ (elab' ina (PRef fc unitTy)) elab' ina (PFalse fc) = elab' ina (PRef fc falseTy) elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes- = do t <- goal- -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))- let insts = findInstances ist t- resolveTC 2 fn insts ist+ = resolveTC 5 fn ist elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c") instanceArg c elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,@@ -210,10 +207,11 @@ -- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist) -- = let dsl' = expandDo d (getTm arg) in -- trace (show dsl') $ elab' ina dsl'- elab' (ina, g) (PApp fc (PRef _ f) args')+ elab' (ina, g) tm@(PApp fc (PRef _ f) args') = do let args = {- case lookupCtxt f (inblock info) of Just ps -> (map (pexp . (PRef fc)) ps ++ args') _ ->-} args'+-- newtm <- mkSpecialised ist fc f (map getTm args') tm ivs <- get_instances -- HACK: we shouldn't resolve type classes if we're defining an instance -- function or default definition.@@ -221,7 +219,6 @@ ctxt <- get_context let guarded = isConName Nothing f ctxt try (do ns <- apply (Var f) (map isph args)- solve let (ns', eargs) = unzip $ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))@@ -230,16 +227,17 @@ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)) (elabArgs (ina || not isinf, guarded) [] False (reverse ns') - (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))+ mkSpecialised ist fc f (map getTm args') tm+ solve) (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)+ mkSpecialised ist fc f (map getTm args') tm solve) ivs' <- get_instances when (not pattern || (ina && not tcgen)) $ mapM_ (\n -> do focus n -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))- t <- goal- let insts = findInstances ist t- resolveTC 7 fn insts ist) (ivs' \\ ivs) + resolveTC 7 fn ist) (ivs' \\ ivs) where tcArg (n, PConstraint _ _ Placeholder) = True tcArg _ = False @@ -323,6 +321,9 @@ False -> return failed elabArgs ina failed r ns args +-- For every alternative, look at the function at the head. Automatically resolve+-- any nested alternatives where that function is also at the head+ pruneAlt :: [PTerm] -> [PTerm] pruneAlt xs = map prune xs where@@ -330,10 +331,17 @@ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as) prune t = t - choose f (PAlternative as) = PAlternative (filter (headIs f) as)+ choose f (PAlternative as)+ = let as' = fmap (choose f) as+ fs = filter (headIs f) as' in+ case fs of+ [a] -> a+ _ -> PAlternative as'+ choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as) choose f t = t headIs f (PApp _ (PRef _ f') _) = f == f'+ headIs f (PApp _ f' _) = headIs f f' headIs f _ = True -- keep if it's not an application trivial :: IState -> ElabD ()@@ -356,12 +364,13 @@ _ -> [] | otherwise = [] -resolveTC :: Int -> Name -> [Name] -> IState -> ElabD ()-resolveTC 0 fn insts ist = fail $ "Can't resolve type class"-resolveTC 1 fn insts ist = try (trivial ist) (resolveTC 0 fn insts ist)-resolveTC depth fn insts ist +resolveTC :: Int -> Name -> IState -> ElabD ()+resolveTC 0 fn ist = fail $ "Can't resolve type class"+resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)+resolveTC depth fn ist = try (trivial ist) (do t <- goal+ let insts = findInstances ist t let (tc, ttypes) = unApply t scopeOnly <- needsDefault t tc ttypes tm <- get_term@@ -373,11 +382,11 @@ elabTC n | n /= fn && tcname n = (resolve n depth, show n) | otherwise = (fail "Can't resolve", show n) - needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]- = do focus a- fill (RConstant IType) -- default Int- solve- return False+-- needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]+-- = do focus a+-- fill (RConstant IType) -- default Int+-- solve+-- return False needsDefault t f as | all boundVar as = return True -- fail $ "Can't resolve " ++ show t needsDefault t f a = return False -- trace (show t) $ return ()@@ -405,7 +414,10 @@ args <- apply (Var n) imps -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $ mapM_ (\ (_,n) -> do focus n- resolveTC (depth - 1) fn insts ist) + t' <- goal+ let (tc', ttype) = unApply t'+ let depth' = if t == t' then depth - 1 else depth+ resolveTC depth' fn ist) (filter (\ (x, y) -> not x) (zip (map fst imps) args)) -- if there's any arguments left, we've failed to resolve solve@@ -497,3 +509,45 @@ runT x = fail $ "Not implemented " ++ show x solveAll = try (do solve; solveAll) (return ())++-- If the function application is specialisable, make a new+-- top level function by normalising the application+-- and elaborating the new expression.++mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm+mkSpecialised i fc n args def+ = do let tm' = def+ case lookupCtxt Nothing n (idris_statics i) of+ [] -> return tm'+ [as] -> if (not (or as)) then return tm' else+ mkSpecDecl i n (zip args as) tm'++mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm+mkSpecDecl i n pargs tm'+ = do t <- goal+ g <- get_guess+ let (f, args) = unApply g+ let sargs = zip args (map snd pargs)+ let staticArgs = map fst (filter (\ (_,x) -> x) sargs)+ let ns = group (sort (concatMap staticFnNames staticArgs))+ let ntimes = map (\xs -> (head xs, length xs - 1)) ns+ if (not (null ns)) then+ do env <- get_env+ let g' = g -- specialise ctxt env ntimes g+ return tm'+-- trace (show t ++ "\n" +++-- show ntimes ++ "\n" ++ +-- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO+ else return tm'+ where+ ctxt = tt_ctxt i+ cg = idris_callgraph i++ staticFnNames tm | (P _ f _, as) <- unApply tm+ = if not (isFnName Nothing f ctxt) then [] + else case lookupCtxt Nothing f cg of+ [ns] -> f : f : [] --(ns \\ [f])+ [] -> [f,f]+ _ -> []+ staticFnNames _ = []+
src/Idris/IBC.hs view
@@ -21,7 +21,7 @@ import Paths_idris ibcVersion :: Word8-ibcVersion = 16+ibcVersion = 17 data IBCFile = IBCFile { ver :: Word8, sourcefile :: FilePath,@@ -30,7 +30,7 @@ ibc_fixes :: [FixDecl], ibc_statics :: [(Name, [Bool])], ibc_classes :: [(Name, ClassInfo)],- ibc_instances :: [(Name, Name)],+ ibc_instances :: [(Bool, Name, Name)], ibc_dsls :: [(Name, DSL)], ibc_datatypes :: [(Name, TypeInfo)], ibc_optimise :: [(Name, OptInfo)],@@ -88,8 +88,8 @@ = case lookupCtxt Nothing n (idris_classes i) of [v] -> return f { ibc_classes = (n,v): ibc_classes f } _ -> fail "IBC write failed"-ibc i (IBCInstance n ins) f - = return f { ibc_instances = (n,ins): ibc_instances f }+ibc i (IBCInstance int n ins) f + = return f { ibc_instances = (int,n,ins): ibc_instances f } ibc i (IBCDSL n) f = case lookupCtxt Nothing n (idris_dsls i) of [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }@@ -177,7 +177,7 @@ pFixes :: [FixDecl] -> Idris () pFixes f = do i <- getIState- putIState (i { idris_infixes = f ++ idris_infixes i })+ putIState (i { idris_infixes = sort $ f ++ idris_infixes i }) pStatics :: [(Name, [Bool])] -> Idris () pStatics ss = mapM_ (\ (n, s) ->@@ -193,8 +193,8 @@ = addDef n c (idris_classes i) })) cs -pInstances :: [(Name, Name)] -> Idris ()-pInstances cs = mapM_ (\ (n, ins) -> addInstance n ins) cs+pInstances :: [(Bool, Name, Name)] -> Idris ()+pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs pDSLs :: [(Name, DSL)] -> Idris () pDSLs cs = mapM_ (\ (n, c) ->@@ -704,6 +704,8 @@ TotalFn -> putWord8 1 TCGen -> putWord8 2 AssertTotal -> putWord8 3+ Specialise x -> do putWord8 4+ put x get = do i <- getWord8 case i of@@ -711,6 +713,8 @@ 1 -> return TotalFn 2 -> return TCGen 3 -> return AssertTotal+ 4 -> do x <- get+ return (Specialise x) _ -> error "Corrupted binary data for FnOpt" instance Binary Fixity where@@ -773,6 +777,10 @@ Constraint x1 x2 -> do putWord8 2 put x1 put x2+ TacImp x1 x2 x3 -> do putWord8 3+ put x1+ put x2+ put x3 get = do i <- getWord8 case i of@@ -785,6 +793,10 @@ 2 -> do x1 <- get x2 <- get return (Constraint x1 x2)+ 3 -> do x1 <- get+ x2 <- get+ x3 <- get+ return (TacImp x1 x2 x3) _ -> error "Corrupted binary data for Plicity" @@ -1057,6 +1069,12 @@ put x1 put x2 put x3+ PTacImplicit x1 x2 x3 x4 x5 -> do putWord8 3+ put x1+ put x2+ put x3+ put x4+ put x5 get = do i <- getWord8 case i of@@ -1073,6 +1091,12 @@ x2 <- get x3 <- get return (PConstraint x1 x2 x3)+ 3 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ return (PTacImplicit x1 x2 x3 x4 x5) _ -> error "Corrupted binary data for PArg'"
src/Idris/Parser.hs view
@@ -141,22 +141,23 @@ parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos) parseImports fname input = do i <- get- case (runParser (do mname <- pHeader+ case (runParser (do whiteSpace+ mname <- pHeader ps <- many pImport rest <- getInput pos <- getPosition return ((mname, ps, rest, pos), i)) i fname input) of- Left err -> fail (ishow err)+ Left err -> fail (show err) Right (x, i) -> do put i return x where ishow err = let ln = sourceLine (errorPos err) in fname ++ ":" ++ show ln ++ ":parse error"--- show (map messageString (errorMessages err))+-- ++ show (map messageString (errorMessages err)) pHeader :: IParser [String] pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';') return (parseName i))- <|> return []+ <|> return [] where parseName x = case span (/='.') x of (x, "") -> [x] (x, '.':y) -> x : parseName y@@ -458,7 +459,7 @@ istate <- getState let fs = map (Fix (f prec)) ops setState (istate { - idris_infixes = sort (fs ++ idris_infixes istate),+ idris_infixes = nub $ sort (fs ++ idris_infixes istate), ibc_write = map IBCFix fs ++ ibc_write istate }) fc <- pfc return (PFix fc (f prec) ops)@@ -479,7 +480,7 @@ n_in <- pName; let n = expandNS syn n_in cs <- many1 carg reserved "where"; open_block - ds <- many1 $ pFunDecl syn+ ds <- many $ pFunDecl syn close_block let allDs = concat ds accData acc n (concatMap declared allDs)@@ -499,7 +500,7 @@ let sc = PApp fc (PRef fc cn) (map pexp args) let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc reserved "where"; open_block - ds <- many1 $ pFunDecl syn+ ds <- many $ pFunDecl syn close_block return [PInstance syn fc cs cn args t (concat ds)] @@ -615,6 +616,10 @@ pFnOpts :: IParser [FnOpt] pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs) <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)+ <|> do lchar '%'; reserved "specialise"; + lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'+ xs <- pFnOpts+ return (Specialise ns : xs) <|> return [] addAcc :: Name -> Maybe Accessibility -> IParser ()@@ -682,6 +687,7 @@ modifyConst syn fc (PConstant (I x)) | not (inPattern syn) = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]+ | otherwise = PConstant (I x) modifyConst syn fc x = x pList syn = do lchar '['; fc <- pfc@@ -922,7 +928,7 @@ <|> do reserved "String"; return StrType <|> do reserved "Ptr"; return PtrType <|> try (do f <- float; return $ Fl f)- <|> try (do i <- natural; lchar 'L'; return $ BI i)+-- <|> try (do i <- natural; lchar 'L'; return $ BI i) <|> try (do i <- natural; return $ I (fromInteger i)) <|> try (do s <- strlit; return $ Str s) <|> try (do c <- chlit; return $ Ch c)@@ -936,7 +942,8 @@ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-")) [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]] ++ toTable (reverse fixes) ++- [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],+ [[backtick],+ [binary "=" (\fc x y -> PEq fc x y) AssocLeft], [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]] toTable fs = map (map toBin) @@ -949,10 +956,13 @@ assoc (Infixr _) = AssocRight assoc (InfixN _) = AssocNone -binary name f assoc = Infix (do { reservedOp name; fc <- pfc; - return (f fc) }) assoc-prefix name f = Prefix (do { reservedOp name; fc <- pfc;- return (f fc) })+binary name f assoc = Infix (do reservedOp name; fc <- pfc; + return (f fc)) assoc+prefix name f = Prefix (do reservedOp name; fc <- pfc;+ return (f fc))+backtick = Infix (do lchar '`'; n <- pfName; lchar '`'+ fc <- pfc+ return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone --------- Data declarations ---------
src/Idris/Primitives.hs view
@@ -45,6 +45,7 @@ charToInt x = x intToChar x = x intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]+bigIntToInt x = foreign_ tyInt "bigIntToInt" [(x, tyBigInt)] strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)] bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)] strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]@@ -158,6 +159,8 @@ ([E.name "x"], intToChar (fun "x")) total, Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt) ([E.name "x"], intToBigInt (fun "x")) total,+ Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)+ ([E.name "x"], bigIntToInt (fun "x")) total, Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt) ([E.name "x"], strToBigInt (fun "x")) total, Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)@@ -257,6 +260,8 @@ c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x)) c_intToBigInt _ = Nothing+c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))+c_bigIntToInt _ = Nothing c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x)) c_bigIntToStr _ = Nothing
src/Idris/Prover.hs view
@@ -45,7 +45,7 @@ put (i { last_proof = Just (n, prf) }) let tree = simpleCase False True [(P Ref n ty, tm)] logLvl 3 (show tree)- (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm+ (ptm, pty) <- recheckC (FC "proof" 0) [] tm ptm' <- applyOpts ptm updateContext (addCasedef n True False True [(P Ref n ty, ptm)] [(P Ref n ty, ptm')] ty)
src/Idris/REPL.hs view
@@ -189,11 +189,13 @@ _ -> return () process fn (Info n) = do i <- get let oi = lookupCtxt Nothing n (idris_optimisation i)- liftIO $ print oi+ when (not (null oi)) $ iputStrLn (show oi)+ let si = lookupCtxt Nothing n (idris_statics i)+ when (not (null si)) $ iputStrLn (show si) process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext ist <- get- let tm' = specialise ctxt (idris_statics ist) tm+ let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm iputStrLn (show (delab ist tm')) process fn (Prove n) = do prover (lit fn) n -- recheck totality
tutorial/examples/interp.idr view
@@ -58,6 +58,9 @@ testFac : Int testFac = interp [] fact 4 +unitTestFac : so (interp [] fact 4 == 24)+unitTestFac = oh+ main : IO () main = do putStr "Enter a number: " x <- getLine