summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-03-06 19:14:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-03-06 19:14:48 -0500
commitdf76c398867ef66c583e5d481bdb33e046acfc09 (patch)
treebc477781e8f3c91a920b10819bf743d10968ca88 /lib/ur
parent6f22b8b971cf196d425d5dad67cdf4da9d8f41b5 (diff)
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/incl.ur4
-rw-r--r--lib/ur/incl.urs2
2 files changed, 3 insertions, 3 deletions
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'