-
Notifications
You must be signed in to change notification settings - Fork 8
/
bwtface.ml
119 lines (106 loc) · 4.14 KB
/
bwtface.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
open Sface
open Bwsface
open Tface
(* Backwards tube faces *)
type (_, _, _, _) bwtface =
| LEnd : 'l Endpoints.t * ('m, 'n, 'k, 'nk) bwtface -> ('m, 'n D.suc, 'k, 'nk D.suc) bwtface
| LMid : ('m, 'n, 'k, 'nk) bwtface -> ('m D.suc, 'n D.suc, 'k, 'nk D.suc) bwtface
| REnd : 'l Endpoints.t * ('m, 'k) bwsface -> ('m, D.zero, 'k D.suc, 'k D.suc) bwtface
| RMid : ('m, D.zero, 'k, 'k) bwtface -> ('m D.suc, D.zero, 'k D.suc, 'k D.suc) bwtface
let rec dom_bwtface : type m n k nk. (m, n, k, nk) bwtface -> m D.t = function
| LEnd (_, d) -> dom_bwtface d
| LMid d -> D.suc (dom_bwtface d)
| REnd (_, d) -> dom_bwsface d
| RMid d -> D.suc (dom_bwtface d)
let rec codl_bwtface : type m n k nk. (m, n, k, nk) bwtface -> n D.t = function
| LEnd (_, d) -> D.suc (codl_bwtface d)
| LMid d -> D.suc (codl_bwtface d)
| REnd (_, _) -> D.zero
| RMid _ -> D.zero
(*
let rec codr_bwtface : type m n k nk. (m, n, k, nk) bwtface -> k D.t = function
| LEnd (_, d) -> codr_bwtface d
| LMid d -> codr_bwtface d
| REnd (_, d) -> D.suc (cod_bwsface d)
| RMid d -> D.suc (codr_bwtface d)
*)
let rec cod_bwtface : type m n k nk. (m, n, k, nk) bwtface -> nk D.t = function
| LEnd (_, d) -> D.suc (cod_bwtface d)
| LMid d -> D.suc (cod_bwtface d)
| REnd (_, d) -> D.suc (cod_bwsface d)
| RMid d -> D.suc (cod_bwtface d)
let rec bwsface_of_bwtface : type m n k nk. (m, n, k, nk) bwtface -> (m, nk) bwsface = function
| LEnd (e, d) -> End (e, bwsface_of_bwtface d)
| LMid d -> Mid (bwsface_of_bwtface d)
| REnd (e, d) -> End (e, d)
| RMid d -> Mid (bwsface_of_bwtface d)
let bwtface_rend :
type l m k. l Endpoints.t -> (m, D.zero, k, k) bwtface -> (m, D.zero, k D.suc, k D.suc) bwtface
=
fun e d -> REnd (e, bwsface_of_bwtface d)
(* Converting a backwards tube face to a forwards one. This requires three helper functions. *)
let rec tface_of_bw_r :
type m1 m2 m n k1 k2 k nk1 nk.
(m1, m2, m) D.plus ->
(k1, k2, k) D.plus ->
(nk1, k2, nk) D.plus ->
(m1, n, k1, nk1) tface ->
(m2, k2) bwsface ->
(m, n, k, nk) tface =
fun m12 k12 nk12 f bf ->
match bf with
| Zero ->
let m1, k1, nk1 = (dom_tface f, codr_tface f, cod_tface f) in
let Eq = D.plus_uniq m12 (D.plus_zero m1) in
let Eq = D.plus_uniq k12 (D.plus_zero k1) in
let Eq = D.plus_uniq nk12 (D.plus_zero nk1) in
f
| End (e, bf) -> tface_of_bw_r m12 (D.suc_plus k12) (D.suc_plus nk12) (tface_end f e) bf
| Mid bf -> tface_of_bw_r (D.suc_plus m12) (D.suc_plus k12) (D.suc_plus nk12) (Mid f) bf
let rec tface_of_bw_lt :
type m1 m2 m n k1 k2 k nk nk1.
(m1, m2, m) D.plus ->
(k1, k2, k) D.plus ->
(nk1, k2, nk) D.plus ->
(n, k1, nk1) D.plus ->
(m1, nk1) sface ->
(m2, D.zero, k2, k2) bwtface ->
(m, n, k, nk) tface =
fun m12 k12 n12k nk12 f bf ->
match bf with
| REnd (e, bf) -> tface_of_bw_r m12 (D.suc_plus k12) (D.suc_plus n12k) (End (f, nk12, e)) bf
| RMid bf ->
tface_of_bw_lt (D.suc_plus m12) (D.suc_plus k12) (D.suc_plus n12k) (Suc nk12) (Mid f) bf
let rec tface_of_bw_ls :
type m1 m2 m n1 n2 k n nk nk2.
(m1, m2, m) D.plus ->
(n1, n2, n) D.plus ->
(n1, nk2, nk) D.plus ->
(m1, n1) sface ->
(m2, n2, k, nk2) bwtface ->
(m, n, k, nk) tface =
fun m12 n12 nk12 f bf ->
match bf with
| LEnd (e, bf) -> tface_of_bw_ls m12 (D.suc_plus n12) (D.suc_plus nk12) (End (f, e)) bf
| LMid bf -> tface_of_bw_ls (D.suc_plus m12) (D.suc_plus n12) (D.suc_plus nk12) (Mid f) bf
| REnd (e, bf) ->
let n1 = cod_sface f in
let Eq = D.plus_uniq n12 (D.plus_zero n1) in
tface_of_bw_r m12
(D.suc_plus_eq_suc (D.zero_plus (cod_bwsface bf)))
(D.suc_plus nk12)
(End (f, D.plus_zero n1, e))
bf
| RMid bf ->
let n1 = cod_sface f in
let Eq = D.plus_uniq n12 (D.plus_zero n1) in
tface_of_bw_lt (D.suc_plus m12)
(D.suc_plus_eq_suc (D.zero_plus (cod_bwtface bf)))
(D.suc_plus nk12) (Suc Zero) (Mid f) bf
let tface_of_bw : type m n k nk. (m, n, k, nk) bwtface -> (m, n, k, nk) tface =
fun bf ->
tface_of_bw_ls
(D.zero_plus (dom_bwtface bf))
(D.zero_plus (codl_bwtface bf))
(D.zero_plus (cod_bwtface bf))
(id_sface D.zero) bf