From e232b5181e141a54e28eec669116c35f9673d691 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 16 Apr 2015 14:49:14 +0200 Subject: [PATCH] keep name if we have it when generating a fresh name --- Connections.hs | 7 +++++++ Eval.hs | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) 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) -- 2.34.1