70b6c86 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak desugaring rules for 'case' in do blocks

(Also for ?holes) If there's no binding, assume that the type being returned by the case block or metavariable is (). This makes it possible to use case and holes in the middle of do blocks without any ugly hacks, and if there's no binding it's probably what was intended anyway.

commit70b6c862f51b8f007a008bdaa36e72573acd089d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Nov 2015, 17:24 (11 years ago) parented5ecbc

2 files changed+4−24

compare with master

unifiedsplit

src/Idris/DSL.hs+4−1 src/Idris/Elab/Clause.hs−23

src/Idris/DSL.hs+4−1

@@ -108,7 +108,10 @@ expandSugar dsl (PDoBlock ds)

108108 block b (DoExp fc tm : rest)

109109 = PApp fc b

110110 [pexp tm,

111− pexp (PLam fc (sMN 0 "bindx") NoFC Placeholder (block b rest))]

111+ pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]

112+ where mkTy (PCase _ _ _) = PRef fc [] unitTy

113+ mkTy (PMetavar _ _) = PRef fc [] unitTy

114+ mkTy _ = Placeholder

112115 block b _ = PElabError (Msg "Invalid statement in do block")

113116

114117expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

src/Idris/Elab/Clause.hs−23

@@ -669,8 +669,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

669669 (erun fc (build i winfo ERHS opts fname rhs))

670670 errAt "right hand side of " fname (Just clhsty)

671671 (erun fc $ psolve lhs_tm)

672− hs <- get_holes

673− mapM_ (elabCaseHole is) hs

674672 tt <- get_term

675673 aux <- getAux

676674 let (tm, ds) = runState (collectDeferred (Just fname)

@@ -788,27 +786,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

788786 (b : bf, af)

789787 sepBlocks' ns [] = ([], [])

790788

791−

792− -- if a hole is just an argument/result of a case block, treat it as

793− -- the unit type. Hack to help elaborate case in do blocks.

794− elabCaseHole aux h = do

795− focus h

796− g <- goal

797− case g of

798− TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve

799− _ -> return ()

800−

801− -- Is the name a pattern argument in the declaration

802− isArg :: Name -> PDecl -> Bool

803− isArg n (PClauses _ _ _ cs) = any isArg' cs

804− where

805− isArg' (PClause _ _ (PApp _ _ args) _ _ _)

806− = any (\x -> case x of

807− PRef _ _ n' -> n == n'

808− _ -> False) (map getTm args)

809− isArg' _ = False

810− isArg _ _ = False

811−

812789 -- term is not within "with" block

813790 isOutsideWith :: PTerm -> Bool

814791 isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False