5da0d60 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Faster processing of alternatives

5da0d60Edwin Brady11 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

src/Idris/AbsSyntax.hs+76−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 p l r) = PPair f p (en l) (en r)

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

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

1009+ en (PAlternative ms a as) = PAlternative ms 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 ms 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 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 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 f) as)

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

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

1688 then Right $ PApp fc (PRef ffc f) as

1689 else Right $ mkPApp fc (length as) (PRef ffc f) as

1690 alts -> Right $

1691− PAlternative (ExactlyOne True) $

1691+ PAlternative [] (ExactlyOne True) $

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

1693 (insertImpl ns as)) alts

1694 where

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

1795 else do put (f : ns)

1796 return (PPatvar fc f)

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

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

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

1799− as' <- slAlts ns as

1799+ as' <- slAlts ns as

1800− return (PAlternative b as')

1800+ return (PAlternative ms b as')

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

1802 a' <- sl a

1803 as' <- slAlts ns as

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

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

1849 su (PApp fc f args)

1850 = PHidden (PApp fc f args)

1851− su (PAlternative b alts)

1851+ su (PAlternative ms b alts)

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

1853 if null alts' then Placeholder

1854− else PAlternative b alts'

1854+ else PAlternative ms b alts'

1855 su (PPair fc p l r) = PPair fc p (su l) (su r)

1856 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1857 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 p x y) = PPair f p (sm xs x) (sm xs y)

2062 sm xs (PDPair f p x t y) = PDPair f 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 p x y) = PPair f p (sm x) (sm y)

2089 sm (PDPair f p x t y) = PDPair f 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,93 @@ 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 p l r)

2177+ mkUniq nmap (PPair fc 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 p l' r'

2179 return $! PPair fc p l' r'

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

2180+ mkUniq nmap (PDPair fc p (PRef fc' 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 p (PRef fc' n') t' sc''

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

2184− mkUniq (PDPair fc p l t r)

2192+ mkUniq nmap (PDPair fc 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 p l' t' r'

2194 return $! PDPair fc 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)

src/Idris/AbsSyntaxTree.hs+11−11

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

850 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

851 | PDPair 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)

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

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

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

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

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

907−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)

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

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

910mapPTermFC f g (PUniverse u) = PUniverse u

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

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

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

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

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

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

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

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

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

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

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

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

1125highestFC (PAs fc _ _) = Just fc

1126−highestFC (PAlternative _ args) =

1126+highestFC (PAlternative _ _ args) =

1127 case mapMaybe highestFC args of

1128 [] -> Nothing

1129 (fc:_) -> Just fc

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

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

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

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

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

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

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

1705 where

1706 prettyAs =

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

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

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

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

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

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

2013 size (PHidden hidden) = size hidden

2014 size (PUnifyLog tm) = size tm

2015 size (PDisamb _ tm) = size tm

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

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

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

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

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

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

2057 ni env (PUnifyLog tm) = ni env tm

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

2059 ni env (PNoImplicits tm) = ni env tm

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

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

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

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

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

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

2083 ni set (PHidden tm) = ni set tm

2084 ni set (PUnifyLog tm) = ni set tm

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

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

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

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

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

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

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

2122 ni env (PHidden tm) = ni env tm

2123 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

2152 ni env (PHidden tm) = ni env tm

2153 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

2183 ni env (PHidden tm) = ni env tm

2184 ni env (PUnifyLog tm) = ni env tm

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

src/Idris/Core/Elaborate.hs+7

@@ -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))

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 p l r) = PPair fc p (expandSugar dsl l) (expandSugar dsl r)

81expandSugar dsl (PDPair fc p l t r) = PDPair fc 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 p l r) = PPair f p (v' i l) (v' i r)

141 v' i (PDPair f p l t r) = PDPair f 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+1−1

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

246 rnf (PDPair x1 x2 x3 x4 x5)

