Open the string scope by default

dhilst · Jan 21, 2020 · 87516ae · 87516ae
1 parent 53a6b7b
commit 87516ae
Show file tree

Hide file tree

Showing 30 changed files with 42 additions and 13 deletions.
diff --git a/src/ast.ml b/src/ast.ml
@@ -45,6 +45,7 @@ let to_coq (ast : t) : SmartPrint.t =
   concat (List.map (fun d -> d ^^ newline) [
     !^ "(** Generated by coq-of-ocaml *)";
     !^ "Require Import OCaml.OCaml." ^^ newline;
+    !^ "Local Open Scope string_scope.";
     !^ "Local Open Scope Z_scope.";
     !^ "Local Open Scope type_scope.";
     !^ "Import ListNotations." ^^ newline;

diff --git a/src/constant.ml b/src/constant.ml
@@ -60,5 +60,5 @@ let rec to_coq (c : t) : SmartPrint.t =
         Buffer.add_string b "\"\""
       else
         Buffer.add_char b c);
-    nest (double_quotes (!^ (Buffer.contents b)) ^^ !^ "%" ^^ !^ "string")
+    double_quotes (!^ (Buffer.contents b))
   | Warn (c, message) -> group (Error.to_comment message ^^ newline ^^ to_coq c)
diff --git a/tests/builtin_types.v b/tests/builtin_types.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -18,7 +19,7 @@ Definition c3 : ascii := "009" % char.
 
 Definition c4 : ascii := """" % char.
 
-Definition s : string := "hi\n\t:)\""" % string.
+Definition s : string := "hi\n\t:)\""".
 
 Definition b1 : bool := false.
 

diff --git a/tests/cfml_set.v b/tests/cfml_set.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/first_class_modules.v b/tests/first_class_modules.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -116,7 +117,7 @@ End Triple.
 Definition tripe : {'[a, b, c, bar] : _ & Triple.signature a b c bar} :=
   let va := 0 in
   let vb := false in
-  let vc := "" % string in
+  let vc := "" in
   let foo := 12 in
   existT _ [_, _, _, _]
     {|

diff --git a/tests/free_type_variables.v b/tests/free_type_variables.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/function_with_explicit_types.v b/tests/function_with_explicit_types.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/functor.v b/tests/functor.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/functor_application.v b/tests/functor_application.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/gadts.v b/tests/gadts.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/interface.v b/tests/interface.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/let_rec_and.v b/tests/let_rec_and.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/lets.v b/tests/lets.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/local_vs_global_name.v b/tests/local_vs_global_name.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/matching.v b/tests/matching.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/modules.v b/tests/modules.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/mutual_types.v b/tests/mutual_types.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/open_modules.v b/tests/open_modules.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/operators.v b/tests/operators.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/pervasives_basics.v b/tests/pervasives_basics.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -22,7 +23,7 @@ Definition n4 : Z := Z.lxor (Z.lor (Z.land 5 7) 3) 9.
 
 Definition n5 : Z := Z.add (Z.shiftl 156 4) (Z.shiftr 12 1).
 
-Definition s : string := String.append "ghj" % string "klm" % string.
+Definition s : string := String.append "ghj" "klm".
 
 Definition c : Z := OCaml.Stdlib.int_of_char "c" % char.
 

diff --git a/tests/pervasives_more.v b/tests/pervasives_more.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -76,19 +77,19 @@ Definition n_lsl : Z := Z.shiftl 12 13.
 
 Definition n_lsr : Z := Z.shiftr 12 13.
 
-Definition ss : string := String.append "begin" % string "end" % string.
+Definition ss : string := String.append "begin" "end".
 
 Definition n_char : Z := OCaml.Stdlib.int_of_char "c" % char.
 
 Definition i : unit := OCaml.Stdlib.ignore 12.
 
 Definition s_bool : string := OCaml.Stdlib.string_of_bool false.
 
-Definition bool_s : bool := OCaml.Stdlib.bool_of_string "false" % string.
+Definition bool_s : bool := OCaml.Stdlib.bool_of_string "false".
 
 Definition s_n : string := OCaml.Stdlib.string_of_int 12.
 
-Definition n_s : Z := OCaml.Stdlib.int_of_string "12" % string.
+Definition n_s : Z := OCaml.Stdlib.int_of_string "12".
 
 Definition n1 : Z := fst (12, 13).
 

diff --git a/tests/polymorphic_function.v b/tests/polymorphic_function.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/pre_defined_types.v b/tests/pre_defined_types.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -22,6 +23,6 @@ Definition o2 : option Z := Some 12.
 
 Definition c : ascii := "g" % char.
 
-Definition s1 : string := "bla" % string.
+Definition s1 : string := "bla".
 
-Definition s2 : string := "\""" % string.
+Definition s2 : string := "\""".
diff --git a/tests/records.v b/tests/records.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -18,10 +19,10 @@ Module SizedString.
 End SizedString.
 
 Definition r : SizedString.t :=
-  {| SizedString.t.name := "gre" % string; SizedString.t.size := 3 |}.
+  {| SizedString.t.name := "gre"; SizedString.t.size := 3 |}.
 
 Definition r' : SizedString.t :=
-  {| SizedString.t.name := "haha" % string; SizedString.t.size := 4 |}.
+  {| SizedString.t.name := "haha"; SizedString.t.size := 4 |}.
 
 Definition s : Z := Z.add (SizedString.t.size r) (SizedString.t.size r').
 
@@ -109,7 +110,7 @@ Module ConstructorWithRecords.
 
   Definition l : loc := {| loc.x := 12; loc.y := 23 |}.
 
-  Definition foo : t := Foo {| t.Foo.name := "foo" % string; t.Foo.size := 12 |}.
+  Definition foo : t := Foo {| t.Foo.name := "foo"; t.Foo.size := 12 |}.
 
   Definition f (x : t) : Z :=
     match x with

diff --git a/tests/recursion.v b/tests/recursion.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/recursion_more.v b/tests/recursion_more.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/sum_types.v b/tests/sum_types.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/tree.v b/tests/tree.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.

diff --git a/tests/tuples.v b/tests/tuples.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.
@@ -10,7 +11,7 @@ Unset Guard Checking.
 
 Definition t0 : unit := tt.
 
-Definition t1 : ascii * string := ("c" % char, "one" % string).
+Definition t1 : ascii * string := ("c" % char, "one").
 
 Definition t2 : Z * Z * Z * bool * bool := (1, 2, 3, false, true).
 

diff --git a/tests/type_synonyms.v b/tests/type_synonyms.v
@@ -1,6 +1,7 @@
 (** Generated by coq-of-ocaml *)
 Require Import OCaml.OCaml.
 
+Local Open Scope string_scope.
 Local Open Scope Z_scope.
 Local Open Scope type_scope.
 Import ListNotations.