Small improvements in Conversion ; marks places where records should be added

Author: diode-lang

app/Agda/Core/ToCore.hs

@@ -302,8 +302,12 @@ toCoreDefn (I.DatatypeDefn dt) ty =
                           dataConstructors      = cons_indexes}
   return $ Core.DatatypeDefn d
 
-toCoreDefn (I.RecordDefn _) _ =
-  throwError "records are not supported"
+toCoreDefn (I.RecordDefn rd) ty =
+  withError (\e -> multiLineText $ "record definition failure \n" <> Pretty.render (nest 1 e)) $ do
+    let I.RecordData{
+      _recPars = pars,
+      _recFields = fields} = rd 
+    throwError "records are not supported"
 
 toCoreDefn (I.ConstructorDefn cs) ty =
   withError (\e -> multiLineText $ "constructor definition failure:\n" <> Pretty.render (nest 1 e)) $ do

src/Agda/Core/Checkers/Converter.agda

@@ -246,14 +246,14 @@ convertWhnf r (TSort s) (TSort t) = convSorts s t
 --     return (CEtaVar x f b proof)
 convertWhnf r functionTerm (TLam x b) = 
   let 
-  depPairX = ⟨ x ⟩ (Zero ⟨ IsZero refl ⟩)
+  -- depPairX = ⟨ x ⟩ (Zero ⟨ IsZero refl ⟩)
   subsetProof = (subWeaken subRefl)
   newScope = singBind r
-  term = TApp (weakenTerm subsetProof functionTerm) (TVar depPairX)
+  term = TApp (weakenTerm subsetProof functionTerm) (TVar (VZero x))
   in
   do
     conversionProof <- convertCheck newScope b term
-    return (CEtaVar2 x functionTerm b conversionProof)
+    return (CEtaFunctions x functionTerm b conversionProof)
 -- convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
 -- convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
 convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"

src/Agda/Core/Name.agda

@@ -113,5 +113,6 @@ instance
 pattern Vsuc n p = ⟨ _ ⟩ (Suc n ⟨ IsSuc p ⟩)
 pattern V2suc n p = ⟨ _ ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩)
 pattern Vzero = ⟨ _ ⟩ Zero ⟨ IsZero refl ⟩
+pattern VZero x = ⟨ x ⟩ Zero ⟨ IsZero refl ⟩
 pattern Vone = ⟨ _ ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩
 -------------------------------------------------------------------------------

src/Agda/Core/Rules/Conversion.agda

@@ -118,12 +118,11 @@ data Conv {α} where
     (b : Term (α ▸ x))
     → b ≅ TApp (TVar depPairF) (TVar depPairX) 
     → TVar f ≅ (TLam x b)
-  CEtaVar2 : (@0 x : Name) (f : Term α) (b : Term (α ▸ x)) → 
+  CEtaFunctions : (@0 x : Name) (f : Term α) (b : Term (α ▸ x)) → 
     let 
-    depPairX = ⟨ x ⟩ (Zero ⟨ IsZero refl ⟩)
     subsetProof = (subWeaken subRefl)
     in
-    b ≅ (TApp (weakenTerm subsetProof f) (TVar depPairX))
+    b ≅ (TApp (weakenTerm subsetProof f) (TVar (VZero x)))
     → f ≅ (TLam x b)
 
 

src/Agda/Core/Syntax/Signature.agda

@@ -119,6 +119,8 @@ data Defn : Set where
   FunctionDefn : (funBody : Term mempty) → Defn
   DatatypeDefn :  (@0 d : NameData) → Datatype d → Defn
   ConstructorDefn : (@0 d : NameData) (@0 c : NameCon d) → Constructor c → Defn
+  -- TODO (diode-lang) : add record defn
+  -- RecordDefn : (@0 d : NameData) → {!!} → Defn
 {-# COMPILE AGDA2HS Defn #-}
 
 

src/Agda/Core/Syntax/Term.agda

@@ -31,6 +31,8 @@ data Term α where
         → (TermS α (fieldScope c)) → Term α
   TLam  : (@0 x : Name) (v : Term (α ▸ x)) → Term α
   TApp  : (u : Term α) (v : Term α) → Term α
+  -- TODO (diode-lang) : Add record terms
+  -- TRec : (d : NameData) → {!!} → Term α
   TProj : (u : Term α) (x : NameIn defScope) → Term α
   TCase : {@0 x : Name}
         → (d : NameData)                                  -- Datatype of the variable we are splitting on