summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/ur/incl.ur40
-rw-r--r--lib/ur/incl.urs20
-rw-r--r--lib/ur/mem.ur38
-rw-r--r--lib/ur/mem.urs13
4 files changed, 0 insertions, 111 deletions
diff --git a/lib/ur/incl.ur b/lib/ur/incl.ur
deleted file mode 100644
index 4ed27391..00000000
--- a/lib/ur/incl.ur
+++ /dev/null
@@ -1,40 +0,0 @@
-con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) =>
- [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'),
- Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2}
-
-con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) =>
- tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp
-
-fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] =
- fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) =>
- f [r2] ! (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x,
- Hide = fn [f :: ({K} -> Type)] x => x})
-
-fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) =
- i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') =>
- i'.Expose [fn r => $r] r --- r')
-
-fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
- [f :: Name -> K -> {K} -> Type]
- (i : incl ([nm = t] ++ r) r')
- (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
- i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
- i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))
-
-fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
- (i : incl ([nm = t] ++ r) r') =
- i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
- fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
- f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] =>
- {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x,
- Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x}))
-
-fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
- (f : nm :: Name -> v :: K -> r' :: {K}
- -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
- (i : tf []) (fl : folder r) =
- @Top.fold [fn r' => incl r' r -> tf r']
- (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
- f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i)))
- (fn _ => i)
- fl (incl [r] [[]])
diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs
deleted file mode 100644
index 24db0a8a..00000000
--- a/lib/ur/incl.urs
+++ /dev/null
@@ -1,20 +0,0 @@
-con incl :: K --> {K} -> {K} -> Type
-
-val incl : K --> r1 :: {K} -> r2 :: {K} -> [r1 ~ r2] => incl r1 (r1 ++ r2)
-val proj : r1 ::: {Type} -> r2 ::: {Type} -> incl r1 r2 -> $r2 -> $r1
-
-val inv1 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K}
- -> [[nm] ~ r] =>
- f :: (Name -> K -> {K} -> Type)
- -> incl ([nm = t] ++ r) r'
- -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r))
- -> f nm t r'
-val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K}
- -> [[nm] ~ r] =>
- incl ([nm = t] ++ r) r' -> incl r r'
-
-val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
- -> (nm :: Name -> v :: K -> r' :: {K}
- -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
- -> tf []
- -> folder r -> tf r
diff --git a/lib/ur/mem.ur b/lib/ur/mem.ur
deleted file mode 100644
index 85ccf988..00000000
--- a/lib/ur/mem.ur
+++ /dev/null
@@ -1,38 +0,0 @@
-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] [v] [r'] [r] [mem] i mem) acc)
- i fl
diff --git a/lib/ur/mem.urs b/lib/ur/mem.urs
deleted file mode 100644
index 78021823..00000000
--- a/lib/ur/mem.urs
+++ /dev/null
@@ -1,13 +0,0 @@
-con mem :: K --> Name -> K -> {K} -> Type
-
-val mem : K --> nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => mem nm t ([nm = t] ++ r)
-val mp : K --> K2 --> f :: (K -> K2) -> nm ::: Name -> t ::: K -> r ::: {K} -> mem nm t r -> mem nm (f t) (map f r)
-
-val proj : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t
-val replace : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t -> $r
-
-val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
- -> (nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
- => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
- -> tf []
- -> folder r -> tf r