diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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) + } diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -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 diff --git a/lib/Makefile b/lib/Makefile --- a/lib/Makefile +++ b/lib/Makefile @@ -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: diff --git a/lib/builtins.idr b/lib/builtins.idr --- a/lib/builtins.idr +++ b/lib/builtins.idr @@ -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 diff --git a/lib/checkall.idr b/lib/checkall.idr --- a/lib/checkall.idr +++ b/lib/checkall.idr @@ -20,6 +20,8 @@ import prelude.vect import prelude.strings import prelude.char +import prelude.heap +import prelude.complex import network.cgi diff --git a/lib/prelude.idr b/lib/prelude.idr --- a/lib/prelude.idr +++ b/lib/prelude.idr @@ -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 diff --git a/lib/prelude/algebra.idr b/lib/prelude/algebra.idr --- a/lib/prelude/algebra.idr +++ b/lib/prelude/algebra.idr @@ -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? diff --git a/lib/prelude/complex.idr b/lib/prelude/complex.idr new file mode 100644 --- /dev/null +++ b/lib/prelude/complex.idr @@ -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) diff --git a/lib/prelude/heap.idr b/lib/prelude/heap.idr new file mode 100644 --- /dev/null +++ b/lib/prelude/heap.idr @@ -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 () +-} diff --git a/lib/prelude/list.idr b/lib/prelude/list.idr --- a/lib/prelude/list.idr +++ b/lib/prelude/list.idr @@ -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; } diff --git a/lib/prelude/nat.idr b/lib/prelude/nat.idr --- a/lib/prelude/nat.idr +++ b/lib/prelude/nat.idr @@ -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 diff --git a/lib/prelude/tactics.idr b/lib/prelude/tactics.idr new file mode 100644 --- /dev/null +++ b/lib/prelude/tactics.idr @@ -0,0 +1,4 @@ +module prelude.tactics + +data Tactic = Intro (List IdrisName) + | Refine IdrisName diff --git a/lib/prelude/vect.idr b/lib/prelude/vect.idr --- a/lib/prelude/vect.idr +++ b/lib/prelude/vect.idr @@ -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; } diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs --- a/src/Core/CaseTree.hs +++ b/src/Core/CaseTree.hs @@ -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 diff --git a/src/Core/Constraints.hs b/src/Core/Constraints.hs --- a/src/Core/Constraints.hs +++ b/src/Core/Constraints.hs @@ -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 diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs --- a/src/Core/Elaborate.hs +++ b/src/Core/Elaborate.hs @@ -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) diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -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 = "<>" @@ -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] diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs --- a/src/Core/ProofState.hs +++ b/src/Core/ProofState.hs @@ -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 diff --git a/src/Core/TT.hs b/src/Core/TT.hs --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -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 diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -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' diff --git a/src/Idris/Compiler.hs b/src/Idris/Compiler.hs --- a/src/Idris/Compiler.hs +++ b/src/Idris/Compiler.hs @@ -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 diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs --- a/src/Idris/Coverage.hs +++ b/src/Idris/Coverage.hs @@ -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 diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs --- a/src/Idris/DSL.hs +++ b/src/Idris/DSL.hs @@ -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 diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -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 diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -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 _ = [] + diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -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'" diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -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 --------- diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs --- a/src/Idris/Primitives.hs +++ b/src/Idris/Primitives.hs @@ -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 diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -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) diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -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 diff --git a/tutorial/examples/interp.idr b/tutorial/examples/interp.idr --- a/tutorial/examples/interp.idr +++ b/tutorial/examples/interp.idr @@ -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