Revert "starting progress on (non-dependent) products"

This reverts commit 2c1f193d77.

examples/logic.pg

@@ -35,17 +35,19 @@ def double_neg_intro (A : ★) (a : A) : not (not A) :=
 
 -- Conjunction
 
-def ∧ (A B : ★) : ★ := A × B;
+def ∧ (A B : ★) : ★ := {A × B};
 infixl 10 ∧;
 
 -- introduction rule
-def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := (a, b);
+def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := <a, b>;
 
 -- left elimination rule
-def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab;
+def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
+    ab A (fun (a : A) (b : B) => a);
 
 -- right elimination rule
-def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab;
+def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
+    ab B (fun (a : A) (b : B) => b);
 
 -- --------------------------------------------------------------------------------------------------------------
 
@@ -146,25 +148,27 @@ section Theorems
 
     -- ~(A ∨ B) => ~A ∧ ~B
     def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
-        ( [a : A] h (or_intro_l A B a)
+        <[a : A] h (or_intro_l A B a)
-        , [b : B] h (or_intro_r A B b));
+        ,[b : B] h (or_intro_r A B b)>;
 
     -- ~A ∧ ~B => ~(A ∨ B)
     def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
         fun (contra : A ∨ B) => 
-            or_elim A B false contra (π₁ h) (π₂ h);
+            or_elim A B false contra
+                (and_elim_l (not A) (not B) h)
+                (and_elim_r (not A) (not B) h);
 
     -- ~A ∨ ~B => ~(A ∧ B)
     def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
         fun (contra : A ∧ B) =>
             or_elim (not A) (not B) false h
-                (fun (na : not A) => na (π₁ contra))
+                (fun (na : not A) => na (and_elim_l A B contra))
-                (fun (nb : not B) => nb (π₂ contra));
+                (fun (nb : not B) => nb (and_elim_r A B contra));
 
     -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
 
     -- A ∧ B => B ∧ A
-    def and_comm (h : A ∧ B) : B ∧ A := (π₂ h, π₁ h);
+    def and_comm (h : A ∧ B) : B ∧ A := <π₂ h, π₁ h>;
 
     -- A ∨ B => B ∨ A
     def or_comm (h : A ∨ B) : B ∨ A :=
@@ -174,11 +178,11 @@ section Theorems
 
     -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
     def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
-        ((π₁ h, π₁ (π₂ h)), π₂ (π₂ h));
+        <<π₁ h, π₁ (π₂ h)>, π₂ (π₂ h)>;
 
     -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
     def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
-        (π₁ (π₁ h), (π₂ (π₁ h), π₂ h));
+        <π₁ (π₁ h), <π₂ (π₁ h), π₂ h>>;
 
     -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
     def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
@@ -201,14 +205,14 @@ section Theorems
     -- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
     def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
         or_elim B C (A ∧ B ∨ A ∧ C) (π₂ h)
-            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) (π₁ h, b))
+            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) <π₁ h, b>)
-            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C) (π₁ h, c));
+            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C) <π₁ h, c>);
 
     -- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
     def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
         or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
-            (fun (ab : A ∧ B) => (π₁ ab, or_intro_l B C (π₂ ab)))
+            (fun (ab : A ∧ B) => <π₁ ab, or_intro_l B C (π₂ ab)>)
-            (fun (ac : A ∧ C) => (π₁ ac, or_intro_r B C (π₂ ac)));
+            (fun (ac : A ∧ C) => <π₁ ac, or_intro_r B C (π₂ ac)>);
 
     -- Thanks Quinn!
     -- A ∨ B => ~B => A

lib/Check.hs

@@ -16,12 +16,6 @@ matchPi x mt =
         (Pi _ a b) -> pure (a, b)
         t -> throwError $ ExpectedPiType x t
 
-matchProd :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
-matchProd x mt =
-    whnf mt >>= \case
-        (Prod a b) -> pure (a, b)
-        t -> throwError $ ExpectedProdType x t
-
 findLevel :: Context -> Expr -> ReaderT Env Result Integer
 findLevel g a = do
     s <- findType g a
@@ -78,17 +72,6 @@ findType g e@(Let _ (Just t) v b) = do
     _ <- findType g t
     betaEquiv' e t res
     pure t
