adam@6: fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t = adam@6: match v adam@6: (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)] adam@6: (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r => adam@14: {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r) adam@6: (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) adam@6: adam@6: fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) = adam@6: match v adam@6: (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)] adam@6: (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] adam@6: (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us)) adam@6: [r'::_] [[nm = u] ++ us ~ r'] r => adam@14: {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r) adam@6: (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) adam@6: adam@6: fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t = adam@6: @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t] adam@6: (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] adam@6: (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t) adam@6: [r' ::_] [[nm] ++ r ~ r'] f' => adam@6: case f' (make [nm] {}) of adam@14: None => acc [[nm] ++ r'] f' adam@6: | v => v) adam@6: (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f adam@6: adam@6: fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) = adam@6: @search (fn v => if f v then Some v else None) fl adam@6: adam@6: fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts)) adam@6: (v : variant ([nm = t] ++ ts)) : option t = adam@6: match v ({nm = Some} adam@6: ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm)) adam@6: adam@6: fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t = adam@6: match v ({nm = Some} adam@6: ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl) adam@6: adam@21: fun weaken [r1 ::: {Type}] [r2 ::: {Type}] [r1 ~ r2] (fl : folder r1) (v : variant r1) : variant (r1 ++ r2) = adam@21: match v adam@21: (@fold [fn r => r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)] adam@21: (fn [nm :: Name] [t ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)) [r'::_] [[nm = t] ++ r ~ r'] => adam@21: {nm = make [nm]} ++ acc [[nm = t] ++ r']) adam@21: (fn [r'::_] [[] ~ r'] => {}) fl [r2] !) adam@21: adam@6: fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool = adam@6: match v1 adam@6: (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)] adam@6: (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] adam@6: (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) adam@6: [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v => adam@6: {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)} adam@14: ++ @acc [[nm] ++ r'] ! fl' v) adam@6: (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2) adam@6: adam@6: fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t = adam@6: @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t] adam@6: (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] adam@6: (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) adam@6: [r' ::_] [[nm] ++ r ~ r'] f' acc' => adam@14: f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) adam@6: (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f adam@6: adam@21: fun mp [r ::: {Unit}] [t ::: Type] (fl : folder r) (f : variant (mapU {} r) -> t) : $(mapU t r) = adam@21: @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)] adam@21: (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] adam@21: (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)) adam@21: [r' ::_] [[nm] ++ r ~ r'] f' => adam@21: {nm = f' (make [nm] {})} ++ acc [[nm] ++ r'] f') adam@21: (fn [r' ::_] [[] ~ r'] _ => {}) fl [[]] ! f adam@21: adam@20: fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t = adam@20: @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t] adam@20: (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr) adam@20: (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t) adam@20: [r' ::_] [[nm] ++ r ~ r'] f' acc' => adam@20: f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc')) adam@20: (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f adam@20: adam@20: fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} = adam@20: @foldR fl (fn var this acc => f var this; acc) record (return ()) adam@20: adam@21: fun mapR [tr] [t] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> t) (record : $(mapU tr r)) : $(mapU t r) = adam@21: @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)] adam@21: (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] adam@21: (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)) adam@21: [r' ::_] [[nm] ++ r ~ r'] f' vs => adam@21: {nm = f' (make [nm] {}) vs.nm} ++ acc [[nm] ++ r'] f' (vs -- nm)) adam@21: (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! f record adam@21: adam@6: fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] adam@6: (f : p :: K -> f p -> fr p -> t) adam@6: [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = adam@6: match v adam@6: (@Top.mp [fr] [fn p => f p -> t] adam@6: (fn [p] (m : fr p) (v : f p) => f [p] v m) adam@6: fl r) adam@6: adam@6: fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type] adam@6: (f : p :: K -> f1 p -> f2 p -> fr p -> t) adam@6: [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t = adam@6: match v1 adam@20: (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] => adam@6: folder (r ++ others) adam@6: -> variant (map f2 (r ++ others)) adam@6: -> $(map (fn p => f1 p -> option t) r)] adam@6: (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p) adam@6: (acc : others :: {K} -> [others ~ r] => adam@6: folder (r ++ others) adam@6: -> variant (map f2 (r ++ others)) adam@6: -> $(map (fn p => f1 p -> option t) r)) adam@6: [others :: {K}] [others ~ [nm = p] ++ r] adam@6: (fl : folder ([nm = p] ++ r ++ others)) adam@6: (v2 : variant (map f2 ([nm = p] ++ r ++ others))) => adam@6: {nm = fn x1 => match v2 adam@6: ({nm = fn x2 => Some (f [p] x1 x2 meta)} adam@6: ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))} adam@14: ++ @acc [[nm = p] ++ others] ! fl v2) adam@6: (fn [others ::_] [others ~ []] _ _ => {}) adam@6: fl r [[]] ! fl v2) adam@6: adam@6: fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] adam@6: (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) = adam@6: @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl)) adam@6: (Eq.cast pf [fn r => variant (map f r)] v) adam@6: adam@6: fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] adam@6: (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) = adam@6: Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x) ezyang@27: ezyang@27: con variantMake ts' ts = $(map (fn t => t -> variant ts') ts) ezyang@27: con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r ezyang@27: fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts ezyang@27: = @Top.fold [mkLabelsAccum] ezyang@27: (fn [nm::_] [v::_] [r::_] [[nm] ~ r] ezyang@27: (k : mkLabelsAccum r) ezyang@27: [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]}) ezyang@27: (fn [s::_] [[] ~ s] => {}) fl [[]] ! ezyang@27: adam@29: con type_case ts t a = (a -> variant ts) -> a -> t ezyang@27: ezyang@27: fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f ezyang@27: fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t ezyang@27: (* Ur/Web not clever enough to calculate these folders, it seems *) ezyang@28: = match v (@Record.ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl))