packages feed

idris 0.9.0 → 0.9.1

raw patch · 48 files changed

+3136/−704 lines, 48 filessetup-changed

Files

Setup.hs view
@@ -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 })
idris.cabal view
@@ -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
lib/Makefile view
@@ -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
lib/builtins.idr view
@@ -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  }
lib/checkall.idr view
@@ -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
+ lib/control/monad/identity.idr view
@@ -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
+ lib/control/monad/state.idr view
@@ -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+
lib/io.idr view
@@ -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)
lib/network/cgi.idr view
@@ -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
lib/prelude.idr view
@@ -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
+ lib/prelude/algebra.idr view
@@ -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
lib/prelude/either.idr view
@@ -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
lib/prelude/fin.idr view
@@ -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
lib/prelude/list.idr view
@@ -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;+}
lib/prelude/maybe.idr view
@@ -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-
lib/prelude/monad.idr view
@@ -3,6 +3,7 @@ -- Monads and Functors  import builtins+import prelude.list  %access public
lib/prelude/nat.idr view
@@ -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; }
lib/prelude/strings.idr view
@@ -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)))
lib/prelude/vect.idr view
@@ -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; }
lib/system.idr view
@@ -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
src/Core/CaseTree.hs view
@@ -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)
src/Core/CoreParser.hs view
@@ -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",
src/Core/Elaborate.hs view
@@ -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)
src/Core/Evaluate.hs view
@@ -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))
src/Core/ProofState.hs view
@@ -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
src/Core/TT.hs view
@@ -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:
src/Core/Typecheck.hs view
@@ -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
src/Core/Unify.hs view
@@ -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))
src/Idris/AbsSyntax.hs view
@@ -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)
src/Idris/Compiler.hs view
@@ -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
src/Idris/Coverage.hs view
@@ -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
+ src/Idris/DSL.hs view
@@ -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]+
src/Idris/Delaborate.hs view
@@ -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
src/Idris/ElabDecls.hs view
@@ -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
src/Idris/ElabTerm.hs view
@@ -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)
src/Idris/Error.hs view
@@ -56,6 +56,7 @@ getErrLine str    = case span (/=':') str of       (_, ':':rest) -> case span isDigit rest of+        ([], _) -> 0         (num, _) -> read num       _ -> 0
src/Idris/IBC.hs view
@@ -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"
src/Idris/Parser.hs view
@@ -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]
src/Idris/Primitives.hs view
@@ -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 }
src/Idris/Prover.hs view
@@ -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)
src/Idris/REPL.hs view
@@ -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 @@     ([""], "", ""),     (["<expr>"], "", "Evaluate an expression"),     ([":t"], "<expr>", "Check the type of an expression"),+    ([":total"], "<name>", "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)"),
src/Idris/REPLParser.hs view
@@ -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))
tutorial/examples/binary.idr view
@@ -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; }
tutorial/examples/btree.idr view
@@ -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
+ tutorial/examples/idiom.idr view
@@ -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 |]+
tutorial/examples/letbind.idr view
@@ -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
tutorial/examples/theorems.idr view
@@ -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
tutorial/examples/views.idr view
@@ -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; }