-findType g (Prod a b) = do
-    aSort <- findType g a
-    bSort <- findType g b
-    liftEither $ compSort a b aSort bSort
-findType g (Pair a b) = do
-    aType <- findType g a
-    bType <- findType g b
-    validateType g $ Prod aType bType
-    pure $ Prod aType bType
-findType g (Pi1 x) = fst <$> (findType g x >>= matchProd x)
-findType g (Pi2 x) = snd <$> (findType g x >>= matchProd x)
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env

lib/Elaborator.hs

@@ -116,10 +116,6 @@ usedVars (I.Let name ascr value body) = saveState $ do
     ascr' <- traverse usedVars ascr
     removeName name
     S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
-usedVars (I.Prod m n) = S.union <$> usedVars m <*> usedVars n
-usedVars (I.Pair m n) = S.union <$> usedVars m <*> usedVars n
-usedVars (I.Pi1 x) = usedVars x
-usedVars (I.Pi2 x) = usedVars x
 
 -- traverse the body of a definition, adding the necessary section arguments to
 -- any definitions made within the section
@@ -146,10 +142,6 @@ traverseBody (I.Let name ascr value body) = saveState $ do
     value' <- traverseBody value
     removeName name
     I.Let name ascr' value' <$> traverseBody body
-traverseBody (I.Prod m n) = I.Prod <$> traverseBody m <*> traverseBody n
-traverseBody (I.Pair m n) = I.Pair <$> traverseBody m <*> traverseBody n
-traverseBody (I.Pi1 x) = I.Pi1 <$> traverseBody x
-traverseBody (I.Pi2 x) = I.Pi2 <$> traverseBody x
 
 mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
 mkPi (param, typ) = I.Pi param typ
