record projection examples

Author: diode-lang

app/Agda/Core/ToCore.hs

@@ -52,6 +52,7 @@ import Agda.TypeChecking.Pretty (PrettyTCM(prettyTCM))
 
 import Agda.Syntax.Common.Pretty(text, render)
 
+import Agda.Core.UtilsH(traceMagenta)
 
 -- TODO(flupe): move this to Agda.Core.Syntax
 -- | Apply a core term to elims
@@ -409,8 +410,12 @@ 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 "TODO: Support record projections"
-  toCore I.IApply{}    = throwError "cubical endpoint application not supported"
+  toCore (I.Proj _ qn) = do
+    let m_idx = traceMagenta ("qn: " ++ show (pretty qn)) $ lookupDef qn >>= \case
+          Nothing -> throwError $ "[When translating an Elim] Trying to access an unknown definition: " <+> pretty qn
+          Just ident -> pure ident
+    TDef <$> m_idx
+  toCore I.IApply{}    = throwError "[When translating an Elim] cubical endpoint application not supported"
 
 
 instance ToCore a => ToCore [a] where

test/EtaRecords.agda

@@ -1,8 +1,5 @@
 module EtaRecords where
-
-data ⊥ : Set where
-  --no constructor
-
+  
 data Nat : Set where
   Zero : Nat
   Suc : Nat → Nat
@@ -51,23 +48,19 @@ x' = Pair.constructor Zero (Suc Zero)
 proj_example : Nat
 proj_example = Pair.fst x
 
--- y : Pair Nat Bool
--- y = record { fst = Pair.fst x; snd = False }
-
--- z : PairExplCon Nat Nat
--- z = _,_ Zero (Suc Zero)
+y : Pair Nat Bool
+y = record { fst = Pair.fst x; snd = False }
 
--- 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
+z : PairExplCon Nat Nat
+z = _,_ Zero (Suc Zero)
 
--- 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 → 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 → {!!}
+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
 
 -- (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) →

test/RecordProjection.agda

@@ -0,0 +1,33 @@
+
+data Nat : Set where
+  Zero : Nat
+  Suc : Nat → Nat
+
+data Bool : Set where
+  True : Bool
+  False : Bool
+
+data _≡_ {A : Set} (x : A) : A → Set where
+ refl : x ≡ x
+
+const : (A : Set) → A → A → A
+const = λ A → λ x → λ y → x
+
+record Pair (A B : Set) : Set where
+    field
+        fst : A
+        snd : B
+
+x : Pair Nat Nat
+x = record { fst = Zero; snd = Suc Zero }
+
+proj_example1 : Nat
+proj_example1 = Pair.fst x
+
+proj_example2 : Bool
+proj_example2 = (record { fst = Zero; snd = False }) .Pair.snd
+
+proj_example3 : Bool
+proj_example3 = (const (Pair Nat Bool) (record { fst = Zero; snd = False }) (record { fst = Zero; snd = False })) .Pair.snd
+
+