edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-30 22:05:32 +03:00
Code Issues Projects Releases Wiki Activity

Cosmetic changes in src/Compiler/Inline

Browse Source 
Refactor LengthMatch into its own file
This commit is contained in:
André Videla 2020-01-09 22:12:01 +00:00
parent 7cde0a7255
commit a145ba99d7
4 changed files with 46 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
src/Compiler/Inline.idr
View File

@ -6,6 +6,7 @@ import Core.FC
import Core.TT
import Data.Vect
import Data.LengthMatch
%default covering
@ -21,18 +22,6 @@ weakenNsEnv : (xs : List Name) -> EEnv free vars -> EEnv (xs ++ free) vars
weakenNsEnv [] env = env
weakenNsEnv (x :: xs) env = weakenEnv (weakenNsEnv xs env)
-- TODO: This is in CaseBuilder too, so tidy it up...
data LengthMatch : List a -> List b -> Type where
NilMatch : LengthMatch [] []
ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
checkLengthMatch [] [] = Just NilMatch
checkLengthMatch [] (x :: xs) = Nothing
checkLengthMatch (x :: xs) [] = Nothing
checkLengthMatch (x :: xs) (y :: ys)
= Just (ConsMatch !(checkLengthMatch xs ys))
extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->
LengthMatch args args' -> EEnv free (args' ++ vars)
extend env [] [] NilMatch = env
@ -128,11 +117,7 @@ mutual
eval rec env stk (CCon fc n t args)
= pure $ unload stk $ CCon fc n t !(traverse (eval rec env []) args)
eval rec env stk (COp fc p args)
= pure $ unload stk $ COp fc p !(mapV (eval rec env []) args)
where
mapV : (a -> Core b) -> Vect n a -> Core (Vect n b)
mapV f [] = pure []
mapV f (x :: xs) = pure $ !(f x) :: !(mapV f xs)
= pure $ unload stk $ COp fc p !(traverseVect (eval rec env []) args)
eval rec env stk (CExtPrim fc p args)
= pure $ unload stk $ CExtPrim fc p !(traverse (eval rec env []) args)
eval rec env stk (CForce fc e)
@ -143,28 +128,18 @@ mutual
= pure $ unload stk (CDelay fc !(eval rec env [] e))
eval rec env stk (CConCase fc sc alts def)
= do sc' <- eval rec env [] sc
case !(pickAlt rec env stk sc' alts def) of
Nothing =>
do def' <- case def of
Nothing => pure Nothing
Just d => pure (Just !(eval rec env stk d))
pure $
CConCase fc sc'
!(traverse (evalAlt fc rec env stk) alts)
def'
Just val => pure val
Nothing <- pickAlt rec env stk sc' alts def | Just val => pure val
def' <- traverseOpt (eval rec env stk) def
pure $ CConCase fc sc'
!(traverse (evalAlt fc rec env stk) alts)
def'
eval rec env stk (CConstCase fc sc alts def)
= do sc' <- eval rec env [] sc
case !(pickConstAlt rec env stk sc' alts def) of
Nothing =>
do def' <- case def of
Nothing => pure Nothing
Just d => pure (Just !(eval rec env stk d))
pure $
CConstCase fc sc'
!(traverse (evalConstAlt rec env stk) alts)
def'
Just val => pure val
Nothing <- pickConstAlt rec env stk sc' alts def | Just val => pure val
def' <- traverseOpt (eval rec env stk) def
pure $ CConstCase fc sc'
!(traverse (evalConstAlt rec env stk) alts)
def'
eval rec env stk (CPrimVal fc c) = pure $ unload stk $ CPrimVal fc c
eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc
eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str
@ -182,7 +157,7 @@ mutual
List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->
Core (CConstAlt free)
evalConstAlt rec env stk (MkConstAlt c sc)
= pure $ MkConstAlt c !(eval rec env stk sc)
= MkConstAlt c <$> eval rec env stk sc
pickAlt : {auto c : Ref Ctxt Defs} ->
List Name -> EEnv free vars -> Stack free ->
@ -190,9 +165,7 @@ mutual
Maybe (CExp (vars ++ free)) ->
Core (Maybe (CExp free))
pickAlt rec env stk (CCon fc n t args) [] def
= case def of
Nothing => pure Nothing
Just d => pure $ Just !(eval rec env stk d)
= traverseOpt (eval rec env stk) def
pickAlt {vars} {free} rec env stk (CCon fc n t args) (MkConAlt n' t' args' sc :: alts) def
= if t == t'
then case checkLengthMatch args args' of
@ -212,18 +185,16 @@ mutual
Maybe (CExp (vars ++ free)) ->
Core (Maybe (CExp free))
pickConstAlt rec env stk (CPrimVal fc c) [] def
= case def of
Nothing => pure Nothing
Just d => pure $ Just !(eval rec env stk d)
= traverseOpt (eval rec env stk) def
pickConstAlt {vars} {free} rec env stk (CPrimVal fc c) (MkConstAlt c' sc :: alts) def
= if c == c'
then pure $ Just !(eval rec env stk sc)
then Just <$> eval rec env stk sc
else pickConstAlt rec env stk (CPrimVal fc c) alts def
pickConstAlt rec env stk _ _ _ = pure Nothing
inline : {auto c : Ref Ctxt Defs} ->
CDef -> Core CDef
inline (MkFun args exp) = pure $ MkFun args !(eval [] [] [] exp)
inline (MkFun args exp) = MkFun args <$> eval [] [] [] exp
inline d = pure d
export
@ -231,14 +202,7 @@ inlineDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
inlineDef n
= do defs <- get Ctxt
case !(lookupCtxtExact n (gamma defs)) of
Nothing => pure ()
Just def =>
case compexpr def of
Nothing => pure ()
Just cexpr =>
do -- coreLift $ putStrLn $ show (fullname def) ++ " before: " ++ show cexpr
inlined <- inline cexpr
-- coreLift $ putStrLn $ show (fullname def) ++ " after: " ++ show inlined
setCompiled n inlined
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(inline cexpr)

13
src/Core/CaseBuilder.idr
View File

@ -8,6 +8,8 @@ import Core.Normalise
import Core.TT
import Core.Value
import Data.LengthMatch
%default covering
public export
@ -187,17 +189,6 @@ substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs
= do pats' <- substInPats fc a (mkTerm vars pat) pats
pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs)
data LengthMatch : List a -> List b -> Type where
NilMatch : LengthMatch [] []
ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
checkLengthMatch [] [] = Just NilMatch
checkLengthMatch [] (x :: xs) = Nothing
checkLengthMatch (x :: xs) [] = Nothing
checkLengthMatch (x :: xs) (y :: ys)
= Just (ConsMatch !(checkLengthMatch xs ys))
data Partitions : List (PatClause vars todo) -> Type where
ConClauses : (cs : List (PatClause vars todo)) ->
Partitions ps -> Partitions (cs ++ ps)

10
src/Core/Core.idr
View File

@ -2,6 +2,7 @@ module Core.Core
import Core.Env
import Core.TT
import Data.Vect
import Parser.Support
import public Control.Catchable
@ -353,6 +354,10 @@ export %inline
map : (a -> b) -> Core a -> Core b
map f (MkCore a) = MkCore (map (map f) a)
export %inline
(<$>) : (a -> b) -> Core a -> Core b
(<$>) f (MkCore a) = MkCore (map (map f) a)
-- Monad (specialised)
export %inline
(>>=) : Core a -> (a -> Core b) -> Core b
@ -395,6 +400,11 @@ export
traverse : (a -> Core b) -> List a -> Core (List b)
traverse f xs = traverse' f xs []
export
traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
traverseVect f [] = pure []
traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]
export
traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
traverseOpt f Nothing = pure Nothing

14
src/Data/LengthMatch.idr Normal file
View File

@ -0,0 +1,14 @@
module Data.LengthMatch
public export
data LengthMatch : List a -> List b -> Type where
NilMatch : LengthMatch [] []
ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
export
checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
checkLengthMatch [] [] = Just NilMatch
checkLengthMatch [] (x :: xs) = Nothing
checkLengthMatch (x :: xs) [] = Nothing
checkLengthMatch (x :: xs) (y :: ys)
= Just (ConsMatch !(checkLengthMatch xs ys))