Implement primitive lists.

The syntax for lists is `[e1, ..., en]` and `e1 :: e2`.

The stuff in `std` seems messed up, although I did convert it so
that it uses lists.

prelude.m31

@@ -2,8 +2,8 @@
 #include_once "std/base.m31"
 #include_once "std/equal.m31"
 
-let top_betas = nil
-let top_hints = nil
-let top_action = reset
+let top_betas = ref []
+let top_hints = ref []
+let top_action = ref reset
 
 #include "std/equal_handle.m31"

src/nucleus/eval.ml

@@ -36,6 +36,10 @@ let as_ref ~loc v =
   let e = Value.as_ref ~loc v in
   Value.return e
 
+let as_list ~loc v =
+  let lst = Value.as_list ~loc v in
+  Value.return lst
+
 (** Evaluate a computation -- infer mode. *)
 let rec infer env (c',loc) =
   match c' with
@@ -75,6 +79,14 @@ let rec infer env (c',loc) =
        in
        fold [] cs
 
+    | Syntax.Nil ->
+       Value.return Value.list_nil
+
+    | Syntax.Cons (c1, c2) ->
+       infer env c1 >>= fun v1 ->
+       infer env c2 >>= as_list ~loc >>= fun lst ->
+       Value.return (Value.list_cons v1 lst)
+
     | Syntax.Handler {Syntax.handler_val; handler_ops; handler_finally} ->
         let handler_val =
           begin match handler_val with
@@ -254,7 +266,7 @@ let rec infer env (c',loc) =
               Value.apply_closure env f >>= fun v ->
               fold v cs
           end
-        | Value.Ty _ | Value.Handler _ | Value.Tag _ | Value.Ref _ ->
+        | Value.Ty _ | Value.Handler _ | Value.Tag _ | Value.List _ | Value.Ref _ ->
           Error.runtime ~loc "cannot apply %s" (Value.name_of v)
     in
     infer env c >>= fun v -> fold v cs
@@ -374,6 +386,8 @@ and check env ((c',loc) as c) (((ctx_check, t_check') as t_check) : Judgement.ty
   | Syntax.Handler _
   | Syntax.External _
   | Syntax.Tag _
+  | Syntax.Nil
+  | Syntax.Cons _
   | Syntax.Where _
   | Syntax.With _
   | Syntax.Typeof _

src/nucleus/value.ml

@@ -24,6 +24,7 @@ type value =
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | List of value list
   | Ref of value ref
 
 and ('a,'b) closure = dynamic -> 'a -> 'b result
@@ -86,6 +87,8 @@ and print_value ?max_level xs v ppf =
   | Closure f -> print_closure xs f ppf
   | Handler h -> print_handler xs h ppf
   | Tag (t, lst) -> print_tag ?max_level xs t lst ppf
+  | List lst -> Print.print ~at_level:0 ppf "[%t]"
+                            (Print.sequence (print_value ~max_level:2 xs) "," lst)
   | Ref v -> Print.print ?max_level ~at_level:1 ppf "ref@ %t" (print_value ~max_level:0 xs (!v))
 
 let name_of v =
@@ -95,67 +98,71 @@ let name_of v =
     | Closure _ -> "a function"
     | Handler _ -> "a handler"
     | Tag _ -> "a data tag"
+    | List _ -> "a list"
     | Ref _ -> "a reference"
 
 let as_term ~loc = function
   | Term e -> e
-  | (Ty _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_ty ~loc = function
   | Ty t -> t
-  | (Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_closure ~loc = function
   | Closure f -> f
-  | (Ty _ | Term _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_handler ~loc = function
   | Handler h -> h
-  | (Ty _ | Term _ | Closure _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Closure _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_ref ~loc = function
   | Ref v -> v
-  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _) as v ->
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | List _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let name_some = Name.make "Some"
 let name_none = Name.make "None"
 let name_pair = Name.make "pair"
-let name_cons = Name.make "cons"
-let name_nil = Name.make "nil"
 let name_unit = Name.make "tt"
 
 let predefined_tags = [
   (name_some, 1);
   (name_none, 0);
   (name_pair, 2);
-  (name_cons, 2);
-  (name_nil, 0);
   (name_unit, 0);
 ]
 
 let as_option ~loc = function
   | Tag (t,[]) when (Name.eq_ident t name_none)  -> None
   | Tag (t,[x]) when (Name.eq_ident t name_some) -> Some x
-  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
+let as_list ~loc = function
+  | List lst -> lst
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a list but got %s" (name_of v)
+
 let from_option = function
   | None -> Tag (name_none, [])
   | Some v -> Tag (name_some, [v])
 
 let from_pair (v1, v2) = Tag (name_pair, [v1; v2])
 
-let rec from_list = function
-  | [] -> Tag (name_nil, [])
-  | v :: vs -> Tag (name_cons, [v; from_list vs])
+let from_list lst = List lst
 
 let mk_tag t lst = Tag (t, lst)
 
+let list_nil = List []
+
+let list_cons v lst = List (v :: lst)
+
 let return x = Return x
 
 let return_term e = Return (Term e)
@@ -233,6 +240,14 @@ let rec equal_value v1 v2 =
         in
       fold vs1 vs2
 
+    | List lst1, List lst2 ->
+       let rec fold = function
+         | [], [] -> true
+         | v1 :: lst1, v2 :: lst2 -> equal_value v1 v2 && fold (lst1, lst2)
+         | [], _::_ | _::_, [] -> false
+       in
+       fold (lst1, lst2)
+
     | Ref v1, Ref v2 ->
        (* XXX should we compare references by value instead? *)
        v1 == v2
@@ -242,12 +257,13 @@ let rec equal_value v1 v2 =
        (* XXX should we use physical comparison == instead? *)
        false
 
-    | Term _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Ty _, (Term _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Closure _, (Term _ | Ty _ | Handler _ | Tag _ | Ref _)
-    | Handler _, (Term _ | Ty _ | Closure _ | Tag _ | Ref _)
-    | Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Ref _)
-    | Ref _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _) ->
+    | Term _, (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Ty _, (Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Closure _, (Term _ | Ty _ | Handler _ | Tag _ | List _ | Ref _)
+    | Handler _, (Term _ | Ty _ | Closure _ | Tag _ | List _ | Ref _)
+    | Tag _, (Term _ | Ty _ | Closure _ | Handler _ | List _ | Ref _)
+    | List _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
+    | Ref _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _) ->
       false
 
 let (>>=) = bind
@@ -705,8 +721,16 @@ module Env = struct
     | Syntax.Patt_Tag (tag, ps), Tag (tag', vs) when Name.eq_ident tag tag' ->
       multicollect_pattern env xvs ps vs
 
-    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | Ref _) ->
+    | Syntax.Patt_Nil, List [] -> xvs
+
+    | Syntax.Patt_Cons (p1, p2), List (v1 :: v2) ->
+       let xvs = collect_pattern env xvs p1 v1 in
+       collect_pattern env xvs p2 (List v2)
+
+    | Syntax.Patt_Nil, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Cons _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) ->
        raise Match_fail
 
   and multicollect_pattern env xvs ps vs =

src/nucleus/value.mli

@@ -21,6 +21,7 @@ type value = private
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | List of value list
   | Ref of value ref
 
 and ('a,'b) closure
@@ -61,8 +62,11 @@ val from_list : value list -> value
 
 (** Convert tags to ocaml types *)
 val as_option : loc:Location.t -> value -> value option
+val as_list : loc:Location.t -> value -> value list
 
 val mk_tag : Name.ident -> value list -> value
+val list_nil : value
+val list_cons : value -> value list -> value
 
 val return : 'a -> 'a result
 val return_term : Judgement.term -> value result

src/parser/desugar.ml

@@ -218,7 +218,7 @@ let rec pattern (env : Value.Env.t) bound vars n (p,loc) =
       let p2, vars, n = tt_pattern env bound vars n p2 in
       (Syntax.Patt_Jdg (p1,p2), loc), vars, n
 
-    | Input.Patt_Data (t,ps) ->
+    | Input.Patt_Tag (t,ps) ->
       let rec fold vars n ps = function
         | [] ->
           let ps = List.rev ps in
@@ -229,6 +229,20 @@ let rec pattern (env : Value.Env.t) bound vars n (p,loc) =
         in
       fold vars n [] ps
 
+    | Input.Patt_Cons (p1, p2) ->
+      let p1, vars, n = pattern env bound vars n p1 in
+      let p2, vars, n = pattern env bound vars n p2 in
+      (Syntax.Patt_Cons (p1,p2), loc), vars, n
+
+    | Input.Patt_List ps ->
+       let rec fold ~loc vars n = function
+         | [] -> (Syntax.Patt_Nil, loc), vars, n
+         | p :: ps ->
+            let p, vars, n = pattern env bound vars n p in
+            let ps, vars, n = fold ~loc:(snd p) vars n ps in
+            (Syntax.Patt_Cons (p, ps), loc), vars, n
+       in
+       fold ~loc vars n ps
 
 let rec comp ~yield (env : Value.Env.t) bound (c',loc) =
   match c' with
@@ -461,6 +475,21 @@ let rec comp ~yield (env : Value.Env.t) bound (c',loc) =
      let cs = List.map (comp ~yield env bound) cs in
      Syntax.Tag (t, cs), loc
 
+  | Input.List cs ->
+     let rec fold ~loc = function
+       | [] -> Syntax.Nil, loc
+       | c :: cs ->
+          let c = comp ~yield env bound c in
+          let cs = fold ~loc:(snd c) cs in
+          Syntax.Cons (c, cs), loc
+     in
+     fold ~loc cs
+
+  | Input.Cons (e1, e2) ->
+    let e1 = comp ~yield env bound e1 in
+    let e2 = comp ~yield env bound e2 in
+    Syntax.Cons (e1,e2), loc
+
   | Input.Congruence (e1,e2) ->
     let e1 = comp ~yield env bound e1 in
     let e2 = comp ~yield env bound e2 in

src/parser/input.mli

@@ -30,7 +30,9 @@ and pattern' =
   | Patt_Var of Name.ident
   | Patt_Name of Name.ident
   | Patt_Jdg of tt_pattern * tt_pattern
-  | Patt_Data of Name.ident * pattern list
+  | Patt_Tag of Name.ident * pattern list
+  | Patt_Cons of pattern * pattern
+  | Patt_List of pattern list
 
 (** Sugared terms *)
 type term = term' * Location.t
@@ -45,6 +47,8 @@ and term' =
   | Handle of comp * handle_case list
   | With of expr * comp
   | Tag of Name.ident * comp list
+  | Cons of comp * comp
+  | List of comp list
   | Match of comp * match_case list
   | Let of (Name.ident * comp) list * comp
   | Lookup of comp

src/parser/lexer.ml

@@ -97,10 +97,13 @@ and token_aux ({ stream;_ } as lexbuf) =
   | quoted_string            -> f (); let s = lexeme lexbuf in QUOTED_STRING (String.sub s 1 (String.length s - 2))
   | '('                      -> f (); LPAREN
   | ')'                      -> f (); RPAREN
+  | '['                      -> f (); LBRACK
+  | ']'                      -> f (); RBRACK
   | '{'                      -> f (); LBRACE
   | '}'                      -> f (); RBRACE
   | "="                      -> f (); EQ
   | ':'                      -> f (); COLON
+  | "::"                     -> f (); COLONCOLON
   | ','                      -> f (); COMMA
   | '?', name                -> f (); PATTVAR (let s = lexeme lexbuf in String.sub s 1 (String.length s - 1))
   | '.', name                -> f (); PROJECTION (let s = lexeme lexbuf in String.sub s 1 (String.length s - 1))

src/parser/parser.mly

@@ -32,7 +32,8 @@
 (* Parentheses & punctuations *)
 %token LPAREN RPAREN
 %token LBRACE RBRACE
-%token COLON COMMA
+%token LBRACK RBRACK
+%token COLON COLONCOLON COMMA
 %token ARROW DARROW
 
 (* Things specific to toplevel *)
@@ -82,6 +83,7 @@
 %nonassoc COLONEQ
 %left     INFIXOP0
 %right    INFIXOP1
+%right    COLONCOLON
 %left     INFIXOP2
 %left     INFIXOP3
 %right    INFIXOP4
@@ -167,6 +169,7 @@ binop_term: mark_location(plain_binop_term) { $1 }
 plain_binop_term:
   | e=plain_app_term                                { e }
   | e1=app_term COLONEQ e2=binop_term               { Update (e1, e2) }
+  | e1=binop_term COLONCOLON e2=binop_term          { Cons (e1, e2) }
   | e2=binop_term op=INFIXOP0 e3=binop_term
     { let e1 = Var (Name.make ~fixity:Name.Infix0 (fst op)), snd op in Spine (e1, [e2; e3]) }
   | e2=binop_term op=INFIXOP1 e3=binop_term
@@ -203,6 +206,7 @@ plain_simple_term:
   | TYPE                                            { Type }
   | x=var_name                                      { Var x }
   | EXTERNAL s=QUOTED_STRING                        { External s }
+  | LBRACK lst=separated_list(COMMA, equal_term) RBRACK { List lst }
   | LPAREN e=plain_term RPAREN                      { e }
   | LBRACE lst=separated_list(COMMA, signature_clause) RBRACE
         { Signature lst }
@@ -330,32 +334,35 @@ binop_pattern: mark_location(plain_binop_pattern) { $1 }
 plain_binop_pattern:
   | e=plain_app_pattern                                { e }
   | e1=binop_pattern op=INFIXOP0 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix0 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix0 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP1 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix1 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix1 (fst op) in Patt_Tag (op, [e1; e2]) }
+  | e1=binop_pattern COLONCOLON  e2=binop_pattern
+    { Patt_Cons (e1, e2) }
   | e1=binop_pattern op=INFIXOP2 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix2 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix2 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP3 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix3 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix3 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP4 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix4 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix4 (fst op) in Patt_Tag (op, [e1; e2]) }
 
 (* app_pattern: mark_location(plain_app_pattern) { $1 } *)
 plain_app_pattern:
   | e=plain_prefix_pattern                    { e }
-  | t=var_name ps=prefix_pattern+             { Patt_Data (t, ps) }
+  | t=var_name ps=prefix_pattern+             { Patt_Tag (t, ps) }
 
 prefix_pattern: mark_location(plain_prefix_pattern) { $1 }
 plain_prefix_pattern:
   | e=plain_simple_pattern           { e }
-  | op=PREFIXOP e=prefix_pattern     { let op = Name.make ~fixity:Name.Prefix (fst op) in Patt_Data (op, [e]) }
+  | op=PREFIXOP e=prefix_pattern     { let op = Name.make ~fixity:Name.Prefix (fst op) in Patt_Tag (op, [e]) }
 
 simple_pattern: mark_location(plain_simple_pattern) { $1 }
 plain_simple_pattern:
   | UNDERSCORE                     { Patt_Anonymous }
   | x=patt_var                     { Patt_Var x }
-  | x=var_name                     { Patt_Name x } 
+  | x=var_name                     { Patt_Name x }
   | LPAREN p=plain_pattern RPAREN  { p }
+  | LBRACK ps=separated_list(COMMA, pattern) RBRACK { Patt_List ps }
 
 tt_pattern: mark_location(plain_tt_pattern) { $1 }
 plain_tt_pattern: