From 9f3675a815f52f43db5c004ab36d06d16711869e Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Wed, 2 Dec 2015 11:29:10 -0500 Subject: [PATCH] Store patvar binding types in idris_patdefs --- src/Idris/AbsSyntaxTree.hs | 4 +-- src/Idris/Coverage.hs | 50 -------------------------------------- src/Idris/Delaborate.hs | 4 +-- src/Idris/Elab/Clause.hs | 6 ++--- src/Idris/Elab/Term.hs | 15 ++++++------ src/Idris/IBC.hs | 6 ++--- src/Idris/REPL.hs | 4 +-- src/Idris/Reflection.hs | 4 +-- test/meta004/meta004.idr | 15 ++++++------ 9 files changed, 29 insertions(+), 79 deletions(-) diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index fadca5b67..41d89cddd 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -188,7 +188,7 @@ data IState = IState { idris_optimisation :: Ctxt OptInfo, idris_datatypes :: Ctxt TypeInfo, idris_namehints :: Ctxt [Name], - idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported + idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported -- ^ list of lhs/rhs, and a list of missing clauses idris_flags :: Ctxt [FnOpt], idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos @@ -717,7 +717,7 @@ data Directive = DLib Codegen String | -- | A set of instructions for things that need to happen in IState -- after a term elaboration when there's been reflected elaboration. data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type - | RClausesInstrs Name [([Name], Term, Term)] + | RClausesInstrs Name [([(Name, Term)], Term, Term)] | RAddInstance Name Name -- | For elaborator state diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs index 4caa9da3f..2cdec3bd7 100644 --- a/src/Idris/Coverage.hs +++ b/src/Idris/Coverage.hs @@ -351,56 +351,6 @@ checkPositive mut_ns (cn, ty') noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg) -calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality -calcProd i fc topn pats - = cp topn pats [] - where - -- every application of n must be in an argument of a coinductive - -- constructor, in every function reachable from here in the - -- call graph. - cp n pats done = do patsprod <- mapM (prodRec n done) pats - if (and patsprod) - then return Productive - else return (Partial NotProductive) - - prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool - prodRec n done _ | n `elem` done = return True - prodRec n done (_, _, tm) = prod n done False (delazy' True tm) - - prod :: Name -> [Name] -> Bool -> Term -> Idris Bool - prod n done ok ap@(App _ _ _) - | (P nt f _, args) <- unApply ap - = do recOK <- checkProdRec (n:done) f - let ctxt = tt_ctxt i - let [ty] = lookupTy f ctxt -- must exist! - let co = cotype nt f ty in - if (not recOK) then return False else - if f == topn - then do argsprod <- mapM (prod n done co) args - return (and (ok : argsprod) ) - else do argsprod <- mapM (prod n done co) args - return (and argsprod) - prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f) - (prod n done False a) - prod n done ok (Bind _ (Let t v) sc) - = liftM2 (&&) (prod n done False v) (prod n done False v) - prod n done ok (Bind _ b sc) = prod n done ok sc - prod n done ok t = return True - - checkProdRec :: [Name] -> Name -> Idris Bool - checkProdRec done f - = case lookupCtxt f (idris_patdefs i) of - [(def, _)] -> do ok <- mapM (prodRec f done) def - return (and ok) - _ -> return True -- defined elsewhere, can't call topn - - cotype (DCon _ _ _) n ty - | (P _ t _, _) <- unApply (getRetTy ty) - = case lookupCtxt t (idris_datatypes i) of - [TI _ True _ _ _] -> True - _ -> False - cotype nt n ty = False - -- | Calculate the totality of a function from its patterns. -- Either follow the size change graph (if inductive) or check for -- productivity (if coinductive) diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs index 31f0736f3..e512647df 100644 --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -204,8 +204,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm [(cases, _)] -> return cases _ -> Nothing return $ PCase un (de env imps scrutinee) - [ (de (env ++ map (\n -> (n, n)) vars) imps (splitArg lhs), - de (env ++ map (\n -> (n, n)) vars) imps rhs) + [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs), + de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs) | (vars, lhs, rhs) <- cases ] where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args) diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index c53dcca8e..caf442402 100644 --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -133,7 +133,7 @@ elabClauses info' fc opts n_in cs = -- pdef is the compile-time pattern definition. -- This will get further inlined to help with totality checking. - let pdef = map debind pats_raw + let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw -- pdef_pe is the one which will get further optimised -- for run-time, and, partially evaluated let pdef_pe = map debind pats_transformed @@ -182,7 +182,7 @@ elabClauses info' fc opts n_in cs = -- pdef' is the version that gets compiled for run-time, -- so we start from the partially evaluated version - pdef_in' <- applyOpts pdef_pe + pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in' logLvl 5 $ "After data structure transformations:\n" ++ show pdef' @@ -289,7 +289,7 @@ elabClauses info' fc opts n_in cs = debind (Left x) = let (vs, x') = depat [] x in (vs, x', Impossible) - depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc) + depat acc (Bind n (PVar t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc) depat acc x = (acc, x) diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs index a42745abc..fd9728690 100644 --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -1763,11 +1763,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased) - patvars :: [Name] -> Term -> ([Name], Term) - patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc) + patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term) + patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc) patvars ns tm = (ns, tm) - pullVars :: (Term, Term) -> ([Name], Term, Term) + pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term) pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs defineFunction :: RFunDefn Raw -> ElabD () @@ -1788,16 +1788,17 @@ runElabAction ist fc env tm ns = do tm' <- eval tm Left lhs -> let (ns, lhs') = patvars [] lhs' in (ns, lhs', Impossible)) clauses' + let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses'' ctxt'<- lift $ addCasedef n (const []) info False (STerm Erased) True False -- TODO what are these? (map snd $ getArgTys ty) [] -- TODO inaccessible types clauses' - clauses'' - clauses'' - clauses'' - clauses'' + clauses''' + clauses''' + clauses''' + clauses''' ty ctxt set_context ctxt' diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index 37bfb1759..33df829d1 100644 --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -40,7 +40,7 @@ import System.Directory import Codec.Archive.Zip ibcVersion :: Word16 -ibcVersion = 127 +ibcVersion = 128 data IBCFile = IBCFile { ver :: Word16, sourcefile :: FilePath, @@ -80,7 +80,7 @@ data IBCFile = IBCFile { ver :: Word16, ibc_errorhandlers :: ![Name], ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))], - ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))], + ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))], ibc_postulates :: ![Name], ibc_externs :: ![(Name, Int)], ibc_parsedSpan :: !(Maybe FC), @@ -505,7 +505,7 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls pHdrs :: [(Codegen, String)] -> Idris () pHdrs hs = mapM_ (uncurry addHdr) hs -pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris () +pPatdefs :: [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris () pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i -> i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 9610a5418..8fe35ef7d 100644 --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -1449,11 +1449,11 @@ pprintDef n = return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++ map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt)) - where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation + where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation ppDef amb ist (n, (clauses, missing)) = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n) <$> - ppClauses ist clauses <> ppMissing missing + ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing ppClauses ist [] = text "No clauses." ppClauses ist cs = vsep (map pp cs) where pp (vars, lhs, rhs) = diff --git a/src/Idris/Reflection.hs b/src/Idris/Reflection.hs index e0a9f6623..02c0bf667 100644 --- a/src/Idris/Reflection.hs +++ b/src/Idris/Reflection.hs @@ -1088,9 +1088,9 @@ buildFunDefns ist n = mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs - mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where + mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where bind Impossible = Impossible - bind tm = Bind n (PVar Erased) tm + bind tm = Bind n (PVar ty) tm -- | Build the reflected datatype definition(s) that correspond(s) to -- a provided unqualified name diff --git a/test/meta004/meta004.idr b/test/meta004/meta004.idr index 609e5245f..aa2c91d2c 100644 --- a/test/meta004/meta004.idr +++ b/test/meta004/meta004.idr @@ -1,19 +1,18 @@ import Language.Reflection.Utils import Pruviloj.Core -forgotToNatAndRename : TTName -> TTName -> Raw -> Raw -forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body) -forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg) -forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat} -forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n -forgotToNatAndRename old new tm = tm +rename : TTName -> TTName -> Raw -> Raw +rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body) +rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg) +rename old new (Var n) = if n == old then Var new else Var n +rename old new tm = tm roundtrip : TTName -> TTName -> Elab () roundtrip old new = do DefineFun _ clauses <- lookupFunDefnExact old clauses' <- for clauses (\(MkFunClause lhs rhs) => do - lhs' <- forgotToNatAndRename old new <$> forget lhs - rhs' <- forgotToNatAndRename old new <$> forget rhs + lhs' <- rename old new <$> forget lhs + rhs' <- rename old new <$> forget rhs pure $ MkFunClause lhs' rhs') defineFunction (DefineFun new clauses')