bfacfbc · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+5−1

compare with master

unifiedsplit

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

1815stripUnmatchable :: IState -> PTerm -> PTerm

1816stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1817 su :: PTerm -> PTerm

1818− su (PRef fc f)

1818+ su tm@(PRef fc f)

1819 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

1820 = Placeholder

1821+ | (TType _ : _) <- lookupTy f (tt_ctxt i)

1822+ = PHidden tm

1823+ | (UType _ : _) <- lookupTy f (tt_ctxt i)

1824+ = PHidden tm

1821 su (PApp fc f@(PRef _ fn) args)

1825 su (PApp fc f@(PRef _ fn) args)

1822 -- here we use canBeDConName because the impossible pattern

1826 -- here we use canBeDConName because the impossible pattern

1823 -- check will not necessarily fully resolve constructor names,

1827 -- check will not necessarily fully resolve constructor names,

src/Idris/Elab/Clause.hs+6−2

@@ -373,7 +373,7 @@ elabPE info fc caller r =

373 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

374 showSep "\n"

375 (map (\ (lhs, rhs) ->

376− (show lhs ++ " = " ++

376+ (showTmImpls lhs ++ " = " ++

377 showTmImpls rhs)) (pe_clauses specdecl))

378

379 logLvl 2 $ show n ++ " transformation rule: " ++

@@ -381,7 +381,8 @@ elabPE info fc caller r =

381

382 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

383 let def = map (\(lhs, rhs) ->

384+ let lhs' = mapPT hiddenToPH $ stripUnmatchable ist lhs in

384− PClause fc newnm lhs [] rhs [])

385+ PClause fc newnm lhs' [] rhs [])

385 (pe_clauses specdecl)

386 (pe_clauses specdecl)

386 trans <- elabTransform info fc False rhs lhs

387 trans <- elabTransform info fc False rhs lhs

387 elabClauses info fc (PEGenerated:opts) newnm def

388 elabClauses info fc (PEGenerated:opts) newnm def

@@ -393,6 +394,9 @@ elabPE info fc caller r =

393 (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

394 (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

394 return [])

395 return [])

395

396

397+ hiddenToPH (PHidden _) = Placeholder

398+ hiddenToPH x = x

399+

396 specName simpl (ImplicitS, tm)

400 specName simpl (ImplicitS, tm)

397 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

401 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

398 specName simpl (ExplicitS, tm)

402 specName simpl (ExplicitS, tm)

src/Idris/PartialEval.hs+2−1

@@ -197,6 +197,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

197 dynArgs (_ : ns) (V _ : as) = dynArgs ns as

198 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

199 dynArgs _ _ = False -- and now we'll get stuck

200+

200mkNewPats ist d ns newname sname lhs rhs =

201mkNewPats ist d ns newname sname lhs rhs =

201 PEDecl lhs rhs (map mkClause d) False

202 PEDecl lhs rhs (map mkClause d) False

202 where

203 where

@@ -235,7 +236,7 @@ mkNewPats ist d ns newname sname lhs rhs =

235 mkSubst :: (Term, Term) -> Maybe (Name, Term)

236 mkSubst :: (Term, Term) -> Maybe (Name, Term)

236 mkSubst (P _ n _, t) = Just (n, t)

237 mkSubst (P _ n _, t) = Just (n, t)

237 mkSubst _ = Nothing

238 mkSubst _ = Nothing

238−

239+

239-- | Creates a new declaration for a specialised function application.

240-- | Creates a new declaration for a specialised function application.

240-- Simple version at the moment: just create a version which is a direct

241-- Simple version at the moment: just create a version which is a direct

241-- application of the function to be specialised.

242-- application of the function to be specialised.

test/reg054/expected+3−1

@@ -3,7 +3,9 @@ When checking an application of constructor Main.MkInfer:

3 Attempting concrete match on polymorphic argument: 0

4reg054.idr:34:7:When checking left hand side of weird:

5No explicit types on left hand side: Char

6+reg054.idr:37:8:When checking left hand side of weird':

7+No explicit types on left hand side: Nat

6−reg054.idr:37:1-8:When checking left hand side of tctrick:

8+reg054.idr:40:1-8:When checking left hand side of tctrick:

7When checking an application of Main.tctrick:

9When checking an application of Main.tctrick:

8 Type mismatch between

10 Type mismatch between

9 Maybe a1 (Type of Just x)

11 Maybe a1 (Type of Just x)

test/reg054/reg054.idr+3

@@ -33,6 +33,9 @@ data Weird : Type -> Type where

33weird : Weird x -> x

34weird {x = Char} y = '5'

35

36+weird' : Weird x -> x

37+weird' {x = Prelude.Nat.Nat} y = Z

38+

36tctrick : a -> Int

39tctrick : a -> Int

37tctrick (Just x) = x

40tctrick (Just x) = x

38tctrick Nothing = 42

41tctrick Nothing = 42