fix: make viewTree* injective

We also add regression tests

primer/src/Primer/API.hs

@@ -79,11 +79,11 @@ import Primer.App (
 import qualified Primer.App as App
 import Primer.Core (
   Expr,
-  Expr' (APP, Ann, Con, LetType, Letrec, Var),
+  Expr' (APP, Ann, GlobalVar, LetType, Letrec),
   ID,
   Kind,
   Type,
-  Type' (TCon, TVar),
+  Type' (TForall),
   defExpr,
   defID,
   defName,
@@ -346,9 +346,8 @@ viewTreeExpr :: Expr -> Tree
 viewTreeExpr = U.para $ \e exprChildren ->
   let c = toS $ showConstr $ toConstr e
       n = case e of
-        Con _ n' -> c <> " " <> unName n'
-        Var _ n' -> c <> " " <> unName n'
-        _ -> c
+        GlobalVar _ i -> c <> " " <> show i
+        _ -> unwords $ c : map unName (U.childrenBi e)
       -- add info about type children
       allChildren = case e of
         Ann _ _ ty -> exprChildren ++ [viewTreeType ty]
@@ -364,9 +363,8 @@ viewTreeType :: Type -> Tree
 viewTreeType = U.para $ \e allChildren ->
   let c = toS $ showConstr $ toConstr e
       n = case e of
-        TCon _ n' -> c <> " " <> unName n'
-        TVar _ n' -> c <> " " <> unName n'
-        _ -> c
+        TForall _ m k _ -> c <> " " <> unName m <> ":" <> show k
+        _ -> unwords $ c : map unName (U.childrenBi e)
    in Tree (getID e) n allChildren
 
 edit :: (MonadIO m, MonadThrow m) => SessionId -> MutationRequest -> PrimerM m (Result ProgError App.Prog)

primer/test/Tests/API.hs

@@ -5,6 +5,10 @@ import Foreword
 import Gen.Core.Raw (evalExprGen, genExpr, genType)
 import Hedgehog
 import Primer.API (viewTreeExpr, viewTreeType)
+import Primer.Core.DSL
+import Test.Tasty.HUnit
+
+import Primer.Core
 
 hprop_viewTreeExpr_injective :: Property
 hprop_viewTreeExpr_injective = property $ do
@@ -19,3 +23,73 @@ hprop_viewTreeType_injective = property $ do
   t2 <- forAll $ evalExprGen 0 genType
   when (t1 == t2) discard
   viewTreeType t1 /== viewTreeType t2
+
+-- regression tests to check we encode names into the tree
+
+unit_viewTreeExpr_injective_con :: Assertion
+unit_viewTreeExpr_injective_con =
+  distinctTreeExpr (con "C") (con "D")
+
+unit_viewTreeExpr_injective_lam :: Assertion
+unit_viewTreeExpr_injective_lam =
+  distinctTreeExpr (lam "x" emptyHole) (lam "y" emptyHole)
+
+unit_viewTreeExpr_injective_LAM :: Assertion
+unit_viewTreeExpr_injective_LAM =
+  distinctTreeExpr (lAM "x" emptyHole) (lAM "y" emptyHole)
+
+unit_viewTreeExpr_injective_var :: Assertion
+unit_viewTreeExpr_injective_var =
+  distinctTreeExpr (var "x") (var "y")
+
+unit_viewTreeExpr_injective_globalvar :: Assertion
+unit_viewTreeExpr_injective_globalvar =
+  distinctTreeExpr (global 0) (global 1)
+
+unit_viewTreeExpr_injective_let :: Assertion
+unit_viewTreeExpr_injective_let =
+  distinctTreeExpr (let_ "x" emptyHole emptyHole) (let_ "y" emptyHole emptyHole)
+
+unit_viewTreeExpr_injective_lettype :: Assertion
+unit_viewTreeExpr_injective_lettype =
+  distinctTreeExpr (letType "x" tEmptyHole emptyHole) (letType "y" tEmptyHole emptyHole)
+
+unit_viewTreeExpr_injective_letrec :: Assertion
+unit_viewTreeExpr_injective_letrec =
+  distinctTreeExpr (letrec "x" emptyHole tEmptyHole emptyHole) (letrec "y" emptyHole tEmptyHole emptyHole)
+
+unit_viewTreeExpr_injective_case_conName :: Assertion
+unit_viewTreeExpr_injective_case_conName =
+  distinctTreeExpr (case_ emptyHole [branch "C" [("x", Nothing)] emptyHole]) (case_ emptyHole [branch "D" [("x", Nothing)] emptyHole])
+
+unit_viewTreeExpr_injective_case_paramName :: Assertion
+unit_viewTreeExpr_injective_case_paramName =
+  distinctTreeExpr (case_ emptyHole [branch "C" [("x", Nothing)] emptyHole]) (case_ emptyHole [branch "C" [("y", Nothing)] emptyHole])
+
+unit_viewTreeType_injective_con :: Assertion
+unit_viewTreeType_injective_con =
+  distinctTreeType (tcon "T") (tcon "S")
+
+unit_viewTreeType_injective_var :: Assertion
+unit_viewTreeType_injective_var =
+  distinctTreeType (tvar "a") (tvar "b")
+
+unit_viewTreeType_injective_forall_param :: Assertion
+unit_viewTreeType_injective_forall_param =
+  distinctTreeType (tforall "a" KType tEmptyHole) (tforall "b" KType tEmptyHole)
+
+unit_viewTreeType_injective_forall_kind :: Assertion
+unit_viewTreeType_injective_forall_kind =
+  distinctTreeType (tforall "a" KType tEmptyHole) (tforall "a" KHole tEmptyHole)
+
+distinctTreeExpr :: S Expr -> S Expr -> Assertion
+distinctTreeExpr e1 e2 =
+  let t1 = viewTreeExpr $ fst $ create e1
+      t2 = viewTreeExpr $ fst $ create e2
+   in assertBool ("non-injective viewTreeExpr: " ++ show t1) (t1 /= t2)
+
+distinctTreeType :: S Type -> S Type -> Assertion
+distinctTreeType e1 e2 =
+  let t1 = viewTreeType $ fst $ create e1
+      t2 = viewTreeType $ fst $ create e2
+   in assertBool ("non-injective viewTreeType: " ++ show t1) (t1 /= t2)