@@ -3,25 +3,43 @@ resource Coordination = open Prelude in {
33param
44 ListSize = TwoElem | ManyElem ;
55
6- oper
6+ oper
7+ -- Type of [X] for any X whose lincat is {s : Str}.
8+ -- example : ListX = {s1 = "a , b" ; s2 = "c"}
79 ListX = {s1, s2 : Str} ;
810
9- twoStr : (x, y : Str) -> ListX = \ x, y ->
11+ -- Helper funs for twoSS and conjSS
12+ twoStr : (x, y : Str) -> ListX = \ x, y ->
1013 {s1 = x ; s2 = y} ;
11- consStr : Str -> ListX -> Str -> ListX = \ comma, xs, x ->
14+ consStr : Str -> ListX -> Str -> ListX = \ comma, xs, x ->
1215 {s1 = xs. s1 ++ comma ++ xs. s2 ; s2 = x } ;
1316
14- twoSS : (_, _ : SS) -> ListX = \ x, y ->
17+ -- Create a ListX from two Xs. Example:
18+ -- x = {s = "here"} ;
19+ -- y = {s = "there"} ;
20+ -- twoSS x y ==> {s1 = "here" ; s2 = "there"}
21+ twoSS : (_, _ : SS) -> ListX = \ x, y ->
1522 twoStr x. s y. s ;
16- consSS : Str -> ListX -> SS -> ListX = \ comma, xs, x ->
23+
24+ -- Add new X to a ListX, along with a separator. Example:
25+ -- comma = ","
26+ -- xs = {s1 = "here" ; s2 = "there"}
27+ -- x = {s = "everywhere"}
28+ -- consSS comma xs x ==> {s1 = "here , there" ; s2 = "everywhere"}
29+ consSS : Str -> ListX -> SS -> ListX = \ comma, xs, x ->
1730 consStr comma xs x. s ;
1831
1932 Conjunction : Type = SS ;
2033 ConjunctionDistr : Type = {s1 : Str ; s2 : Str} ;
2134
35+ -- Form an X from Conjunction and ListX. Example:
36+ -- or = {s = "and"}
37+ -- xs = {s1 = "here , there" ; s2 = "everywhere"}
38+ -- conjunctX or xs = {s = "here, there and everywhere"}
2239 conjunctX : Conjunction -> ListX -> Str = \ or, xs ->
2340 xs. s1 ++ or. s ++ xs. s2 ;
24-
41+
42+ -- Like conjunctX, but conjunction has two parts: "both here and there"
2543 conjunctDistrX : ConjunctionDistr -> ListX -> Str = \ or, xs ->
2644 or. s1 ++ xs. s1 ++ or. s2 ++ xs. s2 ;
2745
3351
3452 -- all this lifted to tables
3553
36- ListTable : PType -> Type = \ P -> {s1, s2 : P => Str} ;
54+ -- Type for a table with the given parameter P on the LHS.
55+ -- For example, if the lincat for X is {s : Number => Str},
56+ -- then the lincat for [X] should be ListTable Number, which expands to {s1, s2 : Number => Str}.
57+ ListTable : PType -> Type = \ P -> {s1, s2 : P => Str} ;
3758
3859 twoTable : (P : PType) -> (_, _ : {s : P => Str}) -> ListTable P = \ _, x, y ->
3960 {s1 = x. s ; s2 = y. s} ;
0 commit comments