diff options
author | 2010-03-06 16:15:26 -0500 | |
---|---|---|
committer | 2010-03-06 16:15:26 -0500 | |
commit | 049d85f6ec161c8df0461550549ded12be9e44e8 (patch) | |
tree | b422a4c17510b07702c1e16492d87680928a517f /lib/ur/mem.ur | |
parent | e59684b553e4e30e7290c7a589cdb582e8f46907 (diff) |
Standard library moduls Incl and Mem; tweaks to Especialize and Unpoly
Diffstat (limited to 'lib/ur/mem.ur')
-rw-r--r-- | lib/ur/mem.ur | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/lib/ur/mem.ur b/lib/ur/mem.ur new file mode 100644 index 00000000..7f66b3c2 --- /dev/null +++ b/lib/ur/mem.ur @@ -0,0 +1,38 @@ +con mem' = K ==> fn (nm :: Name) (t :: K) (r :: {K}) (r' :: {K}) => + [[nm] ~ r'] => {Expose : f :: ({K} -> Type) -> f r -> f ([nm = t] ++ r'), + Hide : f :: ({K} -> Type) -> f ([nm = t] ++ r') -> f r} + +con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) => + tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp + +fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] = + fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) => + f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, + Hide = fn [f :: {K} -> Type] x => x}) + +fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) = + m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') => + fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] => + mem' nm (f t) (map f r) r' -> tp) => + f [map f r'] ! (fn [[nm] ~ map f r'] => + {Expose = fn [f' :: {K2} -> Type] x => + m'.Expose [fn r => f' (map f r)] x, + Hide = fn [f' :: {K2} -> Type] x => + m'.Hide [fn r => f' (map f r)] x})) + +fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) = + m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => + (m'.Expose [fn r => $r] r).nm) + +fun replace [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) (v : t) = + m [$r] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => + m'.Hide [fn r => $r] (m'.Expose [fn r => $r] r -- nm ++ {nm = v})) + +fun fold [K] [tf :: ({K} -> Type)] [r ::: {K}] + (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r'] + => mem nm v r -> tf r' -> tf ([nm = v] ++ r')) + (i : tf []) (fl : folder r) = + @@Incl.fold [tf] [r] + (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => + f [nm] [v] [r'] ! (Incl.inv1 [nm] [r'] [r] [mem] i mem) acc) + i fl |