bfacfbc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better partial evaluation of polymorphic HOFs

Need to make sure types constructors are stripped on the LHS or they won't get past the elaborator.

commitbfacfbc85e0ea9f0d81de90e541b9182e8985660 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 6 Jun 2015, 12:04 (11 years ago) parent7f20feb

5 files changed+19−5

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−1 src/Idris/Elab/Clause.hs+6−2 src/Idris/PartialEval.hs+2−1 test/reg054/expected+3−1 test/reg054/reg054.idr+3

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

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

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

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

374374 showSep "\n"

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

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

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

377377 showTmImpls rhs)) (pe_clauses specdecl))

378378

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

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

381381

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

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

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

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

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

385386 (pe_clauses specdecl)

386387 trans <- elabTransform info fc False rhs lhs

387388 elabClauses info fc (PEGenerated:opts) newnm def

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

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

394395 return [])

395396

397+ hiddenToPH (PHidden _) = Placeholder

398+ hiddenToPH x = x

399+

396400 specName simpl (ImplicitS, tm)

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

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

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/reg054/expected+3−1

@@ -3,7 +3,9 @@ When 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:

55No explicit types on left hand side: Char

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

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:

79When checking an application of Main.tctrick:

810 Type mismatch between

911 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