9056a4a · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+6−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,

@@ -1835,6 +1839,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

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

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

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

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

1837 su t@(PPi _ _ _ _ _) = PHidden t

1841 su t@(PPi _ _ _ _ _) = PHidden t

1842+ su t@(PConstant _ c) | isTypeConst c = PHidden t

1838 su t = t

1843 su t = t

1839

1844

1840 ctxt = tt_ctxt i

1845 ctxt = tt_ctxt i

src/Idris/AbsSyntaxTree.hs+1

@@ -573,6 +573,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

573 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

574 | Constructor -- Data constructor type

575 | AutoHint -- use in auto implicit search

576+ | PEGenerated -- generated by partial evaluator

576 deriving (Show, Eq)

577 deriving (Show, Eq)

577{-!

578{-!

578deriving instance Binary FnOpt

579deriving instance Binary FnOpt

src/Idris/Core/DeepSeq.hs+1

@@ -198,6 +198,7 @@ instance NFData Totality where

198 rnf Productive = ()

199 rnf (Partial x1) = rnf x1 `seq` ()

200 rnf Unchecked = ()

201+ rnf Generated = ()

201

202

202instance NFData PReason where

203instance NFData PReason where

203 rnf (Other x1) = rnf x1 `seq` ()

204 rnf (Other x1) = rnf x1 `seq` ()

src/Idris/Core/Evaluate.hs+2

@@ -740,6 +740,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

740 | Productive -- ^ productive

741 | Partial PReason

742 | Unchecked

743+ | Generated

743 deriving Eq

744 deriving Eq

744{-!

745{-!

745deriving instance NFData Totality

746deriving instance NFData Totality

@@ -767,6 +768,7 @@ instance Show Totality where

767 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

768 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

768 showSep " --> " (map show ns)

769 showSep " --> " (map show ns)

769 show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n

770 show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n

771+ show Generated = "auto-generated"

770

772

771{-!

773{-!

772deriving instance Binary Accessibility

774deriving instance Binary Accessibility

src/Idris/Elab/Clause.hs+13−8

@@ -189,9 +189,9 @@ elabClauses info' fc opts n_in cs =

189

190 ist <- getIState

191 -- let wf = wellFounded ist n sc

192− let tot = if pcover || AssertTotal `elem` opts

192+ let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later

193− then Unchecked -- finish checking later

193+ | PEGenerated `elem` opts = Generated

194− else Partial NotCovering -- already know it's not total

194+ | otherwise = Partial NotCovering -- already know it's not total

195

196 -- case lookupCtxt (namespace info) n (idris_flags ist) of

197 -- [fs] -> if TotalFn `elem` fs

@@ -241,7 +241,8 @@ elabClauses info' fc opts n_in cs =

241 setContext ctxt'

242 addIBC (IBCDef n)

243 setTotality n tot

244+ when (not reflect && PEGenerated `notElem` opts) $

244− when (not reflect) $ do totcheck (fc, n)

245+ do totcheck (fc, n)

245 defer_totcheck (fc, n)

246 defer_totcheck (fc, n)

246 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

247 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

247 i <- getIState

248 i <- getIState

@@ -372,18 +373,19 @@ elabPE info fc caller r =

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

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

373 showSep "\n"

374 showSep "\n"

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

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

375− (show lhs ++ " = " ++

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

376 showTmImpls rhs)) (pe_clauses specdecl))

377 showTmImpls rhs)) (pe_clauses specdecl))

377

378

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

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

379− show rhs ++ " ==> " ++ show lhs

380+ showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

380

381

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

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

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

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

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

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

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

384 (pe_clauses specdecl)

386 (pe_clauses specdecl)

385 trans <- elabTransform info fc False rhs lhs

387 trans <- elabTransform info fc False rhs lhs

386− elabClauses info fc opts newnm def

388+ elabClauses info fc (PEGenerated:opts) newnm def

387 return [trans]

389 return [trans]

388 else return [])

390 else return [])

389 -- if it doesn't work, just don't specialise. Could happen for lots

391 -- if it doesn't work, just don't specialise. Could happen for lots

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

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

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

393 return [])

395 return [])

394

396

397+ hiddenToPH (PHidden _) = Placeholder

398+ hiddenToPH x = x

399+

395 specName simpl (ImplicitS, tm)

400 specName simpl (ImplicitS, tm)

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

397 specName simpl (ExplicitS, tm)

402 specName simpl (ExplicitS, tm)

src/Idris/Elab/Term.hs+8−7

@@ -35,7 +35,7 @@ import qualified Data.Text as T

35

36import Debug.Trace

37

38−data ElabMode = ETyDecl | ELHS | ERHS

38+data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

39 deriving Eq

40

41

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

220 sequence_ (get_delayed_elab est)

221 end_unify

222 ptm <- get_term

223− when pattern -- convert remaining holes to pattern vars

223+ when (pattern || intransform) -- convert remaining holes to pattern vars

224 (do update_term orderPats

225 unify_all

226 matchProblems False -- only the ones we matched earlier

@@ -228,7 +228,8 @@ elab ist info emode opts fn tm

228 mkPat)

229 where

230 pattern = emode == ELHS

231+ intransform = emode == ETransLHS

231− bindfree = emode == ETyDecl || emode == ELHS

232+ bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS

232

233

233 get_delayed_elab est =

234 get_delayed_elab est =

234 let ds = delayed_elab est in

235 let ds = delayed_elab est in

@@ -489,7 +490,7 @@ elab ist info emode opts fn tm

489 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

490 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

490 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

491 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

491 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

492 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

492− | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

493+ | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

493 = do let ina = e_inarg ec

494 = do let ina = e_inarg ec

494 guarded = e_guarded ec

