9f3675a · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+2−2

compare with master

unifiedsplit

@@ -188,7 +188,7 @@ data IState = IState {

188 idris_optimisation :: Ctxt OptInfo,

189 idris_datatypes :: Ctxt TypeInfo,

190 idris_namehints :: Ctxt [Name],

191− idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported

191+ idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported

192 -- ^ list of lhs/rhs, and a list of missing clauses

193 idris_flags :: Ctxt [FnOpt],

194 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

@@ -717,7 +717,7 @@ data Directive = DLib Codegen String |

717-- | A set of instructions for things that need to happen in IState

718-- after a term elaboration when there's been reflected elaboration.

719data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

720− | RClausesInstrs Name [([Name], Term, Term)]

720+ | RClausesInstrs Name [([(Name, Term)], Term, Term)]

721 | RAddInstance Name Name

722

723-- | For elaborator state

src/Idris/Coverage.hs−50

@@ -351,56 +351,6 @@ checkPositive mut_ns (cn, ty')

351 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

352

353

354−calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

355−calcProd i fc topn pats

356− = cp topn pats []

357− where

358− -- every application of n must be in an argument of a coinductive

359− -- constructor, in every function reachable from here in the

360− -- call graph.

361− cp n pats done = do patsprod <- mapM (prodRec n done) pats

362− if (and patsprod)

363− then return Productive

364− else return (Partial NotProductive)

365−

366− prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool

367− prodRec n done _ | n `elem` done = return True

368− prodRec n done (_, _, tm) = prod n done False (delazy' True tm)

369−

370− prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

371− prod n done ok ap@(App _ _ _)

372− | (P nt f _, args) <- unApply ap

373− = do recOK <- checkProdRec (n:done) f

374− let ctxt = tt_ctxt i

375− let [ty] = lookupTy f ctxt -- must exist!

376− let co = cotype nt f ty in

377− if (not recOK) then return False else

378− if f == topn

379− then do argsprod <- mapM (prod n done co) args

380− return (and (ok : argsprod) )

381− else do argsprod <- mapM (prod n done co) args

382− return (and argsprod)

383− prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)

384− (prod n done False a)

385− prod n done ok (Bind _ (Let t v) sc)

386− = liftM2 (&&) (prod n done False v) (prod n done False v)

387− prod n done ok (Bind _ b sc) = prod n done ok sc

388− prod n done ok t = return True

389−

390− checkProdRec :: [Name] -> Name -> Idris Bool

391− checkProdRec done f

392− = case lookupCtxt f (idris_patdefs i) of

393− [(def, _)] -> do ok <- mapM (prodRec f done) def

394− return (and ok)

395− _ -> return True -- defined elsewhere, can't call topn

396−

397− cotype (DCon _ _ _) n ty

398− | (P _ t _, _) <- unApply (getRetTy ty)

399− = case lookupCtxt t (idris_datatypes i) of

400− [TI _ True _ _ _] -> True

401− _ -> False

402− cotype nt n ty = False

403−

404-- | Calculate the totality of a function from its patterns.

354-- | Calculate the totality of a function from its patterns.

405-- Either follow the size change graph (if inductive) or check for

355-- Either follow the size change graph (if inductive) or check for

406-- productivity (if coinductive)

356-- productivity (if coinductive)

src/Idris/Delaborate.hs+2−2

@@ -204,8 +204,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

204 [(cases, _)] -> return cases

205 _ -> Nothing

206 return $ PCase un (de env imps scrutinee)

207− [ (de (env ++ map (\n -> (n, n)) vars) imps (splitArg lhs),

207+ [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),

208− de (env ++ map (\n -> (n, n)) vars) imps rhs)

208+ de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)

209 | (vars, lhs, rhs) <- cases

210 ]

211 where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

src/Idris/Elab/Clause.hs+3−3

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

133

134 -- pdef is the compile-time pattern definition.

135 -- This will get further inlined to help with totality checking.

136− let pdef = map debind pats_raw

136+ let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw

137 -- pdef_pe is the one which will get further optimised

138 -- for run-time, and, partially evaluated

139 let pdef_pe = map debind pats_transformed

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

182

183 -- pdef' is the version that gets compiled for run-time,

184 -- so we start from the partially evaluated version

185− pdef_in' <- applyOpts pdef_pe

185+ pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe

186 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

187

188 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

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

289 debind (Left x) = let (vs, x') = depat [] x in

290 (vs, x', Impossible)

291

292− depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)

292+ depat acc (Bind n (PVar t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)

293 depat acc x = (acc, x)

294

295

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

@@ -1763,11 +1763,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1763

1764 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)

1765

1766− patvars :: [Name] -> Term -> ([Name], Term)

1766+ patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)

1767− patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)

