Inference for Elem: return the canonical type; Remove nova.ipkg; Fix …

…an indexing bug in Context.idr

nova-api.ipkg

@@ -15,6 +15,7 @@ modules =
         , Nova.Core.Context
         , Nova.Core.Conversion
         , Nova.Core.Evaluation
+        , Nova.Core.Inference
         , Nova.Core.Language
         , Nova.Core.Monad
         , Nova.Core.Name

src/idris/Nova/Core/Context.idr

@@ -1,5 +1,9 @@
 module Nova.Core.Context
 
+import Data.Fin
+import Data.Util
+import Data.AVL
+
 import Nova.Core.Language
 import Nova.Core.Substitution
 
@@ -94,7 +98,38 @@ namespace Index
   public export
   lookupSignature : Signature -> Nat -> Maybe (VarName, SignatureEntry)
   lookupSignature [<] _ = Nothing
-  lookupSignature (_ :< (x, t)) Z = Just (x, t)
+  lookupSignature (_ :< (x, t)) Z = Just (x, subst t Wk)
   lookupSignature (sig :< _) (S k) = do
     (x, e) <- lookupSignature sig k
     pure (x, subst e Wk)
+
+  ||| Weakens the type.
+  public export
+  lookupContext : Context -> Nat -> Maybe (VarName, Typ)
+  lookupContext ctx idx = do
+    (_, (x, ty), _) <- mbIndex idx ctx
+    pure (x, ContextSubstElim ty (Context.WkN (S idx)))
+
+||| In case the entry is an element entry, return the context and the type.
+public export
+mbElemSignature : SignatureEntry -> Maybe (Context, Typ)
+mbElemSignature (ElemEntry ctx ty) = Just (ctx, ty)
+mbElemSignature (LetElemEntry ctx rhs ty) = Just (ctx, ty)
+mbElemSignature (TypeEntry sx) = Nothing
+mbElemSignature (LetTypeEntry sx x) = Nothing
+
+namespace Omega
+  public export
+  lookupOmega : Omega -> OmegaName -> Maybe OmegaEntry
+  lookupOmega omega x = OrdTree.lookup x omega
+
+  ||| In case the entry is an element entry, return the context and the type.
+  public export
+  mbElemSignature : OmegaEntry -> Maybe (Context, Typ)
+  mbElemSignature (MetaType {}) = Nothing
+  mbElemSignature (LetType {}) = Nothing
+  mbElemSignature (MetaElem ctx ty _) = Just (ctx, ty)
+  mbElemSignature (LetElem ctx rhs ty) = Just (ctx, ty)
+  mbElemSignature (TypeConstraint sx x y) = Nothing
+  mbElemSignature (ElemConstraint sx x y z) = Nothing
+  mbElemSignature (SubstContextConstraint x y sx sy) = Nothing

src/idris/Nova/Core/Conversion.idr

@@ -57,7 +57,7 @@ mutual
       conv sig omega f0 f1
     convNu sig omega (ImplicitPiVal x0 _ _ f0) (ImplicitPiVal x1 _ _ f1) =
       conv sig omega f0 f1
-    convNu sig omega (SigmaVal p0 q0) (SigmaVal p1 q1) =
+    convNu sig omega (SigmaVal _ _ _ p0 q0) (SigmaVal _ _ _ p1 q1) =
       conv sig omega p0 p1 `and` conv sig omega q0 q1
     convNu sig omega (PiElim f0 x0 a0 b0 e0) (PiElim f1 x1 a1 b1 e1) =
       conv sig omega f0 f1 `and` conv sig omega e0 e1
@@ -82,7 +82,7 @@ mutual
       conv sig omega z0 z1
         `and`
       conv sig omega s0 s1
