[interpretation] Add support for addition between vectors.

src/interpretation.ml

@@ -220,6 +220,43 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
     | [ Term _t1; Term _t2 ] -> reconstruct ()
     | _ -> invalid_arg (error_message ls)
   in
+  let vplus : _ CRE.builtin =
+   fun engine ls vl ty ->
+    match vl with
+    | [
+     Term ({ t_node = Tapp (ls1, tl1); _ } as _t1);
+     Term ({ t_node = Tapp (ls2, _); _ } as _t2);
+    ] -> (
+      match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
+      | Vector v, Data (D_csv data) ->
+        let n = Option.value_exn (Language.lookup_vector v) in
+        assert (n = List.length data);
+        let ty_cst =
+          match ty with
+          | Some { ty_node = Tyapp (_, [ ty ]); _ } -> ty
+          | _ -> assert false
+        in
+        let csts =
+          List.map data ~f:(fun d ->
+            let cst = const_real_of_float (Float.of_string d) in
+            Term.t_const cst ty_cst)
+        in
+        let { env; _ } = CRE.user_env engine in
+        let args =
+          let plus =
+            (* TODO: generalize wrt the type of constants [csts]. *)
+            let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+            Theory.(ns_find_ls th.th_export [ Ident.op_infix ".+" ])
+          in
+          List.map2_exn tl1 csts ~f:(fun tl c ->
+            (Term.t_app_infer plus [ tl; c ], ty_cst))
+        in
+        let caisar_op = Vector (Language.create_vector env n) in
+        value_term (term_of_caisar_op ~args engine caisar_op ty)
+      | _ -> assert false)
+    | [ Term _t1; Term _t2 ] -> reconstruct ()
+    | _ -> invalid_arg (error_message ls)
+  in
   let vmapi : _ CRE.builtin =
    fun engine ls vl ty ->
     match vl with
@@ -345,6 +382,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
       [
         ([ Ident.op_get "" ] (* ([]) *), None, vget);
         ([ Ident.op_infix "-" ], None, vminus);
+        ([ Ident.op_infix "+" ], None, vplus);
         ([ "length" ], None, vlength);
         ([ "mapi" ], None, vmapi);
       ] );