From: Simon Huber <hubsim@gmail.com>
Date: Thu, 16 Apr 2015 12:49:14 +0000 (+0200)
Subject: keep name if we have it when generating a fresh name
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e232b5181e141a54e28eec669116c35f9673d691;p=cubicaltt.git

keep name if we have it when generating a fresh name
---

diff --git a/Connections.hs b/Connections.hs
index da48162..8a3d65a 100644
--- 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 9c8fcfd..c3591e5 100644
--- 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)