-- Representation of expressions ready for compiling-- Type erased, explicit case treesmodule Core.CompileExpr import Core.FCimport Core.Nameimport Core.TT import Data.NameMapimport Data.Vect %default covering mutual  ||| CExp - an expression ready for compiling.  public export  data CExp : List Name -> Type where       CLocal : {idx : Nat} -> FC -> .(IsVar x idx vars) -> CExp vars       CRef : FC -> Name -> CExp vars       -- Lambda expression       CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars       -- Let bindings       CLet : FC -> (x : Name) -> (inlineOK : Bool) -> -- Don't inline if set              CExp vars -> CExp (x :: vars) -> CExp vars       -- Application of a defined function. The length of the argument list is       -- exactly the same length as expected by its definition (so saturate with       -- lambdas if necessary, or overapply with additional CApps)       CApp : FC -> CExp vars -> List (CExp vars) -> CExp vars       -- A saturated constructor application       CCon : FC -> Name -> (tag : Maybe Int) -> List (CExp vars) -> CExp vars       -- Internally defined primitive operations       COp : FC -> PrimFn arity -> Vect arity (CExp vars) -> CExp vars       -- Externally defined primitive operations       CExtPrim : FC -> (p : Name) -> List (CExp vars) -> CExp vars       -- A forced (evaluated) value       CForce : FC -> CExp vars -> CExp vars       -- A delayed value       CDelay : FC -> CExp vars -> CExp vars       -- A case match statement       CConCase : FC -> (sc : CExp vars) -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars       CConstCase : FC -> (sc : CExp vars) -> List (CConstAlt vars) -> Maybe (CExp vars) -> CExp vars       -- A primitive value       CPrimVal : FC -> Constant -> CExp vars       -- An erased value       CErased : FC -> CExp vars       -- Some sort of crash?       CCrash : FC -> String -> CExp vars   public export  data CConAlt : List Name -> Type where       -- If no tag, then match by constructor name. Back ends might want to       -- convert names to a unique integer for performance.       MkConAlt : Name -> (tag : Maybe Int) -> (args : List Name) ->                  CExp (args ++ vars) -> CConAlt vars   public export  data CConstAlt : List Name -> Type where       MkConstAlt : Constant -> CExp vars -> CConstAlt vars mutual  ||| NamedCExp - as above, but without the name index, so with explicit  ||| names, which are faster (but less safe) to manipulate in the inliner.  ||| You can, howeveer, assume that name bindings are unique - translation  ||| to this form (and the liner) ensure that, even if the type doesn't  ||| guarantee it!  public export  data NamedCExp : Type where       NmLocal : FC -> Name -> NamedCExp       NmRef : FC -> Name -> NamedCExp       -- Lambda expression       NmLam : FC -> (x : Name) -> NamedCExp -> NamedCExp       -- Let bindings       NmLet : FC -> (x : Name) -> NamedCExp -> NamedCExp -> NamedCExp       -- Application of a defined function. The length of the argument list is       -- exactly the same length as expected by its definition (so saturate with       -- lambdas if necessary, or overapply with additional CApps)       NmApp : FC -> NamedCExp -> List NamedCExp -> NamedCExp       -- A saturated constructor application       NmCon : FC -> Name -> (tag : Maybe Int) -> List NamedCExp -> NamedCExp       -- Internally defined primitive operations       NmOp : FC -> PrimFn arity -> Vect arity NamedCExp -> NamedCExp       -- Externally defined primitive operations       NmExtPrim : FC -> (p : Name) -> List NamedCExp -> NamedCExp       -- A forced (evaluated) value       NmForce : FC -> NamedCExp -> NamedCExp       -- A delayed value       NmDelay : FC -> NamedCExp -> NamedCExp       -- A case match statement       NmConCase : FC -> (sc : NamedCExp) -> List NamedConAlt -> Maybe NamedCExp -> NamedCExp       NmConstCase : FC -> (sc : NamedCExp) -> List NamedConstAlt -> Maybe NamedCExp -> NamedCExp       -- A primitive value       NmPrimVal : FC -> Constant -> NamedCExp       -- An erased value       NmErased : FC -> NamedCExp       -- Some sort of crash?       NmCrash : FC -> String -> NamedCExp   public export  data NamedConAlt : Type where       MkNConAlt : Name -> (tag : Maybe Int) -> (args : List Name) ->                   NamedCExp -> NamedConAlt   public export  data NamedConstAlt : Type where       MkNConstAlt : Constant -> NamedCExp -> NamedConstAlt -- Argument type descriptors for foreign function callspublic exportdata CFType : Type where     CFUnit : CFType     CFInt : CFType     CFString : CFType     CFDouble : CFType     CFChar : CFType     CFPtr : CFType     CFWorld : CFType     CFFun : CFType -> CFType -> CFType     CFIORes : CFType -> CFType     CFStruct : String -> List (String, CFType) -> CFType     CFUser : Name -> List CFType -> CFType public exportdata CDef : Type where     -- Normal function definition     MkFun : (args : List Name) -> CExp args -> CDef     -- Constructor     MkCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> CDef     -- Foreign definition     MkForeign : (ccs : List String) ->                 (fargs : List CFType) ->                 CFType ->                 CDef     -- A function which will fail at runtime (usually due to being a hole) so needs     -- to run, discarding arguments, no matter how many arguments are passed     MkError : CExp [] -> CDef public exportdata NamedDef : Type where     -- Normal function definition     MkNmFun : (args : List Name) -> NamedCExp -> NamedDef     -- Constructor     MkNmCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> NamedDef     -- Foreign definition     MkNmForeign : (ccs : List String) ->                   (fargs : List CFType) ->                   CFType ->                   NamedDef     -- A function which will fail at runtime (usually due to being a hole) so needs     -- to run, discarding arguments, no matter how many arguments are passed     MkNmError : NamedCExp -> NamedDef mutual  export  Show NamedCExp where    show (NmLocal _ x) = "!" ++ show x    show (NmRef _ x) = show x    show (NmLam _ x y) = "(%lam " ++ show x ++ " " ++ show y ++ ")"    show (NmLet _ x y z) = "(%let " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"    show (NmApp _ x xs)        = assert_total $ "(" ++ show x ++ " " ++ show xs ++ ")"    show (NmCon _ x tag xs)        = assert_total $ "(%con " ++ show x ++ " " ++ show tag ++ " " ++ show xs ++ ")"    show (NmOp _ op xs)        = assert_total $ "(" ++ show op ++ " " ++ show xs ++ ")"    show (NmExtPrim _ p xs)        = assert_total $ "(%extern " ++ show p ++ " " ++ show xs ++ ")"    show (NmForce _ x) = "(%force " ++ show x ++ ")"    show (NmDelay _ x) = "(%delay " ++ show x ++ ")"    show (NmConCase _ sc xs def)        = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"    show (NmConstCase _ sc xs def)        = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"    show (NmPrimVal _ x) = show x    show (NmErased _) = "___"    show (NmCrash _ x) = "(CRASH " ++ show x ++ ")"   export  Show NamedConAlt where    show (MkNConAlt x tag args exp)         = "(%concase " ++ show x ++ " " ++ show tag ++ " " ++             show args ++ " " ++ show exp ++ ")"   export  Show NamedConstAlt where    show (MkNConstAlt x exp)         = "(%constcase " ++ show x ++ " " ++ show exp ++ ")" exportdata Names : List Name -> Type where     Nil : Names []     (::) : Name -> Names xs -> Names (x :: xs) elem : Name -> Names xs -> Boolelem n [] = Falseelem n (x :: xs) = if n == x then True else elem n xs tryNext : Name -> NametryNext (UN n) = MN n 0tryNext (MN n i) = MN n (1 + i)tryNext n = MN (nameRoot n) 0 uniqueName : Name -> Names vs -> NameuniqueName s ns =    if s `elem` ns       then uniqueName (tryNext s) ns       else s exportgetLocName : (idx : Nat) -> Names vars -> .(IsVar name idx vars) -> NamegetLocName Z (x :: xs) First = xgetLocName (S k) (x :: xs) (Later p) = getLocName k xs p exportaddLocs : (args : List Name) -> Names vars -> Names (args ++ vars)addLocs [] ns = nsaddLocs (x :: xs) ns    = let rec = addLocs xs ns in          uniqueName x rec :: rec conArgs : (args : List Name) -> Names (args ++ vars) -> List NameconArgs [] ns = []conArgs (a :: as) (n :: ns) = n :: conArgs as ns mutual  forgetExp : Names vars -> CExp vars -> NamedCExp  forgetExp locs (CLocal fc p) = NmLocal fc (getLocName _ locs p)  forgetExp locs (CRef fc n) = NmRef fc n  forgetExp locs (CLam fc x sc)      = let locs' = addLocs [x] locs in            NmLam fc (getLocName _ locs' First) (forgetExp locs' sc)  forgetExp locs (CLet fc x _ val sc)      = let locs' = addLocs [x] locs in            NmLet fc (getLocName _ locs' First)                      (forgetExp locs val)                     (forgetExp locs' sc)  forgetExp locs (CApp fc f args)      = NmApp fc (forgetExp locs f) (map (forgetExp locs) args)  forgetExp locs (CCon fc n t args)      = NmCon fc n t (map (forgetExp locs) args)  forgetExp locs (COp fc op args)      = NmOp fc op (map (forgetExp locs) args)  forgetExp locs (CExtPrim fc p args)      = NmExtPrim fc p (map (forgetExp locs) args)  forgetExp locs (CForce fc f)      = NmForce fc (forgetExp locs f)  forgetExp locs (CDelay fc f)      = NmDelay fc (forgetExp locs f)  forgetExp locs (CConCase fc sc alts def)      = NmConCase fc (forgetExp locs sc) (map (forgetConAlt locs) alts)                     (map (forgetExp locs) def)  forgetExp locs (CConstCase fc sc alts def)      = NmConstCase fc (forgetExp locs sc) (map (forgetConstAlt locs) alts)                       (map (forgetExp locs) def)  forgetExp locs (CPrimVal fc c) = NmPrimVal fc c  forgetExp locs (CErased fc) = NmErased fc  forgetExp locs (CCrash fc msg) = NmCrash fc msg   forgetConAlt : Names vars -> CConAlt vars -> NamedConAlt  forgetConAlt locs (MkConAlt n t args exp)      = let args' = addLocs args locs in            MkNConAlt n t (conArgs args args') (forgetExp args' exp)   forgetConstAlt : Names vars -> CConstAlt vars -> NamedConstAlt  forgetConstAlt locs (MkConstAlt c exp)      = MkNConstAlt c (forgetExp locs exp) exportforget : {vars : _} -> CExp vars -> NamedCExpforget {vars} exp    = forgetExp (addLocs vars [])                (rewrite appendNilRightNeutral vars in exp) exportforgetDef : CDef -> NamedDefforgetDef (MkFun args def)    = let ns = addLocs args []          args' = conArgs args ns in          MkNmFun args' (forget def)forgetDef (MkCon t a nt) = MkNmCon t a ntforgetDef (MkForeign ccs fargs ty) = MkNmForeign ccs fargs tyforgetDef (MkError err) = MkNmError (forget err) exportShow (CExp vars) where  show exp = show (forget exp) exportShow CFType where  show CFUnit = "Unit"  show CFInt = "Int"  show CFString = "String"  show CFDouble = "Double"  show CFChar = "Char"  show CFPtr = "Ptr"  show CFWorld = "%World"  show (CFFun s t) = show s ++ " -> " ++ show t  show (CFIORes t) = "IORes " ++ show t  show (CFStruct n args) = "struct " ++ show n ++ " " ++ showSep " " (map show args)  show (CFUser n args) = show n ++ " " ++ showSep " " (map show args) exportShow CDef where  show (MkFun args exp) = show args ++ ": " ++ show exp  show (MkCon tag arity pos)      = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++        maybe "" (\n => " (newtype by " ++ show n ++ ")") pos  show (MkForeign ccs args ret)      = "Foreign call " ++ show ccs ++ " " ++        show args ++ " -> " ++ show ret  show (MkError exp) = "Error: " ++ show exp exportShow NamedDef where  show (MkNmFun args exp) = show args ++ ": " ++ show exp  show (MkNmCon tag arity pos)      = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++        maybe "" (\n => " (newtype by " ++ show n ++ ")") pos  show (MkNmForeign ccs args ret)      = "Foreign call " ++ show ccs ++ " " ++        show args ++ " -> " ++ show ret  show (MkNmError exp) = "Error: " ++ show exp mutual  export  thin : (n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)  thin n (CLocal fc prf)      = let MkNVar var' = insertNVar {n} _ prf in            CLocal fc var'  thin _ (CRef fc x) = CRef fc x  thin {outer} {inner} n (CLam fc x sc)      = let sc' = thin {outer = x :: outer} {inner} n sc in            CLam fc x sc'  thin {outer} {inner} n (CLet fc x inl val sc)      = let sc' = thin {outer = x :: outer} {inner} n sc in            CLet fc x inl (thin n val) sc'  thin n (CApp fc x xs)      = CApp fc (thin n x) (assert_total (map (thin n) xs))  thin n (CCon fc x tag xs)      = CCon fc x tag (assert_total (map (thin n) xs))  thin n (COp fc x xs)      = COp fc x (assert_total (map (thin n) xs))  thin n (CExtPrim fc p xs)      = CExtPrim fc p (assert_total (map (thin n) xs))  thin n (CForce fc x) = CForce fc (thin n x)  thin n (CDelay fc x) = CDelay fc (thin n x)  thin n (CConCase fc sc xs def)      = CConCase fc (thin n sc) (assert_total (map (thinConAlt n) xs))                 (assert_total (map (thin n) def))  thin n (CConstCase fc sc xs def)      = CConstCase fc (thin n sc) (assert_total (map (thinConstAlt n) xs))                   (assert_total (map (thin n) def))  thin _ (CPrimVal fc x) = CPrimVal fc x  thin _ (CErased fc) = CErased fc  thin _ (CCrash fc x) = CCrash fc x   thinConAlt : (n : Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ n :: inner)  thinConAlt {outer} {inner} n (MkConAlt x tag args sc)        = let sc' : CExp ((args ++ outer) ++ inner)                  = rewrite sym (appendAssociative args outer inner) in sc in              MkConAlt x tag args               (rewrite appendAssociative args outer (n :: inner) in                        thin n sc')   thinConstAlt : (n : Name) -> CConstAlt (outer ++ inner) -> CConstAlt (outer ++ n :: inner)  thinConstAlt n (MkConstAlt x sc) = MkConstAlt x (thin n sc) mutual  export  insertNames : {outer, inner : _} ->                (ns : List Name) -> CExp (outer ++ inner) ->                CExp (outer ++ (ns ++ inner))  insertNames ns (CLocal fc prf)      = let MkNVar var' = insertNVarNames {ns} _ prf in            CLocal fc var'  insertNames _ (CRef fc x) = CRef fc x  insertNames {outer} {inner} ns (CLam fc x sc)      = let sc' = insertNames {outer = x :: outer} {inner} ns sc in            CLam fc x sc'  insertNames {outer} {inner} ns (CLet fc x inl val sc)      = let sc' = insertNames {outer = x :: outer} {inner} ns sc in            CLet fc x inl (insertNames ns val) sc'  insertNames ns (CApp fc x xs)      = CApp fc (insertNames ns x) (assert_total (map (insertNames ns) xs))  insertNames ns (CCon fc x tag xs)      = CCon fc x tag (assert_total (map (insertNames ns) xs))  insertNames ns (COp fc x xs)      = COp fc x (assert_total (map (insertNames ns) xs))  insertNames ns (CExtPrim fc p xs)      = CExtPrim fc p (assert_total (map (insertNames ns) xs))  insertNames ns (CForce fc x) = CForce fc (insertNames ns x)  insertNames ns (CDelay fc x) = CDelay fc (insertNames ns x)  insertNames ns (CConCase fc sc xs def)      = CConCase fc (insertNames ns sc) (assert_total (map (insertNamesConAlt ns) xs))                 (assert_total (map (insertNames ns) def))  insertNames ns (CConstCase fc sc xs def)      = CConstCase fc (insertNames ns sc) (assert_total (map (insertNamesConstAlt ns) xs))                   (assert_total (map (insertNames ns) def))  insertNames _ (CPrimVal fc x) = CPrimVal fc x  insertNames _ (CErased fc) = CErased fc  insertNames _ (CCrash fc x) = CCrash fc x   insertNamesConAlt : (ns : List Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ (ns ++ inner))  insertNamesConAlt {outer} {inner} ns (MkConAlt x tag args sc)        = let sc' : CExp ((args ++ outer) ++ inner)                  = rewrite sym (appendAssociative args outer inner) in sc in              MkConAlt x tag args               (rewrite appendAssociative args outer (ns ++ inner) in                        insertNames ns sc')   insertNamesConstAlt : (ns : List Name) -> CConstAlt (outer ++ inner) -> CConstAlt (outer ++ (ns ++ inner))  insertNamesConstAlt ns (MkConstAlt x sc) = MkConstAlt x (insertNames ns sc) mutual  export  embed : CExp args -> CExp (args ++ vars)  embed cexp = believe_me cexp  -- It is identity at run time, but it would be implemented as below  -- (not sure theere's much performance benefit, mind...)  {-  embed (CLocal fc prf) = CLocal fc (varExtend prf)  embed (CRef fc n) = CRef fc n  embed (CLam fc x sc) = CLam fc x (embed sc)  embed (CLet fc x inl val sc) = CLet fc x inl (embed val) (embed sc)  embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))  embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))  embed (COp fc p args) = COp fc p (assert_total (map embed args))  embed (CExtPrim fc p args) = CExtPrim fc p (assert_total (map embed args))  embed (CForce fc e) = CForce fc (embed e)  embed (CDelay fc e) = CDelay fc (embed e)  embed (CConCase fc sc alts def)      = CConCase fc (embed sc) (assert_total (map embedAlt alts))                 (assert_total (map embed def))  embed (CConstCase fc sc alts def)      = CConstCase fc (embed sc) (assert_total (map embedConstAlt alts))                   (assert_total (map embed def))  embed (CPrimVal fc c) = CPrimVal fc c  embed (CErased fc) = CErased fc  embed (CCrash fc msg) = CCrash fc msg   embedAlt : CConAlt args -> CConAlt (args ++ vars)  embedAlt {args} {vars} (MkConAlt n t as sc)     = MkConAlt n t as (rewrite appendAssociative as args vars in embed sc)   embedConstAlt : CConstAlt args -> CConstAlt (args ++ vars)  embedConstAlt (MkConstAlt c sc) = MkConstAlt c (embed sc)  -} mutual  -- Shrink the scope of a compiled expression, replacing any variables not  -- in the remaining set with Erased  export  shrinkCExp : SubVars newvars vars -> CExp vars -> CExp newvars  shrinkCExp sub (CLocal fc prf)      = case subElem prf sub of             Nothing => CErased fc             Just (MkVar prf') => CLocal fc prf'  shrinkCExp _ (CRef fc x) = CRef fc x  shrinkCExp sub (CLam fc x sc)      = let sc' = shrinkCExp (KeepCons sub) sc in            CLam fc x sc'  shrinkCExp sub (CLet fc x inl val sc)      = let sc' = shrinkCExp (KeepCons sub) sc in            CLet fc x inl (shrinkCExp sub val) sc'  shrinkCExp sub (CApp fc x xs)      = CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))  shrinkCExp sub (CCon fc x tag xs)      = CCon fc x tag (assert_total (map (shrinkCExp sub) xs))  shrinkCExp sub (COp fc x xs)      = COp fc x (assert_total (map (shrinkCExp sub) xs))  shrinkCExp sub (CExtPrim fc p xs)      = CExtPrim fc p (assert_total (map (shrinkCExp sub) xs))  shrinkCExp sub (CForce fc x) = CForce fc (shrinkCExp sub x)  shrinkCExp sub (CDelay fc x) = CDelay fc (shrinkCExp sub x)  shrinkCExp sub (CConCase fc sc xs def)      = CConCase fc (shrinkCExp sub sc)                 (assert_total (map (shrinkConAlt sub) xs))                 (assert_total (map (shrinkCExp sub) def))  shrinkCExp sub (CConstCase fc sc xs def)      = CConstCase fc (shrinkCExp sub sc)                   (assert_total (map (shrinkConstAlt sub) xs))                   (assert_total (map (shrinkCExp sub) def))  shrinkCExp _ (CPrimVal fc x) = CPrimVal fc x  shrinkCExp _ (CErased fc) = CErased fc  shrinkCExp _ (CCrash fc x) = CCrash fc x   shrinkConAlt : SubVars newvars vars -> CConAlt vars -> CConAlt newvars  shrinkConAlt sub (MkConAlt x tag args sc)        = MkConAlt x tag args (shrinkCExp (subExtend args sub) sc)   shrinkConstAlt : SubVars newvars vars -> CConstAlt vars -> CConstAlt newvars  shrinkConstAlt sub (MkConstAlt x sc) = MkConstAlt x (shrinkCExp sub sc) exportWeaken CExp where  weaken = thin {outer = []} _  weakenNs ns tm = insertNames {outer = []} ns tm -- Substitute some explicit terms for names in a term, and remove those-- names from the scopenamespace SubstCEnv

Lines 1–500 of 678. Load more