ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 14:09:30 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'elab-lookup-function-def' of https://github.com/shlevy/Idris-dev into shlevy-elab-lookup-function-def

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-12-02 18:56:56 +01:00
commit 1527899e07
9 changed files with 29 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/AbsSyntaxTree.hs
View File

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

50
src/Idris/Coverage.hs
View File

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

4
src/Idris/Delaborate.hs
View File

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

6
src/Idris/Elab/Clause.hs
View File

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

15
src/Idris/Elab/Term.hs
View File

@ -1775,11 +1775,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 ()
@ -1800,16 +1800,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'

6
src/Idris/IBC.hs
View File

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

4
src/Idris/REPL.hs
View File

@ -1450,11 +1450,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) =

4
src/Idris/Reflection.hs
View File

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

15
test/meta004/meta004.idr
View File

@ -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')