Implement let definitions where RHS is a large type

nova-api.ipkg

@@ -15,10 +15,10 @@ modules =
         , Nova.Core.Context
         , Nova.Core.Conversion
         , Nova.Core.Evaluation
-        , Nova.Core.FreeVariable
         , Nova.Core.Language
         , Nova.Core.Monad
         , Nova.Core.Name
+        , Nova.Core.Occurrence
         , Nova.Core.Pretty
         , Nova.Core.Rigidity
         , Nova.Core.Shrinking

nova.ipkg

@@ -15,10 +15,10 @@ modules =
         , Nova.Core.Context
         , Nova.Core.Conversion
         , Nova.Core.Evaluation
-        , Nova.Core.FreeVariable
         , Nova.Core.Language
         , Nova.Core.Monad
         , Nova.Core.Name
+        , Nova.Core.Occurrence
         , Nova.Core.Pretty
         , Nova.Core.Rigidity
         , Nova.Core.Shrinking

src/idris/Nova/Core/Context.idr

@@ -8,38 +8,87 @@ import Nova.Core.Substitution
 ||| Σ ⊦ Δ(↑(x Σ₁))
 ||| Σ Δ(↑(x Σ₁)) ⊦ A(↑(x Σ₁)) type
 public export
-lookupSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
-lookupSignature [<] x = Nothing
-lookupSignature (sig :< (x, ElemEntry ctx ty)) y = M.do
+lookupElemSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
+lookupElemSignature [<] x = Nothing
+lookupElemSignature (sig :< (x, ElemEntry ctx ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, ty) <- lookupSignature sig y
+      (ctx, i, ty) <- lookupElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
-lookupSignature (sig :< (x, LetElemEntry ctx _ ty)) y = M.do
+lookupElemSignature (sig :< (x, LetElemEntry ctx _ ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, ty) <- lookupSignature sig y
+      (ctx, i, ty) <- lookupElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
+lookupElemSignature (sig :< (x, TypeEntry {})) y = do
+  (ctx, i, ty) <- lookupElemSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
+lookupElemSignature (sig :< (x, LetTypeEntry {})) y = do
+  (ctx, i, ty) <- lookupElemSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
 
-||| TODO: Factor this out
 public export
-lookupLetSignature : Signature -> VarName -> Maybe (Context, Nat, Elem, Typ)
-lookupLetSignature [<] x = Nothing
-lookupLetSignature (sig :< (x, ElemEntry ctx ty)) y = M.do
+lookupTypeSignature : Signature -> VarName -> Maybe (Context, Nat)
+lookupTypeSignature [<] x = Nothing
+lookupTypeSignature (sig :< (x, ElemEntry ctx ty)) y = do
+  (ctx, i) <- lookupTypeSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, LetElemEntry ctx _ ty)) y = do
+  (ctx, i) <- lookupTypeSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, TypeEntry ctx)) y = do
   case x == y of
-    True => Nothing
+    True => Just (subst ctx SubstSignature.Wk, 0)
     False => do
-      (ctx, i, rhs, ty) <- lookupLetSignature sig y
-      Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
-lookupLetSignature (sig :< (x, LetElemEntry ctx rhs ty)) y = M.do
+      (ctx, i) <- lookupTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, LetTypeEntry ctx rhs)) y = do
+  case x == y of
+    True => Just (subst ctx SubstSignature.Wk, 0)
+    False => do
+      (ctx, i) <- lookupTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i)
+
+public export
+lookupLetElemSignature : Signature -> VarName -> Maybe (Context, Nat, Elem, Typ)
+lookupLetElemSignature [<] x = Nothing
+lookupLetElemSignature (sig :< (x, ElemEntry ctx ty)) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, TypeEntry {})) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, LetTypeEntry {})) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, LetElemEntry ctx rhs ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, rhs, ty) <- lookupLetSignature sig y
+      (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
 
+public export
+lookupLetTypeSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
+lookupLetTypeSignature [<] x = Nothing
+lookupLetTypeSignature (sig :< (x, ElemEntry ctx ty)) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, TypeEntry {})) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, LetElemEntry {})) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, LetTypeEntry ctx rhs)) y = do
+  case x == y of
+    True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim rhs Wk)
+    False => do
+      (ctx, i, rhs) <- lookupLetTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+
 namespace Index
   ||| Looks up a signature entry by index. Weakens the result to be typed in the original signature.
   public export

