1{-# LANGUAGE PatternSynonyms #-} 2 3-- | The treeless syntax is intended to be used as input for the compiler backends. 4-- It is more low-level than Internal syntax and is not used for type checking. 5-- 6-- Some of the features of treeless syntax are: 7-- - case expressions instead of case trees 8-- - no instantiated datatypes / constructors 9module Agda.Syntax.Treeless 10 ( module Agda.Syntax.Abstract.Name 11 , module Agda.Syntax.Treeless 12 ) where 13 14import Control.Arrow (first, second) 15import Control.DeepSeq 16 17import Data.Data (Data) 18import Data.Word 19 20import GHC.Generics (Generic) 21 22import Agda.Syntax.Position 23import Agda.Syntax.Literal 24import Agda.Syntax.Common 25import Agda.Syntax.Abstract.Name 26 27data Compiled = Compiled 28 { cTreeless :: TTerm 29 , cArgUsage :: Maybe [ArgUsage] 30 -- ^ 'Nothing' if treeless usage analysis has not run yet. 31 } 32 deriving (Data, Show, Eq, Ord, Generic) 33 34-- | Usage status of function arguments in treeless code. 35data ArgUsage 36 = ArgUsed 37 | ArgUnused 38 deriving (Data, Show, Eq, Ord, Generic) 39 40-- | The treeless compiler can behave differently depending on the target 41-- language evaluation strategy. For instance, more aggressive erasure for 42-- lazy targets. 43data EvaluationStrategy = LazyEvaluation | EagerEvaluation 44 deriving (Eq, Show) 45 46type Args = [TTerm] 47 48-- this currently assumes that TApp is translated in a lazy/cbn fashion. 49-- The AST should also support strict translation. 50-- 51-- All local variables are using de Bruijn indices. 52data TTerm = TVar Int 53 | TPrim TPrim 54 | TDef QName 55 | TApp TTerm Args 56 | TLam TTerm 57 | TLit Literal 58 | TCon QName 59 | TLet TTerm TTerm 60 -- ^ introduces a new local binding. The bound term 61 -- MUST only be evaluated if it is used inside the body. 62 -- Sharing may happen, but is optional. 63 -- It is also perfectly valid to just inline the bound term in the body. 64 | TCase Int CaseInfo TTerm [TAlt] 65 -- ^ Case scrutinee (always variable), case type, default value, alternatives 66 -- First, all TACon alternatives are tried; then all TAGuard alternatives 67 -- in top to bottom order. 68 -- TACon alternatives must not overlap. 69 | TUnit -- used for levels right now 70 | TSort 71 | TErased 72 | TCoerce TTerm -- ^ Used by the GHC backend 73 | TError TError 74 -- ^ A runtime error, something bad has happened. 75 deriving (Data, Show, Eq, Ord, Generic) 76 77-- | Compiler-related primitives. This are NOT the same thing as primitives 78-- in Agda's surface or internal syntax! 79-- Some of the primitives have a suffix indicating which type of arguments they take, 80-- using the following naming convention: 81-- Char | Type 82-- C | Character 83-- F | Float 84-- I | Integer 85-- Q | QName 86-- S | String 87data TPrim 88 = PAdd | PAdd64 89 | PSub | PSub64 90 | PMul | PMul64 91 | PQuot | PQuot64 92 | PRem | PRem64 93 | PGeq 94 | PLt | PLt64 95 | PEqI | PEq64 96 | PEqF 97 | PEqS 98 | PEqC 99 | PEqQ 100 | PIf 101 | PSeq 102 | PITo64 | P64ToI 103 deriving (Data, Show, Eq, Ord, Generic) 104 105isPrimEq :: TPrim -> Bool 106isPrimEq p = p `elem` [PEqI, PEqF, PEqS, PEqC, PEqQ, PEq64] 107 108-- | Strip leading coercions and indicate whether there were some. 109coerceView :: TTerm -> (Bool, TTerm) 110coerceView = \case 111 TCoerce t -> (True,) $ snd $ coerceView t 112 t -> (False, t) 113 114mkTApp :: TTerm -> Args -> TTerm 115mkTApp x [] = x 116mkTApp (TApp x as) bs = TApp x (as ++ bs) 117mkTApp x as = TApp x as 118 119tAppView :: TTerm -> (TTerm, [TTerm]) 120tAppView = \case 121 TApp a bs -> second (++ bs) $ tAppView a 122 t -> (t, []) 123 124-- | Expose the format @coerce f args@. 125-- 126-- We fuse coercions, even if interleaving with applications. 127-- We assume that coercion is powerful enough to satisfy 128-- @ 129-- coerce (coerce f a) b = coerce f a b 130-- @ 131coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm]) 132coerceAppView = \case 133 TCoerce t -> first ((True,) . snd) $ coerceAppView t 134 TApp a bs -> second (++ bs) $ coerceAppView a 135 t -> ((False, t), []) 136 137tLetView :: TTerm -> ([TTerm], TTerm) 138tLetView (TLet e b) = first (e :) $ tLetView b 139tLetView e = ([], e) 140 141tLamView :: TTerm -> (Int, TTerm) 142tLamView = go 0 143 where go n (TLam b) = go (n + 1) b 144 go n t = (n, t) 145 146mkTLam :: Int -> TTerm -> TTerm 147mkTLam n b = foldr ($) b $ replicate n TLam 148 149-- | Introduces a new binding 150mkLet :: TTerm -> TTerm -> TTerm 151mkLet x body = TLet x body 152 153tInt :: Integer -> TTerm 154tInt = TLit . LitNat 155 156intView :: TTerm -> Maybe Integer 157intView (TLit (LitNat x)) = Just x 158intView _ = Nothing 159 160word64View :: TTerm -> Maybe Word64 161word64View (TLit (LitWord64 x)) = Just x 162word64View _ = Nothing 163 164tPlusK :: Integer -> TTerm -> TTerm 165tPlusK 0 n = n 166tPlusK k n | k < 0 = tOp PSub n (tInt (-k)) 167tPlusK k n = tOp PAdd (tInt k) n 168 169-- -(k + n) 170tNegPlusK :: Integer -> TTerm -> TTerm 171tNegPlusK k n = tOp PSub (tInt (-k)) n 172 173plusKView :: TTerm -> Maybe (Integer, TTerm) 174plusKView (TApp (TPrim PAdd) [k, n]) | Just k <- intView k = Just (k, n) 175plusKView (TApp (TPrim PSub) [n, k]) | Just k <- intView k = Just (-k, n) 176plusKView _ = Nothing 177 178negPlusKView :: TTerm -> Maybe (Integer, TTerm) 179negPlusKView (TApp (TPrim PSub) [k, n]) | Just k <- intView k = Just (-k, n) 180negPlusKView _ = Nothing 181 182tOp :: TPrim -> TTerm -> TTerm -> TTerm 183tOp op a b = TPOp op a b 184 185pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm 186pattern TPOp op a b = TApp (TPrim op) [a, b] 187 188pattern TPFn :: TPrim -> TTerm -> TTerm 189pattern TPFn op a = TApp (TPrim op) [a] 190 191tUnreachable :: TTerm 192tUnreachable = TError TUnreachable 193 194tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm 195tIfThenElse c i e = TApp (TPrim PIf) [c, i, e] 196 197data CaseType 198 = CTData Quantity QName 199 -- Case on datatype. The 'Quantity' is zero for matches on erased 200 -- arguments. 201 | CTNat 202 | CTInt 203 | CTChar 204 | CTString 205 | CTFloat 206 | CTQName 207 deriving (Data, Show, Eq, Ord, Generic) 208 209data CaseInfo = CaseInfo 210 { caseLazy :: Bool 211 , caseType :: CaseType } 212 deriving (Data, Show, Eq, Ord, Generic) 213 214data TAlt 215 = TACon { aCon :: QName, aArity :: Int, aBody :: TTerm } 216 -- ^ Matches on the given constructor. If the match succeeds, 217 -- the pattern variables are prepended to the current environment 218 -- (pushes all existing variables aArity steps further away) 219 | TAGuard { aGuard :: TTerm, aBody :: TTerm } 220 -- ^ Binds no variables 221 | TALit { aLit :: Literal, aBody:: TTerm } 222 deriving (Data, Show, Eq, Ord, Generic) 223 224data TError 225 = TUnreachable 226 -- ^ Code which is unreachable. E.g. absurd branches or missing case defaults. 227 -- Runtime behaviour of unreachable code is undefined, but preferably 228 -- the program will exit with an error message. The compiler is free 229 -- to assume that this code is unreachable and to remove it. 230 | TMeta String 231 -- ^ Code which could not be obtained because of a hole in the program. 232 -- This should throw a runtime error. 233 -- The string gives some information about the meta variable that got compiled. 234 deriving (Data, Show, Eq, Ord, Generic) 235 236 237class Unreachable a where 238 -- | Checks if the given expression is unreachable or not. 239 isUnreachable :: a -> Bool 240 241instance Unreachable TAlt where 242 isUnreachable = isUnreachable . aBody 243 244instance Unreachable TTerm where 245 isUnreachable (TError TUnreachable{}) = True 246 isUnreachable (TLet _ b) = isUnreachable b 247 isUnreachable _ = False 248 249instance KillRange Compiled where 250 killRange c = c -- bogus, but not used anyway 251 252 253-- * Utilities for ArgUsage 254--------------------------------------------------------------------------- 255 256-- | @filterUsed used args@ drops those @args@ which are labelled 257-- @ArgUnused@ in list @used@. 258-- 259-- Specification: 260-- 261-- @ 262-- filterUsed used args = [ a | (a, ArgUsed) <- zip args $ used ++ repeat ArgUsed ] 263-- @ 264-- 265-- Examples: 266-- 267-- @ 268-- filterUsed [] == id 269-- filterUsed (repeat ArgUsed) == id 270-- filterUsed (repeat ArgUnused) == const [] 271-- @ 272filterUsed :: [ArgUsage] -> [a] -> [a] 273filterUsed = curry $ \case 274 ([], args) -> args 275 (_ , []) -> [] 276 (ArgUsed : used, a : args) -> a : filterUsed used args 277 (ArgUnused : used, a : args) -> filterUsed used args 278 279-- NFData instances 280--------------------------------------------------------------------------- 281 282instance NFData Compiled 283instance NFData ArgUsage 284instance NFData TTerm 285instance NFData TPrim 286instance NFData CaseType 287instance NFData CaseInfo 288instance NFData TAlt 289instance NFData TError 290