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

src/Idris/AbsSyntaxTree.hs+2−2

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

188188 idris_optimisation :: Ctxt OptInfo,

189189 idris_datatypes :: Ctxt TypeInfo,

190190 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

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

193193 idris_flags :: Ctxt [FnOpt],

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

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

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

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

719719data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

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

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

721721 | RAddInstance Name Name

722722

723723-- | For elaborator state

src/Idris/Coverage.hs−50

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

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

352352

353353

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−

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

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

406356-- productivity (if coinductive)

src/Idris/Delaborate.hs+2−2

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

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

205205 _ -> Nothing

206206 return $ PCase un (de env imps scrutinee)

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

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

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

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

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

210210 ]

211211 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 =

133133

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

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

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

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

139139 let pdef_pe = map debind pats_transformed

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

182182

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

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

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

187187

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

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

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

290290 (vs, x', Impossible)

291291

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)

293293 depat acc x = (acc, x)

294294

295295

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

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

17631763

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

17651765

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

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

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

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

17681768 patvars ns tm = (ns, tm)

17691769

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

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

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

17721772

17731773 defineFunction :: RFunDefn Raw -> ElabD ()

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

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

17891789 in (ns, lhs', Impossible))

17901790 clauses'

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

17911792 ctxt'<- lift $

17921793 addCasedef n (const [])

17931794 info False (STerm Erased)

17941795 True False -- TODO what are these?

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

17961797 clauses'

1797− clauses''

1798− clauses''

1799− clauses''

1800− clauses''

1798+ clauses'''

1799+ clauses'''

1800+ clauses'''

1801+ clauses'''

18011802 ty

18021803 ctxt

18031804 set_context ctxt'

src/Idris/IBC.hs+3−3

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 127

43+ibcVersion = 128

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

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

8080 ibc_errorhandlers :: ![Name],

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

8282 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]))],

8484 ibc_postulates :: ![Name],

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

8686 ibc_parsedSpan :: !(Maybe FC),

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

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

506506pHdrs hs = mapM_ (uncurry addHdr) hs

507507

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

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

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

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

511511

src/Idris/REPL.hs+2−2

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

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

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

14511451 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

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

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

14551455 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

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

14581458 ppClauses ist cs = vsep (map pp cs)

14591459 where pp (vars, lhs, rhs) =

src/Idris/Reflection.hs+2−2

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

10881088

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

10901090 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

10921092 bind Impossible = Impossible

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

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

10941094

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

10961096-- a provided unqualified name

test/meta004/meta004.idr+7−8

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

11import Language.Reflection.Utils

22import Pruviloj.Core

33

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

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

6−forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename 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

9−forgotToNatAndRename old new tm = tm

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

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

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

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

8+rename old new tm = tm

109

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

1211roundtrip old new = do

1312 DefineFun _ clauses <- lookupFunDefnExact old

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

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

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

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

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

1716 pure $ MkFunClause lhs' rhs')

1817 defineFunction (DefineFun new clauses')

1918