Mercurial > urweb

annotate lib/ur/mem.ur @ 1182:0b1d666bddb4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spiffed-up Split1; remove spurious error message triggered by 'open'ing a module containing a functor
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Mar 2010 17:50:42 -0500
parents ac3dbbc85c6e
children
rev   line source
adamc@1180 1 con mem' = K ==> fn (nm :: Name) (t :: K) (r :: {K}) (r' :: {K}) =>
adamc@1180 2 [[nm] ~ r'] => {Expose : f :: ({K} -> Type) -> f r -> f ([nm = t] ++ r'),
adamc@1180 3 Hide : f :: ({K} -> Type) -> f ([nm = t] ++ r') -> f r}
adamc@1180 4
adamc@1180 5 con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) =>
adamc@1180 6 tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp
adamc@1180 7
adamc@1180 8 fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] =
adamc@1180 9 fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) =>
adamc@1180 10 f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x,
adamc@1180 11 Hide = fn [f :: {K} -> Type] x => x})
adamc@1180 12
adamc@1180 13 fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) =
adamc@1180 14 m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') =>
adamc@1180 15 fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] =>
adamc@1180 16 mem' nm (f t) (map f r) r' -> tp) =>
adamc@1180 17 f [map f r'] ! (fn [[nm] ~ map f r'] =>
adamc@1180 18 {Expose = fn [f' :: {K2} -> Type] x =>
adamc@1180 19 m'.Expose [fn r => f' (map f r)] x,
adamc@1180 20 Hide = fn [f' :: {K2} -> Type] x =>
adamc@1180 21 m'.Hide [fn r => f' (map f r)] x}))
adamc@1180 22
adamc@1180 23 fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) =
adamc@1180 24 m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
adamc@1180 25 (m'.Expose [fn r => $r] r).nm)
adamc@1180 26
adamc@1180 27 fun replace [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) (v : t) =
adamc@1180 28 m [$r] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
adamc@1180 29 m'.Hide [fn r => $r] (m'.Expose [fn r => $r] r -- nm ++ {nm = v}))
adamc@1180 30
adamc@1180 31 fun fold [K] [tf :: ({K} -> Type)] [r ::: {K}]
adamc@1180 32 (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
adamc@1180 33 => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
adamc@1180 34 (i : tf []) (fl : folder r) =
adamc@1180 35 @@Incl.fold [tf] [r]
adamc@1180 36 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc =>
adamc@1182 37 f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc)
adamc@1180 38 i fl