bc2915c · Idris-dev · git.iko.soy

idris.cabal+3

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

403403 test/dsl003/run

404404 test/dsl003/*.idr

405405 test/dsl003/expected

406+ test/dsl004/run

407+ test/dsl004/*.idr

408+ test/dsl004/expected

406409

407410 test/effects001/run

408411 test/effects001/*.idr

libs/prelude/Builtins.idr+2−1

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

119119

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

121121 ||| 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!

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

124125 lend x = Read x

125126

libs/prelude/Decidable/Equality.idr+21

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

192192 primitiveEq = believe_me (Refl {x})

193193 postulate primitiveNotEq : x = y -> Void

194194

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+

195216

src/Idris/AbsSyntax.hs+77−63

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

10061006 en (PTyped l r) = PTyped (en l) (en r)

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

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

10101010 en (PHidden t) = PHidden (en t)

10111011 en (PUnifyLog t) = PUnifyLog (en t)

10121012 en (PDisamb ds t) = PDisamb ds (en t)

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

11771177 pri (PTyped l r) = pri l

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

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

11811181 pri (PConstant _ _) = 0

11821182 pri Placeholder = 1

11831183 pri _ = 3

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

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

15001500 namesIn uvars ist r

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

15031503 = do (decls, ns) <- get

15041504 let isn = concatMap (namesIn uvars ist) as

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

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

15421542

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

15441544addImpl' 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)

15461546 where

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

15481548 ai qq env ds (PRef fc fcs f)

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

15681568 t' = ai qq env ds t

15691569 r' = ai qq env ds r in

15701570 PDPair fc hls p l' t' r'

1571− ai qq env ds (PAlternative a as)

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

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

1573− PAlternative a as'

1573+ PAlternative ms a as'

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

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

15761576 = 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

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

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

16911691 alts -> Right $

1692− PAlternative (ExactlyOne True) $

1692+ PAlternative [] (ExactlyOne True) $

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

16941694 (insertImpl ns as)) alts

16951695 where

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

17961796 else do put (f : ns)

17971797 return (PPatvar fc f)

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

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

1800− as' <- slAlts ns as

1801− return (PAlternative b as')

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

1800+ as' <- slAlts ns as

1801+ return (PAlternative ms b as')

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

18031803 a' <- sl a

18041804 as' <- slAlts ns as

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

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

18501850 su (PApp fc f args)

18511851 = PHidden (PApp fc f args)

1852− su (PAlternative b alts)

1852+ su (PAlternative ms b alts)

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

18541854 if null alts' then Placeholder

1855− else PAlternative b alts'

1855+ else PAlternative ms b alts'

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

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

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

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

19761976 mt <- match' t t'

19771977 mr <- match' r r'

19781978 return (ml ++ mt ++ mr)

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

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

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

19811981 return (concat ms)

1982− match a@(PAlternative _ as) b

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

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

19841984 case (rights (map toEither ms)) of

19851985 (x: _) -> return x

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

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

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

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

20642064 sm xs (PHidden x) = PHidden (sm xs x)

20652065 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

20662066 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

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

20872087 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

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

20932093 sm (PHidden x) = PHidden (sm x)

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

20972097

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

20992099-- about with shadowing anywhere else).

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

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

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

2101+mkUniqueNames env shadows tm

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

2103+

2104+ initMap = M.fromList shadows

2105+

21022106 inScope :: S.Set Name

21032107 inScope = S.fromList $ boundNamesIn tm

21042108

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

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

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

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

21072111

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

21092113 -- looking for too long...)

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

21132117

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

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

2116− mkUniqT tac = return tac

2120+ mkUniqT nmap tac = return tac

21172121

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

2119− mkUniq (PLam fc n nfc ty sc)

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

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

21202124 = do env <- get

21212125 (n', sc') <-

21222126 if n `S.member` env

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

21242128 (S.union env inScope)

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

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

21262130 else return (n, sc)

21272131 put (S.insert n' env)

2128− ty' <- mkUniq ty

2129− sc'' <- mkUniq sc'

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

2133+ ty' <- mkUniq nmap ty

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

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

2131− mkUniq (PPi p n fc ty sc)

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

21322137 = do env <- get

21332138 (n', sc') <-

21342139 if n `S.member` env

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

21362141 (S.union env inScope)

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

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

21382143 else return (n, sc)

21392144 put (S.insert n' env)

2140− ty' <- mkUniq ty

2141− sc'' <- mkUniq sc'

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

2146+ ty' <- mkUniq nmap ty

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

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

21442150 = do env <- get

21452151 (n', sc') <-

21462152 if n `S.member` env

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

21482154 (S.union env inScope)

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

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

21502156 else return (n, sc)

21512157 put (S.insert n' env)

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

2153− sc'' <- mkUniq sc'

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

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

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

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

2155− mkUniq (PApp fc t args)

2156− = do t' <- mkUniq t

2157− args' <- mapM mkUniqA args

2162+ mkUniq nmap (PApp fc t args)

2163+ = do t' <- mkUniq nmap t

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

21582165 return $! PApp fc t' args'

2159− mkUniq (PAppBind fc t args)

2160− = do t' <- mkUniq t

2161− args' <- mapM mkUniqA args

2166+ mkUniq nmap (PAppBind fc t args)

2167+ = do t' <- mkUniq nmap t

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

21622169 return $! PAppBind fc t' args'

2163− mkUniq (PCase fc t alts)

2164− = do t' <- mkUniq t

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

2170+ mkUniq nmap (PCase fc t alts)

2171+ = do t' <- mkUniq nmap t

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

21662173 return (x', y')) alts

21672174 return $! PCase fc t' alts'

2168− mkUniq (PIfThenElse fc c t f)

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

2170− mkUniq (PPair fc hls p l r)

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

2175+ mkUniq nmap (PIfThenElse fc c t f)

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

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

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

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

21742181 | t /= Placeholder

21752182 = do env <- get

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

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

21792186 else return (n, sc)

21802187 put (S.insert n' env)

2181− t' <- mkUniq t

2182− sc'' <- mkUniq sc'

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

2189+ t' <- mkUniq nmap t

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

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

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

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

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

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

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

2187− mkUniq (PAlternative b as)

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

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

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

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

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

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

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

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

2196− mkUniq t = return t

2195+ mkUniq nmap (PAlternative ns b 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

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

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

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

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

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

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

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

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

850850 | 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.

851851 | 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.

852852 | 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.

854854 | PHidden PTerm -- ^ Irrelevant or hidden pattern

855855 | PType FC -- ^ 'Type' type

856856 | PUniverse Universe -- ^ Some universe

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

877877

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

879879 | FirstSuccess

880+ | TryImplicit

880881 deriving (Eq, Data, Typeable)

881882

882883-- | 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

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

904905mapPTermFC 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)

905906mapPTermFC 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)

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

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

909910mapPTermFC f g (PUniverse u) = PUniverse u

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

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

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

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

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

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

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

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

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

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

11241125highestFC (PAs fc _ _) = Just fc

1125−highestFC (PAlternative _ args) =

1126+highestFC (PAlternative _ _ args) =

11261127 case mapMaybe highestFC args of

11271128 [] -> Nothing

11281129 (fc:_) -> Just fc

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

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

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

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

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

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

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

17041705 where

17051706 prettyAs =

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

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

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

20102011 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

20122013 size (PHidden hidden) = size hidden

20132014 size (PUnifyLog tm) = size tm

20142015 size (PDisamb _ tm) = size tm

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

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

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

20542055 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

20562057 ni env (PUnifyLog tm) = ni env tm

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

20582059 ni env (PNoImplicits tm) = ni env tm

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

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

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

20802081 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

20822083 ni set (PHidden tm) = ni set tm

20832084 ni set (PUnifyLog tm) = ni set tm

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

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

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

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

21192120 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

21212122 ni env (PHidden tm) = ni env tm

21222123 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

21492150 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

21512152 ni env (PHidden tm) = ni env tm

21522153 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

21802181 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

21822183 ni env (PHidden tm) = ni env tm

21832184 ni env (PUnifyLog tm) = ni env tm

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

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

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

210210get_holes = do ES p _ _ <- get

211211 return $! (holes (fst p))

212212

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+

213220get_probs :: Elab' aux Fails

214221get_probs = do ES p _ _ <- get

215222 return $! (problems (fst p))

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

812819 = do s <- get

813820 ps <- get_probs

814821 ulog <- getUnifyLog

815− case prunStateT 999999 False ps t1 s of

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

817− return $! v

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

823+ case runStateT t1 s of

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

825+ return $! v

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

819827 case runStateT (t2 e1) s of

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

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

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

864872 else (f, i)

865873

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

866875prunStateT

867876 :: Int

868877 -> 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 #-}

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

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

45

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

357358 size _ = 1

358359

359360score :: Err -> Int

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

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

361362score (CantResolve _ _) = 20

362363score (NoSuchVariable _) = 1000

363364score (ProofSearchFail e) = score e

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

13841385

13851386uniqueNameSet :: Name -> Set Name -> Name

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

1387− | otherwise = n

1388+ | otherwise = n

13881389

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

13901391uniqueBinders ns = ubSet (fromList ns) where

src/Idris/Coverage.hs+1−1

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

3737 return $ mkApp t' args'

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

3939 -- 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

4141 toTT _ = do v <- get

4242 put (v + 1)

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

src/Idris/DSL.hs+2−2

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

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

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

8282 (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)

8484expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

8585expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

8686expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

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

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

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

141141 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

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

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

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

src/Idris/DeepSeq.hs+2−1

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

246246 rnf (PDPair x1 x2 x3 x4 x5 x6)

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

248248 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` ()

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

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

252252 rnf (PUniverse _) = ()

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

274274instance NFData PAltType where

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

276276 rnf FirstSuccess = ()

277+ rnf TryImplicit = ()

277278

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

279280 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

250250

251251 mkTyDecl (n, op, t, _)

252252 = PTy emptyDocstring [] syn fc op n NoFC

253− (mkUniqueNames [] t)

253+ (mkUniqueNames [] [] t)

254254

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

256256 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

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

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

427427 pexp l, pexp r])

428+

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

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

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

431432 pexp l, pexp r])

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

433− = do as' <- doPrune as

433+ elab' ina fc (PAlternative ms (ExactlyOne delayok) 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

434439 (h : hs) <- get_holes

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

441+ ty <- goal

435442 case as' of

436443 [x] -> elab' ina fc x

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

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

457464 doPrune as =

458465 do hnf_compute

459466 ty <- goal

460− ctxt <- get_context

461467 let (tc, _) = unApply ty

462468 env <- get_env

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

469+ return $ pruneByType env tc ist as

464470

465471

466472 isAmbiguous (CantResolveAlts _) = delayok

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

469475 isAmbiguous (At _ e) = isAmbiguous e

470476 isAmbiguous _ = False

471477

472− elab' ina fc (PAlternative FirstSuccess as)

473− = trySeq 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

482+ trySeq as

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

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

476485 try' e1 (trySeq' e1 xs) True

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

479488 trySeq' deferr (x : xs)

480489 = try' (do elab' ina fc x

481490 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+

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

483554 = do patvar n

484555 update_term liftPats

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

867938 solve

868939 where headRef (PRef _ _ _) = True

869940 headRef (PApp _ f _) = headRef f

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

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

871942 headRef _ = False

872943

873944 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

12271298

12281299 getFC d (PApp fc _ _) = fc

12291300 getFC d (PRef fc _ _) = fc

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

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

12311302 getFC d x = d

12321303

12331304 insertLazy :: PTerm -> ElabD PTerm

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

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

12421313 case tyh of

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

1244− -> return (PAlternative FirstSuccess tries)

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

12451316 _ -> return t

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

12481319 mkDelay env t

12491320 = let fc = fileFC "Delay" in

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

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

12591330 notImplicitable (PRef _ _ n)

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

12611332 = NoImplicit `elem` opts

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

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

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

12641335 -- they can go in the branches separately.

12651336 notImplicitable (PCase _ _ _) = True

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

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

13031374 (PCoerced tm, _) -> tm

13041375 (_, []) -> t

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

1306− PAlternative (ExactlyOne False)

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

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

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

13081378 return t'

13091379 where

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

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

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

13771447 prune t = t

13781448

1379− choose f (PAlternative a as)

1449+ choose f (PAlternative ms a as)

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

13811451 fs = filter (headIs f) as' in

13821452 case fs of

13831453 [a] -> a

1384− _ -> PAlternative a as'

1454+ _ -> PAlternative ms a as'

13851455

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

13871457 choose f t = t

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

13921462

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

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

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

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

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

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

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

13981468pruneByType env t c as

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

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

14011471 locallyBound [] = Nothing

14021472 locallyBound (t:ts)

14031473 | Just n <- getName t,

1404− n `elem` env = Just t

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

14051475 | otherwise = locallyBound ts

14061476 getName (PRef _ _ n) = Just n

14071477 getName (PApp _ f _) = getName f

14081478 getName (PHidden t) = getName t

14091479 getName _ = Nothing

14101480

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

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

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

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

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

14131484 | Nothing <- lookupTyExact n ctxt = as

14141485 | otherwise

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

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

14201491 _ -> asV

14211492 _ -> as'

14221493 where

1494+ ctxt = tt_ctxt ist

1495+

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

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

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

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

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

14361509 case unApply (getRetTy ty') of

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

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

1511+ (V _, _) ->

1512+ -- keep, variable

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

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

1515+ isPlausible ist var env n ty

14391516 _ -> False

14401517 _ -> False

14411518

14421519pruneByType _ t _ as = as

14431520

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+

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

14451551findHighlight :: Name -> ElabD OutputAnnotation

14461552findHighlight 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

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

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

122122elabExec :: FC -> PTerm -> PTerm

123−elabExec fc tm = runtm (PAlternative FirstSuccess

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

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

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

126126 tm,

src/Idris/ElabQuasiquote.hs+2−2

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

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

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

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

128−extractUnquotes n (PAlternative b alts)

128+extractUnquotes n (PAlternative ms b alts)

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

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

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

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

132132extractUnquotes n (PHidden tm)

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

134134 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 >>

109109 Foldable.mapM_ (warnDisamb ist) z

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

111111warnDisamb 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

113113warnDisamb ist (PHidden tm) = warnDisamb ist tm

114114warnDisamb ist (PType _) = return ()

115115warnDisamb ist (PUniverse _) = return ()

src/Idris/IBC.hs+9−5

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 115

43+ibcVersion = 116

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

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

15941594 put x4

15951595 put x5

15961596 put x6

1597− PAlternative x1 x2 -> do putWord8 20

1598− put x1

1599− put x2

1597+ PAlternative x1 x2 x3 -> do putWord8 20

1598+ put x1

1599+ put x2

1600+ put x3

16001601 PHidden x1 -> do putWord8 21

16011602 put x1

16021603 PType x1 -> do putWord8 22

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

17381739 return (PDPair x1 x2 x3 x4 x5 x6)

17391740 20 -> do x1 <- get

17401741 x2 <- get

1741− return (PAlternative x1 x2)

1742+ x3 <- get

1743+ return (PAlternative x1 x2 x3)

17421744 21 -> do x1 <- get

17431745 return (PHidden x1)

17441746 22 -> do x1 <- get

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

18091811 ExactlyOne x1 -> do putWord8 0

18101812 put x1

18111813 FirstSuccess -> putWord8 1

1814+ TryImplicit -> putWord8 2

18121815 get

18131816 = do i <- getWord8

18141817 case i of

18151818 0 -> do x1 <- get

18161819 return (ExactlyOne x1)

18171820 1 -> return FirstSuccess

1821+ 2 -> return TryImplicit

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

18191823

18201824

src/Idris/IdrisDoc.hs+1−1

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

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

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

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

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

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

312312extractPTermNames (PHidden p) = extract p

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

314314extractPTermNames (PDoBlock pdos) = concatMap extractPDo pdos

src/Idris/ParseExpr.hs+5−5

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

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

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

198198 = 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)

200200 update ns (PHidden t) = PHidden (update ns t)

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

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

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

464464modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

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

466466 | not (inPattern syn)

467− = PAlternative FirstSuccess

467+ = PAlternative [] FirstSuccess

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

469469 : consts)

470− | otherwise = PAlternative FirstSuccess consts

470+ | otherwise = PAlternative [] FirstSuccess consts

471471 where

472472 consts = [ PConstant inFC (BI x)

473473 , PConstant inFC (I (fromInteger x))

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

490490-}

491491alt :: SyntaxInfo -> IdrisParser PTerm

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

493− return (PAlternative FirstSuccess alts)

493+ return (PAlternative [] FirstSuccess alts)

494494

495495{- | Parses a possibly hidden simple expression

496496@

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

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

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

596596 -- 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

598598 | Just i <- getFromInt alts

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

600600 flattenFromInt fc f args = PApp fc f args

test/dsl004/Door0.idrnew file+33

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

1+import IOu

2+

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

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

5+

6+

7+

8+

9+

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

2+

3+import Data.Vect

4+

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

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

7+

8+

9+

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

2+

3+data DoorState = OPEN | CLOSED

4+

5+data DoorH : DoorState -> UniqueType where

6+ MkDH : DoorH s

7+

8+infix 5 @@

9+

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

2+

3+data DoorState = OPEN | CLOSED

4+

5+data DoorH : DoorState -> UniqueType where

6+ MkDH : DoorH s

7+

8+infix 5 @@

9+

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

2+

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

4+

5+data IOu : AnyType -> AnyType where

6+ MkIOu : IO a -> IOu a

7+

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

66

77testVal : Imp

88testVal = MkImp (apply id Z)

9+