Change array syntax and fix propagation of mutability

samples/hoare.as

@@ -1,12 +1,12 @@
 /* integer quicksort as top-level functions */
 
-func swap(a : var Int[], i : Nat, j : Nat) {
+func swap(a : [var Int], i : Nat, j : Nat) {
   let temp = a[i];
   a[i] := a[j];
   a[j] := temp;
 };
 
-func partition(a : var Int[], lo : Nat, hi : Nat) : Nat {
+func partition(a : [var Int], lo : Nat, hi : Nat) : Nat {
   let pivot = a[lo];
   var i : Nat = lo;
   var j : Nat = hi;
@@ -19,13 +19,13 @@ func partition(a : var Int[], lo : Nat, hi : Nat) : Nat {
   };
 };
 
-func quicksort(a : var Int[], lo : Nat, hi : Nat) {
+func quicksort(a : [var Int], lo : Nat, hi : Nat) {
   if (lo < hi) {
     let p = partition(a, lo, hi);
 	  quicksort(a, lo, p);
 	  quicksort(a, p + 1, hi);  
 	};
 };
 
-let a : var Int[] = [8, 3, 9, 5, 2];
+let a : [var Int] = [var 8, 3, 9, 5, 2];
 quicksort(a, 0, 4);

samples/hoare.txt

@@ -1,8 +1,8 @@
 -- Checking hoare.as:
-let a : var Int[]
-let partition : (var Int[], Nat, Nat) -> Nat
-let quicksort : (var Int[], Nat, Nat) -> ()
-let swap : (var Int[], Nat, Nat) -> ()
+let a : [var Int]
+let partition : ([var Int], Nat, Nat) -> Nat
+let quicksort : ([var Int], Nat, Nat) -> ()
+let swap : ([var Int], Nat, Nat) -> ()
 -- Interpreting hoare.as:
 quicksort([8, 3, 9, 5, 2], 0, 4)
   partition([8, 3, 9, 5, 2], 0, 4)
@@ -37,8 +37,8 @@ quicksort([8, 3, 9, 5, 2], 0, 4)
     <= ()
   <= ()
 -- Finished hoare.as:
-let a : var Int[] = [2, 3, 5, 8, 9]
-let partition : (var Int[], Nat, Nat) -> Nat = func
-let quicksort : (var Int[], Nat, Nat) -> () = func
-let swap : (var Int[], Nat, Nat) -> () = func
+let a : [var Int] = [2, 3, 5, 8, 9]
+let partition : ([var Int], Nat, Nat) -> Nat = func
+let quicksort : ([var Int], Nat, Nat) -> () = func
+let swap : ([var Int], Nat, Nat) -> () = func
 

samples/quicksort.as

@@ -2,7 +2,7 @@
    - inplace sorting of mutable arrays of T, for any type T
 */
 
-type Array<T> = var T[];
+type Array<T> = [var T];
 
 class QS<T>(cmp : (T, T) -> Int) {
   quicksort(a : Array<T>, lo : Nat, hi : Nat) {
@@ -44,5 +44,5 @@ class QS<T>(cmp : (T, T) -> Int) {
 
 func cmpi(i : Int, j : Int) : Int = i - j;
 let qs = QS<Int>(cmpi);
-let a : Array<Int> = [8, 3, 9, 5, 2];
+let a : Array<Int> = [var 8, 3, 9, 5, 2];
 qs.quicksort(a, 0, 4);

samples/quicksort.txt

@@ -1,5 +1,5 @@
 -- Checking quicksort.as:
-type Array<T> = var T[]
+type Array<T> = [var T]
 type QS<T> <: {quicksort : (Array<T>, Nat, Nat) -> ()}
 let QS : class <T>((T, T) -> Int) -> QS<T>
 let a : Array<Int>

src/arrange.ml

@@ -15,7 +15,7 @@ let rec exp e = match e.it with
   | ObjE (s, i, efs)    -> "ObjE"    $$ [obj_sort s; id i] @ List.map exp_field efs
   | DotE (e, n)         -> "DotE"    $$ [exp e; name n]
   | AssignE (e1, e2)    -> "AssignE" $$ [exp e1; exp e2]
-  | ArrayE es           -> "ArrayE"  $$ List.map exp es
+  | ArrayE (m, es)      -> "ArrayE"  $$ [mut m] @ List.map exp es
   | IdxE (e1, e2)       -> "IdxE"    $$ [exp e1; exp e2]
   | CallE (e1, ts, e2)  -> "CallE"   $$ [exp e1] @ List.map typ ts @ [exp e2]
   | BlockE ds           -> "BlockE"  $$ List.map dec ds

src/arrange_ir.ml

@@ -15,7 +15,7 @@ let rec exp e = match e.it with
   | ObjE (s, i, efs)    -> "ObjE"    $$ [Arrange.obj_sort s; id i] @ List.map exp_field efs
   | DotE (e, n)         -> "DotE"    $$ [exp e; name n]
   | AssignE (e1, e2)    -> "AssignE" $$ [exp e1; exp e2]
-  | ArrayE es           -> "ArrayE"  $$ List.map exp es
+  | ArrayE (m, es)      -> "ArrayE"  $$ [Arrange.mut m] @ List.map exp es
   | IdxE (e1, e2)       -> "IdxE"    $$ [exp e1; exp e2]
   | CallE (cc, e1, ts, e2) -> "CallE" $$ [Atom (Value.string_of_call_conv cc); exp e1] @ List.map Arrange.typ ts @ [exp e2]
   | BlockE ds           -> "BlockE"  $$ List.map dec ds

src/async.ml

@@ -235,8 +235,8 @@ and t_exp' (exp:Syntax.exp) =
     DotE (t_exp exp1, id)
   | AssignE (exp1, exp2) ->
     AssignE (t_exp exp1, t_exp exp2)
-  | ArrayE exps ->
-    ArrayE (List.map t_exp exps)
+  | ArrayE (mut, exps) ->
+    ArrayE (mut, List.map t_exp exps)
   | IdxE (exp1, exp2) ->
      IdxE (t_exp exp1, t_exp exp2)
   | CallE ({it=PrimE "@await";_}, typs, exp2) ->

src/awaitopt.ml

@@ -86,8 +86,8 @@ and t_exp' context exp' =
     DotE (t_exp context exp1, id)
   | AssignE (exp1, exp2) ->
     AssignE (t_exp context exp1, t_exp context exp2)
-  | ArrayE exps ->
-    ArrayE (List.map (t_exp context) exps)
+  | ArrayE (mut, exps) ->
+    ArrayE (mut, List.map (t_exp context) exps)
   | IdxE (exp1, exp2) ->
     IdxE (t_exp context exp1, t_exp context exp2)
   | CallE (exp1, typs, exp2) ->
@@ -409,8 +409,8 @@ and c_exp' context exp k =
     unary context k (fun v1 -> e (DotE (v1, id))) exp1 
   | AssignE (exp1, exp2) ->
     binary context k (fun v1 v2 -> e (AssignE (v1, v2))) exp1 exp2
-  | ArrayE exps ->
-    nary context k (fun vs -> e (ArrayE vs)) exps
+  | ArrayE (mut, exps) ->
+    nary context k (fun vs -> e (ArrayE (mut, vs))) exps
   | IdxE (exp1, exp2) ->
     binary context k (fun v1 v2 -> e (IdxE (v1, v2))) exp1 exp2
   | CallE (exp1, typs, exp2) ->

src/compile.ml

@@ -3076,7 +3076,7 @@ and compile_exp (env : E.t) exp = match exp.it with
   | ProjE (e1,n) ->
      compile_exp env e1 ^^ (* offset to tuple (an array) *)
      Array.load_n (Int32.of_int n)
-  | ArrayE es -> Array.lit env (List.map (compile_exp env) es)
+  | ArrayE (m, es) -> Array.lit env (List.map (compile_exp env) es)
   | ObjE ({ it = Type.Object _ (*sharing*); _}, name, fs) -> (* TBR - really the same for local and shared? *)
      let fs' = List.map
       (fun (f : Ir.exp_field) ->

src/desugar.ml

@@ -37,7 +37,7 @@ let
     | S.ObjE (s, i, es) -> I.ObjE (s, i, exp_fields es)
     | S.DotE (e, n) -> I.DotE (exp e, n)
     | S.AssignE (e1, e2) -> I.AssignE (exp e1, exp e2)
-    | S.ArrayE es -> I.ArrayE (exps es)
+    | S.ArrayE (m, es) -> I.ArrayE (m, exps es)
     | S.IdxE (e1, e2) -> I.IdxE (exp e1, exp e2)
     | S.CallE (e1, inst, e2) ->
       let cc = Value.call_conv_of_typ e1.Source.note.S.note_typ in

src/effect.ml

@@ -50,7 +50,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
     let t2 = effect_exp exp2 in
     max_eff t1 t2
   | TupE exps 
-  | ArrayE exps ->
+  | ArrayE (_, exps) ->
     let es = List.map effect_exp exps in
     List.fold_left max_eff Type.Triv es
   | BlockE decs ->

src/freevars.ml

@@ -44,7 +44,7 @@ let rec exp e : f = match e.it with
   | ObjE (s, i, efs)    -> close (exp_fields efs) // i.it
   | DotE (e, i)         -> exp e
   | AssignE (e1, e2)    -> exps [e1; e2]
-  | ArrayE es           -> exps es
+  | ArrayE (m, es)      -> exps es
   | IdxE (e1, e2)       -> exps [e1; e2]
   | CallE (e1, ts, e2)  -> exps [e1; e2]
   | BlockE ds           -> close (decs ds)

src/freevars_ir.ml

@@ -70,7 +70,7 @@ let rec exp e : f = match e.it with
   | ObjE (s, i, efs)    -> close (exp_fields efs) // i.it
   | DotE (e, i)         -> exp e
   | AssignE (e1, e2)    -> exps [e1; e2]
-  | ArrayE es           -> exps es
+  | ArrayE (m, es)      -> exps es
   | IdxE (e1, e2)       -> exps [e1; e2]
   | CallE (_, e1, ts, e2) -> exps [e1; e2]
   | BlockE ds           -> close (decs ds)

src/interpret.ml

@@ -285,13 +285,12 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
         V.as_mut v1 := v2; k V.unit
       )
     )
-  | ArrayE exps ->
-    let t = exp.note.note_typ in
+  | ArrayE (mut, exps) ->
     interpret_exps env exps [] (fun vs ->
       let vs' =
-        match t with
-        | T.Array (T.Mut _) -> List.map (fun v -> V.Mut (ref v)) vs
-        | _ -> vs
+        match mut.it with
+        | Var -> List.map (fun v -> V.Mut (ref v)) vs
+        | Const -> vs
       in k (V.Array (Array.of_list vs'))
     )
   | IdxE (exp1, exp2) ->

src/ir.ml

@@ -25,7 +25,7 @@ and exp' =
   | ObjE of Syntax.obj_sort * Syntax.id * exp_field list     (* object *)
   | DotE of exp * Syntax.name                  (* object projection *)
   | AssignE of exp * exp                       (* assignment *)
-  | ArrayE of exp list                         (* array *)
+  | ArrayE of Syntax.mut * exp list            (* array *)
   | IdxE of exp * exp                          (* array indexing *)
   | CallE of Value. call_conv * exp * Syntax.typ list * exp (* function call *)
   | BlockE of dec list                         (* block *)

src/parser.mly

@@ -161,9 +161,6 @@ seplist1(X, SEP) :
     { fun sort sloc ->
       ("anon-" ^ sort ^ "-" ^ string_of_pos (at sloc).left) @@ at sloc }
 
-%inline var :
-  | VAR { Var @@ at $sloc }
-
 %inline var_opt :
   | (* empty *) { Const @@ no_region }
   | VAR { Var @@ at $sloc }
@@ -200,14 +197,14 @@ typ_nullary :
     { TupT(ts) @@ at $sloc }
   | x=id tso=typ_args?
     {	VarT(x, Lib.Option.get tso []) @@ at $sloc }
+  | LBRACKET m=var_opt t=typ RBRACKET
+    { ArrayT(m, t) @@ at $sloc }
   | tfs=typ_obj
     { ObjT(Type.Object Type.Local @@ at $sloc, tfs) @@ at $sloc }
 
 typ_post :
   | t=typ_nullary
     { t }
-  | t=typ_post LBRACKET RBRACKET
-    { ArrayT(Const @@ no_region, t) @@ at $sloc }
   | t=typ_post QUEST
     { OptT(t) @@ at $sloc }
 
@@ -220,8 +217,6 @@ typ_pre :
     { AsyncT(t) @@ at $sloc }
   | LIKE t=typ_pre
     { LikeT(t) @@ at $sloc }
-  | mut=var t=typ_nullary LBRACKET RBRACKET
-    { ArrayT(mut, t) @@ at $sloc }
   | s=obj_sort tfs=typ_obj
     { let tfs' =
         if s.it = Type.Object Type.Local
@@ -349,12 +344,14 @@ exp_nullary :
         then efs
         else List.map share_expfield efs
       in ObjE(s, xf anon $sloc, efs') @? at $sloc }
+  | PRIM s=TEXT
+    { PrimE(s) @? at $sloc }
 
 exp_post :
   | e=exp_nullary
     { e }
-  | LBRACKET es=seplist(exp, COMMA) RBRACKET
-    { ArrayE(es) @? at $sloc }
+  | LBRACKET m=var_opt es=seplist(exp_nonvar, COMMA) RBRACKET
+    { ArrayE(m, es) @? at $sloc }
   | e=exp_post QUEST
     { OptE(e) @? at $sloc }
   | e1=exp_post LBRACKET e2=exp RBRACKET
@@ -399,8 +396,6 @@ exp_bin :
 exp_pre :
   | e=exp_bin
     { e }
-  | PRIM s=TEXT
-    { PrimE(s) @? at $sloc }
   | RETURN eo=exp_pre?
     { let e = Lib.Option.get eo (TupE([]) @? at $sloc) in
       RetE(e) @? at $sloc }
@@ -445,10 +440,16 @@ exp_nondec :
   | FOR LPAR p=pat IN e1=exp RPAR e2=exp
     { ForE(p, e1, e2) @? at $sloc }
 
-exp :
+exp_nonvar :
   | e=exp_nondec
     { e }
-  | d=dec_nonexp
+  | d=dec_nonvar
+    { DecE(d) @? at $sloc }
+
+exp :
+  | e=exp_nonvar
+    { e }
+  | d=dec_var
     { DecE(d) @? at $sloc }
 
 
@@ -518,7 +519,7 @@ return_typ_nullary :
 
 (* Declarations *)
 
-dec_nonexp :
+dec_var :
   | LET p=pat EQ e=exp
     { let p', e' =
         match p.it with
@@ -531,6 +532,8 @@ dec_nonexp :
         | None -> e
         | Some t -> AnnotE (e, t) @? span t.at e.at
       in VarD(x, e') @? at $sloc }
+
+dec_nonvar :
   | s=shared_opt FUNC xf=id_opt fd=func_dec
     { (fd s (xf "func" $sloc)).it @? at $sloc }
   | TYPE x=id tps=typ_params_opt EQ t=typ
@@ -544,8 +547,11 @@ dec_nonexp :
       in
       let id as tid = xf "class" $sloc in	
       ClassD(xf "class" $sloc, tid, tps, s, p, x, efs') @? at $sloc }
+
 dec :
-  | d=dec_nonexp
+  | d=dec_var
+    { d }
+  | d=dec_nonvar
     { d }
   | e=exp_nondec
     { ExpD e @? at $sloc }