wip

src/Lower.hs

@@ -18,6 +18,7 @@ import qualified Data.OrderedHashMap as OrderedHashMap
 import qualified Data.Sequence as Seq
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
+import qualified Environment
 import Index (Index)
 import qualified Index
 import qualified Index.Map
@@ -75,6 +76,10 @@ data Collectible
   = CollectibleLet !(PassBy ()) !Name !Var !Value
   | CollectibleSeq !Value
 
+data Function
+  = Body !Value
+  | Parameter !Name !Var !Function
+
 type Collect = StateT (Tsil Collectible) M
 
 let_ :: PassBy () -> Name -> Value -> Collect Operand
@@ -121,24 +126,43 @@ addRepresentation :: Operand -> Operand -> Value
 addRepresentation x y =
   Call (Name.Lifted Builtin.AddRepresentationName 0) [x, y]
 
-lowerDefinition :: Name.Lifted -> CC.Syntax.Definition -> M [Low.Syntax.Definition]
-lowerDefinition name = \case
-  CC.Syntax.TypeDeclaration _ -> pure Nothing
+definition :: Name.Lifted -> CC.Syntax.Definition -> M [Low.Syntax.Definition]
+definition name = \case
+  CC.Syntax.TypeDeclaration _ -> pure mempty
   CC.Syntax.ConstantDefinition term -> do
     signature <- fetch $ Query.LowSignature name
     case signature of
-      Low.Syntax.ConstantSignature repr -> _
+      Low.Syntax.ConstantSignature repr -> do
+        value <- runCollect $ storeTerm CC.empty mempty (Global name) term
+        let term = readback Index.Map.Empty value
+        pure [Low.Syntax.ConstantDefinition term]
       _ -> panic "Constant without constant signature"
   CC.Syntax.FunctionDefinition tele -> do
     signature <- fetch $ Query.LowSignature name
     case signature of
-      Low.Syntax.FunctionSignature passArgsBy passReturnBy -> _
+      Low.Syntax.FunctionSignature passArgsBy passReturnBy -> do
+        functionValue <- lowerFunction CC.empty mempty passArgsBy passReturnBy tele
+        let function = readbackFunction Index.Map.Empty functionValue
+        pure [Low.Syntax.FunctionDefinition function]
       _ -> panic "Function without function signature"
-  CC.Syntax.DataDefinition boxity tele -> do
-    _
+  CC.Syntax.DataDefinition boxity dataDef -> do
+    let Name.Lifted qname n = name
+    when (n /= 0) $ panic "data isn't first def"
+    compiled <- CC.Representation.compileData Environment.empty name tele
   CC.Syntax.ParameterisedDataDefinition boxity tele -> do
     _
 
+lowerFunction
+  :: CC.Context v
+  -> Seq (PassedBy Operand)
+  -> [PassBy ()]
+  -> PassBy ()
+  -> Telescope Name CC.Syntax.Type CC.Syntax.Term v
+  -> M Function
+lowerFunction context indices passArgsBy passReturnBy = \case
+  Telescope.Empty body -> _
+  Telescope.Extend _ _ _ _ -> _
+
 storeOperand
   :: Operand
   -> PassedBy Operand
@@ -472,6 +496,11 @@ boxedConstructorSize env con params args = do
 
 -------------------------------------------------------------------------------
 
+readbackFunction :: Index.Map v Var -> Function -> Low.Syntax.Function v
+readbackFunction env = \case
+  Body body -> Low.Syntax.Body $ readback env body
+  Parameter name var function -> Low.Syntax.Parameter name $ readbackFunction (env Index.Map.:> var) function
+
 readback :: Index.Map v Var -> Value -> Low.Syntax.Term v
 readback env = \case
   Operand operand -> Low.Syntax.Operand $ readbackOperand env operand