notes/Lists.txt

   1 Lists in Prop are simply syntactic sugar.  For example, the declaration
   2
   3     datatype List = #[]
   4                   | #[ int ... List ]
   5                   ;
   6
   7 defines a list of integers.   The special form #[ ... ] is used to
   8 build lists of arbitrary lengths.   Here are some examples of valid
   9 list expressions:
  10
  11      List a = #[];             // the empty list
  12      List b = #[ 1, 2, 3 ];    // list of three elements
  13      List c = #[ 4, 5 ... b ]; // the list #[ 4, 5, 1, 2, 3]
  14                                // i.e. 4 and 5 prepended to the list b.
  15
  16 List patterns are written in a form that directly reflects the
  17 constructor syntax:
  18
  19    match (l) {
  20       case #[]:     cout << "Matches the empty list\n";
  21       case #[x]:    cout << "List of one element " << x << '\n';
  22       case #[x,y]:  cout << "List of two elements "
  23                          << x << " and " << y << '\n';
  24       case #[x, y, z ... l]:   // Pattern variables x, y, z are bound the
  25                                // first 3 elements, while l is bound to
  26                                // the rest of the list
  27                     cout << "List of three of more elements\n";
  28
  29    }
  30
  31 Of course, list pattern may be arbitrary nested and may also contain
  32 subpatterns.  Everything that applies to algebraic datatypes also apply
  33 to list patterns.
  34
  35 Note (1): that there are *no* built-in lists (having the list type built
  36 in would make customization difficult.)   The users must declare their
  37 own list types.   But this is entirely trivial.
  38
  39 Note (2): besides #[] and #[ ... ], there are 2 other pairs of list-like
  40 constructors:
  41
  42      #()   #( ... )
  43      #{}   #{ ... }
  44
  45 It is possible to define multiple list-like datatypes, each using a different
  46 special form.
  47
  48 Note (3): you are allowed to have other variants within a list-like type.
  49 For example, definitions like
  50
  51     datatype SEXPR = #()
  52                    | #( SEXPR ... SEXPR )
  53                    | number  (int)
  54                    | string  (char *)
  55                    | boolean (bool)
  56                    ;
  57
  58 are allowed.   The only restriction in this case is that #() and #( ... ) must
  59 be defined within the same datatype and that the second argument type of
  60 #( ... ) must be the same as SEXPR.
  61
  62 Note (4):  aside from the special form syntax currently there are no
  63 special support for lists.  You'll have to roll your own list processing
  64 functions.  In the future I'll provide a standard list template library.