(fix) Aggressive extraction for String.append

Signed-off-by: Jerome Simeon <[email protected]>

Makefile

@@ -94,7 +94,6 @@ cleanall-npm: clean-npm
 clean: Makefile.coq
 	- @$(MAKE) clean-npm
 	- @$(MAKE) clean-extraction
-	- @$(MAKE) clean-mechanization
 	- @$(MAKE) -C packages/ergo-compiler clean
 	- @$(MAKE) -C packages/ergo-engine clean
 	- @$(MAKE) -C packages/ergo-cli clean

extraction/ErgoExtraction.v

@@ -18,13 +18,19 @@
 
 Require Extraction.
 Extraction Language OCaml.
-Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlNatInt ExtrOcamlZInt.
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlString.
+Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlZInt.
 Require Import Qcert.Extraction.ExtrOcamlFloatNatIntZInt.
+
 Extraction Blacklist String List.
 
 Require Import Qcert.Utils.Digits.
 Extract Constant Digits.nat_to_string10 => "(fun x -> Util.char_list_of_string (string_of_int x))".
 
+Extract Constant String.append => "(fun s1 s2 -> Util.char_list_append s1 s2)".
+
 (* Ergo modules *)
 Require ErgoCompiler.
 Extraction "ErgoComp" ErgoCompiler.ErgoCompiler.

extraction/Makefile

@@ -95,7 +95,7 @@ $(BIN1): $(ATDS) extracted/StaticConfig.ml extracted/ErgoComp.ml extracted/ErgoC
 	$(OCAMLBUILD) $(MENHIRFLAG) -Is extracted -Is src $(BIN1)
 
 ## JavaScript
-$(DIST2): $(ATDS) extracted/StaticConfig.ml extracted/ErgoComp.ml extracted/ErgoComp.mli _build_js/$(BYTE2)
+$(DIST2): $(ATDS) extracted/StaticConfig.ml extracted/ErgoComp.ml extracted/ErgoComp.mli _build_js/$(BYTE2) $(DIST1)
 	js_of_ocaml _build_js/$(BYTE2) -o _build_js/$(BIN2)
 	cp _build_js/$(BIN2) $(DIST2)
 

extraction/ergocoreJS.ml

@@ -102,7 +102,7 @@ let ergo_compile input =
     begin try
       Js.to_string input##.ergo
     with exn ->
-      ergo_raise (ergo_system_error ("[Compilation Error] Couldn't load contract: "^(Printexc.to_string exn)))
+      ergo_raise (ergo_system_error ("Couldn't load contract: "^(Printexc.to_string exn)))
     end
   in
   begin try

extraction/src/Util.ml

@@ -26,23 +26,18 @@ type dnrc_logger_token_type = string
 (* Data type conversions between Coq and OCaml *)
 
 let string_of_char_list l =
-  begin try
-    let b = Bytes.create (List.length l) in
-    let i = ref 0 in
-    List.iter (fun c -> Bytes.set b !i c; incr i) l;
-    Bytes.to_string b
-  with
-  | exn -> raise (Failure ("Error in string_of_char_list: " ^ (Printexc.to_string exn)))
-  end
+  let b = Bytes.create (List.length l) in
+  let i = ref 0 in
+  List.iter (fun c -> Bytes.set b !i c; incr i) l;
+  Bytes.to_string b
 
 let char_list_of_string s =
-  begin try
-    let rec exp i l =
-      if i < 0 then l else exp (i - 1) (s.[i] :: l) in
-    exp (String.length s - 1) []
-  with
-  | exn -> raise (Failure ("Error in char_list_of_string: " ^ (Printexc.to_string exn)))
-  end
+  let rec exp i l =
+    if i < 0 then l else exp (i - 1) (s.[i] :: l) in
+  exp (String.length s - 1) []
+
+let char_list_append s1 s2 =
+  char_list_of_string ((string_of_char_list s1) ^ (string_of_char_list s2))
 
 let coq_Z_of_int i = i
 
@@ -205,3 +200,9 @@ let global_replace const_expr repl text =
 
 let filename_append dir path =
   List.fold_left Filename.concat dir path
+
+let loc_error s f x =
+  begin try f x with
+  | Failure exn -> raise (Failure exn)
+  | exn -> raise (Failure ("[In " ^ s ^ "]" ^ (Printexc.to_string exn)))
+  end

extraction/src/Util.mli

@@ -22,6 +22,7 @@
 
 val string_of_char_list : char list -> string
 val char_list_of_string : string -> char list
+val char_list_append : char list -> char list -> char list
 val coq_Z_of_int : int -> int
 
 (*******)
@@ -71,3 +72,5 @@ val global_replace : string -> string -> string -> string
 val filename_append : string -> string list -> string
 (** [filename_append dir subdirlist] Append sub-directories to a root directory *)
 
+val loc_error : string -> ('a -> 'b) -> 'a -> 'b
+

mechanization/Version.v

@@ -17,7 +17,7 @@
 Require Import String.
 
 Section Version.
-    Definition ergo_version := "0.0.59"%string.
+    Definition ergo_version := "0.0.60"%string.
 
 End Version.