diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 diff --git a/effects/Effect/Exception.idr b/effects/Effect/Exception.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/Exception.idr @@ -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? + diff --git a/effects/Effect/File.idr b/effects/Effect/File.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/File.idr @@ -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 + + + + diff --git a/effects/Effect/Random.idr b/effects/Effect/Random.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/Random.idr @@ -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) + + diff --git a/effects/Effect/Select.idr b/effects/Effect/Select.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/Select.idr @@ -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 + diff --git a/effects/Effect/State.idr b/effects/Effect/State.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/State.idr @@ -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) + diff --git a/effects/Effect/StdIO.idr b/effects/Effect/StdIO.idr new file mode 100644 --- /dev/null +++ b/effects/Effect/StdIO.idr @@ -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 diff --git a/effects/Effects.idr b/effects/Effects.idr new file mode 100644 --- /dev/null +++ b/effects/Effects.idr @@ -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 () + diff --git a/effects/Makefile b/effects/Makefile new file mode 100644 --- /dev/null +++ b/effects/Makefile @@ -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: diff --git a/effects/effects.ipkg b/effects/effects.ipkg new file mode 100644 --- /dev/null +++ b/effects/effects.ipkg @@ -0,0 +1,6 @@ +package effects + +opts = "-i ../lib" +modules = Effects, + Effect.Exception, Effect.File, Effect.State, + Effect.Random, Effect.StdIO, Effect.Select diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -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 diff --git a/lib/Builtins.idr b/lib/Builtins.idr --- a/lib/Builtins.idr +++ b/lib/Builtins.idr @@ -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 diff --git a/lib/Control/Arrow.idr b/lib/Control/Arrow.idr --- a/lib/Control/Arrow.idr +++ b/lib/Control/Arrow.idr @@ -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) diff --git a/lib/Control/Catchable.idr b/lib/Control/Catchable.idr new file mode 100644 --- /dev/null +++ b/lib/Control/Catchable.idr @@ -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 () = [] diff --git a/lib/Control/Category.idr b/lib/Control/Category.idr --- a/lib/Control/Category.idr +++ b/lib/Control/Category.idr @@ -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) diff --git a/lib/Control/IOExcept.idr b/lib/Control/IOExcept.idr new file mode 100644 --- /dev/null +++ b/lib/Control/IOExcept.idr @@ -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 + diff --git a/lib/Data/Morphisms.idr b/lib/Data/Morphisms.idr --- a/lib/Data/Morphisms.idr +++ b/lib/Data/Morphisms.idr @@ -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 diff --git a/lib/Data/Sign.idr b/lib/Data/Sign.idr new file mode 100644 --- /dev/null +++ b/lib/Data/Sign.idr @@ -0,0 +1,6 @@ +module Data.Sign + +data Sign = Plus | Minus + +class Signed t where + total sign : t -> Sign diff --git a/lib/Data/Z.idr b/lib/Data/Z.idr new file mode 100644 --- /dev/null +++ b/lib/Data/Z.idr @@ -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 + diff --git a/lib/Decidable/Equality.idr b/lib/Decidable/Equality.idr new file mode 100644 --- /dev/null +++ b/lib/Decidable/Equality.idr @@ -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 + + diff --git a/lib/Effects.idr b/lib/Effects.idr new file mode 100644 --- /dev/null +++ b/lib/Effects.idr @@ -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 () + diff --git a/lib/Prelude.idr b/lib/Prelude.idr --- a/lib/Prelude.idr +++ b/lib/Prelude.idr @@ -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 diff --git a/lib/Prelude/Either.idr b/lib/Prelude/Either.idr --- a/lib/Prelude/Either.idr +++ b/lib/Prelude/Either.idr @@ -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 diff --git a/lib/Prelude/Fin.idr b/lib/Prelude/Fin.idr --- a/lib/Prelude/Fin.idr +++ b/lib/Prelude/Fin.idr @@ -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 diff --git a/lib/Prelude/Maybe.idr b/lib/Prelude/Maybe.idr --- a/lib/Prelude/Maybe.idr +++ b/lib/Prelude/Maybe.idr @@ -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 --- : \"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.\" +-- : "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 diff --git a/lib/Prelude/Vect.idr b/lib/Prelude/Vect.idr --- a/lib/Prelude/Vect.idr +++ b/lib/Prelude/Vect.idr @@ -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 diff --git a/lib/base.ipkg b/lib/base.ipkg --- a/lib/base.ipkg +++ b/lib/base.ipkg @@ -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 diff --git a/rts/idris_gmp.c b/rts/idris_gmp.c --- a/rts/idris_gmp.c +++ b/rts/idris_gmp.c @@ -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)); } } diff --git a/rts/idris_rts.c b/rts/idris_rts.c --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -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; diff --git a/rts/idris_rts.h b/rts/idris_rts.h --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -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" diff --git a/rts/libidris_rts.a b/rts/libidris_rts.a Binary files a/rts/libidris_rts.a and b/rts/libidris_rts.a differ diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs --- a/src/Core/CaseTree.hs +++ b/src/Core/CaseTree.hs @@ -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 diff --git a/src/Core/Constraints.hs b/src/Core/Constraints.hs --- a/src/Core/Constraints.hs +++ b/src/Core/Constraints.hs @@ -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 diff --git a/src/Core/CoreParser.hs b/src/Core/CoreParser.hs --- a/src/Core/CoreParser.hs +++ b/src/Core/CoreParser.hs @@ -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"] } diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs --- a/src/Core/Elaborate.hs +++ b/src/Core/Elaborate.hs @@ -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 diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -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) diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs --- a/src/Core/ProofState.hs +++ b/src/Core/ProofState.hs @@ -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) = diff --git a/src/Core/TT.hs b/src/Core/TT.hs --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -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 diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs --- a/src/IRTS/Defunctionalise.hs +++ b/src/IRTS/Defunctionalise.hs @@ -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 diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -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 diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -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) diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs --- a/src/Idris/Completion.hs +++ b/src/Idris/Completion.hs @@ -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 diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -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 [] = "" diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -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) diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -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 diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -21,7 +21,7 @@ import Paths_idris ibcVersion :: Word8 -ibcVersion = 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 diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -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 () diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -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