packages feed

idris 0.9.10 → 0.9.10.1

raw patch · 46 files changed

+882/−650 lines, 46 files

Files

Makefile view
@@ -1,4 +1,4 @@-.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test  include config.mk -include custom.mk@@ -13,7 +13,9 @@ build: dist/setup-config 	$(CABAL) build $(CABALFLAGS) -test:+test: doc test_c++test_c: 	$(MAKE) -C test IDRIS=../dist/build/idris  test_java:
idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.10+Version:        0.9.10.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -101,8 +101,6 @@                         llvm/*.c                        llvm/Makefile--                       tutorial/examples/*.idr                         test/Makefile                        test/runtest.pl
libs/base/Data/Vect/Quantifiers.idr view
@@ -5,8 +5,8 @@   There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)  anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_-anyNilAbsurd Here impossible-anyNilAbsurd There impossible+anyNilAbsurd (Here _) impossible +anyNilAbsurd (There _) impossible  anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b anyElim _ f (Here p) = f p
libs/prelude/Decidable/Equality.idr view
@@ -177,3 +177,40 @@     decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl     decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))     decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))+    ++-- For the primitives, we have to cheat because we don't have access to their+-- internal implementations.++--------------------------------------------------------------------------------+-- Int+--------------------------------------------------------------------------------++instance DecEq Int where+    decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)+                          else No (really_believe_me _|_)++--------------------------------------------------------------------------------+-- Char+--------------------------------------------------------------------------------++instance DecEq Char where+    decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)+                          else No (really_believe_me _|_)++--------------------------------------------------------------------------------+-- Integer+--------------------------------------------------------------------------------++instance DecEq Integer where+    decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)+                          else No (really_believe_me _|_)++--------------------------------------------------------------------------------+-- Float+--------------------------------------------------------------------------------++instance DecEq Float where+    decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)+                          else No (really_believe_me _|_)+
libs/prelude/Prelude/Fin.idr view
@@ -3,6 +3,8 @@ import Prelude.Nat import Prelude.Either +%default total+ data Fin : Nat -> Type where     fZ : Fin (S k)     fS : Fin k -> Fin (S k)@@ -12,19 +14,25 @@     (==) (fS k) (fS k') = k == k'     (==) _ _ = False -finToNat : Fin n -> Nat -> Nat-finToNat fZ a = a-finToNat (fS x) a = finToNat x (S a)+FinZAbsurd : Fin Z -> _|_+FinZAbsurd fZ impossible +FinZElim : Fin Z -> a+FinZElim x = FalseElim (FinZAbsurd x)++finToNat : Fin n -> Nat+finToNat fZ = Z+finToNat (fS k) = S (finToNat k)+ instance Cast (Fin n) Nat where-    cast x = finToNat x Z+    cast x = finToNat x -finToInt : Fin n -> Integer -> Integer-finToInt fZ a = a-finToInt (fS x) a = finToInt x (a + 1)+finToInteger : Fin n -> Integer+finToInteger fZ     = 0+finToInteger (fS k) = 1 + finToInteger k  instance Cast (Fin n) Integer where-    cast x = finToInt x 0+    cast x = finToInteger x  weaken : Fin n -> Fin (S n) weaken fZ     = fZ
libs/prelude/Prelude/List.idr view
@@ -15,9 +15,12 @@ infixr 7 :: infixl 8 ++ -data List a+%elim data List a   = Nil   | (::) a (List a)++-- Name hints for interactive editing+%name List xs, ys, zs, ws  -------------------------------------------------------------------------------- -- Syntactic tests
libs/prelude/Prelude/Nat.idr view
@@ -10,9 +10,12 @@ %access public %default total -data Nat+%elim data Nat   = Z   | S Nat++-- name hints for interactive editing+%name Nat k,j,i,n,m  -------------------------------------------------------------------------------- -- Syntactic tests
libs/prelude/Prelude/Vect.idr view
@@ -11,10 +11,13 @@  infixr 7 :: -data Vect : Nat -> Type -> Type where+%elim data Vect : Nat -> Type -> Type where   Nil  : Vect Z a-  (::) : a -> Vect n a -> Vect (S n) a+  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a +-- Hints for interactive editing+%name Vect xs,ys,zs,ws+ -------------------------------------------------------------------------------- -- Indexing into vectors --------------------------------------------------------------------------------@@ -51,15 +54,14 @@ -- Subvectors -------------------------------------------------------------------------------- -take : Fin n -> Vect n a -> (p ** Vect p a)-take fZ     xs      = (_ ** [])-take (fS k) []      impossible-take (fS k) (x::xs) with (take k xs)-  | (_ ** tail) = (_ ** x::tail)+take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a+take (fS k) []      = FinZElim k+take fZ     _       = []+take (fS k) (x::xs) = x :: take k xs -drop : Fin n -> Vect n a -> (p ** Vect p a)-drop fZ     xs      = (_ ** xs)-drop (fS k) []      impossible+drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a+drop (fS k) []      = FinZElim k+drop fZ     xs      ?= xs drop (fS k) (x::xs) = drop k xs  --------------------------------------------------------------------------------@@ -143,15 +145,13 @@     reverse' acc []      ?= acc     reverse' acc (x::xs) ?= reverse' (x::acc) xs -total intersperse' : a -> Vect m a -> (p ** Vect p a)-intersperse' sep []      = (_ ** [])-intersperse' sep (y::ys) with (intersperse' sep ys)-  | (_ ** tail) = (_ ** sep::y::tail)--total intersperse : a -> Vect m a -> (p ** Vect p a)-intersperse sep []      = (_ ** [])-intersperse sep (x::xs) with (intersperse' sep xs)-  | (_ ** tail) = (_ ** x::tail)+intersperse : a -> Vect n a -> Vect (n + pred n) a+intersperse sep []      = []+intersperse sep (x::xs) = x :: intersperse' sep xs+  where+    intersperse' : a -> Vect n a -> Vect (n + n) a+    intersperse' sep []      = []+    intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs  -------------------------------------------------------------------------------- -- Membership tests@@ -311,6 +311,12 @@ -- Proofs -------------------------------------------------------------------------------- +Prelude.Vect.drop_lemma_1 = proof {+  intros;+  rewrite sym (minusZeroRight n);+  trivial;+}+ Prelude.Vect.reverse'_lemma_2 = proof {     intros;     rewrite (plusSuccRightSucc m n1);@@ -323,3 +329,8 @@     exact value; } +Prelude.Vect.intersperse'_lemma_1 = proof {+  intros;+  rewrite (plusSuccRightSucc n1 n1);+  trivial;+}
src/Core/Elaborate.hs view
@@ -392,7 +392,7 @@                    = do ctxt <- get_context                         case lookupTy n ctxt of                                 [] -> lift $ tfail $ NoSuchVariable n-                                _ -> fail $ "Too many arguments for " ++ show fn+                                _ -> lift $ tfail $ TooManyArguments n             | otherwise = fail $ "Too many arguments for " ++ show fn      doClaim ((i, _), n, t) = do claim n t
src/Core/Evaluate.hs view
@@ -767,7 +767,7 @@                      OK (CaseDef args_ct sc_ct _),                      OK (CaseDef args_inl sc_inl _),                      OK (CaseDef args_rt sc_rt _)) ->-                       let inl = alwaysInline -- || tcdict+                       let inl = alwaysInline -- tcdict                            inlc = (inl || small n args_ct sc_ct) && (not asserted)                            inlr = inl || small n args_rt sc_rt                            cdef = CaseDefs (args_tot, sc_tot)
src/Core/TT.hs view
@@ -85,6 +85,7 @@          | UnifyScope Name Name Term [(Name, Type)]          | CantInferType String          | NonFunctionType Term Term+         | TooManyArguments Name          | CantIntroduce Term          | NoSuchVariable Name          | NoTypeDecl Name@@ -237,6 +238,7 @@                  | ParentN Name String                  | MethodN Name                  | CaseN Name+                 | ElimN Name   deriving (Eq, Ord) {-! deriving instance Binary SpecialName@@ -269,19 +271,20 @@     show (MethodN m) = "method " ++ show m     show (ParentN p c) = show p ++ "#" ++ c     show (CaseN n) = "case block in " ++ show n+    show (ElimN n) = "<<" ++ show n ++ " eliminator>>"  -- Show a name in a way decorated for code generation, not human reading showCG :: Name -> String showCG (UN n) = n-showCG (NS n s) = showSep "." (reverse s) ++ "." ++ show n+showCG (NS n s) = showSep "." (reverse s) ++ "." ++ showCG n showCG (MN _ "underscore") = "_" showCG (MN i s) = "{" ++ s ++ show i ++ "}" showCG (SN s) = showCG' s-  where showCG' (WhereN i p c) = show p ++ ":" ++ show c ++ ":" ++ show i-        showCG' (InstanceN cl inst) = '@':show cl ++ '$':showSep ":" inst-        showCG' (MethodN m) = '!':show m-        showCG' (ParentN p c) = show p ++ "#" ++ show c-        showCG' (CaseN c) = show c ++ "_case"+  where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i+        showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" inst+        showCG' (MethodN m) = '!':showCG m+        showCG' (ParentN p c) = showCG p ++ "#" ++ show c+        showCG' (CaseN c) = showCG c ++ "_case" showCG NErased = "_"  @@ -830,6 +833,11 @@ getRetTy (Bind n (PVTy _) sc) = getRetTy sc getRetTy (Bind n (Pi _) sc)   = getRetTy sc getRetTy sc = sc++uniqueNameFrom :: [Name] -> [Name] -> Name+uniqueNameFrom (s : supply) hs+       | s `elem` hs = uniqueNameFrom supply hs+       | otherwise   = s  uniqueName :: Name -> [Name] -> Name uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
src/Idris/AbsSyntax.hs view
@@ -167,6 +167,25 @@    = do i <- getIState         putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) } +addNameHint :: Name -> Name -> Idris ()+addNameHint ty n+   = do i <- getIState+        ty' <- case lookupCtxtName ty (idris_implicits i) of+                       [(tyn, _)] -> return tyn+                       [] -> throwError (NoSuchVariable ty)+                       tyns -> throwError (CantResolveAlts (map show (map fst tyns)))+        let ns' = case lookupCtxt ty' (idris_namehints i) of+                       [ns] -> ns ++ [n]+                       _ -> [n]+        putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }++getNameHints :: IState -> Name -> [Name]+getNameHints i (UN "->") = [UN "f",UN "g"]+getNameHints i n =+        case lookupCtxt n (idris_namehints i) of+             [ns] -> ns+             _ -> []+ addToCalledG :: Name -> [Name] -> Idris () addToCalledG n ns = return () -- TODO @@ -634,6 +653,7 @@                       [("", inferCon, PPi impl (MN 0 "A") PType (                                   PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))                                   (PRef bi inferTy)), bi)]+inferOpts = []  infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t] infP = P (TCon 6 0) inferTy (TType (UVal 0))@@ -646,7 +666,7 @@ getInferType (Bind n b sc) = Bind n b $ getInferType sc getInferType (App (App _ ty) _) = ty --- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class  primNames = [unitTy, unitCon,              falseTy, pairTy, pairCon,@@ -656,9 +676,11 @@ unitCon  = MN 0 "__II" unitDecl = PDatadecl unitTy PType                      [("", unitCon, PRef bi unitTy, bi)]+unitOpts = [DefaultEliminator]  falseTy   = MN 0 "__False" falseDecl = PDatadecl falseTy PType []+falseOpts = []  pairTy    = MN 0 "__Pair" pairCon   = MN 0 "__MkPair"@@ -670,6 +692,7 @@                            (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),                                                 pexp (PRef bi (n "B"))])))), bi)]     where n a = MN 0 a+pairOpts = []  eqTy = UN "=" eqCon = UN "refl"@@ -683,7 +706,15 @@                                                     pexp (PRef bi (n "x")),                                                     pexp (PRef bi (n "x"))])), bi)]     where n a = MN 0 a+eqOpts = [] +elimName       = UN "__Elim"+elimMethElimTy = UN "__elimTy"+elimMethElim   = UN "elim"+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)] +                     [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,+                      PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]+ -- Defined in builtins.idr sigmaTy   = UN "Exists" existsCon = UN "Ex_intro"@@ -1360,26 +1391,6 @@                              put (False : spos)                              return (PPi p n t sc')         pos ns ss t = return t---- Debugging/logging stuff--dumpDecls :: [PDecl] -> String-dumpDecls [] = ""-dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds--dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops-dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t-dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)-dumpDecl (PData _ _ _ _ d) = showDImp True d-dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"-dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"-dumpDecl (PSyntax _ syn) = "syntax " ++ show syn-dumpDecl (PClass _ _ _ cs n ps ds)-    = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds-dumpDecl (PInstance _ _ cs n _ t _ ds)-    = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds-dumpDecl _ = "..."--- dumpDecl (PImport i) = "import " ++ i  -- for 6.12/7 compatibility data EitherErr a b = LeftErr a | RightOK b
src/Idris/AbsSyntaxTree.hs view
@@ -92,6 +92,7 @@     idris_dsls :: Ctxt DSL,     idris_optimisation :: Ctxt OptInfo,     idris_datatypes :: Ctxt TypeInfo,+    idris_namehints :: Ctxt [Name],     idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported       -- ^ list of lhs/rhs, and a list of missing clauses     idris_flags :: Ctxt [FnOpt],@@ -183,12 +184,14 @@               | IBCDoc Name               | IBCCoercion Name               | IBCDef Name -- i.e. main context+              | IBCNameHint (Name, Name)               | IBCLineApp FilePath Int PTerm   deriving Show  idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext+                   emptyContext                    [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []                    [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput                    True defaultTheme stdout@@ -392,6 +395,14 @@ dictionary :: FnOpts -> Bool dictionary = elem Dictionary ++-- | Data declaration options+data DataOpt = Codata -- Set if the the data-type is coinductive+             | DefaultEliminator -- Set if an eliminator should be generated for data type+    deriving (Show, Eq)++type DataOpts = [DataOpt]+ -- | Top-level declarations such as compiler directives, definitions, -- datatypes and typeclasses. data PDecl' t@@ -400,7 +411,7 @@    | 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.+   | PData    String SyntaxInfo FC DataOpts (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@@ -869,13 +880,23 @@ instance Show PData where     show d = showDImp False d +showDecls :: Bool -> [PDecl] -> String+showDecls _ [] = ""+showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds+ showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops-showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty-showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty-showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)-showDeclImp _ (PData _ _ _ _ d) = show d-showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++-                                    showSep "\n" (map show ps)+showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t+showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)+showDeclImp _ (PData _ _ _ _ d) = showDImp True d+showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"+showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"+showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn+showDeclImp i (PClass _ _ _ cs n ps ds)+    = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds+showDeclImp i (PInstance _ _ cs n _ t _ ds)+    = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds+showDeclImp _ _ = "..."+-- showDeclImp (PImport i) = "import " ++ i   showCImp :: Bool -> PClause -> String@@ -1121,7 +1142,7 @@                                    Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n                                    Nothing -> showbasic n     where name = if impl then show n else showbasic n-          showbasic n@(UN _) = show n+          showbasic n@(UN _) = showCG n           showbasic (MN _ s) = s           showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n           showbasic (SN s) = show s
src/Idris/CaseSplit.hs view
@@ -3,6 +3,7 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,                        getClause, getProofClause,                        mkWith,+                       nameMissing,                        getUniq, nameRoot) where  -- splitting a variable in a pattern clause@@ -71,38 +72,68 @@                    logLvl 3 ("Split:\n" ++                               (showSep "\n" (map show (mapMaybe id newPats))))                    logLvl 3 "----"-                   let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)+                   let newPats' = mergeAllPats ist n t (mapMaybe id newPats)                    iLOG ("Name updates " ++ showSep "\n"                          (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))                    return (map snd newPats')  data MergeState = MS { namemap :: [(Name, Name)],+                       invented :: [(Name, Name)],+                       explicit :: [Name],                        updates :: [(Name, PTerm)] }  addUpdate n tm = do ms <- get                     put (ms { updates = ((n, stripNS tm) : updates ms) } ) +inventName ist ty n = +    do ms <- get+       let supp = case ty of+                       Nothing -> []+                       Just t -> getNameHints ist t+       let nsupp = case n of+                        MN i ('_':_) -> mkSupply (supp ++ varlist)+                        MN i n -> mkSupply (UN n : supp ++ varlist)+                        x -> mkSupply (x : supp)+       let badnames = map snd (namemap ms) ++ map snd (invented ms) +++                      explicit ms+       case lookup n (invented ms) of+          Just n' -> return n'+          Nothing ->+             do let n' = uniqueNameFrom nsupp badnames+                put (ms { invented = (n, n') : invented ms })+                return n'+                +mkSupply ns = mkSupply' ns (map nextName ns)+  where mkSupply' xs ns' = xs ++ mkSupply ns'+   +varlist = map (UN . (:[])) "xyzwstuv" -- EB's personal preference :)+ stripNS tm = mapPT dens tm where     dens (PRef fc n) = PRef fc (nsroot n)     dens t = t -mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]-mergeAllPats ctxt t [] = []-mergeAllPats ctxt t (p : ps)-    = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])-          ps' = mergeAllPats ctxt t ps in-          ((p, u) : ps')+mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]+mergeAllPats ist cv t [] = []+mergeAllPats ist cv t (p : ps)+    = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing) +                                      (MS [] [] (filter (/=cv) (patvars t)) [])+          ps' = mergeAllPats ist cv t ps in+          ((p', u) : ps')+  where patvars (PRef _ n) = [n]+        patvars (PApp _ _ as) = concatMap (patvars . getTm) as+        patvars (PPatvar _ n) = [n]+        patvars _ = [] -mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm+mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm -- If any names are unified, make sure they stay unified. Always prefer -- user provided name (first pattern)-mergePat ctxt (PPatvar fc n) new-  = mergePat ctxt (PRef fc n) new-mergePat ctxt old (PPatvar fc n)-  = mergePat ctxt old (PRef fc n)-mergePat ctxt orig@(PRef fc n) new@(PRef _ n')-  | isDConName n' ctxt = do addUpdate n new;-                            return new+mergePat ist (PPatvar fc n) new t+  = mergePat ist (PRef fc n) new t+mergePat ist old (PPatvar fc n) t+  = mergePat ist old (PRef fc n) t+mergePat ist orig@(PRef fc n) new@(PRef _ n') t+  | isDConName n' (tt_ctxt ist) = do addUpdate n new+                                     return new   | otherwise     = do ms <- get          case lookup n' (namemap ms) of@@ -110,36 +141,49 @@                            return (PRef fc x)               Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })                             return (PRef fc n)-mergePat ctxt (PApp _ _ args) (PApp fc f args')-      = do newArgs <- zipWithM mergeArg args args'+mergePat ist (PApp _ _ args) (PApp fc f args') t+      = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))            return (PApp fc f newArgs)-   where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)-                           case x of-                                (PImp _ _ _ _ _ _) ->-                                   return (y { machine_inf = machine_inf x,-                                               getTm = tm' })-                                _ -> return (y { getTm = tm' })-mergePat ctxt (PRef fc n) t = do tm <- tidy t-                                 addUpdate n tm-                                 return tm-mergePat ctxt x y = return y+   where mergeArg x (y, t)+              = do tm' <- mergePat ist (getTm x) (getTm y) t+                   case x of+                        (PImp _ _ _ _ _ _) ->+                             return (y { machine_inf = machine_inf x,+                                         getTm = tm' })+                        _ -> return (y { getTm = tm' })+mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty+                                    addUpdate n tm+                                    return tm+mergePat ist x y t = return y  mergeUserImpl :: PTerm -> PTerm -> PTerm mergeUserImpl x y = x -tidy orig@(PRef fc n)+argTys :: IState -> PTerm -> [Maybe Name]+argTys ist (PRef fc n) +    = case lookupTy n (tt_ctxt ist) of+           [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing+           _ -> repeat Nothing+  where tyName (Bind _ (Pi _) _) = Just (UN "->")+        tyName t | (P _ n _, _) <- unApply t = Just n+                 | otherwise = Nothing+argTys _ _ = repeat Nothing++tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm+tidy ist orig@(PRef fc n) ty      = do ms <- get           case lookup n (namemap ms) of                Just x -> return (PRef fc x)                Nothing -> case n of                                (UN _) -> return orig-                               _ -> return Placeholder-tidy (PApp fc f args)-     = do args' <- mapM tidyArg args+                               _ -> do n' <- inventName ist ty n+                                       return (PRef fc n')+tidy ist (PApp fc f args) ty+     = do args' <- zipWithM tidyArg args (argTys ist f)           return (PApp fc f args')-    where tidyArg x = do tm' <- tidy (getTm x)-                         return (x { getTm = tm' })-tidy tm = return tm+    where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'+                             return (x { getTm = tm' })+tidy ist tm ty = return tm   -- mapPT tidyVar tm@@ -184,10 +228,10 @@  replaceVar ctxt n t pat = pat -splitOnLine :: Int -- ^ line number-               -> Name -- ^ variable-               -> FilePath -- ^ name of file-               -> Idris [[(Name, PTerm)]]+splitOnLine :: Int         -- ^ line number+            -> Name        -- ^ variable+            -> FilePath    -- ^ name of file+            -> Idris [[(Name, PTerm)]] splitOnLine l n fn = do --     let (before, later) = splitAt (l-1) (lines inp) --     i <- getIState@@ -242,9 +286,9 @@             '{' : space ++ updatePat False n tm rest'     updatePat True n tm xs@(c:rest) | length xs > length n         = let (before, after@(next:_)) = splitAt (length n) xs in-              if (before == n && not (isAlpha next))+              if (before == n && not (isAlphaNum next))                  then addBrackets tm ++ updatePat False n tm after-                 else c : updatePat (not (isAlpha c)) n tm rest+                 else c : updatePat (not (isAlphaNum c)) n tm rest     updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest      addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"@@ -263,25 +307,36 @@              (before, ('_' : after)) -> nameRoot (acc ++ [before]) after              _ -> showSep "_" (acc ++ [nm]) -getClause :: Int -> -- ^ Line type is declared on-             Name -> -- ^ Function name-             FilePath -> -- ^ Source file name-             Idris String+getClause :: Int      -- ^ line number that the type is declared on+          -> Name     -- ^ Function name+          -> FilePath -- ^ Source file name+          -> Idris String getClause l fn fp = do ty <- getInternalApp fp l-                       let ap = mkApp ty [1..]+                       ist <- get+                       let ap = mkApp ist ty []                        return (show fn ++ " " ++ ap ++                                    "= ?" ++ show fn ++ "_rhs")-   where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)-               = "x" ++ show n ++ " " ++ mkApp sc ns-         mkApp (PPi (Exp _ _ _ False) n _ sc) ns-               = show n ++ " " ++ mkApp sc ns-         mkApp (PPi _ _ _ sc) ns = mkApp sc ns-         mkApp _ _ = ""+   where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used+               = let n = getNameFrom i used ty in+                     show n ++ " " ++ mkApp i sc (n : used) +         mkApp i (PPi (Exp _ _ _ False) n _ sc) used +               = show n ++ " " ++ mkApp i sc (n : used) +         mkApp i (PPi _ _ _ sc) used = mkApp i sc used+         mkApp i _ _ = "" -getProofClause :: Int -> -- ^ Line type is declared on-                  Name -> -- ^ Function name-                  FilePath -> -- ^ Source file name-                  Idris String+         getNameFrom i used (PPi _ _ _ _) +              = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used+         getNameFrom i used (PApp fc f as) = getNameFrom i used f+         getNameFrom i used (PRef fc f) +            = case getNameHints i f of+                   [] -> uniqueName (UN "x") used+                   ns -> uniqueNameFrom (mkSupply ns) used+         getNameFrom i used _ = uniqueName (UN "x") used ++getProofClause :: Int      -- ^ line number that the type is declared+               -> Name     -- ^ Function name+               -> FilePath -- ^ Source file name+               -> Idris String getProofClause l fn fp                   = do ty <- getInternalApp fp l                        return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")@@ -292,16 +347,34 @@ -- match clause  mkWith :: String -> Name -> String-mkWith str n = let ind = getIndent str-                   str' = replicate ind ' ' ++-                          replaceRHS str "with (_)"-                   newpat = replicate (ind + 2) ' ' +++mkWith str n = let str' = replaceRHS str "with (_)"+                   newpat = "  " ++                             replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in                    str' ++ "\n" ++ newpat -   where getIndent s = length (takeWhile isSpace s)--         replaceRHS [] str = str+   where replaceRHS [] str = str          replaceRHS ('?':'=': rest) str = str-         replaceRHS ('=': rest) str = str+         replaceRHS ('=': rest) str +              | not ('=' `elem` rest) = str          replaceRHS (x : rest) str = x : replaceRHS rest str++-- Replace _ with names in missing clauses++nameMissing :: [PTerm] -> Idris [PTerm]+nameMissing ps = do ist <- get+                    newPats <- mapM nm ps+                    let newPats' = mergeAllPats ist (UN "_") (base (head ps))+                                                newPats+                    return (map fst newPats')+  where+    base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (UN "_")))) args)+    base t = t++    nm ptm = do mptm <- elabNewPat ptm+                case mptm of+                     Nothing -> return ptm+                     Just ptm' -> return ptm'+                       +++
src/Idris/Completion.hs view
@@ -38,6 +38,7 @@              , ("let", Nothing) -- FIXME syntax for let              , ("focus", Just ExprTArg)              , ("exact", Just ExprTArg)+             , ("equiv", Just ExprTArg)              , ("applyTactic", Just ExprTArg)              , ("reflect", Just ExprTArg)              , ("fill", Just ExprTArg)
src/Idris/Coverage.hs view
@@ -50,7 +50,7 @@         logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)         logLvl 10 $ show argss ++ "\n" ++ show all_args         logLvl 10 $ "Original: \n" ++-             showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True)) xs)+             showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)         -- add an infinite supply of explicit arguments to update the possible         -- cases for (the return type may be variadic, or function type, sp         -- there may be more case splitting that the idris_implicits record@@ -68,13 +68,13 @@         return new --         return (map (\t -> PClause n t [] PImpossible []) new)   where getLHS i term-            | (f, args) <- unApply term = map (\t -> delab' i t True) args+            | (f, args) <- unApply term = map (\t -> delab' i t True True) args             | otherwise = []          lhsApp (PClause _ _ l _ _ _) = l         lhsApp (PWith _ _ l _ _ _) = l -        noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of+        noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of                                           Right _ -> False                                           Left miss -> True) xs
src/Idris/DeepSeq.hs view
@@ -31,6 +31,7 @@         rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (MethodN x1) = rnf x1 `seq` ()         rnf (CaseN x1) = rnf x1 `seq` ()+        rnf (ElimN x1) = rnf x1 `seq` ()  instance NFData IntTy where         rnf (ITFixed x1) = rnf x1 `seq` ()@@ -163,6 +164,10 @@         rnf (CExport x1) = rnf x1 `seq` ()         rnf Reflection = ()         rnf (Specialise x1) = rnf x1 `seq` ()++instance NFData DataOpt where+        rnf Codata = ()+        rnf DefaultEliminator = ()  instance (NFData t) => NFData (PDecl' t) where         rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
src/Idris/Delaborate.hs view
@@ -14,21 +14,27 @@ bugaddr = "https://github.com/idris-lang/Idris-dev/issues"  delab :: IState -> Term -> PTerm-delab i tm = delab' i tm False+delab i tm = delab' i tm False False +delabMV :: IState -> Term -> PTerm+delabMV i tm = delab' i tm False True+ delabTy :: IState -> Name -> PTerm delabTy i n     = case lookupTy n (tt_ctxt i) of            (ty:_) -> case lookupCtxt n (idris_implicits i) of-                         (imps:_) -> delabTy' i imps ty False-                         _ -> delabTy' i [] ty False+                         (imps:_) -> delabTy' i imps ty False False+                         _ -> delabTy' i [] ty False False -delab' :: IState -> Term -> Bool -> PTerm-delab' i t f = delabTy' i [] t f+delab' :: IState -> Term -> Bool -> Bool -> PTerm+delab' i t f mvs = delabTy' i [] t f mvs  delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any-          -> Term -> Bool -> PTerm-delabTy' ist imps tm fullname = de [] imps tm+          -> Term +          -> Bool -- ^ use full names+          -> Bool -- ^ Don't treat metavariables specially+          -> PTerm+delabTy' ist imps tm fullname mvs = de [] imps tm   where     un = fileFC "(val)" @@ -84,11 +90,12 @@          | n == eqTy    = PEq un (de env [] l) (de env [] r)          | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder                                           (de env [] r)-    deFn env (P _ n _) args+    deFn env (P _ n _) args | not mvs          = case lookup n (idris_metavars ist) of                 Just (Just _, mi, _) ->                      mkMVApp (dens n) (drop mi (map (de env []) args))                 _ -> mkPApp (dens n) (map (de env []) args)+         | otherwise = mkPApp (dens n) (map (de env []) args)     deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))      mkMVApp n []@@ -147,6 +154,8 @@       let colour = idris_colourRepl i in           showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("             ++ showImp (Just i) imps colour (delab i ty) ++ ")"+pshow i (TooManyArguments f)+    = "Too many arguments for " ++ show f pshow i (CantIntroduce ty)     = let imps = opt_showimp (idris_options i) in       let colour = idris_colourRepl i in
src/Idris/ElabDecls.hs view
@@ -33,6 +33,12 @@ import Data.Maybe import Debug.Trace +import qualified Data.Map as Map+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty)+ recheckC fc env t     = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)          ctxt <- getContext@@ -143,9 +149,10 @@          -- remove it from the deferred definitions list          solveDeferred n -elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()-elabData info syn doc fc codata (PLaterdecl n t_in)-    = do iLOG (show (fc, doc))+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()+elabData info syn doc fc opts (PLaterdecl n t_in)+    = do let codata = Codata `elem` opts+         iLOG (show (fc, doc))          checkUndefined fc n          ctxt <- getContext          i <- getIState@@ -161,8 +168,9 @@          logLvl 2 $ "---> " ++ show cty          updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons -elabData info syn doc fc codata (PDatadecl n t_in dcons)-    = do iLOG (show fc)+elabData info syn doc fc opts (PDatadecl n t_in dcons)+    = do let codata = Codata `elem` opts+         iLOG (show fc)          undef <- isUndefined fc n          ctxt <- getContext          i <- getIState@@ -173,6 +181,9 @@                   (errAt "data declaration " n (erun fc (build i info False n t)))          def' <- checkDef fc defer          let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'+         -- if n is defined already, make sure it is just a type declaration+         -- with the same type we've just elaborated+         checkDefinedAs fc n t' (tt_ctxt i)          addDeferredTyCon def''          mapM_ (elabCaseBlock info []) is          (cty, _)  <- recheckC fc [] t'@@ -194,7 +205,17 @@          collapseCons n cons          updateContext (addDatatype (Data n ttag cty cons))          mapM_ (checkPositive n) cons+         if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty+                                          else return ()   where+        checkDefinedAs fc n t ctxt +            = case lookupDef n ctxt of+                   [] -> return ()+                   [TyDecl _ ty] -> +                      case converts ctxt [] t ty of+                           OK () -> return ()+                           _ -> tclift $ tfail (At fc (AlreadyDefined n))+                   _ -> tclift $ tfail (At fc (AlreadyDefined n))         -- parameters are names which are unchanged across the structure,         -- which appear exactly once in the return type of a constructor @@ -245,12 +266,252 @@                        | otherwise = count n ts         mParam args (_ : rest) = Nothing : mParam args rest +type EliminatorState = StateT (Map.Map String Int) Idris++-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()+elabEliminator paramPos n ty cons info = do+  elimLog $ "Elaborating eliminator"+  let (cnstrs, _) = splitPi ty+  let (splittedTy@(pms, idxs)) = splitPms cnstrs+  generalParams <- namePis False pms+  motiveIdxs    <- namePis False idxs+  let motive = mkMotive n paramPos generalParams motiveIdxs+  consTerms <- mapM (\(c@(_,cnm,_,_)) -> do+                              name <- freshName $ "elim_" ++ simpleName cnm+                              consTerm <- extractConsTerm c generalParams+                              return (name, expl, consTerm)) cons+  scrutineeIdxs <- namePis False idxs+  let motiveConstr = [(motiveName, expl, motive)]+  let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))+  let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))+  let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy+  let clauseConsElimArgs = map getPiName consTerms+  let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs+  let clauseGeneralArgs  = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'+  let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy+  eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)+  let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses+  elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef+  Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())+  -- Do not elaborate clauses if there aren't any+  case eliminatorClauses of+    [] -> return ()+    _  -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())+  where elimLog :: String -> EliminatorState ()+        elimLog s = Control.Monad.State.lift (logLvl 2 s)++        elimFC :: FC+        elimFC = fileFC "(eliminator)"++        elimDeclName :: Name+        elimDeclName = SN $ ElimN n++        applyNS :: Name -> [String] -> Name+        applyNS n []  = n+        applyNS n ns  = NS n ns++        splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)+        splitPi = splitPi' []+          where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)+                splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr+                splitPi' acc t                  = (reverse acc, t)++        splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])+        splitPms cnstrs = (map fst pms, map fst idxs)+           where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])++        isMachineGenerated :: Name -> Bool+        isMachineGenerated (MN _ _) = True+        isMachineGenerated _        = False++        namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]+        namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms+                                 let oldNames = map fst names+                                 let params   = map snd names+                                 return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params++        mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))+        mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))+        mkPiName _ (oldName, pl, piarg) =  do name <- freshName $ keyOf piarg+                                              return (oldName, (name, pl, piarg))+          where keyOf :: PTerm -> String+                keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"+                keyOf (PApp _ tyf _) = keyOf tyf+                keyOf PType = "ty__"+                keyOf _     = "carg__"+                nameStart :: Name -> Char+                nameStart n = nameStart' (simpleName n)+                  where nameStart' :: String -> Char+                        nameStart' "" = ' '+                        nameStart' ns = head ns++        simpleName :: Name -> String+        simpleName (NS n _) = simpleName n+        simpleName (MN i n) = n ++ show i+        simpleName n        = show n++        nameSpaces :: Name -> [String]+        nameSpaces (NS _ ns) = ns+        nameSpaces _         = []++        freshName :: String -> EliminatorState Name+        freshName key = do+          nameMap <- get+          let i = fromMaybe 0 (Map.lookup key nameMap)+          let name = key ++ show i ++ "__"+          put $ Map.insert key (i+1) nameMap+          return (MN i name)++        scrutineeName :: Name+        scrutineeName = MN 0 "scrutinee"++        scrutineeArgName :: Name+        scrutineeArgName = MN 0 "scrutineeArg"++        motiveName :: Name+        motiveName = MN 0 "prop"++        mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm+        mkMotive n paramPos params indicies =+          let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))+          in piConstr (indicies ++ [scrutineeTy]) PType++        piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm+        piConstr [] ty = ty+        piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)++        interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]+        interlievePos idxs []     l2     i = l2+        interlievePos idxs l1     []     i = l1+        interlievePos idxs (x:xs) l2     i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))+        interlievePos idxs l1     (y:ys) i = y:(interlievePos idxs l1 ys (i+1))++        replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm+        replaceParams paramPos params cns =+          let (_, cnsResTy) = splitPi cns+          in case cnsResTy of+               PApp _ _ args ->+                let oldParams = paramNamesOf 0 paramPos args+                in removeParamPis oldParams params cns+               _ -> cns++        removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm+        removeParamPis oldParams params (PPi pl n tyb tyr) =+          case findIndex (== n) oldParams of+            Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))+            Just i  -> (removeParamPis oldParams params tyr)+        removeParamPis oldParams params (PRef _ n) = +          case findIndex (== n) oldParams of+               Nothing -> (PRef elimFC n)+               Just i  -> let (newname,_,_) = params !! i in (PRef elimFC (newname))+        removeParamPis oldParams params (PApp _ cns args) =+          PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args+            where replaceParamArgs :: [PArg] -> [PArg]+                  replaceParamArgs []          = []+                  replaceParamArgs (arg:args)  =+                    case extractName (getTm arg) of+                      []   -> arg:replaceParamArgs args+                      [n]  ->+                        case findIndex (== n) oldParams of+                          Nothing -> arg:replaceParamArgs args+                          Just i  -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args+        removeParamPis oldParams params t = t++        paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]+        paramNamesOf i paramPos []          = []+        paramNamesOf i paramPos (arg:args)  = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args++        extractName :: PTerm -> [Name]+        extractName (PRef _ n) = [n]+        extractName _          = []++        splitArgPms :: PTerm -> ([PTerm], [PTerm])+        splitArgPms (PApp _ f args) = splitArgPms' args+          where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])+                splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)+                    where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])+        splitArgPms _                 = ([],[])+++        implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]+        implicitIndexes (cns@(doc, cnm, ty, fc)) = do+          i <-  Control.Monad.State.lift getIState+          implargs' <- case lookupCtxt cnm (idris_implicits i) of+            [] -> do fail $ "Error while showing implicits for " ++ show cnm+            [args] -> do return args+            _ -> do fail $ "Ambigous name for " ++ show cnm+          let implargs = mapMaybe convertImplPi implargs'+          let (_, cnsResTy) = splitPi ty+          case cnsResTy of+             PApp _ _ args ->+              let oldParams = paramNamesOf 0 paramPos args+              in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs+             _ -> return implargs++        extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm+        extractConsTerm (doc, cnm, ty, fc) generalParameters = do+          let cons' = replaceParams paramPos generalParameters ty+          let (args, resTy) = splitPi cons'+          implidxs <- implicitIndexes (doc, cnm, ty, fc)+          consArgs <- namePis True args+          let recArgs = findRecArgs consArgs+          let recMotives = map applyRecMotive recArgs+          let (_, consIdxs) = splitArgPms resTy+          return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))+            where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)+                  applyRecMotive (n,_,ty)  = (MN 0 $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))+                      where (_, idxs) = splitArgPms ty++        findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]+        findRecArgs []                            = []+        findRecArgs (ty@(_,_,PRef _ tn):rs)            | simpleName tn == simpleName n = ty:findRecArgs rs+        findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs+        findRecArgs (ty:rs)                                                            = findRecArgs rs++        applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm+        applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)++        convertArg :: (Name, Plicity, PTerm) -> PArg+        convertArg (n, _, _)      = pexp (PRef elimFC n)++        applyMotive :: [PTerm] -> PTerm -> PTerm+        applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])++        getPiName :: (Name, Plicity, PTerm) -> Name+        getPiName (name,_,_) = name++        convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)+        convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)+        convertImplPi _                             = Nothing++        generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause+        generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do+          let cons' = replaceParams paramPos generalParameters ty+          let (args, resTy) = splitPi cons'+          i <- Control.Monad.State.lift getIState+          implidxs <- implicitIndexes (doc, cnm, ty, fc)+          let (_, generalIdxs') = splitArgPms resTy+          let generalIdxs = map pexp generalIdxs'+          consArgs <- namePis True args+          let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])+          let recArgs = findRecArgs consArgs+          let recElims = map applyRecElim recArgs+          let rhsExpr    = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)+          return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []+            where applyRecElim :: (Name, Plicity, PTerm) -> PArg+                  applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])+                    where (_, idxs) = splitArgPms recTy+ -- | Elaborate primitives  elabPrims :: Idris () elabPrims = do mapM_ (elabDecl EAll toplevel)-                     (map (PData "" defaultSyntax (fileFC "builtin") False)-                         [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])+                     (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)+                        (zip+                         [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]+                         [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))+               elabDecl EAll toplevel elimDecl                mapM_ elabPrim primitives                -- Special case prim__believe_me because it doesn't work on just constants                elabBelieveMe@@ -400,7 +661,7 @@ elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->               PTerm -> String -> Name -> PTerm -> Idris () elabRecord info syn doc fc tyn ty cdoc cn cty-    = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])+    = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])          cty' <- implicit syn cn cty          i <- getIState          cty <- case lookupTy cn (tt_ctxt i) of@@ -638,7 +899,7 @@                 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats                 _ -> return () -           let optpdef = map debind optpats -- $ map (simple_lhs (tt_ctxt ist)) optpats+           let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats            tree@(CaseDef scargs sc _) <- tclift $                    simpleCase tcase False reflect CompileTime fc pdef            cov <- coverage@@ -728,7 +989,7 @@                [] -> return ()            return ()   where-    noMatch i cs tm = all (\x -> case matchClause i (delab' i x True) tm of+    noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of                                       Right _ -> False                                       Left miss -> True) cs @@ -918,15 +1179,27 @@ --                   b <- inferredDiff fc (delab' i lhs_tm True) lhs --                   return (not b) -- then return (Just lhs_tm) else return Nothing --                   trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)-            err@(Error _) -> return False+            Error err -> return (impossibleError err)+    where impossibleError (CantUnify _ topx topy e _ _) +              = not (sameFam topx topy || not (impossibleError e))+          impossibleError (CantConvert _ _ _) = False+          impossibleError (At _ e) = impossibleError e+          impossibleError (Elaborating _ _ e) = impossibleError e+          impossibleError _ = True +          sameFam topx topy +              = case (unApply topx, unApply topy) of+                     ((P _ x _, _), (P _ y _, _)) -> x == y+                     _ -> False+ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->               Idris (Either Term (Term, Term)) elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])    = do let tcgen = Dictionary `elem` opts         b <- checkPossible info fc tcgen fname lhs_in         case b of-            True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"+            True -> tclift $ tfail (At fc +                                (Msg $ show lhs_in ++ " is a valid case"))             False -> do ptm <- mkPatTm lhs_in                         return (Left ptm) elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)@@ -960,9 +1233,11 @@          (clhs_c, clhsty) <- recheckC fc [] lhs_tm         let clhs = normalise ctxt [] clhs_c+        +        logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs)) -        addInternalApp (fc_fname fc) (fc_line fc) (delab i clhs)-        addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i clhs))+        addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)+        addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))          logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)         -- Elaborate where block@@ -1023,7 +1298,7 @@             OK _ -> return ()             Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))         i <- getIState-        checkInferred fc (delab' i crhs True) rhs+        checkInferred fc (delab' i crhs True True) rhs         return $ Right (clhs, crhs)   where     decorate (NS x ns)@@ -1284,7 +1559,7 @@          let cons = [("", cn, cty, fc)]          let ddecl = PDatadecl tn tty cons          logLvl 5 $ "Class data " ++ showDImp True ddecl-         elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl+         elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl          -- for each constraint, build a top level function to chase it          logLvl 5 $ "Building functions"          let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps@@ -1707,7 +1982,7 @@          elabRecord info s doc f tyn ty cdoc cn cty   | otherwise     = do iLOG $ "Elaborating [type of] " ++ show tyn-         elabData info s doc f False (PLaterdecl tyn ty)+         elabData info s doc f [] (PLaterdecl tyn ty) elabDecl' _ info (PDSL n dsl)     = do i <- getIState          putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
src/Idris/ElabTerm.hs view
@@ -47,14 +47,16 @@          when (not pattern) $               mapM_ (\n -> when (n `elem` hs) $                              do focus n-                                try (resolveTC 7 fn ist)+                                g <- goal+                                try (resolveTC 7 g fn ist)                                     (movelast n)) ivs          ivs <- get_instances          hs <- get_holes          when (not pattern) $               mapM_ (\n -> when (n `elem` hs) $                              do focus n-                                resolveTC 7 fn ist) ivs+                                g <- goal+                                resolveTC 7 g fn ist) ivs          tm <- get_term          ctxt <- get_context          when (not pattern) $ do matchProblems; unifyProblems@@ -150,12 +152,12 @@                                    (elab' ina (PRef fc unitTy))     elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)     elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes-       = resolveTC 5 fn ist+       = do g <- goal; resolveTC 5 g fn ist     elab' ina (PResolveTC fc)         | True = do c <- unique_hole (MN 0 "class")                     instanceArg c         | otherwise = do g <- goal-                         try (resolveTC 2 fn ist)+                         try (resolveTC 2 g fn ist)                           (do c <- unique_hole (MN 0 "class")                               instanceArg c)     elab' ina (PRefl fc t)@@ -414,7 +416,7 @@                                         hs <- get_holes                                         if all (\n -> not (n `elem` hs)) (freeNames g)                                         -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))-                                         then try (resolveTC 7 fn ist)+                                         then try (resolveTC 7 g fn ist)                                                   (movelast n)                                          else movelast n)                               (ivs' \\ ivs)@@ -649,10 +651,10 @@     = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist  -resolveTC :: Int -> Name -> IState -> ElabD ()-resolveTC 0 fn ist = fail $ "Can't resolve type class"-resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True-resolveTC depth fn ist+resolveTC :: Int -> Term -> Name -> IState -> ElabD ()+resolveTC 0 topg fn ist = fail $ "Can't resolve type class"+resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True+resolveTC depth topg fn ist       = do hnf_compute            g <- goal            ptm <- get_term@@ -701,7 +703,7 @@      blunderbuss t d [] = do -- c <- get_env                             -- ps <- get_probs-                            lift $ tfail $ CantResolve t+                            lift $ tfail $ CantResolve topg     blunderbuss t d (n:ns)         | n /= fn && tcname n = try' (resolve n d)                                      (blunderbuss t d ns) True@@ -729,7 +731,7 @@                                      t' <- goal                                      let (tc', ttype) = unApply t'                                      let depth' = if t == t' then depth - 1 else depth-                                     resolveTC depth' fn ist)+                                     resolveTC depth' topg fn ist)                       (filter (\ (x, y) -> not x) (zip (map fst imps) args))                 -- if there's any arguments left, we've failed to resolve                 hs <- get_holes
src/Idris/IBC.hs view
@@ -23,7 +23,7 @@ import Paths_idris  ibcVersion :: Word8-ibcVersion = 44+ibcVersion = 46  data IBCFile = IBCFile { ver :: Word8,                          sourcefile :: FilePath,@@ -51,7 +51,8 @@                          ibc_docstrings :: [(Name, String)],                          ibc_transforms :: [(Term, Term)],                          ibc_coercions :: [Name],-                         ibc_lineapps :: [(FilePath, Int, PTerm)]+                         ibc_lineapps :: [(FilePath, Int, PTerm)],+                         ibc_namehints :: [(Name, Name)]                        }    deriving Show {-!@@ -59,7 +60,7 @@ !-}  initIBC :: IBCFile-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []  loadIBC :: FilePath -> Idris () loadIBC fp = do iLOG $ "Loading ibc " ++ fp@@ -137,6 +138,8 @@ ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f } ibc i (IBCLineApp fp l t) f      = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }+ibc i (IBCNameHint (n, ty)) f+     = return f { ibc_namehints = (n, ty) : ibc_namehints f }  process :: IBCFile -> FilePath -> Idris () process i fn@@ -172,6 +175,7 @@                pCoercions (ibc_coercions i)                pTrans (ibc_transforms i)                pLineApps (ibc_lineapps i)+               pNameHints (ibc_namehints i)  timestampOlder :: FilePath -> FilePath -> IO () timestampOlder src ibc = do srct <- getModificationTime src@@ -319,6 +323,9 @@ pLineApps :: [(FilePath, Int, PTerm)] -> Idris () pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls +pNameHints :: [(Name, Name)] -> Idris ()+pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns+ ----- Generated by 'derive'  instance Binary SizeChange where@@ -410,6 +417,7 @@                 MethodN x1 -> do putWord8 3                                  put x1                 CaseN x1 -> do putWord8 4; put x1+                ElimN x1 -> do putWord8 5; put x1         get           = do i <- getWord8                case i of@@ -427,6 +435,8 @@                            return (MethodN x1)                    4 -> do x1 <- get                            return (CaseN x1)+                   5 -> do x1 <- get+                           return (ElimN x1)                    _ -> error "Corrupted binary data for SpecialName"  @@ -870,7 +880,7 @@                    _ -> error "Corrupted binary data for Totality"  instance Binary IBCFile where-        put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)+        put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)          = {-# SCC "putIBCFile" #-}             do put x1                put x2@@ -899,6 +909,7 @@                put x25                put x26                put x27+               put x28         get           = do x1 <- get                if x1 == ibcVersion then@@ -928,8 +939,18 @@                     x25 <- get                     x26 <- get                     x27 <- 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 x24 x25 x26 x27)+                    x28 <- 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 x24 x25 x26 x27 x28)                   else return (initIBC { ver = x1 })++instance Binary DataOpt where+  put x = case x of+    Codata -> putWord8 0+    DefaultEliminator -> putWord8 1+  get = do i <- getWord8+           case i of+            0 -> return Codata+            1 -> return DefaultEliminator  instance Binary FnOpt where         put x
src/Idris/ParseData.hs view
@@ -70,13 +70,19 @@ {- | Parses data declaration type (normal or codata) DataI ::= 'data' | 'codata'; -}-dataI :: IdrisParser Bool-dataI = do reserved "data"; return False-    <|> do reserved "codata"; return True+dataI :: IdrisParser DataOpts+dataI = do reserved "data"; return []+    <|> do reserved "codata"; return [Codata] +{- | Parses if a data should not have a default eliminator +DefaultEliminator ::= 'noelim'?+ -}+defaultEliminator :: IdrisParser DataOpts+defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])+ {- | Parses a data type declaration-Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?-       | DocComment? Accessibility? DataI FnName Name*   DataRest?+Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?+       | DocComment? Accessibility? DataI DefaultEliminator FnName Name*   DataRest?        ; Constructor' ::= Constructor KeepTerminator; ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;@@ -90,29 +96,31 @@   ; -} data_ :: SyntaxInfo -> IdrisParser PDecl-data_ syn = do (doc, acc, co) <- try (do+data_ syn = do (doc, acc, dataOpts) <- try (do                     doc <- option "" (docComment '|')                     pushIndent                     acc <- optional accessibility+                    elim <- defaultEliminator                     co <- dataI-                    return (doc, acc, co))+                    let dataOpts = combineDataOpts(elim ++ co)+                    return (doc, acc, dataOpts))                fc <- getFC                tyn_in <- fnName                (do try (lchar ':')                    popIndent                    ty <- typeExpr (allowImp syn)                    let tyn = expandNS syn tyn_in-                   option (PData doc syn fc co (PLaterdecl tyn ty)) (do+                   option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do                      reserved "where"                      cons <- indentedBlock (constructor syn)                      accData acc tyn (map (\ (_, n, _, _) -> n) cons)-                     return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do+                     return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do                     args <- many name                     let ty = bindArgs (map (const PType) args) PType                     let tyn = expandNS syn tyn_in-                    option (PData doc syn fc co (PLaterdecl tyn ty)) (do+                    option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do                       try (lchar '=') <|> do reserved "where"-                                             let kw = (if co then "co" else "") ++ "data "+                                             let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "                                              let n  = show tyn_in ++ " "                                              let s  = kw ++ n                                              let as = concat (intersperse " " $ map show args) ++ " "@@ -129,14 +137,16 @@                                    do let cty = bindArgs cargs conty                                       return (doc, x, cty, cfc)) cons                       accData acc tyn (map (\ (_, n, _, _) -> n) cons')-                      return $ PData doc syn fc co (PDatadecl tyn ty cons')))+                      return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))            <?> "data type declaration"   where     mkPApp :: FC -> PTerm -> [PTerm] -> PTerm     mkPApp fc t [] = t     mkPApp fc t xs = PApp fc t (map pexp xs)     bindArgs :: [PTerm] -> PTerm -> PTerm-    bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs+    bindArgs xs t = foldr (PPi expl (MN 0 "_t")) t xs+    combineDataOpts :: DataOpts -> DataOpts+    combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts   {- | Parses a type constructor declaration
src/Idris/ParseExpr.hs view
@@ -42,8 +42,10 @@ disallowImp :: SyntaxInfo -> SyntaxInfo disallowImp syn = syn { implicitAllowed = False } -{- | Parses an expression as a whole+{-| Parses an expression as a whole+@   FullExpr ::= Expr EOF_t;+@  -} fullExpr :: SyntaxInfo -> IdrisParser PTerm fullExpr syn = do x <- expr syn@@ -53,7 +55,9 @@   {- |Parses an expression+@   Expr ::= Expr';+@ -} expr :: SyntaxInfo -> IdrisParser PTerm expr syn = do i <- get@@ -61,10 +65,10 @@  {- | Parses either an internally defined expression or     a user-defined one-+@ Expr' ::=  "External (User-defined) Syntax"       |   InternalExpr;-+@  -} expr' :: SyntaxInfo -> IdrisParser PTerm expr' syn =     try (externalExpr syn)@@ -92,7 +96,7 @@         _ -> False     isSimple _ = False -{- | Tries to parse a user-defined expression given a list of syntactic extensions -}+{- | Tries to parse a user-defined expression given a list of syntactic extensions -} extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm extensions syn rules = choice (map (try . extension syn) (filter isValid rules))                        <?> "user-defined expression"@@ -160,8 +164,8 @@     update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)     update ns t = t -{- |Parses a (normal) built-in expression-+{- | Parses a (normal) built-in expression+@ InternalExpr ::=   App   | MatchApp@@ -173,8 +177,9 @@   | Let   | RewriteTerm   | Pi-  | DoBlock+  | DoBlock   ;+@ -} internalExpr :: SyntaxInfo -> IdrisParser PTerm internalExpr syn =@@ -193,8 +198,10 @@      <?> "expression"  {- | Parses a case expression+@ CaseExpr ::=   'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;+@ -} caseExpr :: SyntaxInfo -> IdrisParser PTerm caseExpr syn = do reserved "case"; fc <- getFC@@ -204,9 +211,11 @@                <?> "case expression"  {- | Parses a case in a case expression+@ CaseOption ::=   Expr '=>' Expr Terminator   ;+@ -} caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm) caseOption syn = do lhs <- expr (syn { inPattern = True })@@ -215,9 +224,11 @@                  <?> "case option"  {- | Parses a proof block+@ ProofExpr ::=   'proof' OpenBlock Tactic'* CloseBlock   ;+@ -} proofExpr :: SyntaxInfo -> IdrisParser PTerm proofExpr syn = do reserved "proof"@@ -225,10 +236,12 @@                    return $ PProof ts                 <?> "proof block" -{- | Parses a tactics block+{- | Parses a tactics block+@ TacticsExpr :=   'tactics' OpenBlock Tactic'* CloseBlock ;+@ -} tacticsExpr :: SyntaxInfo -> IdrisParser PTerm tacticsExpr syn = do reserved "tactics"@@ -236,7 +249,8 @@                      return $ PTactics ts                   <?> "tactics block" -{- | Parses a simple expresion+{- | Parses a simple expression+@ SimpleExpr ::=   '![' Term ']'   | '?' Name@@ -257,6 +271,7 @@   | '_'   | {- External (User-defined) Simple Expression -}   ;+@ -} simpleExpr :: SyntaxInfo -> IdrisParser PTerm simpleExpr syn =@@ -267,6 +282,7 @@                tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';                                             return t)                return (PRefl fc tm)+        <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))         <|> proofExpr syn         <|> tacticsExpr syn         <|> caseExpr syn@@ -295,7 +311,8 @@         <?> "expression"  -{- |Parses the rest of an expression in braces+{- |Parses the rest of an expression in braces+@ Bracketed ::=   ')'   | Expr ')'@@ -305,6 +322,7 @@   | Expr Operator ')'   | Name ':' Expr '**' Expr ')'   ;+@ -} bracketed :: SyntaxInfo -> IdrisParser PTerm bracketed syn =@@ -377,15 +395,17 @@ modifyConst syn fc x = x  {- | Parses a list literal expression e.g. [1,2,3]+@ ListExpr ::=   '[' ExprList? ']' ;-+@+@ ExprList ::=   Expr   | Expr ',' ExprList   ;-+@  -} listExpr :: SyntaxInfo -> IdrisParser PTerm listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'@@ -398,22 +418,26 @@   {- | Parses an alternative expression+@   Alt ::= '(|' Expr_List '|)';    Expr_List ::=     Expr'     | Expr' ',' Expr_List   ;+@ -} alt :: SyntaxInfo -> IdrisParser PTerm alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"              return (PAlternative False alts)  {- | Parses a possibly hidden simple expression+@ HSimpleExpr ::=   '.' SimpleExpr   | SimpleExpr   ;+@ -} hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm hsimpleExpr syn =@@ -424,9 +448,11 @@   <?> "expression"  {- | Parses a matching application expression+@ MatchApp ::=   SimpleExpr '<==' FnName   ;+@ -} matchApp :: SyntaxInfo -> IdrisParser PTerm matchApp syn = do ty <- simpleExpr syn@@ -451,9 +477,11 @@                <?> "unification log expression"  {- | Parses a no implicits expression+@ NoImplicits ::=   '%' 'noImplicits' SimpleExpr   ;+@ -} noImplicits :: SyntaxInfo -> IdrisParser PTerm noImplicits syn = do lchar '%'; reserved "noImplicits";@@ -462,10 +490,12 @@                  <?> "no implicits expression"  {- | Parses a function application expression+@ App ::=   'mkForeign' Arg Arg*   | SimpleExpr Arg+   ;+@ -} app :: SyntaxInfo -> IdrisParser PTerm app syn = do f <- reserved "mkForeign"@@ -499,12 +529,14 @@             = desugar (syn { dsl_info = d }) i (getTm a)     dslify i t = t -{- |Parses a function argument+{-| Parses a function argument+@ Arg ::=   ImplicitArg   | ConstraintArg   | SimpleExpr   ;+@ -} arg :: SyntaxInfo -> IdrisParser PArg arg syn =  implicitArg syn@@ -513,10 +545,12 @@               return (pexp e)        <?> "function argument" -{- |Parses an implicit function argument+{-| Parses an implicit function argument+@ ImplicitArg ::=   '{' Name ('=' Expr)? '}'   ;+@ -} implicitArg :: SyntaxInfo -> IdrisParser PArg implicitArg syn = do lchar '{'@@ -528,10 +562,12 @@                      return (pimp n v False)                   <?> "implicit function argument" -{- |Parses a constraint argument (for selecting a named type class instance)-ConstraintArg ::=-  '@{' Expr '}'-  ;+{-| Parses a constraint argument (for selecting a named type class instance)++>    ConstraintArg ::=+>      '@{' Expr '}'+>      ;+ -} constraintArg :: SyntaxInfo -> IdrisParser PArg constraintArg syn = do symbol "@{"@@ -541,18 +577,22 @@                     <?> "constraint argument"  -{- |Parses a record field setter expression+{-| Parses a record field setter expression+@ RecordType ::=   'record' '{' FieldTypeList '}';-+@+@ FieldTypeList ::=   FieldType   | FieldType ',' FieldTypeList   ;-+@+@ FieldType ::=   FnName '=' Expr   ;+@ -} recordType :: SyntaxInfo -> IdrisParser PTerm recordType syn@@ -579,17 +619,21 @@          applyAll fc ((n, e) : es) x             = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x]) -{- |Creates setters for record types on necessary functions -}+-- | Creates setters for record types on necessary functions mkType :: Name -> Name mkType (UN n) = UN ("set_" ++ n) mkType (MN 0 n) = MN 0 ("set_" ++ n) mkType (NS n s) = NS (mkType n) s -{- |Parses a type signature+{- | Parses a type signature+@ TypeSig ::=   ':' Expr   ;+@+@ TypeExpr ::= ConstraintList? Expr;+@  -} typeExpr :: SyntaxInfo -> IdrisParser PTerm typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []@@ -597,15 +641,19 @@                   return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)                <?> "type signature" -{- |Parses a lambda expression+{- | Parses a lambda expression+@ Lambda ::=     '\\' TypeOptDeclList '=>' Expr   | '\\' SimpleExprList  '=>' Expr   ;+@+@ SimpleExprList ::=   SimpleExpr   | SimpleExpr ',' SimpleExprList   ;+@ -} lambda :: SyntaxInfo -> IdrisParser PTerm lambda syn = do lchar '\\'@@ -627,10 +675,12 @@                         (PCase fc (PRef fc (MN i "lamp"))                                 [(x, pmList xs sc)]) -{- |Parses a term rewrite expression+{- | Parses a term rewrite expression+@ RewriteTerm ::=   'rewrite' Expr ('==>' Expr)? 'in' Expr   ;+@ -} rewriteTerm :: SyntaxInfo -> IdrisParser PTerm rewriteTerm syn = do reserved "rewrite"@@ -644,6 +694,7 @@                   <?> "term rewrite expression"  {- |Parses a let binding+@ Let ::=   'let' Name TypeSig'? '=' Expr  'in' Expr | 'let' Expr'          '=' Expr' 'in' Expr@@ -651,6 +702,7 @@ TypeSig' ::=   ':' Expr'   ;+@  -} let_ :: SyntaxInfo -> IdrisParser PTerm let_ syn = try (do reserved "let"; n <- name;@@ -665,10 +717,13 @@                    return (PCase fc v [(pat, sc)]))            <?> "let binding" -{- |Parses a quote goal+{- | Parses a quote goal++@ QuoteGoal ::=   'quoteGoal' Name 'by' Expr 'in' Expr   ;+@  -} quoteGoal :: SyntaxInfo -> IdrisParser PTerm quoteGoal syn = do reserved "quoteGoal"; n <- name;@@ -680,13 +735,15 @@                    return (PGoal fc r n sc)                 <?> "quote goal expression" -{- |Parses a dependent type signature+{- | Parses a dependent type signature+@ Pi ::=     '|'? Static? '('           TypeDeclList ')' DocComment '->' Expr   | '|'? Static? '{'           TypeDeclList '}'            '->' Expr   |              '{' 'auto'    TypeDeclList '}'            '->' Expr   |              '{' 'default' TypeDeclList '}'            '->' Expr   ;+@  -}  pi :: SyntaxInfo -> IdrisParser PTerm@@ -728,10 +785,13 @@   <?> "dependent type signature"  {- | Parses a type constraint list++@ ConstraintList ::=     '(' Expr_List ')' '=>'   | Expr              '=>'   ;+@ -} constraintList :: SyntaxInfo -> IdrisParser [PTerm] constraintList syn = try (do lchar '('@@ -745,16 +805,20 @@                  <|> return []                  <?> "type constraint list" -{- |Parses a type declaration list+{- | Parses a type declaration list+@ TypeDeclList ::=     FunctionSignatureList   | NameList TypeSig   ;+@ +@ FunctionSignatureList ::=     Name TypeSig   | Name TypeSig ',' FunctionSignatureList   ;+@ -} typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)] typeDeclList syn = try (sepBy1 (do x <- fnName@@ -768,13 +832,17 @@                           return (map (\x -> (x, t)) ns)                    <?> "type declaration list" -{- |Parses a type declaration list with optional parameters+{- | Parses a type declaration list with optional parameters+@ TypeOptDeclList ::=     NameOrPlaceholder TypeSig?   | NameOrPlaceholder TypeSig? ',' TypeOptDeclList   ;+@ +@ NameOrPlaceHolder ::= Name | '_';+@ -} tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)] tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder@@ -789,13 +857,17 @@                                   return (MN 0 "underscore")                            <?> "name or placeholder" -{- |Parses a list comprehension+{- | Parses a list comprehension+@ Comprehension ::= '[' Expr '|' DoList ']';+@ +@ DoList ::=     Do   | Do ',' DoList   ;+@ -} comprehension :: SyntaxInfo -> IdrisParser PTerm comprehension syn@@ -814,12 +886,16 @@                                                     [pexp e])           addGuard x = x -{- |Parses a do-block+{- | Parses a do-block+@ Do' ::= Do KeepTerminator;+@ +@ DoBlock ::=   'do' OpenBlock Do'+ CloseBlock   ;+@  -} doBlock :: SyntaxInfo -> IdrisParser PTerm doBlock syn@@ -828,7 +904,8 @@          return (PDoBlock ds)       <?> "do block" -{- |Parses an expression inside a do block+{- | Parses an expression inside a do block+@ Do ::=     'let' Name  TypeSig'?      '=' Expr   | 'let' Expr'                '=' Expr@@ -836,6 +913,7 @@   | Expr' '<-' Expr   | Expr   ;+@ -} do_ :: SyntaxInfo -> IdrisParser PDo do_ syn@@ -868,8 +946,10 @@           return (DoExp fc e)    <?> "do block expression" -{- |Parses an expression in idiom brackets+{- | Parses an expression in idiom brackets+@ Idiom ::= '[|' Expr '|]';+@ -} idiom :: SyntaxInfo -> IdrisParser PTerm idiom syn@@ -881,6 +961,8 @@       <?> "expression in idiom brackets"  {- |Parses a constant or literal expression++@ Constant ::=     'Integer'   | 'Int'@@ -901,6 +983,7 @@   | String_t   | Char_t   ;+@ -} constant :: IdrisParser Core.TT.Const constant =  do reserved "Integer";return (AType (ATInt ITBig))@@ -923,17 +1006,22 @@         <|> try (do c <- charLiteral;   return $ Ch c)         <?> "constant or literal" -{- |Parses a static modifier+{- | Parses a static modifier++@ Static ::=   '[' static ']' ;+@ -} static :: IdrisParser Static static =     do lchar '['; reserved "static"; lchar ']'; return Static          <|> return Dynamic          <?> "static modifier" -{- | Parses a tactic script+{- | Parses a tactic script++@ Tactic ::= 'intro' NameList?        |   'intros'        |   'refine'      Name Imp+@@ -967,7 +1055,7 @@     Tactic ';' Tactic   | Tactic ';' TacticSeq   ;-+@ -}  tactic :: SyntaxInfo -> IdrisParser PTactic@@ -1040,7 +1128,7 @@     mergeSeq [t]    = t     mergeSeq (t:ts) = TSeq t (mergeSeq ts) -{- | Parses a tactic as a whole -}+-- | Parses a tactic as a whole fullTactic :: SyntaxInfo -> IdrisParser PTactic fullTactic syn = do t <- tactic syn                     eof
src/Idris/ParseOps.hs view
@@ -29,8 +29,8 @@ import qualified Data.Text as T import qualified Data.ByteString.UTF8 as UTF8 -{- |Creates table for fixity declarations to build expression parser using-  pre-build and user-defined operator/fixity declarations -}+-- | Creates table for fixity declarations to build expression parser+-- using pre-build and user-defined operator/fixity declarations table :: [FixDecl] -> OperatorTable IdrisParser PTerm table fixes    = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))@@ -40,7 +40,7 @@        [binary "="  PEq AssocLeft],        [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]] -{- |Calculates table for fixtiy declarations -}+-- | Calculates table for fixtiy declarations toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm toTable fs = map (map toBin)                  (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)@@ -52,20 +52,20 @@          assoc (Infixr _) = AssocRight          assoc (InfixN _) = AssocNone -{- |Binary operator -}+-- | Binary operator binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm binary name f = Infix (do fc <- getFC                           reservedOp name                           doc <- option "" (docComment '^')                           return (f fc)) -{- |Prefix operator -}+-- | Prefix operator prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm prefix name f = Prefix (do reservedOp name                            fc <- getFC                            return (f fc)) -{- |Backtick operator -}+-- | Backtick operator backtick :: Operator IdrisParser PTerm backtick = Infix (do lchar '`'; n <- fnName                      lchar '`'@@ -75,22 +75,29 @@ {- | Parses an operator in function position i.e. enclosed by `()', with an  optional namespace +@   OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';+@+ -} operatorFront :: IdrisParser Name operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []  {- | Parses a function (either normal name or operator)-  FnName ::= Name | OperatorFront;++@+  FnName ::= Name | OperatorFront;+@ -} fnName :: IdrisParser Name fnName = try operatorFront <|> name <?> "function name"  {- | Parses a fixity declaration-+@ Fixity ::=   FixityType Natural_t OperatorList Terminator   ;+@ -} fixity :: IdrisParser PDecl fixity = do pushIndent@@ -121,12 +128,14 @@                    extractName (Fix _ n) = n  {- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)-FixityType ::=-  'infixl'-  | 'infixr'-  | 'infix'-  | 'prefix'-  ;+@+    FixityType ::=+      'infixl'+      | 'infixr'+      | 'infix'+      | 'prefix'+      ;+@  -} fixityType :: IdrisParser (Int -> Fixity) fixityType = do reserved "infixl"; return Infixl
src/Idris/Parser.hs view
@@ -797,6 +797,7 @@            |   'default'  Totality            |   'logging'  Natural            |   'dynamic'  StringList+           |   'name'     Name NameList            |   'language' 'TypeProviders'            |   'language' 'ErrorReflection'            ;@@ -839,6 +840,12 @@                                              Left lib -> addIBC (IBCDyLib (lib_name lib))                                              Right msg ->                                                  fail $ msg)]+             <|> do try (lchar '%' *> reserved "name")+                    ty <- iName []+                    ns <- sepBy1 name (lchar ',')+                    return [PDirective +                               (do mapM_ (addNameHint ty) ns+                                   mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]               <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;                     return [PDirective (addLangExt ext)]              <?> "directive"@@ -1021,7 +1028,7 @@                                    f file pos                   unless (null ds') $ do                     let ds = namespaces mname ds'-                    logLvl 3 (dumpDecls ds)+                    logLvl 3 (showDecls True ds)                     i <- getIState                     logLvl 10 (show (toAlist (idris_implicits i)))                     logLvl 3 (show (idris_infixes i))@@ -1047,7 +1054,10 @@                     -- Redo totality check for deferred names                     let deftots = idris_defertotcheck i                     iLOG $ "Totality checking " ++ show deftots-                    mapM_ (\x -> setTotality x Unchecked) (map snd deftots)+                    mapM_ (\x -> do tot <- getTotality x+                                    case tot of+                                         Total _ -> setTotality x Unchecked+                                         _ -> return ()) (map snd deftots)                     mapM_ buildSCG deftots                     mapM_ checkDeclTotality deftots
src/Idris/REPL.hs view
@@ -629,7 +629,8 @@          extras <- case lookupCtxt n' (idris_patdefs i) of                        [] -> return ""-                       [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms+                       [(_, tms)] -> do tms' <- nameMissing tms+                                        showNew (show n ++ "_rhs") 1 indent tms'         let (nonblank, rest) = span (not . all isSpace) (tyline:later)         if updatefile           then do let fb = fn ++ "~"@@ -665,9 +666,12 @@ process h fn (MakeWith updatefile l n)    = do src <- runIO $ readFile fn         let (before, tyline : later) = splitAt (l-1) (lines src)+        let ind = getIndent tyline         let with = mkWith tyline n-        -- add clause before first blank line in 'later'-        let (nonblank, rest) = span (not . all isSpace) later+        -- add clause before first blank line in 'later',+        -- or (TODO) before first line with same indentation as tyline+        let (nonblank, rest) = span (\x -> not (all isSpace x) &&+                                           not (ind == getIndent x)) later         if updatefile then            do let fb = fn ++ "~"               runIO $ writeFile fb (unlines (before ++ nonblank)@@ -675,6 +679,8 @@                                     unlines rest)               runIO $ copyFile fb fn            else ihPrintResult h with+  where getIndent s = length (takeWhile isSpace s)+     process h fn (DoProofSearch updatefile l n hints)     = do src <- runIO $ readFile fn          let (before, tyline : later) = splitAt (l-1) (lines src)@@ -703,7 +709,7 @@          if updatefile then             do let fb = fn ++ "~"                runIO $ writeFile fb (unlines before ++-                                     updateMeta tyline (show n) newmv ++ "\n"+                                     updateMeta False tyline (show n) newmv ++ "\n"                                        ++ unlines later)                runIO $ copyFile fb fn             else ihPrintResult h newmv@@ -721,16 +727,22 @@           nsroot (SN (WhereN _ _ n)) = nsroot n           nsroot n = n -          updateMeta ('?':cs) n new+          updateMeta brack ('?':cs) n new             | length cs >= length n               = case splitAt (length n) cs of                      (mv, c:cs) ->                           if (isSpace c && mv == n)-                             then new ++ (c : cs)-                             else '?' : mv ++ c : updateMeta cs n new+                             then addBracket brack new ++ (c : cs)+                             else '?' : mv ++ c : updateMeta True cs n new                      (mv, []) -> if (mv == n) then new else '?' : mv-          updateMeta (c:cs) n new = c : updateMeta cs n new-          updateMeta [] n new = ""+          updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new+          updateMeta brack (c:cs) n new +              = c : updateMeta (not (not brack && isSpace c)) cs n new+          updateMeta brack [] n new = ""++          addBracket False new = new+          addBracket True new | any isSpace new = '(' : new ++ ")"+                              | otherwise = new  process h fn (Spec t)                     = do (tm, ty) <- elabVal toplevel False t
src/Pkg/Package.hs view
@@ -68,7 +68,7 @@           mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)  buildMods :: [Opt] -> [Name] -> IO ()-buildMods opts ns = do let f = map (toPath . show) ns+buildMods opts ns = do let f = map (toPath . showCG) ns --                        putStrLn $ "MODULE: " ++ show f                        idris (map Filename f ++ opts)                        return ()
test/test032/expected view
@@ -1,11 +1,14 @@ Type checking ./test032.idr isElem x [] = ?isElem_rhs_1-isElem x (_ :: _) = ?isElem_rhs_3+isElem x (y :: xs) = ?isElem_rhs_3 -   localZipWith f (_ :: _) (_ :: _) = ?localZipWith_rhs_1+   localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1  f x :: (map f xs) isElem2 x (y :: ys) with (_)   isElem2 x (y :: ys) | with_pat = ?isElem2_rhs   isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3++              [] => ?bar_1+              (x :: ys) => ?bar_2
test/test032/input view
@@ -3,3 +3,4 @@ :ps 21 maprhs :mw 25 isElem2 :cs 30 p+:cs 35 xs'
test/test032/test032.idr view
@@ -30,3 +30,6 @@   isElem3 x (y :: ys) | (Yes p) = ?isElem3_rhs_1   isElem3 x (y :: ys) | (No _) = ?isElem3_rhs_2 +foo : List a -> List a+foo xs = case xs of+              xs' => ?bar
− tutorial/examples/binary.idr 
@@ -1,62 +0,0 @@-module Main--data Binary : Nat -> Type where-    bEnd : Binary Z-    bO : Binary n -> Binary (n + n)-    bI : Binary n -> Binary (S (n + n))--instance Show (Binary n) where-    show (bO x) = show x ++ "0"-    show (bI x) = show x ++ "1"-    show bEnd = ""--data Parity : Nat -> Type where-   even : Parity (n + n)-   odd  : Parity (S (n + n))--parity : (n:Nat) -> Parity n-parity Z     = even {n=Z}-parity (S Z) = odd {n=Z}-parity (S (S k)) with (parity k)-    parity (S (S (j + j)))     | even ?= even {n=S j}-    parity (S (S (S (j + j)))) | odd  ?= odd {n=S j}--natToBin : (n:Nat) -> Binary n-natToBin Z = bEnd-natToBin (S k) with (parity k)-   natToBin (S (j + j))     | even  = bI (natToBin j)-   natToBin (S (S (j + j))) | odd  ?= bO (natToBin (S j))--intToNat : Int -> Nat-intToNat 0 = Z-intToNat x = if (x>0) then (S (intToNat (x-1))) else Z--main : IO ()-main = do putStr "Enter a number: "-          x <- getLine-          print (natToBin (fromInteger (cast x)))------------ Proofs ------------parity_lemma_1 = proof {-    intros;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--natToBin_lemma_1 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--parity_lemma_2 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}---
− tutorial/examples/bmain.idr 
@@ -1,8 +0,0 @@-module Main--import btree--main : IO ()-main = do let t = toTree [1,8,2,7,9,3]-          print (btree.toList t)-
− tutorial/examples/btree.idr 
@@ -1,18 +0,0 @@-module btree--data BTree a = Leaf-             | Node (BTree a) a (BTree a)--insert : Ord a => a -> BTree a -> BTree a-insert x Leaf = Node Leaf x Leaf-insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)-                                   else (Node l v (insert x r))--toList : BTree a -> List a-toList Leaf = []-toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)--toTree : Ord a => List a -> BTree a-toTree [] = Leaf-toTree (x :: xs) = insert x (toTree xs)-
− tutorial/examples/classes.idr 
@@ -1,10 +0,0 @@-m_add : Maybe Int -> Maybe Int -> Maybe Int-m_add x y = do x' <- x -- Extract value from x-               y' <- y -- Extract value from y-               return (x' + y') -- Add them--m_add' : Maybe Int -> Maybe Int -> Maybe Int-m_add' x y = [ x' + y' | x' <- x, y' <- y ]--sortAndShow : (Ord a, Show a) => List a -> String-sortAndShow xs = show (sort xs)
− tutorial/examples/foo.idr 
@@ -1,10 +0,0 @@-module foo--namespace x-  test : Int -> Int-  test x = x * 2--namespace y-  test : String -> String-  test x = x ++ x-
− tutorial/examples/hello.idr 
@@ -1,5 +0,0 @@-module Main--main : IO ()-main = putStrLn "Hello world"-
− tutorial/examples/idiom.idr 
@@ -1,38 +0,0 @@-module idiom--data Expr = Var String-          | Val Int-          | Add Expr Expr--data Eval : Type -> Type where-   MkEval : (List (String, Int) -> Maybe a) -> Eval a--fetch : String -> Eval Int-fetch x = MkEval (\e => fetchVal e) where-    fetchVal : List (String, Int) -> Maybe Int-    fetchVal [] = Nothing-    fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)--instance Functor Eval where-    map f (MkEval g) = MkEval (\e => map f (g e))--instance Applicative Eval where-    pure x = MkEval (\e => Just x)--    (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where-       app : Maybe (a -> b) -> Maybe a -> Maybe b-       app (Just fx) (Just gx) = Just (fx gx)-       app _         _         = Nothing--eval : Expr -> Eval Int-eval (Var x)   = fetch x-eval (Val x)   = [| x |]-eval (Add x y) = [| eval x + eval y |]--runEval : List (String, Int) -> Expr -> Maybe Int-runEval env e = case eval e of-    MkEval envFn => envFn env--m_add' : Maybe Int -> Maybe Int -> Maybe Int-m_add' x y = [| x + y |]-
− tutorial/examples/interp.idr 
@@ -1,71 +0,0 @@-module Main--data Ty = TyInt | TyBool| TyFun Ty Ty--interpTy : Ty -> Type-interpTy TyInt       = Int-interpTy TyBool      = Bool-interpTy (TyFun s t) = interpTy s -> interpTy t--using (G : Vect n Ty)--  data Env : Vect n Ty -> Type where-      Nil  : Env Nil-      (::) : interpTy a -> Env G -> Env (a :: G)--  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where-      stop : HasType fZ (t :: G) t-      pop  : HasType k G t -> HasType (fS k) (u :: G) t--  lookup : HasType i G t -> Env G -> interpTy t-  lookup stop    (x :: xs) = x-  lookup (pop k) (x :: xs) = lookup k xs--  data Expr : Vect n Ty -> Ty -> Type where-      Var : HasType i G t -> Expr G t-      Val : (x : Int) -> Expr G TyInt-      Lam : Expr (a :: G) t -> Expr G (TyFun a t)-      App : Expr G (TyFun a t) -> Expr G a -> Expr G t-      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->-            Expr G c-      If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a--  interp : Env G -> {static} Expr G t -> interpTy t-  interp env (Var i)     = lookup i env-  interp env (Val x)     = x-  interp env (Lam sc)    = \x => interp (x :: env) sc-  interp env (App f s)   = interp env f (interp env s)-  interp env (Op op x y) = op (interp env x) (interp env y)-  interp env (If x t e)  = if interp env x then interp env t-                                           else interp env e--  eId : Expr G (TyFun TyInt TyInt)-  eId = Lam (Var stop)--  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))-  eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))--  eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))-  eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop))))--  eDouble : Expr G (TyFun TyInt TyInt)-  eDouble = Lam (App (App eAdd (Var stop)) (Var stop))--  app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t-  app = \f, a => App f a--  fact : Expr G (TyFun TyInt TyInt)-  fact = Lam (If (Op (==) (Var stop) (Val 0))-                 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))--testFac : Int-testFac = interp [] fact 4--unitTestFac : so (interp [] fact 4 == 24)-unitTestFac = oh--main : IO ()-main = do putStr "Enter a number: "-          x <- getLine-          print (interp [] fact (cast x))-
− tutorial/examples/letbind.idr 
@@ -1,16 +0,0 @@-module letbind--mirror : List a -> List a-mirror xs = let xs' = reverse xs in-                xs ++ xs'--data Person = MkPerson String Int--showPerson : Person -> String-showPerson p = let MkPerson name age = p in-                   name ++ " is " ++ show age ++ " years old"--splitAt : Char -> String -> (String, String)-splitAt c x = case break (== c) x of-                  (x, y) => (x, strTail y)-
− tutorial/examples/prims.idr 
@@ -1,14 +0,0 @@-module prims--x : Int-x = 42--foo : String-foo = "Sausage machine"--bar : Char-bar = 'Z'--quux : Bool-quux = False-
− tutorial/examples/theorems.idr 
@@ -1,57 +0,0 @@--fiveIsFive : 5 = 5-fiveIsFive = refl--twoPlusTwo : 2 + 2 = 4-twoPlusTwo = refl--total disjoint : (n : Nat) -> Z = S n -> _|_-disjoint n p = replace {P = disjointTy} p ()-  where-    disjointTy : Nat -> Type-    disjointTy Z = ()-    disjointTy (S k) = _|_--total acyclic : (n : Nat) -> n = S n -> _|_-acyclic Z p = disjoint _ p-acyclic (S k) p = acyclic k (succInjective _ _ p)--empty1 : _|_-empty1 = hd [] where-    hd : List a -> a-    hd (x :: xs) = x--empty2 : _|_-empty2 = empty2--plusReduces : (n:Nat) -> plus Z n = n-plusReduces n = refl--plusReducesZ : (n:Nat) -> n = plus n Z-plusReducesZ Z = refl-plusReducesZ (S k) = cong (plusReducesZ k)--plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)-plusReducesS Z m = refl-plusReducesS (S k) m = cong (plusReducesS k m)--plusReducesZ' : (n:Nat) -> n = plus n Z-plusReducesZ' Z     = ?plusredZ_Z-plusReducesZ' (S k) = let ih = plusReducesZ' k in-                      ?plusredZ_S------------- Proofs ------------plusredZ_S = proof {-    intro;-    intro;-    rewrite ih;-    trivial;-}--plusredZ_Z = proof {-    compute;-    trivial;-}-
− tutorial/examples/universe.idr 
@@ -1,7 +0,0 @@-myid : (a : Type) -> a -> a-myid _ x = x--idid :  (a : Type) -> a -> a-idid = myid _ myid--
− tutorial/examples/usefultypes.idr 
@@ -1,20 +0,0 @@--intVec : Vect 5 Int-intVec = [1, 2, 3, 4, 5]--double : Int -> Int-double x = x * 2--vec : (n ** Vect n Int)-vec = (_ ** [3, 4])--list_lookup : Nat -> List a -> Maybe a-list_lookup _     Nil         = Nothing-list_lookup Z     (x :: xs) = Just x-list_lookup (S k) (x :: xs) = list_lookup k xs--lookup_default : Nat -> List a -> a -> a-lookup_default i xs def = case list_lookup i xs of-                              Nothing => def-                              Just x => x-
− tutorial/examples/vbroken.idr 
@@ -1,5 +0,0 @@-vapp : Vect n a -> Vect m a -> Vect (n + m) a-vapp Nil       ys = ys-vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN--
− tutorial/examples/views.idr 
@@ -1,37 +0,0 @@-module views--data Parity : Nat -> Type where-   even : Parity (n + n)-   odd  : Parity (S (n + n))--parity : (n:Nat) -> Parity n-parity Z     = even {n=Z}-parity (S Z) = odd {n=Z}-parity (S (S k)) with (parity k)-  parity (S (S (j + j)))     | even ?= even {n=S j}-  parity (S (S (S (j + j)))) | odd  ?= odd {n=S j}--natToBin : Nat -> List Bool-natToBin Z = Nil-natToBin k with (parity k)-   natToBin (j + j)     | even = False :: natToBin j-   natToBin (S (j + j)) | odd  = True  :: natToBin j------------- Proofs ------------views.parity_lemma_2 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--views.parity_lemma_1 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--
− tutorial/examples/wheres.idr 
@@ -1,14 +0,0 @@-module wheres--even : Nat -> Bool-even Z = True-even (S k) = odd k where-  odd Z = False-  odd (S k) = even k--test : List Nat-test = [c (S 1), c Z, d (S Z)]-  where c x = 42 + x-        d y = c (y + 1 + z y)-              where z w = y + w-