1767+ patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)

1768 patvars ns tm = (ns, tm)

1769

1770− pullVars :: (Term, Term) -> ([Name], Term, Term)

1770+ pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)

1771 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1772

1773 defineFunction :: RFunDefn Raw -> ElabD ()

@@ -1788,16 +1788,17 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1788 Left lhs -> let (ns, lhs') = patvars [] lhs'

1789 in (ns, lhs', Impossible))

1790 clauses'

1791+ let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''

1791 ctxt'<- lift $

1792 ctxt'<- lift $

1792 addCasedef n (const [])

1793 addCasedef n (const [])

1793 info False (STerm Erased)

1794 info False (STerm Erased)

1794 True False -- TODO what are these?

1795 True False -- TODO what are these?

1795 (map snd $ getArgTys ty) [] -- TODO inaccessible types

1796 (map snd $ getArgTys ty) [] -- TODO inaccessible types

1796 clauses'

1797 clauses'

1797− clauses''

1798+ clauses'''

1798− clauses''

1799+ clauses'''

1799− clauses''

1800+ clauses'''

1800− clauses''

1801+ clauses'''

1801 ty

1802 ty

1802 ctxt

1803 ctxt

1803 set_context ctxt'

1804 set_context ctxt'

src/Idris/IBC.hs+3−3

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 127

43+ibcVersion = 128

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -80,7 +80,7 @@ data IBCFile = IBCFile { ver :: Word16,

80 ibc_errorhandlers :: ![Name],

81 ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

82 ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],

83− ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

83+ ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))],

84 ibc_postulates :: ![Name],

85 ibc_externs :: ![(Name, Int)],

86 ibc_parsedSpan :: !(Maybe FC),

@@ -505,7 +505,7 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

505pHdrs :: [(Codegen, String)] -> Idris ()

506pHdrs hs = mapM_ (uncurry addHdr) hs

507

508−pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

508+pPatdefs :: [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris ()

509pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->

510 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds

511

src/Idris/REPL.hs+2−2

@@ -1449,11 +1449,11 @@ pprintDef n =

1449 return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++

1450 map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++

1451 map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))

1452− where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation

1452+ where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation

1453 ppDef amb ist (n, (clauses, missing)) =

1454 prettyName True amb [] n <+> colon <+>

1455 align (pprintDelabTy ist n) <$>

1456− ppClauses ist clauses <> ppMissing missing

1456+ ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing

1457 ppClauses ist [] = text "No clauses."

1458 ppClauses ist cs = vsep (map pp cs)

1459 where pp (vars, lhs, rhs) =

src/Idris/Reflection.hs+2−2

@@ -1088,9 +1088,9 @@ buildFunDefns ist n =

1088

1089 mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs

1090 mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs

1091− mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

1091+ mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

1092 bind Impossible = Impossible

1093− bind tm = Bind n (PVar Erased) tm

1093+ bind tm = Bind n (PVar ty) tm

1094

1095-- | Build the reflected datatype definition(s) that correspond(s) to

1096-- a provided unqualified name

test/meta004/meta004.idr+7−8

@@ -1,19 +1,18 @@

1import Language.Reflection.Utils

2import Pruviloj.Core

3

4−forgotToNatAndRename : TTName -> TTName -> Raw -> Raw

4+rename : TTName -> TTName -> Raw -> Raw

5−forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body)

5+rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)

6−forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg)

6+rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)

7−forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat}

8−forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n

7+rename old new (Var n) = if n == old then Var new else Var n

9−forgotToNatAndRename old new tm = tm

8+rename old new tm = tm

10

9

11roundtrip : TTName -> TTName -> Elab ()

10roundtrip : TTName -> TTName -> Elab ()

12roundtrip old new = do

11roundtrip old new = do

13 DefineFun _ clauses <- lookupFunDefnExact old

12 DefineFun _ clauses <- lookupFunDefnExact old

14 clauses' <- for clauses (\(MkFunClause lhs rhs) => do

13 clauses' <- for clauses (\(MkFunClause lhs rhs) => do

15− lhs' <- forgotToNatAndRename old new <$> forget lhs

14+ lhs' <- rename old new <$> forget lhs

16− rhs' <- forgotToNatAndRename old new <$> forget rhs

15+ rhs' <- rename old new <$> forget rhs

17 pure $ MkFunClause lhs' rhs')

16 pure $ MkFunClause lhs' rhs')

18 defineFunction (DefineFun new clauses')

17 defineFunction (DefineFun new clauses')

19

18