-    convNu sig omega (ZeroElim t0) (ZeroElim t1) =
+    convNu sig omega (ZeroElim _ t0) (ZeroElim _ t1) =
       conv sig omega t0 t1
     convNu sig omega (ContextSubstElim {}) b = throw "convNu(ContextSubstElim)"
     convNu sig omega (SignatureSubstElim {}) b = throw "convNu(SignatureSubstElim)"

src/idris/Nova/Core/Evaluation.idr

@@ -19,13 +19,13 @@ mutual
     closedEvalNu sig omega ZeroTy = return ZeroTy
     closedEvalNu sig omega OneTy = return OneTy
     closedEvalNu sig omega OneVal = return OneVal
-    closedEvalNu sig omega (ZeroElim t) = throw "closedEval(ZeroElim)"
+    closedEvalNu sig omega (ZeroElim ty t) = throw "closedEval(ZeroElim)"
     closedEvalNu sig omega (PiTy x a b) = return (PiTy x a b)
     closedEvalNu sig omega (ImplicitPiTy x a b) = return (ImplicitPiTy x a b)
     closedEvalNu sig omega (SigmaTy x a b) = return (SigmaTy x a b)
     closedEvalNu sig omega (PiVal x a b f) = return (PiVal x a b f)
     closedEvalNu sig omega (ImplicitPiVal x a b f) = return (ImplicitPiVal x a b f)
-    closedEvalNu sig omega (SigmaVal a b) = return (SigmaVal a b)
+    closedEvalNu sig omega (SigmaVal x a b p q) = return (SigmaVal x a b p q)
     closedEvalNu sig omega (PiElim f x a b e) = M.do
       PiVal _ _ _ f <- closedEval sig omega f
         | _ => throw "closedEval(PiElim)"
@@ -35,11 +35,11 @@ mutual
         | _ => throw "closedEval(ImplicitPiElim)"
       closedEval sig omega (ContextSubstElim f (Ext Terminal e))
     closedEvalNu sig omega (SigmaElim1 f x a b) = M.do
-      SigmaVal p q <- closedEval sig omega f
+      SigmaVal _ _ _ p q <- closedEval sig omega f
         | _ => throw "closedEval(SigmaElim1)"
       closedEval sig omega p
     closedEvalNu sig omega (SigmaElim2 f x a b) = M.do
-      SigmaVal p q <- closedEval sig omega f
+      SigmaVal _ _ _ p q <- closedEval sig omega f
         | _ => throw "closedEval(SigmaElim2)"
       closedEval sig omega q
     closedEvalNu sig omega NatVal0 = return NatVal0
@@ -62,8 +62,8 @@ 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 TyEqVal = return TyEqVal
-    closedEvalNu sig omega ElEqVal = return ElEqVal
+    closedEvalNu sig omega (TyEqVal ty) = return (TyEqVal ty)
+    closedEvalNu sig omega (ElEqVal ty e) = return (ElEqVal ty e)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Σ must only contain let-elem's
@@ -79,14 +79,14 @@ mutual
     openEvalNu sig omega OneTy = return OneTy
     openEvalNu sig omega NatTy = return NatTy
     openEvalNu sig omega OneVal = return OneVal
-    openEvalNu sig omega (ZeroElim t) = M.do
-      return (ZeroElim t)
+    openEvalNu sig omega (ZeroElim ty t) = M.do
+      return (ZeroElim ty t)
     openEvalNu sig omega (PiTy x a b) = return (PiTy x a b)
     openEvalNu sig omega (ImplicitPiTy x a b) = return (ImplicitPiTy x a b)
     openEvalNu sig omega (SigmaTy x a b) = return (SigmaTy x a b)
     openEvalNu sig omega (PiVal x a b f) = return (PiVal x a b f)
     openEvalNu sig omega (ImplicitPiVal x a b f) = return (ImplicitPiVal x a b f)
-    openEvalNu sig omega (SigmaVal a b) = return (SigmaVal a b)
+    openEvalNu sig omega (SigmaVal x a b p q) = return (SigmaVal x a b p q)
     openEvalNu sig omega (PiElim f x a b e) = M.do
       PiVal _ _ _ f <- openEval sig omega f
         | f => return (PiElim f x a b e)
