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

git.iko.soy/Idris-dev

Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical

commit9056a4a1fef3c111ec1e3952dc8490ac7efaaf4f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 7 Jun 2015, 13:28 (11 years ago) parentcb1805b 76b39b1

12 files changed+52−23

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/Evaluate.hs+2 src/Idris/Elab/Clause.hs+13−8 src/Idris/Elab/Term.hs+8−7 src/Idris/Elab/Transform.hs+6−2 src/Idris/IBC.hs+4 src/Idris/PartialEval.hs+2−1 test/error004/FunErrTest.idr+2−1 test/reg054/expected+4−3 test/reg054/reg054.idr+3

src/Idris/AbsSyntax.hs+6−1

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

18151815stripUnmatchable :: IState -> PTerm -> PTerm

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

18171817 su :: PTerm -> PTerm

1818− su (PRef fc f)

1818+ su tm@(PRef fc f)

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

18201820 = Placeholder

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

1822+ = PHidden tm

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

1824+ = PHidden tm

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

18221826 -- here we use canBeDConName because the impossible pattern

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

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

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

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

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

18381843 su t = t

18391844

18401845 ctxt = tt_ctxt i

src/Idris/AbsSyntaxTree.hs+1

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

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

574574 | Constructor -- Data constructor type

575575 | AutoHint -- use in auto implicit search

576+ | PEGenerated -- generated by partial evaluator

576577 deriving (Show, Eq)

577578{-!

578579deriving instance Binary FnOpt

src/Idris/Core/DeepSeq.hs+1

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

198198 rnf Productive = ()

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

200200 rnf Unchecked = ()

201+ rnf Generated = ()

201202

202203instance NFData PReason where

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

src/Idris/Core/Evaluate.hs+2

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

740740 | Productive -- ^ productive

741741 | Partial PReason

742742 | Unchecked

743+ | Generated

743744 deriving Eq

744745{-!

745746deriving instance NFData Totality

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

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

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

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

771+ show Generated = "auto-generated"

770772

771773{-!

772774deriving instance Binary Accessibility

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

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

189189

190190 ist <- getIState

191191 -- let wf = wellFounded ist n sc

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

193− then Unchecked -- finish checking later

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

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

193+ | PEGenerated `elem` opts = Generated

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

195195

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

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

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

241241 setContext ctxt'

242242 addIBC (IBCDef n)

243243 setTotality n tot

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

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

245+ do totcheck (fc, n)

245246 defer_totcheck (fc, n)

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

247248 i <- getIState

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

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

373374 showSep "\n"

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

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

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

376377 showTmImpls rhs)) (pe_clauses specdecl))

377378

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

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

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

380381

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

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

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

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

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

384386 (pe_clauses specdecl)

385387 trans <- elabTransform info fc False rhs lhs

386− elabClauses info fc opts newnm def

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

387389 return [trans]

388390 else return [])

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

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

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

393395 return [])

394396

397+ hiddenToPH (PHidden _) = Placeholder

398+ hiddenToPH x = x

399+

395400 specName simpl (ImplicitS, tm)

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

397402 specName simpl (ExplicitS, tm)

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

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

3535

3636import Debug.Trace

3737

38−data ElabMode = ETyDecl | ELHS | ERHS

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

3939 deriving Eq

4040

4141

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

220220 sequence_ (get_delayed_elab est)

221221 end_unify

222222 ptm <- get_term

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

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

224224 (do update_term orderPats

225225 unify_all

226226 matchProblems False -- only the ones we matched earlier

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

228228 mkPat)

229229 where

230230 pattern = emode == ELHS

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

231+ intransform = emode == ETransLHS

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

232233

233234 get_delayed_elab est =

234235 let ds = delayed_elab est in

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

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

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

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

493494 = do let ina = e_inarg ec

494495 guarded = e_guarded ec

495496 inty = e_intype ec

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

500501 _ -> True

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

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

503− if (tcname n && ina)

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

504505 then erun fc $

505506 do patvar n

506507 update_term liftPats

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

611612 ivs' <- get_instances

612613 env <- get_env

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

614− when (not pattern) $

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

615616 mapM_ (\n -> do focus n

616617 g <- goal

617618 hs <- get_holes

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

799800 -- to be needed.

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

801802 implicitApp elab

802− | pattern = do elab; return ()

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

803804 | otherwise

804805 = do s <- get

805806 imps <- elab

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

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

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

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

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

5758 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")

5960 (infTerm lhs)))

6061 setContext ctxt'

6162 processTacticDecls info newDecls

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

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

6869 let clhs_tm = renamepats pnames clhs_tm_in

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

70−

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

72+

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

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

75+

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

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

7478 (do pbinds i lhs_tm

src/Idris/IBC.hs+4

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

948948 put x1

949949 Unchecked -> do putWord8 2

950950 Productive -> do putWord8 3

951+ Generated -> do putWord8 4

951952 get

952953 = do i <- getWord8

953954 case i of

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

957958 return (Partial x1)

958959 2 -> return Unchecked

959960 3 -> return Productive

961+ 4 -> return Generated

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

961963

962964instance Binary MetaInformation where

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

10071009 CExport x1 -> do putWord8 14

10081010 put x1

10091011 AutoHint -> putWord8 15

1012+ PEGenerated -> putWord8 16

10101013 get

10111014 = do i <- getWord8

10121015 case i of

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

10281031 14 -> do x1 <- get

10291032 return $ CExport x1

10301033 15 -> return AutoHint

1034+ 16 -> return PEGenerated

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

10321036

10331037instance 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)

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

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

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

200+

200201mkNewPats ist d ns newname sname lhs rhs =

201202 PEDecl lhs rhs (map mkClause d) False

202203 where

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

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

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

237238 mkSubst _ = Nothing

238−

239+

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

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

241242-- application of the function to be specialised.

test/error004/FunErrTest.idr+2−1

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

1717

1818extractList : TT -> Maybe TT

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

20−extractList _ = Nothing

20+extractList t = Just t -- Nothing

2121

2222total

2323has2elts : Err -> Maybe (List ErrorReportPart)

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

3939

4040goodCadr : Int

4141goodCadr = cadr [1, 2]

42+

test/reg054/expected+4−3

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

22When checking an application of constructor Main.MkInfer:

33 Attempting concrete match on polymorphic argument: 0

44reg054.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

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

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

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

89When checking an application of Main.tctrick:

910 Type mismatch between

1011 Maybe a1 (Type of Just x)

test/reg054/reg054.idr+3

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

3333weird : Weird x -> x

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

3535

36+weird' : Weird x -> x

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

38+

3639tctrick : a -> Int

3740tctrick (Just x) = x

3841tctrick Nothing = 42