bc2915c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into parser-highlights

bc2915cDavid Raymond Christiansen11 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -403,6 +403,9 @@ Extra-source-files:

403 test/dsl003/run

404 test/dsl003/*.idr

405 test/dsl003/expected

406+ test/dsl004/run

407+ test/dsl004/*.idr

408+ test/dsl004/expected

406

409

407 test/effects001/run

410 test/effects001/run

408 test/effects001/*.idr

411 test/effects001/*.idr

libs/prelude/Builtins.idr+2−1

@@ -119,7 +119,8 @@ namespace Ownership

119

120 ||| Make a read-only version of a unique value, which can be passed to another

121 ||| function without the unique value being consumed.

122− implicit

122+ implicit -- needs a special case in the coercion code, since implicits need

123+ -- a concrete type to coerce!

123 lend : {a : UniqueType} -> a -> Borrowed a

124 lend : {a : UniqueType} -> a -> Borrowed a

124 lend x = Read x

125 lend x = Read x

125

126

libs/prelude/Decidable/Equality.idr+21

@@ -192,4 +192,25 @@ instance DecEq String where

192 primitiveEq = believe_me (Refl {x})

193 postulate primitiveNotEq : x = y -> Void

194

195+--------------------------------------------------------------------------------

196+-- Ptr

197+--------------------------------------------------------------------------------

198+

199+instance DecEq Ptr where

200+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

201+ where primitiveEq : x = y

202+ primitiveEq = believe_me (Refl {x})

203+ postulate primitiveNotEq : x = y -> Void

204+

205+--------------------------------------------------------------------------------

206+-- ManagedPtr

207+--------------------------------------------------------------------------------

208+

209+instance DecEq ManagedPtr where

210+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

211+ where primitiveEq : x = y

212+ primitiveEq = believe_me (Refl {x})

213+ postulate primitiveNotEq : x = y -> Void

214+

215+

195

216

src/Idris/AbsSyntax.hs+77−63

@@ -1006,7 +1006,7 @@ expandParams dec ps ns infs tm = en tm

1006 en (PTyped l r) = PTyped (en l) (en r)

1007 en (PPair f hls p l r) = PPair f hls p (en l) (en r)

1008 en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)

1009− en (PAlternative a as) = PAlternative a (map en as)

1009+ en (PAlternative ns a as) = PAlternative ns a (map en as)

1010 en (PHidden t) = PHidden (en t)

1011 en (PUnifyLog t) = PUnifyLog (en t)

1012 en (PDisamb ds t) = PDisamb ds (en t)

@@ -1177,7 +1177,7 @@ getPriority i tm = 1 -- pri tm

1177 pri (PTyped l r) = pri l

1178 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1179 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1180− pri (PAlternative a as) = maximum (map pri as)

1180+ pri (PAlternative _ a as) = maximum (map pri as)

1181 pri (PConstant _ _) = 0

1182 pri Placeholder = 1

1183 pri _ = 3

@@ -1499,7 +1499,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1499 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++

1500 namesIn uvars ist r

1501 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

1502− imps top env (PAlternative a as)

1502+ imps top env (PAlternative ms a as)

1503 = do (decls, ns) <- get

1504 let isn = concatMap (namesIn uvars ist) as

1505 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

@@ -1542,7 +1542,7 @@ addImpl = addImpl' False [] []

1542

1543addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1544addImpl' inpat env infns imp_meths ist ptm

1545− = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

1545+ = mkUniqueNames env [] (ai False (zip env (repeat Nothing)) [] ptm)

1546 where

1547 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1548 ai qq env ds (PRef fc fcs f)

@@ -1568,9 +1568,9 @@ addImpl' inpat env infns imp_meths ist ptm

1568 t' = ai qq env ds t

1569 r' = ai qq env ds r in

1570 PDPair fc hls p l' t' r'

1571− ai qq env ds (PAlternative a as)

1571+ ai qq env ds (PAlternative ms a as)

1572 = let as' = map (ai qq env ds) as in

1573− PAlternative a as'

1573+ PAlternative ms a as'

1574 ai qq env _ (PDisamb ds' as) = ai qq env ds' as

1575 ai qq env ds (PApp fc (PInferRef ffc hl f) as)

1576 = let as' = map (fmap (ai qq env ds)) as in

@@ -1689,7 +1689,7 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

1689 then Right $ PApp fc (PRef ffc [ffc] f) as

1690 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

1691 alts -> Right $

1692− PAlternative (ExactlyOne True) $

1692+ PAlternative [] (ExactlyOne True) $

1693 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

1694 (insertImpl ns as)) alts

1695 where

@@ -1796,9 +1796,9 @@ stripLinear i tm = evalState (sl tm) [] where

1796 else do put (f : ns)

1797 return (PPatvar fc f)

1798 -- Assumption is that variables are all the same in each alternative

1799− sl t@(PAlternative b as) = do ns <- get

1799+ sl t@(PAlternative ms b as) = do ns <- get

1800− as' <- slAlts ns as

1800+ as' <- slAlts ns as

1801− return (PAlternative b as')

1801+ return (PAlternative ms b as')

1802 where slAlts ns (a : as) = do put ns

1803 a' <- sl a

1804 as' <- slAlts ns as

@@ -1849,10 +1849,10 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1849 = PApp fc f (fmap (fmap su) args)

1850 su (PApp fc f args)

1851 = PHidden (PApp fc f args)

1852− su (PAlternative b alts)

1852+ su (PAlternative ms b alts)

1853 = let alts' = filter (/= Placeholder) (map su alts) in

1854 if null alts' then Placeholder

1855− else PAlternative b alts'

1855+ else PAlternative ms b alts'

1856 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)

1857 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)

1858 su t@(PLam fc _ _ _ _) = PHidden t

@@ -1976,10 +1976,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1976 mt <- match' t t'

1977 mr <- match' r r'

1978 return (ml ++ mt ++ mr)

1979− match (PAlternative a as) (PAlternative a' as')

1979+ match (PAlternative _ a as) (PAlternative _ a' as')

1980 = do ms <- zipWithM match' as as'

1981 return (concat ms)

1982− match a@(PAlternative _ as) b

1982+ match a@(PAlternative _ _ as) b

1983 = do let ms = zipWith match' as (repeat b)

1984 case (rights (map toEither ms)) of

1985 (x: _) -> return x

@@ -2060,7 +2060,7 @@ substMatchShadow n shs tm t = sm shs t where

2060 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

2061 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)

2062 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)

2063− sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

2063+ sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)

2064 sm xs (PHidden x) = PHidden (sm xs x)

2065 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2066 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

@@ -2087,7 +2087,7 @@ shadow n n' t = sm t where

2087 sm (PTyped x y) = PTyped (sm x) (sm y)

2088 sm (PPair f hls p x y) = PPair f hls p (sm x) (sm y)

2089 sm (PDPair f hls p x t y) = PDPair f hls p (sm x) (sm t) (sm y)

2090− sm (PAlternative a as) = PAlternative a (map sm as)

2090+ sm (PAlternative ms a as) = PAlternative ms a (map sm as)

2091 sm (PTactics ts) = PTactics (map (fmap sm) ts)

2092 sm (PProof ts) = PProof (map (fmap sm) ts)

2093 sm (PHidden x) = PHidden (sm x)

@@ -2097,13 +2097,17 @@ shadow n n' t = sm t where

2097

2098-- | Rename any binders which are repeated (so that we don't have to mess

2099-- about with shadowing anywhere else).

2100−mkUniqueNames :: [Name] -> PTerm -> PTerm

2100+mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2101+mkUniqueNames env shadows tm

2101−mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2102+ = evalState (mkUniq initMap tm) (S.fromList env) where

2103+

2104+ initMap = M.fromList shadows

2105+

2102 inScope :: S.Set Name

2106 inScope :: S.Set Name

2103 inScope = S.fromList $ boundNamesIn tm

2107 inScope = S.fromList $ boundNamesIn tm

2104

2108

2105− mkUniqA arg = do t' <- mkUniq (getTm arg)

2109+ mkUniqA nmap arg = do t' <- mkUniq nmap (getTm arg)

2106− return (arg { getTm = t' })

2110+ return (arg { getTm = t' })

2107

2111

2108 -- Initialise the unique name with the environment length (so we're not

2112 -- Initialise the unique name with the environment length (so we're not

2109 -- looking for too long...)

2113 -- looking for too long...)

@@ -2113,84 +2117,94 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2113

2117

2114 -- FIXME: Probably ought to do this for completeness! It's fine as

2118 -- FIXME: Probably ought to do this for completeness! It's fine as

2115 -- long as there are no bindings inside tactics though.

2119 -- long as there are no bindings inside tactics though.

2116− mkUniqT tac = return tac

2120+ mkUniqT nmap tac = return tac

2117

2121

2118− mkUniq :: PTerm -> State (S.Set Name) PTerm

2122+ mkUniq :: M.Map Name Name -> PTerm -> State (S.Set Name) PTerm

2119− mkUniq (PLam fc n nfc ty sc)

2123+ mkUniq nmap (PLam fc n nfc ty sc)

2120 = do env <- get

2124 = do env <- get

2121 (n', sc') <-

2125 (n', sc') <-

2122 if n `S.member` env

2126 if n `S.member` env

2123 then do let n' = uniqueNameSet (initN n (S.size env))

2127 then do let n' = uniqueNameSet (initN n (S.size env))

2124 (S.union env inScope)

2128 (S.union env inScope)

2125− return (n', shadow n n' sc)

2129+ return (n', sc) -- shadow n n' sc)

2126 else return (n, sc)

2130 else return (n, sc)

2127 put (S.insert n' env)

2131 put (S.insert n' env)

2132+ let nmap' = M.insert n n' nmap

2128− ty' <- mkUniq ty

2133+ ty' <- mkUniq nmap ty

2129− sc'' <- mkUniq sc'

2134+ sc'' <- mkUniq nmap' sc'

2130 return $! PLam fc n' nfc ty' sc''

2135 return $! PLam fc n' nfc ty' sc''

2131− mkUniq (PPi p n fc ty sc)

2136+ mkUniq nmap (PPi p n fc ty sc)

2132 = do env <- get

2137 = do env <- get

2133 (n', sc') <-

2138 (n', sc') <-

2134 if n `S.member` env

2139 if n `S.member` env

2135 then do let n' = uniqueNameSet (initN n (S.size env))

2140 then do let n' = uniqueNameSet (initN n (S.size env))

2136 (S.union env inScope)

2141 (S.union env inScope)

2137− return (n', shadow n n' sc)

2142+ return (n', sc) -- shadow n n' sc)

2138 else return (n, sc)

2143 else return (n, sc)

2139 put (S.insert n' env)

2144 put (S.insert n' env)

2145+ let nmap' = M.insert n n' nmap

2140− ty' <- mkUniq ty

2146+ ty' <- mkUniq nmap ty

2141− sc'' <- mkUniq sc'

2147+ sc'' <- mkUniq nmap' sc'

2142 return $! PPi p n' fc ty' sc''

2148 return $! PPi p n' fc ty' sc''

2143− mkUniq (PLet fc n nfc ty val sc)

2149+ mkUniq nmap (PLet fc n nfc ty val sc)

2144 = do env <- get

2150 = do env <- get

2145 (n', sc') <-

2151 (n', sc') <-

2146 if n `S.member` env

2152 if n `S.member` env

2147 then do let n' = uniqueNameSet (initN n (S.size env))

2153 then do let n' = uniqueNameSet (initN n (S.size env))

2148 (S.union env inScope)

2154 (S.union env inScope)

2149− return (n', shadow n n' sc)

2155+ return (n', sc) -- shadow n n' sc)

2150 else return (n, sc)

2156 else return (n, sc)

2151 put (S.insert n' env)

2157 put (S.insert n' env)

2158+ let nmap' = M.insert n n' nmap

2152− ty' <- mkUniq ty; val' <- mkUniq val

2159+ ty' <- mkUniq nmap ty; val' <- mkUniq nmap val

2153− sc'' <- mkUniq sc'

2160+ sc'' <- mkUniq nmap' sc'

2154 return $! PLet fc n' nfc ty' val' sc''

2161 return $! PLet fc n' nfc ty' val' sc''

2155− mkUniq (PApp fc t args)

2162+ mkUniq nmap (PApp fc t args)

2156− = do t' <- mkUniq t

2163+ = do t' <- mkUniq nmap t

2157− args' <- mapM mkUniqA args

2164+ args' <- mapM (mkUniqA nmap) args

2158 return $! PApp fc t' args'

2165 return $! PApp fc t' args'

2159− mkUniq (PAppBind fc t args)

2166+ mkUniq nmap (PAppBind fc t args)

2160− = do t' <- mkUniq t

2167+ = do t' <- mkUniq nmap t

2161− args' <- mapM mkUniqA args

2168+ args' <- mapM (mkUniqA nmap) args

2162 return $! PAppBind fc t' args'

2169 return $! PAppBind fc t' args'

2163− mkUniq (PCase fc t alts)

2170+ mkUniq nmap (PCase fc t alts)

2164− = do t' <- mkUniq t

2171+ = do t' <- mkUniq nmap t

2165− alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y

2172+ alts' <- mapM (\(x,y)-> do x' <- mkUniq nmap x; y' <- mkUniq nmap y

2166 return (x', y')) alts

2173 return (x', y')) alts

2167 return $! PCase fc t' alts'

2174 return $! PCase fc t' alts'

2168− mkUniq (PIfThenElse fc c t f)

2175+ mkUniq nmap (PIfThenElse fc c t f)

2169− = liftM3 (PIfThenElse fc) (mkUniq c) (mkUniq t) (mkUniq f)

2176+ = liftM3 (PIfThenElse fc) (mkUniq nmap c) (mkUniq nmap t) (mkUniq nmap f)

2170− mkUniq (PPair fc hls p l r)

2177+ mkUniq nmap (PPair fc hls p l r)

2171− = do l' <- mkUniq l; r' <- mkUniq r

2178+ = do l' <- mkUniq nmap l; r' <- mkUniq nmap r

2172 return $! PPair fc hls p l' r'

2179 return $! PPair fc hls p l' r'

2173− mkUniq (PDPair fc hls p (PRef fc' hls' n) t sc)

2180+ mkUniq nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

2174 | t /= Placeholder

2181 | t /= Placeholder

2175 = do env <- get

2182 = do env <- get

2176 (n', sc') <- if n `S.member` env

2183 (n', sc') <- if n `S.member` env

2177 then do let n' = uniqueNameSet n (S.union env inScope)

2184 then do let n' = uniqueNameSet n (S.union env inScope)

2178− return (n', shadow n n' sc)

2185+ return (n', sc) -- shadow n n' sc)

2179 else return (n, sc)

2186 else return (n, sc)

2180 put (S.insert n' env)

2187 put (S.insert n' env)

2188+ let nmap' = M.insert n n' nmap

2181− t' <- mkUniq t

2189+ t' <- mkUniq nmap t

2182− sc'' <- mkUniq sc'

2190+ sc'' <- mkUniq nmap' sc'

2183 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2191 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2184− mkUniq (PDPair fc hls p l t r)

2192+ mkUniq nmap (PDPair fc hls p l t r)

2185− = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

2193+ = do l' <- mkUniq nmap l; t' <- mkUniq nmap t; r' <- mkUniq nmap r

2186 return $! PDPair fc hls p l' t' r'

2194 return $! PDPair fc hls p l' t' r'

2187− mkUniq (PAlternative b as)

2195+ mkUniq nmap (PAlternative ns b as)

2188− = liftM (PAlternative b) (mapM mkUniq as)

2196+ -- store the nmap and defer the rest until we've pruned the set

2197+ -- during elaboration

2198+ = return $ PAlternative (M.toList nmap ++ ns) b as

2189− mkUniq (PHidden t) = liftM PHidden (mkUniq t)

2199+ mkUniq nmap (PHidden t) = liftM PHidden (mkUniq nmap t)

2190− mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)

2200+ mkUniq nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq nmap t)

2191− mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)

2201+ mkUniq nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq nmap t)

2192− mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2202+ mkUniq nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq nmap t)

2193− mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2203+ mkUniq nmap (PProof ts) = liftM PProof (mapM (mkUniqT nmap) ts)

2194− mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2204+ mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

2195− mkUniq (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq ts)

2205+ mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2196− mkUniq t = return t

2206+ mkUniq nmap t = return (shadowAll (M.toList nmap) t)

2207+ where

2208+ shadowAll [] t = t

2209+ shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2210+

src/Idris/AbsSyntaxTree.hs+12−11

@@ -850,7 +850,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

850 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

851 | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

852 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

853− | PAlternative PAltType [PTerm] -- ^ True if only one may work. (| A, B, C|)

853+ | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

854 | PHidden PTerm -- ^ Irrelevant or hidden pattern

855 | PType FC -- ^ 'Type' type

856 | PUniverse Universe -- ^ Some universe

@@ -877,6 +877,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

877

878data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

879 | FirstSuccess

880+ | TryImplicit

880 deriving (Eq, Data, Typeable)

881 deriving (Eq, Data, Typeable)

881

882

882-- | Transform the FCs in a PTerm. The first function transforms the

883-- | Transform the FCs in a PTerm. The first function transforms the

@@ -903,7 +904,7 @@ mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (map

903mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)

904mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)

904mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

905mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

905mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

906mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

906−mapPTermFC f g (PAlternative ty ts) = PAlternative ty (map (mapPTermFC f g) ts)

907+mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)

907mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

908mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

908mapPTermFC f g (PType fc) = PType (f fc)

909mapPTermFC f g (PType fc) = PType (f fc)

909mapPTermFC f g (PUniverse u) = PUniverse u

910mapPTermFC f g (PUniverse u) = PUniverse u

@@ -952,7 +953,7 @@ mapPT f t = f (mpt t) where

952 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

953 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

953 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)

954 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)

954 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)

955 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)

955− mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)

956+ mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)

956 mpt (PHidden t) = PHidden (mapPT f t)

957 mpt (PHidden t) = PHidden (mapPT f t)

957 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

958 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

958 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

959 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

@@ -1122,7 +1123,7 @@ highestFC (PRewrite fc _ _ _) = Just fc

1122highestFC (PPair fc _ _ _ _) = Just fc

1123highestFC (PPair fc _ _ _ _) = Just fc

1123highestFC (PDPair fc _ _ _ _ _) = Just fc

1124highestFC (PDPair fc _ _ _ _ _) = Just fc

1124highestFC (PAs fc _ _) = Just fc

1125highestFC (PAs fc _ _) = Just fc

1125−highestFC (PAlternative _ args) =

1126+highestFC (PAlternative _ _ args) =

1126 case mapMaybe highestFC args of

1127 case mapMaybe highestFC args of

1127 [] -> Nothing

1128 [] -> Nothing

1128 (fc:_) -> Just fc

1129 (fc:_) -> Just fc

@@ -1699,7 +1700,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1699 (left, addBinding) = case (l, pun) of

1700 (left, addBinding) = case (l, pun) of

1700 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1701 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1701 _ -> (prettySe (decD d) startPrec bnd l, id)

1702 _ -> (prettySe (decD d) startPrec bnd l, id)

1702− prettySe d p bnd (PAlternative a as) =

1703+ prettySe d p bnd (PAlternative ns a as) =

1703 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1704 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1704 where

1705 where

1705 prettyAs =

1706 prettyAs =

@@ -2008,7 +2009,7 @@ instance Sized PTerm where

2008 size (PRewrite fc left right _) = 1 + size left + size right

2009 size (PRewrite fc left right _) = 1 + size left + size right

2009 size (PPair fc _ _ left right) = 1 + size left + size right

2010 size (PPair fc _ _ left right) = 1 + size left + size right

2010 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

2011 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

2011− size (PAlternative a alts) = 1 + size alts

2012+ size (PAlternative _ a alts) = 1 + size alts

2012 size (PHidden hidden) = size hidden

2013 size (PHidden hidden) = size hidden

2013 size (PUnifyLog tm) = size tm

2014 size (PUnifyLog tm) = size tm

2014 size (PDisamb _ tm) = size tm

2015 size (PDisamb _ tm) = size tm

@@ -2052,7 +2053,7 @@ allNamesIn tm = nub $ ni [] tm

2052 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r

2053 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r

2053 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2054 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2054 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2055 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2055− ni env (PAlternative a ls) = concatMap (ni env) ls

2056+ ni env (PAlternative ns a ls) = concatMap (ni env) ls

2056 ni env (PUnifyLog tm) = ni env tm

2057 ni env (PUnifyLog tm) = ni env tm

2057 ni env (PDisamb _ tm) = ni env tm

2058 ni env (PDisamb _ tm) = ni env tm

2058 ni env (PNoImplicits tm) = ni env tm

2059 ni env (PNoImplicits tm) = ni env tm

@@ -2078,7 +2079,7 @@ boundNamesIn tm = S.toList (ni S.empty tm)

2078 ni set (PPair _ _ _ l r) = ni (ni set l) r

2079 ni set (PPair _ _ _ l r) = ni (ni set l) r

2079 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r

2080 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r

2080 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r

2081 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r

2081− ni set (PAlternative a as) = niTms set as

2082+ ni set (PAlternative ns a as) = niTms set as

2082 ni set (PHidden tm) = ni set tm

2083 ni set (PHidden tm) = ni set tm

2083 ni set (PUnifyLog tm) = ni set tm

2084 ni set (PUnifyLog tm) = ni set tm

2084 ni set (PDisamb _ tm) = ni set tm

2085 ni set (PDisamb _ tm) = ni set tm

@@ -2117,7 +2118,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

2117 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2118 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2118 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2119 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2119 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2120 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2120− ni env (PAlternative a as) = concatMap (ni env) as

2121+ ni env (PAlternative ns a as) = concatMap (ni env) as

2121 ni env (PHidden tm) = ni env tm

2122 ni env (PHidden tm) = ni env tm

2122 ni env (PUnifyLog tm) = ni env tm

2123 ni env (PUnifyLog tm) = ni env tm

2123 ni env (PDisamb _ tm) = ni env tm

2124 ni env (PDisamb _ tm) = ni env tm

@@ -2147,7 +2148,7 @@ namesIn uvars ist tm = nub $ ni [] tm

2147 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2148 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2148 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2149 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2149 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2150 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2150− ni env (PAlternative a as) = concatMap (ni env) as

2151+ ni env (PAlternative ns a as) = concatMap (ni env) as

2151 ni env (PHidden tm) = ni env tm

2152 ni env (PHidden tm) = ni env tm

2152 ni env (PUnifyLog tm) = ni env tm

2153 ni env (PUnifyLog tm) = ni env tm

2153 ni env (PDisamb _ tm) = ni env tm

2154 ni env (PDisamb _ tm) = ni env tm

@@ -2178,7 +2179,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

2178 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2179 ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2179 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2180 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2180 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2181 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2181− ni env (PAlternative a as) = concatMap (ni env) as

2182+ ni env (PAlternative ns a as) = concatMap (ni env) as

2182 ni env (PHidden tm) = ni env tm

2183 ni env (PHidden tm) = ni env tm

2183 ni env (PUnifyLog tm) = ni env tm

2184 ni env (PUnifyLog tm) = ni env tm

2184 ni env (PDisamb _ tm) = ni env tm

2185 ni env (PDisamb _ tm) = ni env tm

src/Idris/Core/Elaborate.hs+12−3

@@ -210,6 +210,13 @@ get_holes :: Elab' aux [Name]

210get_holes = do ES p _ _ <- get

211 return $! (holes (fst p))

212

213+get_usedns :: Elab' aux [Name]

214+get_usedns = do ES p _ _ <- get

215+ let bs = bound_in (pterm (fst p)) ++

216+ bound_in_term (ptype (fst p))

217+ let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)

218+ return $! nouse

219+

213get_probs :: Elab' aux Fails

220get_probs :: Elab' aux Fails

214get_probs = do ES p _ _ <- get

221get_probs = do ES p _ _ <- get

215 return $! (problems (fst p))

222 return $! (problems (fst p))

@@ -812,9 +819,10 @@ tryCatch t1 t2

812 = do s <- get

819 = do s <- get

813 ps <- get_probs

820 ps <- get_probs

814 ulog <- getUnifyLog

821 ulog <- getUnifyLog

815− case prunStateT 999999 False ps t1 s of

822+-- case prunStateT 999999 False ps t1 s of

823+ case runStateT t1 s of

816− OK ((v, _, _), s') -> do put s'

824+ OK (v, s') -> do put s'

817− return $! v

825+ return $! v

818 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

826 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

819 case runStateT (t2 e1) s of

827 case runStateT (t2 e1) s of

820 OK (v, s') -> do put s'

828 OK (v, s') -> do put s'

@@ -863,6 +871,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

863 if (s >= i) then (lift (tfail err), s)

871 if (s >= i) then (lift (tfail err), s)

864 else (f, i)

872 else (f, i)

865

873

874+-- Run an elaborator, and fail if any problems are introduced

866prunStateT

875prunStateT

867 :: Int

876 :: Int

868 -> Bool

877 -> Bool

src/Idris/Core/TT.hs+4−3

@@ -1,4 +1,5 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,

2+ DeriveDataTypeable, PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3{-| TT is the core language of Idris. The language has:

4{-| TT is the core language of Idris. The language has:

@@ -357,7 +358,7 @@ instance Sized Err where

357 size _ = 1

358 size _ = 1

358

359

359score :: Err -> Int

360score :: Err -> Int

360−score (CantUnify _ _ _ m _ s) = s + score m

361+score (CantUnify _ _ _ m _ s) = 1 + s + score m

361score (CantResolve _ _) = 20

362score (CantResolve _ _) = 20

362score (NoSuchVariable _) = 1000

363score (NoSuchVariable _) = 1000

363score (ProofSearchFail e) = score e

364score (ProofSearchFail e) = score e

@@ -1384,7 +1385,7 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

1384

1385

1385uniqueNameSet :: Name -> Set Name -> Name

1386uniqueNameSet :: Name -> Set Name -> Name

1386uniqueNameSet n hs | n `member` hs = uniqueNameSet (nextName n) hs

1387uniqueNameSet n hs | n `member` hs = uniqueNameSet (nextName n) hs

1387− | otherwise = n

1388+ | otherwise = n

1388

1389

1389uniqueBinders :: [Name] -> TT Name -> TT Name

1390uniqueBinders :: [Name] -> TT Name -> TT Name

1390uniqueBinders ns = ubSet (fromList ns) where

1391uniqueBinders ns = ubSet (fromList ns) where

src/Idris/Coverage.hs+1−1

@@ -37,7 +37,7 @@ mkPatTm t = do i <- getIState

37 return $ mkApp t' args'

38 -- For alternatives, pick the first and drop the namespaces. It doesn't

39 -- really matter which is taken since matching will ignore the namespace.

40− toTT (PAlternative _ (a : as)) = toTT a

40+ toTT (PAlternative _ _ (a : as)) = toTT a

41 toTT _ = do v <- get

42 put (v + 1)

43 return (P Bound (sMN v "imp") Erased)

src/Idris/DSL.hs+2−2

@@ -80,7 +80,7 @@ expandSugar dsl (PIfThenElse fc c t f) =

80expandSugar dsl (PPair fc hls p l r) = PPair fc hls p (expandSugar dsl l) (expandSugar dsl r)

81expandSugar dsl (PDPair fc hls p l t r) = PDPair fc hls p (expandSugar dsl l) (expandSugar dsl t)

82 (expandSugar dsl r)

83−expandSugar dsl (PAlternative a as) = PAlternative a (map (expandSugar dsl) as)

83+expandSugar dsl (PAlternative ms a as) = PAlternative ms a (map (expandSugar dsl) as)

84expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

85expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

86expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

@@ -139,7 +139,7 @@ var dsl n t i = v' i t where

139 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

140 v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)

141 v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)

142− v' i (PAlternative a as) = PAlternative a $ map (v' i) as

142+ v' i (PAlternative ms a as) = PAlternative ms a $ map (v' i) as

143 v' i (PHidden t) = PHidden (v' i t)

144 v' i (PIdiom f t) = PIdiom f (v' i t)

145 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)

src/Idris/DeepSeq.hs+2−1

@@ -246,7 +246,7 @@ instance NFData PTerm where

246 rnf (PDPair x1 x2 x3 x4 x5 x6)

247 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` x6 `seq` ()

248 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

249− rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

249+ rnf (PAlternative x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

250 rnf (PHidden x1) = rnf x1 `seq` ()

251 rnf (PType fc) = rnf fc `seq` ()

252 rnf (PUniverse _) = ()

@@ -274,6 +274,7 @@ instance NFData PTerm where

274instance NFData PAltType where

275 rnf (ExactlyOne x1) = rnf x1 `seq` ()

276 rnf FirstSuccess = ()

277+ rnf TryImplicit = ()

277

278

278instance (NFData t) => NFData (PTactic' t) where

279instance (NFData t) => NFData (PTactic' t) where

279 rnf (Intro x1) = rnf x1 `seq` ()

280 rnf (Intro x1) = rnf x1 `seq` ()

src/Idris/Elab/Instance.hs+1−1

@@ -250,7 +250,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

250

251 mkTyDecl (n, op, t, _)

252 = PTy emptyDocstring [] syn fc op n NoFC

253− (mkUniqueNames [] t)

253+ (mkUniqueNames [] [] t)

254

255 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

256 conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

src/Idris/Elab/Term.hs+128−22

@@ -425,13 +425,20 @@ elab ist info emode opts fn tm

425 [pimp (sMN 0 "a") t False,

426 pimp (sMN 0 "P") Placeholder True,

427 pexp l, pexp r])

428+

428 elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

429 elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

429 [pimp (sMN 0 "a") t False,

430 [pimp (sMN 0 "a") t False,

430 pimp (sMN 0 "P") Placeholder True,

431 pimp (sMN 0 "P") Placeholder True,

431 pexp l, pexp r])

432 pexp l, pexp r])

432− elab' ina fc (PAlternative (ExactlyOne delayok) as)

433+ elab' ina fc (PAlternative ms (ExactlyOne delayok) as)

433− = do as' <- doPrune as

434+ = do as_pruned <- doPrune as

435+ -- Finish the mkUniqueNames job with the pruned set, rather than

436+ -- the full set.

437+ uns <- get_usedns

438+ let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned

434 (h : hs) <- get_holes

439 (h : hs) <- get_holes

440+-- trace (show (map showHd as')) $

441+ ty <- goal

435 case as' of

442 case as' of

436 [x] -> elab' ina fc x

443 [x] -> elab' ina fc x

437 -- If there's options, try now, and if that fails, postpone

444 -- If there's options, try now, and if that fails, postpone

@@ -457,10 +464,9 @@ elab ist info emode opts fn tm

457 doPrune as =

464 doPrune as =

458 do hnf_compute

465 do hnf_compute

459 ty <- goal

466 ty <- goal

460− ctxt <- get_context

461 let (tc, _) = unApply ty

467 let (tc, _) = unApply ty

462 env <- get_env

468 env <- get_env

463− return $ pruneByType (map fst env) tc ctxt as

469+ return $ pruneByType env tc ist as

464

470

465

471

466 isAmbiguous (CantResolveAlts _) = delayok

472 isAmbiguous (CantResolveAlts _) = delayok

@@ -469,8 +475,11 @@ elab ist info emode opts fn tm

469 isAmbiguous (At _ e) = isAmbiguous e

475 isAmbiguous (At _ e) = isAmbiguous e

470 isAmbiguous _ = False

476 isAmbiguous _ = False

471

477

472− elab' ina fc (PAlternative FirstSuccess as)

478+ elab' ina fc (PAlternative ms FirstSuccess as_in)

479+ = do -- finish the mkUniqueNames job

480+ uns <- get_usedns

481+ let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in

473− = trySeq as

482+ trySeq as

474 where -- if none work, take the error from the first

483 where -- if none work, take the error from the first

475 trySeq (x : xs) = let e1 = elab' ina fc x in

484 trySeq (x : xs) = let e1 = elab' ina fc x in

476 try' e1 (trySeq' e1 xs) True

485 try' e1 (trySeq' e1 xs) True

@@ -479,6 +488,68 @@ elab ist info emode opts fn tm

479 trySeq' deferr (x : xs)

488 trySeq' deferr (x : xs)

480 = try' (do elab' ina fc x

489 = try' (do elab' ina fc x

481 solveAutos ist fn False) (trySeq' deferr xs) True

490 solveAutos ist fn False) (trySeq' deferr xs) True

491+ elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

492+ env <- get_env

493+ ty <- goal

494+ let doelab = elab' ina fc orig

495+ tryCatch doelab

496+ (\err ->

497+ if recoverableErr err

498+ then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

499+ -- show alts ++ "\n" ++

500+ -- showQuick err) $

501+ -- Prune the coercions so that only the ones

502+ -- with the right type to fix the error will be tried!

503+ case pruneAlts err alts env of

504+ [] -> lift $ tfail err

505+ alts' ->

506+ try' (elab' ina fc (PAlternative [] (ExactlyOne False) alts'))

507+ (lift $ tfail err) -- take error from original if all fail

508+ True

509+ else lift $ tfail err)

510+ where

511+ recoverableErr (CantUnify _ _ _ _ _ _) = True

512+ recoverableErr (TooManyArguments _) = False

513+ recoverableErr (CantSolveGoal _ _) = False

514+ recoverableErr (CantResolveAlts _) = False

515+ recoverableErr (ProofSearchFail (Msg _)) = True

516+ recoverableErr (ProofSearchFail _) = False

517+ recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

518+ recoverableErr (At _ e) = recoverableErr e

519+ recoverableErr (ElabScriptDebug _ _ _) = False

520+ recoverableErr _ = True

521+

522+ pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env

523+ = case unApply (normalise (tt_ctxt ist) env inc) of

524+ (P (TCon _ _) n _, _) -> filter (hasArg n env) alts

525+ (Constant _, _) -> alts

526+ _ -> filter isLend alts -- special case hack for 'Borrowed'

527+ pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

528+ pruneAlts (At _ e) alts env = pruneAlts e alts env

529+ pruneAlts _ alts _ = filter isLend alts

530+

531+ hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

532+ hasArg n env (PApp _ (PRef _ _ a) _)

533+ = case lookupTyExact a (tt_ctxt ist) of

534+ Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

535+ any (fnIs n) args

536+ Nothing -> False

537+ hasArg n _ _ = False

538+

539+ isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]

540+ isLend _ = False

541+

542+ fnIs n ty = case unApply ty of

543+ (P _ n' _, _) -> n == n'

544+ _ -> False

545+

546+ showQuick (CantUnify _ (l, _) (r, _) _ _ _)

547+ = show (l, r)

548+ showQuick (ElaboratingArg _ _ _ e) = showQuick e

549+ showQuick (At _ e) = showQuick e

550+ showQuick (ProofSearchFail (Msg _)) = "search fail"

551+ showQuick _ = "No chance"

552+

482 elab' ina _ (PPatvar fc n) | bindfree

553 elab' ina _ (PPatvar fc n) | bindfree

483 = do patvar n

554 = do patvar n

484 update_term liftPats

555 update_term liftPats

@@ -867,7 +938,7 @@ elab ist info emode opts fn tm

867 solve

938 solve

868 where headRef (PRef _ _ _) = True

939 where headRef (PRef _ _ _) = True

869 headRef (PApp _ f _) = headRef f

940 headRef (PApp _ f _) = headRef f

870− headRef (PAlternative _ as) = all headRef as

941+ headRef (PAlternative _ _ as) = all headRef as

871 headRef _ = False

942 headRef _ = False

872

943

873 elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

944 elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

@@ -1227,7 +1298,7 @@ elab ist info emode opts fn tm

1227

1298

1228 getFC d (PApp fc _ _) = fc

1299 getFC d (PApp fc _ _) = fc

1229 getFC d (PRef fc _ _) = fc

1300 getFC d (PRef fc _ _) = fc

1230− getFC d (PAlternative _ (x:_)) = getFC d x

1301+ getFC d (PAlternative _ _ (x:_)) = getFC d x

1231 getFC d x = d

1302 getFC d x = d

1232

1303

1233 insertLazy :: PTerm -> ElabD PTerm

1304 insertLazy :: PTerm -> ElabD PTerm

@@ -1241,10 +1312,10 @@ elab ist info emode opts fn tm

1241 let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

1312 let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

1242 case tyh of

1313 case tyh of

1243 P _ (UN l) _ | l == txt "Lazy'"

1314 P _ (UN l) _ | l == txt "Lazy'"

1244− -> return (PAlternative FirstSuccess tries)

1315+ -> return (PAlternative [] FirstSuccess tries)

1245 _ -> return t

1316 _ -> return t

1246 where

1317 where

1247− mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

1318+ mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)

1248 mkDelay env t

1319 mkDelay env t

1249 = let fc = fileFC "Delay" in

1320 = let fc = fileFC "Delay" in

1250 addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))

1321 addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))

@@ -1259,7 +1330,7 @@ elab ist info emode opts fn tm

1259 notImplicitable (PRef _ _ n)

1330 notImplicitable (PRef _ _ n)

1260 | [opts] <- lookupCtxt n (idris_flags ist)

1331 | [opts] <- lookupCtxt n (idris_flags ist)

1261 = NoImplicit `elem` opts

1332 = NoImplicit `elem` opts

1262− notImplicitable (PAlternative (ExactlyOne _) as) = any notImplicitable as

1333+ notImplicitable (PAlternative _ (ExactlyOne _) as) = any notImplicitable as

1263 -- case is tricky enough without implicit coercions! If they are needed,

1334 -- case is tricky enough without implicit coercions! If they are needed,

1264 -- they can go in the branches separately.

1335 -- they can go in the branches separately.

1265 notImplicitable (PCase _ _ _) = True

1336 notImplicitable (PCase _ _ _) = True

@@ -1302,9 +1373,8 @@ elab ist info emode opts fn tm

1302 let t' = case (t, cs) of

1373 let t' = case (t, cs) of

1303 (PCoerced tm, _) -> tm

1374 (PCoerced tm, _) -> tm

1304 (_, []) -> t

1375 (_, []) -> t

1305− (_, cs) -> PAlternative FirstSuccess [t ,

1376+ (_, cs) -> PAlternative [] TryImplicit

1306− PAlternative (ExactlyOne False)

1307− (map (mkCoerce env t) cs)]

1377+ (t : map (mkCoerce env t) cs)

1308 return t'

1378 return t'

1309 where

1379 where

1310 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1380 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

@@ -1376,12 +1446,12 @@ pruneAlt xs = map prune xs

1376 = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

1446 = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

1377 prune t = t

1447 prune t = t

1378

1448

1379− choose f (PAlternative a as)

1449+ choose f (PAlternative ms a as)

1380 = let as' = fmap (choose f) as

1450 = let as' = fmap (choose f) as

1381 fs = filter (headIs f) as' in

1451 fs = filter (headIs f) as' in

1382 case fs of

1452 case fs of

1383 [a] -> a

1453 [a] -> a

1384− _ -> PAlternative a as'

1454+ _ -> PAlternative ms a as'

1385

1455

1386 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

1456 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

1387 choose f t = t

1457 choose f t = t

@@ -1392,8 +1462,8 @@ pruneAlt xs = map prune xs

1392

1462

1393-- Rule out alternatives that don't return the same type as the head of the goal

1463-- Rule out alternatives that don't return the same type as the head of the goal

1394-- (If there are none left as a result, do nothing)

1464-- (If there are none left as a result, do nothing)

1395−pruneByType :: [Name] -> Term -> -- head of the goal

1465+pruneByType :: Env -> Term -> -- head of the goal

1396− Context -> [PTerm] -> [PTerm]

1466+ IState -> [PTerm] -> [PTerm]

1397-- if an alternative has a locally bound name at the head, take it

1467-- if an alternative has a locally bound name at the head, take it

1398pruneByType env t c as

1468pruneByType env t c as

1399 | Just a <- locallyBound as = [a]

1469 | Just a <- locallyBound as = [a]

@@ -1401,15 +1471,16 @@ pruneByType env t c as

1401 locallyBound [] = Nothing

1471 locallyBound [] = Nothing

1402 locallyBound (t:ts)

1472 locallyBound (t:ts)

1403 | Just n <- getName t,

1473 | Just n <- getName t,

1404− n `elem` env = Just t

1474+ n `elem` map fst env = Just t

1405 | otherwise = locallyBound ts

1475 | otherwise = locallyBound ts

1406 getName (PRef _ _ n) = Just n

1476 getName (PRef _ _ n) = Just n

1407 getName (PApp _ f _) = getName f

1477 getName (PApp _ f _) = getName f

1408 getName (PHidden t) = getName t

1478 getName (PHidden t) = getName t

1409 getName _ = Nothing

1479 getName _ = Nothing

1410

1480

1481+-- 'n' is the name at the head of the goal type

1411−pruneByType env (P _ n _) ctxt as

1482+pruneByType env (P _ n _) ist as

1412−-- if the goal type is polymorphic, keep e

1483+-- if the goal type is polymorphic, keep everything

1413 | Nothing <- lookupTyExact n ctxt = as

1484 | Nothing <- lookupTyExact n ctxt = as

1414 | otherwise

1485 | otherwise

1415 = let asV = filter (headIs True n) as

1486 = let asV = filter (headIs True n) as

@@ -1420,6 +1491,8 @@ pruneByType env (P _ n _) ctxt as

1420 _ -> asV

1491 _ -> asV

1421 _ -> as'

1492 _ -> as'

1422 where

1493 where

1494+ ctxt = tt_ctxt ist

1495+

1423 headIs var f (PRef _ _ f') = typeHead var f f'

1496 headIs var f (PRef _ _ f') = typeHead var f f'

1424 headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

1497 headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

1425 headIs var f (PApp _ f' _) = headIs var f f'

1498 headIs var f (PApp _ f' _) = headIs var f f'

@@ -1435,12 +1508,45 @@ pruneByType env (P _ n _) ctxt as

1435 _ -> let ty' = normalise ctxt [] ty in

1508 _ -> let ty' = normalise ctxt [] ty in

1436 case unApply (getRetTy ty') of

1509 case unApply (getRetTy ty') of

1437 (P _ ftyn _, _) -> ftyn == f

1510 (P _ ftyn _, _) -> ftyn == f

1511+ (V _, _) ->

1438− (V _, _) -> var -- keep, variable

1512+ -- keep, variable

1513+-- trace ("Keeping " ++ show (f', ty')

1514+-- ++ " for " ++ show n) $

1515+ isPlausible ist var env n ty

1439 _ -> False

1516 _ -> False

1440 _ -> False

1517 _ -> False

1441

1518

1442pruneByType _ t _ as = as

1519pruneByType _ t _ as = as

1443

1520

1521+-- Could the name feasibly be the return type?

1522+-- If there is a type class constraint on the return type, and no instance

1523+-- in the environment or globally for that name, then no

1524+-- Otherwise, yes

1525+-- (FIXME: This isn't complete, but I'm leaving it here and coming back

1526+-- to it later - just returns 'var' for now. EB)

1527+isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

1528+isPlausible ist var env n ty

1529+ = let (hvar, classes) = collectConstraints [] [] ty in

1530+ case hvar of

1531+ Nothing -> True

1532+ Just rth -> var -- trace (show (rth, classes)) var

1533+ where

1534+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1535+ (Maybe Name, [(Term, [Name])])

1536+ collectConstraints env tcs (Bind n (Pi _ ty _) sc)

1537+ = let tcs' = case unApply ty of

1538+ (P _ c _, _) ->

1539+ case lookupCtxtExact c (idris_classes ist) of

1540+ Just tc -> ((ty, map fst (class_instances tc))

1541+ : tcs)

1542+ Nothing -> tcs

1543+ _ -> tcs

1544+ in

1545+ collectConstraints (n : env) tcs' sc

1546+ collectConstraints env tcs t

1547+ | (V i, _) <- unApply t = (Just (env !! i), tcs)

1548+ | otherwise = (Nothing, tcs)

1549+

1444-- | Use the local elab context to work out the highlighting for a name

1550-- | Use the local elab context to work out the highlighting for a name

1445findHighlight :: Name -> ElabD OutputAnnotation

1551findHighlight :: Name -> ElabD OutputAnnotation

1446findHighlight n = do ctxt <- get_context

1552findHighlight n = do ctxt <- get_context

src/Idris/Elab/Value.hs+1−1

@@ -120,7 +120,7 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

120-- | Try running the term directly (as IO ()), then printing it as an Integer

121-- (as a default numeric tye), then printing it as any Showable thing

122elabExec :: FC -> PTerm -> PTerm

123−elabExec fc tm = runtm (PAlternative FirstSuccess

123+elabExec fc tm = runtm (PAlternative [] FirstSuccess

124 [printtm (PApp fc (PRef fc [] (sUN "the"))

125 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

126 tm,

src/Idris/ElabQuasiquote.hs+2−2

@@ -125,10 +125,10 @@ extractUnquotes n (PDPair fc hls info a b c)

125 (b', ex2) <- extractUnquotes n b

126 (c', ex3) <- extractUnquotes n c

127 return (PDPair fc hls info a' b' c', ex1 ++ ex2 ++ ex3)

128−extractUnquotes n (PAlternative b alts)

128+extractUnquotes n (PAlternative ms b alts)

129 = do alts' <- mapM (extractUnquotes n) alts

130 let (alts'', exs) = unzip alts'

131− return (PAlternative b alts'', concat exs)

131+ return (PAlternative ms b alts'', concat exs)

132extractUnquotes n (PHidden tm)

133 = do (tm', ex) <- extractUnquotes n tm

134 return (PHidden tm', ex)

src/Idris/Error.hs+1−1

@@ -109,7 +109,7 @@ warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

109 Foldable.mapM_ (warnDisamb ist) z

110warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

111warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

112−warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms

112+warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms

113warnDisamb ist (PHidden tm) = warnDisamb ist tm

114warnDisamb ist (PType _) = return ()

115warnDisamb ist (PUniverse _) = return ()

src/Idris/IBC.hs+9−5

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 115

43+ibcVersion = 116

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -1594,9 +1594,10 @@ instance Binary PTerm where

1594 put x4

1595 put x5

1596 put x6

1597− PAlternative x1 x2 -> do putWord8 20

1597+ PAlternative x1 x2 x3 -> do putWord8 20

1598− put x1

1598+ put x1

1599− put x2

1599+ put x2

1600+ put x3

1600 PHidden x1 -> do putWord8 21

1601 PHidden x1 -> do putWord8 21

1601 put x1

1602 put x1

1602 PType x1 -> do putWord8 22

1603 PType x1 -> do putWord8 22

@@ -1738,7 +1739,8 @@ instance Binary PTerm where

1738 return (PDPair x1 x2 x3 x4 x5 x6)

1739 return (PDPair x1 x2 x3 x4 x5 x6)

1739 20 -> do x1 <- get

1740 20 -> do x1 <- get

1740 x2 <- get

1741 x2 <- get

1742+ x3 <- get

1741− return (PAlternative x1 x2)

1743+ return (PAlternative x1 x2 x3)

1742 21 -> do x1 <- get

1744 21 -> do x1 <- get

1743 return (PHidden x1)

1745 return (PHidden x1)

1744 22 -> do x1 <- get

1746 22 -> do x1 <- get

@@ -1809,12 +1811,14 @@ instance Binary PAltType where

1809 ExactlyOne x1 -> do putWord8 0

1811 ExactlyOne x1 -> do putWord8 0

1810 put x1

1812 put x1

1811 FirstSuccess -> putWord8 1

1813 FirstSuccess -> putWord8 1

1814+ TryImplicit -> putWord8 2

1812 get

1815 get

1813 = do i <- getWord8

1816 = do i <- getWord8

1814 case i of

1817 case i of

1815 0 -> do x1 <- get

1818 0 -> do x1 <- get

1816 return (ExactlyOne x1)

1819 return (ExactlyOne x1)

1817 1 -> return FirstSuccess

1820 1 -> return FirstSuccess

1821+ 2 -> return TryImplicit

1818 _ -> error "Corrupted binary data for PAltType"

1822 _ -> error "Corrupted binary data for PAltType"

1819

1823

1820

1824

src/Idris/IdrisDoc.hs+1−1

@@ -308,7 +308,7 @@ extractPTermNames (PRewrite _ a b m) | Just c <- m =

308extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

309extractPTermNames (PPair _ _ _ p1 p2) = concatMap extract [p1, p2]

310extractPTermNames (PDPair _ _ _ a b c) = concatMap extract [a, b, c]

311−extractPTermNames (PAlternative _ l) = concatMap extract l

311+extractPTermNames (PAlternative _ _ l) = concatMap extract l

312extractPTermNames (PHidden p) = extract p

313extractPTermNames (PGoal _ p1 n p2) = n : concatMap extract [p1, p2]

314extractPTermNames (PDoBlock pdos) = concatMap extractPDo pdos

src/Idris/ParseExpr.hs+5−5

@@ -196,7 +196,7 @@ extension syn ns rules =

196 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

197 update ns (PDPair fc hls p l t r)

198 = PDPair fc hls p (update ns l) (update ns t) (update ns r)

199− update ns (PAlternative a as) = PAlternative a (map (update ns) as)

199+ update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)

200 update ns (PHidden t) = PHidden (update ns t)

201 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

202 where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]

@@ -464,10 +464,10 @@ bracketedExpr syn openParenFC e =

464modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

465modifyConst syn fc (PConstant inFC (BI x))

466 | not (inPattern syn)

467− = PAlternative FirstSuccess

467+ = PAlternative [] FirstSuccess

468 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

469 : consts)

470− | otherwise = PAlternative FirstSuccess consts

470+ | otherwise = PAlternative [] FirstSuccess consts

471 where

472 consts = [ PConstant inFC (BI x)

473 , PConstant inFC (I (fromInteger x))

@@ -490,7 +490,7 @@ modifyConst syn fc x = x

490-}

491alt :: SyntaxInfo -> IdrisParser PTerm

492alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

493− return (PAlternative FirstSuccess alts)

493+ return (PAlternative [] FirstSuccess alts)

494

495{- | Parses a possibly hidden simple expression

496@

@@ -594,7 +594,7 @@ app syn = do f <- simpleExpr syn

594 -- literal to an argument, which we may want for obscure applications

595 -- of fromInteger, and this will help disambiguate better.

596 -- We know, at least, it won't be one of the constants!

597− flattenFromInt fc (PAlternative x alts) args

597+ flattenFromInt fc (PAlternative _ x alts) args

598 | Just i <- getFromInt alts

599 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

600 flattenFromInt fc f args = PApp fc f args

test/dsl004/Door0.idrnew file+33

@@ -0,0 +1,33 @@

1+import IOu

3+data Result : (a : Type) -> (a -> Type) -> Type* where

4+ Res : {k : a -> Type} -> (val : a) -> k val -> Result a k

10+

11+

12+------

13+data DoorState = OPEN | CLOSED

14+

15+data DoorH : DoorState -> Type where

16+ MkDH : {s : DoorState} -> DoorH s

17+

18+data DoorCmd : Type -> Type where

19+ Open : DoorH CLOSED -> DoorCmd (DoorH OPEN)

20+ Knock : DoorH CLOSED -> DoorCmd (DoorH CLOSED)

21+ Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

22+

23+data DoorLang : Type -> Type where

24+ Return : a -> DoorLang a

25+ Action : DoorCmd a -> DoorLang a

26+ (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

27+

28+testProg : DoorH CLOSED -> DoorLang ()

29+testProg h = do h <- Action (Knock h)

30+ h <- Action (Open h)

31+ h <- Action (Close h)

32+ Return ()

33+

test/dsl004/Door1.idrnew file+37

@@ -0,0 +1,37 @@

1+import IOu

3+import Data.Vect

5+data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where

6+ Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k

10+

11+

12+------

13+data DoorState = OPEN | CLOSED

14+

15+data DoorH : DoorState -> UniqueType where

16+ MkDH : DoorH s

17+

18+data DoorCmd : AnyType -> AnyType where

19+ Open : DoorH CLOSED -> DoorCmd (DoorH OPEN)

20+ Knock : DoorH CLOSED -> DoorCmd (DoorH CLOSED)

21+ Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

22+

23+data DoorLang : AnyType -> AnyType where

24+ Return : {a : AnyType} -> a -> DoorLang a

25+ Action : DoorCmd a -> DoorLang a

26+ (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

27+

28+implicit

29+action : DoorCmd a -> DoorLang a

30+action = Action

31+

32+testProg : DoorH CLOSED -> DoorLang ()

33+testProg h = do h <- Knock h

34+ h <- Open h

35+ h <- Close h

36+ Return ()

37+

test/dsl004/Door2.idrnew file+37

@@ -0,0 +1,37 @@

1+import IOu

3+data DoorState = OPEN | CLOSED

5+data DoorH : DoorState -> UniqueType where

6+ MkDH : DoorH s

8+infix 5 @@

10+data Res : (a : AnyType) -> (a -> AnyType) -> AnyType where

11+ (@@) : (val : a) -> (h : k val) -> Res a k

12+

13+data DoorCmd : AnyType -> AnyType where

14+ Open : DoorH CLOSED ->

15+ DoorCmd (Res Bool (\ok => case ok of

16+ True => DoorH OPEN

17+ False => DoorH CLOSED))

18+ Knock : DoorH CLOSED -> DoorCmd (DoorH CLOSED)

19+ Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

20+

21+data DoorLang : AnyType -> AnyType where

22+ Return : a -> DoorLang a

23+ Action : DoorCmd a -> DoorLang a

24+ (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

25+

26+implicit

27+action : DoorCmd a -> DoorLang a

28+action = Action

29+

30+covering

31+testProg : DoorH CLOSED -> DoorLang ()

32+testProg h = do h <- Action (Knock h)

33+ (True @@ h) <- Action (Open h)

34+ | (False @@ h) => testProg h

35+ h <- Action (Close h)

36+ Return ()

37+

test/dsl004/Door3.idrnew file+30

@@ -0,0 +1,30 @@

1+import IOu

3+data DoorState = OPEN | CLOSED

5+data DoorH : DoorState -> UniqueType where

6+ MkDH : DoorH s

8+infix 5 @@

10+data Res : (a : AnyType) -> (a -> AnyType) -> AnyType where

11+ (@@) : {k : a -> AnyType} -> (val : a) -> k val -> Res a k

12+

13+data DoorCmd : AnyType -> AnyType where

14+ Open : DoorH CLOSED ->

15+ DoorCmd (Res Bool (\ok => if ok then DoorH OPEN

16+ else DoorH CLOSED))

17+ Knock : DoorH CLOSED -> DoorCmd (DoorH CLOSED)

18+ Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

19+

20+data DoorLang : AnyType -> AnyType where

21+ Return : {a : AnyType} -> a -> DoorLang a

22+ Action : DoorCmd a -> DoorLang a

23+ (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

24+

25+testProg : DoorH CLOSED -> DoorLang (DoorH CLOSED)

26+testProg h = do h <- Action (Knock h)

27+ (True @@ h) <- Action (Open h)

28+ | (False @@ h) => Return h

29+ Action (Close h)

30+

test/dsl004/IOu.idrnew file+19

@@ -0,0 +1,19 @@

1+module IOu

3+-------- An IO type supporting possibly unique values

5+data IOu : AnyType -> AnyType where

6+ MkIOu : IO a -> IOu a

8+(>>=) : {a,b: AnyType} -> IOu a -> (a -> IOu b) -> IOu b

9+(>>=) (MkIOu x) k = MkIOu (do x' <- x

10+ case k x' of

11+ MkIOu k' => k')

12+

13+pure : {a : AnyType} -> a -> IOu a

14+pure x = MkIOu (pure x)

15+

16+run : IOu a -> IO a

17+run (MkIOu x) = x

18+

19+

test/dsl004/expectednew file

No changes to the content.

test/dsl004/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris $@ Door0.idr --check

3+idris $@ Door1.idr --check

4+idris $@ Door2.idr --check

5+rm -f *.ibc

test/reg001/reg001.idr+1

@@ -6,3 +6,4 @@ data Imp : Type where

7testVal : Imp

8testVal = MkImp (apply id Z)