Mercurial > urweb

comparison lib/top.ur @ 345:b85e6ba56618

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents 389399d65331
children 383c72d11db8
comparison
equal deleted inserted replaced
344:3c0feecd057d 345:b85e6ba56618
20 20
21 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v) 21 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
22 22
23 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) 23 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
24 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 24 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
25 -> tf t -> tr rest -> tr ([nm = t] ++ rest)) 25 => tf t -> tr rest -> tr ([nm = t] ++ rest))
26 (i : tr []) = 26 (i : tr []) =
27 fold [fn r :: {Type} => $(mapTT tf r) -> tr r] 27 fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
28 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) => 28 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) =>
29 [[nm] ~ rest] => 29 [[nm] ~ rest] =>
30 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm))) 30 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm)))
31 (fn _ => i) 31 (fn _ => i)
32 32
33 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) 33 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
34 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 34 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
35 -> tf t -> tr rest -> tr ([nm = t] ++ rest)) 35 => tf t -> tr rest -> tr ([nm = t] ++ rest))
36 (i : tr []) = 36 (i : tr []) =
37 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] 37 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
38 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) => 38 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) =>
39 [[nm] ~ rest] => 39 [[nm] ~ rest] =>
40 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm))) 40 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm)))
41 (fn _ => i) 41 (fn _ => i)
42 42
43 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) 43 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
44 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 44 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
45 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 45 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
46 (i : tr []) = 46 (i : tr []) =
47 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] 47 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
48 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) => 48 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
49 [[nm] ~ rest] => 49 [[nm] ~ rest] =>
50 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 50 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
51 (fn _ _ => i) 51 (fn _ _ => i)
52 52
53 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) 53 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
54 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 54 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
55 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 55 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
56 (i : tr []) = 56 (i : tr []) =
57 fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] 57 fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
58 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) => 58 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) =>
59 [[nm] ~ rest] => 59 [[nm] ~ rest] =>
60 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 60 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
61 (fn _ _ => i) 61 (fn _ _ => i)
62 62
63 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) 63 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
64 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 64 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
65 -> tf t -> xml ctx [] []) = 65 => tf t -> xml ctx [] []) =
66 foldTR [tf] [fn _ => xml ctx [] []] 66 foldTR [tf] [fn _ => xml ctx [] []]
67 (fn (nm :: Name) (t :: Type) (rest :: {Type}) => 67 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
68 [[nm] ~ rest] => 68 [[nm] ~ rest] =>
69 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>) 69 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>)
70 <xml></xml> 70 <xml></xml>
71 71
72 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) 72 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
73 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 73 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
74 -> tf t -> xml ctx [] []) = 74 => tf t -> xml ctx [] []) =
75 foldT2R [tf] [fn _ => xml ctx [] []] 75 foldT2R [tf] [fn _ => xml ctx [] []]
76 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => 76 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
77 [[nm] ~ rest] => 77 [[nm] ~ rest] =>
78 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>) 78 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>)
79 <xml></xml> 79 <xml></xml>
80 80
81 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) 81 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
82 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 82 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
83 -> tf1 t -> tf2 t -> xml ctx [] []) = 83 => tf1 t -> tf2 t -> xml ctx [] []) =
84 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] 84 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
85 (fn (nm :: Name) (t :: Type) (rest :: {Type}) => 85 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
86 [[nm] ~ rest] => 86 [[nm] ~ rest] =>
87 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 87 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
88 <xml></xml> 88 <xml></xml>
89 89
90 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit}) 90 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit})
91 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 91 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
92 -> tf1 t -> tf2 t -> xml ctx [] []) = 92 => tf1 t -> tf2 t -> xml ctx [] []) =
93 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] 93 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
94 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => 94 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
95 [[nm] ~ rest] => 95 [[nm] ~ rest] =>
96 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 96 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
97 <xml></xml> 97 <xml></xml>