packages feed

idris 0.9.6.1 → 0.9.7

raw patch · 48 files changed

+1429/−188 lines, 48 filessetup-changed

Files

Setup.hs view
@@ -25,7 +25,8 @@ #endif  cleanStdLib verbosity-    = make verbosity [ "-C", "lib", "clean" ]+    = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ]+         make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ]  installStdLib pkg local verbosity copy     = do let dirs = L.absoluteInstallDirs pkg local copy@@ -37,6 +38,11 @@                , "TARGET=" ++ idir                , "IDRIS=" ++ icmd                ]+         make verbosity+               [ "-C", "effects", "install"+               , "TARGET=" ++ idir+               , "IDRIS=" ++ icmd+               ]          let idirRts = idir </> "rts"          putStrLn $ "Installing run time system in " ++ idirRts          make verbosity@@ -62,6 +68,10 @@          putStrLn $ "Building libraries..."          make verbosity                [ "-C", "lib", "check"+               , "IDRIS=" ++ icmd+               ]+         make verbosity+               [ "-C", "effects", "check"                , "IDRIS=" ++ icmd                ]          make verbosity
+ effects/Effect/Exception.idr view
@@ -0,0 +1,37 @@+module Effect.Exception++import Effects+import System+import Control.IOExcept++data Exception : Type -> Type -> Type -> Type -> Type where+     Raise : a -> Exception a () () b ++instance Handler (Exception a) Maybe where+     handle _ (Raise e) k = Nothing++instance Show a => Handler (Exception a) IO where+     handle _ (Raise e) k = do print e+                               believe_me (exit 1)++instance Handler (Exception a) (IOExcept a) where+     handle _ (Raise e) k = ioM (return (Left e))++EXCEPTION : Type -> EFF +EXCEPTION t = MkEff () (Exception t) ++raise : a -> Eff m [EXCEPTION a] b+raise err = Raise err++++++++-- TODO: Catching exceptions mid program?+-- probably need to invoke a new interpreter++-- possibly add a 'handle' to the Eff language so that an alternative+-- handler can be introduced mid interpretation?+
+ effects/Effect/File.idr view
@@ -0,0 +1,65 @@+module Effect.File++import Effects+import Control.IOExcept++data OpenFile : Mode -> Type where+     FH : File -> OpenFile m++data FileIO : Effect where+     Open  : String -> (m : Mode) -> FileIO () (OpenFile m) ()+     Close :                         FileIO (OpenFile m) () ()++     ReadLine  :           FileIO (OpenFile Read)  (OpenFile Read) String+     WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()+     EOF       :           FileIO (OpenFile Read)  (OpenFile Read) Bool++instance Handler FileIO IO where+    handle () (Open fname m) k = do h <- openFile fname m+                                    k (FH h) ()+    handle (FH h) Close      k = do closeFile h+                                    k () ()+    handle (FH h) ReadLine        k = do str <- fread h+                                         k (FH h) str+    handle (FH h) (WriteLine str) k = do fwrite h str+                                         k (FH h) ()+    handle (FH h) EOF             k = do e <- feof h+                                         k (FH h) e++instance Handler FileIO (IOExcept String) where+    handle () (Open fname m) k +       = do h <- ioe_lift (openFile fname m)+            valid <- ioe_lift (validFile h)+            if valid then k (FH h) ()+                     else ioe_fail "File open failed"+    handle (FH h) Close           k = do ioe_lift (closeFile h); k () ()+    handle (FH h) ReadLine        k = do str <- ioe_lift (fread h)+                                         k (FH h) str+    handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)+                                         k (FH h) ()+    handle (FH h) EOF             k = do e <- ioe_lift (feof h)+                                         k (FH h) e++FILE_IO : Type -> EFF+FILE_IO t = MkEff t FileIO ++open : Handler FileIO e =>+       String -> (m : Mode) -> EffM e [FILE_IO ()] [FILE_IO (OpenFile m)] ()+open f m = Open f m++close : Handler FileIO e =>+        EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()+close = Close++readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String+readLine = ReadLine++writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()+writeLine str = WriteLine str++eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool+eof = EOF++++
+ effects/Effect/Random.idr view
@@ -0,0 +1,21 @@+module Effect.Random++import Effects++data Random : Type -> Type -> Type -> Type where+     getRandom : Random Int Int Int++using (m : Type -> Type)+  instance Handler Random m where+     handle seed getRandom k+              = let seed' = 1664525 * seed + 1013904223 in+                    k seed' seed'+                    +RND : EFF+RND = MkEff Int Random++rndInt : Int -> Int -> Eff m [RND] Int+rndInt lower upper = do v <- getRandom +                        return (v `mod` (upper - lower) + lower)++
+ effects/Effect/Select.idr view
@@ -0,0 +1,23 @@+module Effect.Select++import Effects++data Selection : Effect where+     Select : List a -> Selection () () a++instance Handler Selection Maybe where+     handle _ (Select xs) k = tryAll xs where+         tryAll [] = Nothing+         tryAll (x :: xs) = case k () x of+                                 Nothing => tryAll xs+                                 Just v => Just v++instance Handler Selection List where+     handle r (Select xs) k = concatMap (k r) xs+     +SELECT : EFF+SELECT = MkEff () Selection++select : List a -> Eff m [SELECT] a+select xs = Select xs+
+ effects/Effect/State.idr view
@@ -0,0 +1,31 @@+module Effect.State++import Effects++%access public++data State : Effect where+     Get :      State a a a+     Put : b -> State a b ()++using (m : Type -> Type)+  instance Handler State m where+     handle st Get     k = k st st+     handle st (Put n) k = k n ()++STATE : Type -> EFF+STATE t = MkEff t State++get : Eff m [STATE x] x+get = Get ++put : x -> Eff m [STATE x] ()+put val = Put val++putM : y -> EffM m [STATE x] [STATE y] ()+putM val = Put val++update : (x -> x) -> Eff m [STATE x] ()+update f = do val <- get+              put (f val) +
+ effects/Effect/StdIO.idr view
@@ -0,0 +1,59 @@+module Effect.StdIO++import Effects+import Control.IOExcept++data StdIO : Effect where+     PutStr : String -> StdIO () () ()+     GetStr : StdIO () () String++instance Handler StdIO IO where+    handle () (PutStr s) k = do putStr s; k () ()+    handle () GetStr     k = do x <- getLine; k () x ++instance Handler StdIO (IOExcept a) where+    handle () (PutStr s) k = do ioe_lift (putStr s); k () ()+    handle () GetStr     k = do x <- ioe_lift getLine; k () x ++-- Handle effects in a pure way, for simulating IO for unit testing/proof++data IOStream a = MkStream (List String -> (a, List String))+  +injStream : a -> IOStream a+injStream v = MkStream (\x => (v, []))+  +instance Handler StdIO IOStream where+    handle () (PutStr s) k+       = MkStream (\x => case k () () of+                         MkStream f => let (res, str) = f x in+                                           (res, s :: str))+    handle {a} () GetStr k+       = MkStream (\x => case x of+                              [] => cont "" []+                              (t :: ts) => cont t ts)+        where+            cont : String -> List String -> (a, List String)+            cont t ts = case k () t of+                             MkStream f => f ts ++--- The Effect and associated functions++STDIO : EFF+STDIO = MkEff () StdIO++putStr : Handler StdIO e => String -> Eff e [STDIO] ()+putStr s = PutStr s++putStrLn : Handler StdIO e => String -> Eff e [STDIO] ()+putStrLn s = putStr (s ++ "\n")++getStr : Handler StdIO e => Eff e [STDIO] String+getStr = GetStr++mkStrFn : Env IOStream xs -> +          Eff IOStream xs a -> +          List String -> (a, List String)+mkStrFn {a} env p input = case mkStrFn' of+                               MkStream f => f input+  where mkStrFn' : IOStream a+        mkStrFn' = runWith injStream env p
+ effects/Effects.idr view
@@ -0,0 +1,207 @@+module Effects++import Language.Reflection+import Control.Catchable++%access public++---- Effects++Effect : Type+Effect = Type -> Type -> Type -> Type++data EFF : Type where+     MkEff : Type -> Effect -> EFF++class Handler (e : Effect) (m : Type -> Type) where+     handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a++---- Properties and proof construction++using (xs : List a, ys : List a)+  data SubList : List a -> List a -> Type where+       SubNil : SubList {a} [] []+       Keep   : SubList xs ys -> SubList (x :: xs) (x :: ys)+       Drop   : SubList xs ys -> SubList xs (x :: ys)++  subListId : SubList xs xs+  subListId {xs = Nil} = SubNil+  subListId {xs = x :: xs} = Keep subListId++data Env  : (m : Type -> Type) -> List EFF -> Type where+     Nil  : Env m Nil+     (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)++data EffElem : (Type -> Type -> Type -> Type) -> Type ->+               List EFF -> Type where+     Here : EffElem x a (MkEff a x :: xs)+     There : EffElem x a xs -> EffElem x a (y :: xs)++-- make an environment corresponding to a sub-list+dropEnv : Env m ys -> SubList xs ys -> Env m xs+dropEnv [] SubNil = []+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest++updateWith : (ys' : List a) -> (xs : List a) ->+             SubList ys xs -> List a+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest+updateWith ys        (x :: xs) (Drop rest) = x :: updateWith ys xs rest+updateWith []        []        SubNil      = []++-- put things back, replacing old with new in the sub-environment+rebuildEnv : Env m ys' -> (prf : SubList ys xs) -> +             Env m xs -> Env m (updateWith ys' xs prf) +rebuildEnv []        SubNil      env = env+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env+rebuildEnv xs        (Drop rest) (y :: env) = y :: rebuildEnv xs rest env++---- The Effect EDSL itself ----++-- some proof automation+findEffElem : Nat -> Tactic -- Nat is maximum search depth+findEffElem O = Refine "Here" `Seq` Solve +findEffElem (S n) = GoalType "EffElem" +          (Try (Refine "Here" `Seq` Solve)+               (Refine "There" `Seq` (Solve `Seq` findEffElem n)))++findSubList : Nat -> Tactic+findSubList O = Refine "SubNil" `Seq` Solve+findSubList (S n)+   = GoalType "SubList" +         (Try (Refine "subListId" `Seq` Solve)+         ((Try (Refine "Keep" `Seq` Solve)+               (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))++updateResTy : (xs : List EFF) -> EffElem e a xs -> e a b t -> +              List EFF+updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs+updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n++infix 5 :::, :-, :=++data LRes : lbl -> Type -> Type where+     (:=) : (x : lbl) -> res -> LRes x res++(:::) : lbl -> EFF -> EFF +(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff++private+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]+unlabel {m} {x = MkEff a eff} [l := v] = [v]++private+relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]+relabel {x = MkEff a eff} l [v] = [l := v]++-- the language of Effects++data EffM : (m : Type -> Type) ->+            List EFF -> List EFF -> Type -> Type where+     value   : a -> EffM m xs xs a+     ebind   : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b+     effect  : {a, b: _} -> {e : Effect} ->+               (prf : EffElem e a xs) -> +               (eff : e a b t) -> +               EffM m xs (updateResTy xs prf eff) t+     lift    : (prf : SubList ys xs) ->+               EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t+     new     : Handler e m =>+               res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->+               EffM m xs xs' a+     catch   : Catchable m err =>+               EffM m xs xs' a -> (err -> EffM m xs xs' a) ->+               EffM m xs xs' a+     (:-)    : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t++--   Eff : List (EFF m) -> Type -> Type++implicit+lift' : {default tactics { reflect findSubList 10; solve; }+           prf : SubList ys xs} ->+        EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t+lift' {prf} e = lift prf e++implicit+effect' : {a, b: _} -> {e : Effect} ->+          {default tactics { reflect findEffElem 10; solve; } +             prf : EffElem e a xs} -> +          (eff : e a b t) -> +         EffM m xs (updateResTy xs prf eff) t+effect' {prf} e = effect prf e+++-- for 'do' notation++return : a -> EffM m xs xs a+return x = value x++(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b+(>>=) = ebind++-- for idiom brackets++infixl 2 <$>++pure : a -> EffM m xs xs a+pure = value++(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b+(<$>) prog v = do fn <- prog+                  arg <- v+                  return (fn arg)++-- an interpreter++private+execEff : Env m xs -> (p : EffElem e res xs) -> +          (eff : e res b a) ->+          (Env m (updateResTy xs p eff) -> a -> m t) -> m t+execEff (val :: env) Here eff' k +    = handle val eff' (\res, v => k (res :: env) v)+execEff (val :: env) (There p) eff k +    = execEff env p eff (\env', v => k (val :: env') v)++eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b+eff env (value x) k = k env x+eff env (prog `ebind` c) k +   = eff env prog (\env', p' => eff env' (c p') k)+eff env (effect prf effP) k = execEff env prf effP k+eff env (lift prf effP) k +   = let env' = dropEnv env prf in +         eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')+eff env (new r prog) k+   = let env' = r :: env in +         eff env' prog (\(v :: envk), p' => k envk p')+eff env (catch prog handler) k+   = catch (eff env prog k)+           (\e => eff env (handler e) k)+eff {xs = [l ::: x]} env (l :- prog) k+   = let env' = unlabel {l} env in+         eff env' prog (\envk, p' => k (relabel l envk) p')++run : Applicative m => Env m xs -> EffM m xs xs' a -> m a+run env prog = eff env prog (\env, r => pure r)++runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)+runEnv env prog = eff env prog (\env, r => pure (env, r))++runPure : Env id xs -> EffM id xs xs' a -> a+runPure env prog = eff env prog (\env, r => r)++runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a+runWith inj env prog = eff env prog (\env, r => inj r)++Eff : (Type -> Type) -> List EFF -> Type -> Type+Eff m xs t = EffM m xs xs t++-- some higher order things++mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)+mapE f []        = pure [] +mapE f (x :: xs) = [| f x :: mapE f xs |]++when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()+when True  e = e+when False e = pure ()+
+ effects/Makefile view
@@ -0,0 +1,13 @@++check: .PHONY+	$(IDRIS) --build effects.ipkg++recheck: clean check++install: +	$(IDRIS) --install effects.ipkg++clean: .PHONY+	$(IDRIS) --clean effects.ipkg++.PHONY:
+ effects/effects.ipkg view
@@ -0,0 +1,6 @@+package effects++opts    = "-i ../lib"+modules = Effects, +          Effect.Exception, Effect.File, Effect.State,+          Effect.Random, Effect.StdIO, Effect.Select
idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.6.1+Version:        0.9.7 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -55,7 +55,10 @@                        lib/Control/Monad/*.idr lib/Language/*.idr                        lib/System/Concurrency/*.idr                        lib/Data/*.idr lib/Debug/*.idr+                       lib/Decidable/*.idr                        tutorial/examples/*.idr lib/base.ipkg+                       effects/Makefile effects/*.idr effects/Effect/*.idr+                       effects/effects.ipkg                        config.mk                        rts/*.c rts/*.h rts/Makefile                        js/*.js
lib/Builtins.idr view
@@ -75,6 +75,10 @@ cong : {f : t -> u} -> (a = b) -> f a = f b cong refl = refl +data Dec : Type -> Type where+    Yes : {A : Type} -> A          -> Dec A+    No  : {A : Type} -> (A -> _|_) -> Dec A+ data Bool = False | True  boolElim : Bool -> |(t : a) -> |(f : a) -> a @@ -82,10 +86,6 @@ boolElim False t e = e  data so : Bool -> Type where oh : so True--data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where-    Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y-    Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y  syntax if [test] then [t] else [e] = boolElim test t e syntax [test] "?" [t] ":" [e] = if test then t else e
lib/Control/Arrow.idr view
@@ -15,12 +15,12 @@   (***)  : arr a b -> arr a' b' -> arr (a, a') (b, b')   (&&&)  : arr a b -> arr a b' -> arr a (b, b') -instance Arrow Homomorphism where-  arrow  f              = Homo f-  first  (Homo f)       = Homo $ \(a, b) => (f a, b)-  second (Homo f)       = Homo $ \(a, b) => (a, f b)-  (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)-  (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)+instance Arrow Morphism where+  arrow  f            = Mor f+  first  (Mor f)      = Mor $ \(a, b) => (f a, b)+  second (Mor f)      = Mor $ \(a, b) => (a, f b)+  (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)+  (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)  instance Monad m => Arrow (Kleislimorphism m) where   arrow f = Kleisli (return . f)@@ -30,11 +30,11 @@   second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b                                                return (a, x) -  (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a +  (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a                                                         y <- g b                                                         return (x, y) -  (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a +  (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a                                                    y <- g a                                                    return (x, y)
+ lib/Control/Catchable.idr view
@@ -0,0 +1,35 @@+module Prelude.Catchable++import Prelude.List+import Prelude.Maybe+import Prelude.Either+import Control.IOExcept++class Catchable (m : Type -> Type) t where+    throw : t -> m a+    catch : m a -> (t -> m a) -> m a++instance Catchable Maybe () where+    catch Nothing  h = h ()+    catch (Just x) h = Just x++    throw () = Nothing++instance Catchable (Either a) a where+    catch (Left err) h = h err+    catch (Right x)  h = (Right x)++    throw x = Left x++instance Catchable (IOExcept err) err where+    catch (ioM prog) h = ioM (do p' <- prog+                                 case p' of+                                      Left e => let ioM he = h e in he+                                      Right val => return (Right val))+    throw x = ioM (return (Left x))++instance Catchable List () where+    catch [] h = h ()+    catch xs h = xs++    throw () = []
lib/Control/Category.idr view
@@ -8,9 +8,9 @@   id  : cat a a   (.) : cat b c -> cat a b -> cat a c -instance Category Homomorphism where-  id                  = Homo Builtins.id-  (Homo f) . (Homo g) = Homo (f . g)+instance Category Morphism where+  id                = Mor Builtins.id+  (Mor f) . (Mor g) = Mor (f . g)  instance Monad m => Category (Kleislimorphism m) where   id                        = Kleisli (return . id)
+ lib/Control/IOExcept.idr view
@@ -0,0 +1,38 @@+module Control.IOExcept++import Prelude++-- An IO monad with exception handling++data IOExcept : Type -> Type -> Type where+     ioM : IO (Either err a) -> IOExcept err a++instance Functor (IOExcept e) where+     fmap f (ioM fn) = ioM (fmap (fmap f) fn)++instance Applicative (IOExcept e) where+     pure x = ioM (pure (pure x))+     (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a+                                   return (f' <$> a'))++instance Monad (IOExcept e) where+     return = pure+     (ioM x) >>= k = ioM (do x' <- x;+                             case x' of+                                  Right a => let (ioM ka) = k a in+                                                 ka+                                  Left err => return (Left err))++ioe_lift : IO a -> IOExcept err a+ioe_lift op = ioM (do op' <- op+                      return (Right op'))++ioe_fail : err -> IOExcept err a+ioe_fail e = ioM (return (Left e))++ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b+ioe_run (ioM act) err ok = do act' <- act+                              case act' of+                                   Left e => err e+                                   Right v => ok v+
lib/Data/Morphisms.idr view
@@ -4,8 +4,8 @@  %access public -data Homomorphism : Type -> Type -> Type where-  Homo : (a -> b) -> Homomorphism a b+data Morphism : Type -> Type -> Type where+  Mor : (a -> b) -> Morphism a b  data Endomorphism : Type -> Type where   Endo : (a -> a) -> Endomorphism a@@ -16,22 +16,22 @@ applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b applyKleisli (Kleisli f) a = f a -applyHomo : Homomorphism a b -> a -> b-applyHomo (Homo f) a = f a+applyMor : Morphism a b -> a -> b+applyMor (Mor f) a = f a  applyEndo : Endomorphism a -> a -> a applyEndo (Endo f) a = f a -instance Functor (Homomorphism r) where-  fmap f (Homo a) = Homo (f . a)+instance Functor (Morphism r) where+  fmap f (Mor a) = Mor (f . a) -instance Applicative (Homomorphism r) where-  pure a                = Homo $ const a-  (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r+instance Applicative (Morphism r) where+  pure a                = Mor $ const a+  (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r -instance Monad (Homomorphism r) where-  return a       = Homo $ const a-  (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r+instance Monad (Morphism r) where+  return a       = Mor $ const a+  (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r  instance Semigroup (Endomorphism a) where   (Endo f) <+> (Endo g) = Endo $ g . f@@ -42,4 +42,4 @@ infixr 1 ~>  (~>) : Type -> Type -> Type-a ~> b = Homomorphism a b+a ~> b = Morphism a b
+ lib/Data/Sign.idr view
@@ -0,0 +1,6 @@+module Data.Sign++data Sign = Plus | Minus++class Signed t where+  total sign : t -> Sign
+ lib/Data/Z.idr view
@@ -0,0 +1,144 @@+module Data.Z++import Decidable.Equality+import Data.Sign++%default total+%access public+++-- | An integer is either a positive nat or the negated successor of a nat.+-- Zero is chosen to be positive.+data Z = Pos Nat | NegS Nat++instance Signed Z where+  sign (Pos _) = Plus+  sign (NegS _) = Minus++absZ : Z -> Nat+absZ (Pos n) = n+absZ (NegS n) = S n++instance Show Z where+  show (Pos n) = show n+  show (NegS n) = "-" ++ show (S n)++negZ : Z -> Z+negZ (Pos O) = Pos O+negZ (Pos (S n)) = NegS n+negZ (NegS n) = Pos (S n)++negNat : Nat -> Z+negNat O = Pos O+negNat (S n) = NegS n++minusNatZ : Nat -> Nat -> Z+minusNatZ n O = Pos n+minusNatZ O (S m) = NegS m+minusNatZ (S n) (S m) = minusNatZ n m++plusZ : Z -> Z -> Z+plusZ (Pos n) (Pos m) = Pos (n + m)+plusZ (NegS n) (NegS m) = NegS (S (n + m))+plusZ (Pos n) (NegS m) = minusNatZ n (S m)+plusZ (NegS n) (Pos m) = minusNatZ m (S n)++subZ : Z -> Z -> Z+subZ n m = plusZ n (negZ m)++instance Eq Z where+  (Pos n) == (Pos m) = n == m+  (NegS n) == (NegS m) = n == m+  _ == _ = False+++instance Ord Z where+  compare (Pos n) (Pos m) = compare n m+  compare (NegS n) (NegS m) = compare m n+  compare (Pos _) (NegS _) = GT+  compare (NegS _) (Pos _) = LT+++multZ : Z -> Z -> Z+multZ (Pos n) (Pos m) = Pos $ n * m+multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)+multZ (NegS n) (Pos m) = negNat $ (S n) * m+multZ (Pos n) (NegS m) = negNat $ n * (S m)++fromInt : Int -> Z+fromInt n = if n < 0+            then NegS $ fromInteger {a=Nat} (-n - 1)+            else Pos $ fromInteger {a=Nat} n++instance Cast Nat Z where+  cast n = Pos n++instance Num Z where+  (+) = plusZ+  (-) = subZ+  (*) = multZ+  abs = cast . absZ+  fromInteger = fromInt++instance Cast Z Int where+  cast (Pos n) = cast n+  cast (NegS n) = (-1) * (cast n + 1)++instance Cast Int Z where+  cast = fromInteger+++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)+             -> n + m = x -> (Pos n) + (Pos m) = Pos x+natPlusZPlus n m x h = cong h++natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)+             -> n * m = x -> (Pos n) * (Pos m) = Pos x+natMultZMult n m x h = cong h++doubleNegElim : (z : Z) -> negZ (negZ z) = z+doubleNegElim (Pos O) = refl+doubleNegElim (Pos (S n)) = refl+doubleNegElim (NegS O) = refl+doubleNegElim (NegS (S n)) = refl++-- Injectivity+posInjective : Pos n = Pos m -> n = m+posInjective refl = refl++negSInjective : NegS n = NegS m -> n = m+negSInjective refl = refl++posNotNeg : Pos n = NegS m -> _|_+posNotNeg refl impossible++-- Decidable equality+instance DecEq Z where+  decEq (Pos n) (NegS m) = No posNotNeg+  decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg+  decEq (Pos n) (Pos m) with (decEq n m)+    | Yes p = Yes $ cong p+    | No p = No $ \h => p $ posInjective h+  decEq (NegS n) (NegS m) with (decEq n m)+    | Yes p = Yes $ cong p+    | No p = No $ \h => p $ negSInjective h++-- Plus+plusZeroLeftNeutralZ : (right : Z) -> 0 + right = right+plusZeroLeftNeutralZ (Pos n) = refl+plusZeroLeftNeutralZ (NegS n) = refl++plusZeroRightNeutralZ : (left : Z) -> left + 0 = left+plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n+plusZeroRightNeutralZ (NegS n) = refl++plusCommutativeZ : (left : Z) -> (right : Z) -> (left + right = right + left)+plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m+plusCommutativeZ (Pos n) (NegS m) = refl+plusCommutativeZ (NegS n) (Pos m) = refl+plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m+
+ lib/Decidable/Equality.idr view
@@ -0,0 +1,102 @@+module Decidable.Equality++import Builtins++--------------------------------------------------------------------------------+-- Utility lemmas+--------------------------------------------------------------------------------++total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)+negEqSym p h = p (sym h)+++--------------------------------------------------------------------------------+-- Decidable equality+--------------------------------------------------------------------------------++class DecEq t where+  total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)++--------------------------------------------------------------------------------+--- Unit+--------------------------------------------------------------------------------++instance DecEq () where+  decEq () () = Yes refl++--------------------------------------------------------------------------------+-- Booleans+--------------------------------------------------------------------------------++total trueNotFalse : True = False -> _|_+trueNotFalse refl impossible++instance DecEq Bool where+  decEq True  True  = Yes refl+  decEq False False = Yes refl+  decEq True  False = No trueNotFalse+  decEq False True  = No (negEqSym trueNotFalse)++--------------------------------------------------------------------------------+-- Nat+--------------------------------------------------------------------------------++total OnotS : O = S n -> _|_+OnotS refl impossible++instance DecEq Nat where+  decEq O     O     = Yes refl+  decEq O     (S _) = No OnotS+  decEq (S _) O     = No (negEqSym OnotS)+  decEq (S n) (S m) with (decEq n m)+    | Yes p = Yes $ cong p+    | No p = No $ \h : (S n = S m) => p $ succInjective n m h++--------------------------------------------------------------------------------+-- Maybe+--------------------------------------------------------------------------------++total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_+nothingNotJust refl impossible++instance (DecEq t) => DecEq (Maybe t) where+  decEq Nothing Nothing = Yes refl+  decEq (Just x') (Just y') with (decEq x' y')+    | Yes p = Yes $ cong p+    | No p = No $ \h : Just x' = Just y' => p $ justInjective h+  decEq Nothing (Just _) = No nothingNotJust+  decEq (Just _) Nothing = No (negEqSym nothingNotJust)++--------------------------------------------------------------------------------+-- Either+--------------------------------------------------------------------------------++total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_+leftNotRight refl impossible++instance (DecEq a, DecEq b) => DecEq (Either a b) where+  decEq {b=b} (Left x') (Left y') with (decEq x' y')+    | Yes p = Yes $ cong p+    | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h+  decEq (Right x') (Right y') with (decEq x' y')+    | Yes p = Yes $ cong p+    | No p = No $ \h : Right x' = Right y' => p $ rightInjective {a = a} h+  decEq (Left x') (Right y') = No leftNotRight+  decEq (Right x') (Left y') = No $ negEqSym leftNotRight++--------------------------------------------------------------------------------+-- Fin+--------------------------------------------------------------------------------++total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_+fONotfS refl impossible++instance DecEq (Fin n) where+  decEq fO fO = Yes refl+  decEq fO (fS f) = No fONotfS+  decEq (fS f) fO = No $ negEqSym fONotfS+  decEq (fS f) (fS f') with (decEq f f')+    | Yes p = Yes $ cong p+    | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h++
+ lib/Effects.idr view
@@ -0,0 +1,228 @@+module Effects++import Prelude+import Prelude.Catchable++import Language.Reflection+import Control.Monad.Identity+import Effective++----------- Effects ------------++Effect : Type+Effect = Type -> Type -> Type -> Type++data EFF : Type where+     MkEff : Type -> Effect -> EFF++class Effective (e : Effect) (m : Type -> Type) where+     runEffect : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a++class Catchable (m : Type -> Type) t where+    throw : t -> m a+    catch : m a -> (t -> m a) -> m a++++++++++++++---------------------++using (xs : Vect a m, ys : Vect a n)+  data SubList : Vect a m -> Vect a n -> Type where+       SubNil : SubList {a} [] []+       Keep   : SubList xs ys -> SubList (x :: xs) (x :: ys)+       Drop   : SubList xs ys -> SubList xs (x :: ys)++  subListId : SubList xs xs+  subListId {xs = Nil} = SubNil+  subListId {xs = x :: xs} = Keep subListId++effType : EFF -> Type+effType (MkEff t _) = t++using (m : Type -> Type, +       xs : Vect EFF n, xs' : Vect EFF n, xs'' : Vect EFF n,+       ys : Vect EFF p)++  data Env  : (m : Type -> Type) -> Vect EFF n -> Type where+       Nil  : Env m Nil+       (::) : Effective eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)++  data EffElem : (Type -> Type -> Type -> Type) -> Type ->+                 Vect EFF n -> Type where+       Here : EffElem x a (MkEff a x :: xs)+       There : EffElem x a xs -> EffElem x a (y :: xs)++  -- make an environment corresponding to a sub-list+  dropEnv : Env m ys -> SubList xs ys -> Env m xs+  dropEnv [] SubNil = []+  dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest+  dropEnv (v :: vs) (Drop rest) = dropEnv vs rest++  updateWith : {ys : Vect a p} ->+               (ys' : Vect a p) -> (xs : Vect a n) ->+               SubList ys xs -> Vect a n+  updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest+  updateWith ys        (x :: xs) (Drop rest) = x :: updateWith ys xs rest+  updateWith []        []        SubNil      = []++  -- put things back, replacing old with new in the sub-environment+  rebuildEnv : {ys' : Vect _ p} ->+               Env m ys' -> (prf : SubList ys xs) -> +               Env m xs -> Env m (updateWith ys' xs prf) +  rebuildEnv []        SubNil      env = env+  rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env+  rebuildEnv xs        (Drop rest) (y :: env) = y :: rebuildEnv xs rest env++---- The Effect EDSL itself ----++using (m : Type -> Type, +       xs : Vect EFF n, xs' : Vect EFF n, xs'' : Vect EFF n,+       ys : Vect EFF p, ys' : Vect EFF p)++  -- some proof automation+  findEffElem : Nat -> Tactic -- Nat is maximum search depth+  findEffElem O = Refine "Here" `Seq` Solve +  findEffElem (S n) = GoalType "EffElem" +            (Try (Refine "Here" `Seq` Solve)+                 (Refine "There" `Seq` (Solve `Seq` findEffElem n)))+ +  findSubList : Nat -> Tactic+  findSubList O = Refine "SubNil" `Seq` Solve+  findSubList (S n)+     = GoalType "SubList" +           (Try (Refine "subListId" `Seq` Solve)+           ((Try (Refine "Keep" `Seq` Solve)+                 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))++  updateResTy : (xs : Vect EFF n) -> EffElem e a xs -> e a b t -> +                Vect EFF n+  updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs+  updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n++  infix 5 :::, :-, :=++  data LRes : lbl -> Type -> Type where+       (:=) : (x : lbl) -> res -> LRes x res++  (:::) : lbl -> EFF -> EFF +  (:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff++  unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]+  unlabel {m} {x = MkEff a eff} [l := v] = [v]++  relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]+  relabel {x = MkEff a eff} l [v] = [l := v]++  -- the language of Effects++  data EffM : (m : Type -> Type) ->+              Vect EFF n -> Vect EFF n -> Type -> Type where+       value  : a -> EffM m xs xs a+       ebind  : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b+       effect : {a, b: _} -> {e : Effect} ->+                {default tactics { reflect findEffElem 10; solve; } +                  prf : EffElem e a xs} -> +                (eff : e a b t) -> +                EffM m xs (updateResTy xs prf eff) t+       lift'  : (prf : SubList ys xs) ->+                EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t+       new    : Effective e m =>+                res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->+                EffM m xs xs' a+       catch  : Catchable m err =>+                EffM m xs xs' a -> (err -> EffM m xs xs' a) ->+                EffM m xs xs' a+       (:-)   : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t++--   Eff : List (EFF m) -> Type -> Type++  implicit+  lift : {default tactics { reflect findSubList 10; solve; }+             prf : SubList ys xs} ->+         EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t+  lift {prf} e = lift' prf e++  -- for 'do' notation++  return : a -> EffM m xs xs a+  return x = value x++  (>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b+  (>>=) = ebind++  -- for idiom brackets++  infixl 2 <$>++  pure : Monad m => a -> EffM m xs xs a+  pure = value++  (<$>) : Monad m => EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b+  (<$>) prog v = do fn <- prog+                    arg <- v+                    return (fn arg)++  -- an interpreter++  execEff : Monad m => Env m xs -> (p : EffElem e res xs) -> +                       (eff : e res b a) ->+                       (Env m (updateResTy xs p eff) -> a -> m t) -> m t+  execEff (val :: env) Here eff' k +      = runEffect val eff' (\res, v => k (res :: env) v)+  execEff (val :: env) (There p) eff k +      = execEff env p eff (\env', v => k (val :: env') v)++  eff : Monad m => +        Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b+  eff env (value x) k = k env x+  eff env (prog `ebind` c) k +     = eff env prog (\env', p' => eff env' (c p') k)+  eff env (effect {prf} effP) k = execEff env prf effP k+  eff env (lift' prf effP) k +     = let env' = dropEnv env prf in +           eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')+  eff env (new r prog) k+     = let env' = r :: env in +           eff env' prog (\(v :: envk), p' => k envk p')+  eff env (catch prog handler) k+     = Effective.catch (eff env prog k)+                       (\e => eff env (handler e) k)+  eff {xs = [l ::: x]} env (l :- prog) k+     = let env' = unlabel {l} env in+           eff env' prog (\envk, p' => k (relabel l envk) p')++  run : Monad m => Env m xs -> EffM m xs xs' a -> m a+  run env prog = eff env prog (\env, r => return r)++  runEnv : Monad m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)+  runEnv env prog = eff env prog (\env, r => return (env, r))++  runPure : Env Identity xs -> EffM Identity xs xs' a -> a+  runPure env prog = case eff env prog (\env, r => return r) of+                          Id v => v++syntax Eff [xs] [a] = Monad m => EffM m xs xs a +syntax EffT [m] [xs] [t] = EffM m xs xs t++-- some higher order things++mapE : Monad m => {xs : Vect EFF n} -> +       (a -> EffM m xs xs b) -> List a -> EffM m xs xs (List b)+mapE f []        = pure [] +mapE f (x :: xs) = [| f x :: mapE f xs |]++when : Monad m => {xs : Vect EFF n} ->+       Bool -> EffM m xs xs () -> EffM m xs xs ()+when True  e = e+when False e = return ()+
lib/Prelude.idr view
@@ -216,6 +216,12 @@ prod : Num a => List a -> a prod = foldl (*) 1 +curry : ((a, b) -> c) -> a -> b -> c+curry f a b = f (a, b)++uncurry : (a -> b -> c) -> (a, b) -> c+uncurry f (a, b) = f a b+ ---- some basic io  partial
lib/Prelude/Either.idr view
@@ -61,3 +61,16 @@ maybeToEither : e -> Maybe a -> Either e a maybeToEither def (Just j) = Right j maybeToEither def Nothing  = Left  def+++--------------------------------------------------------------------------------+-- Injectivity of constructors+--------------------------------------------------------------------------------++total leftInjective : {b : Type} -> {x : a} -> {y : a}+                    -> (Left {b = b} x = Left {b = b} y) -> (x = y)+leftInjective refl = refl++total rightInjective : {a : Type} -> {x : b} -> {y : b}+                     -> (Right {a = a} x = Right {a = a} y) -> (x = y)+rightInjective refl = refl
lib/Prelude/Fin.idr view
@@ -40,3 +40,6 @@ last : Fin (S n) last {n=O} = fO last {n=S _} = fS last++total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'+fSinjective refl = refl
lib/Prelude/Maybe.idr view
@@ -39,6 +39,16 @@ toMaybe True  j = Just j toMaybe False j = Nothing +justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y+justInjective refl = refl++lowerMaybe : Monoid a => Maybe a -> a+lowerMaybe Nothing = neutral+lowerMaybe (Just x) = x++raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a+raiseToMaybe x = if x == neutral then Nothing else Just x+ -------------------------------------------------------------------------------- -- Class instances --------------------------------------------------------------------------------@@ -47,23 +57,27 @@ maybe_bind Nothing  k = Nothing maybe_bind (Just x) k = k x +instance (Eq a) => Eq (Maybe a) where+  Nothing  == Nothing  = True+  Nothing  == (Just _) = False+  (Just _) == Nothing  = False+  (Just a) == (Just b) = a == b+ -- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to--- <http://en.wikipedia.org/wiki/Monoid>: \"Any semigroup S may be--- turned into a monoid simply by adjoining an element e not in S--- and defining i+i = i and i+s = s = s+i for all s ∈ S.\"+-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be+-- turned into a monoid simply by adjoining an element i not in S+-- and defining i+i = i and i+s = s = s+i for all s ∈ S."  instance (Semigroup a) => Semigroup (Maybe a) where   Nothing <+> m = m   m <+> Nothing = m   (Just m1) <+> (Just m2) = Just (m1 <+> m2) -instance (Monoid a) => Monoid (Maybe a) where+instance (Semigroup a) => Monoid (Maybe a) where   neutral = Nothing - instance (Monoid a, Eq a) => Cast a (Maybe a) where-  cast x = if x == neutral then Nothing else Just x+  cast = raiseToMaybe  instance (Monoid a) => Cast (Maybe a) a where-  cast Nothing = neutral-  cast (Just x) = x+  cast = lowerMaybe
lib/Prelude/Vect.idr view
@@ -36,6 +36,11 @@ index (fS k) (x::xs) = index k xs index fO     [] impossible +deleteAt : Fin (S n) -> Vect a (S n) -> Vect a n+deleteAt           fO     (x::xs) = xs+deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs+deleteAt           _      [] impossible+ -------------------------------------------------------------------------------- -- Subvectors --------------------------------------------------------------------------------@@ -79,9 +84,12 @@ -- Zips and unzips -------------------------------------------------------------------------------- +zipWith : (a -> b -> c) -> Vect a n -> Vect b n -> Vect c n+zipWith f []      []      = []+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys+ zip : Vect a n -> Vect b n -> Vect (a, b) n-zip []        []        = []-zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)+zip = zipWith (\x => \y => (x,y))  unzip : Vect (a, b) n -> (Vect a n, Vect b n) unzip []           = ([], [])@@ -121,6 +129,10 @@ -------------------------------------------------------------------------------- -- Special folds --------------------------------------------------------------------------------++concat : Vect (Vect a n) m -> Vect a (m * n)+concat []      = []+concat (v::vs) = v ++ concat vs  total and : Vect Bool m -> Bool and = foldr (&&) True
lib/base.ipkg view
@@ -6,16 +6,19 @@           Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,           Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,           Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, -          Prelude.Heap, Prelude.Complex, Prelude.Functor,+          Prelude.Heap, Prelude.Complex, Prelude.Functor,             Network.Cgi,           Debug.Trace,            System.Concurrency.Raw, System.Concurrency.Process, +          Decidable.Equality,+           Language.Reflection, -          Data.Morphisms, Data.Bits, Data.Mod2,+          Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,            Control.Monad.Identity, Control.Monad.State, Control.Category,-          Control.Arrow+          Control.Arrow,+          Control.Catchable, Control.IOExcept
rts/idris_gmp.c view
@@ -231,7 +231,7 @@     if (ISINT(x) && ISINT(y)) {         return MKINT((i_int)(GETINT(x) == GETINT(y)));     } else {-        return bigEq(vm, x, y);+        return bigEq(vm, GETBIG(vm, x), GETBIG(vm, y));     } } @@ -239,7 +239,7 @@     if (ISINT(x) && ISINT(y)) {         return MKINT((i_int)(GETINT(x) < GETINT(y)));     } else {-        return bigLt(vm, x, y);+        return bigLt(vm, GETBIG(vm, x), GETBIG(vm, y));     } } @@ -247,7 +247,7 @@     if (ISINT(x) && ISINT(y)) {         return MKINT((i_int)(GETINT(x) <= GETINT(y)));     } else {-        return bigLe(vm, x, y);+        return bigLe(vm, GETBIG(vm, x), GETBIG(vm, y));     } } @@ -255,7 +255,7 @@     if (ISINT(x) && ISINT(y)) {         return MKINT((i_int)(GETINT(x) > GETINT(y)));     } else {-        return bigGt(vm, x, y);+        return bigGt(vm, GETBIG(vm, x), GETBIG(vm, y));     } } @@ -263,7 +263,7 @@     if (ISINT(x) && ISINT(y)) {         return MKINT((i_int)(GETINT(x) >= GETINT(y)));     } else {-        return bigGe(vm, x, y);+        return bigGe(vm, GETBIG(vm, x), GETBIG(vm, y));     } }
rts/idris_rts.c view
@@ -77,6 +77,24 @@     free(vm); } +void idris_requireAlloc(VM* vm, size_t size) {+    if (!(vm -> heap_next + size < vm -> heap_end)) {+        idris_gc(vm);+    }++    int lock = vm->processes > 0;+    if (lock) { // not message passing+       pthread_mutex_lock(&vm->alloc_lock); +    }+}++void idris_doneAlloc(VM* vm) {+    int lock = vm->processes > 0;+    if (lock) { // not message passing+       pthread_mutex_unlock(&vm->alloc_lock); +    }+}+ void* allocate(VM* vm, size_t size, int outerlock) { //    return malloc(size);     int lock = vm->processes > 0 && !outerlock;
rts/idris_rts.h view
@@ -168,6 +168,15 @@ void* allocate(VM* vm, size_t size, int outerlock); // void* allocCon(VM* vm, int arity, int outerlock); +// When allocating from C, call 'idris_requireAlloc' with a size to+// guarantee that no garbage collection will happen (and hence nothing+// will move) until at least size bytes have been allocated.+// idris_doneAlloc *must* be called when allocation from C is done (as it+// may take a lock if other threads are running).++void idris_requireAlloc(VM* vm, size_t size);+void idris_doneAlloc(VM* vm);+ #define allocCon(cl, vm, t, a, o) \   cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*a, o); \   SETTY(cl, CON); \@@ -221,6 +230,25 @@ // Just reports an error and exits.  void stackOverflow();++// Some FFI help (functions and macros below are all which C code should+// use)++// When allocating from C, call 'idris_requireAlloc' with a size to+// guarantee that no garbage collection will happen (and hence nothing+// will move) until at least size bytes have been allocated.+// idris_doneAlloc *must* be called when allocation from C is done (as it+// may take a lock if other threads are running).++void idris_requireAlloc(VM* vm, size_t size);+void idris_doneAlloc(VM* vm);++// I think these names are nicer for an API...++#define idris_constructor allocCon+#define idris_setConArg SETARG+#define idris_getConArg GETARG+#define idris_mkInt(x) MKINT((intptr_t)(x))  #include "idris_gmp.h"
rts/libidris_rts.a view

binary file changed (50408 → 52032 bytes)

src/Core/CaseTree.hs view
@@ -418,8 +418,8 @@     applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)     applyMaps ms t = t -prune :: Bool -> -- ^ Convert single branches to projections (only useful at runtime)-         SC -> SC+prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)+      -> SC -> SC prune proj (Case n alts)      = let alts' = filter notErased (map pruneAlt alts) in           case alts' of
src/Core/Constraints.hs view
@@ -1,3 +1,4 @@+-- | Check universe constraints. module Core.Constraints(ucheck) where  import Core.TT@@ -13,6 +14,7 @@  import Debug.Trace +-- | Check that a list of universe constraints can be satisfied. ucheck :: [(UConstraint, FC)] -> TC () ucheck cs = acyclic rels (map fst (M.toList rels))   where lhs (ULT l _) = l
src/Core/CoreParser.hs view
@@ -34,7 +34,7 @@                     "infix", "infixl", "infixr",                      "where", "with", "syntax", "proof", "postulate",                     "using", "namespace", "class", "instance",-                    "public", "private", "abstract", +                    "public", "private", "abstract", "implicit",                     "Int", "Integer", "Float", "Char", "String", "Ptr",                     "Bits8", "Bits16", "Bits32", "Bits64"]            }
src/Core/Elaborate.hs view
@@ -40,6 +40,15 @@ proof :: ElabState aux -> ProofState proof (ES (p, _) _ _) = p +-- Insert a 'proofSearchFail' error if necessary to shortcut any further+-- fruitless searching+proofFail :: Elab' aux a -> Elab' aux a+proofFail e = do s <- get+                 case runStateT e s of+                      OK (a, s') -> do put s'+                                       return a+                      Error err -> lift $ Error (ProofSearchFail err)+ saveState :: Elab' aux () saveState = do e@(ES p s _) <- get                put (ES p s (Just e))@@ -55,6 +64,8 @@                  case runStateT elab s of                     OK (a, s')     -> do put s'                                          return a+                    Error (ProofSearchFail (At f e))+                                   -> lift $ Error (ProofSearchFail (At f e))                     Error (At f e) -> lift $ Error (At f e)                     Error e        -> lift $ Error (At f e) @@ -368,7 +379,7 @@ apply fn imps =      do args <- prepare_apply fn (map fst imps)        fill (raw_apply fn (map Var args))-       -- *Don't* solve the arguments we're specifying by hand.+       -- _Don't_ solve the arguments we're specifying by hand.        -- (remove from unified list before calling end_unify)        -- HMMM: Actually, if we get it wrong, the typechecker will complain!        -- so do nothing@@ -508,14 +519,17 @@                case prunStateT ps t1 s of                     OK (v, s') -> do put s'                                      return v-                    Error e1 -> if proofSearch || recoverableErr e1 then+                    Error e1 -> if recoverableErr e1 then                                    do case runStateT t2 s of                                          OK (v, s') -> do put s'; return v                                          Error e2 -> if score e1 >= score e2                                                          then lift (tfail e1)                                                          else lift (tfail e2)                                    else lift (tfail e1)-  where recoverableErr (CantUnify r _ _ _ _ _) = r+  where recoverableErr err@(CantUnify r _ _ _ _ _) +             = -- traceWhen r (show err) $+               r || proofSearch+        recoverableErr (ProofSearchFail _) = False         recoverableErr _ = True  tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
src/Core/Evaluate.hs view
@@ -29,7 +29,7 @@ initEval = ES []  -- VALUES (as HOAS) ----------------------------------------------------------+-- | A HOAS representation of values data Value = VP NameType Name Value            | VV Int            | VBind Name (Binder Value) (Value -> Eval Value)@@ -62,7 +62,7 @@ -- i.e. it's an intermediate environment that we have while type checking or -- while building a proof. --- Normalise fully type checked terms (so, assume all names/let bindings resolved)+-- | Normalise fully type checked terms (so, assume all names/let bindings resolved) normaliseC :: Context -> Env -> TT Name -> TT Name normaliseC ctxt env t     = evalState (do val <- eval False ctxt [] env t []@@ -86,9 +86,8 @@    = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []                    quote 0 val) (initEval { limited = limits }) --- Like normalise, but we only reduce functions that are marked as okay to +-- | Like normalise, but we only reduce functions that are marked as okay to  -- inline (and probably shouldn't reduce lets?)- simplify :: Context -> Bool -> Env -> TT Name -> TT Name simplify ctxt runtime env t     = evalState (do val <- eval False ctxt [(UN "lazy", 0),@@ -98,6 +97,7 @@                                  [Simplify runtime]                    quote 0 val) initEval +-- | Reduce a term to head normal form hnf :: Context -> Env -> TT Name -> TT Name hnf ctxt env t     = evalState (do val <- eval False ctxt [] @@ -130,9 +130,8 @@                   _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)                             else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns) --- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,+-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed, -- such as we might have during construction of a proof)- eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->          [EvalOpt] -> Eval Value eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where@@ -576,7 +575,7 @@  -- CONTEXTS ----------------------------------------------------------------- -{- A definition is either a simple function (just an expression with a type),+{-| A definition is either a simple function (just an expression with a type),    a constant, which could be a data or type constructor, an axiom or as an    yet undefined function, or an Operator.    An Operator is a function which explains how to reduce. @@ -620,12 +619,14 @@ data Accessibility = Public | Frozen | Hidden     deriving (Show, Eq) -data Totality = Total [Int] -- well-founded arguments-              | Productive+-- | The result of totality checking+data Totality = Total [Int] -- ^ well-founded arguments+              | Productive -- ^ productive               | Partial PReason               | Unchecked     deriving Eq +-- | Reasons why a function may not be total data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name              | BelieveMe | Mutual [Name] | NotProductive     deriving (Show, Eq)@@ -655,14 +656,18 @@ deriving instance Binary PReason !-} +-- | Contexts used for global definitions and for proof state. They contain+-- universe constraints and existing definitions. data Context = MkContext {                    uconstraints :: [UConstraint],                   next_tvar    :: Int,                   definitions  :: Ctxt (Def, Accessibility, Totality)                  } +-- | The initial empty context initContext = MkContext [] 0 emptyContext +-- | Get the definitions from a context ctxtAlist :: Context -> [(Name, Def)] ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
src/Core/ProofState.hs view
@@ -508,6 +508,7 @@ compute :: RunTactic compute ctxt env (Bind x (Hole ty) sc) =     do return $ Bind x (Hole (normalise ctxt env ty)) sc+compute ctxt env t = return t          hnf_compute :: RunTactic hnf_compute ctxt env (Bind x (Hole ty) sc) =
src/Core/TT.hs view
@@ -1,5 +1,23 @@ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-} +{-| TT is the core language of Idris. The language has:++   * Full dependent types++   * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...++   * Pattern matching letrec binding++   * (primitive types defined externally)++   Some technical stuff:++   * Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.++   * We have a simple collection of tactics which we use to elaborate source+     programs with implicit syntax into fully explicit terms.+-}+ module Core.TT where  import Control.Monad.State@@ -12,25 +30,14 @@  import Util.Pretty hiding (Str) -{- The language has:-   * Full dependent types-   * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...-   * Pattern matching letrec binding-   * (primitive types defined externally)--   Some technical stuff:-   * Typechecker is kept as simple as possible -        - no unification, just a checker for incomplete terms.-   * We have a simple collection of tactics which we use to elaborate source-     programs with implicit syntax into fully explicit terms.--}- data Option = TTypeInTType             | CheckConv   deriving Eq -data FC = FC { fc_fname :: String,-               fc_line :: Int }+-- | Source location. These are typically produced by the parser 'Idris.Parser.pfc'+data FC = FC { fc_fname :: String, -- ^ Filename+               fc_line :: Int -- ^ Line number+             }     deriving Eq {-!  deriving instance Binary FC @@ -61,6 +68,7 @@          | Inaccessible Name          | NonCollapsiblePostulate Name          | AlreadyDefined Name+         | ProofSearchFail Err          | At FC Err   deriving Eq @@ -85,6 +93,7 @@ score (CantUnify _ _ _ m _ s) = s + score m score (CantResolve _) = 20 score (NoSuchVariable _) = 1000+score (ProofSearchFail _) = 10000 score _ = 0  instance Show Err where@@ -161,14 +170,12 @@  -- RAW TERMS ---------------------------------------------------------------- --- Names are hierarchies of strings, describing scope (so no danger of+-- | Names are hierarchies of strings, describing scope (so no danger of -- duplicate names, but need to be careful on lookup).--- Also MN for machine chosen names--data Name = UN String-          | NS Name [String] -- root, namespaces -          | MN Int String-          | NErased -- name of somethng which is never used in scope+data Name = UN String -- ^ User-provided name+          | NS Name [String] -- ^ Root, namespaces +          | MN Int String -- ^ Machine chosen names+          | NErased -- ^ Name of somethng which is never used in scope   deriving (Eq, Ord) {-!  deriving instance Binary Name @@ -191,9 +198,8 @@     show (MN i s) = "{" ++ s ++ show i ++ "}"     show NErased = "_" --- Contexts allow us to map names to things. A root name maps to a collection+-- |Contexts allow us to map names to things. A root name maps to a collection -- of things in different namespaces with that name.- type Ctxt a = Map.Map Name (Map.Map Name a) emptyContext = Map.empty @@ -215,14 +221,17 @@                         Just xs -> Map.insert (nsroot n)                                          (Map.insert n v xs) ctxt -{- lookup a name in the context, given an optional namespace.+{-| Look up a name in the context, given an optional namespace.    The name (n) may itself have a (partial) namespace given.     Rules for resolution:+     - if an explicit namespace is given, return the names which match it. If none       match, return all names.+     - if the name has has explicit namespace given, return the names which match it       and ignore the given namespace.+     - otherwise, return all names.  -}@@ -314,10 +323,11 @@ deriving instance Binary Raw  !-} -data Binder b = Lam   { binderTy  :: b }+-- | All binding forms are represented in a unform fashion.+data Binder b = Lam   { binderTy  :: b {-^ type annotation for bound variable-}}               | Pi    { binderTy  :: b }               | Let   { binderTy  :: b,-                        binderVal :: b }+                        binderVal :: b {-^ value for bound variable-}}               | NLet  { binderTy  :: b,                         binderVal :: b }               | Hole  { binderTy  :: b}@@ -379,8 +389,9 @@  -- WELL TYPED TERMS --------------------------------------------------------- -data UExp = UVar Int -- universe variable-          | UVal Int -- explicit universe level+-- | Universe expressions for universe checking+data UExp = UVar Int -- ^ universe variable+          | UVal Int -- ^ explicit universe level   deriving (Eq, Ord)  instance Sized UExp where@@ -400,8 +411,9 @@     show (UVal x) = show x --     show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")" -data UConstraint = ULT UExp UExp-                 | ULE UExp UExp+-- | Universe constraints+data UConstraint = ULT UExp UExp -- ^ Strictly less than+                 | ULE UExp UExp -- ^ Less than or equal to   deriving Eq  instance Show UConstraint where@@ -429,15 +441,16 @@     TCon _ a == TCon _ b = (a == b) -- ignore tag     _        == _        = False -data TT n = P NameType n (TT n) -- embed type-          | V Int -          | Bind n (Binder (TT n)) (TT n)-          | App (TT n) (TT n) -- function, function type, arg-          | Constant Const-          | Proj (TT n) Int -- argument projection; runtime only-          | Erased-          | Impossible -- special case for totality checking-          | TType UExp+-- | Terms in the core language+data TT n = P NameType n (TT n) -- ^ named references+          | V Int -- ^ a resolved de Bruijn-indexed variable+          | Bind n (Binder (TT n)) (TT n) -- ^ a binding+          | App (TT n) (TT n) -- ^ function, function type, arg+          | Constant Const -- ^ constant+          | Proj (TT n) Int -- ^ argument projection; runtime only+          | Erased -- ^ an erased term+          | Impossible -- ^ special case for totality checking+          | TType UExp -- ^ the type of types at some level   deriving (Ord, Functor) {-!  deriving instance Binary TT @@ -493,8 +506,11 @@     (==) _              Erased         = True     (==) _              _              = False --- A few handy operations on well typed terms:+-- * A few handy operations on well typed terms: +-- | A term is injective iff it is a data constructor, type constructor,+-- constant, the type Type, pi-binding, or an application of an injective+-- term. isInjective :: TT n -> Bool isInjective (P (DCon _ _) _ _) = True isInjective (P (TCon _ _) _ _) = True@@ -504,7 +520,7 @@ isInjective (App f a)          = isInjective f isInjective _                  = False --- Count the number of instances of a de Bruijn index in a term+-- | Count the number of instances of a de Bruijn index in a term vinstances :: Int -> TT n -> Int vinstances i (V x) | i == x = 1 vinstances i (App f a) = vinstances i f + vinstances i a@@ -542,7 +558,7 @@ pToV' n i (Proj t idx) = Proj (pToV' n i t) idx pToV' n i t = t --- Convert several names. First in the list comes out as V 0+-- | Convert several names. First in the list comes out as V 0 pToVs :: Eq n => [n] -> TT n -> TT n pToVs ns tm = pToVs' ns tm 0 where     pToVs' []     tm i = tm@@ -591,8 +607,7 @@     no' i (Proj x _) = no' i x     no' i _ = True --- Returns all names used free in the term-+-- | Returns all names used free in the term freeNames :: Eq n => TT n -> [n] freeNames (P _ n _) = [n] freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])@@ -602,14 +617,12 @@ freeNames (Proj x i) = nub $ freeNames x freeNames _ = [] --- Return the arity of a (normalised) type-+-- | Return the arity of a (normalised) type arity :: TT n -> Int arity (Bind n (Pi t) sc) = 1 + arity sc arity _ = 0 --- deconstruct an application; returns the function and a list of arguments-+-- | Deconstruct an application; returns the function and a list of arguments unApply :: TT n -> (TT n, [TT n]) unApply t = ua [] t where     ua args (App f a) = ua (a:args) f@@ -792,8 +805,7 @@     bracket outer inner str | inner > outer = "(" ++ str ++ ")"                             | otherwise = str --- Check whether a term has any holes in it - impure if so-+-- | Check whether a term has any holes in it - impure if so pureTerm :: TT Name -> Bool pureTerm (App f a) = pureTerm f && pureTerm a pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where@@ -807,8 +819,7 @@  pureTerm _ = True --- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)-+-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings) weakenTm :: Int -> TT n -> TT n weakenTm i t = wk i 0 t   where wk i min (V x) | x >= min = V (i + x)@@ -817,7 +828,7 @@         wk i m t = t         wkb i m t           = fmap (wk i m) t --- weaken an environment so that all the de Bruijn indices are correct according+-- | Weaken an environment so that all the de Bruijn indices are correct according -- to the latest bound variable  weakenEnv :: EnvTT n -> EnvTT n
src/IRTS/Defunctionalise.hs view
@@ -212,10 +212,13 @@  mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl) mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]-                             (mkBigCase (MN 0 "APPLY")-                                        256 (DApp False (MN 0 "EVAL")-                                            [DV (Glob (MN 0 "fn"))])-                                 (mapMaybe applyCase xs)))+                             (case mapMaybe applyCase xs of+                                [] -> DNothing+                                cases ->+                                    mkBigCase (MN 0 "APPLY") 256+                                              (DApp False (MN 0 "EVAL")+                                               [DV (Glob (MN 0 "fn"))])+                                              cases))   where     applyCase (n, t, ApplyCase x) = Just x     applyCase _ = Nothing
src/Idris/AbsSyntax.hs view
@@ -68,10 +68,29 @@                 [t] -> return t                 _ -> return (Total []) +-- Get coercions which might return the required type+getCoercionsTo :: IState -> Type -> [Name]+getCoercionsTo i ty =+    let cs = idris_coercions i+        (fn,_) = unApply (getRetTy ty) in+        findCoercions fn cs+    where findCoercions t [] = []+          findCoercions t (n : ns) =+             let ps = case lookupTy Nothing n (tt_ctxt i) of+                         [ty] -> case unApply (getRetTy ty) of+                                   (t', _) -> +                                      if t == t' then [n] else []+                         _ -> [] in+                 ps ++ findCoercions t ns+ addToCG :: Name -> CGInfo -> Idris () addToCG n cg     = do i <- getIState         putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }++addCoercion :: Name -> Idris ()+addCoercion n = do i <- getIState+                   putIState $ i { idris_coercions = n : idris_coercions i }  addDocStr :: Name -> String -> Idris () addDocStr n doc
src/Idris/AbsSyntaxTree.hs view
@@ -46,10 +46,12 @@ -- This will include all the functions and data declarations, plus fixity declarations -- and syntax macros. +-- | The global state used in the Idris monad data IState = IState {-    tt_ctxt :: Context,+    tt_ctxt :: Context, -- ^ All the currently defined names and their terms     idris_constraints :: [(UConstraint, FC)],-    idris_infixes :: [FixDecl],+      -- ^ A list of universe constraints and their corresponding source locations+    idris_infixes :: [FixDecl], -- ^ Currently defined infix operators     idris_implicits :: Ctxt [PArg],     idris_statics :: Ctxt [Bool],     idris_classes :: Ctxt ClassInfo,@@ -65,10 +67,11 @@     idris_log :: String,     idris_options :: IOption,     idris_name :: Int,-    idris_metavars :: [Name],+    idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables+    idris_coercions :: [Name],     syntax_rules :: [Syntax],     syntax_keywords :: [String],-    imported :: [FilePath],+    imported :: [FilePath], -- ^ The imported modules     idris_scprims :: [(Name, (Int, PrimFn))],     idris_objs :: [FilePath],     idris_libs :: [String],@@ -125,16 +128,17 @@               | IBCFlags Name [FnOpt]               | IBCCG Name               | IBCDoc Name+              | IBCCoercion Name               | IBCDef Name -- i.e. main context   deriving Show  idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext                     emptyContext emptyContext emptyContext emptyContext-                   [] "" defaultOpts 6 [] [] [] [] [] [] [] []+                   [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []                    [] Nothing Nothing [] [] [] Hidden False [] Nothing --- The monad for the main REPL - reading and processing files and updating +-- | The monad for the main REPL - reading and processing files and updating  -- global state (hence the IO inner monad). type Idris = StateT IState IO @@ -147,6 +151,7 @@             | Bytecode     deriving (Show, Eq) +-- | REPL commands data Command = Quit              | Help              | Eval PTerm@@ -281,6 +286,7 @@  data FnOpt = Inlinable | TotalFn | PartialFn            | Coinductive | AssertTotal | TCGen+           | Implicit -- implicit coercion            | CExport String    -- export, with a C name            | Specialise [Name] -- specialise it, freeze these names     deriving (Show, Eq)@@ -293,32 +299,37 @@ inlinable :: FnOpts -> Bool inlinable = elem Inlinable -data PDecl' t -   = PFix     FC Fixity [String] -- fixity declaration-   | PTy      String SyntaxInfo FC FnOpts Name t   -- type declaration-   | PPostulate String SyntaxInfo FC FnOpts Name t-   | PClauses FC FnOpts Name [PClause' t]   -- pattern clause-   | PCAF     FC Name t -- top level constant-   | PData    String SyntaxInfo FC Bool -- codata-                            (PData' t)  -- data declaration-   | PParams  FC [(Name, t)] [PDecl' t] -- params block-   | PNamespace String [PDecl' t] -- new namespace-   | PRecord  String SyntaxInfo FC Name t String Name t     -- record declaration+-- | Top-level declarations such as compiler directives, definitions,+-- datatypes and typeclasses.+data PDecl' t+   = PFix     FC Fixity [String] -- ^ Fixity declaration+   | PTy      String SyntaxInfo FC FnOpts Name t   -- ^ Type declaration+   | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate+   | PClauses FC FnOpts Name [PClause' t]   -- ^ Pattern clause+   | PCAF     FC Name t -- ^ Top level constant+   | PData    String SyntaxInfo FC Bool (PData' t)  -- ^ Data declaration. The Bool argument is True for codata.+   | PParams  FC [(Name, t)] [PDecl' t] -- ^ Params block+   | PNamespace String [PDecl' t] -- ^ New namespace+   | PRecord  String SyntaxInfo FC Name t String Name t  -- ^ Record declaration    | PClass   String SyntaxInfo FC                [t] -- constraints               Name               [(Name, t)] -- parameters               [PDecl' t] -- declarations+              -- ^ Type class: arguments are documentation, syntax info, source location, constraints,+              -- class name, parameters, method declarations    | PInstance SyntaxInfo FC [t] -- constraints                              Name -- class                              [t] -- parameters                              t -- full instance type                              (Maybe Name) -- explicit name                              [PDecl' t]-   | PDSL     Name (DSL' t)-   | PSyntax  FC Syntax-   | PMutual  FC [PDecl' t]-   | PDirective (Idris ())+               -- ^ Instance declaration: arguments are syntax info, source location, constraints,+               -- class name, parameters, full instance type, optional explicit name, and definitions+   | PDSL     Name (DSL' t) -- ^ DSL declaration+   | PSyntax  FC Syntax -- ^ Syntax definition+   | PMutual  FC [PDecl' t] -- ^ Mutual block+   | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.   deriving Functor {-! deriving instance Binary PDecl'@@ -333,10 +344,14 @@ deriving instance Binary PClause' !-} -data PData' t  = PDatadecl { d_name :: Name,-                             d_tcon :: t,-                             d_cons :: [(String, Name, t, FC)] }+-- | Data declaration+data PData' t  = PDatadecl { d_name :: Name, -- ^ The name of the datatype+                             d_tcon :: t, -- ^ Type constructor+                             d_cons :: [(String, Name, t, FC)] -- ^ Constructors+                           }+                 -- ^ Data declaration                | PLaterdecl { d_name :: Name, d_tcon :: t }+                 -- ^ "Placeholder" for data whose constructors are defined later     deriving Functor {-! deriving instance Binary PData'@@ -411,16 +426,15 @@ --                                      (map (updateDNs ns) ds) -- updateDNs ns c = c --- High level language terms-+-- | High level language terms data PTerm = PQuote Raw            | PRef FC Name-           | PInferRef FC Name -- a name to be defined later+           | PInferRef FC Name -- ^ A name to be defined later            | PPatvar FC Name            | PLam Name PTerm PTerm            | PPi  Plicity Name PTerm PTerm-           | PLet Name PTerm PTerm PTerm -           | PTyped PTerm PTerm -- term with explicit type+           | PLet Name PTerm PTerm PTerm+           | PTyped PTerm PTerm -- ^ Term with explicit type            | PApp FC PTerm [PArg]            | PCase FC PTerm [(PTerm, PTerm)]            | PTrue FC@@ -431,7 +445,7 @@            | PPair FC PTerm PTerm            | PDPair FC PTerm PTerm PTerm            | PAlternative Bool [PTerm] -- True if only one may work-           | PHidden PTerm -- irrelevant or hidden pattern+           | PHidden PTerm -- ^ Irrelevant or hidden pattern            | PType            | PConstant Const            | Placeholder@@ -439,10 +453,11 @@            | PIdiom FC PTerm            | PReturn FC            | PMetavar Name-           | PProof [PTactic]-           | PTactics [PTactic] -- as PProof, but no auto solving-           | PElabError Err -- error to report on elaboration-           | PImpossible -- special case for declaring when an LHS can't typecheck+           | PProof [PTactic] -- ^ Proof script+           | PTactics [PTactic] -- ^ As PProof, but no auto solving+           | PElabError Err -- ^ Error to report on elaboration+           | PImpossible -- ^ Special case for declaring when an LHS can't typecheck+           | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice     deriving Eq {-!  deriving instance Binary PTerm @@ -984,6 +999,7 @@     se p Placeholder = "_"     se p (PDoBlock _) = "do block show not implemented"     se p (PElabError s) = show s+    se p (PCoerced t) = se p t --     se p x = "Not implemented"      sArg (PImp _ _ n tm _) = siArg (n, tm)
src/Idris/Completion.hs view
@@ -1,3 +1,4 @@+-- | Support for command-line completion at the REPL and in the prover module Idris.Completion (replCompletion, proverCompletion) where  import Core.Evaluate (ctxtAlist)@@ -122,6 +123,7 @@           completeArg ExprArg = completeExpr [] (prev, next)           completeCmdName = return $ ("", completeWith commands cmd) +-- | Complete REPL commands and defined identifiers replCompletion :: CompletionFunc Idris replCompletion (prev, next) = case firstWord of                                 ':':cmdName -> completeCmd (':':cmdName) (prev, next)@@ -137,7 +139,8 @@           completeArg (Just ExprTArg)   = completeExpr as (prev, next)           completeArg (Just AltsTArg)   = noCompletion (prev, next) -- TODO --proverCompletion :: [String] -> CompletionFunc Idris+-- | Complete tactics and their arguments+proverCompletion :: [String] -- ^ The names of current local assumptions+                 -> CompletionFunc Idris proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)     where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
src/Idris/Delaborate.hs view
@@ -108,6 +108,7 @@ pshow i (NonCollapsiblePostulate n)      = "The return type of postulate " ++ show n ++ " is not collapsible" pshow i (AlreadyDefined n) = show n ++ " is already defined"+pshow i (ProofSearchFail e) = pshow i e pshow i (At f e) = show f ++ ":" ++ pshow i e  showSc i [] = ""
src/Idris/ElabDecls.hs view
@@ -78,6 +78,8 @@          addDocStr n doc          addIBC (IBCDoc n)          addIBC (IBCFlags n opts')+         when (Implicit `elem` opts) $ do addCoercion n+                                          addIBC (IBCCoercion n)          when corec $ do setAccessibility n Frozen                          addIBC (IBCAccess n Frozen) @@ -1281,10 +1283,10 @@         logLvl 10 $ "Checking match"         i <- getIState         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)+            _ -> return ()+--             Left (x, y) -> tfail $ At fc +--                                     (Msg $ "The type-checked term and given term do not match: "+--                                            ++ show x ++ " and " ++ show y)         logLvl 10 $ "Checked match" --                           ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)
src/Idris/ElabTerm.hs view
@@ -120,7 +120,9 @@     elabE ina t = {- do g <- goal                  tm <- get_term                  trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm) -                    $ -} elab' ina t+                    $ -} +                  do t' <- insertCoerce ina t+                     elab' ina t'      local f = do e <- get_env                  return (f `elem` map fst e)@@ -191,9 +193,10 @@         = trySeq as         where -- if none work, take the error from the first               trySeq (x : xs) = let e1 = elab' ina x in-                                    try e1 (trySeq' e1 xs)-              trySeq' deferr [] = deferr-              trySeq' deferr (x : xs) = try (elab' ina x) (trySeq' deferr xs)+                                    try' e1 (trySeq' e1 xs) True+              trySeq' deferr [] = proofFail deferr+              trySeq' deferr (x : xs) +                  = try' (elab' ina x) (trySeq' deferr xs) True     elab' ina (PPatvar fc n) | pattern = patvar n     elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)                          = do ctxt <- get_context@@ -348,7 +351,7 @@                                             compare (priority x) (priority y))                                     (zip ns args)                     elabArgs (ina || not isinf, guarded)-                           [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)+                           [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)                     mkSpecialised ist fc f (map getTm args') tm                     solve                     ptm <- get_term@@ -442,14 +445,31 @@              shadowed new (PRef _ n) | n `elem` new = Placeholder              shadowed new t = t -    elabArgs ina failed retry [] _+    insertCoerce ina t =+        do ty <- goal+           -- Check for possible coercions to get to the goal+           -- and add them as 'alternatives'+           env <- get_env+           let ty' = normalise (tt_ctxt ist) env ty+           let cs = getCoercionsTo ist ty'+           let t' = case (t, cs) of+                         (PCoerced tm, _) -> tm+                         (_, []) -> t+                         (_, cs) -> PAlternative False [t ,+                                       PAlternative True (map (mkCoerce t) cs)]+           return t'+       where +         mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!+                            addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])++    elabArgs ina failed fc retry [] _ --         | retry = let (ns, ts) = unzip (reverse failed) in --                       elabArgs ina [] False ns ts         | otherwise = return ()-    elabArgs ina failed r (n:ns) ((_, Placeholder) : args) -        = elabArgs ina failed r ns args-    elabArgs ina failed r (n:ns) ((lazy, t) : args)-        | lazy && not pattern +    elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args) +        = elabArgs ina failed fc r ns args+    elabArgs ina failed fc r (n:ns) ((lazy, t) : args)+        | lazy && not pattern           = do elabArg n (PApp bi (PRef bi (UN "lazy"))                                [pimp (UN "a") Placeholder,                                 pexp t]); @@ -457,15 +477,17 @@       where elabArg n t                  = do hs <- get_holes                      tm <- get_term+                     t' <- insertCoerce ina t                      failed' <- -- trace (show (n, t, hs, tm)) $ +                                -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $                                 case n `elem` hs of                                    True -> --                                       if r --                                          then try (do focus n; elabE ina t; return failed) --                                                   (return ((n,(lazy, t)):failed))-                                         do focus n; elabE ina t; return failed+                                         do focus n; elab' ina t'; return failed                                    False -> return failed-                     elabArgs ina failed r ns args+                     elabArgs ina failed fc r ns args  -- For every alternative, look at the function at the head. Automatically resolve -- any nested alternatives where that function is also at the head
src/Idris/IBC.hs view
@@ -21,7 +21,7 @@ import Paths_idris  ibcVersion :: Word8-ibcVersion = 26+ibcVersion = 27  data IBCFile = IBCFile { ver :: Word8,                          sourcefile :: FilePath,@@ -44,14 +44,15 @@                          ibc_flags :: [(Name, [FnOpt])],                          ibc_cg :: [(Name, CGInfo)],                          ibc_defs :: [(Name, Def)],-                         ibc_docstrings :: [(Name, String)]+                         ibc_docstrings :: [(Name, String)],+                         ibc_coercions :: [Name]                        } {-!  deriving instance Binary IBCFile  !-}  initIBC :: IBCFile-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []  loadIBC :: FilePath -> Idris () loadIBC fp = do iLOG $ "Loading ibc " ++ fp@@ -119,6 +120,7 @@ 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 (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f } 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 }@@ -151,6 +153,7 @@                pTotal (ibc_total i)                pCG (ibc_cg i)                pDocs (ibc_docstrings i)+               pCoercions (ibc_coercions i)  timestampOlder :: FilePath -> FilePath -> IO () timestampOlder src ibc = do srct <- getModificationTime src@@ -270,6 +273,9 @@ pCG :: [(Name, CGInfo)] -> Idris () pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds +pCoercions :: [Name] -> Idris ()+pCoercions ns = mapM_ (\ n -> addCoercion n) ns+ ----- Generated by 'derive'  instance Binary SizeChange where@@ -738,7 +744,7 @@                    _ -> 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 x17 x18 x19 x20 x21 x22)+        put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23)           = do put x1                put x2                put x3@@ -761,6 +767,7 @@                put x20                put x21                put x22+               put x23         get           = do x1 <- get                if x1 == ibcVersion then @@ -785,7 +792,8 @@                     x20 <- get                     x21 <- get                     x22 <- get-                    return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22)+                    x23 <- get+                    return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23)                   else return (initIBC { ver = x1 })   instance Binary FnOpt where@@ -799,6 +807,7 @@                                    put x                 Coinductive -> putWord8 5                 PartialFn -> putWord8 6+                Implicit -> putWord8 7         get           = do i <- getWord8                case i of@@ -810,6 +819,7 @@                            return (Specialise x)                    5 -> return Coinductive                    6 -> return PartialFn+                   7 -> return Implicit                    _ -> error "Corrupted binary data for FnOpt"  instance Binary Fixity where
src/Idris/Parser.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE PatternGuards #-}-+-- | Parse the full Idris language. module Idris.Parser where  import Idris.AbsSyntax@@ -259,6 +259,7 @@                                         when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"                     _             -> return () +-- | Use Parsec's internal state to construct a source code position pfc :: IParser FC pfc = do s <- getPosition          let (dir, file) = splitFileName (sourceName s)@@ -270,9 +271,8 @@              return (toPath f)   where toPath n = foldl1 (</>) $ splitOn "." n --- a program is a list of declarations, possibly with associated--- documentation strings-+-- | A program is a list of declarations, possibly with associated+-- documentation strings. parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->               Idris [PDecl] parseProg syn fname input pos@@ -288,8 +288,7 @@             Right (x, i) -> do putIState i                                return (collect x) --- Collect PClauses with the same function name-+-- | Collect 'PClauses' with the same function name collect :: [PDecl] -> [PDecl] collect (c@(PClauses _ o _ _) : ds)      = clauses (cname c) [] (c : ds)@@ -323,6 +322,7 @@                i <- getState                return $ desugar syn i x +-- | Parse a top-level declaration pDecl :: SyntaxInfo -> IParser [PDecl] pDecl syn = do notEndBlock                pDeclBody where@@ -401,12 +401,13 @@     name _ = Nothing      -- Can't parse two full expressions (i.e. expressions with application) in a row-    -- so change the first to a simple expression+    -- so change them both 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' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :+                                           mkSimple es     mkSimple' (e : es) = e : mkSimple' es     mkSimple' [] = [] @@ -672,7 +673,7 @@            UN n <- iName (syntax_keywords i)            return (UN ('@':n)) --- Parser for an operator in function position, i.e. enclosed by `()', with an+-- | Parser for an operator in function position, i.e. enclosed by `()', with an -- optional namespace. pOpFront = maybeWithNS pOpFrontNoNS False []   where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o@@ -706,6 +707,7 @@       <|> do lchar '%'; reserved "specialise";               lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'              pFnOpts (Specialise ns : opts)+      <|> do reserved "implicit"; pFnOpts (Implicit : opts)       <|> return opts  addAcc :: Name -> Maybe Accessibility -> IParser ()
src/Idris/REPL.hs view
@@ -50,7 +50,10 @@ import Data.Char import Data.Version -repl :: IState -> [FilePath] -> InputT Idris ()+-- | Run the REPL+repl :: IState -- ^ The initial state+     -> [FilePath] -- ^ The loaded modules+     -> InputT Idris () repl orig mods    = H.catch       (do let prompt = mkPrompt mods@@ -69,10 +72,12 @@          ctrlC e = do lift $ iputStrLn (show e)                       repl orig mods +-- | The prompt consists of the currently loaded modules, or "Idris" if there are none mkPrompt [] = "Idris" mkPrompt [x] = "*" ++ dropExtension x mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs +-- | Determine whether a file uses literate syntax lit f = case splitExtension f of             (_, ".lidr") -> True             _ -> False