@@ -214,7 +206,3 @@ elaborate ir = evalState (elaborate' ir) []
         ty' <- elaborate' ty
         modify (name :)
         E.Let name (Just ty') val' <$> elaborate' body
-    elaborate' (I.Prod m n) = E.Prod <$> elaborate' m <*> elaborate' n
-    elaborate' (I.Pair m n) = E.Pair <$> elaborate' m <*> elaborate' n
-    elaborate' (I.Pi1 x) = E.Pi1 <$> elaborate' x
-    elaborate' (I.Pi2 x) = E.Pi2 <$> elaborate' x

lib/Errors.hs

@@ -9,7 +9,6 @@ data Error
     = UnboundVariable Text
     | NotASort Expr
     | ExpectedPiType Expr Expr
-    | ExpectedProdType Expr Expr
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
@@ -19,7 +18,6 @@ instance Pretty Error where
     pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
     pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
     pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
-    pretty (ExpectedProdType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
     pretty (NotEquivalent a a' e) =
         group $
             hang 4 ("Cannot unify" <> line <> pretty a)

lib/Eval.hs

@@ -45,10 +45,6 @@ subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
-subst k s (Prod m n) = Prod (subst k s m) (subst k s n)
-subst k s (Pair m n) = Pair (subst k s m) (subst k s n)
-subst k s (Pi1 x) = Pi1 (subst k s x)
-subst k s (Pi2 x) = Pi2 (subst k s x)
 
 envLookupVal :: Text -> ReaderT Env Result Expr
 envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
@@ -63,12 +59,6 @@ reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
 reduce (Let _ _ v b) = pure $ subst 0 v b
-reduce (Prod a b) = Prod <$> reduce a <*> reduce b
-reduce (Pair a b) = Pair <$> reduce a <*> reduce b
-reduce (Pi1 (Pair a _)) = pure a
-reduce (Pi2 (Pair _ b)) = pure b
-reduce (Pi1 x) = Pi1 <$> reduce x
-reduce (Pi2 x) = Pi2 <$> reduce x
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -88,18 +78,6 @@ whnf (App m n) = do
         else whnf $ App m' n
 whnf (Free n) = envLookupVal n >>= whnf
 whnf (Let _ _ v b) = whnf $ subst 0 v b
-whnf (Pi1 (Pair a _)) = pure a
-whnf (Pi2 (Pair _ b)) = pure b
-whnf (Pi1 x) = do
-    x' <- whnf x
-    if x == x'
-        then pure $ Pi1 x
-        else whnf $ Pi1 x'
-whnf (Pi2 x) = do
-    x' <- whnf x
-    if x == x'
-        then pure $ Pi2 x
-        else whnf $ Pi2 x'
 whnf e = pure e
 
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
@@ -121,10 +99,6 @@ betaEquiv e1 e2
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
-            (Prod a b, Prod a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
-            (Pair a b, Pair a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
-            (Pi1 x, Pi1 x') -> betaEquiv x x'
-            (Pi2 x, Pi2 x') -> betaEquiv x x'
             _ -> pure False -- remaining cases impossible, false, or redundant
 
 betaEquiv' :: Expr -> Expr -> Expr -> ReaderT Env Result ()

lib/Expr.hs

@@ -15,10 +15,6 @@ data Expr where
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
     Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
-    Prod :: Expr -> Expr -> Expr
-    Pair :: Expr -> Expr -> Expr
-    Pi1 :: Expr -> Expr
-    Pi2 :: Expr -> Expr
     deriving (Show, Ord)
 
 instance Pretty Expr where
@@ -34,10 +30,6 @@ instance Eq Expr where
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
     (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
-    (Prod x1 y1) == (Prod x2 y2) = x1 == x2 && y1 == y2
-    (Pair x1 y1) == (Pair x2 y2) = x1 == x2 && y1 == y2
-    (Pi1 x) == (Pi1 y) = x == y
-    (Pi2 x) == (Pi2 y) = x == y
     _ == _ = False
 
 occursFree :: Integer -> Expr -> Bool
@@ -50,10 +42,6 @@ occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
-occursFree n (Prod x y) = occursFree n x || occursFree n y
-occursFree n (Pair x y) = occursFree n x || occursFree n y
-occursFree n (Pi1 x) = occursFree n x
-occursFree n (Pi2 x) = occursFree n x
 
 shiftIndices :: Integer -> Integer -> Expr -> Expr
 shiftIndices d c (Var x k)
@@ -67,10 +55,6 @@ shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
-shiftIndices d c (Prod m n) = Prod (shiftIndices d c m) (shiftIndices d c n)
-shiftIndices d c (Pair m n) = Pair (shiftIndices d c m) (shiftIndices d c n)
-shiftIndices d c (Pi1 x) = Pi1 (shiftIndices d c x)
-shiftIndices d c (Pi2 x) = Pi2 (shiftIndices d c x)
 
 incIndices :: Expr -> Expr
 incIndices = shiftIndices 1 0
@@ -222,10 +206,6 @@ prettyExpr k expr = case expr of
       where
         (binds, body) = collectLets expr
         bindings = sep $ map pretty binds
-    (Prod x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y)
-    (Pair x y) -> parens $ pretty x <> "," <+> pretty y
-    (Pi1 x) -> parens $ "π₁" <+> parens (pretty x)
-    (Pi2 x) -> parens $ "π₂" <+> parens (pretty x)
 
 prettyT :: Expr -> Text
 prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty

lib/IR.hs

@@ -27,16 +27,6 @@ data IRExpr
         , letValue :: IRExpr
         , letBody :: IRExpr
         }
-    | Prod
-        { prodLeft :: IRExpr
-        , prodRight :: IRExpr
-        }
-    | Pair
-        { pairLeft :: IRExpr
-        , pairRight :: IRExpr
-        }
-    | Pi1 IRExpr
-    | Pi2 IRExpr
     deriving (Show, Eq, Ord)
 
 data IRSectionDef

lib/Parser.hs

@@ -187,11 +187,16 @@ pSort = lexeme $ pStar <|> pSquare
 pOpSection :: Parser IRExpr
 pOpSection = lexeme $ parens $ Var <$> pSymbol
 
-pPair :: Parser IRExpr
+pProd :: Parser IRExpr
-pPair = lexeme $ between (char '(') (char ')') $ do
+pProd = lexeme $ between (char '{') (char '}') $ do
-    skipSpace
     left <- pIRExpr
-    _ <- lexeme $ symbol ","
+    _ <- symbol "×"
+    Prod left <$> pIRExpr
+
+pPair :: Parser IRExpr
+pPair = lexeme $ between (char '<') (char '>') $ do
+    left <- pIRExpr
+    _ <- symbol ","
     Pair left <$> pIRExpr
 
 pPi1 :: Parser IRExpr
@@ -201,7 +206,7 @@ pPi2 :: Parser IRExpr
 pPi2 = lexeme $ symbol "π₂" >> Pi2 <$> pIRExpr
 
 pTerm :: Parser IRExpr
-pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, try pPair, try pOpSection, parens pIRExpr]
+pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, pProd, pPair, try pOpSection, parens pIRExpr]
 
 pInfix :: Parser IRExpr
 pInfix = parseWithPrec 0