Add CompileExpr

src/Core/CompileExpr.idr

@@ -0,0 +1,185 @@
+-- Representation of expressions ready for compiling
+-- Type erased, explicit case trees
+module Core.CompileExpr
+
+import Core.Name
+import Core.TT
+
+import Data.Vect
+
+%default total
+
+mutual
+  ||| CExp - an expression ready for compiling.
+  public export
+  data CExp : List Name -> Type where
+       CLocal : {idx : Nat} -> .(IsVar x idx vars) -> CExp vars
+       CRef : Name -> CExp vars
+       -- Lambda expression
+       CLam : (x : Name) -> CExp (x :: vars) -> CExp vars
+       -- Let bindings
+       CLet : (x : Name) -> 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 : CExp vars -> List (CExp vars) -> CExp vars
+       -- A saturated constructor application
+       CCon : Name -> (tag : Int) -> List (CExp vars) -> CExp vars
+       -- Internally defined primitive operations
+       COp : PrimFn arity -> Vect arity (CExp vars) -> CExp vars
+       -- Externally defined primitive operations
+       CExtPrim : (p : Name) -> List (CExp vars) -> CExp vars
+       -- A forced (evaluated) value (TODO: is this right?)
+       CForce : CExp vars -> CExp vars
+       -- A delayed value (lazy? TODO: check)
+       CDelay : CExp vars -> CExp vars
+       -- A case match statement
+       CConCase : (sc : CExp vars) -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars
+       CConstCase : (sc : CExp vars) -> List (CConstAlt vars) -> Maybe (CExp vars) -> CExp vars
+       -- A primitive value
+       CPrimVal : Constant -> CExp vars
+       -- An erased value
+       CErased : CExp vars
+       -- Some sort of crash?
+       CCrash : String -> CExp vars
+
+  public export
+  data CConAlt : List Name -> Type where
+       MkConAlt : Name -> (tag : Int) -> (args : List Name) ->
+                  CExp (args ++ vars) -> CConAlt vars
+
+  public export
+  data CConstAlt : List Name -> Type where
+       MkConstAlt : Constant -> CExp vars -> CConstAlt vars
+
+public export
+data CDef : Type where
+     -- Normal function definition
+     MkFun : (args : List Name) -> CExp args -> CDef
+     -- Constructor
+     MkCon : (tag : Int) -> (arity : Nat) -> 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
+
+mutual
+  export
+  Show (CExp vars) where
+    show (CLocal {x} y) = "!" ++ show x
+    show (CRef x) = show x
+    show (CLam x y) = "(%lam " ++ show x ++ " " ++ show y ++ ")"
+    show (CLet x y z) = "(%let " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
+    show (CApp x xs)
+        = assert_total $ "(" ++ show x ++ " " ++ show xs ++ ")"
+    show (CCon x tag xs)
+        = assert_total $ "(%con " ++ show x ++ " " ++ show tag ++ " " ++ show xs ++ ")"
+    show (COp op xs)
+        = assert_total $ "(" ++ show op ++ " " ++ show xs ++ ")"
+    show (CExtPrim p xs)
+        = assert_total $ "(%extern " ++ show p ++ " " ++ show xs ++ ")"
+    show (CForce x) = "(%force " ++ show x ++ ")"
+    show (CDelay x) = "(%delay " ++ show x ++ ")"
+    show (CConCase sc xs def)
+        = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"
+    show (CConstCase sc xs def)
+        = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"
+    show (CPrimVal x) = show x
+    show CErased = "___"
+    show (CCrash x) = "(CRASH " ++ show x ++ ")"
+
+  export
+  Show (CConAlt vars) where
+    show (MkConAlt x tag args exp)
+         = "(%concase " ++ show x ++ " " ++ show tag ++ " " ++
+             show args ++ " " ++ show exp ++ ")"
+
+  export
+  Show (CConstAlt vars) where
+    show (MkConstAlt x exp)
+         = "(%constcase " ++ show x ++ " " ++ show exp ++ ")"
+
+export
+Show CDef where
+  show (MkFun args exp) = show args ++ ": " ++ show exp
+  show (MkCon tag arity) = "Constructor tag " ++ show tag ++ " arity " ++ show arity
+  show (MkError exp) = "Error: " ++ show exp
+
+mutual
+  export
+  thin : (n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)
+  thin n (CLocal prf) 
+      = let MkVar var' = insertVar {n} _ prf in
+            CLocal var'
+  thin n (CRef x) = CRef x
+  thin {outer} {inner} n (CLam x sc)
+      = let sc' = thin {outer = x :: outer} {inner} n sc in
+            CLam x sc'
+  thin {outer} {inner} n (CLet x val sc)
+      = let sc' = thin {outer = x :: outer} {inner} n sc in
+            CLet x (thin n val) sc'
+  thin n (CApp x xs)
+      = CApp (thin n x) (assert_total (map (thin n) xs))
+  thin n (CCon x tag xs)
+      = CCon x tag (assert_total (map (thin n) xs))
+  thin n (COp x xs)
+      = COp x (assert_total (map (thin n) xs))
+  thin n (CExtPrim p xs)
+      = CExtPrim p (assert_total (map (thin n) xs))
+  thin n (CForce x) = CForce (thin n x)
+  thin n (CDelay x) = CDelay (thin n x)
+  thin n (CConCase sc xs def)
+      = CConCase (thin n sc) (assert_total (map (thinConAlt n) xs))
+                 (assert_total (map (thin n) def))
+  thin n (CConstCase sc xs def)
+      = CConstCase (thin n sc) (assert_total (map (thinConstAlt n) xs))
+                   (assert_total (map (thin n) def))
+  thin n (CPrimVal x) = CPrimVal x
+  thin n CErased = CErased
+  thin n (CCrash x) = CCrash 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
+  embed : CExp args -> CExp (args ++ vars)
+  embed (CLocal prf) = CLocal (varExtend prf)
+  embed (CRef n) = CRef n
+  embed (CLam x sc) = CLam x (embed sc)
+  embed (CLet x val sc) = CLet x (embed val) (embed sc)
+  embed (CApp f args) = CApp (embed f) (assert_total (map embed args))
+  embed (CCon n t args) = CCon n t (assert_total (map embed args))
+  embed (COp p args) = COp p (assert_total (map embed args))
+  embed (CExtPrim p args) = CExtPrim p (assert_total (map embed args))
+  embed (CForce e) = CForce (embed e)
+  embed (CDelay e) = CDelay (embed e)
+  embed (CConCase sc alts def)
+      = CConCase (embed sc) (assert_total (map embedAlt alts))
+                 (assert_total (map embed def))
+  embed (CConstCase sc alts def)
+      = CConstCase (embed sc) (assert_total (map embedConstAlt alts))
+                   (assert_total (map embed def))
+  embed (CPrimVal c) = CPrimVal c
+  embed CErased = CErased
+  embed (CCrash msg) = CCrash 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
+  export
+  Weaken CExp where
+    weaken = thin {outer = []} _
+

