diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -25,13 +25,16 @@ let cenv = compilerTemplateEnv (compilerId (compiler local)) let dirs_pkg = substituteInstallDirTemplates penv (installDirTemplates local) let dirs = substituteInstallDirTemplates cenv dirs_pkg - let datad = datadir dirs - let datasubd = datasubdir dirs 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) putStrLn $ "Installing libraries in " ++ idir - system' $ "make -C lib install TARGET=" ++ idir ++ " BINDIR=" ++ bind + system' $ "make -C lib install TARGET=" ++ idir ++ " IDRIS=" ++ icmd main = defaultMainWithHooks (simpleUserHooks { postInst = postInstLib, postClean = postCleanLib }) diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.9.0 +Version: 0.9.1 License: BSD3 License-file: LICENSE Author: Edwin Brady @@ -8,7 +8,7 @@ Stability: Beta Category: Compilers/Interpreters, Dependent Types -Synopsis: Dependently Typed Functional Programming Language +Synopsis: Functional Programming Language with Dependent Types Description: Idris is a general purpose language with full dependent types. It is compiled, with eager evaluation. Dependent types allow types to be predicated on values, @@ -41,7 +41,7 @@ Build-type: Custom Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr - tutorial/examples/*.idr + lib/control/monad/*.idr tutorial/examples/*.idr source-repository head type: git @@ -61,7 +61,7 @@ Idris.Delaborate, Idris.Primitives, Idris.Imports, Idris.Compiler, Idris.Prover, Idris.ElabTerm, Idris.Coverage, Idris.IBC, Idris.Unlit, - Idris.DataOpts, Idris.Transforms, + Idris.DataOpts, Idris.Transforms, Idris.DSL, Paths_idris diff --git a/lib/Makefile b/lib/Makefile --- a/lib/Makefile +++ b/lib/Makefile @@ -1,20 +1,23 @@ check: .PHONY - $(BINDIR)/idris --noprelude --verbose --check checkall.idr + $(IDRIS) --noprelude --verbose --check checkall.idr recheck: clean check install: check mkdir -p $(TARGET)/prelude mkdir -p $(TARGET)/network + mkdir -p $(TARGET)/control/monad install *.ibc $(TARGET) install prelude/*.ibc $(TARGET)/prelude install network/*.ibc $(TARGET)/network + install control/monad/*.ibc $(TARGET)/control/monad clean: .PHONY rm -f *.ibc rm -f prelude/*.ibc rm -f network/*.ibc + rm -f control/monad/*.ibc linecount: .PHONY wc -l *.idr network/*.idr prelude/*.idr diff --git a/lib/builtins.idr b/lib/builtins.idr --- a/lib/builtins.idr +++ b/lib/builtins.idr @@ -51,6 +51,9 @@ ($) : (a -> b) -> a -> b f $ a = f a +cong : {f : t -> u} -> (a = b) -> f a = f b +cong refl = refl + data Bool = False | True boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a @@ -113,6 +116,10 @@ instance Eq String where (==) = boolOp prim__eqString +instance (Eq a, Eq b) => Eq (a, b) where + (==) (a, c) (b, d) = (a == b) && (c == d) + + data Ordering = LT | EQ | GT class Eq a => Ord a where @@ -172,6 +179,13 @@ GT +instance (Ord a, Ord b) => Ord (a, b) where + compare (xl, xr) (yl, yr) = + if xl /= yl + then compare xl yl + else compare xr yr + + class (Eq a, Ord a) => Num a where (+) : a -> a -> a (-) : a -> a -> a @@ -232,8 +246,8 @@ strIndex : String -> Int -> Char strIndex = prim__strIndex -rev : String -> String -rev = prim__strRev +reverse : String -> String +reverse = prim__strRev } diff --git a/lib/checkall.idr b/lib/checkall.idr --- a/lib/checkall.idr +++ b/lib/checkall.idr @@ -8,6 +8,7 @@ import io import system +import prelude.algebra import prelude.cast import prelude.nat import prelude.fin @@ -22,3 +23,5 @@ import network.cgi +import control.monad.identity +import control.monad.state diff --git a/lib/control/monad/identity.idr b/lib/control/monad/identity.idr new file mode 100644 --- /dev/null +++ b/lib/control/monad/identity.idr @@ -0,0 +1,10 @@ +module control.monad.identity + +import prelude.monad + +public record Identity : Set -> Set where + Id : (runIdentity : a) -> Identity a + +instance Monad Identity where + return x = Id x + (Id x) >>= k = k x diff --git a/lib/control/monad/state.idr b/lib/control/monad/state.idr new file mode 100644 --- /dev/null +++ b/lib/control/monad/state.idr @@ -0,0 +1,29 @@ +module control.monad.state + +import control.monad.identity +import prelude.monad + +%access public + +class Monad m => MonadState s (m : Set -> Set) where + get : m s + put : s -> m () + +record StateT : Set -> (Set -> Set) -> Set -> Set where + ST : {m : Set -> Set} -> + (runStateT : s -> m (a, s)) -> StateT s m a + +instance Monad m => Monad (StateT s m) where + return x = ST (\st => return (x, st)) + + (ST f) >>= k = ST (\st => do (v, st') <- f st + let ST kv = k v + kv st') + +instance Monad m => MonadState s (StateT s m) where + get = ST (\x => return (x, x)) + put x = ST (\y => return ((), x)) + +State : Set -> Set -> Set +State s a = StateT s Identity a + diff --git a/lib/io.idr b/lib/io.idr --- a/lib/io.idr +++ b/lib/io.idr @@ -29,7 +29,7 @@ interpFTy FUnit = () ForeignTy : (xs:List FTy) -> (t:FTy) -> Set -ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where +ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where mkForeign' : List FTy -> Set -> Set mkForeign' Nil ty = ty mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty) diff --git a/lib/network/cgi.idr b/lib/network/cgi.idr --- a/lib/network/cgi.idr +++ b/lib/network/cgi.idr @@ -6,36 +6,19 @@ Vars : Set Vars = List (String, String) -data CGIInfo = CGISt Vars -- GET - Vars -- POST - Vars -- Cookies - String -- User agent - String -- headers - String -- output - -get_GET : CGIInfo -> Vars -get_GET (CGISt g _ _ _ _ _) = g - -get_POST : CGIInfo -> Vars -get_POST (CGISt _ p _ _ _ _) = p - -get_Cookies : CGIInfo -> Vars -get_Cookies (CGISt _ _ c _ _ _) = c - -get_UAgent : CGIInfo -> String -get_UAgent (CGISt _ _ _ a _ _) = a - -get_Headers : CGIInfo -> String -get_Headers (CGISt _ _ _ _ h _) = h - -get_Output : CGIInfo -> String -get_Output (CGISt _ _ _ _ _ o) = o +record CGIInfo : Set where + CGISt : (GET : Vars) -> + (POST : Vars) -> + (Cookies : Vars) -> + (UserAgent : String) -> + (Headers : String) -> + (Output : String) -> CGIInfo add_Headers : String -> CGIInfo -> CGIInfo -add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o +add_Headers str st = record { Headers = Headers st ++ str } st add_Output : String -> CGIInfo -> CGIInfo -add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str) +add_Output str st = record { Output = Output st ++ str } st abstract data CGI : Set -> Set where @@ -70,17 +53,17 @@ abstract queryVars : CGI Vars queryVars = do i <- getInfo - return (get_GET i) + return (GET i) abstract postVars : CGI Vars postVars = do i <- getInfo - return (get_POST i) + return (POST i) abstract cookieVars : CGI Vars cookieVars = do i <- getInfo - return (get_Cookies i) + return (Cookies i) abstract queryVar : String -> CGI (Maybe String) @@ -89,11 +72,11 @@ getOutput : CGI String getOutput = do i <- getInfo - return (get_Output i) + return (Output i) getHeaders : CGI String getHeaders = do i <- getInfo - return (get_Headers i) + return (Headers i) abstract flushHeaders : CGI () @@ -116,7 +99,7 @@ getContent : Int -> IO String getContent x = getC x "" where getC : Int -> String -> IO String - getC 0 acc = return $ rev acc + getC 0 acc = return $ reverse acc getC n acc = do x <- getChar getC (n-1) (strCons x acc) @@ -134,11 +117,11 @@ let post_vars = getVars ['&'] content let cookies = getVars [';'] cookie - p <- getAction prog (CGISt get_vars post_vars cookies agent - "Content-type: text/html\n" - "") - putStrLn (get_Headers (snd p)) - putStr (get_Output (snd p)) - return (fst p) + (v, st) <- getAction prog (CGISt get_vars post_vars cookies agent + "Content-type: text/html\n" + "") + putStrLn (Headers st) + putStr (Output st) + return v diff --git a/lib/prelude.idr b/lib/prelude.idr --- a/lib/prelude.idr +++ b/lib/prelude.idr @@ -49,15 +49,15 @@ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")" instance Show a => Show (List a) where - show xs = "[" ++ show' xs ++ "]" where - show' : Show a => List a -> String - show' [] = "" - show' [x] = show x - show' (x :: xs) = show x ++ ", " ++ show' xs + show xs = "[" ++ show' "" xs ++ "]" where + show' : String -> List a -> String + show' acc [] = acc + show' acc [x] = acc ++ show x + show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs instance Show a => Show (Vect a n) where show xs = "[" ++ show' xs ++ "]" where - show' : Show a => Vect a n -> String + show' : Vect a m -> String show' [] = "" show' [x] = show x show' (x :: xs) = show x ++ ", " ++ show' xs @@ -91,7 +91,7 @@ instance MonadPlus List where mzero = [] - mplus = app + mplus = (++) ---- Functor instances @@ -108,7 +108,7 @@ pure = Just (Just f) <$> (Just a) = Just (f a) - Nothing <$> Nothing = Nothing + _ <$> _ = Nothing ---- some mathematical operations @@ -164,9 +164,6 @@ = count start (next - start) end ---- More utilities - -flip : (a -> b -> c) -> b -> a -> c -flip f x y = f y x sum : Num a => List a -> a sum = foldl (+) 0 diff --git a/lib/prelude/algebra.idr b/lib/prelude/algebra.idr new file mode 100644 --- /dev/null +++ b/lib/prelude/algebra.idr @@ -0,0 +1,32 @@ +module algebra + +import builtins + +-- Sets with an associative binary operation +-- Must satisfy: +-- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c +class Semigroup a where + (<*>) : 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 => 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 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 diff --git a/lib/prelude/either.idr b/lib/prelude/either.idr --- a/lib/prelude/either.idr +++ b/lib/prelude/either.idr @@ -2,12 +2,62 @@ import builtins -data Either a b = Left a | Right b +import prelude.maybe +import prelude.list +data Either a b + = Left a + | Right b + +-------------------------------------------------------------------------------- +-- Syntactic tests +-------------------------------------------------------------------------------- + +isLeft : Either a b -> Bool +isLeft (Left l) = True +isLeft (Right r) = False + +isRight : Either a b -> Bool +isRight (Left l) = False +isRight (Right r) = True + +-------------------------------------------------------------------------------- +-- Misc. +-------------------------------------------------------------------------------- + choose : (b : Bool) -> Either (so b) (so (not b)) -choose True = Left oh +choose True = Left oh choose False = Right oh either : Either a b -> (a -> c) -> (b -> c) -> c either (Left x) l r = l x either (Right x) l r = r x + +lefts : List (Either a b) -> List a +lefts [] = [] +lefts (x::xs) = + case x of + Left l => l :: lefts xs + Right r => lefts xs + +rights : List (Either a b) -> List b +rights [] = [] +rights (x::xs) = + case x of + Left l => rights xs + Right r => r :: rights xs + +partitionEithers : List (Either a b) -> (List a, List b) +partitionEithers l = (lefts l, rights l) + +fromEither : Either a a -> a +fromEither (Left l) = l +fromEither (Right r) = r + +-------------------------------------------------------------------------------- +-- Conversions +-------------------------------------------------------------------------------- + +maybeToEither : e -> Maybe a -> Either e a +maybeToEither def (Just j) = Right j +maybeToEither def Nothing = Left def diff --git a/lib/prelude/fin.idr b/lib/prelude/fin.idr --- a/lib/prelude/fin.idr +++ b/lib/prelude/fin.idr @@ -7,7 +7,9 @@ fS : Fin k -> Fin (S k) instance Eq (Fin n) where - fO == fO = True - (fS k) == (fS k') = k == k' - _ == _ = False + (==) = eq where + eq : Fin m -> Fin m -> Bool + eq fO fO = True + eq (fS k) (fS k') = eq k k' + eq _ _ = False diff --git a/lib/prelude/list.idr b/lib/prelude/list.idr --- a/lib/prelude/list.idr +++ b/lib/prelude/list.idr @@ -1,104 +1,544 @@ module prelude.list -import prelude.maybe import builtins +import prelude.maybe +import prelude.nat + %access public -infixr 7 :: +infixr 10 :: -data List a = Nil | (::) a (List a) +data List a + = Nil + | (::) a (List a) -rev : List a -> List a -rev xs = revAcc [] xs where - revAcc : List a -> List a -> List a - revAcc acc [] = acc - revAcc acc (x :: xs) = revAcc (x :: acc) xs +-------------------------------------------------------------------------------- +-- Syntactic tests +-------------------------------------------------------------------------------- -app : List a -> List a -> List a -app [] xs = xs -app (x :: xs) ys = x :: app xs ys +isNil : List a -> Bool +isNil [] = True +isNil (x::xs) = False -length : List a -> Int -length [] = 0 -length (x :: xs) = 1 + length xs +isCons : List a -> Bool +isCons [] = False +isCons (x::xs) = True -take : Int -> List a -> List a -take 0 xs = [] -take n [] = [] -take n (x :: xs) = x :: take (n-1) xs +-------------------------------------------------------------------------------- +-- Indexing into lists +-------------------------------------------------------------------------------- -drop : Int -> List a -> List a -drop 0 xs = xs -drop n [] = [] -drop n (x :: xs) = drop (n-1) xs +head : (l : List a) -> (isCons l = True) -> a +head (x::xs) p = x -map : (a -> b) -> List a -> List b -map f [] = [] -map f (x :: xs) = f x :: map f xs +head' : (l : List a) -> Maybe a +head' [] = Nothing +head' (x::xs) = Just x -concatMap : (a -> List b) -> List a -> List b -concatMap f [] = [] -concatMap f (x :: xs) = app (f x) (concatMap f xs) +tail : (l : List a) -> (isCons l = True) -> List a +tail (x::xs) p = xs +tail' : (l : List a) -> Maybe (List a) +tail' [] = Nothing +tail' (x::xs) = Just xs + +last : (l : List a) -> (isCons l = True) -> a +last (x::xs) p = + case xs of + [] => x + y::ys => last (y::ys) ?lastProof + +last' : (l : List a) -> Maybe a +last' [] = Nothing +last' (x::xs) = + case xs of + [] => Just x + y::ys => last' xs + +init : (l : List a) -> (isCons l = True) -> List a +init (x::xs) p = + case xs of + [] => [] + y::ys => x :: init (y::ys) ?initProof + +init' : (l : List a) -> Maybe (List a) +init' [] = Nothing +init' (x::xs) = + case xs of + [] => Just [] + y::ys => + -- XXX: Problem with typechecking a "do" block here + case init' $ y::ys of + Nothing => Nothing + Just j => Just $ x :: j + +-------------------------------------------------------------------------------- +-- Sublists +-------------------------------------------------------------------------------- + +take : Nat -> List a -> List a +take Z xs = [] +take (S n) [] = [] +take (S n) (x::xs) = x :: take n xs + +drop : Nat -> List a -> List a +drop Z xs = xs +drop (S n) [] = [] +drop (S n) (x::xs) = drop n xs + +-------------------------------------------------------------------------------- +-- Misc. +-------------------------------------------------------------------------------- + +list : a -> (a -> List a -> a) -> List a -> a +list nil cons [] = nil +list nil cons (x::xs) = cons x xs + +length : List a -> Nat +length [] = 0 +length (x::xs) = 1 + length xs + +-------------------------------------------------------------------------------- +-- Building bigger lists +-------------------------------------------------------------------------------- + +(++) : List a -> List a -> List a +(++) [] right = right +(++) (x::xs) right = x :: (xs ++ right) + +-------------------------------------------------------------------------------- +-- Maps +-------------------------------------------------------------------------------- + +map : (a -> b) -> List a -> List b +map f [] = [] +map f (x::xs) = f x :: map f xs + mapMaybe : (a -> Maybe b) -> List a -> List b -mapMaybe f [] = [] -mapMaybe f (x :: xs) = case f x of - Nothing => mapMaybe f xs - Just v => v :: mapMaybe f xs +mapMaybe f [] = [] +mapMaybe f (x::xs) = + case f x of + Nothing => mapMaybe f xs + Just j => j :: mapMaybe f xs +-------------------------------------------------------------------------------- +-- Folds +-------------------------------------------------------------------------------- + foldl : (a -> b -> a) -> a -> List b -> a -foldl f a [] = a -foldl f a (x :: xs) = foldl f (f a x) xs +foldl f e [] = e +foldl f e (x::xs) = foldl f (f e x) xs foldr : (a -> b -> b) -> b -> List a -> b -foldr f b [] = b -foldr f b (x :: xs) = f x (foldr f b xs) +foldr f e [] = e +foldr f e (x::xs) = f x (foldr f e xs) -filter : (y -> Bool) -> List y -> List y -filter pred [] = [] -filter pred (x :: xs) = if (pred x) then (x :: filter pred xs) - else (filter pred xs) +-------------------------------------------------------------------------------- +-- Special folds +-------------------------------------------------------------------------------- +concat : List (List a) -> List a +concat = foldr (++) [] + +concatMap : (a -> List b) -> List a -> List b +concatMap f [] = [] +concatMap f (x::xs) = f x ++ concatMap f xs + +and : List Bool -> Bool +and = foldr (&&) True + +or : List Bool -> Bool +or = foldr (||) False + +any : (a -> Bool) -> List a -> Bool +any p = or . map p + +all : (a -> Bool) -> List a -> Bool +all p = and . map p + +-------------------------------------------------------------------------------- +-- Transformations +-------------------------------------------------------------------------------- + +reverse : List a -> List a +reverse = reverse' [] + where + reverse' : List a -> List a -> List a + reverse' acc [] = acc + reverse' acc (x::xs) = reverse' (x::acc) xs + +intersperse : a -> List a -> List a +intersperse sep [] = [] +intersperse sep (x::xs) = x :: intersperse' sep xs + where + intersperse' : a -> List a -> List a + intersperse' sep [] = [] + intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys + +intercalate : List a -> List (List a) -> List a +intercalate sep l = concat $ intersperse sep l + +-------------------------------------------------------------------------------- +-- Membership tests +-------------------------------------------------------------------------------- + +elemBy : (a -> a -> Bool) -> a -> List a -> Bool +elemBy p e [] = False +elemBy p e (x::xs) = + if p e x then + True + else + elemBy p e xs + elem : Eq a => a -> List a -> Bool -elem x [] = False -elem x (y :: ys) = if (x == y) then True else (elem x ys) +elem = elemBy (==) -lookup : Eq k => k -> List (k, v) -> Maybe v -lookup k [] = Nothing -lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs) +lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b +lookupBy p e [] = Nothing +lookupBy p e (x::xs) = + let (l, r) = x in + if p e l then + Just r + else + lookupBy p e xs -sort : Ord a => List a -> List a -sort [] = [] -sort [x] = [x] -sort xs = let (x, y) = split xs in - merge (sort x) (sort y) where - splitrec : List a -> List a -> (List a -> List a) -> (List a, List a) - splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y)) - splitrec _ ys zs = (zs [], ys) +lookup : Eq a => a -> List (a, b) -> Maybe b +lookup = lookupBy (==) - split : List a -> (List a, List a) - split xs = splitrec xs xs id +hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool +hasAnyBy p elems [] = False +hasAnyBy p elems (x::xs) = + if elemBy p x elems then + True + else + hasAnyBy p elems xs - merge : Ord a => List a -> List a -> List a - merge xs [] = xs - merge [] ys = ys - merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys)) - else (y :: merge (x :: xs) ys) +hasAny : Eq a => List a -> List a -> Bool +hasAny = hasAnyBy (==) +-------------------------------------------------------------------------------- +-- Searching with a predicate +-------------------------------------------------------------------------------- + +find : (a -> Bool) -> List a -> Maybe a +find p [] = Nothing +find p (x::xs) = + if p x then + Just x + else + find p xs + +findIndex : (a -> Bool) -> List a -> Maybe Nat +findIndex = findIndex' 0 + where + findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat + findIndex' cnt p [] = Nothing + findIndex' cnt p (x::xs) = + if p x then + Just cnt + else + findIndex' (S cnt) p xs + +findIndices : (a -> Bool) -> List a -> List Nat +findIndices = findIndices' 0 + where + findIndices' : Nat -> (a -> Bool) -> List a -> List Nat + findIndices' cnt p [] = [] + findIndices' cnt p (x::xs) = + if p x then + cnt :: findIndices' (S cnt) p xs + else + findIndices' (S cnt) p xs + +elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat +elemIndexBy p e = findIndex $ p e + +elemIndex : Eq a => a -> List a -> Maybe Nat +elemIndex = elemIndexBy (==) + +elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat +elemIndicesBy p e = findIndices $ p e + +elemIndices : Eq a => a -> List a -> List Nat +elemIndices = elemIndicesBy (==) + +-------------------------------------------------------------------------------- +-- Filters +-------------------------------------------------------------------------------- + +filter : (a -> Bool) -> List a -> List a +filter p [] = [] +filter p (x::xs) = + if p x then + x :: filter p xs + else + filter p xs + +nubBy : (a -> a -> Bool) -> List a -> List a +nubBy = nubBy' [] + where + nubBy' : List a -> (a -> a -> Bool) -> List a -> List a + nubBy' acc p [] = [] + nubBy' acc p (x::xs) = + if elemBy p x acc then + nubBy' acc p xs + else + x :: nubBy' (x::acc) p xs + +nub : Eq a => List a -> List a +nub = nubBy (==) + +-------------------------------------------------------------------------------- +-- Splitting and breaking lists +-------------------------------------------------------------------------------- + span : (a -> Bool) -> List a -> (List a, List a) -span p [] = ([], []) -span p (x :: xs) with (p x) - | True with (span p xs) - | (ys, zs) = (x :: ys, zs) - | False = ([], x :: xs) +span p [] = ([], []) +span p (x::xs) = + if p x then + let (ys, zs) = span p xs in + (x::ys, zs) + else + ([], x::xs) break : (a -> Bool) -> List a -> (List a, List a) break p = span (not . p) - + split : (a -> Bool) -> List a -> List (List a) split p [] = [] -split p xs = case break p xs of - (chunk, []) => [chunk] - (chunk, (c :: rest)) => chunk :: split p rest +split p xs = + case break p xs of + (chunk, []) => [chunk] + (chunk, (c :: rest)) => chunk :: split p rest + +partition : (a -> Bool) -> List a -> (List a, List a) +partition p [] = ([], []) +partition p (x::xs) = + let (lefts, rights) = partition p xs in + if p x then + (x::lefts, rights) + else + (lefts, x::rights) + +-------------------------------------------------------------------------------- +-- Predicates +-------------------------------------------------------------------------------- + +isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool +isPrefixOfBy p [] right = True +isPrefixOfBy p left [] = False +isPrefixOfBy p (x::xs) (y::ys) = + if p x y then + isPrefixOfBy p xs ys + else + False + +isPrefixOf : Eq a => List a -> List a -> Bool +isPrefixOf = isPrefixOfBy (==) + +isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool +isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) + +isSuffixOf : Eq a => List a -> List a -> Bool +isSuffixOf = isSuffixOfBy (==) + +-------------------------------------------------------------------------------- +-- Sorting +-------------------------------------------------------------------------------- + +sorted : Ord a => List a -> Bool +sorted [] = True +sorted (x::xs) = + case xs of + Nil => True + (y::ys) => x <= y && sorted (y::ys) + +mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a +mergeBy order [] right = right +mergeBy order left [] = left +mergeBy order (x::xs) (y::ys) = + case order x y of + LT => x :: mergeBy order xs (y::ys) + _ => y :: mergeBy order (x::xs) ys + +merge : Ord a => List a -> List a -> List a +merge = mergeBy compare + +sort : Ord a => List a -> List a +sort [] = [] +sort [x] = [x] +sort xs = + let (x, y) = split xs in + merge (sort x) (sort y) + where + splitRec : List a -> List a -> (List a -> List a) -> (List a, List a) + splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y)) + splitRec _ ys zs = (zs [], ys) + + split : List a -> (List a, List a) + split xs = splitRec xs xs id + +-------------------------------------------------------------------------------- +-- Conversions +-------------------------------------------------------------------------------- + +maybeToList : Maybe a -> List a +maybeToList Nothing = [] +maybeToList (Just j) = [j] + +listToMaybe : List a -> Maybe a +listToMaybe [] = Nothing +listToMaybe (x::xs) = Just x + +-------------------------------------------------------------------------------- +-- Misc +-------------------------------------------------------------------------------- + +catMaybes : List (Maybe a) -> List a +catMaybes [] = [] +catMaybes (x::xs) = + case x of + Nothing => catMaybes xs + Just j => j :: catMaybes xs + +-------------------------------------------------------------------------------- +-- Instances +-------------------------------------------------------------------------------- + +instance (Eq a) => Eq (List a) where + (==) [] [] = True + (==) (a::restA) (b::restB) = + if a == b + then restA == restB + else False + (==) _ _ = False + + +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 + +-------------------------------------------------------------------------------- +-- Properties +-------------------------------------------------------------------------------- + +mapPreservesLength : (f : a -> b) -> (l : List a) -> + length (map f l) = length l +mapPreservesLength f [] = refl +mapPreservesLength f (x::xs) = + let inductiveHypothesis = mapPreservesLength f xs in + ?mapPreservesLengthStepCase + +mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) -> + map f (l ++ r) = map f l ++ map f r +mapDistributesOverAppend f [] r = refl +mapDistributesOverAppend f (x::xs) r = + let inductiveHypothesis = mapDistributesOverAppend f xs r in + ?mapDistributesOverAppendStepCase + +mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) -> + map f (map g l) = map (f . g) l +mapFusion f g [] = refl +mapFusion f g (x::xs) = + 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 + +hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) -> + hasAnyBy p [] l = False +hasAnyByNilFalse p [] = refl +hasAnyByNilFalse p (x::xs) = + 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 +-------------------------------------------------------------------------------- + +lengthAppendStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +hasAnyNilFalseBody = proof { + intros; + rewrite (hasAnyByNilFalse (==) l); + trivial; +} + +hasAnyByNilFalseStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +initProof = proof { + intros; + trivial; +} + +lastProof = proof { + intros; + trivial; +} + +appendNilRightNeutralStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +appendAssociativeStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +mapFusionStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +mapDistributesOverAppendStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +mapPreservesLengthStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} diff --git a/lib/prelude/maybe.idr b/lib/prelude/maybe.idr --- a/lib/prelude/maybe.idr +++ b/lib/prelude/maybe.idr @@ -1,12 +1,43 @@ module prelude.maybe -data Maybe a = Nothing | Just a +import builtins +data Maybe a + = Nothing + | Just a + +-------------------------------------------------------------------------------- +-- Syntactic tests +-------------------------------------------------------------------------------- + +isNothing : Maybe a -> Bool +isNothing Nothing = True +isNothing (Just j) = False + +isJust : Maybe a -> Bool +isJust Nothing = False +isJust (Just j) = True + +-------------------------------------------------------------------------------- +-- Misc +-------------------------------------------------------------------------------- + maybe : |(def : b) -> (a -> b) -> Maybe a -> b maybe n j Nothing = n maybe n j (Just x) = j x +fromMaybe : |(def: a) -> Maybe a -> a +fromMaybe def Nothing = def +fromMaybe def (Just j) = j + +toMaybe : Bool -> a -> Maybe a +toMaybe True j = Just j +toMaybe False j = Nothing + +-------------------------------------------------------------------------------- +-- Class instances +-------------------------------------------------------------------------------- + maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b -maybe_bind Nothing k = Nothing +maybe_bind Nothing k = Nothing maybe_bind (Just x) k = k x - diff --git a/lib/prelude/monad.idr b/lib/prelude/monad.idr --- a/lib/prelude/monad.idr +++ b/lib/prelude/monad.idr @@ -3,6 +3,7 @@ -- Monads and Functors import builtins +import prelude.list %access public diff --git a/lib/prelude/nat.idr b/lib/prelude/nat.idr --- a/lib/prelude/nat.idr +++ b/lib/prelude/nat.idr @@ -1,124 +1,750 @@ module prelude.nat import builtins + +import prelude.algebra import prelude.cast %access public -data Nat = O | S Nat +data Nat + = O + | S Nat -instance Cast Nat Int where - cast O = 0 - cast (S k) = 1 + cast k +-------------------------------------------------------------------------------- +-- Syntactic tests +-------------------------------------------------------------------------------- -plus : Nat -> Nat -> Nat -plus O y = y -plus (S k) y = S (plus k y) +isZero : Nat -> Bool +isZero O = True +isZero (S n) = False -eqRespS : m = n -> S m = S n -eqRespS refl = refl +isSucc : Nat -> Bool +isSucc O = False +isSucc (S n) = True -eqRespS' : S m = S n -> m = n -eqRespS' refl = refl +-------------------------------------------------------------------------------- +-- Basic arithmetic functions +-------------------------------------------------------------------------------- -sub : Nat -> Nat -> Nat -sub O y = O -sub (S k) (S y) = sub k y -sub x O = x +plus : Nat -> Nat -> Nat +plus O right = right +plus (S left) right = S (plus left right) mult : Nat -> Nat -> Nat -mult O y = O -mult (S k) y = plus y (mult k y) +mult O right = O +mult (S left) right = plus right $ mult left right -instance Eq Nat where - O == O = True - (S x) == (S y) = x == y - O == (S y) = False - (S x) == O = False +minus : Nat -> Nat -> Nat +minus O right = O +minus left O = left +minus (S left) (S right) = minus left right +power : Nat -> Nat -> Nat +power base O = S O +power base (S exp) = mult base $ power base exp + +-------------------------------------------------------------------------------- +-- Type class instances +-------------------------------------------------------------------------------- + +instance Eq Nat where + O == O = True + (S l) == (S r) = l == r + _ == _ = False + +instance Cast Nat Int where + cast O = 0 + cast (S k) = 1 + cast k + instance Ord Nat where - compare O O = EQ - compare O (S k) = LT - compare (S k) O = GT - compare (S x) (S y) = compare x y + compare O O = EQ + compare O (S k) = LT + compare (S k) O = GT + compare (S x) (S y) = compare x y instance Num Nat where - (+) = plus - (-) = sub - (*) = mult + (+) = plus + (-) = minus + (*) = mult - fromInteger 0 = O - fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O + fromInteger = intToNat where + %assert_total + intToNat : Int -> Nat + intToNat 0 = O + intToNat n = if (n > 0) then S (fromInteger (n-1)) else O -plusnO : (m : Nat) -> m + O = m -plusnO O = refl -plusnO (S k) = eqRespS (plusnO k) +-------------------------------------------------------------------------------- +-- Division and modulus +-------------------------------------------------------------------------------- -plusn_Sm : (n, m : Nat) -> (plus n (S m)) = S (plus n m) -plusn_Sm O m = refl -plusn_Sm (S j) m = eqRespS (plusn_Sm _ _) +-------------------------------------------------------------------------------- +-- Auxilliary notions +-------------------------------------------------------------------------------- -plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n -plus_commutes O m = sym (plusnO m) -plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk +pred : Nat -> Nat +pred O = O +pred (S n) = n -plus_commutes_Sk = proof { +-------------------------------------------------------------------------------- +-- Fibonacci and factorial +-------------------------------------------------------------------------------- + +fib : Nat -> Nat +fib O = 0 +fib (S O) = 1 +fib (S (S n)) = fib (S n) + fib n + +-------------------------------------------------------------------------------- +-- GCD and LCM +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- Comparisons +-------------------------------------------------------------------------------- + +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 + +maximum : Nat -> Nat -> Nat +maximum left right = + if lte left right then + right + else + left + +-------------------------------------------------------------------------------- +-- Properties +-------------------------------------------------------------------------------- + +-- Succ +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) -> + left = right +succInjective left right refl = refl + +-- Plus +plusZeroLeftNeutral : (right : Nat) -> 0 + right = right +plusZeroLeftNeutral right = refl + +plusZeroRightNeutral : (left : Nat) -> left + 0 = left +plusZeroRightNeutral O = refl +plusZeroRightNeutral (S n) = + let inductiveHypothesis = plusZeroRightNeutral n in + ?plusZeroRightNeutralStepCase + +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) -> + 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) -> + 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) -> + (p : left = right) -> left + c = right + c +plusConstantRight left right c refl = refl + +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 +plusOneSucc n = refl + +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) -> + (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) -> + (p : left + right = left) -> right = O +plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase +plusLeftLeftRightZero (S left) right p = + let inductiveHypothesis = plusLeftLeftRightZero left right in + ?plusLeftLeftRightZeroStepCase + +-- Mult +multZeroLeftZero : (right : Nat) -> O * right = O +multZeroLeftZero right = refl + +multZeroRightZero : (left : Nat) -> left * O = O +multZeroRightZero O = refl +multZeroRightZero (S left) = + let inductiveHypothesis = multZeroRightZero left in + ?multZeroRightZeroStepCase + +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) -> + (S left) * right = right + (left * right) +multLeftSuccPlus left right = refl + +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) -> + 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) -> + (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) -> + 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 +multOneLeftNeutral O = refl +multOneLeftNeutral (S right) = + let inductiveHypothesis = multOneLeftNeutral right in + ?multOneLeftNeutralStepCase + +multOneRightNeutral : (left : Nat) -> left * 1 = left +multOneRightNeutral O = refl +multOneRightNeutral (S left) = + let inductiveHypothesis = multOneRightNeutral left in + ?multOneRightNeutralStepCase + +-- Minus +minusSuccSucc : (left : Nat) -> (right : Nat) -> + (S left) - (S right) = left - right +minusSuccSucc left right = refl + +minusZeroLeft : (right : Nat) -> 0 - right = O +minusZeroLeft right = refl + +minusZeroRight : (left : Nat) -> left - 0 = left +minusZeroRight O = refl +minusZeroRight (S left) = refl + +minusZeroN : (n : Nat) -> O = n - n +minusZeroN O = refl +minusZeroN (S n) = minusZeroN n + +minusOneSuccN : (n : Nat) -> S O = (S n) - n +minusOneSuccN O = refl +minusOneSuccN (S n) = minusOneSuccN n + +minusSuccOne : (n : Nat) -> S n - 1 = n +minusSuccOne O = refl +minusSuccOne (S n) = refl + +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) -> + left - centre - right = left - (centre + right) +minusMinusMinusPlus O O right = refl +minusMinusMinusPlus (S left) O right = refl +minusMinusMinusPlus O (S centre) right = refl +minusMinusMinusPlus (S left) (S centre) right = + let inductiveHypothesis = minusMinusMinusPlus left centre right in + ?minusMinusMinusPlusStepCase + +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) -> + (left - centre) * right = (left * right) - (centre * right) +multDistributesOverMinusLeft O O right = refl +multDistributesOverMinusLeft (S left) O right = + ?multDistributesOverMinusLeftBaseCase +multDistributesOverMinusLeft O (S centre) right = refl +multDistributesOverMinusLeft (S left) (S centre) right = + let inductiveHypothesis = multDistributesOverMinusLeft left centre right in + ?multDistributesOverMinusLeftStepCase + +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) = + base * (power base exp) +powerSuccPowerLeft base exp = refl + +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 +powerZeroOne base = refl + +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 +powerOneSuccOne O = refl +powerOneSuccOne (S exp) = + let inductiveHypothesis = powerOneSuccOne exp in + ?powerOneSuccOneStepCase + +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) -> + power (power base exp) exp' = power base (exp * exp') +powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase +powerPowerMultPower base exp (S exp') = + let inductiveHypothesis = powerPowerMultPower base exp exp' in + ?powerPowerMultPowerStepCase + +-- Pred +predSucc : (n : Nat) -> pred (S n) = n +predSucc n = refl + +minusSuccPred : (left : Nat) -> (right : Nat) -> + left - (S right) = pred (left - right) +minusSuccPred O right = refl +minusSuccPred (S left) O = + let inductiveHypothesis = minusSuccPred left O in + ?minusSuccPredStepCase +minusSuccPred (S left) (S right) = + let inductiveHypothesis = minusSuccPred left right in + ?minusSuccPredStepCase' + +-- boolElim +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) -> + 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) -> + (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) -> + 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) -> + (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 +lteNTrue O = refl +lteNTrue (S n) = lteNTrue n + +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 +minimumZeroZeroRight O = refl +minimumZeroZeroRight (S right) = minimumZeroZeroRight right + +minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O +minimumZeroZeroLeft O = refl +minimumZeroZeroLeft (S left) = refl + +minimumSuccSucc : (left : Nat) -> (right : Nat) -> + minimum (S left) (S right) = S (minimum left right) +minimumSuccSucc O O = refl +minimumSuccSucc (S left) O = refl +minimumSuccSucc O (S right) = refl +minimumSuccSucc (S left) (S right) = + let inductiveHypothesis = minimumSuccSucc left right in + ?minimumSuccSuccStepCase + +minimumCommutative : (left : Nat) -> (right : Nat) -> + minimum left right = minimum right left +minimumCommutative O O = refl +minimumCommutative O (S right) = refl +minimumCommutative (S left) O = refl +minimumCommutative (S left) (S right) = + let inductiveHypothesis = minimumCommutative left right in + ?minimumCommutativeStepCase + +maximumZeroNRight : (right : Nat) -> maximum O right = right +maximumZeroNRight O = refl +maximumZeroNRight (S right) = refl + +maximumZeroNLeft : (left : Nat) -> maximum left O = left +maximumZeroNLeft O = refl +maximumZeroNLeft (S left) = refl + +maximumSuccSucc : (left : Nat) -> (right : Nat) -> + S (maximum left right) = maximum (S left) (S right) +maximumSuccSucc O O = refl +maximumSuccSucc (S left) O = refl +maximumSuccSucc O (S right) = refl +maximumSuccSucc (S left) (S right) = + let inductiveHypothesis = maximumSuccSucc left right in + ?maximumSuccSuccStepCase + +maximumCommutative : (left : Nat) -> (right : Nat) -> + maximum left right = maximum right left +maximumCommutative O O = refl +maximumCommutative (S left) O = refl +maximumCommutative O (S right) = refl +maximumCommutative (S left) (S right) = + let inductiveHypothesis = maximumCommutative left right in + ?maximumCommutativeStepCase + +-------------------------------------------------------------------------------- +-- Proofs +-------------------------------------------------------------------------------- + +powerPowerMultPowerStepCase = proof { intros; - refine sym; - rewrite sym ih; - rewrite plusn_Sm m k; + rewrite sym inductiveHypothesis; + rewrite sym (multRightSuccPlus exp exp'); + rewrite (multPowerPowerPlus base exp (mult exp exp')); trivial; } -plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p -plus_assoc O m p = refl -plus_assoc (S k) m p = let ih = plus_assoc k m p in eqRespS ih +powerPowerMultPowerBaseCase = proof { + intros; + rewrite sym (multZeroRightZero exp); + trivial; +} -data Cmp : Nat -> Nat -> Set where - cmpLT : (y : Nat) -> Cmp x (x + S y) - cmpEQ : Cmp x x - cmpGT : (x : Nat) -> Cmp (y + S x) y - -cmp : (n, m : Nat) -> Cmp n m -cmp O O = cmpEQ -cmp (S n) O = cmpGT _ -cmp O (S n) = cmpLT _ -cmp (S x) (S y) with (cmp x y) - cmp (S x) (S x) | cmpEQ = cmpEQ - cmp (S (y + S x)) (S y) | cmpGT _ = cmpGT _ - cmp (S x) (S (x + S y)) | cmpLT _ = cmpLT _ - -multnO : (n : Nat) -> (n * O) = O -multnO O = refl -multnO (S k) = multnO k +powerSuccSuccMultStepCase = proof { + intros; + rewrite (multOneRightNeutral base); + rewrite sym (multOneRightNeutral base); + trivial; +} -multn_Sm : (n, m : Nat) -> n * S m = n + n * m -multn_Sm O m = refl -multn_Sm (S k) m = let ih = multn_Sm k m in ?multnSmSk +powerOneSuccOneStepCase = proof { + intros; + rewrite inductiveHypothesis; + rewrite sym (plusZeroRightNeutral (power (S O) exp)); + trivial; +} -mult_commutes : (n, m : Nat) -> n * m = m * n -mult_commutes O m = ?mult_commO -mult_commutes (S k) m = let ih = mult_commutes k m in ?mult_commSk +powerOneNeutralStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} -mult_commSk = proof { +multAssociativeStepCase = proof { intros; - rewrite sym ih; - rewrite multn_Sm m k; + rewrite sym (multDistributesOverPlusLeft centre (mult left centre) right); + rewrite inductiveHypothesis; trivial; } -mult_commO = proof { - intro; - rewrite multnO m; +minusSuccPredStepCase' = proof { + intros; + rewrite sym inductiveHypothesis; trivial; } -multnSmSk = proof { +minusSuccPredStepCase = proof { intros; - rewrite plus_commutes (mult k m) m; - rewrite sym (plus_assoc k (mult k m) m); - rewrite ih; - rewrite plus_commutes m (mult k (S m)); + rewrite (minusZeroRight left); + trivial; +} + +multPowerPowerPlusStepCase = proof { + intros; + rewrite inductiveHypothesis; + rewrite (multAssociative base (power base exp) (power base exp')); + trivial; +} + +multPowerPowerPlusBaseCase = proof { + intros; + rewrite (plusZeroRightNeutral (power base exp')); + trivial; +} + +multOneRightNeutralStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +multOneLeftNeutralStepCase = proof { + intros; + rewrite (plusZeroRightNeutral right); + trivial; +} + +multDistributesOverPlusLeftStepCase = proof { + intros; + rewrite sym inductiveHypothesis; + rewrite sym (plusAssociative right (mult left right) (mult centre right)); + trivial; +} + +multDistributesOverPlusRightStepCase = proof { + intros; + rewrite sym inductiveHypothesis; + rewrite sym (plusAssociative (plus centre (mult left centre)) right (mult left right)); + rewrite (plusAssociative centre (mult left centre) right); + rewrite sym (plusCommutative (mult left centre) right); + rewrite sym (plusAssociative centre right (mult left centre)); + rewrite sym (plusAssociative (plus centre right) (mult left centre) (mult left right)); + trivial; +} + +multCommutativeStepCase = proof { + intros; + rewrite sym (multRightSuccPlus right left); + rewrite inductiveHypothesis; + trivial; +} + +multCommutativeBaseCase = proof { + intros; + rewrite (multZeroRightZero right); + trivial; +} + +multRightSuccPlusStepCase = proof { + intros; + rewrite inductiveHypothesis; + rewrite sym inductiveHypothesis; + rewrite sym (plusAssociative right left (mult left right)); + rewrite sym (plusCommutative right left); + rewrite (plusAssociative left right (mult left right)); + trivial; +} + +multZeroRightZeroStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +plusAssociativeStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +plusCommutativeStepCase = proof { + intros; + rewrite (plusSuccRightSucc right left); + rewrite inductiveHypothesis; + trivial; +} + +plusSuccRightSuccStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +plusCommutativeBaseCase = proof { + intros; + rewrite sym (plusZeroRightNeutral right); + trivial; +} + +plusZeroRightNeutralStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +maximumCommutativeStepCase = proof { + intros; + rewrite (boolElimSuccSucc (lte left right) right left); + rewrite (boolElimSuccSucc (lte right left) left right); + rewrite inductiveHypothesis; + trivial; +} + +maximumSuccSuccStepCase = proof { + intros; + rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left)); + trivial; +} + +minimumCommutativeStepCase = proof { + intros; + rewrite (boolElimSuccSucc (lte left right) left right); + rewrite (boolElimSuccSucc (lte right left) right left); + rewrite inductiveHypothesis; + trivial; +} + +minimumSuccSuccStepCase = proof { + intros; + rewrite (boolElimSuccSucc (lte left right) (S left) (S right)); + trivial; +} + +multDistributesOverMinusRightBody = proof { + intros; + rewrite sym (multCommutative left (minus centre right)); + rewrite sym (multDistributesOverMinusLeft centre right left); + rewrite sym (multCommutative centre left); + rewrite sym (multCommutative right left); + trivial; +} + +multDistributesOverMinusLeftStepCase = proof { + intros; + rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right)); + trivial; +} + +multDistributesOverMinusLeftBaseCase = proof { + intros; + rewrite (minusZeroRight (plus right (mult left right))); + trivial; +} + +plusMinusLeftCancelStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +minusMinusMinusPlusStepCase = proof { + intros; + rewrite inductiveHypothesis; + trivial; +} + +plusLeftLeftRightZeroBaseCase = proof { + intros; + rewrite p; + trivial; +} + +plusLeftLeftRightZeroStepCase = proof { + intros; + refine inductiveHypothesis; + let p' = succInjective (plus left right) left p; + rewrite p'; + trivial; +} + +plusRightCancelStepCase = proof { + intros; + refine inductiveHypothesis; + refine succInjective; + rewrite sym (plusSuccRightSucc left right); + rewrite sym (plusSuccRightSucc left' right); + rewrite p; + trivial; +} + +plusRightCancelBaseCase = proof { + intros; + rewrite (plusZeroRightNeutral left); + rewrite (plusZeroRightNeutral left'); + rewrite p; + trivial; +} + +plusLeftCancelStepCase = proof { + intros; + let injectiveProof = succInjective (plus left right) (plus left right') p; + rewrite (inductiveHypothesis injectiveProof); + trivial; +} + +plusLeftCancelBaseCase = proof { + intros; + rewrite p; trivial; } diff --git a/lib/prelude/strings.idr b/lib/prelude/strings.idr --- a/lib/prelude/strings.idr +++ b/lib/prelude/strings.idr @@ -21,7 +21,7 @@ strM : (x : String) -> StrM x strM x with (choose (not (x == ""))) - strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p)) + strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p) strM x | (Right p) = believe_me StrNil unpack : String -> List Char @@ -60,5 +60,5 @@ = if (isSpace x) then (ltrim xs) else (strCons x xs) trim : String -> String -trim xs = ltrim (rev (ltrim (rev xs))) +trim xs = ltrim (reverse (ltrim (reverse xs))) diff --git a/lib/prelude/vect.idr b/lib/prelude/vect.idr --- a/lib/prelude/vect.idr +++ b/lib/prelude/vect.idr @@ -5,7 +5,7 @@ %access public -infixr 7 :: +infixr 10 :: data Vect : Set -> Nat -> Set where Nil : Vect a O @@ -20,9 +20,9 @@ lookup fO [] impossible lookup (fS _) [] impossible -app : Vect a n -> Vect a m -> Vect a (n + m) -app [] ys = ys -app (x :: xs) ys = x :: app xs ys +(++) : Vect a n -> Vect a m -> Vect a (n + m) +(++) [] ys = ys +(++) (x :: xs) ys = x :: xs ++ ys filter : (a -> Bool) -> Vect a n -> (p ** Vect a p) filter p [] = ( _ ** [] ) @@ -34,8 +34,8 @@ map f [] = [] map f (x :: xs) = f x :: map f xs -rev : Vect a n -> Vect a n -rev xs = revAcc [] xs where +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 @@ -44,13 +44,13 @@ revAcc_lemma_2 = proof { intros; - rewrite sym (plusn_Sm n k); + rewrite plusSuccRightSucc n k; exact value; } revAcc_lemma_1 = proof { intros; - rewrite sym (plusnO n); + rewrite sym (plusZeroRightNeutral n); exact value; } diff --git a/lib/system.idr b/lib/system.idr --- a/lib/system.idr +++ b/lib/system.idr @@ -15,7 +15,7 @@ getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x ga' : List String -> Int -> Int -> IO (List String) - ga' acc i n = if (i == n) then (return $ rev acc) else + ga' acc i n = if (i == n) then (return $ reverse acc) else do arg <- getArg i ga' (arg :: acc) (i+1) n diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs --- a/src/Core/CaseTree.hs +++ b/src/Core/CaseTree.hs @@ -1,12 +1,14 @@ module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree, - simpleCase, small) where + simpleCase, small, namesUsed) where import Core.TT import Control.Monad.State +import Data.Maybe +import Data.List hiding (partition) import Debug.Trace -data CaseDef = CaseDef [Name] SC +data CaseDef = CaseDef [Name] SC [Term] deriving Show data SC = Case Name [CaseAlt] @@ -26,23 +28,40 @@ !-} type CaseTree = SC -type Clause = ([Pat], Term) -type CS = Int +type Clause = ([Pat], (Term, Term)) +type CS = ([Term], Int) -- simple terms can be inlined trivially - good for primitives in particular small :: SC -> Bool -- small (STerm t) = True small _ = False +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 _ = [] + + nua ps (ConCase n i args sc) = nu' (ps ++ args) sc + nua ps (ConstCase _ sc) = nu' ps sc + nua ps (DefaultCase sc) = nu' ps sc + + nut ps (P _ n _) | n `elem` ps = [] + | otherwise = [n] + nut ps (App f a) = nut ps f ++ nut ps a + nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc + nut ps (Bind n b sc) = nut (n:ps) sc + nut ps _ = [] + simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef simpleCase tc cover [] - = CaseDef [] (UnmatchedCase "No pattern clauses") + = CaseDef [] (UnmatchedCase "No pattern clauses") [] simpleCase tc cover cs - = let pats = map (\ (l, r) -> (toPats tc l, r)) cs - numargs = length (fst (head pats)) - ns = take numargs args - tree = evalState (match ns pats (defaultCase cover)) numargs in - CaseDef ns (prune tree) + = let pats = map (\ (l, r) -> (toPats tc l, (l, r))) cs + numargs = length (fst (head pats)) + ns = take numargs args + (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in + CaseDef ns (prune tree) (fst st) where args = map (\i -> MN i "e") [0..] defaultCase True = STerm Erased defaultCase False = UnmatchedCase "Error" @@ -109,8 +128,12 @@ match :: [Name] -> [Clause] -> SC -- error case -> State CS SC -match [] (([], ret) : _) err = return $ STerm ret -- run out of arguments -match vs cs err = mixture vs (partition cs) err +match [] (([], ret) : xs) err + = do (ts, v) <- get + put (ts ++ (map (fst.snd) xs), v) + return $ STerm (snd ret) -- run out of arguments +match vs cs err = do cs <- mixture vs (partition cs) err + return cs mixture :: [Name] -> [Partition] -> SC -> State CS SC mixture vs [] err = return err @@ -166,7 +189,7 @@ addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs) getVar :: State CS Name -getVar = do v <- get; put (v+1); return (MN v "e") +getVar = do (t, v) <- get; put (t, v+1); return (MN v "e") groupCons :: [Clause] -> State CS [Group] groupCons cs = gc [] cs @@ -195,7 +218,7 @@ do let alts' = map (repVar v) alts match vs alts' err where - repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res) + repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res)) repVar v (PAny : ps , res) = (ps, res) prune :: SC -> SC @@ -205,7 +228,7 @@ case alts' of [] -> STerm Erased as -> Case n as - where pruneAlt (ConCase n i ns sc) = ConCase n i ns (prune sc) + where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune sc) pruneAlt (ConstCase c sc) = ConstCase c (prune sc) pruneAlt (DefaultCase sc) = DefaultCase (prune sc) diff --git a/src/Core/CoreParser.hs b/src/Core/CoreParser.hs --- a/src/Core/CoreParser.hs +++ b/src/Core/CoreParser.hs @@ -19,9 +19,9 @@ opLetter = iOpLetter, identLetter = identLetter haskellDef <|> lchar '.', reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"], - reservedNames = ["let", "in", "data", "Set", + reservedNames = ["let", "in", "data", "record", "Set", "do", "dsl", "import", "impossible", - "case", "of", + "case", "of", "total", "infix", "infixl", "infixr", "prefix", "where", "with", "forall", "syntax", "proof", "using", "params", "namespace", "class", "instance", diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs --- a/src/Core/Elaborate.hs +++ b/src/Core/Elaborate.hs @@ -427,7 +427,11 @@ OK (v, s') -> tryAll' ((do put s' return v):cs) f xs Error err -> do put s - tryAll' cs (better err f) xs + if (score err) < 100 + then + tryAll' cs (better err f) xs + else + tryAll' [] (better err f) xs -- give up better err (f, i) = let s = score err in if (s >= i) then (lift (tfail err), s) diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -2,12 +2,13 @@ PatternGuards #-} module Core.Evaluate(normalise, normaliseC, normaliseAll, - simplify, specialise, hnf, - Def(..), Accessibility(..), + simplify, specialise, hnf, convEq, convEq', + Def(..), Accessibility(..), Totality(..), PReason(..), Context, initContext, ctxtAlist, uconstraints, next_tvar, - addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype, + addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype, addCasedef, addOperator, - lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName, + lookupTy, lookupP, lookupDef, lookupVal, lookupTotal, + lookupTyEnv, isConName, Value(..)) where import Debug.Trace @@ -423,6 +424,56 @@ getValArgs (HApp t env args) = (t, env, args) getValArgs t = (t, [], []) +convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, []) + +convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool +convEq ctxt = ceq [] where + ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool + ceq ps (P xt x _) (P yt y _) + | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True + | otherwise = sameDefs ps x y + ceq ps (V x) (V y) = return (x == y) + ceq ps (Bind _ xb xs) (Bind _ yb ys) + = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys) + where + ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') + ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') + ceqB ps b b' = ceq ps (binderTy b) (binderTy b') + ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay) + ceq ps (Constant x) (Constant y) = return (x == y) + ceq ps (Set x) (Set y) = do (v, cs) <- get + put (v, ULE x y : cs) + return True + ceq ps Erased _ = return True + ceq ps _ Erased = return True + ceq ps _ _ = return False + + caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs' + where + caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest') + = do q1 <- caseeq (zip as as' ++ ps) sc sc' + q2 <- caseeqA ps rest rest' + return $ x == x' && i == i' && q1 && q2 + caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest') + = do q1 <- caseeq ps sc sc' + q2 <- caseeqA ps rest rest' + return $ x == x' && q1 && q2 + caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest') + = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest') + caseeqA ps [] [] = return True + caseeqA ps _ _ = return False + caseeq ps (STerm x) (STerm y) = ceq ps x y + caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True + caseeq ps _ _ = return False + + sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of + ([Function _ xdef], [Function _ ydef]) + -> ceq ((x,y):ps) xdef ydef + ([CaseOp _ _ _ _ xdef _ _], + [CaseOp _ _ _ _ ydef _ _]) + -> caseeq ((x,y):ps) xdef ydef + _ -> return False + -- SPECIALISATION ----------------------------------------------------------- -- We need too much control to be able to do this by tweaking the main -- evaluator @@ -470,42 +521,76 @@ data Accessibility = Public | Frozen | Hidden deriving (Show, Eq) + +data Totality = Total [Int] -- well-founded arguments + | Partial PReason + | Unchecked + deriving Eq + +data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name + | Mutual [Name] + deriving (Show, Eq) + +instance Show Totality where + show (Total args)= "Total" -- ++ show args ++ " decreasing arguments" + show Unchecked = "not yet checked for totality" + show (Partial Itself) = "possibly not total as it is not well founded" + show (Partial NotCovering) = "not total as there are missing cases" + show (Partial NotPositive) = "not strictly positive" + show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns) + show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++ + showSep " --> " (map show ns) + {-! deriving instance Binary Accessibility !-} +{-! +deriving instance Binary Totality +!-} + +{-! +deriving instance Binary PReason +!-} + data Context = MkContext { uconstraints :: [UConstraint], next_tvar :: Int, - definitions :: Ctxt (Def, Accessibility) } + definitions :: Ctxt (Def, Accessibility, Totality) } initContext = MkContext [] 0 emptyContext ctxtAlist :: Context -> [(Name, Def)] -ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt) +ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt) veval ctxt env t = evalState (eval ctxt emptyContext env t []) () addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt = let ctxt = definitions uctxt - ctxt' = addDef n (Function ty tm, Public) ctxt in + ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in uctxt { definitions = ctxt' } setAccess :: Name -> Accessibility -> Context -> Context setAccess n a uctxt = let ctxt = definitions uctxt - ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in + ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in uctxt { definitions = ctxt' } +setTotal :: Name -> Totality -> Context -> Context +setTotal n t uctxt + = let ctxt = definitions uctxt + ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in + uctxt { definitions = ctxt' } + addCtxtDef :: Name -> Def -> Context -> Context addCtxtDef n d c = let ctxt = definitions c - ctxt' = addDef n (d, Public) ctxt in + ctxt' = addDef n (d, Public, Unchecked) ctxt in c { definitions = ctxt' } addTyDecl :: Name -> Type -> Context -> Context addTyDecl n ty uctxt = let ctxt = definitions uctxt - ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in + ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in uctxt { definitions = ctxt' } addDatatype :: Datatype Name -> Context -> Context @@ -513,14 +598,14 @@ = let ctxt = definitions uctxt ty' = normalise uctxt [] ty ctxt' = addCons 0 cons (addDef n - (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in + (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in uctxt { definitions = ctxt' } where addCons tag [] ctxt = ctxt addCons tag ((n, ty) : cons) ctxt = let ty' = normalise uctxt [] ty in addCons (tag+1) cons (addDef n - (TyDecl (DCon tag (arity ty')) ty, Public) ctxt) + (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt) addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] -> Type -> Context -> Context @@ -529,10 +614,10 @@ ps' = ps -- simpl ps in ctxt' = case (simpleCase tcase covering ps', simpleCase tcase covering psrt) of - (CaseDef args sc, CaseDef args' sc') -> + (CaseDef args sc _, CaseDef args' sc' _) -> let inl = alwaysInline in addDef n (CaseOp inl ty ps args sc args' sc', - Public) ctxt in + Public, Unchecked) ctxt in uctxt { definitions = ctxt' } where simpl [] = [] simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs @@ -540,13 +625,15 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context addOperator n ty a op uctxt = let ctxt = definitions uctxt - ctxt' = addDef n (Operator ty a op, Public) ctxt in + ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in uctxt { definitions = ctxt' } +tfst (a, _, _) = a + lookupTy :: Maybe [String] -> Name -> Context -> [Type] lookupTy root n ctxt = do def <- lookupCtxt root n (definitions ctxt) - case fst def of + case tfst def of (Function ty _) -> return ty (TyDecl _ ty) -> return ty (Operator ty _ _) -> return ty @@ -555,7 +642,7 @@ isConName :: Maybe [String] -> Name -> Context -> Bool isConName root n ctxt = or $ do def <- lookupCtxt root n (definitions ctxt) - case fst def of + case tfst def of (TyDecl (DCon _ _) _) -> return True (TyDecl (TCon _ _) _) -> return True _ -> return False @@ -564,26 +651,30 @@ lookupP root n ctxt = do def <- lookupCtxt root n (definitions ctxt) p <- case def of - (Function ty tm, a) -> return (P Ref n ty, a) - (TyDecl nt ty, a) -> return (P nt n ty, a) - (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a) - (Operator ty _ _, a) -> return (P Ref n ty, a) + (Function ty tm, a, _) -> return (P Ref n ty, a) + (TyDecl nt ty, a, _) -> return (P nt n ty, a) + (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a) + (Operator ty _ _, a, _) -> return (P Ref n ty, a) case snd p of Hidden -> [] _ -> return (fst p) lookupDef :: Maybe [String] -> Name -> Context -> [Def] -lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt) +lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt) lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)] lookupDefAcc root n mkpublic ctxt = map mkp $ lookupCtxt root n (definitions ctxt) - where mkp (d, a) = if mkpublic then (d, Public) else (d, a) + where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a) +lookupTotal :: Name -> Context -> [Totality] +lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt) + where mkt (d, a, t) = t + lookupVal :: Maybe [String] -> Name -> Context -> [Value] lookupVal root n ctxt = do def <- lookupCtxt root n (definitions ctxt) - case fst def of + case tfst def of (Function _ htm) -> return (veval ctxt [] htm) (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty)) diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs --- a/src/Core/ProofState.hs +++ b/src/Core/ProofState.hs @@ -308,7 +308,7 @@ -- unified = (uh, uns ++ [(x, val)]), instances = instances ps \\ [x] }) return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc) - | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val + | otherwise = lift $ tfail $ IncompleteTerm val solve _ _ h = fail $ "Not a guess " ++ show h introTy :: Raw -> Maybe Name -> RunTactic diff --git a/src/Core/TT.hs b/src/Core/TT.hs --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -39,7 +39,9 @@ data Err = Msg String | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify + | NoSuchVariable Name | NotInjective Term Term Term + | CantResolve Term | IncompleteTerm Term | UniverseError | ProgramLineComment @@ -48,6 +50,8 @@ score :: Err -> Int score (CantUnify _ _ m s) = s + score m +score (CantResolve _) = 20 +score (NoSuchVariable _) = 1000 score _ = 0 instance Show Err where @@ -322,23 +326,6 @@ (==) Erased _ = True (==) _ Erased = True (==) _ _ = False - -convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool -convEq (P xt x _) (P yt y _) = return (xt == yt && x == y) -convEq (V x) (V y) = return (x == y) -convEq (Bind _ xb xs) (Bind _ yb ys) - = liftM2 (&&) (convEqB xb yb) (convEq xs ys) - where convEqB (Let v t) (Let v' t') = liftM2 (&&) (convEq v v') (convEq t t') - convEqB (Guess v t) (Guess v' t') = liftM2 (&&) (convEq v v') (convEq t t') - convEqB b b' = convEq (binderTy b) (binderTy b') -convEq (App fx ax) (App fy ay) = liftM2 (&&) (convEq fx fy) (convEq ax ay) -convEq (Constant x) (Constant y) = return (x == y) -convEq (Set x) (Set y) = do (v, cs) <- get - put (v, ULE x y : cs) - return True -convEq Erased _ = return True -convEq _ Erased = return True -convEq _ _ = return False -- A few handy operations on well typed terms: diff --git a/src/Core/Typecheck.hs b/src/Core/Typecheck.hs --- a/src/Core/Typecheck.hs +++ b/src/Core/Typecheck.hs @@ -16,8 +16,8 @@ convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC () convertsC ctxt env x y - = do c <- convEq (finalise (normalise ctxt env x)) - (finalise (normalise ctxt env y)) + = do c <- convEq ctxt (finalise (normalise ctxt env x)) + (finalise (normalise ctxt env y)) if c then return () else fail ("Can't convert between " ++ showEnv env (finalise (normalise ctxt env x)) ++ " and " ++ @@ -53,7 +53,7 @@ chk env (Var n) | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty) | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty) - | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env) + | otherwise = do lift $ tfail $ NoSuchVariable n chk env (RApp f a) = do (fv, fty) <- chk env f (av, aty) <- chk env a diff --git a/src/Core/Unify.hs b/src/Core/Unify.hs --- a/src/Core/Unify.hs +++ b/src/Core/Unify.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternGuards #-} + module Core.Unify(unify, Fails) where import Core.TT @@ -95,7 +97,7 @@ h2 <- un' False ((x,y):bnames) sx sy combine bnames h1 h2 un' fn bnames x y - | x == y = do sc 1; return [] + | OK True <- convEq' ctxt x y = do sc 1; return [] | otherwise = do UI s i f <- get let err = CantUnify topx topy (CantUnify x y (Msg "") s) s put (UI s i ((x, y, env, err) : f)) diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -40,9 +40,13 @@ idris_implicits :: Ctxt [PArg], idris_statics :: Ctxt [Bool], idris_classes :: Ctxt ClassInfo, + idris_dsls :: Ctxt DSL, idris_optimisation :: Ctxt OptInfo, idris_datatypes :: Ctxt TypeInfo, idris_patdefs :: Ctxt [(Term, Term)], -- not exported + idris_flags :: Ctxt [FnOpt], + idris_callgraph :: Ctxt [Name], + idris_totcheck :: [(FC, Name)], idris_log :: String, idris_options :: IOption, idris_name :: Int, @@ -70,6 +74,8 @@ | IBCImp Name | IBCStatic Name | IBCClass Name + | IBCInstance Name Name + | IBCDSL Name | IBCData Name | IBCOpt Name | IBCSyntax Syntax @@ -79,12 +85,16 @@ | IBCLib String | IBCHeader String | IBCAccess Name Accessibility + | IBCTotal Name Totality + | IBCFlags Name [FnOpt] + | IBCCG Name | IBCDef Name -- i.e. main context deriving Show idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext - emptyContext emptyContext emptyContext - "" defaultOpts 6 [] [] [] [] [] [] [] [] + emptyContext emptyContext emptyContext emptyContext + emptyContext emptyContext + [] "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing Nothing [] [] [] Hidden [] Nothing -- The monad for the main REPL - reading and processing files and updating @@ -109,12 +119,53 @@ addHdr :: String -> Idris () addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i }) +totcheck :: (FC, Name) -> Idris () +totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i }) + +setFlags :: Name -> [FnOpt] -> Idris () +setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) }) + setAccessibility :: Name -> Accessibility -> Idris () setAccessibility n a = do i <- get let ctxt = setAccess n a (tt_ctxt i) put (i { tt_ctxt = ctxt }) +setTotality :: Name -> Totality -> Idris () +setTotality n a + = do i <- get + let ctxt = setTotal n a (tt_ctxt i) + put (i { tt_ctxt = ctxt }) + +getTotality :: Name -> Idris Totality +getTotality n + = do i <- get + case lookupTotal n (tt_ctxt i) of + [t] -> return t + _ -> return (Total []) + +addToCG :: Name -> [Name] -> Idris () +addToCG n ns = do i <- get + put (i { idris_callgraph = addDef n ns (idris_callgraph i) }) + +addInstance :: Name -> Name -> Idris () +addInstance 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) + put (ist { idris_classes = cs }) + _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist) + put (ist { idris_classes = cs }) + +addClass :: Name -> ClassInfo -> Idris () +addClass n i + = do ist <- get + let i' = case lookupCtxt Nothing n (idris_classes ist) of + [c] -> c { class_instances = class_instances i } + _ -> i + put (ist { idris_classes = addDef n i' (idris_classes ist) }) + addIBC :: IBCWrite -> Idris () addIBC ibc@(IBCDef n) = do i <- get @@ -290,7 +341,8 @@ -- Commands in the REPL -data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit +data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name + | Reload | Edit | Compile String | Execute | ExecVal PTerm | Metavars | Prove Name | AddProof | Universes | TTShell @@ -337,6 +389,9 @@ pstatic :: Static } | Constraint { plazy :: Bool, pstatic :: Static } + | TacImp { plazy :: Bool, + pstatic :: Static, + pscript :: PTerm } deriving (Show, Eq) {-! @@ -346,9 +401,13 @@ impl = Imp False Dynamic expl = Exp False Dynamic constraint = Constraint False Static +tacimpl = TacImp False Dynamic -data FnOpt = Inlinable | Partial | Abstract | Private | TCGen +data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen deriving (Show, Eq) +{-! +deriving instance Binary FnOpt +!-} type FnOpts = [FnOpt] @@ -356,11 +415,12 @@ inlinable = elem Inlinable data PDecl' t = PFix FC Fixity [String] -- fixity declaration - | PTy SyntaxInfo FC Name t -- type declaration + | PTy SyntaxInfo FC FnOpts Name t -- type declaration | PClauses FC FnOpts Name [PClause' t] -- pattern clause | PData SyntaxInfo FC (PData' t) -- data declaration | PParams FC [(Name, t)] [PDecl' t] -- params block | PNamespace String [PDecl' t] -- new namespace + | PRecord SyntaxInfo FC Name t Name t -- record declaration | PClass SyntaxInfo FC [t] -- constraints Name @@ -371,14 +431,15 @@ [t] -- parameters t -- full instance type [PDecl' t] + | PDSL Name (DSL' t) | PSyntax FC Syntax | PDirective (Idris ()) deriving Functor -data PClause' t = PClause Name t [t] t [PDecl' t] - | PWith Name t [t] t [PDecl' t] - | PClauseR [t] t [PDecl' t] - | PWithR [t] t [PDecl' t] +data PClause' t = PClause FC Name t [t] t [PDecl' t] + | PWith FC Name t [t] t [PDecl' t] + | PClauseR FC [t] t [PDecl' t] + | PWithR FC [t] t [PDecl' t] deriving Functor data PData' t = PDatadecl { d_name :: Name, @@ -397,7 +458,7 @@ declared :: PDecl -> [Name] declared (PFix _ _ _) = [] -declared (PTy _ _ n t) = [n] +declared (PTy _ _ _ n t) = [n] declared (PClauses _ _ n _) = [] -- not a declaration declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts where fstt (a, _, _) = a @@ -433,6 +494,7 @@ | PLam Name PTerm PTerm | PPi Plicity Name PTerm PTerm | PLet Name PTerm PTerm PTerm + | PTyped PTerm PTerm -- term with explicit type | PApp FC PTerm [PArg] | PCase FC PTerm [(PTerm, PTerm)] | PTrue FC @@ -453,7 +515,7 @@ | PMetavar Name | PProof [PTactic] | PTactics [PTactic] -- as PProof, but no auto solving - | PElabError String -- error to report on elaboration + | PElabError Err -- error to report on elaboration | PImpossible -- special case for declaring when an LHS can't typecheck deriving Eq {-! @@ -468,6 +530,7 @@ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as) mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os) mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r) + mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r) mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r) mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r) mpt (PAlternative as) = PAlternative (map (mapPT f) as) @@ -486,7 +549,7 @@ | ProofState | ProofTerm | Undo | Try (PTactic' t) (PTactic' t) | TSeq (PTactic' t) (PTactic' t) - | Qed + | Qed | Abandon deriving (Show, Eq, Functor) {-! deriving instance Binary PTactic' @@ -516,6 +579,10 @@ lazyarg :: Bool, getTm :: t } | PConstraint { priority :: Int, lazyarg :: Bool, getTm :: t } + | PTacImplicit { priority :: Int, + lazyarg :: Bool, pname :: Name, + getScript :: t, + getTm :: t } deriving (Show, Eq, Functor) {-! deriving instance Binary PArg' @@ -524,15 +591,17 @@ pimp = PImp 0 True pexp = PExp 0 False pconst = PConstraint 0 False +ptacimp = PTacImplicit 0 True type PArg = PArg' PTerm -- Type class data data ClassInfo = CI { instanceName :: Name, - class_methods :: [(Name, PTerm)], + class_methods :: [(Name, (FnOpts, PTerm))], class_defaults :: [(Name, Name)], -- method name -> default impl - class_params :: [Name] } + class_params :: [Name], + class_instances :: [Name] } deriving Show {-! deriving instance Binary ClassInfo @@ -555,17 +624,23 @@ -- Syntactic sugar info -data DSL = DSL { dsl_bind :: PTerm, - dsl_return :: PTerm, - dsl_apply :: PTerm, - dsl_pure :: PTerm, - index_first :: Maybe PTerm, - index_next :: Maybe PTerm, - dsl_lambda :: Maybe PTerm, - dsl_let :: Maybe PTerm - } - deriving Show +data DSL' t = DSL { dsl_bind :: t, + dsl_return :: t, + dsl_apply :: t, + dsl_pure :: t, + dsl_var :: Maybe t, + index_first :: Maybe t, + index_next :: Maybe t, + dsl_lambda :: Maybe t, + dsl_let :: Maybe t + } + deriving (Show, Functor) +{-! +deriving instance Binary DSL' +!-} +type DSL = DSL' PTerm + data SynContext = PatternSyntax | TermSyntax | AnySyntax deriving Show {-! @@ -581,6 +656,7 @@ data SSymbol = Keyword Name | Symbol String | Expr Name + | SimpleExpr Name deriving Show {-! deriving instance Binary SSymbol @@ -594,6 +670,7 @@ Nothing Nothing Nothing + Nothing where f = FC "(builtin)" 0 data SyntaxInfo = Syn { using :: [(Name, PTerm)], @@ -607,16 +684,20 @@ defaultSyntax = Syn [] [] [] [] id False initDSL +expandNS :: SyntaxInfo -> Name -> Name +expandNS syn n@(NS _ _) = n +expandNS syn n = case syn_namespace syn of + [] -> n + xs -> NS n xs + + --- Pretty printing declarations and terms instance Show PTerm where show tm = showImp False tm instance Show PDecl where - show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops - show (PTy _ _ n ty) = show n ++ " : " ++ show ty - show (PClauses _ _ n c) = showSep "\n" (map show c) - show (PData _ _ d) = show d + show d = showDeclImp False d instance Show PClause where show c = showCImp True c @@ -624,14 +705,19 @@ instance Show PData where show d = showDImp False d +showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops +showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty +showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c) +showDeclImp _ (PData _ _ d) = show d + showCImp :: Bool -> PClause -> String -showCImp impl (PClause n l ws r w) +showCImp impl (PClause _ n l ws r w) = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r ++ " where " ++ show w where showWs [] = "" showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs -showCImp impl (PWith n l ws r w) +showCImp impl (PWith _ n l ws r w) = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r ++ " { " ++ show w ++ " } " where @@ -666,8 +752,8 @@ showImp :: Bool -> PTerm -> String showImp impl tm = se 10 tm where se p (PQuote r) = "![" ++ show r ++ "]" - se p (PRef _ n) = if impl then show n - else showbasic n + 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 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n @@ -675,7 +761,8 @@ se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++ " in " ++ se 10 sc se p (PPi (Exp l s) n ty sc) - | n `elem` allNamesIn sc = bracket p 2 $ + | n `elem` allNamesIn sc || impl + = bracket p 2 $ if l then "|(" else "(" ++ show n ++ " : " ++ se 10 ty ++ ") " ++ st ++ @@ -712,6 +799,7 @@ se p (PTrue _) = "()" se p (PFalse _) = "_|_" se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r + se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")" se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")" se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")" se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)" @@ -724,16 +812,18 @@ se p PImpossible = "impossible" se p Placeholder = "_" se p (PDoBlock _) = "do block show not implemented" - se p (PElabError s) = s + se p (PElabError s) = show s -- se p x = "Not implemented" sArg (PImp _ _ n tm) = siArg (n, tm) sArg (PExp _ _ tm) = seArg tm sArg (PConstraint _ _ tm) = scArg tm + sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm) seArg arg = " " ++ se 0 arg siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}" scArg val = " {{" ++ se 10 val ++ "}}" + stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}" bracket outer inner str | inner > outer = "(" ++ str ++ ")" | otherwise = str @@ -749,6 +839,7 @@ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc ni env (PHidden tm) = ni env tm ni env (PEq _ l r) = ni env l ++ ni env r + ni env (PTyped l r) = ni env l ++ ni env r ni env (PPair _ l r) = ni env l ++ ni env r ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r @@ -768,6 +859,7 @@ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc ni env (PEq _ l r) = ni env l ++ ni env r + ni env (PTyped l r) = ni env l ++ ni env r ni env (PPair _ l r) = ni env l ++ ni env r ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r @@ -879,6 +971,7 @@ PLet n' (en ty) (en v) (en (shadow n n' s)) | otherwise = PLet n (en ty) (en v) (en s) en (PEq f l r) = PEq f (en l) (en r) + en (PTyped l r) = PTyped (en l) (en r) en (PPair f l r) = PPair f (en l) (en r) en (PDPair f l t r) = PDPair f (en l) (en t) (en r) en (PAlternative as) = PAlternative (map en as) @@ -901,30 +994,30 @@ expandParamsD :: IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl -expandParamsD ist dec ps ns (PTy syn fc n ty) +expandParamsD ist dec ps ns (PTy syn fc o n ty) = if n `elem` ns - then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty)) - else PTy syn fc n (expandParams dec ps ns ty) + then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty)) + else PTy syn fc o n (expandParams dec ps ns ty) expandParamsD ist dec ps ns (PClauses fc opts n cs) = let n' = if n `elem` ns then dec n else n in PClauses fc opts n' (map expandParamsC cs) where - expandParamsC (PClause n lhs ws rhs ds) + expandParamsC (PClause fc n lhs ws rhs ds) = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..]) ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..]) n' = if n `elem` ns then dec n else n in - PClause n' (expandParams dec ps'' ns lhs) - (map (expandParams dec ps'' ns) ws) - (expandParams dec ps'' ns rhs) - (map (expandParamsD ist dec ps'' ns) ds) - expandParamsC (PWith n lhs ws wval ds) + PClause fc n' (expandParams dec ps'' ns lhs) + (map (expandParams dec ps'' ns) ws) + (expandParams dec ps'' ns rhs) + (map (expandParamsD ist dec ps'' ns) ds) + expandParamsC (PWith fc n lhs ws wval ds) = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..]) ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..]) n' = if n `elem` ns then dec n else n in - PWith n' (expandParams dec ps'' ns lhs) - (map (expandParams dec ps'' ns) ws) - (expandParams dec ps'' ns wval) - (map (expandParamsD ist dec ps'' ns) ds) + PWith fc n' (expandParams dec ps'' ns lhs) + (map (expandParams dec ps'' ns) ws) + (expandParams dec ps'' ns wval) + (map (expandParamsD ist dec ps'' ns) ds) updateps yn nm [] = [] updateps yn nm (((a, t), i):as) | (a `elem` nm) == yn = (a, t) : updateps yn nm as @@ -954,6 +1047,7 @@ pri (PEq _ l r) = max 1 (max (pri l) (pri r)) pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as))) pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as))) + pri (PTyped l r) = pri l pri (PPair _ l r) = max 1 (max (pri l) (pri r)) pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r))) pri (PAlternative as) = maximum (map pri as) @@ -1022,10 +1116,20 @@ put (PConstraint 10 l ty : decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) imps True (n:env) sc + imps top env (PPi (TacImp l _ scr) n ty sc) + = do let isn = nub (namesIn uvars ist ty ++ case sc of + (PRef _ x) -> namesIn uvars ist sc `dropAll` [n] + _ -> []) + (decls, ns) <- get -- ignore decls in HO types + put (PTacImplicit 10 l n scr ty : decls, + nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) + imps True (n:env) sc imps top env (PEq _ l r) = do (decls, ns) <- get let isn = namesIn uvars ist l ++ namesIn uvars ist r put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) + imps top env (PTyped l r) + = imps top env l imps top env (PPair _ l r) = do (decls, ns) <- get let isn = namesIn uvars ist l ++ namesIn uvars ist r @@ -1056,15 +1160,31 @@ Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc) -- Add implicit arguments in function calls +addImplPat :: IState -> PTerm -> PTerm +addImplPat = addImpl' True [] +addImplBound :: IState -> [Name] -> PTerm -> PTerm +addImplBound ist ns = addImpl' False ns ist + addImpl :: IState -> PTerm -> PTerm -addImpl ist ptm = ai [] ptm +addImpl = addImpl' False [] + +-- TODO: in patterns, don't add implicits to function names guarded by constructors +-- and *not* inside a PHidden + +addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm +addImpl' inpat env ist ptm = ai env ptm where ai env (PRef fc f) - | not (f `elem` env) = aiFn ist fc f [] + | not (f `elem` env) = handleErr $ aiFn inpat ist fc f [] + ai env (PHidden (PRef fc f)) + | not (f `elem` env) = handleErr $ aiFn False ist fc f [] ai env (PEq fc l r) = let l' = ai env l r' = ai env r in PEq fc l' r' + ai env (PTyped l r) = let l' = ai env l + r' = ai env r in + PTyped l' r' ai env (PPair fc l r) = let l' = ai env l r' = ai env r in PPair fc l' r' @@ -1077,7 +1197,7 @@ ai env (PApp fc (PRef _ f) as) | not (f `elem` env) = let as' = map (fmap (ai env)) as in - aiFn ist fc f as' + handleErr $ aiFn False ist fc f as' ai env (PApp fc f as) = let f' = ai env f as' = map (fmap (ai env)) as in mkPApp fc 1 f' as' @@ -1100,19 +1220,34 @@ ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts) ai env tm = tm -aiFn :: IState -> FC -> Name -> [PArg] -> PTerm -aiFn ist fc f as - | f `elem` primNames = PApp fc (PRef fc f) as -aiFn ist fc f as + handleErr (Left err) = PElabError err + handleErr (Right x) = x + +-- if in a pattern, and there are no arguments, and there's no possible +-- names with zero explicit arguments, don't add implicits. + +aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm +aiFn True ist fc f [] + = case lookupCtxt Nothing f (idris_implicits ist) of + [] -> Right $ PRef fc f + alts -> if (any (all imp) alts) + then aiFn False ist fc f [] -- use it as a constructor + else Right $ PRef fc f + where imp (PExp _ _ _) = False + imp _ = True +aiFn inpat ist fc f as + | f `elem` primNames = Right $ PApp fc (PRef fc f) as +aiFn inpat ist fc f as -- This is where namespaces get resolved by adding PAlternative = case lookupCtxtName Nothing f (idris_implicits ist) of - [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as) + [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as) [] -> if f `elem` idris_metavars ist - then PApp fc (PRef fc f) as - else mkPApp fc (length as) (PRef fc f) as - alts -> PAlternative $ - map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f') - (insertImpl ns as)) alts + then Right $ PApp fc (PRef fc f) as + else Right $ mkPApp fc (length as) (PRef fc f) as + alts -> Right $ + PAlternative $ + map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f') + (insertImpl ns as)) alts where insertImpl :: [PArg] -> [PArg] -> [PArg] insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) = @@ -1125,6 +1260,11 @@ case find n given [] of Just (tm, given') -> PImp p l n tm : insertImpl ps given' Nothing -> PImp p l n Placeholder : insertImpl ps given + insertImpl (PTacImplicit p l n sc ty : ps) given = + case find n given [] of + Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given' + Nothing -> PTacImplicit p l n sc sc + : insertImpl ps given insertImpl expected [] = [] insertImpl _ given = given @@ -1177,7 +1317,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops -dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t +dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs) dumpDecl (PData _ _ d) = showDImp True d dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n" @@ -1205,11 +1345,11 @@ -- syntactic match of a against b, returning pair of variables in a -- and what they match. Returns the pair that failed if not a match. -matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] +matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] matchClause = matchClause' False -matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] -matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where +matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] +matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y)) fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs)) @@ -1230,10 +1370,17 @@ match (PRef f n) (PApp _ x []) = match (PRef f n) x match (PApp _ x []) (PRef f n) = match x (PRef f n) match (PRef _ n) (PRef _ n') | n == n' = return [] - match (PRef _ n) tm | not names = return [(n, tm)] + match (PRef _ n) tm + | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder) + = return [(n, tm)] match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l' mr <- match' r r' return (ml ++ mr) + match (PTyped l r) (PTyped l' r') = do ml <- match l l' + mr <- match r r' + return (ml ++ mr) + match (PTyped l r) x = match l x + match x (PTyped l r) = match x l match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l' mr <- match' r r' return (ml ++ mr) @@ -1271,7 +1418,7 @@ return (mt ++ mty ++ ms) match (PHidden x) (PHidden y) = match' x y match Placeholder _ = return [] - match _ Placeholder = return [] +-- match _ Placeholder = return [] match (PResolveTC _) _ = return [] match a b | a == b = return [] | otherwise = LeftErr (a, b) @@ -1297,6 +1444,7 @@ sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as) sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as) sm (PEq f x y) = PEq f (sm x) (sm y) + sm (PTyped x y) = PTyped (sm x) (sm y) sm (PPair f x y) = PPair f (sm x) (sm y) sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y) sm (PAlternative as) = PAlternative (map sm as) @@ -1311,6 +1459,7 @@ sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as) sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as) sm (PEq f x y) = PEq f (sm x) (sm y) + sm (PTyped x y) = PTyped (sm x) (sm y) sm (PPair f x y) = PPair f (sm x) (sm y) sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y) sm (PAlternative as) = PAlternative (map sm as) diff --git a/src/Idris/Compiler.hs b/src/Idris/Compiler.hs --- a/src/Idris/Compiler.hs +++ b/src/Idris/Compiler.hs @@ -24,7 +24,9 @@ compile :: FilePath -> Term -> Idris () compile f tm = do checkMVs - ds <- mkDecls tm + let tmnames = namesUsed (STerm tm) + used <- mapM (allNames []) tmnames + ds <- mkDecls tm (concat used) objs <- getObjectFiles libs <- getLibs hdrs <- getHdrs @@ -34,7 +36,7 @@ Nothing -> do m <- epicMain tm let mainval = EpicFn (name "main") m - liftIO $ compileObjWith [Debug] + liftIO $ compileObjWith [] (mkProgram (incs ++ mainval : ds)) (f ++ ".o") liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f where checkMVs = do i <- get @@ -42,10 +44,20 @@ [] -> return () ms -> fail $ "There are undefined metavariables: " ++ show ms -mkDecls :: Term -> Idris [EpicDecl] -mkDecls t = do i <- getIState - decls <- mapM build (ctxtAlist (tt_ctxt i)) - return $ basic_defs ++ decls +allNames :: [Name] -> Name -> Idris [Name] +allNames ns n | n `elem` ns = return [] +allNames ns n = do i <- get + case lookupCtxt Nothing n (idris_callgraph i) of + [ns'] -> do more <- mapM (allNames (n:ns)) ns' + return (nub (n : concat more)) + _ -> return [n] + +mkDecls :: Term -> [Name] -> Idris [EpicDecl] +mkDecls t used + = do i <- getIState + let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i) + decls <- mapM build ds + return $ basic_defs ++ decls -- EpicFn (name "main") epicMain : decls diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs --- a/src/Idris/Coverage.hs +++ b/src/Idris/Coverage.hs @@ -4,10 +4,14 @@ import Core.TT import Core.Evaluate +import Core.CaseTree + import Idris.AbsSyntax import Idris.Delaborate +import Idris.Error import Data.List +import Data.Either import Debug.Trace -- Given a list of LHSs, generate a extra clauses which cover the remaining @@ -17,7 +21,7 @@ -- This will only work after the given clauses have been typechecked and the -- names are fully explicit! -genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PClause] +genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm] genClauses fc n xs given = do i <- getIState let lhss = map (getLHS i) xs @@ -30,30 +34,35 @@ let parg = case lookupCtxt Nothing n (idris_implicits i) of (p : _) -> p _ -> repeat (pexp Placeholder) - let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args + let tryclauses = mkClauses parg all_args + let new = mnub i $ filter (noMatch i) tryclauses logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new) - return (map (\t -> PClause n t [] PImpossible []) new) +-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses) + return new +-- return (map (\t -> PClause n t [] PImpossible []) new) where getLHS i term | (f, args) <- unApply term = map (\t -> delab' i t True) args | otherwise = [] - lhsApp (PClause _ l _ _ _) = l - lhsApp (PWith _ l _ _ _) = l + lhsApp (PClause _ _ l _ _ _) = l + lhsApp (PWith _ _ l _ _ _) = l mnub i [] = [] mnub i (x : xs) = - if (any (\t -> case matchClause x t of + if (any (\t -> case matchClause i x t of Right _ -> True Left _ -> False) xs) then mnub i xs else x : mnub i xs - noMatch i tm = all (\x -> case matchClause (delab' i x True) tm of + noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of Right _ -> False Left miss -> True) xs mkClauses :: [PArg] -> [[PTerm]] -> [PTerm] mkClauses parg args + | all (== [Placeholder]) args = [] + mkClauses parg args = do args' <- mkArg args let tm = PApp fc (PRef fc n) (zipWith upd args' parg) return tm @@ -64,13 +73,22 @@ as' <- mkArg as return (a':as') +-- FIXME: Just look for which one is the deepest, then generate all possibilities +-- up to that depth. + genAll :: IState -> [PTerm] -> [PTerm] -genAll i args = concatMap otherPats (nub args) +genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of + [] -> [Placeholder] + xs -> xs where + conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i) + conForm (PRef fc n) = isConName Nothing n (tt_ctxt i) + conForm _ = False + otherPats :: PTerm -> [PTerm] otherPats o@(PRef fc n) = ops fc n [] o otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o - otherPats arg = return arg + otherPats arg = return Placeholder ops fc n xs o | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i) @@ -80,7 +98,7 @@ case lookupCtxt Nothing tyn (idris_datatypes i) of (TI ns : _) -> p : map (mkPat fc) (ns \\ [n]) _ -> [p] - ops fc n arg o = return o + ops fc n arg o = return Placeholder getTy n ctxt = case lookupTy Nothing n ctxt of (t : _) -> case unApply (getRetTy t) of @@ -94,4 +112,206 @@ _ -> error "Can't happen - genAll" 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 + +checkPositive :: Name -> (Name, Type) -> Idris () +checkPositive n (cn, ty) + = do let p = cp ty + i <- getIState + let tot = if p then Total (args ty) else Partial NotPositive + let ctxt' = setTotal cn tot (tt_ctxt i) + putIState (i { tt_ctxt = ctxt' }) + addIBC (IBCTotal cn tot) + where + args t = [0..length (getArgTys t)-1] + + cp (Bind n (Pi aty) sc) = posArg aty && cp sc + cp t = True + + posArg (Bind _ (Pi nty) sc) + | (P _ n' _, args) <- unApply nty + = n /= n' && posArg sc + posArg t = True + +-- Totality checking - check for structural recursion (no mutual definitions yet) + +data LexOrder = LexXX | LexEQ | LexLT + deriving (Show, Eq, Ord) + +calcTotality :: [Name] -> FC -> Name -> [(Term, Term)] -> Idris Totality +calcTotality path fc n pats + = do orders <- mapM ctot pats + let order = sortBy cmpOrd $ concat orders + let (errs, valid) = partitionEithers order + let lex = stripNoLT (stripXX valid) + case errs of + [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex) + logLvl 10 $ show pats + checkDecreasing lex + (e : _) -> return e -- FIXME: should probably combine them + where + cmpOrd (Left _) (Left _) = EQ + cmpOrd (Left _) (Right _) = LT + cmpOrd (Right _) (Left _) = GT + cmpOrd (Right x) (Right y) = compare x y + + checkDecreasing [] = return (Total []) + checkDecreasing (c : cs) | dec c = checkDecreasing cs + | otherwise = return (Partial Itself) + + dec [] = False + dec (LexLT : _) = True + dec (LexEQ : xs) = dec xs + dec (LexXX : xs) = False + + stripXX [] = [] + stripXX v@(c : cs) + = case span (==LexXX) c of + (ns, rest) -> map (drop (length ns)) v + + -- argument positions which are never LT are no use to us + stripNoLT [] = [] -- no recursive calls + stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of + [] -> [[]] -- recursive calls are all useless... + xs -> xs + + ctot (lhs, rhs) + | (_, args) <- unApply lhs + = do -- check lhs doesn't use any dodgy names + lhsOK <- mapM (chkOrd [] []) args + chkOrd (filter isLeft (concat lhsOK)) args rhs + + isLeft (Left _) = True + isLeft _ = False + + chkOrd ords args (Bind n (Let t v) sc) + = do ov <- chkOrd ords args v + chkOrd ov args sc + chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc + chkOrd ords args ap@(App f a) + | (P _ fn _, args') <- unApply ap + = if fn == n && length args == length args' + then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f + chkOrd orf args a + else do orf <- chkOrd ords args f + chkOrd orf args a + | otherwise = do orf <- chkOrd ords args f + chkOrd orf args a + chkOrd ords args (P _ fn _) + | n /= fn + = do tf <- checkTotality (n : path) fc fn + case tf of + Total _ -> return ords + p@(Partial (Mutual x)) -> return ((Left p) : ords) + _ -> return (Left (Partial (Other [fn])) : ords) + | null args = return (Left (Partial Itself) : ords) + chkOrd ords args _ = return ords + + lexOrd x y | x == y = LexEQ + lexOrd f@(App _ _) x + | (f', args) <- unApply f + = let ords = map (\x' -> lexOrd x' x) args in + if any (\o -> o == LexEQ || o == LexLT) ords + then LexLT + else LexXX + lexOrd _ _ = LexXX + +checkTotality :: [Name] -> FC -> Name -> Idris Totality +checkTotality path fc n + | n `elem` path = return (Partial (Mutual (n : path))) + | otherwise = do + t <- getTotality n + ctxt <- getContext + 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 + [CaseOp _ _ pats _ _ _ _] -> + do t' <- if AssertTotal `elem` opts + then return $ Total [] + else calcTotality path fc n pats + setTotality n t' + addIBC (IBCTotal n t') + -- if it's not total, it can't reduce, to keep + -- typechecking decidable + case t' of +-- FIXME: Put this back when we can handle mutually recursive things +-- p@(Partial _) -> +-- do setAccessibility n Frozen +-- addIBC (IBCAccess n Frozen) +-- iputStrLn $ "HIDDEN: " ++ show n ++ show p + _ -> return () + return t' + _ -> return $ Total [] + x -> return x + if TotalFn `elem` opts + then case t' of + Total _ -> return t' + e -> totalityError t' + else return t' + where + totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t))) + +checkDeclTotality :: (FC, Name) -> Idris Totality +checkDeclTotality (fc, n) + = do logLvl 2 $ "Checking " ++ show n ++ " for totality" + checkTotality [] fc n diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs new file mode 100644 --- /dev/null +++ b/src/Idris/DSL.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE PatternGuards #-} + +module Idris.DSL where + +import Idris.AbsSyntax +import Paths_idris + +import Core.CoreParser +import Core.TT +import Core.Evaluate + +desugar :: SyntaxInfo -> IState -> PTerm -> PTerm +desugar syn i t = let t' = expandDo (dsl_info syn) t in + t' -- addImpl i t' + +expandDo :: DSL -> PTerm -> PTerm +expandDo dsl (PLam n ty tm) + | Just lam <- dsl_lambda dsl + = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in + expandDo dsl sc +expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm) +expandDo dsl (PLet n ty v tm) + | Just letb <- dsl_let dsl + = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in + expandDo dsl sc +expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm) +expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm) +expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t) + (map (fmap (expandDo dsl)) args) +expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s) + (map (pmap (expandDo dsl)) opts) +expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r) +expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t) + (expandDo dsl r) +expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as) +expandDo dsl (PHidden t) = PHidden (expandDo dsl t) +expandDo dsl (PReturn fc) = dsl_return dsl +expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds + where + block b [DoExp fc tm] = tm + block b [a] = PElabError (Msg "Last statement in do block must be an expression") + block b (DoBind fc n tm : rest) + = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))] + block b (DoBindP fc p tm : rest) + = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder + (PCase fc (PRef fc (MN 0 "bpat")) + [(p, block b rest)]))] + block b (DoLet fc n ty tm : rest) + = PLet n ty tm (block b rest) + block b (DoLetP fc p tm : rest) + = PCase fc tm [(p, block b rest)] + block b (DoExp fc tm : rest) + = PApp fc b + [pexp tm, + pexp (PLam (MN 0 "bindx") Placeholder (block b rest))] + block b _ = PElabError (Msg "Invalid statement in do block") + +expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e +expandDo dsl t = t + +var :: DSL -> Name -> PTerm -> Int -> PTerm +var dsl n t i = v' i t where + v' i (PRef fc x) | x == n = + case dsl_var dsl of + Nothing -> PElabError (Msg "No 'variable' defined in dsl") + Just v -> PApp fc v [pexp (mkVar fc i)] + v' i (PLam n ty sc) + | Nothing <- dsl_lambda dsl + = PLam n ty (v' i sc) + | otherwise = PLam n (v' i ty) (v' (i + 1) sc) + v' i (PLet n ty val sc) + | Nothing <- dsl_let dsl + = PLet n (v' i ty) (v' i val) (v' i sc) + | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc) + v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc) + v' i (PTyped l r) = PTyped (v' i l) (v' i r) + v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as) + v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as) + v' i (PEq f l r) = PEq f (v' i l) (v' i r) + v' i (PPair f l r) = PPair f (v' i l) (v' i r) + v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r) + 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 t = t + + mkVar fc 0 = case index_first dsl of + Nothing -> PElabError (Msg "No index_first defined") + Just f -> f + mkVar fc n = case index_next dsl of + Nothing -> PElabError (Msg "No index_next defined") + Just f -> PApp fc f [pexp (mkVar fc (n-1))] + +unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm +unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in + mkap (getFn e) + where + getFn (PApp fc f args) = (PApp fc pure [pexp f], args) + getFn f = (f, []) + + mkap (f, []) = f + mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as) + +unIdiom ap pure fc e = PApp fc pure [pexp e] + diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -19,17 +19,20 @@ un = FC "(val)" 0 de env (App f a) = deFn env f [a] - de env (V i) | i < length env = PRef un (env!!i) + de env (V i) | i < length env = PRef un (snd (env!!i)) | otherwise = PRef un (UN ("v" ++ show i ++ "")) de env (P _ n _) | n == unitTy = PTrue un | n == unitCon = PTrue un | n == falseTy = PFalse un + | Just n' <- lookup n env = PRef un n' | otherwise = PRef un (dens n) - de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc) - de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de (n:env) sc) + de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de ((n,n):env) sc) + de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de ((n,n):env) sc) de env (Bind n (Let ty val) sc) - = PLet n (de env ty) (de env val) (de (n:env) sc) - de env (Bind n _ sc) = de (n:env) sc + = PLet n (de env ty) (de env val) (de ((n,n):env) sc) + de env (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) sc + de env (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) sc + de env (Bind n _ sc) = de ((n,n):env) sc de env (Constant i) = PConstant i de env Erased = Placeholder de env (Set i) = PSet @@ -61,16 +64,22 @@ imp (PImp p l n _) arg = PImp p l n arg imp (PExp p l _) arg = PExp p l arg imp (PConstraint p l _) arg = PConstraint p l arg + imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg pshow :: IState -> Err -> String pshow i (Msg s) = s -pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x) - ++ " with " ++ show (delab i y) --- ++ "\n\t(" ++ pshow i e ++ ")" +pshow i (CantUnify x y e s) + = "Can't unify " ++ show (delab i x) + ++ " with " ++ show (delab i y) ++ + case e of + Msg "" -> "" + _ -> "\n\nSpecifically:\n\t " ++ pshow i e pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++ " when unifying " ++ show (delab i x) ++ " and " ++ show (delab i y) -pshow i (IncompleteTerm t) = "Incomplete term " ++ show t +pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c) +pshow i (NoSuchVariable n) = "No such variable " ++ show n +pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t) pshow i UniverseError = "Universe inconsistency" pshow i ProgramLineComment = "Program line next to comment" pshow i (At f e) = show f ++ ":" ++ pshow i e diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -1,8 +1,10 @@ -{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor, + PatternGuards #-} module Idris.ElabDecls where import Idris.AbsSyntax +import Idris.DSL import Idris.Error import Idris.Delaborate import Idris.Imports @@ -26,7 +28,9 @@ recheckC ctxt fc env t = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...) - (tm, ty, cs) <- tclift $ recheck ctxt env (forget t) t + (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of + Error e -> tfail (At fc e) + OK x -> return x addConstraints fc cs return (tm, ty) @@ -34,14 +38,15 @@ mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t return (n, t')) ns -elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris () -elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in +elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris () +elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in n = liftname info n_in in -} do checkUndefined fc n ctxt <- getContext i <- get ty' <- implicit syn n ty' 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)) [] (erun fc (build i info False n ty)) @@ -51,6 +56,8 @@ ds <- checkDef fc ((n, nty):defer) addIBC (IBCDef n) addDeferred ds + setFlags n opts + addIBC (IBCFlags n opts) mapM_ (elabCaseBlock info) is elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris () @@ -69,7 +76,7 @@ (cty, _) <- recheckC ctxt fc [] t' logLvl 2 $ "---> " ++ show cty updateContext (addTyDecl n cty) -- temporary, to check cons - cons <- mapM (elabCon info syn) dcons + cons <- mapM (elabCon info syn n) dcons ttag <- getName i <- get put (i { idris_datatypes = addDef n (TI (map fst cons)) @@ -78,9 +85,109 @@ addIBC (IBCData n) collapseCons n cons updateContext (addDatatype (Data n ttag cty cons)) + mapM_ (checkPositive n) cons -elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type) -elabCon info syn (n, t_in, fc) +elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name -> + PTerm -> Name -> PTerm -> Idris () +elabRecord info syn fc tyn ty cn cty + = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)]) + cty' <- implicit syn cn cty + i <- get + cty <- case lookupTy Nothing cn (tt_ctxt i) of + [t] -> return (delab i t) + _ -> fail "Something went inexplicably wrong" + cimp <- case lookupCtxt Nothing cn (idris_implicits i) of + [imps] -> return imps + let ptys = getProjs [] (renameBs cimp cty) + let ptys_u = getProjs [] cty + let recty = getRecTy cty + logLvl 6 $ show (recty, ptys) + let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n) + [pexp (PRef fc rec)])) ptys + proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..]) + let nonImp = mapMaybe isNonImp (zip cimp ptys_u) + let implBinds = getImplB id cty' + update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..]) + mapM_ (elabDecl info) (concat (proj_decls ++ update_decls)) + where +-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in } + + isNonImp (PExp _ _ _, a) = Just a + isNonImp _ = Nothing + + getImplB k (PPi (Imp l s) n Placeholder sc) + = getImplB k sc + getImplB k (PPi (Imp l s) n ty sc) + = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc + getImplB k (PPi _ n ty sc) + = getImplB k sc + getImplB k _ = k + + renameBs (PImp _ _ _ _ : ps) (PPi p n ty s) + = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s)) + renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s) + renameBs _ t = t + + getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s + getProjs acc r = reverse acc + + getRecTy (PPi _ n ty s) = getRecTy s + getRecTy t = t + + rec = MN 0 "rec" + + mkp (UN n) = MN 0 ("p_" ++ n) + mkp (MN 0 n) = MN 0 ("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 (NS n s) = NS (mkImp n) s + + mkSet (UN n) = UN ("set_" ++ n) + mkSet (MN 0 n) = MN 0 ("set_" ++ n) + mkSet (NS n s) = NS (mkSet n) s + + mkProj recty substs cimp ((pn_in, pty), pos) + = do let pn = expandNS syn pn_in + let pfnTy = PTy defaultSyntax fc [] pn + (PPi expl rec recty + (substMatches substs pty)) + let pls = repeat Placeholder + let before = pos + let after = length substs - (pos + 1) + let args = take before pls ++ PRef fc (mkp pn) : take after pls + let iargs = map implicitise (zip cimp args) + let lhs = PApp fc (PRef fc pn) + [pexp (PApp fc (PRef fc cn) iargs)] + let rhs = PRef fc (mkp pn) + let pclause = PClause fc pn lhs [] rhs [] + return [pfnTy, PClauses fc [] pn [pclause]] + + implicitise (pa, t) = pa { getTm = t } + + mkUpdate recty k num ((pn, pty), pos) + = do let setname = expandNS syn $ mkSet pn + let valname = MN 0 "updateval" + let pt = k (PPi expl pn pty + (PPi expl rec recty recty)) + let pfnTy = PTy defaultSyntax fc [] setname pt + let pls = map (\x -> PRef fc (MN x "field")) [0..num-1] + let lhsArgs = pls + let rhsArgs = take pos pls ++ (PRef fc valname) : + drop (pos + 1) pls + let before = pos + let pclause = PClause fc setname (PApp fc (PRef fc setname) + [pexp (PRef fc valname), + pexp (PApp fc (PRef fc cn) + (map pexp lhsArgs))]) + [] + (PApp fc (PRef fc cn) + (map pexp rhsArgs)) [] + return [pfnTy, PClauses fc [] setname [pclause]] + +elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type) +elabCon info syn tn (n, t_in, fc) = do checkUndefined fc n ctxt <- getContext i <- get @@ -95,14 +202,21 @@ mapM_ (elabCaseBlock info) is ctxt <- getContext (cty, _) <- recheckC ctxt fc [] t' + tyIs cty logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty addIBC (IBCDef n) forceArgs n cty return (n, cty) + where + tyIs (Bind n b sc) = tyIs sc + tyIs t | (P _ n' _, _) <- unApply t + = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn))) + else return () + tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn))) elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris () elabClauses info fc opts n_in cs = let n = liftname info n_in in - do pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs + do pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs solveDeferred n let pats = mapMaybe id pats_in logLvl 3 (showSep "\n" (map (\ (l,r) -> @@ -114,15 +228,51 @@ cov <- coverage pcover <- if cov - then idrisCatch - (do missing <- genClauses fc n (map fst pdef) cs - mapM_ (elabClause info fc True) missing - return True) - (\c -> do -- iputStrLn $ "Warning: " ++ show c - return False) + then do missing <- genClauses fc n (map fst pdef) cs + missing' <- filterM (checkPossible info fc True n) missing +-- let missing' = mapMaybe (\x -> case x of +-- Nothing -> Nothing +-- Just t -> Just $ delab ist t) +-- poss + logLvl 3 $ "Must be unreachable:\n" ++ + showSep "\n" (map (showImp True) missing') ++ + "\nAgainst: " ++ + showSep "\n" (map (\t -> showImp True (delab ist t)) (map fst pdef)) + if null missing' + then return True + else return False +-- -- if there's missing cases, add a catch all case. If it's +-- -- unreachable, we're still covering +-- do let mrhs = P Ref (MN 0 "reach?") undefined +-- let (f,as) = unApply $ depat (head missing') +-- let arity = length as +-- let mlhs = mkApp f (map (\a -> P Bound (MN a "v") undefined) +-- [0..arity-1]) +-- let untree@(CaseDef _ sc _) = simpleCase tcase True +-- (pdef ++ [(mlhs, mrhs)]) +-- logLvl 5 $ "Tree is " ++ show sc +-- return False else return False pdef' <- applyOpts pdef - let tree = simpleCase tcase pcover pdef + let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef + ist <- get +-- let wf = wellFounded ist n sc + let tot = if pcover || AssertTotal `elem` opts + then Unchecked -- finish checking later + else Partial NotCovering -- already know it's not total +-- case lookupCtxt (namespace info) n (idris_flags ist) of +-- [fs] -> if TotalFn `elem` fs +-- then case tot of +-- Total _ -> return () +-- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t))) +-- else return () +-- _ -> return () + case tree of + CaseDef _ _ [] -> return () + CaseDef _ _ xs -> mapM_ (\x -> + iputStrLn $ show fc ++ + ":warning - Unreachable case: " ++ + show (delab ist x)) xs let tree' = simpleCase tcase pcover pdef' tclift $ sameLength pdef logLvl 3 (show tree) @@ -134,6 +284,18 @@ [ty] -> do updateContext (addCasedef n (inlinable opts) tcase pcover pdef pdef' ty) addIBC (IBCDef n) + setTotality n tot + totcheck (fc, n) + when (tot /= Unchecked) $ addIBC (IBCTotal n tot) + i <- get + case lookupDef Nothing n (tt_ctxt i) of + (CaseOp _ _ _ _ sc _ _ : _) -> + do let ns = namesUsed sc + logLvl 2 $ "Called names: " ++ show ns + addToCG n ns + addIBC (IBCCG n) + _ -> return () +-- addIBC (IBCTotal n tot) [] -> return () where debind (x, y) = (depat x, depat y) @@ -160,30 +322,39 @@ logLvl 3 ("Value: " ++ show tm') let vtm = getInferTerm tm' logLvl 2 (show vtm) - recheckC ctxt (FC "prompt" 0) [] vtm + recheckC ctxt (FC "(input)" 0) [] vtm -elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term)) -elabClause info fc tcgen (PClause fname lhs_in [] PImpossible []) +-- checks if the clause is a possible left hand side. Returns the term if +-- possible, otherwise Nothing. + +checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool +checkPossible info fc tcgen fname lhs_in = do ctxt <- getContext i <- get let lhs = addImpl i lhs_in - -- if the LHS type checks, it is possible, so report an error + -- if the LHS type checks, it is possible case elaborate ctxt (MN 0 "patLHS") infP [] (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of OK ((lhs', _, _), _) -> do let lhs_tm = orderPats (getInferTerm lhs') - checkInferred fc (delab' i lhs_tm True) lhs - fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case" - ++ "\n" ++ showImp True lhs - Error _ -> return () - return Nothing -elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock) + b <- inferredDiff fc (delab' i lhs_tm True) lhs + return (not b) -- then return (Just lhs_tm) else return Nothing +-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b) + Error _ -> return False + +elabClause :: ElabInfo -> Bool -> PClause -> Idris (Maybe (Term, Term)) +elabClause info tcgen (PClause fc fname lhs_in [] PImpossible []) + = do b <- checkPossible info fc tcgen fname lhs_in + case b of + True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case" + False -> return Nothing +elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock) = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- get - let lhs = addImpl i lhs_in - logLvl 5 ("LHS: " ++ showImp True lhs) + let lhs = addImplPat i lhs_in + logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs) ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP [] (erun fc (buildTC i info True tcgen fname (infTerm lhs))) @@ -204,15 +375,15 @@ -- Now build the RHS, using the type of the LHS as the goal. i <- get -- new implicits from where block logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in)) - let rhs = addImpl i (expandParams decorate newargs decls rhs_in) - -- TODO: but don't do names in scope + let rhs = addImplBound i (map fst newargs) + (expandParams decorate newargs decls rhs_in) logLvl 2 (showImp True rhs) ctxt <- getContext -- new context with where block added ((rhs', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty [] (do pbinds lhs_tm (_, _, is) <- erun fc (build i info False fname rhs) - psolve lhs_tm + erun fc $ psolve lhs_tm tt <- get_term let (tm, ds) = runState (collectDeferred tt) [] return (tm, ds, is)) @@ -242,7 +413,7 @@ -- _ -> MN i (show n)) . l } -elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock) +elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock) = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings @@ -258,7 +429,7 @@ (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm logLvl 5 ("Checked " ++ show clhs) let bargs = getPBtys lhs_tm - let wval = addImpl i wval_in + let wval = addImplBound i (map fst bargs) wval_in logLvl 5 ("Checking " ++ showImp True wval) -- Elaborate wval in this context ((wval', defer, is), _) <- @@ -267,7 +438,7 @@ (do pbinds lhs_tm -- TODO: may want where here - see winfo abpve (_', d, is) <- erun fc (build i info False fname (infTerm wval)) - psolve lhs_tm + erun fc $ psolve lhs_tm tt <- get_term return (tt, d, is)) def' <- checkDef fc defer @@ -322,26 +493,26 @@ | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n mkAuxC wname lhs ns d = return $ d - mkAux wname toplhs ns (PClause n tm_in (w:ws) rhs wheres) + mkAux wname toplhs ns (PClause fc n tm_in (w:ws) rhs wheres) = do i <- get let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs) - case matchClause toplhs tm of + case matchClause i toplhs tm of Left _ -> fail $ show fc ++ "with clause does not match top level" Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars) lhs <- updateLHS n wname mvars ns (fullApp tm) w - return $ PClause wname lhs ws rhs wheres - mkAux wname toplhs ns (PWith n tm_in (w:ws) wval withs) + return $ PClause fc wname lhs ws rhs wheres + mkAux wname toplhs ns (PWith fc n tm_in (w:ws) wval withs) = do i <- get let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs) withs' <- mapM (mkAuxC wname toplhs ns) withs - case matchClause toplhs tm of + case matchClause i toplhs tm of Left _ -> fail $ show fc ++ "with clause does not match top level" Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w - return $ PWith wname lhs ws wval withs' + return $ PWith fc wname lhs ws wval withs' updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w = return $ substMatches mvars $ @@ -381,8 +552,7 @@ mapM_ (elabDecl info) (concat (map (snd.snd) defs)) i <- get let defaults = map (\ (x, (y, z)) -> (x,y)) defs - put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps)) - (idris_classes i) }) + addClass tn (CI cn imethods defaults (map fst ps) []) addIBC (IBCClass tn) where pibind [] x = x @@ -392,34 +562,34 @@ conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x) conbind [] x = x - tdecl (PTy syn _ n t) = do t' <- implicit syn n t - return ( (n, (toExp (map fst ps) Exp t')), - (n, (toExp (map fst ps) Imp t')), - (n, (syn, t) ) ) + tdecl (PTy syn _ o n t) = do t' <- implicit syn n t + return ( (n, (toExp (map fst ps) Exp t')), + (n, (o, (toExp (map fst ps) Imp t'))), + (n, (syn, o, t) ) ) tdecl _ = fail "Not allowed in a class declaration" -- Create default definitions defdecl mtys c d@(PClauses fc opts n cs) = case lookup n mtys of - Just (syn, ty) -> do let ty' = insertConstraint c ty - let ds = map (decorateid defaultdec) - [PTy syn fc n ty', - PClauses fc (TCGen:opts) n cs] - iLOG (show ds) - return (n, (defaultdec n, ds)) + Just (syn, o, ty) -> do let ty' = insertConstraint c ty + let ds = map (decorateid defaultdec) + [PTy syn fc [] n ty', + PClauses fc (TCGen:o ++ opts) n cs] + iLOG (show ds) + return (n, (defaultdec n, ds)) _ -> fail $ show n ++ " is not a method" defdecl _ _ _ = fail "Can't happen (defdecl)" defaultdec (UN n) = UN ("default#" ++ n) defaultdec (NS n ns) = NS (defaultdec n) ns - tydecl (PTy _ _ _ _) = True + tydecl (PTy _ _ _ _ _) = True tydecl _ = False clause (PClauses _ _ _ _) = True clause _ = False cfun cn c syn all con - = do let cfn = UN ('@':show cn ++ "#" ++ show con) + = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con) let mnames = take (length all) $ map (\x -> MN x "meth") [0..] let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) let lhs = PApp fc (PRef fc cfn) [pconst capp] @@ -427,10 +597,20 @@ let ty = PPi constraint (MN 0 "pc") c con iLOG (showImp True ty) iLOG (showImp True lhs ++ " = " ++ showImp True rhs) - return [PTy syn fc cfn ty, - PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]] + i <- get + let conn = case con of + PRef _ n -> n + PApp _ (PRef _ n) _ -> n + 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)) + return [PTy syn fc [] cfn ty, + PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]] - tfun cn c syn all (m, ty) + tfun cn c syn all (m, (o, ty)) = do let ty' = insertConstraint c ty let mnames = take (length all) $ map (\x -> MN x "meth") [0..] let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) @@ -441,8 +621,8 @@ iLOG (showImp True ty) iLOG (show (m, ty', capp, margs)) iLOG (showImp True lhs ++ " = " ++ showImp True rhs) - return [PTy syn fc m ty', - PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]] + return [PTy syn fc o m ty', + PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]] getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc @@ -480,30 +660,62 @@ = do i <- get (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of [c] -> return c - _ -> fail $ show n ++ " is not a type class" + _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class" let iname = UN ('@':show n ++ "$" ++ show ps) - elabType info syn fc iname t + -- 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 + elabType info syn fc [] iname t let ips = zip (class_params ci) ps let ns = case n of NS n ns' -> ns' _ -> [] - let mtys = map (\ (n, t) -> let t' = substMatches ips t in - (decorate ns n, coninsert cs t', t')) + let mtys = map (\ (n, (op, t)) -> + let t' = substMatches ips t in + (decorate ns n, op, coninsert cs t', t')) (class_methods ci) logLvl 3 (show (mtys, ips)) 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)) let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds' - let lhs = PRef fc iname + logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys) + -- get the implicit parameters that need passing through to the where block + wparams <- mapM (\p -> case p of + PApp _ _ args -> getWParams args + _ -> return []) ps + logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++ + show (concat (nub wparams)) + let lhs = case concat (nub wparams) of + [] -> PRef fc iname + as -> PApp fc (PRef fc iname) as let rhs = PApp fc (PRef fc (instanceName ci)) (map (pexp . mkMethApp) mtys) let idecl = PClauses fc [Inlinable, TCGen] iname - [PClause iname lhs [] rhs wb] + [PClause fc iname lhs [] rhs wb] iLOG (show idecl) elabDecl info idecl + addIBC (IBCInstance n iname) where - mkMethApp (n, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty)) + checkNotOverlapping i t n + | take 2 (show n) == "@@" = return () + | otherwise + = case lookupTy Nothing n (tt_ctxt i) of + [t'] -> let tret = getRetType t + tret' = getRetType (delab i t') in + case matchClause i tret' tret of + Right _ -> overlapping tret tret' + Left _ -> case matchClause i tret tret' of + Right _ -> overlapping tret tret' + Left _ -> return () + _ -> return () + overlapping t t' = tclift $ tfail (At fc (Msg $ + "Overlapping instance: " ++ show t' ++ " already defined")) + getRetType (PPi _ _ _ sc) = getRetType sc + getRetType t = t + + mkMethApp (n, _, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty)) lamBind i (PPi (Constraint _ _) _ _ sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc') lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc') @@ -519,10 +731,20 @@ papp fc f [] = f papp fc f as = PApp fc f as + getWParams [] = return [] + getWParams (p : ps) + | PRef _ n <- getTm p + = do ps' <- getWParams ps + ctxt <- getContext + case lookupP Nothing n ctxt of + [] -> return (pimp n (PRef fc n) : ps') + _ -> return ps' + getWParams (_ : ps) = getWParams ps + decorate ns (UN n) = NS (UN ('!':n)) ns decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns - mkTyDecl (n, t, _) = PTy syn fc n t + mkTyDecl (n, op, t, _) = PTy syn fc op n t conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x) conbind [] x = x @@ -538,8 +760,8 @@ insertDef meth def ns decls | null $ filter (clauseFor meth ns) decls = decls ++ [PClauses fc [Inlinable,TCGen] meth - [PClause meth (PApp fc (PRef fc meth) []) [] - (PApp fc (PRef fc def) []) []]] + [PClause fc meth (PApp fc (PRef fc meth) []) [] + (PApp fc (PRef fc def) []) []]] | otherwise = decls warnMissing decls ns meth @@ -550,11 +772,11 @@ clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m' clauseFor m ns _ = False -decorateid decorate (PTy s f n t) = PTy s f (decorate n) t +decorateid decorate (PTy s f o n t) = PTy s f o (decorate n) t decorateid decorate (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs) - where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds - dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w + where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds + dc (PWith fc n t as w ds) = PWith fc (decorate n) (dappname t) as w (map (decorateid decorate) ds) dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as dappname t = t @@ -585,12 +807,16 @@ elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate -elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n - elabType info s f n ty +elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n + elabType info s f o n ty elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d) elabData info s f d elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n - elabClauses info f o n ps + i <- get -- get the type options too + let o' = case lookupCtxt Nothing n (idris_flags i) of + [fs] -> fs + [] -> [] + elabClauses info f (o ++ o') n ps elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps where pinfo = let ds = concatMap declared ps @@ -609,10 +835,19 @@ elabDecl' info (PInstance s f cs n ps t ds) = do iLOG $ "Elaborating instance " ++ show n elabInstance info s f cs n ps t ds +elabDecl' info (PRecord s f tyn ty cn cty) + = do iLOG $ "Elaborating record " ++ show tyn + elabRecord info s f tyn ty cn cty +elabDecl' info (PDSL n dsl) + = do i <- get + put (i { idris_dsls = addDef n dsl (idris_dsls i) }) + addIBC (IBCDSL n) + elabDecl' info (PDirective i) = i elabCaseBlock info d@(PClauses f o n ps) = do addIBC (IBCDef n) +-- iputStrLn $ "CASE BLOCK: " ++ show (n, d) elabDecl' info d -- elabDecl' info (PImport i) = loadModule i @@ -625,10 +860,23 @@ checkInferred fc inf user = do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++ showImp True user - tclift $ case matchClause' True user inf of + i <- get + tclift $ case matchClause' True i user inf of Right vs -> return () Left (x, y) -> tfail $ At fc (Msg $ "The type-checked term and given term do not match: " ++ show x ++ " and " ++ show y) -- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user) + +-- Return whether inferred term is different from given term +-- (as above, but return a Bool) + +inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool +inferredDiff fc inf user = + do i <- get + logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++ + showImp True user + tclift $ case matchClause' True i user inf of + Right vs -> return False + Left (x, y) -> return True diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -1,6 +1,10 @@ +{-# LANGUAGE PatternGuards #-} + module Idris.ElabTerm where import Idris.AbsSyntax +import Idris.DSL +import Idris.Delaborate import Core.Elaborate hiding (Tactic(..)) import Core.TT @@ -59,7 +63,7 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm -> ElabD () elab ist info pattern tcgen fn tm - = do elabE False tm + = do elabE (False, False) tm -- (in argument, guarded) when pattern -- convert remaining holes to pattern vars mkPat inj <- get_inj @@ -97,7 +101,10 @@ (elab' ina (PRef fc unitTy)) elab' ina (PFalse fc) = elab' ina (PRef fc falseTy) elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes - = resolveTC 2 fn ist + = do t <- goal + -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist)) + let insts = findInstances ist t + resolveTC 2 fn insts 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, @@ -105,9 +112,10 @@ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder, pimp (MN 0 "b") Placeholder, pexp l, pexp r]) - elab' ina (PPair fc l r) = try (elabE True (PApp fc (PRef fc pairTy) + elab' ina@(_, a) (PPair fc l r) + = try (elabE (True, a) (PApp fc (PRef fc pairTy) [pexp l,pexp r])) - (elabE True (PApp fc (PRef fc pairCon) + (elabE (True, a) (PApp fc (PRef fc pairCon) [pimp (MN 0 "A") Placeholder, pimp (MN 0 "B") Placeholder, pexp l, pexp r])) @@ -132,31 +140,38 @@ (tryAll (zip (map (elab' ina) as) (map showHd as))) where showHd (PApp _ h _) = show h showHd x = show x - elab' ina (PRef fc n) | pattern && not (inparamBlock n) + elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n) = do ctxt <- get_context let iscon = isConName Nothing n ctxt - if (not iscon && ina) then erun fc $ patvar n - else try (do apply (Var n) []; solve) - (patvar n) + let defined = case lookupTy Nothing n ctxt of + [] -> False + _ -> True + -- this is to stop us resolve type classes recursively + -- trace (show (n, guarded)) $ + if (tcname n && ina) then erun fc $ patvar n + else if (defined && not guarded) + then do apply (Var n) []; solve + else try (do apply (Var n) []; solve) + (patvar n) where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of [] -> False _ -> True elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve - elab' ina (PLam n Placeholder sc) - = do attack; intro (Just n); elabE True sc; solve - elab' ina (PLam n ty sc) + elab' ina@(_, a) (PLam n Placeholder sc) + = do attack; intro (Just n); elabE (True, a) sc; solve + elab' ina@(_, a) (PLam n ty sc) = do tyn <- unique_hole (MN 0 "lamty") claim tyn RSet attack introTy (Var tyn) (Just n) -- end_unify focus tyn - elabE True ty - elabE True sc + elabE (True, a) ty + elabE (True, a) sc solve - elab' ina (PPi _ n Placeholder sc) - = do attack; arg n (MN 0 "ty"); elabE True sc; solve - elab' ina (PPi _ n ty sc) + elab' ina@(_,a) (PPi _ n Placeholder sc) + = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve + elab' ina@(_,a) (PPi _ n ty sc) = do attack; tyn <- unique_hole (MN 0 "ty") claim tyn RSet n' <- case n of @@ -164,10 +179,10 @@ _ -> return n forall n' (Var tyn) focus tyn - elabE True ty - elabE True sc + elabE (True, a) ty + elabE (True, a) sc solve - elab' ina (PLet n ty val sc) + elab' ina@(_,a) (PLet n ty val sc) = do attack; tyn <- unique_hole (MN 0 "letty") claim tyn RSet @@ -177,49 +192,60 @@ case ty of Placeholder -> return () _ -> do focus tyn - elabE True ty + elabE (True, a) ty focus valn - elabE True val - elabE True sc + elabE (True, a) val + elabE (True, a) sc solve - elab' ina (PApp fc (PRef _ f) args') +-- elab' ina (PTyped val ty) +-- = do tyn <- unique_hole (MN 0 "castty") +-- claim tyn RSet +-- valn <- unique_hole (MN 0 "castval") +-- claim valn (Var tyn) +-- focus tyn +-- elabE True ty +-- focus valn +-- elabE True val +-- elab' ina (PApp fc (PRef _ dsl) [arg]) +-- | [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') = do let args = {- case lookupCtxt f (inblock info) of Just ps -> (map (pexp . (PRef fc)) ps ++ args') _ ->-} args' ivs <- get_instances -- HACK: we shouldn't resolve type classes if we're defining an instance - -- function or default defition. + -- function or default definition. let isinf = f == inferCon || tcname f + 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)) (zip ns args) - try (elabArgs (ina || not isinf) + try (elabArgs (ina || not isinf, guarded) [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)) - (elabArgs (ina || not isinf) + (elabArgs (ina || not isinf, guarded) [] False (reverse ns') (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))) --- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args)) - (do apply_elab f (map (toElab (ina || not isinf)) args) - solve) + (do apply_elab f (map (toElab (ina || not isinf, guarded)) args) + solve) ivs' <- get_instances when (not pattern || (ina && not tcgen)) $ mapM_ (\n -> do focus n - resolveTC 7 fn ist) (ivs' \\ ivs) --- ivs <- get_instances --- when (not (null ivs)) $ --- do t <- get_term --- trace (show ivs ++ "\n" ++ show t) $ --- mapM_ (\n -> do focus n --- resolveTC ist) ivs + -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist)) + t <- goal + let insts = findInstances ist t + resolveTC 7 fn insts ist) (ivs' \\ ivs) where tcArg (n, PConstraint _ _ Placeholder) = True tcArg _ = False - elab' a (PApp fc f [arg]) + elab' ina@(_, a) (PApp fc f [arg]) = erun fc $ - do simple_app (elabE a f) (elabE True (getTm arg)) + do simple_app (elabE ina f) (elabE (True, a) (getTm arg)) solve elab' ina Placeholder = do (h : hs) <- get_holes movelast h @@ -230,9 +256,11 @@ Just xs@(_:_) -> NS n xs _ -> n elab' ina (PProof ts) = do mapM_ (runTac True ist) ts - elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts - elab' ina (PElabError e) = fail e - elab' ina c@(PCase fc scr opts) + elab' ina (PTactics ts) + | not pattern = do mapM_ (runTac False ist) ts + | otherwise = elab' ina Placeholder + elab' ina (PElabError e) = fail (pshow ist e) + elab' ina@(_, a) c@(PCase fc scr opts) = do attack tyn <- unique_hole (MN 0 "scty") claim tyn RSet @@ -241,11 +269,12 @@ claim valn (Var tyn) letbind scvn (Var tyn) (Var valn) focus valn - elabE True scr + elabE (True, a) scr args <- get_env cname <- unique_hole (mkCaseName fn) elab' ina (PMetavar cname) - let newdef = PClauses fc [] cname (caseBlock fc cname (reverse args) opts) + let cname' = mkN cname + let newdef = PClauses fc [] cname' (caseBlock fc cname' (reverse args) opts) -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args -- elaborate case updateAux (newdef : ) @@ -253,6 +282,10 @@ where mkCaseName (NS n ns) = NS (mkCaseName n) ns mkCaseName (UN x) = UN (x ++ "_case") mkCaseName (MN i x) = MN i (x ++ "_case") + mkN n@(NS _ _) = n + mkN n = case namespace info of + Just xs@(_:_) -> NS n xs + _ -> n elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?" caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause] @@ -262,7 +295,7 @@ where -- mkarg (MN _ _) = Placeholder mkarg n = PRef fc n mkClause args (l, r) - = PClause n (PApp fc (PRef fc n) + = PClause fc n (PApp fc (PRef fc n) (map pexp args ++ [pexp l])) [] r [] elabArgs ina failed retry [] _ @@ -315,17 +348,27 @@ (MN 0 "tac") (PRef (FC "prf" 0) x)) (tryAll xs) -resolveTC :: Int -> Name -> IState -> ElabD () -resolveTC 0 fn ist = fail $ "Can't resolve type class" -resolveTC depth fn ist +findInstances :: IState -> Term -> [Name] +findInstances ist t + | (P _ n _, _) <- unApply t + = case lookupCtxt Nothing n (idris_classes ist) of + [CI _ _ _ _ ins] -> ins + _ -> [] + | 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 = try (trivial ist) (do t <- goal let (tc, ttypes) = unApply t - needsDefault t tc ttypes + scopeOnly <- needsDefault t tc ttypes tm <- get_term -- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $ -- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist))))) - blunderbuss t (map fst (ctxtAlist (tt_ctxt ist)))) + let depth' = if scopeOnly then 2 else depth + blunderbuss t depth' insts) where elabTC n | n /= fn && tcname n = (resolve n depth, show n) | otherwise = (fail "Can't resolve", show n) @@ -334,33 +377,38 @@ = do focus a fill (RConstant IType) -- default Int solve --- needsDefault t f as --- | all boundVar as = fail $ "Can't resolve " ++ show t - needsDefault t f a = return () + 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 () boundVar (P Bound _ _) = True boundVar _ = False - blunderbuss t [] = fail $ "Can't resolve type class " ++ show t - blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth) - (blunderbuss t ns) - | otherwise = blunderbuss t ns + blunderbuss t d [] = lift $ tfail $ CantResolve t + blunderbuss t d (n:ns) + | n /= fn && tcname n = try (resolve n d) + (blunderbuss t d ns) + | otherwise = blunderbuss t d ns resolve n depth | depth == 0 = fail $ "Can't resolve type class" | otherwise - = do t <- goal + = do t <- goal + let (tc, ttypes) = unApply t +-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist +-- else do -- if there's a hole in the goal, don't even try - let imps = case lookupCtxtName Nothing n (idris_implicits ist) of + let imps = case lookupCtxtName Nothing n (idris_implicits ist) of [] -> [] [args] -> map isImp (snd args) -- won't be overloaded! - args <- apply (Var n) imps - tm <- get_term - mapM_ (\ (_,n) -> do focus n - resolveTC (depth - 1) fn ist) - (filter (\ (x, y) -> not x) (zip (map fst imps) args)) - -- if there's any arguments left, we've failed to resolve - solve + 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) + (filter (\ (x, y) -> not x) (zip (map fst imps) args)) + -- if there's any arguments left, we've failed to resolve + solve where isImp (PImp p _ _ _) = (True, p) isImp arg = (False, priority arg) diff --git a/src/Idris/Error.hs b/src/Idris/Error.hs --- a/src/Idris/Error.hs +++ b/src/Idris/Error.hs @@ -56,6 +56,7 @@ getErrLine str = case span (/=':') str of (_, ':':rest) -> case span isDigit rest of + ([], _) -> 0 (num, _) -> read num _ -> 0 diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -13,7 +13,6 @@ import Data.Binary import Data.List import Data.ByteString.Lazy as B hiding (length, elem) --- import Data.DeriveTH import Control.Monad import Control.Monad.State hiding (get, put) import System.FilePath @@ -22,7 +21,7 @@ import Paths_idris ibcVersion :: Word8 -ibcVersion = 8 +ibcVersion = 16 data IBCFile = IBCFile { ver :: Word8, sourcefile :: FilePath, @@ -31,6 +30,8 @@ ibc_fixes :: [FixDecl], ibc_statics :: [(Name, [Bool])], ibc_classes :: [(Name, ClassInfo)], + ibc_instances :: [(Name, Name)], + ibc_dsls :: [(Name, DSL)], ibc_datatypes :: [(Name, TypeInfo)], ibc_optimise :: [(Name, OptInfo)], ibc_syntax :: [Syntax], @@ -39,13 +40,16 @@ ibc_libs :: [String], ibc_hdrs :: [String], ibc_access :: [(Name, Accessibility)], + ibc_total :: [(Name, Totality)], + ibc_flags :: [(Name, [FnOpt])], + ibc_cg :: [(Name, [Name])], ibc_defs :: [(Name, Def)] } {-! deriving instance Binary IBCFile !-} initIBC :: IBCFile -initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] +initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] loadIBC :: FilePath -> Idris () loadIBC fp = do iLOG $ "Loading ibc " ++ fp @@ -84,6 +88,12 @@ = 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 (IBCDSL n) f + = case lookupCtxt Nothing n (idris_dsls i) of + [v] -> return f { ibc_dsls = (n,v): ibc_dsls f } + _ -> fail "IBC write failed" ibc i (IBCData n) f = case lookupCtxt Nothing n (idris_datatypes i) of [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f } @@ -100,7 +110,12 @@ ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of [v] -> return f { ibc_defs = (n,v) : ibc_defs f } _ -> fail "IBC write failed" +ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of + [v] -> return f { ibc_cg = (n,v) : ibc_cg f } + _ -> fail "IBC write failed" ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f } +ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f } +ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f } process :: IBCFile -> FilePath -> Idris () process i fn @@ -116,6 +131,8 @@ pFixes (ibc_fixes i) pStatics (ibc_statics i) pClasses (ibc_classes i) + pInstances (ibc_instances i) + pDSLs (ibc_dsls i) pDatatypes (ibc_datatypes i) pOptimise (ibc_optimise i) pSyntax (ibc_syntax i) @@ -125,6 +142,8 @@ pHdrs (ibc_hdrs i) pDefs (ibc_defs i) pAccess (ibc_access i) + pTotal (ibc_total i) + pCG (ibc_cg i) timestampOlder :: FilePath -> FilePath -> IO () timestampOlder src ibc = do srct <- getModificationTime src @@ -174,6 +193,16 @@ = addDef n c (idris_classes i) })) cs +pInstances :: [(Name, Name)] -> Idris () +pInstances cs = mapM_ (\ (n, ins) -> addInstance n ins) cs + +pDSLs :: [(Name, DSL)] -> Idris () +pDSLs cs = mapM_ (\ (n, c) -> + do i <- getIState + putIState (i { idris_dsls + = addDef n c (idris_dsls i) })) + cs + pDatatypes :: [(Name, TypeInfo)] -> Idris () pDatatypes cs = mapM_ (\ (n, c) -> do i <- getIState @@ -218,6 +247,18 @@ putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds +pFlags :: [(Name, [FnOpt])] -> Idris () +pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds + +pTotal :: [(Name, Totality)] -> Idris () +pTotal ds = mapM_ (\ (n, a) -> + do i <- getIState + putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) })) + ds + +pCG :: [(Name, [Name])] -> Idris () +pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds + ----- Generated by 'derive' @@ -567,8 +608,48 @@ 2 -> return Hidden _ -> error "Corrupted binary data for Accessibility" +instance Binary PReason where + put x + = case x of + Other x1 -> do putWord8 0 + put x1 + Itself -> putWord8 1 + NotCovering -> putWord8 2 + NotPositive -> putWord8 3 + Mutual x1 -> do putWord8 4 + put x1 + get + = do i <- getWord8 + case i of + 0 -> do x1 <- get + return (Other x1) + 1 -> return Itself + 2 -> return NotCovering + 3 -> return NotPositive + 4 -> do x1 <- get + return (Mutual x1) + _ -> error "Corrupted binary data for PReason" + +instance Binary Totality where + put x + = case x of + Total x1 -> do putWord8 0 + put x1 + Partial x1 -> do putWord8 1 + put x1 + Unchecked -> do putWord8 2 + get + = do i <- getWord8 + case i of + 0 -> do x1 <- get + return (Total x1) + 1 -> do x1 <- get + return (Partial x1) + 2 -> return Unchecked + _ -> error "Corrupted binary data for Totality" + instance Binary IBCFile where - put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) + put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21) = do put x1 put x2 put x3 @@ -585,6 +666,11 @@ put x14 put x15 put x16 + put x17 + put x18 + put x19 + put x20 + put x21 get = do x1 <- get if x1 == ibcVersion then @@ -603,9 +689,30 @@ x14 <- get x15 <- get x16 <- get - return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) + x17 <- get + x18 <- get + x19 <- get + x20 <- get + x21 <- get + return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21) else return (initIBC { ver = x1 }) +instance Binary FnOpt where + put x + = case x of + Inlinable -> putWord8 0 + TotalFn -> putWord8 1 + TCGen -> putWord8 2 + AssertTotal -> putWord8 3 + get + = do i <- getWord8 + case i of + 0 -> return Inlinable + 1 -> return TotalFn + 2 -> return TCGen + 3 -> return AssertTotal + _ -> error "Corrupted binary data for FnOpt" + instance Binary Fixity where put x = case x of @@ -746,8 +853,8 @@ put x1 PTactics x1 -> do putWord8 22 put x1 - PElabError x1 -> do putWord8 23 - put x1 +-- PElabError x1 -> do putWord8 23 +-- put x1 PImpossible -> putWord8 24 get = do i <- getWord8 @@ -814,8 +921,8 @@ return (PProof x1) 22 -> do x1 <- get return (PTactics x1) - 23 -> do x1 <- get - return (PElabError x1) +-- 23 -> do x1 <- get +-- return (PElabError x1) 24 -> return PImpossible _ -> error "Corrupted binary data for PTerm" @@ -970,7 +1077,7 @@ instance Binary ClassInfo where - put (CI x1 x2 x3 x4) + put (CI x1 x2 x3 x4 _) = do put x1 put x2 put x3 @@ -980,7 +1087,7 @@ x2 <- get x3 <- get x4 <- get - return (CI x1 x2 x3 x4) + return (CI x1 x2 x3 x4 []) instance Binary OptInfo where put (Optimise x1 x2 x3) @@ -1024,6 +1131,28 @@ x3 <- get return (Rule x1 x2 x3) +instance (Binary t) => Binary (DSL' t) where + put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9) + = do put x1 + put x2 + put x3 + put x4 + put x5 + put x6 + put x7 + put x8 + put x9 + get + = do x1 <- get + x2 <- get + x3 <- get + x4 <- get + x5 <- get + x6 <- get + x7 <- get + x8 <- get + x9 <- get + return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9) instance Binary SSymbol where put x @@ -1034,6 +1163,8 @@ put x1 Expr x1 -> do putWord8 2 put x1 + SimpleExpr x1 -> do putWord8 3 + put x1 get = do i <- getWord8 case i of @@ -1043,4 +1174,6 @@ return (Symbol x1) 2 -> do x1 <- get return (Expr x1) + 3 -> do x1 <- get + return (SimpleExpr x1) _ -> error "Corrupted binary data for SSymbol" diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -1,10 +1,14 @@ +{-# LANGUAGE PatternGuards #-} + module Idris.Parser where import Idris.AbsSyntax +import Idris.DSL import Idris.Imports import Idris.Error import Idris.ElabDecls import Idris.ElabTerm +import Idris.Coverage import Idris.IBC import Idris.Unlit import Paths_idris @@ -97,6 +101,8 @@ v <- verbose when v $ iputStrLn $ "Type checking " ++ f mapM_ (elabDecl toplevel) ds + i <- get + mapM_ checkDeclTotality (idris_totcheck i) iLOG ("Finished " ++ f) let ibc = dropExtension f ++ ".ibc" iucheck @@ -106,6 +112,7 @@ when ok $ idrisCatch (do writeIBC f ibc; clearIBC) (\c -> return ()) -- failure is harmless + i <- getIState putIState (i { hide_list = [] }) return () where @@ -273,14 +280,14 @@ collect :: [PDecl] -> [PDecl] collect (c@(PClauses _ o _ _) : ds) = clauses (cname c) [] (c : ds) - where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds) - | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds - clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds) - | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds + where clauses n acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds) + | n == n' = clauses n (PClause fc' n' l ws r (collect w) : acc) ds + clauses n acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds) + | n == n' = clauses n (PWith fc' n' l ws r (collect w) : acc) ds clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs - cname (PClauses fc _ _ [PClause n _ _ _ _]) = n - cname (PClauses fc _ _ [PWith n _ _ _ _]) = n + cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = n + cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = n getfc (PClauses fc _ _ _) = fc collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds @@ -310,10 +317,10 @@ <|> pNamespace syn <|> pClass syn <|> pInstance syn + <|> do d <- pDSL syn; return [d] <|> pDirective <|> try (do reserved "import" fp <- identifier - lchar ';' fail "imports must be at the top of file") pFunDecl :: SyntaxInfo -> IParser [PDecl] @@ -331,6 +338,7 @@ = try pFixity <|> pFunDecl' syn <|> try (pData syn) + <|> try (pRecord syn) <|> pSyntaxDecl syn pSyntaxDecl :: SyntaxInfo -> IParser PDecl @@ -366,13 +374,23 @@ lchar '=' tm <- pExpr syn pTerminator - return (Rule syms tm sty) + return (Rule (mkSimple syms) tm sty) where expr (Expr _) = True expr _ = False name (Expr n) = Just n name _ = Nothing + -- Can't parse two full expressions (i.e. expressions with application) in a row + -- so change the first to a simple expression + + mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es + mkSimple xs = mkSimple' xs + + mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es) + mkSimple' (e : es) = e : mkSimple' es + mkSimple' [] = [] + pSynSym :: IParser SSymbol pSynSym = try (do lchar '['; n <- pName; lchar ']' return (Expr n)) @@ -383,7 +401,9 @@ pFunDecl' :: SyntaxInfo -> IParser PDecl pFunDecl' syn = try (do push_indent + opts <- pFnOpts acc <- pAccessibility + opts' <- pFnOpts n_in <- pfName let n = expandNS syn n_in ty <- pTSig syn @@ -391,7 +411,7 @@ pTerminator -- ty' <- implicit syn n ty addAcc n acc - return (PTy syn fc n ty)) + return (PTy syn fc (opts ++ opts') n ty)) <|> try (pPattern syn) pUsing :: SyntaxInfo -> IParser [PDecl] @@ -428,12 +448,6 @@ close_block return [PNamespace n (concat ds)] -expandNS :: SyntaxInfo -> Name -> Name -expandNS syn n@(NS _ _) = n -expandNS syn n = case syn_namespace syn of - [] -> n - xs -> NS n xs - --------- Fixity --------- pFixity :: IParser PDecl @@ -508,6 +522,7 @@ pExtensions syn (filter simple (syntax_rules i)) where simple (Rule (Expr x:xs) _ _) = False + simple (Rule (SimpleExpr x:xs) _ _) = False simple (Rule [Keyword _] _ _) = True simple (Rule [Symbol _] _ _) = True simple (Rule (_:xs) _ _) = case (last xs) of @@ -518,6 +533,7 @@ pNoExtExpr syn = try (pApp syn) + <|> pRecordSet syn <|> try (pSimpleExpr syn) <|> pLambda syn <|> pLet syn @@ -534,17 +550,18 @@ pExt :: SyntaxInfo -> Syntax -> IParser PTerm -pExt syn (Rule (s:ssym) ptm _) - = do s1 <- pSymbol pSimpleExpr s - smap <- mapM (pSymbol pExpr) ssym - let ns = mapMaybe id (s1:smap) +pExt syn (Rule ssym ptm _) + = do smap <- mapM pSymbol ssym + let ns = mapMaybe id smap return (update ns ptm) -- updated with smap where - pSymbol p (Keyword n) = do reserved (show n); return Nothing - pSymbol p (Expr n) = do tm <- p syn - return $ Just (n, tm) - pSymbol p (Symbol s) = do symbol s - return Nothing + pSymbol (Keyword n) = do reserved (show n); return Nothing + pSymbol (Expr n) = do tm <- pExpr syn + return $ Just (n, tm) + pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn + return $ Just (n, tm) + pSymbol (Symbol s) = do symbol s + return Nothing dropn n [] = [] dropn n ((x,t) : xs) | n == x = xs | otherwise = (x,t):dropn n xs @@ -595,6 +612,11 @@ = do acc <- pAccessibility'; return (Just acc) <|> return Nothing +pFnOpts :: IParser [FnOpt] +pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs) + <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs) + <|> return [] + addAcc :: Name -> Maybe Accessibility -> IParser () addAcc n a = do i <- getState setState (i { hide_list = (n, a) : hide_list i }) @@ -639,6 +661,9 @@ bracketed syn = try (pPair syn) <|> try (do e <- pExpr syn; lchar ')'; return e) +-- <|> try (do reserved "typed" +-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')' +-- return (PTyped e t)) <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')' return $ PLam (MN 0 "x") Placeholder (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")), @@ -713,7 +738,13 @@ fc <- pfc args <- many1 (do notEndApp pArg syn) - return (PApp fc f args) + i <- getState + return (dslify i $ PApp fc f args) + where + dslify i (PApp fc (PRef _ f) [a]) + | [d] <- lookupCtxt Nothing f (idris_dsls i) + = desugar (syn { dsl_info = d }) i (getTm a) + dslify i t = t pArg :: SyntaxInfo -> IParser PArg pArg syn = try (pImplicitArg syn) @@ -730,6 +761,29 @@ pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}" return (pconst e) +pRecordSet syn + = do reserved "record" + lchar '{' + fields <- sepBy1 pFieldSet (lchar ',') + lchar '}' + fc <- pfc + rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e)) + case rec of + Nothing -> + return (PLam (MN 0 "fldx") Placeholder + (applyAll fc fields (PRef fc (MN 0 "fldx")))) + Just v -> return (applyAll fc fields v) + where pFieldSet = do n <- pfName; lchar '=' + e <- pExpr syn + return (n, e) + applyAll fc [] x = x + applyAll fc ((n, e) : es) x + = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x]) + +mkSet (UN n) = UN ("set_" ++ n) +mkSet (MN 0 n) = MN 0 ("set_" ++ n) +mkSet (NS n s) = NS (mkSet n) s + pTSig syn = do lchar ':' cs <- pConstList syn sc <- pExpr syn @@ -775,6 +829,17 @@ symbol "->" sc <- pExpr syn return (bindList (PPi (Imp lazy st)) xt sc)) + <|> try (do lchar '{'; reserved "auto" + xt <- tyDeclList syn; lchar '}' + symbol "->" + sc <- pExpr syn + return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc)) + <|> try (do lchar '{'; reserved "default" + script <- pSimpleExpr syn + xt <- tyDeclList syn; lchar '}' + symbol "->" + sc <- pExpr syn + return (bindList (PPi (TacImp False Dynamic script)) xt sc)) <|> do --lazy <- option False (do lchar '|'; return True) lchar '{'; reserved "static"; lchar '}' t <- pExpr' syn @@ -897,6 +962,32 @@ mapM_ (\n -> addAcc n (Just Hidden)) ns accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns +pRecord :: SyntaxInfo -> IParser PDecl +pRecord syn = do acc <- pAccessibility + reserved "record"; fc <- pfc + tyn_in <- pfName; ty <- pTSig syn + let tyn = expandNS syn tyn_in + reserved "where" + open_block + push_indent + (cn, cty, _) <- pConstructor syn + pKeepTerminator + pop_indent + close_block + accData acc tyn [cn] + let rsyn = syn { syn_namespace = show (nsroot tyn) : + syn_namespace syn } + let fns = getRecNames rsyn cty + mapM_ (\n -> addAcc n (toFreeze acc)) fns + return $ PRecord rsyn fc tyn ty cn cty + where + getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)] + ++ getRecNames syn sc + getRecNames _ _ = [] + + toFreeze (Just Frozen) = Just Hidden + toFreeze x = x + pData :: SyntaxInfo -> IParser PDecl pData syn = try (do acc <- pAccessibility reserved "data"; fc <- pfc @@ -937,12 +1028,13 @@ bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t) pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC) -pConstructor syn +pConstructor syn = do cn_in <- pfName; fc <- pfc let cn = expandNS syn cn_in ty <- pTSig syn -- ty' <- implicit syn cn ty return (cn, ty, fc) + pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC) pSimpleCon syn @@ -953,11 +1045,50 @@ pSimpleExpr syn) return (cn, args, fc) +--------- DSL syntax overloading --------- + +pDSL :: SyntaxInfo -> IParser PDecl +pDSL syn = do reserved "dsl"; n <- pfName + open_block; push_indent + bs <- many1 (do notEndBlock + b <- pOverload syn + pKeepTerminator + return b) + pop_indent; close_block + let dsl = mkDSL bs (dsl_info syn) + checkDSL dsl + i <- getState + setState (i { idris_dsls = addDef n dsl (idris_dsls i) }) + return (PDSL n dsl) + where mkDSL bs dsl = let var = lookup "variable" bs + first = lookup "index_first" bs + next = lookup "index_next" bs + leto = lookup "let" bs + lambda = lookup "lambda" bs in + initDSL { dsl_var = var, + index_first = first, + index_next = next, + dsl_lambda = lambda, + dsl_let = leto } + +checkDSL :: DSL -> IParser () +checkDSL dsl = return () + +pOverload :: SyntaxInfo -> IParser (String, PTerm) +pOverload syn = do o <- identifier <|> do reserved "let"; return "let" + if (not (o `elem` overloadable)) + then fail $ show o ++ " is not an overloading" + else do + lchar '=' + t <- pExpr syn + return (o, t) + where overloadable = ["let","lambda","index_first","index_next","variable"] + --------- Pattern match clauses --------- pPattern :: SyntaxInfo -> IParser PDecl -pPattern syn = do clause <- pClause syn - fc <- pfc +pPattern syn = do fc <- pfc + clause <- pClause syn return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later pArgExpr syn = let syn' = syn { inPattern = True } in @@ -994,13 +1125,14 @@ (iargs ++ cargs ++ map pexp args) ist <- getState setState (ist { lastParse = Just n }) - return $ PClause n capp wargs rhs wheres) + return $ PClause fc n capp wargs rhs wheres) <|> try (do push_indent wargs <- many1 (pWExpr syn) ist <- getState n <- case lastParse ist of Just t -> return t Nothing -> fail "Invalid clause" + fc <- pfc rhs <- pRHS syn n let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } @@ -1009,7 +1141,7 @@ return x, do pTerminator return ([], [])] - return $ PClauseR wargs rhs wheres) + return $ PClauseR fc wargs rhs wheres) <|> try (do push_indent n_in <- pfName; let n = expandNS syn n_in @@ -1029,16 +1161,17 @@ ist <- getState setState (ist { lastParse = Just n }) pop_indent - return $ PWith n capp wargs wval withs) + return $ PWith fc n capp wargs wval withs) <|> try (do wargs <- many1 (pWExpr syn) + fc <- pfc reserved "with" wval <- pSimpleExpr syn open_block ds <- many1 $ pFunDecl syn let withs = concat ds close_block - return $ PWithR wargs wval withs) + return $ PWithR fc wargs wval withs) <|> do push_indent l <- pArgExpr syn @@ -1057,7 +1190,7 @@ ist <- getState let capp = PApp fc (PRef fc n) [pexp l, pexp r] setState (ist { lastParse = Just n }) - return $ PClause n capp wargs rhs wheres + return $ PClause fc n capp wargs rhs wheres <|> do l <- pArgExpr syn op <- operator @@ -1074,12 +1207,12 @@ let capp = PApp fc (PRef fc n) [pexp l, pexp r] let withs = map (fillLHSD n capp wargs) $ concat ds setState (ist { lastParse = Just n }) - return $ PWith n capp wargs wval withs + return $ PWith fc n capp wargs wval withs where - fillLHS n capp owargs (PClauseR wargs v ws) - = PClause n capp (owargs ++ wargs) v ws - fillLHS n capp owargs (PWithR wargs v ws) - = PWith n capp (owargs ++ wargs) v + fillLHS n capp owargs (PClauseR fc wargs v ws) + = PClause fc n capp (owargs ++ wargs) v ws + fillLHS n capp owargs (PWithR fc wargs v ws) + = PWith fc n capp (owargs ++ wargs) v (map (fillLHSD n capp (owargs ++ wargs)) ws) fillLHS _ _ _ c = c @@ -1161,59 +1294,9 @@ <|> do reserved "term"; return ProofTerm <|> do reserved "undo"; return Undo <|> do reserved "qed"; return Qed + <|> do reserved "abandon"; return Abandon + <|> do lchar ':'; reserved "q"; return Abandon where imp = do lchar '?'; return False <|> do lchar '_'; return True - -desugar :: SyntaxInfo -> IState -> PTerm -> PTerm -desugar syn i t = let t' = expandDo (dsl_info syn) t in - t' -- addImpl i t' - -expandDo :: DSL -> PTerm -> PTerm -expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm) -expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm) -expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm) -expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t) - (map (fmap (expandDo dsl)) args) -expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s) - (map (pmap (expandDo dsl)) opts) -expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r) -expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t) - (expandDo dsl r) -expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as) -expandDo dsl (PHidden t) = PHidden (expandDo dsl t) -expandDo dsl (PReturn fc) = dsl_return dsl -expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds - where - block b [DoExp fc tm] = tm - block b [a] = PElabError "Last statement in do block must be an expression" - block b (DoBind fc n tm : rest) - = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))] - block b (DoBindP fc p tm : rest) - = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder - (PCase fc (PRef fc (MN 0 "bpat")) - [(p, block b rest)]))] - block b (DoLet fc n ty tm : rest) - = PLet n ty tm (block b rest) - block b (DoLetP fc p tm : rest) - = PCase fc tm [(p, block b rest)] - block b (DoExp fc tm : rest) - = PApp fc b - [pexp tm, - pexp (PLam (MN 0 "bindx") Placeholder (block b rest))] - block b _ = PElabError "Invalid statement in do block" -expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e -expandDo dsl t = t - -unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm -unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in - mkap (getFn e) - where - getFn (PApp fc f args) = (PApp fc pure [pexp f], args) - getFn f = (f, []) - - mkap (f, []) = f - mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as) - -unIdiom ap pure fc e = PApp fc pure [pexp e] diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs --- a/src/Idris/Primitives.hs +++ b/src/Idris/Primitives.hs @@ -16,7 +16,8 @@ p_type :: Type, p_arity :: Int, p_def :: [Value] -> Maybe Value, - p_epic :: ([E.Name], E.Term) + p_epic :: ([E.Name], E.Term), + p_total :: Totality } ty [] x = Constant x @@ -71,138 +72,141 @@ strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)] strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)] +total = Total [] +partial = Partial NotCovering + primitives = -- operators [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+)) - (eOp E.plus_), + (eOp E.plus_) total, Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-)) - (eOp E.minus_), + (eOp E.minus_) total, Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*)) - (eOp E.times_), + (eOp E.times_) total, Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div)) - (eOp E.divide_), + (eOp E.divide_) partial, Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==)) - (eOp E.eq_), + (eOp E.eq_) total, Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<)) - (eOp E.lt_), + (eOp E.lt_) total, Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=)) - (eOp E.lte_), + (eOp E.lte_) total, Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>)) - (eOp E.gt_), + (eOp E.gt_) total, Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=)) - (eOp E.gte_), + (eOp E.gte_) total, Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==)) - (eOp E.eq_), + (eOp E.eq_) total, Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<)) - (eOp E.lt_), + (eOp E.lt_) total, Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=)) - (eOp E.lte_), + (eOp E.lte_) total, Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>)) - (eOp E.gt_), + (eOp E.gt_) total, Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=)) - (eOp E.gte_), + (eOp E.gte_) total, Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+)) - (eOpFn tyBigInt tyBigInt "addBig"), + (eOpFn tyBigInt tyBigInt "addBig") total, Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-)) - (eOpFn tyBigInt tyBigInt "subBig"), + (eOpFn tyBigInt tyBigInt "subBig") total, Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*)) - (eOpFn tyBigInt tyBigInt "mulBig"), + (eOpFn tyBigInt tyBigInt "mulBig") total, Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div)) - (eOpFn tyBigInt tyBigInt "divBig"), + (eOpFn tyBigInt tyBigInt "divBig") partial, Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==)) - (eOpFn tyBigInt tyInt "eqBig"), + (eOpFn tyBigInt tyInt "eqBig") total, Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<)) - (eOpFn tyBigInt tyInt "ltBig"), + (eOpFn tyBigInt tyInt "ltBig") total, Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=)) - (eOpFn tyBigInt tyInt "leBig"), + (eOpFn tyBigInt tyInt "leBig") total, Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>)) - (eOpFn tyBigInt tyInt "gtBig"), + (eOpFn tyBigInt tyInt "gtBig") total, Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=)) - (eOpFn tyBigInt tyInt "geBig"), + (eOpFn tyBigInt tyInt "geBig") total, Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+)) - (eOp E.plusF_), + (eOp E.plusF_) total, Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-)) - (eOp E.minusF_), + (eOp E.minusF_) total, Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*)) - (eOp E.timesF_), + (eOp E.timesF_) total, Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/)) - (eOp E.divideF_), + (eOp E.divideF_) total, Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==)) - (eOp E.eqF_), + (eOp E.eqF_) total, Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<)) - (eOp E.ltF_), + (eOp E.ltF_) total, Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=)) - (eOp E.lteF_), + (eOp E.lteF_) total, Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>)) - (eOp E.gtF_), + (eOp E.gtF_) total, Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=)) - (eOp E.gteF_), + (eOp E.gteF_) total, Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++)) - ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"), + ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y") total, Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==)) - ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")), + ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")) total, Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<)) - ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")), + ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")) total, -- Conversions Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt) - ([E.name "x"], strToInt (fun "x")), + ([E.name "x"], strToInt (fun "x")) total, Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr) - ([E.name "x"], intToStr (fun "x")), + ([E.name "x"], intToStr (fun "x")) total, Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt) - ([E.name "x"], charToInt (fun "x")), + ([E.name "x"], charToInt (fun "x")) total, Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar) - ([E.name "x"], intToChar (fun "x")), + ([E.name "x"], intToChar (fun "x")) total, Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt) - ([E.name "x"], intToBigInt (fun "x")), + ([E.name "x"], intToBigInt (fun "x")) total, Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt) - ([E.name "x"], strToBigInt (fun "x")), + ([E.name "x"], strToBigInt (fun "x")) total, Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr) - ([E.name "x"], bigIntToStr (fun "x")), + ([E.name "x"], bigIntToStr (fun "x")) total, Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat) - ([E.name "x"], strToFloat (fun "x")), + ([E.name "x"], strToFloat (fun "x")) total, Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr) - ([E.name "x"], floatToStr (fun "x")), + ([E.name "x"], floatToStr (fun "x")) total, Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat) - ([E.name "x"], intToFloat (fun "x")), + ([E.name "x"], intToFloat (fun "x")) total, Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt) - ([E.name "x"], floatToInt (fun "x")), + ([E.name "x"], floatToInt (fun "x")) total, Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp) - ([E.name "x"], floatExp (fun "x")), + ([E.name "x"], floatExp (fun "x")) total, Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog) - ([E.name "x"], floatLog (fun "x")), + ([E.name "x"], floatLog (fun "x")) total, Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin) - ([E.name "x"], floatSin (fun "x")), + ([E.name "x"], floatSin (fun "x")) total, Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos) - ([E.name "x"], floatCos (fun "x")), + ([E.name "x"], floatCos (fun "x")) total, Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan) - ([E.name "x"], floatTan (fun "x")), + ([E.name "x"], floatTan (fun "x")) total, Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin) - ([E.name "x"], floatASin (fun "x")), + ([E.name "x"], floatASin (fun "x")) total, Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos) - ([E.name "x"], floatACos (fun "x")), + ([E.name "x"], floatACos (fun "x")) total, Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan) - ([E.name "x"], floatATan (fun "x")), + ([E.name "x"], floatATan (fun "x")) total, Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt) - ([E.name "x"], floatSqrt (fun "x")), + ([E.name "x"], floatSqrt (fun "x")) total, Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor) - ([E.name "x"], floatFloor (fun "x")), + ([E.name "x"], floatFloor (fun "x")) total, Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil) - ([E.name "x"], floatCeil (fun "x")), + ([E.name "x"], floatCeil (fun "x")) total, Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead) - ([E.name "x"], strHead (fun "x")), + ([E.name "x"], strHead (fun "x")) partial, Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail) - ([E.name "x"], strTail (fun "x")), + ([E.name "x"], strTail (fun "x")) partial, Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons) - ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")), + ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")) total, Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex) - ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")), + ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")) partial, Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev) - ([E.name "x"], strRev (fun "x")), + ([E.name "x"], strRev (fun "x")) total, Prim (UN "prim__believe_me") believeTy 3 (p_believeMe) - ([E.name "a", E.name "b", E.name "x"], fun "x") + ([E.name "a", E.name "b", E.name "x"], fun "x") total -- ahem ] p_believeMe [_,_,x] = Just x @@ -241,7 +245,9 @@ c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x)) c_intToStr _ = Nothing -c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x)) +c_strToInt [VConstant (Str x)] = case reads x of + [(n,"")] -> Just $ VConstant (I n) + _ -> Just $ VConstant (I 0) c_strToInt _ = Nothing c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x)) @@ -254,12 +260,16 @@ c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x)) c_bigIntToStr _ = Nothing -c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x)) +c_strToBigInt [VConstant (Str x)] = case reads x of + [(n,"")] -> Just $ VConstant (BI n) + _ -> Just $ VConstant (BI 0) c_strToBigInt _ = Nothing c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x)) c_floatToStr _ = Nothing -c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x)) +c_strToFloat [VConstant (Str x)] = case reads x of + [(n,"")] -> Just $ VConstant (Fl n) + _ -> Just $ VConstant (Fl 0) c_strToFloat _ = Nothing c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x)) @@ -296,8 +306,9 @@ p_strRev _ = Nothing elabPrim :: Prim -> Idris () -elabPrim (Prim n ty i def epic) +elabPrim (Prim n ty i def epic tot) = do updateContext (addOperator n ty i def) + setTotality n tot i <- getIState putIState i { idris_prims = (n, epic) : idris_prims i } diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -93,6 +93,9 @@ (cmd, step) <- case x of Nothing -> fail "Abandoned" Just input -> do return (parseTac i input, input) + case cmd of + Right Abandon -> fail "Abandoned" + _ -> return () (d, st, done, prf') <- idrisCatch (case cmd of Left err -> do iputStrLn (show err) diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -12,6 +12,7 @@ import Idris.Compiler import Idris.Prover import Idris.Parser +import Idris.Coverage import Paths_idris import Core.Evaluate @@ -176,9 +177,16 @@ [] -> return () [d] -> do iputStrLn "Original definiton:\n" mapM_ (printCase i) d + case lookupTotal n (tt_ctxt i) of + [t] -> iputStrLn (showTotal t i) + _ -> return () where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs) liftIO $ putStr " = " liftIO $ putStrLn $ showImp True (delab i rhs) +process fn (TotCheck n) = do i <- get + case lookupTotal n (tt_ctxt i) of + [t] -> iputStrLn (showTotal t i) + _ -> return () process fn (Info n) = do i <- get let oi = lookupCtxt Nothing n (idris_optimisation i) liftIO $ print oi @@ -187,7 +195,12 @@ ist <- get let tm' = specialise ctxt (idris_statics ist) tm iputStrLn (show (delab ist tm')) -process fn (Prove n) = prover (lit fn) n +process fn (Prove n) = do prover (lit fn) n + -- recheck totality + i <- get + totcheck (FC "(input)" 0, n) + mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i) + mapM_ checkDeclTotality (idris_totcheck i) process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext ist <- get @@ -223,6 +236,13 @@ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs process fn NOP = return () +showTotal t@(Partial (Other ns)) i + = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns) +showTotal t i = show t +showTotalN i n = case lookupTotal n (tt_ctxt i) of + [t] -> showTotal t i + _ -> "" + displayHelp = let vstr = showVersion version in "\nIdris version " ++ vstr ++ "\n" ++ "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++ @@ -237,6 +257,7 @@ ([""], "", ""), ([""], "", "Evaluate an expression"), ([":t"], "", "Check the type of an expression"), + ([":total"], "", "Check the totality of a name"), ([":r",":reload"], "", "Reload current file"), ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"), ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"), diff --git a/src/Idris/REPLParser.hs b/src/Idris/REPLParser.hs --- a/src/Idris/REPLParser.hs +++ b/src/Idris/REPLParser.hs @@ -34,6 +34,7 @@ <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t)) <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t)) <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n)) + <|> try (do cmd ["total"]; do n <- pName; eof; return (TotCheck n)) <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t)) <|> try (do cmd ["u", "universes"]; eof; return Universes) <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n)) diff --git a/tutorial/examples/binary.idr b/tutorial/examples/binary.idr --- a/tutorial/examples/binary.idr +++ b/tutorial/examples/binary.idr @@ -41,21 +41,21 @@ natToBin_lemma_1 = proof { intro; intro; - rewrite plusn_Sm j j; + rewrite sym (plusSuccRightSucc j j); trivial; } parity_lemma_2 = proof { intro; intro; - rewrite plusn_Sm j j; + rewrite sym (plusSuccRightSucc j j); trivial; } parity_lemma_1 = proof { intro j; intro; - rewrite plusn_Sm j j; + rewrite sym (plusSuccRightSucc j j); trivial; } diff --git a/tutorial/examples/btree.idr b/tutorial/examples/btree.idr --- a/tutorial/examples/btree.idr +++ b/tutorial/examples/btree.idr @@ -10,7 +10,7 @@ toList : BTree a -> List a toList Leaf = [] -toList (Node l v r) = app (toList l) (v :: toList r) +toList (Node l v r) = toList l ++ (v :: toList r) toTree : Ord a => List a -> BTree a toTree [] = Leaf diff --git a/tutorial/examples/idiom.idr b/tutorial/examples/idiom.idr new file mode 100644 --- /dev/null +++ b/tutorial/examples/idiom.idr @@ -0,0 +1,38 @@ +module idiom + +data Expr = Var String + | Val Int + | Add Expr Expr + +data Eval : Set -> Set where + MkEval : (List (String, Int) -> Maybe a) -> Eval a + +fetch : String -> Eval Int +fetch x = MkEval (\e => fetchVal e) where + fetchVal : List (String, Int) -> Maybe Int + fetchVal [] = Nothing + fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs) + +instance Functor Eval where + fmap f (MkEval g) = MkEval (\e => fmap f (g e)) + +instance Applicative Eval where + pure x = MkEval (\e => Just x) + + (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where + app : Maybe (a -> b) -> Maybe a -> Maybe b + app (Just fx) (Just gx) = Just (fx gx) + app _ _ = Nothing + +eval : Expr -> Eval Int +eval (Var x) = fetch x +eval (Val x) = [| x |] +eval (Add x y) = [| eval x + eval y |] + +runEval : List (String, Int) -> Expr -> Maybe Int +runEval env e = case eval e of + MkEval envFn => envFn env + +m_add' : Maybe Int -> Maybe Int -> Maybe Int +m_add' x y = [| x + y |] + diff --git a/tutorial/examples/letbind.idr b/tutorial/examples/letbind.idr --- a/tutorial/examples/letbind.idr +++ b/tutorial/examples/letbind.idr @@ -1,8 +1,8 @@ module letbind mirror : List a -> List a -mirror xs = let xs' = rev xs in - app xs xs' +mirror xs = let xs' = reverse xs in + xs ++ xs' data Person = MkPerson String Int diff --git a/tutorial/examples/theorems.idr b/tutorial/examples/theorems.idr --- a/tutorial/examples/theorems.idr +++ b/tutorial/examples/theorems.idr @@ -5,16 +5,35 @@ twoPlusTwo : 2 + 2 = 4 twoPlusTwo = refl +total disjoint : (n : Nat) -> O = S n -> _|_ +disjoint n p = replace {P = disjointTy} p () + where + disjointTy : Nat -> Set + disjointTy O = () + disjointTy (S k) = _|_ + +total acyclic : (n : Nat) -> n = S n -> _|_ +acyclic O p = disjoint _ p +acyclic (S k) p = acyclic k (succInjective _ _ p) + +empty1 : _|_ +empty1 = hd [] where + hd : List a -> a + hd (x :: xs) = x + +empty2 : _|_ +empty2 = empty2 + plusReduces : (n:Nat) -> plus O n = n plusReduces n = refl plusReducesO : (n:Nat) -> n = plus n O plusReducesO O = refl -plusReducesO (S k) = eqRespS (plusReducesO k) +plusReducesO (S k) = cong (plusReducesO k) plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m) plusReducesS O m = refl -plusReducesS (S k) m = eqRespS (plusReducesS k m) +plusReducesS (S k) m = cong (plusReducesS k m) plusReducesO' : (n:Nat) -> n = plus n O plusReducesO' O = ?plusredO_O diff --git a/tutorial/examples/views.idr b/tutorial/examples/views.idr --- a/tutorial/examples/views.idr +++ b/tutorial/examples/views.idr @@ -23,14 +23,14 @@ views.parity_lemma_2 = proof { intro; intro; - rewrite plusn_Sm j j; + rewrite sym (plusSuccRightSucc j j); trivial; } views.parity_lemma_1 = proof { intro; intro; - rewrite plusn_Sm j j; + rewrite sym (plusSuccRightSucc j j); trivial; }