fixed some sneaky bugs

examples/peano.pg

@@ -404,7 +404,7 @@ def rec_def_sat_suc : eq2 rec_def := fun (n : nat) =>
 
 -- {{{ The function satisfying these equations is unique
 
-def rec_def_unique (fS : nat -> A -> A) (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
+def rec_def_unique (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
     : forall (n : nat), eq A (f n) (g n) :=
         nat_ind (fun (n : nat) => eq A (f n) (g n))
         -- base case: f 0 = g 0

lib/Eval.hs

@@ -80,6 +80,12 @@ normalize e = do
         then pure e
         else normalize e'
 
+-- betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
+-- betaEquiv e1 e2 = do
+--     e1' <- normalize e1
+--     e2' <- normalize e2
+--     pure $ e1' == e2'
+
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
 betaEquiv e1 e2
     | e1 == e2 = pure True
@@ -87,11 +93,16 @@ betaEquiv e1 e2
         e1' <- whnf e1
         e2' <- whnf e2
         case (e1', e2') of
+            (Var _ n1, Var _ n2) -> pure $ n1 == n2
+            (Free n, Free m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
+            (Axiom n1, Axiom n2) -> pure $ n1 == n2
+            (Star, Star) -> pure True
+            (Level i, Level j) -> pure $ i == j
+            (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
             (Abs _ t1 _ v1, Abs _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
             (Pi _ t1 _ v1, Pi _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
-            (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible, false, or redundant

lib/Expr.hs

@@ -18,7 +18,7 @@ data Expr where
     deriving (Show, Ord)
 
 instance Pretty Expr where
-    pretty = prettyExpr 0 . cleanNames
+    pretty = prettyExpr 0 . cleanNames . dedupNames
 
 instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
@@ -27,8 +27,8 @@ instance Eq Expr where
     Star == Star = True
     (Level i) == (Level j) = i == j
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
-    (Abs _ _ t1 b1) == (Abs _ _ t2 b2) = t1 == t2 && b1 == b2
-    (Pi _ _ t1 b1) == (Pi _ _ t2 b2) = t1 == t2 && b1 == b2
+    (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
     _ == _ = False
 
@@ -61,6 +61,26 @@ incIndices = shiftIndices 1 0
 
 {- --------------------- PRETTY PRINTING ----------------------------- -}
 
+dedupNames :: Expr -> Expr
+dedupNames = go []
+  where
+    varName :: [Text] -> Text -> Int -> Text
+    varName bs x k = case bs !!? k of
+        Nothing -> x
+        Just x' ->
+            let count = (length $ filter (== x') $ drop (k + 1) bs)
+             in if count > 0
+                    then x <> printLevel count
+                    else x
+
+    go :: [Text] -> Expr -> Expr
+    go bs (Var x k) = Var (varName bs x (fromIntegral k)) k
+    go bs (App m n) = App (go bs m) (go bs n)
+    go bs (Abs x ty ascr b) = Abs (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b)
+    go bs (Pi x ty ascr b) = Pi (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b)
+    go bs (Let x ascr val b) = Let (varName (x : bs) x 0) (go bs <$> ascr) (go bs val) (go (x : bs) b)
+    go _ e = e
+
 data Param = Param Text Expr
 data ParamGroup = ParamGroup [Text] Expr
 data Binding = Binding Text [ParamGroup] Expr
@@ -96,6 +116,12 @@ collectPis (Pi x ty _ body) = (Param x ty : params, final)
     (params, final) = collectPis body
 collectPis e = ([], e)
 
+collectArrows :: Expr -> NonEmpty Expr
+collectArrows (Pi "" t1 _ t2) = t1 :| toList rest
+  where
+    rest = collectArrows t2
+collectArrows e = pure e
+
 collectApps :: Expr -> NonEmpty Expr
 collectApps (App e1 e2) = e2 :| toList rest
   where
@@ -119,7 +145,7 @@ groupParams = foldr addParam []
         | incIndices t == s = ParamGroup (x : xs) t : rest
         | otherwise = ParamGroup [x] t : l
 
-printLevel :: Integer -> Doc ann
+printLevel :: (IsString s, Semigroup s, Integral i) => i -> s
 printLevel k
     | k == 0 = "₀"
     | k == 1 = "₁"
@@ -131,7 +157,7 @@ printLevel k
     | k == 7 = "₇"
     | k == 8 = "₈"
     | k == 9 = "₉"
-    | k < 0 = pretty k
+    | k < 0 = printLevel k
     | otherwise = printLevel (k `div` 10) <> printLevel (k `mod` 10)
 
 prettyExpr :: Integer -> Expr -> Doc ann
@@ -149,11 +175,12 @@ prettyExpr k expr = case expr of
       where
         (top :| rest) = NE.reverse $ collectApps expr
         application = group $ hang 4 $ prettyExpr 3 top <> line <> align (sep $ map (prettyExpr 4) rest)
-    Pi "" t1 _ t2
+    Pi "" _ _ _
         | k > 2 -> parens piType
         | otherwise -> piType
       where
-        piType = group $ prettyExpr 3 t1 <+> "->" <+> align (prettyExpr 2 t2)
+        (top :| rest) = collectArrows expr
+        piType = group $ hang 4 $ prettyExpr 3 top <+> align (sep $ map (("->" <+>) . prettyExpr 2) rest)
     Pi{} -> group $ hang 4 $ "∏" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body)
       where
         (params, body) = collectPis expr

lib/Program.hs

@@ -32,7 +32,7 @@ handleDef (Def name (Just irTy) irBody) = do
     ty' <- liftEither $ checkType env body
     _ <- liftEither $ checkType env ty
     liftEither $ checkBeta env ty ty' body
-    modify $ insertDef name ty' body
+    modify $ insertDef name ty body
   where
     body = elaborate irBody
     ty = elaborate irTy