495 guarded = e_guarded ec

495 inty = e_intype ec

496 inty = e_intype ec

@@ -500,7 +501,7 @@ elab ist info emode opts fn tm

500 _ -> True

501 _ -> True

501 -- this is to stop us resolve type classes recursively

502 -- this is to stop us resolve type classes recursively

502 -- trace (show (n, guarded)) $

503 -- trace (show (n, guarded)) $

503− if (tcname n && ina)

504+ if (tcname n && ina && not intransform)

504 then erun fc $

505 then erun fc $

505 do patvar n

506 do patvar n

506 update_term liftPats

507 update_term liftPats

@@ -611,7 +612,7 @@ elab ist info emode opts fn tm

611 ivs' <- get_instances

612 ivs' <- get_instances

612 env <- get_env

613 env <- get_env

613 elabE (ina { e_inarg = True }) (Just fc) sc

614 elabE (ina { e_inarg = True }) (Just fc) sc

614− when (not pattern) $

615+ when (not (pattern || intransform)) $

615 mapM_ (\n -> do focus n

616 mapM_ (\n -> do focus n

616 g <- goal

617 g <- goal

617 hs <- get_holes

618 hs <- get_holes

@@ -799,7 +800,7 @@ elab ist info emode opts fn tm

799 -- to be needed.

800 -- to be needed.

800 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

801 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

801 implicitApp elab

802 implicitApp elab

802− | pattern = do elab; return ()

803+ | pattern || intransform = do elab; return ()

803 | otherwise

804 | otherwise

804 = do s <- get

805 = do s <- get

805 imps <- elab

806 imps <- elab

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

@@ -53,9 +53,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56+ logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)

56 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

57 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

57 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

58 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

58− (erun fc (buildTC i info ELHS [] (sUN "transform")

59+ (erun fc (buildTC i info ETransLHS [] (sUN "transform")

59 (infTerm lhs)))

60 (infTerm lhs)))

60 setContext ctxt'

61 setContext ctxt'

61 processTacticDecls info newDecls

62 processTacticDecls info newDecls

@@ -67,8 +68,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

67 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

68 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

68 let clhs_tm = renamepats pnames clhs_tm_in

69 let clhs_tm = renamepats pnames clhs_tm_in

69 logLvl 3 ("Transform LHS " ++ show clhs_tm)

70 logLvl 3 ("Transform LHS " ++ show clhs_tm)

70−

71+ logLvl 3 ("Transform type " ++ show clhs_ty)

72+

71 let rhs = addImplBound i (map fst newargs) rhs_in

73 let rhs = addImplBound i (map fst newargs) rhs_in

74+ logLvl 5 ("Transform RHS input: " ++ showTmImpls rhs)

75+

72 ((rhs', defer, ctxt', newDecls), _) <-

76 ((rhs', defer, ctxt', newDecls), _) <-

73 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

77 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

74 (do pbinds i lhs_tm

78 (do pbinds i lhs_tm

src/Idris/IBC.hs+4

@@ -948,6 +948,7 @@ instance Binary Totality where

948 put x1

949 Unchecked -> do putWord8 2

950 Productive -> do putWord8 3

951+ Generated -> do putWord8 4

951 get

952 get

952 = do i <- getWord8

953 = do i <- getWord8

953 case i of

954 case i of

@@ -957,6 +958,7 @@ instance Binary Totality where

957 return (Partial x1)

958 return (Partial x1)

958 2 -> return Unchecked

959 2 -> return Unchecked

959 3 -> return Productive

960 3 -> return Productive

961+ 4 -> return Generated

960 _ -> error "Corrupted binary data for Totality"

962 _ -> error "Corrupted binary data for Totality"

961

963

962instance Binary MetaInformation where

964instance Binary MetaInformation where

@@ -1007,6 +1009,7 @@ instance Binary FnOpt where

1007 CExport x1 -> do putWord8 14

1009 CExport x1 -> do putWord8 14

1008 put x1

1010 put x1

1009 AutoHint -> putWord8 15

1011 AutoHint -> putWord8 15

1012+ PEGenerated -> putWord8 16

1010 get

1013 get

1011 = do i <- getWord8

1014 = do i <- getWord8

1012 case i of

1015 case i of

@@ -1028,6 +1031,7 @@ instance Binary FnOpt where

1028 14 -> do x1 <- get

1031 14 -> do x1 <- get

1029 return $ CExport x1

1032 return $ CExport x1

1030 15 -> return AutoHint

1033 15 -> return AutoHint

1034+ 16 -> return PEGenerated

1031 _ -> error "Corrupted binary data for FnOpt"

1035 _ -> error "Corrupted binary data for FnOpt"

1032

1036

1033instance Binary Fixity where

1037instance Binary Fixity where

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/error004/FunErrTest.idr+2−1

@@ -17,7 +17,7 @@ cadr [] {cons1=Refl} {cons2=Refl} impossible

17

18extractList : TT -> Maybe TT

19extractList (App (App reflCon (App isCons lst)) _) = Just lst

20−extractList _ = Nothing

20+extractList t = Just t -- Nothing

21

22total

23has2elts : Err -> Maybe (List ErrorReportPart)

@@ -39,3 +39,4 @@ badCadr2 = cadr [1]

39

40goodCadr : Int

41goodCadr = cadr [1, 2]

42+

test/reg054/expected+4−3

@@ -2,9 +2,10 @@ reg054.idr:18:5:When checking left hand side of inf:

2When 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:

5−When checking argument x to Main.weird:

6− No explicit types on left hand side: Char

5+No 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

7−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:

8When checking an application of Main.tctrick:

9When checking an application of Main.tctrick:

9 Type mismatch between

10 Type mismatch between

10 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