src/idris/Nova/Core/Conversion.idr

@@ -34,6 +34,10 @@ mutual
       conv sig omega a0 a1 `and` conv sig omega b0 b1
     convNu sig omega (ElEqTy a0 b0 ty0) (ElEqTy a1 b1 ty1) =
       conv sig omega a0 a1 `and` conv sig omega b0 b1 `and` conv sig omega ty0 ty1
+    convNu sig omega (SignatureVarElim x0 sigma) (SignatureVarElim x1 tau) =
+     return (x0 == x1)
+        `and`
+      conv sig omega sigma tau
     convNu _ _ _ _ = return False
 
     public export

src/idris/Nova/Core/Evaluation.idr

@@ -7,8 +7,6 @@ import Nova.Core.Monad
 import Nova.Core.Language
 import Nova.Core.Substitution
 
---TODO: El should evaluate both in closed and open cases
-
 -- Closed term evaluation
 
 mutual
@@ -171,6 +169,7 @@ mutual
         _ => throw "closedEval(OmegaVarElim)"
     closedEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     closedEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
+    closedEvalNu sig omega (SignatureVarElim idx tau) = return (SignatureVarElim idx tau)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Σ must only contain let-elem's
@@ -214,6 +213,8 @@ mutual
         Nothing => throw "openEval/Type(OmegaVarElim(Nothing))"
     openEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     openEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
+    openEvalNu sig omega (SignatureVarElim k sigma) = M.do
+      return (SignatureVarElim k sigma)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Computes head-normal form w.r.t. (~) relation used in unification.

src/idris/Nova/Core/Language.idr

@@ -9,7 +9,9 @@ mutual
   public export
   data SignatureEntryInstance : Type where
     ElemEntryInstance : Elem -> SignatureEntryInstance
-    LetEntryInstance : SignatureEntryInstance
+    LetElemEntryInstance : SignatureEntryInstance
+    TypeEntryInstance : Typ -> SignatureEntryInstance
+    LetTypeEntryInstance : SignatureEntryInstance
 
   namespace SubstSignature
     ||| σ : Σ₀ ⇒ Σ₁
@@ -89,6 +91,8 @@ mutual
       SignatureSubstElim : Typ -> SubstSignature -> Typ
       ||| Xᵢ(σ)
       OmegaVarElim : OmegaName -> SubstContext -> Typ
+      ||| Xᵢ(σ)
+      SignatureVarElim : Nat -> SubstContext -> Typ
 
   namespace E
     public export
@@ -166,6 +170,10 @@ data SignatureEntry : Type where
   ElemEntry : Context -> Typ -> SignatureEntry
   ||| Γ ⊦ a : A
   LetElemEntry : Context -> Elem -> Typ -> SignatureEntry
+  ||| Γ ⊦ type
+  TypeEntry : Context -> SignatureEntry
+  ||| Γ ⊦ A
+  LetTypeEntry : Context -> Typ -> SignatureEntry
 
 Signature = SnocList (VarName, SignatureEntry)
 
@@ -174,6 +182,8 @@ namespace SignatureEntry
   getContext : SignatureEntry -> Context
   getContext (ElemEntry ctx ty)= ctx
   getContext (LetElemEntry ctx rhs ty) = ctx
+  getContext (TypeEntry ctx)= ctx
+  getContext (LetTypeEntry ctx rhs) = ctx
 
 public export
 data MetaKind = NoSolve | SolveByUnification | SolveByElaboration

