Mercurial > urweb

comparison lib/ur/incl.ur @ 1181:618f9f458da9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
author Adam Chlipala <adamc@hcoop.net>
date Sat, 06 Mar 2010 19:14:48 -0500
parents ac3dbbc85c6e
children 0b1d666bddb4
comparison
equal deleted inserted replaced
1180:ac3dbbc85c6e 1181:618f9f458da9
19 (i : incl ([nm = t] ++ r) r') 19 (i : incl ([nm = t] ++ r) r')
20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = 20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => 21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) 22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))
23 23
24 fun inv2 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] 24 fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
25 (i : incl ([nm = t] ++ r) r') = 25 (i : incl ([nm = t] ++ r) r') =
26 i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => 26 i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
27 fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => 27 fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
28 f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] => 28 f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] =>
29 {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x, 29 {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x,
33 (f : nm :: Name -> v :: K -> r' :: {K} 33 (f : nm :: Name -> v :: K -> r' :: {K}
34 -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r')) 34 -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
35 (i : tf []) (fl : folder r) = 35 (i : tf []) (fl : folder r) =
36 @Top.fold [fn r' => incl r' r -> tf r'] 36 @Top.fold [fn r' => incl r' r -> tf r']
37 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => 37 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
38 f [nm] [v] [r'] ! i (acc (inv2 [nm] [r'] [r] i))) 38 f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i)))
39 (fn _ => i) 39 (fn _ => i)
40 fl (incl [r] [[]]) 40 fl (incl [r] [[]])