Mercurial > urweb

annotate lib/ur/incl.ur @ 1249:7c6fc92f6c31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 11:47:24 -0400
parents 0b1d666bddb4
children
rev   line source
adamc@1180 1 con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) =>
adamc@1180 2 [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'),
adamc@1180 3 Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2}
adamc@1180 4
adamc@1180 5 con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) =>
adamc@1180 6 tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp
adamc@1180 7
adamc@1180 8 fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] =
adamc@1180 9 fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) =>
adamc@1180 10 f [r2] ! (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x,
adamc@1180 11 Hide = fn [f :: ({K} -> Type)] x => x})
adamc@1180 12
adamc@1180 13 fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) =
adamc@1180 14 i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') =>
adamc@1180 15 i'.Expose [fn r => $r] r --- r')
adamc@1180 16
adamc@1182 17 fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
adamc@1180 18 [f :: Name -> K -> {K} -> Type]
adamc@1180 19 (i : incl ([nm = t] ++ r) r')
adamc@1180 20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
adamc@1180 21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
adamc@1180 22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))
adamc@1180 23
adamc@1181 24 fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
adamc@1180 25 (i : incl ([nm = t] ++ r) r') =
adamc@1180 26 i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
adamc@1180 27 fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
adamc@1180 28 f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] =>
adamc@1180 29 {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x,
adamc@1180 30 Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x}))
adamc@1180 31
adamc@1180 32 fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
adamc@1180 33 (f : nm :: Name -> v :: K -> r' :: {K}
adamc@1180 34 -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
adamc@1180 35 (i : tf []) (fl : folder r) =
adamc@1180 36 @Top.fold [fn r' => incl r' r -> tf r']
adamc@1180 37 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
adamc@1181 38 f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i)))
adamc@1180 39 (fn _ => i)
adamc@1180 40 fl (incl [r] [[]])