0 | module Pipeline.Dependent
  1 |
  2 | import public Data.Telescope.Telescope
  3 | import Data.Vect
  4 |
  5 | import Debug.Trace
  6 |
  7 | export typebind infixr 0 .-
  8 | %hide Data.Telescope.Telescope.infixr.(.-)
  9 | private autobind infixr 0 ^^
 10 | export autobind infixr 0 |>>>
 11 |
 12 | public export
 13 | head : Right.Telescope (S n) -> Type
 14 | head (x .- _) = x
 15 |
 16 | FSuc : (xs : Right.Telescope (S n)) -> {0 ty : Type} -> {0 tel : ty -> Right.Telescope n} ->
 17 |        xs === ((t : ty) .- tel t) -> head xs === ty
 18 | FSuc _ Refl = Refl
 19 |
 20 | public export
 21 | tail : (xs : Right.Telescope (S n)) -> head xs -> Right.Telescope n
 22 | tail (ty .- gamma) x = gamma x
 23 |
 24 | 0 tailSuc : (xs : Right.Telescope (S n)) -> {ty : Type} -> {tel : ty -> Right.Telescope n} ->
 25 |   (p : xs === ((t : ty) .- tel t)) -> (v : ty) -> tail xs (rewrite__impl Basics.id (FSuc xs p) v) === tel v
 26 | tailSuc _ Refl v = Refl
 27 |
 28 | EnvZero : (xs : Right.Telescope 0) -> Right.Environment xs === Unit
 29 | EnvZero [] = Refl
 30 |
 31 | public export
 32 | record DContPair' (x, y : Type) (f : y -> Type)  where
 33 |   constructor (|>>>)
 34 |   fst : x
 35 |   cont : (v : y) -> f v
 36 |
 37 | public export
 38 | DContPair : (x : Type) -> (y : x -> Type) -> Type
 39 | DContPair x = DContPair' x x
 40 |
 41 | appDCont : (p : DContPair a b) -> b p.fst
 42 | appDCont ((|>>>) v c) = c v
 43 |
 44 | public export
 45 | DContPairM : (m : Type -> Type) -> (x : Type) -> (y : x -> Type) -> Type
 46 | DContPairM m x f = DContPair' (m x) x f
 47 |
 48 | appDContM : Monad m => (p : DContPairM m x y) -> m (vx : x ** y vx)
 49 | appDContM (f |>>> c) = f >>= \vx => pure (vx ** c vx)
 50 |
 51 | public export
 52 | HasShow : (Right.Telescope xs) -> Type
 53 | HasShow [] = Unit
 54 | HasShow (ty .- gamma) = (Show ty, (x : ty) -> HasShow (gamma x))
 55 |
 56 | public export
 57 | ToSigma : Right.Telescope n -> Type
 58 | ToSigma [] = Unit
 59 | ToSigma (ty .- gamma)
 60 |     = DContPair ty (ToSigma . gamma)
 61 |
 62 | public export
 63 | ToImpl : Right.Telescope n -> Type
 64 | ToImpl [] = Void
 65 | ToImpl (ty .- gamma) = (x : ty) -> ToSigma (gamma x)
 66 |
 67 | ||| How to run the implementation of a telescope and obtain a
 68 | ||| sigma-types with all the intermediate results
 69 | export
 70 | RunDep : {n : _} -> (xs : Right.Telescope (S (S n)) ) ->
 71 |          (imp : ToImpl xs) -> (val : head xs) -> Environment (tail xs val)
 72 | RunDep {n = 0} (ty .- gamma) imp val with (imp val)
 73 |   RunDep {n = 0} (ty .- gamma) imp val | res with (gamma val)
 74 |     RunDep {n = 0} (ty .- gamma) imp val | (vv |>>> cont) | (x .- f) =
 75 |       (vv ** (rewrite EnvZero (f vv) in ()))
 76 | RunDep {n = S n} (ty .- gamma) imp val with (imp val)
 77 |   RunDep (ty .- gamma) imp val | res with (gamma val) proof q
 78 |     RunDep (ty .- gamma) imp val | (vx |>>> cont) | (ty' .- tel) =
 79 |       let rr = cont vx
 80 |           rx = RunDep (gamma val) (rewrite q in cont) (rewrite q in vx)
 81 |           gn' = replace {p = Environment} (tailSuc _ q vx) rx
 82 |       in (vx ** gn')
 83 |
 84 | ||| How to run the implementation of a telescope and obtain a
 85 | ||| sigma-types with all the intermediate results
 86 | export
 87 | RunTraceDep : {n : _} -> (xs : Right.Telescope (S (S n)) ) -> (s : HasShow xs) =>
 88 |          (imp : ToImpl xs) -> (val : head xs) -> Environment (tail xs val)
 89 | RunTraceDep {s = (s, ss)} {n = 0} (ty .- gamma) imp val with (imp val)
 90 |   RunTraceDep {s = (s, ss)} {n = 0} (ty .- gamma) imp val | res with (gamma val) proof q
 91 |     RunTraceDep {s = (s, ss)} {n = 0} (ty .- gamma) imp val | (vv |>>> cont) | (x .- f) =
 92 |       let gg = replace {p = HasShow} q (ss val)
 93 |       in (vv ** (rewrite EnvZero (f vv) in trace (show vv) ()))
 94 | RunTraceDep {s = (s, ss)} {n = S n} (ty .- gamma) imp val with (imp val)
 95 |   RunTraceDep  (ty .- gamma) imp val | res with (gamma val) proof q
 96 |     RunTraceDep (ty .- gamma) imp val | (vx |>>> cont) | (ty' .- tel) =
 97 |       let pp = replace {p = HasShow} q (ss val)
 98 |           rr = cont (traceValBy show vx)
 99 |           rx = RunTraceDep (gamma val) (rewrite q in cont) (rewrite q in vx) {s = ss val}
100 |           gn' = replace {p = Environment} (tailSuc _ q vx) rx
101 |       in (vx ** gn')
102 |
103 | parameters (m : Type -> Type) {auto inst : Monad m}
104 |
105 |   public export
106 |   ToSigmaM : Right.Telescope n -> Type
107 |   ToSigmaM [] = Unit
108 |   ToSigmaM (ty .- gamma)
109 |       = DContPairM m ty (ToSigmaM . gamma)
110 |
111 |   public export
112 |   ToImplM : Right.Telescope n -> Type
113 |   ToImplM [] = Void
114 |   ToImplM (ty .- gamma) = (x : ty) -> ToSigmaM (gamma x)
115 |
116 |   ||| How to run the implementation of a telescope and obtain a
117 |   ||| sigma-types with all the intermediate results
118 |   export
119 |   RunDepM : {n : _} -> (xs : Right.Telescope (S (S n)) ) ->
120 |            (imp : ToImplM xs) -> (val : head xs) -> m (Environment (tail xs val))
121 |   RunDepM {n = 0} (ty .- gamma) imp val with (imp val)
122 |     RunDepM {n = 0} (ty .- gamma) imp val | res with (gamma val)
123 |       RunDepM {n = 0} (ty .- gamma) imp val | (fst |>>> cont) | (x .- f) = do
124 |         vx <- fst
125 |         pure (vx ** (rewrite EnvZero (f vx) in ()))
126 |   RunDepM {n = S n} (ty .- gamma) imp val with (imp val)
127 |     RunDepM (ty .- gamma) imp val | res with (gamma val) proof q
128 |       RunDepM (ty .- gamma) imp val | (vx |>>> cont) | (ty' .- tel) = do
129 |         vy <- vx
130 |         gn <- RunDepM (gamma val) (rewrite q in cont) (rewrite q in vy)
131 |         let gn' = replace {p = Environment} (tailSuc _ q vy) gn
132 |         pure (vy ** gn')
133 |
134 |   export
135 |   RunTraceDepM : {n : _} -> (xs : Right.Telescope (S (S n)) ) -> (s : HasShow xs) =>
136 |              (imp : ToImplM xs) -> (val : head xs) -> m (Environment (tail xs val))
137 |   RunTraceDepM {n = 0} {s} (ty .- gamma) imp val with (imp val)
138 |     RunTraceDepM {n = 0} {s} (ty .- gamma) imp val | res with (gamma val) proof p
139 |       RunTraceDepM {n = 0} {s = (s, ss)} (ty .- gamma) imp val | (fst |>>> cont) | (x .- f) = do
140 |         vx <- fst
141 |         let (sx, sn') = replace {p = HasShow} p (ss val)
142 |         trace (show vx) (pure ())
143 |         pure (vx ** (rewrite EnvZero (f vx) in ()))
144 |   RunTraceDepM {n = S n} {s} (ty .- gamma) imp val with (imp val)
145 |     RunTraceDepM {s} (ty .- gamma) imp val | res with (gamma val) proof q
146 |       RunTraceDepM {s = (s, ss)} (ty .- gamma) imp val | (vx |>>> cont) | (ty' .- tel) = do
147 |         vy <- vx
148 |         trace (show val) (pure ())
149 |         gn <- RunTraceDepM {s = ss val} (gamma val) (rewrite q in cont) (rewrite q in vy)
150 |         let gn' = replace {p = Environment} (tailSuc _ q vy) gn
151 |         pure (vy ** gn')
152 |
153 |
154 |
155 |