From df76c398867ef66c583e5d481bdb33e046acfc09 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 6 Mar 2010 19:14:48 -0500 Subject: Got split1 working, but noticed a nasty type inference bug with transplanted unification variables --- lib/ur/incl.ur | 4 ++-- lib/ur/incl.urs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/ur/incl.ur b/lib/ur/incl.ur index d0f4b521..ebf7acef 100644 --- a/lib/ur/incl.ur +++ b/lib/ur/incl.ur @@ -21,7 +21,7 @@ fun inv1 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) -fun inv2 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] +fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] (i : incl ([nm = t] ++ r) r') = i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => @@ -35,6 +35,6 @@ fun fold [K] [tf :: {K} -> Type] [r ::: {K}] (i : tf []) (fl : folder r) = @Top.fold [fn r' => incl r' r -> tf r'] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => - f [nm] [v] [r'] ! i (acc (inv2 [nm] [r'] [r] i))) + f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i))) (fn _ => i) fl (incl [r] [[]]) diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs index d0d78b36..2c77369f 100644 --- a/lib/ur/incl.urs +++ b/lib/ur/incl.urs @@ -9,7 +9,7 @@ val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} -> incl ([nm = t] ++ r) r' -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) -> f nm t r' -val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} +val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K} -> [[nm] ~ r] => incl ([nm = t] ++ r) r' -> incl r r' -- cgit v1.2.3