src/Core/Context.idr

@@ -1,6 +1,7 @@
 module Core.Context
 
 import        Core.CaseTree
+import        Core.CompileExpr
 import public Core.Core
 import        Core.Env
 import        Core.Hash
@@ -391,6 +392,47 @@ TTC DefFlag where
              6 => do x <- fromBuf s b; pure (SetTotal x)
              _ => corrupt "DefFlag"
 
+public export
+data SizeChange = Smaller | Same | Unknown
+
+export
+Show SizeChange where
+  show Smaller = "Smaller"
+  show Same = "Same"
+  show Unknown = "Unknown"
+
+public export
+record SCCall where
+     constructor MkSCCall
+     fnCall : Name -- Function called
+     fnArgs : List (Maybe (Nat, SizeChange))
+        -- relationship to arguments of calling function; argument position
+        -- (in the calling function), and how its size changed in the call.
+        -- 'Nothing' if it's not related to any of the calling function's
+        -- arguments
+
+export
+TTC SizeChange where
+  toBuf b Smaller = tag 0
+  toBuf b Same = tag 1
+  toBuf b Unknown = tag 2
+
+  fromBuf s b
+      = case !getTag of
+             0 => pure Smaller
+             1 => pure Same
+             2 => pure Unknown
+             _ => corrupt "SizeChange"
+
+export
+TTC SCCall where
+  toBuf b c = do toBuf b (fnCall c); toBuf b (fnArgs c)
+  fromBuf s b
+      = do fn <- fromBuf s b
+           args <- fromBuf s b
+           pure (MkSCCall fn args)
+
+
 public export
 record GlobalDef where
   constructor MkGlobalDef
