From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 07:45:17 +0000 (+0200)
Subject: Use old gensym and fresh again
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=dfb412aef298a43b519585a52c9b215c6f5fad0f;p=cubicaltt.git

Use old gensym and fresh again
---

diff --git a/Connections.hs b/Connections.hs
index ba1234a..e43076f 100644
--- 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 0f7bbdc..5caceb1 100644
--- 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)