@@ -96,11 +96,11 @@ mutual
         | f => return (ImplicitPiElim f x a b e)
       openEval sig omega (ContextSubstElim f (Ext Id e))
     openEvalNu sig omega (SigmaElim1 f x a b) = M.do
-      SigmaVal p q <- openEval sig omega f
+      SigmaVal _ _ _ p q <- openEval sig omega f
         | f => return (SigmaElim1 f x a b)
       openEval sig omega p
     openEvalNu sig omega (SigmaElim2 f x a b) = M.do
-      SigmaVal p q <- openEval sig omega f
+      SigmaVal _ _ _ p q <- openEval sig omega f
         | f => return (SigmaElim2 f x a b)
       openEval sig omega q
     openEvalNu sig omega NatVal0 = return NatVal0
@@ -129,8 +129,8 @@ mutual
         Nothing => throw "openEval/Elem(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 TyEqVal = return TyEqVal
-    openEvalNu sig omega ElEqVal = return ElEqVal
+    openEvalNu sig omega (TyEqVal ty) = return (TyEqVal ty)
+    openEvalNu sig omega (ElEqVal ty e) = return (ElEqVal ty e)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Computes head-normal form w.r.t. (~) relation used in unification.

src/idris/Nova/Core/Inference.idr

@@ -0,0 +1,58 @@
+module Nova.Core.Inference
+
+import Nova.Core.Context
+import Nova.Core.Evaluation
+import Nova.Core.Language
+import Nova.Core.Monad
+
+-- Every Elem has a canonical syntactic type
+-- Moreover, every Elem has a unique type up to equality.
+
+public export
+inferNu : Signature -> Omega -> Context -> Elem -> M Typ
+inferNu sig omega ctx (PiTy str x y) = return UniverseTy
+inferNu sig omega ctx (ImplicitPiTy str x y) = return UniverseTy
+inferNu sig omega ctx (SigmaTy str x y) = return UniverseTy
+inferNu sig omega ctx (PiVal x dom cod f) = return (PiTy x dom cod)
+inferNu sig omega ctx (ImplicitPiVal x dom cod f) = return (ImplicitPiTy x dom cod)
+inferNu sig omega ctx (SigmaVal x dom cod p q) = return (SigmaTy x dom cod)
+inferNu sig omega ctx (PiElim f x dom cod e) = return (ContextSubstElim cod (Ext Id e))
+inferNu sig omega ctx (ImplicitPiElim f x dom cod e) = return (ContextSubstElim cod (Ext Id e))
+inferNu sig omega ctx (SigmaElim1 f x dom cod) = return dom
+inferNu sig omega ctx (SigmaElim2 f x dom cod) = return (ContextSubstElim cod (Ext Id (SigmaElim1 f x dom cod)))
+inferNu sig omega ctx NatVal0 = return NatTy
+inferNu sig omega ctx (NatVal1 x) = return NatTy
+inferNu sig omega ctx NatTy = return UniverseTy
+inferNu sig omega ctx (NatElim x schema z y h s t) = return (ContextSubstElim schema (Ext Id t))
+inferNu sig omega ctx (ContextSubstElim x y) = assert_total $ idris_crash "inferNu(ContextSubstElim)"
+inferNu sig omega ctx (SignatureSubstElim x y) = assert_total $ idris_crash "inferNu(SignatureSubstElim)"
+inferNu sig omega ctx (ContextVarElim k) = M.do
+  case lookupContext ctx k of
+    Just (x, ty) => return ty
+    Nothing => assert_total $ idris_crash "inferNu(ContextVarElim)"
+inferNu sig omega ctx (SignatureVarElim k tau) =
+  case lookupSignature sig k of
+    Just (x, e) =>
+      case mbElemSignature e of
+        Just (delta, ty) => return (ContextSubstElim ty tau)
+        Nothing => assert_total $ idris_crash "inferNu(SignatureVarElim(1))"
+    Nothing => assert_total $ idris_crash "inferNu(SignatureVarElim(2))"
+inferNu sig omega ctx (OmegaVarElim x tau) =
+  case lookupOmega omega x of
+    Just e =>
+      case mbElemSignature e of
+        Just (ctx, ty) => return (ContextSubstElim ty tau)
+        Nothing =>  assert_total $ idris_crash "inferNu(OmegaVarElim(1))"
+    Nothing => assert_total $ idris_crash "inferNu(OmegaVarElim(2))"
+inferNu sig omega ctx (TyEqTy x y) = return UniverseTy
+inferNu sig omega ctx (ElEqTy x y z) = return UniverseTy
+inferNu sig omega ctx (TyEqVal ty) = return (TyEqTy ty ty)
+inferNu sig omega ctx (ElEqVal ty a) = return (ElEqTy a a ty)
+inferNu sig omega ctx ZeroTy = return UniverseTy
+inferNu sig omega ctx OneTy = return UniverseTy
+inferNu sig omega ctx OneVal = return OneTy
+inferNu sig omega ctx (ZeroElim ty y) = return ty
+
+public export
+infer : Signature -> Omega -> Context -> Elem -> M Typ
+infer sig omega ctx el = inferNu sig omega ctx !(openEval sig omega el)