247 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `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 _) = ()

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+68−22

@@ -429,9 +429,15 @@ elab ist info emode opts fn tm

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

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

431 pexp l, pexp r])

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

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

433− = do as' <- doPrune as

433+ = do as_pruned <- doPrune as

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

435+ -- the full set.

436+ uns <- get_usedns

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

434 (h : hs) <- get_holes

438 (h : hs) <- get_holes

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

440+ ty <- goal

435 case as' of

441 case as' of

436 [x] -> elab' ina fc x

442 [x] -> elab' ina fc x

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

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

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

457 doPrune as =

463 doPrune as =

458 do hnf_compute

464 do hnf_compute

459 ty <- goal

465 ty <- goal

460− ctxt <- get_context

461 let (tc, _) = unApply ty

466 let (tc, _) = unApply ty

462 env <- get_env

467 env <- get_env

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

468+ return $ pruneByType env tc ist as

464

469

465

470

466 isAmbiguous (CantResolveAlts _) = delayok

471 isAmbiguous (CantResolveAlts _) = delayok

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

469 isAmbiguous (At _ e) = isAmbiguous e

474 isAmbiguous (At _ e) = isAmbiguous e

470 isAmbiguous _ = False

475 isAmbiguous _ = False

471

476

472− elab' ina fc (PAlternative FirstSuccess as)

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

478+ = do -- finish the mkUniqueNames job

479+ uns <- get_usedns

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

473− = trySeq as

481+ trySeq as

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

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

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

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

476 try' e1 (trySeq' e1 xs) True

484 try' e1 (trySeq' e1 xs) True

@@ -479,8 +487,9 @@ elab ist info emode opts fn tm

479 trySeq' deferr (x : xs)

487 trySeq' deferr (x : xs)

480 = try' (do elab' ina fc x

488 = try' (do elab' ina fc x

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

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

482− elab' ina fc (PAlternative TryImplicit (orig : alts)) = do

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

483 env <- get_env

491 env <- get_env

492+ ty <- goal

484 let doelab = elab' ina fc orig

493 let doelab = elab' ina fc orig

485 tryCatch doelab

494 tryCatch doelab

486 (\err ->

495 (\err ->

@@ -493,12 +502,13 @@ elab ist info emode opts fn tm

493 case pruneAlts err alts env of

502 case pruneAlts err alts env of

494 [] -> lift $ tfail err

503 [] -> lift $ tfail err

495 alts' ->

504 alts' ->

496− try' (elab' ina fc (PAlternative (ExactlyOne False) alts'))

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

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

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

498 True

507 True

499 else lift $ tfail err)

508 else lift $ tfail err)

500 where

509 where

501 recoverableErr (CantUnify _ _ _ _ _ _) = True

510 recoverableErr (CantUnify _ _ _ _ _ _) = True

511+ recoverableErr (TooManyArguments _) = False

502 recoverableErr (CantSolveGoal _ _) = False

512 recoverableErr (CantSolveGoal _ _) = False

503 recoverableErr (CantResolveAlts _) = False

513 recoverableErr (CantResolveAlts _) = False

504 recoverableErr (ProofSearchFail (Msg _)) = True

514 recoverableErr (ProofSearchFail (Msg _)) = True

@@ -924,7 +934,7 @@ elab ist info emode opts fn tm

924 solve

934 solve

925 where headRef (PRef _ _) = True

935 where headRef (PRef _ _) = True

926 headRef (PApp _ f _) = headRef f

936 headRef (PApp _ f _) = headRef f

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

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

928 headRef _ = False

938 headRef _ = False

929

939

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

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

@@ -1284,7 +1294,7 @@ elab ist info emode opts fn tm

1284

1294

1285 getFC d (PApp fc _ _) = fc

1295 getFC d (PApp fc _ _) = fc

1286 getFC d (PRef fc _) = fc

1296 getFC d (PRef fc _) = fc

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

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

1288 getFC d x = d

1298 getFC d x = d

1289

1299

1290 insertLazy :: PTerm -> ElabD PTerm

1300 insertLazy :: PTerm -> ElabD PTerm

@@ -1298,10 +1308,10 @@ elab ist info emode opts fn tm

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

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

1299 case tyh of

1309 case tyh of

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

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

1301− -> return (PAlternative FirstSuccess tries)

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

1302 _ -> return t

1312 _ -> return t

1303 where

1313 where

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

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

1305 mkDelay env t

1315 mkDelay env t

1306 = let fc = fileFC "Delay" in

1316 = let fc = fileFC "Delay" in

1307 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

1317 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

@@ -1316,7 +1326,7 @@ elab ist info emode opts fn tm

1316 notImplicitable (PRef _ n)

1326 notImplicitable (PRef _ n)

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

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

1318 = NoImplicit `elem` opts

1328 = NoImplicit `elem` opts

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

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

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

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

1321 -- they can go in the branches separately.

1331 -- they can go in the branches separately.

1322 notImplicitable (PCase _ _ _) = True

1332 notImplicitable (PCase _ _ _) = True

@@ -1359,7 +1369,7 @@ elab ist info emode opts fn tm

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

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

1360 (PCoerced tm, _) -> tm

1370 (PCoerced tm, _) -> tm

1361 (_, []) -> t

1371 (_, []) -> t

1362− (_, cs) -> PAlternative TryImplicit

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

1363 (t : map (mkCoerce env t) cs)

1373 (t : map (mkCoerce env t) cs)

1364 return t'

1374 return t'

1365 where

1375 where

@@ -1432,12 +1442,12 @@ pruneAlt xs = map prune xs

1432 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1442 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1433 prune t = t

1443 prune t = t

1434

1444

1435− choose f (PAlternative a as)

1445+ choose f (PAlternative ms a as)

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

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

1437 fs = filter (headIs f) as' in

1447 fs = filter (headIs f) as' in

1438 case fs of

1448 case fs of

1439 [a] -> a

1449 [a] -> a

1440− _ -> PAlternative a as'

1450+ _ -> PAlternative ms a as'

1441

1451

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

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

1443 choose f t = t

1453 choose f t = t

@@ -1448,8 +1458,8 @@ pruneAlt xs = map prune xs

1448

1458

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

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

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

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

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

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

1452− Context -> [PTerm] -> [PTerm]

1462+ IState -> [PTerm] -> [PTerm]

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

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

1454pruneByType env t c as

1464pruneByType env t c as

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

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

@@ -1457,15 +1467,16 @@ pruneByType env t c as

1457 locallyBound [] = Nothing

1467 locallyBound [] = Nothing

1458 locallyBound (t:ts)

1468 locallyBound (t:ts)

1459 | Just n <- getName t,

1469 | Just n <- getName t,

1460− n `elem` env = Just t

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

1461 | otherwise = locallyBound ts

1471 | otherwise = locallyBound ts

1462 getName (PRef _ n) = Just n

1472 getName (PRef _ n) = Just n

1463 getName (PApp _ f _) = getName f

1473 getName (PApp _ f _) = getName f

1464 getName (PHidden t) = getName t

1474 getName (PHidden t) = getName t

1465 getName _ = Nothing

1475 getName _ = Nothing

1466

1476

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

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

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

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

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

1469 | Nothing <- lookupTyExact n ctxt = as

1480 | Nothing <- lookupTyExact n ctxt = as

1470 | otherwise

1481 | otherwise

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

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

@@ -1476,6 +1487,8 @@ pruneByType env (P _ n _) ctxt as

1476 _ -> asV

1487 _ -> asV

1477 _ -> as'

1488 _ -> as'

1478 where

1489 where

1490+ ctxt = tt_ctxt ist

1491+

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

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

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

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

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

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

@@ -1491,12 +1504,45 @@ pruneByType env (P _ n _) ctxt as

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

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

1492 case unApply (getRetTy ty') of

1505 case unApply (getRetTy ty') of

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

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

1507+ (V _, _) ->

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

1508+ -- keep, variable

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

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

1511+ isPlausible ist var env n ty

1495 _ -> False

1512 _ -> False

1496 _ -> False

1513 _ -> False

1497

1514

1498pruneByType _ t _ as = as

1515pruneByType _ t _ as = as

1499

1516

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

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

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

1520+-- Otherwise, yes

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

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

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

1524+isPlausible ist var env n ty

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

1526+ case hvar of

1527+ Nothing -> True

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

1529+ where

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

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

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

1533+ = let tcs' = case unApply ty of

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

1535+ case lookupCtxtExact c (idris_classes ist) of

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

1537+ : tcs)

1538+ Nothing -> tcs

1539+ _ -> tcs

1540+ in

1541+ collectConstraints (n : env) tcs' sc

1542+ collectConstraints env tcs t

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

1544+ | otherwise = (Nothing, tcs)

1545+

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

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

1501findHighlight :: Name -> ElabD OutputAnnotation

1547findHighlight :: Name -> ElabD OutputAnnotation

1502findHighlight n = do ctxt <- get_context

1548findHighlight 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 info a b c)

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

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

127 return (PDPair fc 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+7−5

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

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 114

43+ibcVersion = 115

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

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

1590 put x3

1591 put x4

1592 put x5

1593− PAlternative x1 x2 -> do putWord8 20

1593+ PAlternative x1 x2 x3 -> do putWord8 20

1594− put x1

1594+ put x1

1595− put x2

1595+ put x2

1596+ put x3

1596 PHidden x1 -> do putWord8 21

1597 PHidden x1 -> do putWord8 21

1597 put x1

1598 put x1

1598 PType x1 -> do putWord8 22

1599 PType x1 -> do putWord8 22

@@ -1730,7 +1731,8 @@ instance Binary PTerm where

1730 return (PDPair x1 x2 x3 x4 x5)

1731 return (PDPair x1 x2 x3 x4 x5)

1731 20 -> do x1 <- get

1732 20 -> do x1 <- get

1732 x2 <- get

1733 x2 <- get

1734+ x3 <- get

1733− return (PAlternative x1 x2)

1735+ return (PAlternative x1 x2 x3)

1734 21 -> do x1 <- get

1736 21 -> do x1 <- get

1735 return (PHidden x1)

1737 return (PHidden x1)

1736 22 -> do x1 <- get

1738 22 -> do x1 <- get

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 p l r) = PPair fc p (update ns l) (update ns r)

197 update ns (PDPair fc p l t r)

198 = PDPair fc 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 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)