Mercurial > meta

comparison variant.ur @ 14:744bf911dcc6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update to expect implicit argument insertion for local variables
author Adam Chlipala <adam@chlipala.net>
date Tue, 14 Jun 2011 08:55:15 -0400
parents 799f43bce62b
children 296807a9fd50
comparison
equal deleted inserted replaced
13:d05943db55e8 14:744bf911dcc6
1 fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t = 1 fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t =
2 match v 2 match v
3 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)] 3 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)]
4 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r => 4 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r =>
5 {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] ! r) 5 {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r)
6 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) 6 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
7 7
8 fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) = 8 fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) =
9 match v 9 match v
10 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)] 10 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)]
11 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] 11 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us]
12 (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us)) 12 (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us))
13 [r'::_] [[nm = u] ++ us ~ r'] r => 13 [r'::_] [[nm = u] ++ us ~ r'] r =>
14 {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] ! r) 14 {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r)
15 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) 15 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
16 16
17 fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t = 17 fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t =
18 @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t] 18 @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t]
19 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] 19 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
20 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t) 20 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t)
21 [r' ::_] [[nm] ++ r ~ r'] f' => 21 [r' ::_] [[nm] ++ r ~ r'] f' =>
22 case f' (make [nm] {}) of 22 case f' (make [nm] {}) of
23 None => acc [[nm] ++ r'] ! f' 23 None => acc [[nm] ++ r'] f'
24 | v => v) 24 | v => v)
25 (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f 25 (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f
26 26
27 fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) = 27 fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) =
28 @search (fn v => if f v then Some v else None) fl 28 @search (fn v => if f v then Some v else None) fl
41 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)] 41 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
42 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] 42 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r]
43 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) 43 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r))
44 [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v => 44 [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v =>
45 {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)} 45 {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)}
46 ++ acc [[nm] ++ r'] ! fl' v) 46 ++ @acc [[nm] ++ r'] ! fl' v)
47 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2) 47 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2)
48 48
49 fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t = 49 fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t =
50 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t] 50 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t]
51 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] 51 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) 52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
53 [r' ::_] [[nm] ++ r ~ r'] f' acc' => 53 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
54 f' (make [nm] {}) (acc [[nm] ++ r'] ! f' acc')) 54 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f 55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
56 56
57 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] 57 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
58 (f : p :: K -> f p -> fr p -> t) 58 (f : p :: K -> f p -> fr p -> t)
59 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = 59 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
79 (fl : folder ([nm = p] ++ r ++ others)) 79 (fl : folder ([nm = p] ++ r ++ others))
80 (v2 : variant (map f2 ([nm = p] ++ r ++ others))) => 80 (v2 : variant (map f2 ([nm = p] ++ r ++ others))) =>
81 {nm = fn x1 => match v2 81 {nm = fn x1 => match v2
82 ({nm = fn x2 => Some (f [p] x1 x2 meta)} 82 ({nm = fn x2 => Some (f [p] x1 x2 meta)}
83 ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))} 83 ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))}
84 ++ acc [[nm = p] ++ others] ! fl v2) 84 ++ @acc [[nm = p] ++ others] ! fl v2)
85 (fn [others ::_] [others ~ []] _ _ => {}) 85 (fn [others ::_] [others ~ []] _ _ => {})
86 fl r [[]] ! fl v2) 86 fl r [[]] ! fl v2)
87 87
88 fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] 88 fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
89 (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) = 89 (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) =