keep name if we have it when generating a fresh name

diff --git a/Connections.hs b/Connections.hs
index da48162e00c54ef78b0c6f4b04e66bbf6c948ee5..8a3d65a85f7c68eaa2037133933c069e432e23be 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -243,6 +243,10 @@ gensym :: [Name] -> Name
 gensym xs = head (ys \\ xs)
   where ys = map Name $ ["i","j","k","l"] ++ map (('i':) . show) [0..]
 
+gensymNice :: Name -> [Name] -> Name
+gensymNice i@(Name s) xs = head (ys \\ xs)
+  where ys = i:map (\n -> Name (s ++ show n)) [0..]
+
 -- gensym :: [Name] -> Name
 -- gensym xs = Name ('?' : show max)
 --   where max = maximum' [ read x | Name ('?':x) <- xs ]
@@ -260,6 +264,9 @@ class Nominal a where
 fresh :: Nominal a => a -> Name
 fresh = gensym . support
 
+freshNice :: Nominal a => Name -> a -> Name
+freshNice i = gensymNice i . support
+
 freshs :: Nominal a => a -> [Name]
 freshs = gensyms . support
 

diff --git a/Eval.hs b/Eval.hs
index 9c8fcfd7080599e3aa8f201f5a28c41f8c1bcda3..c3591e51b6c305cbfe434fc2d4387e6365792fac 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -151,7 +151,7 @@ eval rho v = case v of
   Hole{}              -> Ter v rho
   IdP a e0 e1         -> VIdP (eval rho a) (eval rho e0) (eval rho e1)
   Path i t            ->
-    let j = fresh rho
+    let j = freshNice i rho
     in VPath j (eval (Sub rho (i,Atom j)) t)
   Trans u v        -> transLine (eval rho u) (eval rho v)
   AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi)