From a3a05ed727e2e7d8f0f3e54a444c556dbe2dfd83 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 3 Jul 2018 14:13:19 +0100
Subject: Fill in a few Coq functions for CHERI from the MIPS prelude

---
 mips/mips_extras.v | 8 ++++++++
 mips/prelude.sail  | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 94e4779c..49899107 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -152,3 +152,11 @@ Qed.
 
 Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r.
 Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r.
+
+
+Definition print_endline (_:string) : unit := tt.
+Definition prerr_endline (_:string) : unit := tt.
+Definition prerr_string (_:string) : unit := tt.
+Definition putchar {T} (_:T) : unit := tt.
+Require DecimalString.
+Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
diff --git a/mips/prelude.sail b/mips/prelude.sail
index b3349799..697ef74a 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -55,7 +55,7 @@ val "prerr_string" : string -> unit
 
 val putchar = {c:"sail_putchar", _:"putchar"} : forall ('a : Type). 'a -> unit
 
-val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string
+val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string
 
 val string_of_int = "string_of_int" : int -> string
 /* Unused?
-- 
cgit v1.2.3