src/idris/Nova/Core/Language.idr

@@ -108,7 +108,7 @@ mutual
       ||| {x} ↦ f
       ImplicitPiVal : VarName -> Typ -> Typ -> Elem -> Elem
       ||| (a, b)
-      SigmaVal : Elem -> Elem -> Elem
+      SigmaVal : VarName -> Typ -> Typ -> Elem -> Elem -> Elem
       ||| (f : (x : A) → B) e
       PiElim : Elem -> VarName -> Typ -> Typ -> Elem -> Elem
       ||| {f : {x : A} → B} e
@@ -140,17 +140,17 @@ mutual
       ||| a₀ ≡ a₁ ∈ A
       ElEqTy : Elem -> Elem -> Elem -> Elem
       ||| Refl
-      TyEqVal : Elem
+      TyEqVal : Typ -> Elem
       ||| Refl
-      ElEqVal : Elem
+      ElEqVal : Typ -> Elem -> Elem
       ||| 𝟘
       ZeroTy : Elem
       ||| 𝟙
       OneTy : Elem
       ||| ()
       OneVal : Elem
-      ||| 𝟘-elim t
-      ZeroElim : Elem -> Elem
+      ||| 𝟘-elim A t
+      ZeroElim : Typ -> Elem -> Elem
 
   public export
   Context : Type

src/idris/Nova/Core/Occurrence.idr

@@ -64,8 +64,8 @@ mutual
       [| unite3 (freeOmegaName sig omega dom) (freeOmegaName sig omega cod) (freeOmegaName sig omega f) |]
     freeOmegaNameNu sig omega (ImplicitPiVal x dom cod f) =
       [| unite3 (freeOmegaName sig omega dom) (freeOmegaName sig omega cod) (freeOmegaName sig omega f) |]
