Use old gensym and fresh again

diff --git a/Connections.hs b/Connections.hs
index ba1234a4fd2250e4e44b9a9aa328e387703fcd84..e43076fff466a59b3745e7aaeb8bb4f8a6ef32f4 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -239,19 +239,19 @@ propInvFormulaIncomp phi b = incomparables (invFormula phi b)
 -- testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1
 
 -- | Nominal
-gensym :: [Name] -> Name
-gensym xs = head (ys \\ xs)
-  where ys = map Name $ ["i","j","k","l"] ++ map (('i':) . show) [0..]
+-- 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..]
+-- 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 ]
---         maximum' [] = 0
---         maximum' xs = maximum xs + 1
+gensym :: [Name] -> Name
+gensym xs = Name ('?' : show max)
+  where max = maximum' [ read x | Name ('?':x) <- xs ]
+        maximum' [] = 0
+        maximum' xs = maximum xs + 1
 
 gensyms :: [Name] -> [Name]
 gensyms d = let x = gensym d in x : gensyms (x : d)
@@ -264,8 +264,8 @@ class Nominal a where
 fresh :: Nominal a => a -> Name
 fresh = gensym . support
 
-freshNice :: Nominal a => Name -> a -> Name
-freshNice i = gensymNice i . 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 0f7bbdc98100c8e769bebdc75fefeae6d91ed48d..5caceb1db34453cbc411cb478ca095d8d280a0b5 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -154,7 +154,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 = freshNice i rho
+    let j = fresh 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)