idris 0.10.3 → 0.11
raw patch · 36 files changed
+364/−159 lines, 36 files
Files
- CHANGELOG +12/−0
- config.mk +9/−2
- idris.cabal +4/−1
- libs/effects/Effects.idr +4/−0
- libs/prelude/Builtins.idr +1/−1
- src/IRTS/Compiler.hs +7/−1
- src/Idris/AbsSyntax.hs +22/−23
- src/Idris/AbsSyntaxTree.hs +48/−24
- src/Idris/Core/Elaborate.hs +17/−9
- src/Idris/Core/TT.hs +3/−2
- src/Idris/DeepSeq.hs +4/−4
- src/Idris/Delaborate.hs +4/−4
- src/Idris/Directives.hs +11/−2
- src/Idris/Elab/AsPat.hs +8/−0
- src/Idris/Elab/Class.hs +5/−5
- src/Idris/Elab/Instance.hs +2/−2
- src/Idris/Elab/Record.hs +1/−1
- src/Idris/Elab/RunElab.hs +1/−1
- src/Idris/Elab/Term.hs +38/−19
- src/Idris/Elab/Type.hs +6/−3
- src/Idris/Elab/Utils.hs +9/−0
- src/Idris/IBC.hs +4/−4
- src/Idris/Parser.hs +36/−25
- src/Idris/Parser/Expr.hs +50/−18
- stack.yaml +1/−1
- test/basic009/expected +2/−0
- test/basic012/basic012a.idr +10/−0
- test/basic012/run +1/−0
- test/basic018/basic018.idr +14/−0
- test/basic018/expected +18/−0
- test/basic018/run +3/−0
- test/disambig002/disambig002.idr +1/−1
- test/proof003/test015.idr +3/−3
- test/proofsearch002/Process.idr +2/−2
- test/reg056/reg056.idr +1/−1
- test/reg068/expected +2/−0
CHANGELOG view
@@ -79,6 +79,18 @@ * More flexible holes. Holes can now depend on other holes in a term (such as implicit arguments which may be inferred from the definition of the hole).+* Programs with holes can now be compiled.+ Attempting to evaluate an expression with a hole results in a run time error.+* Dependent pairs now can be specified using a telescope-style syntax, without+ requirement of nesting, e.g. it is possible to now write the following:+ (a : Type ** n : Nat ** Vect n a)+* Idris will give a warning if an implicit is bound automatically, but would+ otherwise be a valid expressio if the name was used as a global++External Dependencies+---------------------++* Curses has been removed as an external dependancy. New in 0.10: ============
config.mk view
@@ -1,5 +1,12 @@-CC ?=cc-AR ?=ar+ifneq (, $(findstring MSYS, $(shell uname -a)))+ ifeq (cc,$(CC))+ # In MSYS2, when using the mingw version of gcc, there is no cc -> gcc+ # symlink. We can't use ?= here because CC is set implicitly to cc.+ # Cross compiling users can set CC to their cross compiler.+ CC =gcc+ endif+endif+ RANLIB ?=ranlib CABAL :=cabal
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.10.3+Version: 0.11 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -378,6 +378,9 @@ test/basic017/run test/basic017/*.idr test/basic017/expected+ test/basic018/run+ test/basic018/*.idr+ test/basic018/expected test/bignum001/run test/bignum001/*.idr
libs/effects/Effects.idr view
@@ -327,6 +327,10 @@ (<*>) prog v = do fn <- prog arg <- v return (fn arg)+ +(<$>) : (a -> b) ->+ EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)+(<$>) f v = pure f <*> v (*>) : EffM m a xs (\v => xs) -> EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
libs/prelude/Builtins.idr view
@@ -93,7 +93,7 @@ replace Refl prf = prf ||| Symmetry of propositional equality-sym : {l:a} -> {r:a} -> l = r -> r = l+sym : {left:a} -> {right:a} -> left = right -> right = left sym Refl = Refl ||| Transitivity of propositional equality
src/IRTS/Compiler.hs view
@@ -18,6 +18,7 @@ import Idris.ASTUtils import Idris.Erasure import Idris.Error+import Idris.Output import Debug.Trace @@ -112,7 +113,9 @@ where checkMVs = do i <- getIState case map fst (idris_metavars i) \\ primDefs of [] -> return ()- ms -> ifail $ "There are undefined holes: " ++ show ms+ ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms+ iputStrLn "\nEvaluation of any of these will crash at run time."+ return () checkTotality = do i <- getIState case idris_totcheckfail i of [] -> return ()@@ -227,6 +230,9 @@ irTerm vs env tm@(App _ f a) = do ist <- getIState case unApply tm of+ (P _ n _, args)+ | n `elem` map fst (idris_metavars ist) \\ primDefs+ -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n (P _ (UN m) _, args) | m == txt "mkForeignPrim" -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
src/Idris/AbsSyntax.hs view
@@ -1471,7 +1471,7 @@ -- if all of args in ns, then add it doAdd (UImplicit n ty : cs) ns t | elem n ns- = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)+ = PPi (Imp [] Dynamic False Nothing False) n NoFC ty (doAdd cs ns t) | otherwise = doAdd cs ns t -- bind the free names which weren't in the using block@@ -1479,7 +1479,7 @@ bindFree (n:ns) tm | elem n (map iname uimpls) = bindFree ns tm | otherwise- = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)+ = PPi (Imp [InaccessibleArg] Dynamic False Nothing False) n NoFC Placeholder (bindFree ns tm) getArgnames (PPi _ n _ c sc) = n : getArgnames sc@@ -1502,9 +1502,9 @@ getImps (Bind n (Pi _ t _) sc) imps | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps where- argInfo n (Imp opt _ _ _) Placeholder+ argInfo n (Imp opt _ _ _ _) Placeholder = (True, PImp 0 True opt n Placeholder)- argInfo n (Imp opt _ _ _) t'+ argInfo n (Imp opt _ _ _ _) t' = (False, PImp (getPriority i t') True opt n t') argInfo n (Exp opt _ _) t' = (InaccessibleArg `elem` opt,@@ -1536,18 +1536,15 @@ implicit' info syn ignore n ptm = do i <- getIState auto <- getAutoImpls- if not auto- then return ptm- else do- let (tm', impdata) = implicitise syn ignore i ptm- defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata- -- let (tm'', spos) = findStatics i tm'- putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }- addIBC (IBCImp n)- logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)- -- i <- get- -- putIState $ i { idris_statics = addDef n spos (idris_statics i) }- return tm'+ let (tm', impdata) = implicitise auto syn ignore i ptm+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata+-- let (tm'', spos) = findStatics i tm'+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }+ addIBC (IBCImp n)+ logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)+-- i <- get+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }+ return tm' where -- Detect unknown names in default arguments and throw error if found. defaultArgCheck :: [Name] -> [PArg] -> Idris ()@@ -1566,15 +1563,17 @@ notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n -implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])-implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $+-- Even if auto_implicits is off, we need to call this so we record which+-- arguments are implicit+implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])+implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $ let (declimps, ns') = execState (imps True [] tm) ([], [])- ns = filter (\n -> implicitable n || elem n (map fst uvars)) $+ ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $ ns' \\ (map fst pvars ++ no_imp syn ++ ignore) nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in if null ns then (tm, reverse declimps)- else implicitise syn ignore ist (pibind uvars nsOrder tm)+ else implicitise auto syn ignore ist (pibind uvars nsOrder tm) where uvars = map ipair (filter uimplicit (using syn)) pvars = syn_params syn@@ -1599,7 +1598,7 @@ = do (decls, ns) <- get let isn = nub (implNamesIn uvars ty) put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))- imps top env (PPi (Imp l _ _ _) n _ ty sc)+ imps top env (PPi (Imp l _ _ _ _) n _ ty sc) = do let isn = nub (implNamesIn uvars ty) `dropAll` [n] (decls , ns) <- get put (PImp (getPriority ist ty) True l n Placeholder : decls,@@ -1665,9 +1664,9 @@ pibind using [] sc = sc pibind using (n:ns) sc = case lookup n using of- Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))+ Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)) False) n NoFC ty (pibind using ns sc)- Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False) n NoFC Placeholder (pibind using ns sc) -- Add implicit arguments in function calls
src/Idris/AbsSyntaxTree.hs view
@@ -615,7 +615,8 @@ data Plicity = Imp { pargopts :: [ArgOpt], pstatic :: Static, pparam :: Bool,- pscoped :: Maybe ImplicitInfo -- Nothing, if top level+ pscoped :: Maybe ImplicitInfo, -- Nothing, if top level+ pinsource :: Bool -- Explicitly written in source } | Exp { pargopts :: [ArgOpt], pstatic :: Static,@@ -633,13 +634,13 @@ !-} is_scoped :: Plicity -> Maybe ImplicitInfo-is_scoped (Imp _ _ _ s) = s+is_scoped (Imp _ _ _ s _) = s is_scoped _ = Nothing -impl = Imp [] Dynamic False (Just (Impl False True))+impl = Imp [] Dynamic False (Just (Impl False True)) False -forall_imp = Imp [] Dynamic False (Just (Impl False False))-forall_constraint = Imp [] Dynamic False (Just (Impl True False))+forall_imp = Imp [] Dynamic False (Just (Impl False False)) False+forall_constraint = Imp [] Dynamic False (Just (Impl True False)) False expl = Exp [] Dynamic False expl_param = Exp [] Dynamic True@@ -784,11 +785,13 @@ case_decls :: [(Name, PDecl)], delayed_elab :: [(Int, Elab' EState ())], new_tyDecls :: [RDeclInstructions],- highlighting :: [(FC, OutputAnnotation)]+ highlighting :: [(FC, OutputAnnotation)],+ auto_binds :: [Name], -- names bound as auto implicits+ implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name) } initEState :: EState-initEState = EState [] [] [] []+initEState = EState [] [] [] [] [] [] type ElabD a = Elab' EState a @@ -1511,14 +1514,15 @@ maxline :: Maybe Int, mut_nesting :: Int, dsl_info :: DSL,- syn_in_quasiquote :: Int }+ syn_in_quasiquote :: Int,+ syn_toplevel :: Bool } deriving Show {-! deriving instance NFData SyntaxInfo deriving instance Binary SyntaxInfo !-} -defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True expandNS :: SyntaxInfo -> Name -> Name expandNS syn n@(NS _ _) = n@@ -1754,7 +1758,7 @@ case s of Static -> text "%static" <> space _ -> empty- prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)+ prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc) | ppopt_impl ppo = depth d . bracket p startPrec $ lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>@@ -1879,23 +1883,38 @@ align . group . vsep . punctuate (ann comma) $ map (prettySe (decD d) startPrec bnd) elts where ann = case pun of- TypeOrTerm -> id- IsType -> annName pairTy- IsTerm -> annName pairCon- prettySe d p bnd (PDPair _ _ pun l t r) =- depth d $- annotated lparen <>- left <+>- annotated (text "**") <+>- prettySe (decD d) startPrec (addBinding bnd) r <>- annotated rparen+ TypeOrTerm -> id+ IsType -> annName pairTy+ IsTerm -> annName pairCon+ prettySe d p bnd dpair@(PDPair _ _ pun l t r)+ | Just elts <- dPairElts dpair+ = depth d . enclose (annotated lparen) (annotated rparen) .+ align . group . vsep . punctuate (space <> annotated (text "**")) $+ ppElts elts bnd+ | otherwise+ = depth d $+ annotated lparen <>+ left <+>+ annotated (text "**") <+>+ prettySe (decD d) startPrec (addBinding bnd) r <>+ annotated rparen where annotated = case pun of- IsType -> annName sigmaTy- IsTerm -> annName sigmaCon- TypeOrTerm -> id+ IsType -> annName sigmaTy+ IsTerm -> annName sigmaCon+ TypeOrTerm -> id+ (left, addBinding) = case (l, pun) of (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))- _ -> (prettySe (decD d) startPrec bnd l, id)+ _ -> (prettySe (decD d) startPrec bnd l, id)++ ppElts [] bs = []+ ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]+ ppElts ((PRef _ _ n, t):rs) bs+ | IsType <- pun+ = (bindingOf n False <+> colon <+>+ prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)+ ppElts ((l, t):rs) bs+ = (prettySe (decD d) startPrec bs l) : ppElts rs bs prettySe d p bnd (PAlternative ns a as) = lparen <> text "|" <> prettyAs <> text "|" <> rparen where@@ -2013,6 +2032,11 @@ pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts) | otherwise = Just [x, y] pairElts _ = Nothing++ dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]+ dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)+ | otherwise = Just [(l, t), (Placeholder, r)]+ dPairElts _ = Nothing natns = "Prelude.Nat."
src/Idris/Core/Elaborate.hs view
@@ -123,15 +123,21 @@ errAt thing n ty = transformErr (Elaborating thing n ty) +erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)+erunAux f elab + = do s <- get+ case runStateT elab s of+ OK (a, s') -> do put s'+ aux <- getAux+ return $! (a, aux)+ Error (ProofSearchFail (At f e))+ -> lift $ Error (ProofSearchFail (At f e))+ Error (At f e) -> lift $ Error (At f e)+ Error e -> lift $ Error (At f e)+ erun :: FC -> Elab' aux a -> Elab' aux a-erun f elab = do s <- get- case runStateT elab s of- OK (a, s') -> do put s'- return $! a- Error (ProofSearchFail (At f e))- -> lift $ Error (ProofSearchFail (At f e))- Error (At f e) -> lift $ Error (At f e)- Error e -> lift $ Error (At f e)+erun f e = do (x, _) <- erunAux f e+ return x runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux) runElab a e ps = runStateT e (ES (ps, a) "" Nothing)@@ -726,7 +732,9 @@ checkPiGoal :: Name -> Elab' aux () checkPiGoal n = do g <- goal- case g of+ ctxt <- get_context+ env <- get_env+ case (normalise ctxt env g) of Bind _ (Pi _ _ _) _ -> return () _ -> do a <- getNameFrom (sMN 0 "__pargTy") b <- getNameFrom (sMN 0 "__pretTy")
src/Idris/Core/TT.hs view
@@ -645,8 +645,9 @@ updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a updateDef n f ctxt- = let ds = lookupCtxtName n ctxt in- foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds+ = case lookupCtxtExact n ctxt of+ Just t -> addDef n (f t) ctxt+ Nothing -> ctxt toAlist :: Ctxt a -> [(Name, a)] toAlist ctxt = let allns = map snd (Map.toList ctxt) in
src/Idris/DeepSeq.hs view
@@ -388,8 +388,8 @@ rnf _ = () instance NFData Plicity where- rnf (Imp x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()+ rnf (Imp x1 x2 x3 x4 x5)+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` () rnf (Exp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` () rnf (Constraint x1 x2)@@ -681,13 +681,13 @@ rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` () instance NFData SyntaxInfo where- rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq`- rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` () instance NFData OutputMode where rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
src/Idris/Delaborate.hs view
@@ -112,14 +112,14 @@ = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc) de env (_ : is) (Bind n (Pi (Just impl) ty _) sc) | toplevel_imp impl -- information in 'imps' repeated- = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)+ = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc) de env is (Bind n (Pi (Just impl) ty _) sc) | tcinstance impl = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc) | otherwise- = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)+ = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc) de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)- = PPi (Imp opts Dynamic False Nothing) n NoFC (de env [] ty) (de ((n,n):env) is sc)+ = PPi (Imp opts Dynamic False Nothing False) n NoFC (de env [] ty) (de ((n,n):env) is sc) de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc) = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc) de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)@@ -488,7 +488,7 @@ else empty pprintErr' i (ReflectionFailed msg err) = text "When attempting to perform error reflection, the following internal error occurred:" <>- indented (pprintErr' i err) <>+ indented (pprintErr' i err) <+> text msg <+> text ("This is probably a bug. Please consider reporting it at " ++ bugaddr) pprintErr' i (ElabScriptDebug msg tm holes) = text "Elaboration halted." <>
src/Idris/Directives.hs view
@@ -29,8 +29,10 @@ directiveAction (DInclude cgn hdr) = do addHdr cgn hdr addIBC (IBCHeader cgn hdr) -directiveAction (DHide n) = do setAccessibility n Hidden- addIBC (IBCAccess n Hidden)+directiveAction (DHide n') = do i <- getIState+ ns <- allNamespaces n'+ mapM_ (\n -> do setAccessibility n Hidden+ addIBC (IBCAccess n Hidden)) ns directiveAction (DFreeze n) = do setAccessibility n Frozen addIBC (IBCAccess n Frozen)@@ -80,3 +82,10 @@ [(n', _)] -> return n' [] -> throwError (NoSuchVariable n) more -> throwError (CantResolveAlts (map fst more))++allNamespaces :: Name -> Idris [Name]+allNamespaces n = do i <- getIState+ case lookupCtxtName n (idris_implicits i) of+ [(n', _)] -> return [n']+ [] -> throwError (NoSuchVariable n)+ more -> return (map fst more)
src/Idris/Elab/AsPat.hs view
@@ -28,6 +28,14 @@ = do as_tm <- mapM collectAs (map getTm as) let as' = zipWith (\a tm -> a { getTm = tm }) as as_tm return (PApp fc t as') -- only valid on args+-- only for 'ExactlyOne' since it means the alternatives will have the+-- same form, so we can assume we only need to extract from the first one+collectAs tm@(PAlternative ns (ExactlyOne d) (a : as)) + = do a' <- collectAs a+ pats <- get+ as' <- mapM collectAs as -- just to drop the '@'+ put pats -- discard later ones, since they're repeated+ return (PAlternative ns (ExactlyOne d) (a' : as')) collectAs x = return x -- | Replace _-patterns under @-patterns with fresh names that can be
src/Idris/Elab/Class.hs view
@@ -84,7 +84,7 @@ mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames - logElab 1 $ "Building methods " ++ show mnames+ logElab 2 $ "Building methods " ++ show mnames ims <- mapM (tdecl mnames) mdecls defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint) (filter clause ds)@@ -176,7 +176,7 @@ logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t' return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')), (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)- (\ l s p -> Imp l s p Nothing) t'))),+ (\ l s p -> Imp l s p Nothing True) t'))), (n, (nfc, syn, o, t) ) ) tdecl _ _ = ifail "Not allowed in a class declaration" @@ -250,7 +250,7 @@ return [PTy doc [] syn fc o m mfc ty', PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]] - getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc+ getMArgs (PPi (Imp _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc getMArgs _ = []@@ -270,7 +270,7 @@ rhsArgs [] _ = [] insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm- insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)+ insertConstraint c all (PPi p@(Imp _ _ _ _ _) n fc ty sc) = PPi p n fc ty (insertConstraint c all sc) insertConstraint c all sc = let dictN = sMN 0 "__class" in PPi (constraint { pstatic = Static })@@ -289,7 +289,7 @@ addC _ _ tm = tm -- make arguments explicit and don't bind class parameters- toExp ns e (PPi (Imp l s p _) n fc ty sc)+ toExp ns e (PPi (Imp l s p _ _) n fc ty sc) | n `elem` ns = toExp ns e sc | otherwise = PPi (e l s p) n fc ty (toExp ns e sc) toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
src/Idris/Elab/Instance.hs view
@@ -233,7 +233,7 @@ lamBind i (PPi _ n _ ty sc) sc' = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc') lamBind i _ sc = sc- methArgs i (PPi (Imp _ _ _ _) n _ ty sc)+ methArgs i (PPi (Imp _ _ _ _ _) n _ ty sc) = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc methArgs i (PPi (Exp _ _ _) n _ ty sc) = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc@@ -266,7 +266,7 @@ conbind [] x = x coninsert :: [(Name, PTerm)] -> PTerm -> PTerm- coninsert cs (PPi p@(Imp _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)+ coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc) coninsert cs sc = conbind cs sc -- Reorder declarations to be in the same order as defined in the
src/Idris/Elab/Record.hs view
@@ -441,7 +441,7 @@ -- | Creates a PArg with a given plicity, name, and term. asArg :: Plicity -> Name -> PTerm -> PArg-asArg (Imp os _ _ _) n t = PImp 0 False os n t+asArg (Imp os _ _ _ _) n t = PImp 0 False os n t asArg (Exp os _ _) n t = PExp 0 os n t asArg (Constraint os _) n t = PConstraint 0 os n t asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
src/Idris/Elab/RunElab.hs view
@@ -36,7 +36,7 @@ tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState (transformErr RunningElabScript (erun fc (do tm <- runElabAction ist fc [] script ns- EState is _ impls highlights <- getAux+ EState is _ impls highlights _ _ <- getAux ctxt <- get_context let ds = [] -- todo log <- getLog
src/Idris/Elab/Term.hs view
@@ -120,7 +120,7 @@ when tydecl (do mkPat update_term liftPats update_term orderPats)- EState is _ impls highlights <- getAux+ EState is _ impls highlights _ _ <- getAux tt <- get_term ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []@@ -165,7 +165,7 @@ -- unification when (not (null dots)) $ lift (Error (CantMatch (getInferTerm tm)))- EState is _ impls highlights <- getAux+ EState is _ impls highlights _ _ <- getAux tt <- get_term ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []@@ -232,11 +232,11 @@ end_unify ptm <- get_term when (pattern || intransform) -- convert remaining holes to pattern vars- (do update_term orderPats- unify_all+ (do unify_all matchProblems False -- only the ones we matched earlier unifyProblems- mkPat)+ mkPat+ update_term liftPats) where pattern = emode == ELHS intransform = emode == ETransLHS@@ -412,16 +412,6 @@ [pimp (sUN "A") Placeholder False, pimp (sUN "B") Placeholder False, pexp l, pexp r])--- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)--- [pimp (sUN "A") Placeholder False,--- pimp (sUN "B") Placeholder False,--- pexp l, pexp r]))--- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)--- [pimp (sUN "A") Placeholder False,--- pimp (sUN "B") Placeholder False,--- pexp l, pexp r]))--- True- elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r) = case t of Placeholder ->@@ -589,7 +579,9 @@ | pattern && not reflection && not (e_qq ec) && e_nomatching ec = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm) | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)- = do let ina = e_inarg ec+ = do ty <- goal+ testImplicitWarning fc n ty+ let ina = e_inarg ec guarded = e_guarded ec inty = e_intype ec ctxt <- get_context@@ -676,6 +668,7 @@ highlightSource nfc (AnnBoundName n False) elab' ina fc (PPi p n nfc Placeholder sc) = do attack; arg n (is_scoped p) (sMN 0 "ty")+ addAutoBind p n addPSname n -- okay for proof search elabE (ina { e_inarg = True, e_intype = True }) fc sc solve@@ -687,6 +680,7 @@ MN _ _ -> unique_hole n _ -> return n forall n' (is_scoped p) (Var tyn)+ addAutoBind p n' addPSname n' -- okay for proof search focus tyn let ec' = ina { e_inarg = True, e_intype = True }@@ -1207,7 +1201,7 @@ -- We now have an elaborated term. Reflect it and solve the -- original goal in the original proof state, preserving highlighting env <- get_env- EState _ _ _ hs <- getAux+ EState _ _ _ hs _ _ <- getAux loadState updateAux (\aux -> aux { highlighting = hs }) @@ -1403,8 +1397,8 @@ -- case block functions that don't yet exist) fullyElaborated :: Term -> ElabD () fullyElaborated (P _ n _) =- do EState cases _ _ _ <- getAux- case lookup n cases of+ do estate <- getAux+ case lookup n (case_decls estate) of Nothing -> return () Just _ -> lift . tfail $ ElabScriptStaging n fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated@@ -1548,6 +1542,31 @@ return result elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] = fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole++ addAutoBind :: Plicity -> Name -> ElabD ()+ addAutoBind (Imp _ _ _ _ False) n+ = updateAux (\est -> est { auto_binds = n : auto_binds est })+ addAutoBind _ _ = return ()++ testImplicitWarning :: FC -> Name -> Type -> ElabD ()+ testImplicitWarning fc n goal + | implicitable n && emode == ETyDecl+ = do env <- get_env+ est <- getAux+ when (n `elem` auto_binds est) $ + tryUnify env (lookupTyName n (tt_ctxt ist))+ | otherwise = return ()+ where+ tryUnify env [] = return ()+ tryUnify env ((nm, ty) : ts)+ = do inj <- get_inj+ hs <- get_holes+ case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)+ inj hs [] [] of+ OK _ -> + updateAux (\est -> est { implicit_warnings =+ (fc, nm) : implicit_warnings est })+ _ -> tryUnify env ts -- For every alternative, look at the function at the head. Automatically resolve -- any nested alternatives where that function is also at the head
src/Idris/Elab/Type.hs view
@@ -64,12 +64,15 @@ let ty = addImpl (imp_methods syn) i ty' logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'- logElab 5 $ show "with methods " ++ show (imp_methods syn)+ logElab 5 $ "with methods " ++ show (imp_methods syn) logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty - (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-+ ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <- tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState- (errAt "type of " n Nothing (erun fc (build i info ETyDecl [] n ty)))+ (errAt "type of " n Nothing + (erunAux fc (build i info ETyDecl [] n ty)))++ displayWarnings est setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights
src/Idris/Elab/Utils.hs view
@@ -395,3 +395,12 @@ case lookupCtxt n opt of [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt } _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }++displayWarnings :: EState -> Idris ()+displayWarnings est + = mapM_ displayImpWarning (implicit_warnings est)+ where+ displayImpWarning :: (FC, Name) -> Idris ()+ displayImpWarning (fc, n) = + iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"+ ++ "\tDid you mean to refer to " ++ show n ++ "?"
src/Idris/IBC.hs view
@@ -1154,7 +1154,7 @@ instance Binary Plicity where put x = case x of- Imp x1 x2 x3 x4 ->+ Imp x1 x2 x3 x4 _ -> do putWord8 0 put x1 put x2@@ -1181,7 +1181,7 @@ x2 <- get x3 <- get x4 <- get- return (Imp x1 x2 x3 x4)+ return (Imp x1 x2 x3 x4 False) 1 -> do x1 <- get x2 <- get x3 <- get@@ -1461,7 +1461,7 @@ _ -> error "Corrupted binary data for Using" instance Binary SyntaxInfo where- put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _) = do put x1 put x2 put x3@@ -1477,7 +1477,7 @@ x5 <- get x6 <- get x7 <- get- return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True) instance (Binary t) => Binary (PClause' t) where put x
src/Idris/Parser.hs view
@@ -487,48 +487,57 @@ -- Prevent syntax variable capture by making all binders under syntax unique -- (the ol' Common Lisp GENSYM approach) uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm- uniquifyBinders userNames = fixBind []+ uniquifyBinders userNames = fixBind 0 [] where- fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm- fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =+ fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm+ fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens = return $ PRef fc hls n'- fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =+ fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens = return $ PPatvar fc n'- fixBind rens (PLam fc n nfc ty body)- | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)+ fixBind 0 rens (PLam fc n nfc ty body)+ | n `elem` userNames = liftM2 (PLam fc n nfc)+ (fixBind 0 rens ty)+ (fixBind 0 rens body) | otherwise =- do ty' <- fixBind rens ty+ do ty' <- fixBind 0 rens ty n' <- gensym n- body' <- fixBind ((n,n'):rens) body+ body' <- fixBind 0 ((n,n'):rens) body return $ PLam fc n' nfc ty' body'- fixBind rens (PPi plic n nfc argTy body)+ fixBind 0 rens (PPi plic n nfc argTy body) | n `elem` userNames = liftM2 (PPi plic n nfc)- (fixBind rens argTy)- (fixBind rens body)+ (fixBind 0 rens argTy)+ (fixBind 0 rens body) | otherwise =- do ty' <- fixBind rens argTy+ do ty' <- fixBind 0 rens argTy n' <- gensym n- body' <- fixBind ((n,n'):rens) body+ body' <- fixBind 0 ((n,n'):rens) body return $ (PPi plic n' nfc ty' body')- fixBind rens (PLet fc n nfc ty val body)+ fixBind 0 rens (PLet fc n nfc ty val body) | n `elem` userNames = liftM3 (PLet fc n nfc)- (fixBind rens ty)- (fixBind rens val)- (fixBind rens body)+ (fixBind 0 rens ty)+ (fixBind 0 rens val)+ (fixBind 0 rens body) | otherwise =- do ty' <- fixBind rens ty- val' <- fixBind rens val+ do ty' <- fixBind 0 rens ty+ val' <- fixBind 0 rens val n' <- gensym n- body' <- fixBind ((n,n'):rens) body+ body' <- fixBind 0 ((n,n'):rens) body return $ PLet fc n' nfc ty' val' body'- fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =+ fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens = return $ PMatchApp fc n' -- Also rename resolved quotations, to allow syntax rules to -- have quoted references to their own bindings.- fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =+ fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens = return $ PQuoteName n' True fc- fixBind rens x = descendM (fixBind rens) x + -- Don't mess with quoted terms+ fixBind q rens (PQuasiquote tm goal) =+ flip PQuasiquote goal <$> fixBind (q + 1) rens tm+ fixBind q rens (PUnquote tm) =+ PUnquote <$> fixBind (q - 1) rens tm+ + fixBind q rens x = descendM (fixBind q rens) x+ gensym :: Name -> IdrisParser Name gensym n = do ist <- get let idx = idris_name ist@@ -599,7 +608,9 @@ return (doc, argDocs, fc, opts', n, nfc, acc)) ty <- typeExpr (allowImp syn) terminator- addAcc n acc+ -- If it's a top level function, note the accessibility+ -- rules+ when (syn_toplevel syn) $ addAcc n acc return (PTy doc argDocs syn fc opts' n nfc ty) <|> postulate syn <|> caf syn@@ -1116,7 +1127,7 @@ Nothing -> fail "Invalid clause" (do r <- rhs syn n let ctxt = tt_ctxt ist- let wsyn = syn { syn_namespace = [] }+ let wsyn = syn { syn_namespace = [], syn_toplevel = False } (wheres, nmap) <- choice [do x <- whereBlock n wsyn popIndent return x,
src/Idris/Parser/Expr.hs view
@@ -398,7 +398,7 @@ <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t)) <|> proofExpr syn <|> tacticsExpr syn- <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes) <|> do reserved "AnyType"; return $ PUniverse AllTypes <|> PType <$> reservedFC "Type" <|> do reserved "UniqueType"; return $ PUniverse UniqueType@@ -440,16 +440,16 @@ bracketed syn = do (FC fn (sl, sc) _) <- getFC lchar '(' <?> "parenthesized expression" bracketed' (FC fn (sl, sc) (sl, sc+1)) syn+ {- |Parses the rest of an expression in braces @ Bracketed' ::= ')' | Expr ')' | ExprList ')'- | Expr '**' Expr ')'+ | DependentPair ')' | Operator Expr ')' | Expr Operator ')'- | Name ':' Expr '**' Expr ')' ; @ -}@@ -458,14 +458,7 @@ do (FC f start (l, c)) <- getFC lchar ')' return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm- <|> try (do (ln, lnfc) <- name- colonFC <- lcharFC ':'- lty <- expr syn- starsFC <- reservedOpFC "**"- fc <- getFC- r <- expr syn- close <- lcharFC ')'- return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))+ <|> try (dependentPair TypeOrTerm [] open syn) <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')' -- No prefix operators! (bit of a hack here...) if (o == "-" || o == "!")@@ -486,20 +479,59 @@ <|> do l <- expr syn bracketedExpr syn open l +++{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}+dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm+dependentPair pun prev openFC syn =+ if prev == [] then+ nametypePart <|> namePart+ else+ case pun of+ IsType -> nametypePart <|> namePart <|> exprPart True+ IsTerm -> exprPart False+ TypeOrTerm -> nametypePart <|> namePart <|> exprPart False+ where nametypePart = do+ (ln, lnfc, colonFC) <- try $ do+ (ln, lnfc) <- name+ colonFC <- lcharFC ':'+ return (ln, lnfc, colonFC)+ lty <- expr' syn+ starsFC <- reservedOpFC "**"+ dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn+ namePart = try $ do+ (ln, lnfc) <- name+ starsFC <- reservedOpFC "**"+ dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn+ exprPart isEnd = do+ e <- expr syn+ sepFCE <-+ let stars = (Left <$> reservedOpFC "**")+ ending = (Right <$> lcharFC ')')+ in if isEnd then ending else stars <|> ending+ case sepFCE of+ Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn+ Right closeFC ->+ return (mkPDPairs pun openFC closeFC (reverse prev) e)+ mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =+ (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)+ pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))+ mergePDPairs pun starsFC' [] r = r+ mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =+ PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)+ -- | Parse the contents of parentheses, after an expression has been parsed. bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm bracketedExpr syn openParenFC e = do lchar ')'; return e- <|> do exprs <- many (do comma <- lcharFC ','+ <|> do exprs <- some (do comma <- lcharFC ',' r <- expr syn return (r, comma)) closeParenFC <- lcharFC ')' let hilite = [openParenFC, closeParenFC] ++ map snd exprs return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs) <|> do starsFC <- reservedOpFC "**"- r <- expr syn- closeParenFC <- lcharFC ')'- return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)+ dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn <?> "end of bracketed expression" where mergePairs :: [(PTerm, FC)] -> PTerm mergePairs [(t, fc)] = t@@ -1047,10 +1079,10 @@ sc <- expr syn let (im,cl) = if implicitAllowed syn- then (Imp opts st False (Just (Impl False True)),+ then (Imp opts st False (Just (Impl False True)) True, constraint)- else (Imp opts st False (Just (Impl False False)),- Imp opts st False (Just (Impl True False)))+ else (Imp opts st False (Just (Impl False False)) True,+ Imp opts st False (Just (Impl True False)) True) return (bindList (PPi im) xt (bindList (PPi cl) cs sc))
stack.yaml view
@@ -1,4 +1,4 @@-resolver: lts-5.5+resolver: lts-5.9 packages: - '.'
test/basic009/expected view
@@ -1,4 +1,6 @@ MAIN-PASS+Faulty.idr:6:9-12:WARNING: num is bound as an implicit+ Did you mean to refer to A.num? Faulty.idr:7:7: When checking right hand side of fault with expected type num = 0
+ test/basic012/basic012a.idr view
@@ -0,0 +1,10 @@+Symmetric : {c : Type} -> (c -> c -> Type) -> Type+Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a++record Symmetry (t : Type) (rel : t -> t -> Type) where+ constructor MkSymmetry+ is_symmetric : Symmetric {c=t} rel++symmetry : {ty : Type} -> Symmetry ty (=)+symmetry = MkSymmetry sym+
test/basic012/run view
@@ -1,4 +1,5 @@ #!/usr/bin/env bash ${IDRIS:-idris} $@ basic012.idr -o basic012 ./basic012+${IDRIS:-idris} $@ basic012a.idr --check rm -f basic012 *.ibc
+ test/basic018/basic018.idr view
@@ -0,0 +1,14 @@+import Data.Vect++thing : Nat+thing = 42++foo : -- (thing : Nat) ->+ Vect thing elem++bar : {thing : Nat} ->+ Vect thing elem++test : thing = S 41+test = Refl+
+ test/basic018/expected view
@@ -0,0 +1,18 @@+basic018.idr:7:12-17:WARNING: thing is bound as an implicit+ Did you mean to refer to Main.thing?+basic018.idr:12:8-13:WARNING: thing is bound as an implicit+ Did you mean to refer to Main.thing?+basic018.idr:13:6:+When checking right hand side of test with expected type+ thing = S 41++Type mismatch between+ 42 = 42 (Type of Refl)+and+ thing = 42 (Expected type)++Specifically:+ Type mismatch between+ 42+ and+ thing
+ test/basic018/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ basic018.idr --check --nocolor+rm -f *.ibc
test/disambig002/disambig002.idr view
@@ -75,7 +75,7 @@ (a : A) -> (p : P a) -> (ss : Vect n (DPair A P)) ->- Elem a (map fst ss) ->+ Elem a (map DPair.fst ss) -> Elem (a ** p) ss toVectComplete : {A : Type} ->
test/proof003/test015.idr view
@@ -44,11 +44,11 @@ testBin : Maybe (Binary 8 42) testBin = natToBin _ _ -pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))-term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))+pattern syntax bitpair [x] [y] = (_ ** _ ** (x, y, _))+term syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl)) addBit : Bit x -> Bit y -> Bit c ->- (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))+ (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)) addBit B0 B0 B0 = bitpair B0 B0 addBit B0 B0 B1 = bitpair B0 B1 addBit B0 B1 B0 = bitpair B0 B1
test/proofsearch002/Process.idr view
@@ -123,10 +123,10 @@ ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') -> Process b iface hs hs'' p p'' - Fork : Process () serveri [] (const []) (runningServer 1) (const doneServer) ->+ Fork : Process () serveri [] (const []) (runningServer 1) (const Process.doneServer) -> Process (ProcID serveri) iface hs (const hs) p (\res => (newServer res p)) Work : (worker : (pid : ProcID iface) -> Worker [pid] ()) ->- (waiter : Process t iface hs (const hs) (runningServer 1) (const doneServer)) ->+ (waiter : Process t iface hs (const hs) (runningServer 1) (const Process.doneServer)) -> Process t iface hs (const hs) p (const p) Request : (r : ProcID serveri) -> (x : serveri ty) ->
test/reg056/reg056.idr view
@@ -6,7 +6,7 @@ dodgy : (a, b : ()) -> a = b -> Void dodgy n m Refl impossible -nonk : (trap = Refl {x = Z}) -> Void+nonk : (Main.trap = Refl {x = Z}) -> Void nonk Refl impossible false : Void
test/reg068/expected view
@@ -3,5 +3,7 @@ This is likely to lead to problems! reg068.idr:2:6:Main.ze has a name which may be implicitly bound. This is likely to lead to problems!+reg068.idr:2:8-11:WARNING: nat is bound as an implicit+ Did you mean to refer to Main.nat? reg068.idr:2:6:When checking constructor Main.ze: Type level variable nat is not Main.nat