CompE and FieldWiseI added

spectec/src/al/al_util.ml

@@ -34,6 +34,7 @@ let performI ?(at = no) (id, el) = PerformI (id, el) |> mk_instr at
 let exitI ?(at = no) a = ExitI a |> mk_instr at
 let replaceI ?(at = no) (e1, p, e2) = ReplaceI (e1, p, e2) |> mk_instr at
 let appendI ?(at = no) (e1, e2) = AppendI (e1, e2) |> mk_instr at
+let fieldwiseappendI ?(at = no) (e1, e2) = FieldWiseAppendI (e1, e2) |> mk_instr at
 let otherwiseI ?(at = no) il = OtherwiseI il |> mk_instr at
 let yetI ?(at = no) s = YetI s |> mk_instr at
 
@@ -48,6 +49,7 @@ let accE ?(at = no) ~note (e, p) = AccE (e, p) |> mk_expr at note
 let updE ?(at = no) ~note (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at note
 let extE ?(at = no) ~note (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at note
 let strE ?(at = no) ~note r = StrE r |> mk_expr at note
+let compE ?(at = no) ~note (e1, e2) = CompE (e1, e2) |> mk_expr at note
 let catE ?(at = no) ~note (e1, e2) = CatE (e1, e2) |> mk_expr at note
 let memE ?(at = no) ~note (e1, e2) = MemE (e1, e2) |> mk_expr at note
 let lenE ?(at = no) ~note e = LenE e |> mk_expr at note

spectec/src/al/ast.ml

@@ -88,7 +88,8 @@ and expr' =
   | UpdE of expr * path list * expr               (* expr `[` path* `]` `:=` expr *)
   | ExtE of expr * path list * expr * extend_dir  (* expr `[` path* `]` `:+` expr *)
   | StrE of (atom, expr) record                   (* `{` (atom `->` expr)* `}` *)
-  | CatE of expr * expr                           (* expr `++` expr *)
+  | CompE of expr * expr                          (* expr `++` expr *)
+  | CatE of expr * expr                           (* expr `::` expr *)
   | MemE of expr * expr                           (* expr `<-` expr *)
   | LenE of expr                                  (* `|` expr `|` *)
   | TupE of expr list                             (* `(` (expr `,`)* `)` *)
@@ -156,7 +157,8 @@ and instr' =
   | PerformI of id * arg list             (* `perform` id expr* *)
   | ExitI of atom                         (* `exit` *)
   | ReplaceI of expr * path * expr        (* `replace` expr `->` path `with` expr *)
-  | AppendI of expr * expr                (* `append` expr expr *)
+  | AppendI of expr * expr                (* `append` expr to expr *)
+  | FieldWiseAppendI of expr * expr       (* for each field x in expr, `append` expr.x to expr.x *)
   (* Administrative instructions *)
   | OtherwiseI of instr list              (* only during the intermediate processing of il->al *)
   | YetI of string                        (* for future not yet implemented feature *)

spectec/src/al/eq.ml

@@ -19,6 +19,7 @@ let rec eq_expr e1 e2 =
   | ExtE (e11, pl1, e12, d1), ExtE (e21, pl2, e22, d2) ->
     eq_expr e11 e21 && eq_paths pl1 pl2 && eq_expr e12 e22 && d1 = d2
   | StrE r1, StrE r2 -> eq_expr_record r1 r2
+  | CompE (e11, e12), CompE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | CatE (e11, e12), CatE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | MemE (e11, e12), MemE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | LenE e1, LenE e2 -> eq_expr e1 e2
@@ -113,6 +114,7 @@ let rec eq_instr i1 i2 =
   | ReplaceI (e11, p1, e12), ReplaceI (e21, p2, e22) ->
     eq_expr e11 e21 && eq_path p1 p2 && eq_expr e12 e22
   | AppendI (e11, e12), AppendI (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
+  | FieldWiseAppendI (e11, e12),FieldWiseAppendI (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | OtherwiseI il1, OtherwiseI il2 -> eq_instrs il1 il2
   | YetI s1, YetI s2 -> s1 = s2
   | _ -> false

spectec/src/al/free.ml

@@ -29,6 +29,7 @@ let rec free_expr expr =
   | ContE e
   | ChooseE e -> free_expr e
   | BinE (_, e1, e2)
+  | CompE (e1, e2)
   | CatE (e1, e2)
   | MemE (e1, e2)
   | LabelE (e1, e2) -> free_expr e1 @ free_expr e2
@@ -92,7 +93,7 @@ let rec free_instr instr =
   | PushI e | PopI e | PopAllI e | ReturnI (Some e)
   | ExecuteI e | ExecuteSeqI e ->
     free_expr e
-  | LetI (e1, e2) | AppendI (e1, e2) -> free_expr e1 @ free_expr e2
+  | LetI (e1, e2) | AppendI (e1, e2) | FieldWiseAppendI (e1, e2) -> free_expr e1 @ free_expr e2
   | EnterI (e1, e2, il) -> free_expr e1 @ free_expr e2 @ free_list free_instr il
   | AssertI e -> free_expr e
   | PerformI (_, al) -> free_list free_arg al

spectec/src/al/print.ml

@@ -144,8 +144,10 @@ and string_of_expr expr =
         |> sprintf "%s_%s" id
     in
     sprintf "$%s^-1(%s)" id' (string_of_args ", " al)
-  | CatE (e1, e2) ->
+  | CompE (e1, e2) ->
     sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
+  | CatE (e1, e2) ->
+    sprintf "%s :: %s" (string_of_expr e1) (string_of_expr e2)
   | MemE (e1, e2) ->
     sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
@@ -340,6 +342,9 @@ let rec string_of_instr' depth instr =
   | AppendI (e1, e2) ->
     sprintf " %s :+ %s"
       (string_of_expr e2) (string_of_expr e1)
+  | FieldWiseAppendI (e1, e2) ->
+    sprintf " %s :⨁ %s"
+      (string_of_expr e2) (string_of_expr e1)
   | YetI s -> sprintf " YetI: %s." s
 
 and string_of_instrs' depth instrs =
@@ -440,6 +445,12 @@ and structured_string_of_expr expr =
     let nl = List.filter_map (fun x -> x) nl in
     sprintf "InvCallE (%s, [%s], [%s])"
       id (string_of_list string_of_int "" nl) (structured_string_of_args al)
+  | CompE (e1, e2) ->
+    "CompE ("
+    ^ structured_string_of_expr e1
+    ^ ", "
+    ^ structured_string_of_expr e2
+    ^ ")"
   | CatE (e1, e2) ->
     "CatE ("
     ^ structured_string_of_expr e1
@@ -615,6 +626,12 @@ let rec structured_string_of_instr' depth instr =
     ^ ", "
     ^ structured_string_of_expr e2
     ^ ")"
+  | FieldWiseAppendI (e1, e2) ->
+    "FieldWiseAppendI ("
+    ^ structured_string_of_expr e1
+    ^ ", "
+    ^ structured_string_of_expr e2
+    ^ ")"
   | YetI s -> "YetI " ^ s
 
 and structured_string_of_instrs' depth instrs =

spectec/src/al/valid.ml

@@ -250,6 +250,15 @@ let check_field source source_typ expr_record typfield =
   | Some (_, expr_ref) -> check_match source !expr_ref.note typ
   | None -> error_field source source_typ atom
 
+let check_struct source typ =
+  match typ.it with
+  | VarT (id, args) -> (
+    let deftyps = get_deftyps id args in
+    if not (List.exists (fun deftyp -> match deftyp.it with StructT _ -> true | _ -> false) deftyps) then
+      error_valid "not a struct" source ""
+  )
+  | _ -> error_valid "not a struct" source ""
+
 let check_tuple source exprs typ =
   match (ground_typ_of typ).it with
   | TupT etl when List.length exprs = List.length etl ->
@@ -316,7 +325,7 @@ let check_inv_call source id indices args result_typ =
     match result_args with
     | [arg] -> (
       match arg.it with
-    | ExpA exp -> exp.note
+      | ExpA exp -> exp.note
       | a -> error_valid (Printf.sprintf "wrong result argument: %s" (Print.string_of_arg (a $ no_region))) source ""
     )
     | _ -> 
@@ -379,6 +388,9 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
   | StrE r ->
     let typfields = get_typfields expr.note in
     List.iter (check_field source expr.note r) typfields
+  | CompE (expr1, expr2) -> 
+    check_struct source expr1.note; check_struct source expr2.note;
+    check_match source expr.note expr1.note; check_match source expr1.note expr2.note
   | CatE (expr1, expr2) ->
     check_list source expr1.note; check_list source expr2.note;
     check_match source expr.note expr1.note; check_match source expr1.note expr2.note
@@ -473,6 +485,7 @@ let valid_instr (walker: unit_walker) (instr: instr) : unit =
   | ReplaceI (expr1, path, expr2) ->
     access source expr1.note path |> check_match source expr2.note
   | AppendI (expr1, _expr2) -> check_list source expr1.note
+  | FieldWiseAppendI (expr1, expr2) -> check_struct source expr1.note; check_struct source expr2.note
   | OtherwiseI _ | YetI _ -> error_valid "invalid instruction" source ""
   | _ -> ()
   );

spectec/src/al/walk.ml

@@ -40,8 +40,8 @@ let walk_expr (walker: unit_walker) (expr: expr) : unit =
   | UnE (_, e) | LenE e | ArityE e | ContE e
   | IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
   | TopValueE (Some e) | TopValuesE e | ChooseE e -> walker.walk_expr walker e
-
-  | BinE (_, e1, e2) | CatE (e1, e2) | MemE (e1, e2)
+  
+  | BinE (_, e1, e2) | CompE (e1, e2) | CatE (e1, e2) | MemE (e1, e2)
   | LabelE (e1, e2) | MatchE (e1, e2) ->
     walker.walk_expr walker e1; walker.walk_expr walker e2
   | FrameE (e_opt, e) ->
@@ -72,7 +72,7 @@ let walk_instr (walker: unit_walker) (instr: instr) : unit =
   | TrapI | NopI | ReturnI None | ExitI _ | YetI _ -> ()
   | AssertI e | PushI e | PopI e | PopAllI e
   | ReturnI (Some e)| ExecuteI e | ExecuteSeqI e -> walker.walk_expr walker e
-  | LetI (e1, e2) | AppendI (e1, e2) ->
+  | LetI (e1, e2) | AppendI (e1, e2) | FieldWiseAppendI (e1, e2) ->
     walker.walk_expr walker e1; walker.walk_expr walker e2
   | PerformI (_, al) -> List.iter (walker.walk_arg walker) al
   | ReplaceI (e1, p, e2) ->
@@ -136,6 +136,7 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | CallE (id, al) -> CallE (id, List.map walk_arg al)
     | InvCallE (id, nl, al) -> InvCallE (id, nl, List.map walk_arg al)
     | ListE el -> ListE (List.map walk_expr el)
+    | CompE (e1, e2) -> CompE (walk_expr e1, walk_expr e2)
     | CatE (e1, e2) -> CatE (walk_expr e1, walk_expr e2)
     | MemE (e1, e2) -> MemE (walk_expr e1, walk_expr e2)
     | LenE e -> LenE (walk_expr e)
@@ -191,6 +192,7 @@ let walk_instr (walker: walker) (instr: instr) : instr =
     | ExitI _ -> instr.it
     | ReplaceI (e1, p, e2) -> ReplaceI (walk_expr e1, walk_path p, walk_expr e2)
     | AppendI (e1, e2) -> AppendI (walk_expr e1, walk_expr e2)
+    | FieldWiseAppendI (e1, e2) -> FieldWiseAppendI (walk_expr e1, walk_expr e2)
     | YetI _ -> instr.it
   in
   { instr with it }
@@ -254,6 +256,7 @@ let rec walk_expr f e =
       | InvCallE (id, nl, el) -> InvCallE (id, nl, List.map (walk_arg f) el)
       (* TODO: Implement walker for iter *)
       | ListE el -> ListE (List.map new_ el)
+      | CompE (e1, e2) -> CompE (new_ e1, new_ e2)
       | CatE (e1, e2) -> CatE (new_ e1, new_ e2)
       | MemE (e1, e2) -> MemE (new_ e1, new_ e2)
       | LenE e' -> LenE (new_ e')
@@ -339,6 +342,7 @@ let rec walk_instr f (instr:instr) : instr list =
       | ExitI _ -> i.it
       | ReplaceI (e1, p, e2) -> ReplaceI (new_e e1, walk_path f p, new_e e2)
       | AppendI (e1, e2) -> AppendI (new_e e1, new_e e2)
+      | FieldWiseAppendI (e1, e2) -> FieldWiseAppendI (new_e e1, new_e e2)
       | YetI _ -> i.it in
     { i with it = i' }
   in

spectec/src/backend-interpreter/interpreter.ml

@@ -244,6 +244,9 @@ and eval_expr env expr =
     )
   (* Data Structure *)
   | ListE el -> List.map (eval_expr env) el |> listV_of_list
+  (* | CompE (_, _) ->
+    (* TODO: interpret CompE *)
+    raise (Exception.MissingReturnValue "CompE") *)
   | CatE (e1, e2) ->
     let a1 = eval_expr env e1 |> unwrap_listv_to_array in
     let a2 = eval_expr env e2 |> unwrap_listv_to_array in
@@ -661,6 +664,22 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     | _, v -> a := Array.append !a [|v|]
     );
     ctx
+  | FieldWiseAppendI (e1, e2) ->
+    let s1 = eval_expr env e1 |> unwrap_strv in
+    let s2 = eval_expr env e2 |> unwrap_strv in
+    Record.iter
+    (fun (id, v) ->
+    let arr1 = match !v with
+    | ListV arr_ref -> arr_ref
+    | _ -> failwith (sprintf "`%s` is not a list" (string_of_value !v))
+    in
+    let arr2 = match Record.find id s2 with
+    | ListV arr_ref -> arr_ref
+    | v -> failwith (sprintf "`%s` is not a list" (string_of_value v))
+    in
+    arr1 := Array.append !arr1 !arr2
+    ) s1;
+    ctx
   | _ -> failwith "cannot step instr"
 
 and try_step_instr fname ctx env instr =

spectec/src/backend-prose/gen.ml

@@ -136,7 +136,7 @@ let get_rel_kind def =
 
 let transpile_expr =
   Al.Walk.walk_expr { Al.Walk.default_config with
-    post_expr = Il2al.Transpile.simplify_record_concat
+    post_expr = fun expr -> expr |> Il2al.Transpile.simplify_record_concat |> Il2al.Transpile.reduce_comp
   }
 
 let exp_to_expr e = translate_exp e |> transpile_expr

spectec/src/backend-prose/print.ml

@@ -119,8 +119,10 @@ and string_of_expr expr =
         |> sprintf "%s_%s" id
     in
     sprintf "$%s^-1(%s)" id' (string_of_args ", " al)
-  | CatE (e1, e2) ->
+  | CompE (e1, e2) ->
     sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
+  | CatE (e1, e2) ->
+    sprintf "%s :: %s" (string_of_expr e1) (string_of_expr e2)
   | MemE (e1, e2) ->
     sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
@@ -347,6 +349,9 @@ let rec string_of_instr' depth instr =
   | AppendI (e1, e2) ->
     sprintf "%s Append %s to the %s." (make_index depth)
       (string_of_expr e2) (string_of_expr e1)
+  | FieldWiseAppendI (e1, e2) ->
+    sprintf "%s Append %s to the %s, fieldwise." (make_index depth)
+      (string_of_expr e2) (string_of_expr e1)
   | YetI s -> sprintf "%s YetI: %s." (make_index depth) s
 
 and string_of_instrs' depth instrs =

spectec/src/backend-prose/render.ml

@@ -672,6 +672,9 @@ let rec render_al_instr env algoname index depth instr =
   | Al.Ast.AppendI (e1, e2) ->
     sprintf "%s Append %s to the %s." (render_order index depth)
       (render_expr env e2) (render_expr env e1)
+  | Al.Ast.FieldWiseAppendI (e1, e2) ->
+    sprintf "%s Append %s to the %s, fieldwise" (render_order index depth)
+      (render_expr env e2) (render_expr env e1)
   | Al.Ast.YetI s -> sprintf "%s YetI: %s." (render_order index depth) s
 
 and render_al_instrs env algoname depth instrs =

spectec/src/il2al/translate.ml

@@ -185,37 +185,8 @@ and translate_exp exp =
   (* property access *)
   | Il.DotE (inner_exp, ({it = Atom _; _} as atom)) ->
     accE (translate_exp inner_exp, dotP atom) ~at:at ~note:note
-  (* conacatenation of records *)
-  | Il.CompE (inner_exp, { it = Il.StrE expfields; _ }) ->
-    (* assumption: CompE is only used with at least one literal *)
-    let nonempty e = (match e.it with ListE [] | OptE None -> false | _ -> true) in
-    List.fold_left
-      (fun acc extend_exp ->
-        match extend_exp with
-        | {it = Il.Atom _; _} as atom, fieldexp ->
-          let extend_expr = translate_exp fieldexp in
-          if nonempty extend_expr then
-            extE (acc, [ dotP atom ], extend_expr, Back) ~at:at ~note:note
-          else
-            acc
-        | _ -> error_exp exp "AL record expression"
-      )
-      (translate_exp inner_exp) expfields
-  | Il.CompE ({ it = Il.StrE expfields; _ }, inner_exp) ->
-    (* assumption: CompE is only used with at least one literal *)
-    let nonempty e = (match e.it with ListE [] | OptE None -> false | _ -> true) in
-    List.fold_left
-      (fun acc extend_exp ->
-        match extend_exp with
-        | {it = Il.Atom _; _} as atom, fieldexp ->
-          let extend_expr = translate_exp fieldexp in
-          if nonempty extend_expr then
-            extE (acc, [ dotP atom ], extend_expr, Front) ~at:at ~note:note
-          else
-            acc
-        | _ -> error_exp exp "AL record expression"
-      )
-      (translate_exp inner_exp) expfields
+  (* concatenation of records *)
+  | Il.CompE (exp1, exp2) -> compE (translate_exp exp1, translate_exp exp2) ~at:at ~note:note
   (* extension of record field *)
   | Il.ExtE (base, path, v) -> extE (translate_exp base, translate_path path, translate_exp v, Back) ~at:at ~note:note
   (* update of record field *)
@@ -1386,7 +1357,7 @@ let translate_rules il =
   |> group_rules
   (* Translate reduction group into algorithm *)
   |> List.map translate_rgroup
-
+  
 let rec collect_def env def =
   let open Il in
   match def.it with
@@ -1424,3 +1395,4 @@ let translate il =
 
   let al = (translate_helpers il' @ translate_rules il') in
   List.map Transpile.remove_state al
+