tsil.ml (1260B)
1 (* A tsil is a backwards list (i.e., tail to left and head to right). In 2 * dependent type systems, telescopes/contexts are essentially tsils, because 3 * later variables can depend on earlier variables. Thus, we sometimes use 4 * tsils instead of lists to aid readability. Moreover, one can view lists as 5 * reversed tsils and vice versa (and this module provides functions in service 6 * of this viewpoint), so disciplined use of tsils and lists can help prevent 7 * accidental telescope/context reversal via static checks in OCaml. That is, 8 * if a tsil represents a context and a list represents a reversed context, 9 * then it is impossible to accidentally reverse a context, because that would 10 * amount to an OCaml type error. *) 11 (* TODO: This comment overstates how much we use tsils. We've mostly switched 12 * to arrays. *) 13 14 type 'a t = Lin | Snoc of 'a t * 'a 15 16 (* Miraculously, (<@) is left associative and (@>) is right associative, as 17 * one would expect. *) 18 19 let rec (<@) l r = match r with 20 | x :: r -> Snoc (l, x) <@ r 21 | [] -> l 22 let appendl = (<@) 23 24 let rec (@>) l r = match l with 25 | Snoc (l, x) -> l @> (x :: r) 26 | Lin -> r 27 let appendr = (@>) 28 29 let of_list r = Lin <@ r 30 31 let to_list l = l @> [] 32 33 module Ops = struct 34 let (<@) = (<@) 35 let (@>) = (@>) 36 end