Mercurial > meta
view variant.ur @ 9:8eaaca74a64c
Import HTML parser
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 15 Dec 2010 09:27:46 -0500 |
parents | 799f43bce62b |
children | 744bf911dcc6 |
line wrap: on
line source
fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t = match v (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)] (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r => {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] ! r) (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) = match v (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)] (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us)) [r'::_] [[nm = u] ++ us ~ r'] r => {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] ! r) (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t = @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t] (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t) [r' ::_] [[nm] ++ r ~ r'] f' => case f' (make [nm] {}) of None => acc [[nm] ++ r'] ! f' | v => v) (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) = @search (fn v => if f v then Some v else None) fl fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts)) (v : variant ([nm = t] ++ ts)) : option t = match v ({nm = Some} ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm)) fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t = match v ({nm = Some} ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl) fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool = match v1 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)] (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v => {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)} ++ acc [[nm] ++ r'] ! fl' v) (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2) fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t = @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t] (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) [r' ::_] [[nm] ++ r ~ r'] f' acc' => f' (make [nm] {}) (acc [[nm] ++ r'] ! f' acc')) (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] (f : p :: K -> f p -> fr p -> t) [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = match v (@Top.mp [fr] [fn p => f p -> t] (fn [p] (m : fr p) (v : f p) => f [p] v m) fl r) fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type] (f : p :: K -> f1 p -> f2 p -> fr p -> t) [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t = match v1 (@foldR [fr] [fn r => others :: {K} -> [others ~ r] => folder (r ++ others) -> variant (map f2 (r ++ others)) -> $(map (fn p => f1 p -> option t) r)] (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p) (acc : others :: {K} -> [others ~ r] => folder (r ++ others) -> variant (map f2 (r ++ others)) -> $(map (fn p => f1 p -> option t) r)) [others :: {K}] [others ~ [nm = p] ++ r] (fl : folder ([nm = p] ++ r ++ others)) (v2 : variant (map f2 ([nm = p] ++ r ++ others))) => {nm = fn x1 => match v2 ({nm = fn x2 => Some (f [p] x1 x2 meta)} ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))} ++ acc [[nm = p] ++ others] ! fl v2) (fn [others ::_] [others ~ []] _ _ => {}) fl r [[]] ! fl v2) fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) = @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl)) (Eq.cast pf [fn r => variant (map f r)] v) fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) = Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)