@@ -410,6 +452,8 @@ record GlobalDef where
                   -- occurs check)
   linearChecked : Bool -- Flag whether we've already checked its linearity
   definition : Def
+  compexpr : Maybe CDef
+  sizeChange : List SCCall
 
 export
 TTC GlobalDef where
@@ -418,6 +462,7 @@ TTC GlobalDef where
         -- be holes where all we will ever need after loading is the definition
         do toBuf b (fullname gdef)
            toBuf b (definition gdef)
+           toBuf b (compexpr gdef)
            when (isUserName (fullname gdef)) $
               do toBuf b (location gdef)
                  toBuf b (type gdef)
@@ -428,10 +473,12 @@ TTC GlobalDef where
                  toBuf b (flags gdef)
                  toBuf b (map fst (toList (refersTo gdef)))
                  toBuf b (noCycles gdef)
+                 toBuf b (sizeChange gdef)
 
   fromBuf r b 
       = do name <- fromBuf r b
            def <- fromBuf r b
+           cdef <- fromBuf r b
            if isUserName name
               then do loc <- fromBuf r b; 
                       ty <- fromBuf r b; mul <- fromBuf r b
@@ -441,18 +488,20 @@ TTC GlobalDef where
                       refsList <- fromBuf r b; 
                       let refs = fromList (map (\x => (x, ())) refsList)
                       c <- fromBuf r b
+                      sc <- fromBuf r b
                       pure (MkGlobalDef loc name ty mul vars vis 
-                                        tot fl refs c True def)
+                                        tot fl refs c True def cdef sc)
               else do let fc = emptyFC
                       pure (MkGlobalDef fc name (Erased fc)
                                         RigW [] Public unchecked [] empty
-                                        False True def)
+                                        False True def cdef [])
 
 export
 newDef : FC -> Name -> RigCount -> List Name -> 
          ClosedTerm -> Visibility -> Def -> GlobalDef
 newDef fc n rig vars ty vis def 
     = MkGlobalDef fc n ty rig vars vis unchecked [] empty False False def
+                  Nothing []
 
 public export
 record Defs where
@@ -546,7 +595,8 @@ addBuiltin : {auto x : Ref Ctxt Defs} ->
              PrimFn arity -> Core ()
 addBuiltin n ty tot op 
     = do addDef n (MkGlobalDef emptyFC n ty RigW [] Public tot 
-                               [Inline] empty False True (Builtin op)) 
+                               [Inline] empty False True (Builtin op)
+                               Nothing []) 
          pure ()
 
 export

src/Core/TTC.idr

@@ -1,12 +1,14 @@
 module Core.TTC
 
 import Core.CaseTree
+import Core.CompileExpr
 import Core.Core
 import Core.Env
 import Core.FC
 import Core.Name
 import Core.TT
 
+import Data.Vect
 import Utils.Binary
 
 %default covering
@@ -532,4 +534,89 @@ TTC (PrimFn n) where
                  20 => pure BelieveMe
                  _ => corrupt "PrimFn 3"
              