src/idris/Nova/Core/FreeVariable.idr → src/idris/Nova/Core/Occurrence.idr

@@ -1,4 +1,4 @@
-module Nova.Core.FreeVariable
+module Nova.Core.Occurrence
 
 import Data.AVL
 
@@ -44,6 +44,7 @@ mutual
       [| unite (freeOmegaName sig omega a) (freeOmegaName sig omega b) |]
     freeOmegaNameNu sig omega (ElEqTy a b ty) = M.do
       [| unite3 (freeOmegaName sig omega a) (freeOmegaName sig omega b) (freeOmegaName sig omega ty) |]
+    freeOmegaNameNu sig omega (SignatureVarElim j sigma) = freeOmegaName sig omega sigma
 
     ||| Compute free occurrences of Ω variables in the term modulo open evaluation.
     public export

src/idris/Nova/Core/Pretty.idr

@@ -106,6 +106,10 @@ wrapTyp (El {}) lvl doc =
   case lvl <= 3 of
     True => return doc
     False => return (parens' doc)
+wrapTyp (SignatureVarElim {}) lvl doc =
+  case lvl <= 3 of
+    True => return doc
+    False => return (parens' doc)
 
 wrapElem : Elem -> Level -> Doc Ann -> M (Doc Ann)
 wrapElem (PiTy x dom cod) lvl doc =
@@ -392,6 +396,12 @@ mutual
     annotate Form "∈"
      <++>
     !(prettyTyp sig omega ctx ty 0)
+  prettyTyp' sig omega ctx (SignatureVarElim k sigma) = M.do
+    x <- prettySignatureVar sig k
+    return $
+      x
+       <+>
+      parens' !(prettySubstContext sig omega ctx sigma)
 
   public export
   prettyTyp : Signature
@@ -632,6 +642,8 @@ mutual
   prettySignatureEntry : Signature -> Omega -> VarName -> SignatureEntry -> M (Doc Ann)
    -- Γ ⊦ χ : A
    -- Γ ⊦ χ ≔ e : A
+   -- Γ ⊦ χ type
+   -- Γ ⊦ χ ≔ A type
   prettySignatureEntry sig omega x (ElemEntry ctx ty) = return $
     !(prettyContext sig omega ctx)
      <++>
@@ -656,6 +668,26 @@ mutual
     annotate Keyword ":"
      <++>
     !(prettyTyp sig omega (map fst ctx) ty 0)
+  prettySignatureEntry sig omega x (TypeEntry ctx) = return $
+    !(prettyContext sig omega ctx)
+     <++>
+    annotate Keyword "⊦"
+     <++>
+    annotate ContextVar (pretty x)
+     <++>
+    annotate Keyword "type"
+  prettySignatureEntry sig omega x (LetTypeEntry ctx e) = return $
+    !(prettyContext sig omega ctx)
+     <++>
+    annotate Keyword "⊦"
+     <++>
+    annotate ContextVar (pretty x)
+     <++>
+    annotate Keyword "≔"
+     <++>
+    !(prettyTyp sig omega (map fst ctx) e 0)
+     <++>
+    annotate Keyword "type"
 
   public export
   prettyConstraintEntry : Signature -> Omega -> ConstraintEntry -> M (Doc Ann)

src/idris/Nova/Core/Rigidity.idr

@@ -34,6 +34,7 @@ mutual
         Nothing => assert_total $ idris_crash "isRigidNu(SignatureVarElim)(3)"
     isRigidNu sig omega (TyEqTy x y) = return True
     isRigidNu sig omega (ElEqTy x y z) = return True
+    isRigidNu sig omega (SignatureVarElim {}) = return True
 
     ||| A term is rigid if
     ||| there is no (~) that changes its constructor.

src/idris/Nova/Core/Shrinking.idr

@@ -93,6 +93,11 @@ mutual
       b <- shrink b gamma1Len gamma2Len
       c <- shrink c gamma1Len gamma2Len
       return (ElEqTy a b c)
+    shrinkNu (SignatureVarElim k sigma) gamma1Len gamma2Len = MMaybe.do
+      -- Σ₀ (Γ ⊦ χ : A) Σ₁ ⊦ σ : Δ ⇒ Γ
+      -- Σ₀ (Γ ⊦ χ : A) Σ₁ Δ ⊦ χ σ
+      sigma <- shrink sigma gamma1Len gamma2Len
+      return (SignatureVarElim k sigma)
 
     ||| Γ₀ ⊦ Γ₁ ctx
     ||| Γ₀ ⊦ Γ₂ ctx

src/idris/Nova/Core/Substitution.idr

@@ -86,8 +86,12 @@ mutual
       subst (SignatureSubstElim t sigma1) spine
     substSignatureVar (S k) (Ext tau _) sigma1 spine =
       substSignatureVar k tau sigma1 spine
-    substSignatureVar 0 (Ext tau (LetEntryInstance {})) sigma1 spine =
-      assert_total $ idris_crash "Elem.substSignatureVar(LetEntryInstance)"
+    substSignatureVar 0 (Ext tau (LetElemEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetElemEntryInstance)"
+    substSignatureVar 0 (Ext tau (TypeEntryInstance t)) sigma1 spine = FailSt.do
+      assert_total $ idris_crash "Elem.substSignatureVar(TypeEntryInstance)"
+    substSignatureVar 0 (Ext tau (LetTypeEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetTypeEntryInstance)"
     substSignatureVar x Terminal sigma1 spine = assert_total $ idris_crash "substSignatureVar(Terminal)"
 
     ||| xᵢ(σ : Γ₁ ⇒ Γ₂)(τ : Γ₀ ⇒ Γ₁)
@@ -259,6 +263,27 @@ mutual
     subst ElEqVal tau = ElEqVal
 
   namespace D
+    public export
+    substSignatureVar : Nat -> SubstSignature -> SubstSignature -> SubstContext -> Typ
+    substSignatureVar x Id Id spine = SignatureVarElim x spine
+    substSignatureVar x Id sigma1 spine = substSignatureVar x sigma1 Id spine
+    substSignatureVar x Wk sigma1 spine = substSignatureVar (S x) sigma1 Id spine
+    substSignatureVar x (Chain Id tau) sigma spine = substSignatureVar x tau sigma spine
+    substSignatureVar x (Chain tau0 tau1) sigma1 spine = substSignatureVar x tau0 (Chain tau1 sigma1) spine
+    -- Σ (Δ ⊦ χ : A) | Γ ⊦ χ₀(ē)[τ, t] = t(ē[τ, t])
+    -- Σ (Δ ⊦ χ : A) | Γ ⊦ χ₁₊ᵢ(ē)[τ, t] = χᵢ(ē[τ, t])[τ]
+    substSignatureVar 0 (Ext tau (ElemEntryInstance t)) sigma1 spine = FailSt.do
+      assert_total $ idris_crash "Elem.substSignatureVar(ElemEntryInstance)"
+    substSignatureVar (S k) (Ext tau _) sigma1 spine =
+      substSignatureVar k tau sigma1 spine
+    substSignatureVar 0 (Ext tau (LetElemEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetElemEntryInstance)"
+    substSignatureVar 0 (Ext tau (TypeEntryInstance t)) sigma1 spine = FailSt.do
+      subst (SignatureSubstElim t sigma1) spine
+    substSignatureVar 0 (Ext tau (LetTypeEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetTypeEntryInstance)"
+    substSignatureVar x Terminal sigma1 spine = assert_total $ idris_crash "substSignatureVar(Terminal)"
+
     public export
     subst : Typ -> SubstSignature -> Typ
     subst (PiTy x a b) sigma = PiTy x (SignatureSubstElim a sigma) (SignatureSubstElim b sigma)
@@ -276,6 +301,7 @@ mutual
     subst (OmegaVarElim k tau) sigma = OmegaVarElim k (subst tau sigma)
     subst (TyEqTy a0 a1) tau = TyEqTy (SignatureSubstElim a0 tau) (SignatureSubstElim a1 tau)
     subst (ElEqTy a0 a1 ty) tau = ElEqTy (SignatureSubstElim a0 tau) (SignatureSubstElim a1 tau) (SignatureSubstElim ty tau)
+    subst (SignatureVarElim k tau) sigma = substSignatureVar k sigma Id (subst tau sigma)
 
   namespace E
     ||| t(σ)
@@ -307,6 +333,7 @@ mutual
     subst (OmegaVarElim k sigma) tau = OmegaVarElim k (Chain sigma tau)
     subst (TyEqTy a0 a1) tau = TyEqTy (ContextSubstElim a0 tau) (ContextSubstElim a1 tau)
     subst (ElEqTy a0 a1 ty) tau = ElEqTy (ContextSubstElim a0 tau) (ContextSubstElim a1 tau) (ContextSubstElim ty tau)
+    subst (SignatureVarElim k sigma) tau = SignatureVarElim k (Chain sigma tau)
 
   namespace List
     public export
@@ -354,12 +381,18 @@ mutual
       ||| σ⁺(E) : Σ₀ E(σ) ⇒ Σ₁ E
       ||| σ⁺(Γ ⊦ x : A) : Σ₀ (Γ(σ) ⊦ x : A(σ)) ⇒ Σ₁ (Γ ⊦ x : A)
       ||| σ⁺(Γ ⊦ x ≔ e : A) : Σ₀ (Γ(σ) ⊦ x ≔ e(σ) : A(σ)) ⇒ Σ₁ (Γ ⊦ x ≔ e : A)
+      ||| σ⁺(Γ ⊦ X type) : Σ₀ (Γ(σ) ⊦ X type) ⇒ Σ₁ (Γ ⊦ X type)
+      ||| σ⁺(Γ ⊦ X ≔ A type) : Σ₀ (Γ(σ) ⊦ X ≔ A(σ) type) ⇒ Σ₁ (Γ ⊦ X ≔ A type)
       public export
       Under : SubstSignature -> SignatureEntry -> SubstSignature
       Under sigma (ElemEntry ctx ty) =
         Ext (Chain sigma Wk) (ElemEntryInstance $ SignatureVarElim 0 Id)
       Under sigma (LetElemEntry ctx e ty) =
-        Ext (Chain sigma Wk) LetEntryInstance
+        Ext (Chain sigma Wk) LetElemEntryInstance
+      Under sigma (TypeEntry ctx) =
+        Ext (Chain sigma Wk) (TypeEntryInstance $ SignatureVarElim 0 Id)
+      Under sigma (LetTypeEntry ctx rhs) =
+        Ext (Chain sigma Wk) LetTypeEntryInstance
 
       ||| σ : Σ₀ ⇒ Σ₁
       ||| Σ₁ ⊦ Δ sig
@@ -385,6 +418,8 @@ namespace SignatureEntry
   subst : SignatureEntry -> SubstSignature -> SignatureEntry
   subst (ElemEntry ctx ty) sigma = ElemEntry (subst ctx sigma) (SignatureSubstElim ty sigma)
   subst (LetElemEntry ctx e ty) sigma = LetElemEntry (subst ctx sigma) (SignatureSubstElim e sigma) (SignatureSubstElim ty sigma)
+  subst (TypeEntry ctx) sigma = TypeEntry (subst ctx sigma)
+  subst (LetTypeEntry ctx rhs) sigma = LetTypeEntry (subst ctx sigma) (SignatureSubstElim rhs sigma)
 
 namespace EntryList
   public export