WIP (compiling)

Author: diode-lang

app/Agda/Core/PrettyPrint.hs

@@ -163,6 +163,8 @@ instance PrettyCore Core.Defn where
     prettyCore m c
   prettyCore m (Core.RecordDefn r) =
     prettyCore m r
+  prettyCore m (Core.ProjDefn) = 
+    "Is a Projection"
 
 instance PrettyCore Core.Definition where
   prettyCore :: NameMap -> Core.Definition -> String

app/Agda/Core/ToCore.hs

@@ -296,8 +296,8 @@ toCoreDefn (I.FunctionDefn def) _ =
             recordIdx <- lookupRec qn >>= \case
                   Nothing -> throwError $ "Trying to access an unknown record definition: " <+> pretty qn
                   Just (recordIndex, _) -> pure recordIndex
-            
-            throwError "TODO: Add support for compiling record projections"
+            -- a dummy Defn object which simply communicates that this Defn is a record projection
+            return Core.ProjDefn
     I.FunctionData{}
       -> throwError "unsupported case (shouldn't happen)"
 
@@ -409,7 +409,7 @@ instance ToCore I.Elim where
   toCore (I.Apply x)   = toCore x
   --TODO (diode-lang) : Support projection as an Elim
   -- toCore (I.Proj _ qn) = TDef <$> lookupDefOrData qn
-  toCore (I.Proj _ qn) = throwError "record projection not supported"
+  toCore (I.Proj _ qn) = throwError "TODO: Support record projections"
   toCore I.IApply{}    = throwError "cubical endpoint application not supported"
 
 

app/Main.hs

@@ -297,6 +297,14 @@ agdaCoreCompile env _ _ def = do
                 , preSigCons = preSigCons
                 , preSigRecs = Map.insert (indexToNat index) recTyp preSigRecs
                 }
+        Core.ProjDefn ->
+          liftIO $ writeIORef ioPreSig $
+            PreSignature
+                {  preSigDefs = preSigDefs
+                , preSigData = preSigData
+                , preSigCons = preSigCons
+                , preSigRecs = preSigRecs
+                }
       return $ pure def'
 
 

src/Agda/Core/Syntax/Signature.agda

@@ -141,6 +141,7 @@ data Defn : Set where
   DatatypeDefn :  (@0 d : NameData) → Datatype d → Defn
   ConstructorDefn : (@0 d : NameData) (@0 c : NameCon d) → Constructor c → Defn
   RecordDefn : (@0 r : NameRec) → Record r → Defn
+  ProjDefn : Defn
 {-# COMPILE AGDA2HS Defn #-}
 
 

test/EtaRecords.agda

@@ -48,27 +48,30 @@ x = record { fst = Zero; snd = Suc Zero }
 x' : Pair Nat Nat
 x' = Pair.constructor Zero (Suc Zero)
 
-y : Pair Nat Bool
-y = record { fst = Pair.fst x; snd = False }
+proj_example : Nat
+proj_example = Pair.fst x
 
-z : PairExplCon Nat Nat
-z = _,_ Zero (Suc Zero)
+-- y : Pair Nat Bool
+-- y = record { fst = Pair.fst x; snd = False }
 
--- (diode-lang): I don't think this statement is actually provable, because we have turned off eta-equality
--- eta-R-two_expl : (A B : Set) (x : PairNoEta A B) →
---   x ≡ record { fst = PairNoEta.fst x ; snd = PairNoEta.snd x }
--- eta-R-two_expl = λ A B → λ x → {!!}
+-- z : PairExplCon Nat Nat
+-- z = _,_ Zero (Suc Zero)
 
+-- eta-R-two : (A B : Set) (x : Pair A B) → 
+--   x ≡ record { fst = (const (Pair A B → A) Pair.fst Pair.fst) x ; snd = Pair.snd x }
+-- eta-R-two = λ A B → λ x → refl
 
-eta-R-two : (A B : Set) (x : Pair A B) → 
-  x ≡ record { fst = (const (Pair A B → A) Pair.fst Pair.fst) x ; snd = Pair.snd x }
-eta-R-two = λ A B → λ x → refl
-
-eta-R-two-expl-con : (A B : Set) (x : PairExplCon A B) → 
-  x ≡ (_,_ (const (PairExplCon A B → A) PairExplCon.fstE PairExplCon.fstE x) (PairExplCon.sndE x))
-eta-R-two-expl-con = λ A B → λ x → refl
+-- eta-R-two-expl-con : (A B : Set) (x : PairExplCon A B) → 
+--   x ≡ (_,_ (const (PairExplCon A B → A) PairExplCon.fstE PairExplCon.fstE x) (PairExplCon.sndE x))
+-- eta-R-two-expl-con = λ A B → λ x → refl
 
 -- eta-R-two : (A B : Set) (x : Pair A B) → 
 --   x ≡ record { fst = (const (Pair A B → A) Pair.fst Pair.fst) x ; snd = Pair.snd x }
 -- eta-R-two = λ A B → λ x → {!!}
 
+-- (diode-lang): I don't think this statement is actually provable, because we have turned off eta-equality
+-- eta-R-two_expl : (A B : Set) (x : PairNoEta A B) →
+--   x ≡ record { fst = PairNoEta.fst x ; snd = PairNoEta.snd x }
+-- eta-R-two_expl = λ A B → λ x → {!!}
+
+