+mutual
+  export
+  TTC (CExp vars) where
+    toBuf b (CLocal {x} {idx} h) = do tag 0; toBuf b x; toBuf b idx
+    toBuf b (CRef n) = do tag 1; toBuf b n
+    toBuf b (CLam x sc) = do tag 2; toBuf b x; toBuf b sc
+    toBuf b (CLet x val sc) = do tag 3; toBuf b x; toBuf b val; toBuf b sc
+    toBuf b (CApp f as) = assert_total $ do tag 4; toBuf b f; toBuf b as
+    toBuf b (CCon t n as) = assert_total $ do tag 5; toBuf b t; toBuf b n; toBuf b as
+    toBuf b (COp {arity} op as) = assert_total $ do tag 6; toBuf b arity; toBuf b op; toBuf b as
+    toBuf b (CExtPrim f as) = assert_total $ do tag 7; toBuf b f; toBuf b as
+    toBuf b (CForce x) = assert_total $ do tag 8; toBuf b x
+    toBuf b (CDelay x) = assert_total $ do tag 9; toBuf b x
+    toBuf b (CConCase sc alts def) = assert_total $ do tag 10; toBuf b sc; toBuf b alts; toBuf b def
+    toBuf b (CConstCase sc alts def) = assert_total $ do tag 11; toBuf b sc; toBuf b alts; toBuf b def
+    toBuf b (CPrimVal c) = do tag 12; toBuf b c
+    toBuf b CErased = do tag 13
+    toBuf b (CCrash msg) = do tag 14; toBuf b msg
+
+    fromBuf s b
+        = assert_total $ case !getTag of
+               0 => do x <- fromBuf s b; idx <- fromBuf s b
+                       pure (CLocal {x} (mkPrf idx))
+               1 => do n <- fromBuf s b
+                       pure (CRef n)
+               2 => do x <- fromBuf s b; sc <- fromBuf s b
+                       pure (CLam x sc)
+               3 => do x <- fromBuf s b; val <- fromBuf s b; sc <- fromBuf s b
+                       pure (CLet x val sc)
+               4 => do f <- fromBuf s b; as <- fromBuf s b
+                       pure (CApp f as)
+               5 => do t <- fromBuf s b; n <- fromBuf s b; as <- fromBuf s b
+                       pure (CCon t n as)
+               6 => do arity <- fromBuf s b; op <- fromBuf s b; args <- fromBuf s b
+                       pure (COp {arity} op args)
+               7 => do p <- fromBuf s b; as <- fromBuf s b
+                       pure (CExtPrim p as)
+               8 => do x <- fromBuf s b
+                       pure (CForce x)
+               9 => do x <- fromBuf s b
+                       pure (CDelay x)
+               10 => do sc <- fromBuf s b; alts <- fromBuf s b; def <- fromBuf s b
+                        pure (CConCase sc alts def)
+               11 => do sc <- fromBuf s b; alts <- fromBuf s b; def <- fromBuf s b
+                        pure (CConstCase sc alts def)
+               12 => do c <- fromBuf s b
+                        pure (CPrimVal c)
+               13 => pure CErased
+               14 => do msg <- fromBuf s b
+                        pure (CCrash msg)
+               _ => corrupt "CExp"
+
+  export
+  TTC (CConAlt vars) where
+    toBuf b (MkConAlt n t as sc) = do toBuf b n; toBuf b t; toBuf b as; toBuf b sc
+
+    fromBuf s b
+        = do n <- fromBuf s b; t <- fromBuf s b
+             as <- fromBuf s b; sc <- fromBuf s b
+             pure (MkConAlt n t as sc)
+
+  export
+  TTC (CConstAlt vars) where
+    toBuf b (MkConstAlt c sc) = do toBuf b c; toBuf b sc
+
+    fromBuf s b
+        = do c <- fromBuf s b; sc <- fromBuf s b
+             pure (MkConstAlt c sc)
+
+export
+  TTC CDef where
+    toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr
+    toBuf b (MkCon t arity) = do tag 1; toBuf b t; toBuf b arity
+    toBuf b (MkError cexpr) = do tag 2; toBuf b cexpr
+
+    fromBuf s b 
+        = case !getTag of
+               0 => do args <- fromBuf s b; cexpr <- fromBuf s b
+                       pure (MkFun args cexpr)
+               1 => do t <- fromBuf s b; arity <- fromBuf s b
+                       pure (MkCon t arity)
+               2 => do cexpr <- fromBuf s b
+                       pure (MkError cexpr)
+               _ => corrupt "CDef"
+
 

yaffle.ipkg

@@ -8,6 +8,7 @@ modules =
     Core.CaseBuilder,
     Core.CaseTree,
     Core.Context,
+    Core.CompileExpr,
     Core.Core,
     Core.Directory,
     Core.Env,