From 6f22b8b971cf196d425d5dad67cdf4da9d8f41b5 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 6 Mar 2010 16:15:26 -0500
Subject: Standard library moduls Incl and Mem; tweaks to Especialize and
 Unpoly

---
 lib/ur/mem.ur | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 lib/ur/mem.ur

(limited to 'lib/ur/mem.ur')

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
-- 
cgit v1.2.3