-    freeOmegaNameNu sig omega (SigmaVal p q) =
-      [| unite (freeOmegaName sig omega p) (freeOmegaName sig omega q) |]
+    freeOmegaNameNu sig omega (SigmaVal x a b p q) = M.do
+      [| unite4 (freeOmegaName sig omega a) (freeOmegaName sig omega b) (freeOmegaName sig omega p) (freeOmegaName sig omega q) |]
     freeOmegaNameNu sig omega (PiElim f x dom cod e) = M.do
       [|
          unite4 (freeOmegaName sig omega f)
@@ -90,8 +90,8 @@ mutual
     freeOmegaNameNu sig omega ZeroTy = return empty
     freeOmegaNameNu sig omega OneTy = return empty
     freeOmegaNameNu sig omega OneVal = return empty
-    freeOmegaNameNu sig omega (ZeroElim t) = M.do
-      freeOmegaName sig omega t
+    freeOmegaNameNu sig omega (ZeroElim ty t) = M.do
+      [| unite (freeOmegaName sig omega ty) (freeOmegaName sig omega t) |]
     freeOmegaNameNu sig omega (NatElim x schema z y h s t) = M.do
       [| unite4
            (freeOmegaName sig omega schema)
@@ -110,8 +110,9 @@ 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 TyEqVal = return empty
-    freeOmegaNameNu sig omega ElEqVal = return empty
+    freeOmegaNameNu sig omega (TyEqVal ty) = freeOmegaName sig omega ty
+    freeOmegaNameNu sig omega (ElEqVal ty e) = M.do
+      [| unite (freeOmegaName sig omega ty) (freeOmegaName sig omega e) |]
 
     ||| Compute free occurrences of Ω variables in the term modulo open evaluation.
     public export

src/idris/Nova/Core/Pretty.idr

@@ -192,7 +192,7 @@ wrapElem (NatElim str x y str1 str2 z w) lvl doc =
   case lvl <= 3 of
     True => return doc
     False => return (parens' doc)
-wrapElem (ZeroElim _) lvl doc =
+wrapElem (ZeroElim _ _) lvl doc =
   case lvl <= 3 of
     True => return doc
     False => return (parens' doc)
@@ -497,7 +497,7 @@ mutual
       annotate Intro "↦"
        <++>
       !(prettyElem sig omega (ctx :< x) f 0)
-  prettyElem' sig omega ctx (SigmaVal a b) =
+  prettyElem' sig omega ctx (SigmaVal _ _ _ a b) =
     return $ introParens' $
       !(prettyElem sig omega ctx a 0)
        <+>
@@ -538,7 +538,7 @@ mutual
     return $ annotate Form "𝟙"
   prettyElem' sig omega ctx OneVal =
     return $ annotate Intro "()"
-  prettyElem' sig omega ctx (ZeroElim t) = M.do
+  prettyElem' sig omega ctx (ZeroElim _ t) = M.do
     return $
       annotate Elim "𝟘-elim"
        <++>
@@ -595,9 +595,9 @@ mutual
     annotate Form "∈"
      <++>
     !(prettyElem sig omega ctx ty 0)
-  prettyElem' sig omega ctx TyEqVal =
+  prettyElem' sig omega ctx (TyEqVal _) =
     return $ annotate Intro "Refl"
-  prettyElem' sig omega ctx ElEqVal =
+  prettyElem' sig omega ctx (ElEqVal _ _) =
     return $ annotate Intro "Refl"
 
   public export

src/idris/Nova/Core/Rigidity.idr

@@ -63,7 +63,7 @@ mutual
     isRigidNu sig omega ZeroTy = return True
     isRigidNu sig omega OneTy = return True
     isRigidNu sig omega OneVal = return True
-    isRigidNu sig omega (ZeroElim t) = return True
+    isRigidNu sig omega (ZeroElim _ t) = return True
     isRigidNu sig omega (NatElim str x y str1 str2 z w) = return True
     isRigidNu sig omega (ContextSubstElim x y) = assert_total $ idris_crash "isRigidNu(ContextSubstElim)"
     isRigidNu sig omega (SignatureSubstElim x y) = assert_total $ idris_crash "isRigidNu(SignatureSubstElim)"
@@ -81,8 +81,8 @@ 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 TyEqVal = return True
-    isRigidNu sig omega ElEqVal = return True
+    isRigidNu sig omega (TyEqVal _) = return True
+    isRigidNu sig omega (ElEqVal _ _) = return True
 
     ||| A term is rigid if
     ||| there is no (~) that changes its constructor.