Make basis know ^ (string concat.) in String and at top-level

Show that one can reason with it in cf_examples, though xlet_auto
doesn't cope at the crucial moment for reasons that are unclear to me.

basis/StringProgScript.sml

@@ -15,6 +15,8 @@ val _ = trans "implode" `implode`
 val _ = trans "size" `strlen`
 val _ = trans "concat" `mlstring$concat`
 val _ = trans "substring" `mlstring$substring`
+val result = translate strcat_def;
+val _ = trans "^" `mlstring$strcat`
 
 val result = translate explode_aux_def;
 val result = translate explode_def;
@@ -33,7 +35,6 @@ val extract_side_thm = Q.prove(
   `!s i opt. extract_side s i opt`,
   rw [extract_side_def, MIN_DEF] ) |> update_precondition
 
-val result = translate strcat_def;
 
 val result = translate concatWith_aux_def;
 val _ = next_ml_names := ["concatWith"];

basis/mlbasicsProgScript.sml

@@ -46,6 +46,9 @@ val _ = trans "~" `\i. - (i:int)`
 val _ = trans "=" `\x1 x2. x1 = x2:'a`
 val _ = trans "not" `\x. ~x:bool`
 val _ = trans "<>" `\x1 x2. x1 <> (x2:'a)`
+val _ = trans "^" `mlstring$strcat`
+
+val _ = remove_ovl_mapping "strcat" {Name = "strcat", Thy = "mlbasicsProg"}
 
 val _ = append_prog
   ``[Tdec (mk_binop ":=" Opassign);

characteristic/cfTacticsBaseLib.sml

@@ -175,7 +175,8 @@ fun pick_name str =
   if str = "-" then "minus" else
   if str = "*" then "times" else
   if str = "!" then "deref" else
-  if str = ":=" then "assign" else str (* name is fine *)
+  if str = ":=" then "assign" else
+  if str = "^" then "strcat" else str (* name is fine *)
 
 (* for debugging
 val st = (basis_st())

characteristic/examples/cf_examplesScript.sml

@@ -351,4 +351,25 @@ val bytearray_fromlist_spec = Q.prove (
   xapp \\ fs [] \\ xsimpl \\ fs [LENGTH_NIL_SYM, LENGTH_REPLICATE]
 )
 
+val strcat_foo = process_topdecs
+  `fun strcat_foo r = r := !r ^ "foo"`
+
+val st = ml_progLib.add_prog strcat_foo pick_name basis_st
+
+val xlet_auto = cfLetAutoLib.xlet_auto
+
+val strcat_foo_spec = Q.prove (
+  `!rv sv s.
+     STRING_TYPE s sv ==>
+     app (p:'ffi ffi_proj) ^(fetch_v "strcat_foo" st) [rv]
+       (REF rv sv)
+       (POSTv uv. SEP_EXISTS sv'.
+            &(UNIT_TYPE () uv /\ STRING_TYPE (s ^ implode "foo") sv') *
+            REF rv sv')`,
+  xcf "strcat_foo" st >>
+  xlet_auto >- xsimpl >>
+  xlet `POSTv sv'. &(STRING_TYPE (s ^ implode "foo") sv') * rv ~~> sv`
+  >- (xapp >> xsimpl >> simp[mlstringTheory.implode_def] >> metis_tac[]) >>
+  rveq >> xapp >> xsimpl);
+
 val _ = export_theory();